This page is dedicated to the case studies related to the submitted paper "Merge and Conquer: State Merging in Parametric Timed Automata".
The version of IMITATOR used to compute the case studies is IMITATOR 2.6.1.
It can be downloaded from the download page.
We present in the following table a list of case studies computed using the inverse method using the above implementation of IMITATOR.
We give from left to right the name of the case study (with a link to the IMITATOR model), the reference, the reference valuation file pi0, the number |A| of automata in parallel, the number |X| of clocks, the number |P| of parameters, and for each of the 2 algorithms, the number |S| of states computed, the number |T| of transitions computed, the computation time t in seconds (excluding the generation of the graphical outputs), and whether the result is complete or maybe not complete. In the last 3 columns, we compare the results: first, we divide the number of states in IM by the number of states in IMMerge' and multiply by 100 (hence, a number smaller than 100 denotes an improvement of IMMerge'); second, we perform the same comparison for the computation time; the last column indicates whether K = Kmerge' or K ⊂ Kmerge'.
Experiments were performed on a KUbuntu 12.10 64 bits system running on an Intel Core i7 CPU 2.67GHz with 4 GiB of RAM.
| Case study | Reference | Pi0 | |X| | |P| | IM | IMMerge' | Comparison | ||||||||||
|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|
| |S| | |T| | t | Complete | Result | |S| | |T| | t | Complete | Result | States | time | K | |||||
| And-Or | [CC05] | AndOr.pi0 | 4 | 12 | 11 | 11 | 0.052 s | Yes | log – states – traces | 9 | 9 | 0.056 s | Yes | log – states – trace set | 82 | 108 | = |
| Flip-Flop | [CC07] | flipflop.pi0 | 5 | 12 | 11 | 10 | 0.06 s | Yes | log – states – traces | 9 | 9 | 0.057 s | Yes | log – states – trace set | 82 | 95 | = |
| Latch | [Andre10] | latchValmem.pi0 | 8 | 13 | 18 | 17 | 0.083 s | ? | log – states – traces | 12 | 12 | 0.069 s | ? | log – states – trace set | 67 | 83 | = |
| SPSMALL memory | [AS13] | spsmall.pi0 | 10 | 26 | 31 | 30 | 0.618 s | Yes | log – states – traces | 31 | 30 | 0.613 s | Yes | log – states – trace set | 100 | 99 | = |
| SIMOP | [AS13] | simop.pi0 | 8 | 7 | - | - | Out of memory | - | - | 172 | 262 | 2.52 s | ? | log – states – trace set | 0 | 0 | - |
| BRP | [DKRT97] | brp.pi0 | 7 | 6 | 429 | 474 | 3.5 s | Yes | log – states – traces | 426 | 473 | 4.3 s | Yes | log – states – trace set | 99 | 123 | = |
| CSMA/CD bc2 | [KNSW07] | csmacdPrism.pi0 | 3 | 3 | 301 | 462 | 0.514 s | Yes | log – states – traces | 300 | 461 | 0.574 s | Yes | log – states – trace set | 100 | 112 | = |
| CSMA/CD bc6 | [KNSW07] | csmacdPrism6.pi0 | 3 | 3 | 13365 | 14271 | 18.3 s | Yes | log – states – traces | 13365 | 14271 | 25.4 s | Yes | log – states – trace set | 100 | 139 | = |
| RCP | [HRSV02] | RCP.pi0 | 5 | 6 | 327 | 518 | 0.748 s | Yes | log – states – traces | 115 | 186 | 0.684 s | Yes | log – states – trace set | 35 | 91 | = |
| WLAN | [KNS02] | wlan.pi0 | 2 | 8 | - | - | Out of memory | - | - | 8430 | 15152 | 2137 s | Yes | log – states – trace set | 0 | 0 | - |
| ABT | [FLMS12] | astrium_basic_thermal_fp.pi0 | 7 | 7 | 63 | 62 | 0.344 s | ? | log – states – traces | 63 | 62 | 0.335 s | ? | log – states – trace set | 100 | 97 | = |
| AM02 | [AM02] | am02.pi0 | 3 | 4 | 182 | 215 | 0.369 s | Yes | log – states – traces | 53 | 70 | 0.112 s | Yes | log – states – trace set | 29 | 30 | ⊂ |
| BB04 | [BB04] | bb.pi0 | 6 | 7 | 806 | 827 | 28 s | ? | log – states – traces | 141 | 145 | 3.15 s | ? | log – states – trace set | 17 | 11 | = |
| CTC | [???] | concurent_tasks_chain.pi0 | 15 | 21 | 1364 | 1363 | 88.9 s | Yes | log – states – traces | 215 | 264 | 17.6 s | Yes | log – states – trace set | 16 | 20 | = |
| LA02 | [Tamura07] | LA02_2.pi0 | 3 | 5 | 6290 | 8023 | 751 s | ? | log – states – traces | 383 | 533 | 17.7 s | Yes | log – states – trace set | 6 | 2 | ⊂ |
| LPPRC10 | [LPPRC10] | hppr10_audio.pi0 | 4 | 7 | 78 | 102 | 0.39 s | ? | log – states – traces | 31 | 40 | 0.251 s | ? | log – states – trace set | 40 | 64 | = |
| M2.4 | [AAM06] | maler_2_4.pi0 | 3 | 8 | 1497 | 1844 | 8.89 s | Yes | log – states – traces | 119 | 181 | 0.374 s | Yes | log – states – trace set | 8 | 4 | ⊂ |
The AndOr case study consists in an "AND" gate linked to an "OR" gate in a cyclic manner.
The flip-flop case study consists in a flip-flop circuit made of 4 components.
The latch case study is a sery of gates simulating the behavior of a latch, designed by ST-Microelectronics during a joint project with LSV.
The SPSMALL case study is the model of an abstraction of an asynchronous circuit designed and sold by ST-Microelectronics.
This case study is a networked automation system studies in the framework of the SIMOP project (LSV and LURPA, ENS de Cachan, France).
BRP is the bounded retransmission protocol.
The 2 CSMA/CD models correspond to the non-probabilistic version of the model described in [KNSW07]. The differences between our two versions is the value of the maximum backoff (2 and 6 respectively).
RCP is the root contention protocol of the IEEE 1394 (“FireWire”) High Performance Serial Bus, considered in the parametric framework in [HRSV02].
WLAN corresponds to the IEEE 802.11 Wireless Local Area Network Protocol.
The ABT case study is a problem of scheduling 3 periodic tasks on a single processor studied in the setting of a collaboration between Astrium and LSV.
The AM02 case study is a problem of preemptive job-shop scheduling with two jobs on three machines.
The BB04 case study corresponds to a three task example from [BB04, Section III, table 1]. It is an FP scheduling problem with three cyclic tasks on one machine.
The CTC (concurrent task chain) case study does not use cyclic tasks but instead has a 4 task chain and a concurrent 3 task chain. Each task in a chain cannot start until the previous one has not terminated. Each task in each chain has a given fixed priority. A scheduler assigns which task has the computational time with a FP policy.
The LPPRC10 is a two-cyclic-tasks problem with an EDF scheduler.
The M2.4 case study is a problem of non-preemptive scheduling. Two sequences of tasks have to run concurrently trough 4 machines. The goal is to schedule the tasks to meet the deadline on the overall execution time.
For all case studies, the standard inverse method IM was called using the following options:
> IMITATOR case_study.imi case_study.pi0 -with-dot -with-log
For all case studies, the inverse method with merging IMMerge' was called using the following options:
> IMITATOR case_study.imi case_study.pi0 -merge -with-dot -with-log
