This page shows that HyTech sometimes crashes due to its intrinsic limitations (floating-point arithmetics, static composition of PTA), whereas IMITATOR may be (much) more efficient.
We do not claim the superiority of IMITATOR to HyTech, but simply that some optimization or features are missing in HyTech, leading to memory overflows.
We also recall that HyTech was developed in the late 90s, more than 15 years before IMITATOR, and that it generalizes to hybrid systems, whereas IMITATOR is specific to timed systems.
We consider the following case study: the SPSMALL memory developed and commercialized by ST-Microelectronics [CEFX09][Andre10].
For this case study, IMITATOR terminates after 0.079 second after exploring 31 states, whereas HyTech crashes by memory overflow before even starting the analysis.
The remainder of this Web page gives more details and explanations.
The version of HyTech used to perform the analysis is HyTech v1.04f (which, to the best of our knowledge, is the latest version).
The exact binary used can be downloaded from here.
The version of IMITATOR used to perform the analysis is IMITATOR 2.6.1.
It can be downloaded from the download page.
Experiments were performed on a KUbuntu 13.10 64 bits system running on an virtual machine (Virtualbox) itself running on a Macbook pro 13' 2013, with 1.5 GiB of available RAM.
We use only one case study (more case studies may be added some day).
This case study is an abstraction modeling the SPSMALL memory developed and commercialized by ST-Microelectronics [CEFX09][Andre10]. More information is also available on the VHDL2TA Web page (in French).
Note that, since the syntax of IMITATOR is almost entirely based on the syntax of HyTech, it is easy to be convinced that the two models for each tool are the same.
The model is made of 10 automata, 10 clocks, no discrete (finite-domain) variable, and no parameter (although see remark below).
We consider here a complete state space exploration.
To summarize, IMITATOR terminates after 0.079 second after exploring 31 states, whereas HyTech crashes by memory overflow before even starting the analysis.
| Tool | Model | States | Transitions | Time | Memory | Log |
|---|---|---|---|---|---|---|
| HyTech | spsmall_blueb_lsv_nop.hy | - | - | - | overflow | spsmall-hytech.log |
| IMITATOR | spsmall_nop.imi | 31 | 30 | 0.079 s | 3.1 MiB | spsmall-imitator.log |
While HyTech crashed after occupying all the available memory (1.5 GiB), IMITATOR terminates within 0.079 second with a total memory occupancy of less than 4 MiB, after visiting only 31 states.
The main explanation is that HyTech seems to perform a static composition of all automata before starting the analysis; in fact, HyTech crashes before starting the analysis. In contrast, IMITATOR works on-the-fly, and the state space is here very small (31 states).
Another explanation is that 28 parameters are defined in the model, but all are valuated (constant). On the one hand, HyTech considers 28 parameters with constraints associating each parameter with a constant value. On the other hand, IMITATOR directly replaces all parameters with their respective constant, and hence handles 0 parameter. Statically replacing each parameter with its constant everywhere in the HyTech model leads to successful termination; but the static composition of automata still requires a huge memory (although less than 1.5 GiB). Finally note that IMITATOR is able to explore the whole state space with 28 parameters, at the cost of a longer analysis (several seconds), and several thousands states.
To the best of our knowledge, the very same algorithm (as described in [AHV93]) is implemented in both tools.
IMITATOR has been used here with no optimization (merging), no abstraction, no improved fixpoint condition, so as to be consistent with HyTech.
> ./hytech-v1.04f-Linux_static spsmall_blueb_lsv_nop.hy
> ./IMITATOR spsmall_nop.imi -mode reachability