This page is dedicated to the case studies related to the paper Dynamic Clock Elimination 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 2 columns, we compare the results: first, we divide the number of states in IM by the number of states in IMdyn and multiply by 100 (hence, a number smaller than 100 denotes an improvement of IMdyn); second, we perform the same comparison for the computation time.
Experiments were performed on a KUbuntu 13.04 64 bits system running on an Intel Core i7 CPU 2.67GHz with 4 GiB of RAM.
| Case study | Reference | Pi0 | |X| | |P| | IM | IMdyn | Comparison | |||||||||
|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|
| |S| | |T| | t | Complete | Result | |S| | |T| | t | Complete | Result | States | time | |||||
| Figure 2 | [Andre13] | loopingDynamic.pi0 | 2 | 2 | - | - | Loop | - | - | 2 | 2 | 0.007 s | Yes | log – states – trace set | 0 | 0 |
| Figure 3 | [Andre13] | exClockElimination.pi0 | 2 | 2 | - | - | Loop | - | - | 6 | 8 | 0.006 s | Yes | log – states – trace set | 0 | 0 |
| And-Or | [CC05] | AndOr.pi0 | 4 | 12 | 11 | 11 | 0.047 s | Yes | log – states – traces | 11 | 11 | 0.05 s | Yes | log – states – trace set | 100 | 106 |
| SPSMALL memory | [AS13] | spsmall.pi0 | 10 | 26 | 31 | 30 | 0.58 s | Yes | log – states – traces | 31 | 30 | 0.584 s | Yes | log – states – trace set | 100 | 101 |
| Train | [AHV93] | TrainAHV93.pi0 | 3 | 6 | 78 | 94 | 0.1 s | Yes | log – states – traces | 61 | 76 | 0.072 s | Yes | log – states – trace set | 78 | 72 |
| BRP | [DKRT97] | brp.pi0 | 7 | 6 | 429 | 474 | 3.5 s | Yes | log – states – traces | 426 | 473 | 3.21 s | Yes | log – states – trace set | 99 | 92 |
| CSMA/CD bc6 | [KNSW07] | csmacdPrism6.pi0 | 3 | 3 | 13365 | 14271 | 19.6 s | Yes | log – states – traces | 13365 | 14271 | 19.5 s | Yes | log – states – trace set | 100 | 99 |
| RCP | [HRSV02] | RCP.pi0 | 5 | 6 | 327 | 518 | 0.68 s | Yes | log – states – traces | 181 | 282 | 0.41 s | Yes | log – states – trace set | 55 | 60 |
| AAM06 | [AAM06] | maler_2_4.pi0 | 3 | 8 | 1497 | 1844 | 8.28 s | Yes | log – states – traces | 768 | 997 | 2.92 s | Yes | log – states – trace set | 51 | 35 |
| AM02 | [AM02] | am02.pi0 | 3 | 4 | 182 | 215 | 0.392 s | Yes | log – states – traces | 182 | 215 | 0.386 s | Yes | log – states – trace set | 100 | 98 |
| BB04 | [BB04] | bb.pi0 | 6 | 7 | 806 | 827 | 25.4 s | ? | log – states – traces | 806 | 827 | 27.2 s | ? | log – states – trace set | 100 | 107 |
| CTC | [???] | concurent_tasks_chain.pi0 | 15 | 21 | 1364 | 1363 | 83.4 s | Yes | log – states – traces | 201 | 291 | 2.52 s | Yes | log – states – trace set | 15 | 3 |
| LA02 | [Tamura07] | LA02_2.pi0 | 3 | 5 | 6290 | 8023 | 710 s | ? | log – states – traces | 4932 | 7154 | 473 s | ? | log – states – trace set | 78 | 67 |
| LPPRC10 | [LPPRC10] | hppr10_audio.pi0 | 4 | 7 | 78 | 102 | 0.375 s | ? | log – states – traces | 78 | 102 | 0.395 s | ? | log – states – trace set | 100 | 105 |
These 2 examples are presented in [Andre13].
The AndOr case study consists in an "AND" gate linked to an "OR" gate in a cyclic manner.
The SPSMALL case study is the model of an abstraction of an asynchronous circuit designed and sold by ST-Microelectronics.
This case study is classical train-gate-controller.
BRP is the bounded retransmission protocol.
The CSMA/CD model corresponds to the non-probabilistic version of the model described in [KNSW07] with a maximum backoff of 6.
RCP is the root contention protocol of the IEEE 1394 (“FireWire”) High Performance Serial Bus, considered in the parametric framework in [HRSV02].
The AAM06 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.
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.
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 dynamic clock elimination IMdyn was called using the following options:
> IMITATOR case_study.imi case_study.pi0 -dynamic-elimination -with-dot -with-log
