Overview
HAT is a tool which can transform an LHA model into equivalent LTS model. Then users can use off-the-shelf LTS checkers to answer considerably difficult questions about the behavioral state space of LHA easily. So far, HAT supports the interaction with three mature LTS checkers which are, ARMC for both reachability analysis and termination analysis, Invgen and interproc for invariant generation.
Download
Please download the tool HAT from this link.
Notice: In order to perform the selected functionalities, please download and install the related LTS checkers and configure the directory of these tools in HAT in advance. You may download ARMC from here, download Invgen from here. For Interproc, as we slightly modified Interproc to make it available to accept the LTS files, please download our modified version from here. In order to run Interproc, you may need to install all the required library files for Interproc in advance.
Case Studies
The ha files we used in the experiment can download here
Here is the model we use inthe experiment
WLM
TCS
Motor
ARMC Based Reachability Checking Result
| Name | Time |
|---|---|
| WLM | 0.63s |
| TCS | 0.84s |
| Motor5 | 0.42s |
| Motor10 | 2.05s |
| Motor20 | 16.41s |
| Motor30 | 77.53s |
| Motor50 | 628.74s |
| Motor60 | 1501.93s |
| Motor70 | 3087.63s |
| Motor78 | N/A |
ARMC Based Termination Analysis Result
| Name | Time | Name | Time |
|---|---|---|---|
WLM |
4.74s |
WLM-tmnt |
1.60s |
TCS |
0.69s |
TCS-tmnt |
0.76s |
Motor5 |
1.45s |
Motor5-tmnt |
0.58s |
Motor6 |
2.63s |
Motor6-tmnt |
0.79s |
Motor7 |
4.12s |
Motor7-tmnt |
0.30s |
Motor8 |
5.77s |
Motor8-tmnt |
0.98s |
Motor9 |
9.54s |
Motor9-tmnt |
0.84s |
Motor10 |
15.32s |
Motor10-tmnt |
0.67s |
Motor20 |
1455.65s |
Motor20-tmnt |
2.00s |
Motor30 |
N/A |
Motor30-tmnt |
3.78s |
Motor40 |
N/A |
Motor40-tmnt |
7.45s |
Motor50 |
N/A |
Motor50-tmnt |
14.84s |
Motor60 |
N/A |
Motor60-tmnt |
25.36s |
Motor100 |
N/A |
Motor100-tmnt |
142.52s |
Interproc Based Invariant Generation Result
| Name | Box | Octagon | PPL |
|---|---|---|---|
| WLM | 0.40s | 0.31s | 0.97s |
| TCS | 0.40s | 0.94s | 0.82s |
| Motor3 | 0.34s | 0.26s | 0.15s |
| Motor4 | 0.58s | 0.88s | 0.54s |
| Motor5 | 0.44s | 0.64s | 3.21s |
| Motor6 | 0.47s | 0.74s | 42.53s |
| Motor7 | 0.52s | 1.26s | 2082.48s |
| Motor8 | 0.58 | 1.47s | N/A |
| Motor9 | 0.66s | 2.25s | N/A |
| Motor10 | 0.76s | 3.15s | N/A |
| Motor20 | 1.17s | 34.16s | N/A |
| Motor30 | 1.22s | 180.29s | N/A |
| Motor40 | 2.31s | N/A | N/A |
| Motor50 | 4.04s | N/A | N/A |
| Motor60 | 6.16s | N/A | N/A |
| Motor100 | 26.17s | N/A | N/A |
Snapshots
ARMC Based Reachability Checking
ARMC Based Termination Analysis
Interproc Based Invariant Generation
