Homepage: http://www.daxc.de/eth
Formulas (SPIN syntax) | Results on negated formulas | |
12 formulas from Etessami and Holzmann [bib] | eh_spin.txt | survey_eh.txt |
27 formulas from Somenzi and Bloem [bib] | sb_spin.txt | survey_sb.txt |
50 patterns of commonly used specification formulas [link] | patterns_spin.txt | survey_patterns.txt |
# of formulas | safety | guarantee | obligation | |
eh | 12 | 3 (25%) | 1 (8%) | 4 (33%) |
sb | 27 | 8 (30%) | 9 (33%) | 15 (56%) |
patterns | 55 | 36 (65%) | 1 (2%) | 40 (73%) |
For both experiments we used a computer with an Intel Pentium 4 processor with 3GHz and with 4GBytes of main memory.
Used LTL to Automata Translators:
Each row corresponds to the i-th formula in patterns40_spin.txt. The numbers denote the sizes of the resulting automata.
1 | 2 | 3 | 4 | 5 | 6 | 7 | 8 | 9 | 10 | 11 | 12 | 13 | 14 | 15 | 16 | 17 | 18 | 19 | 20 | |
SPIN | 2 | 3 | 3 | 4 | 6 | 1 | 6 | 3 | 7 | 36 | -- | -- | -- | -- | 2 | 3 | 3 | 4 | 6 | 4 |
TMP | 2 | 3 | 3 | 4 | 3 | 1 | 2 | 3 | 3 | 6 | 7 | 7 | 8 | 7 | 2 | 3 | 3 | 4 | 3 | 4 |
LTL2BA | 2 | 3 | 3 | 4 | 3 | 1 | 2 | 3 | 3 | 6 | 7 | 12 | 8 | 7 | 2 | 3 | 3 | 4 | 3 | 4 |
MODELLA | 2 | 3 | 3 | 5 | 4 | 1 | 2 | 2 | 4 | 6 | 7 | 7 | 9 | 11 | 2 | 3 | 3 | 5 | 4 | 4 |
WDBA | 2 | 3 | 3 | 4 | 3 | 1 | 2 | 2 | 3 | 6 | 7 | 7 | 8 | 7 | 2 | 3 | 3 | 4 | 3 | 4 |
21 | 22 | 23 | 24 | 25 | 26 | 27 | 28 | 29 | 30 | 31 | 32 | 33 | 34 | 35 | 36 | 37 | 38 | 39 | 40 | |
SPIN | 3 | 4 | 6 | 7 | 8 | 14 | 6 | 40 | 7 | 15 | 8 | 4 | 82 | 5 | 16 | 9 | 15 | 16 | 15 | -- |
TMP | 3 | 4 | 3 | 3 | 4 | 3 | 4 | 4 | 5 | 4 | 3 | 4 | 22 | 5 | 4 | 5 | 4 | 5 | 4 | 5 |
LTL2BA | 3 | 4 | 3 | 3 | 4 | 3 | 4 | 4 | 5 | 4 | 4 | 4 | 10 | 5 | 14 | 5 | 4 | 5 | 4 | 5 |
MODELLA | 3 | 5 | 4 | 3 | 6 | 3 | 4 | 4 | 6 | 5 | 4 | 5 | 5 | 7 | 23 | 5 | 4 | 8 | 4 | 10 |
WDBA | 3 | 4 | 3 | 3 | 4 | 3 | 4 | 4 | 5 | 4 | 3 | 4 | 4 | 5 | 4 | 5 | 4 | 5 | 4 | 5 |
Formulas (SPIN syntax) | |
50 patterns of commonly used specification formulas [link] | patterns_spin.txt |
40 obligation formulas from patterns | patterns40_spin.txt |
40 automata sizes for SPIN | sizes40_spin.txt |
40 automata sizes for TMP | sizes40_tmp.txt |
40 automata sizes for LTL2BA | sizes40_ltl2ba.txt |
40 automata sizes for MODELLA | sizes40_modella.txt |
40 automata sizes for WDBA | sizes40_wdba.txt |
A detailed description can be found at http://anna.fi.muni.cz/models/cgi/model_info.cgi?name=bopdp
Specification:
[] ( (p0 /\ p1) -> ((! p1) V (p0 \/ (! p1))) )
Automata generated by the translators:
Models:
SPIN | TMP | LTL2BA | MODELLA | WDBA | |
bopdp.7.pm | 0m05/172 MB | 0m05/172 MB | 0m05/172 MB | 0m05/172 MB | 0m03/155 MB |
bopdp.14.pm | 0m21/367 MB | 0m21/367 MB | 0m21/367 MB | 0m21/367 MB | 0m13/297 MB |
bopdp.28.pm | 1m32/1146 MB | 1m32/1146 MB | 1m32/1146 MB | 1m32/1146 MB | 0m55/877 MB |
bopdp.56.pm* | 14m04/2856 MB | 14m04/2856 MB | 14m04/2856 MB | 14m04/2856 MB | 8m05/2112 MB |
A detailed description can be found at http://anna.fi.muni.cz/models/cgi/model_info.cgi?name=elevator2
Specification (SPIN syntax):
( [] (r0 -> (!p0 U (p0 U (!p0 U (p0 U (p0 /\ co)))))) )
Automata generated by the translators:
≤≥ ! (r0 -> (!p0 U (p0 U (!p0 U (p0 U (p0 /\ co))))))
".
Models:
SPIN | TMP | LTL2BA | MODELLA | WDBA | |
elevator2.1.pm | 0m00/112 MB | 0m00/368 MB | 0m00/240 MB | 0m01/368 MB | 0m00/240 MB |
elevator2.2.pm | 0m00/240 MB | 0m01/368 MB | 0m00/240 MB | 0m01/369 MB | 0m00/240 MB |
elevator2.3.pm | 5m57/1667 MB | 2m42/1182 MB | 2m42/1054 MB | 2m28/1149 MB | 2m26/1021 MB |
elevator2.4.pm* | >3000 MB | 6m41/2162 MB | 7m16/2107 MB | 7m19/2235 MB | 6m31/2034 MB |
elevator2.5.pm* |
A detailed description can be found in [bib].
Specifications (SPIN syntax):
( [] ( ! t -> ( ( ! p U t ) \/ [] ! p ) ) )
Automata generated by the translators:
The model:
SPIN | TMP | LTL2BA | MODELLA | WDBA | |
giop3.pm | >3000 MB | 0m04/378 MB | 0m13/664 MB | >3000 MB | 0m06/350 MB |
A detailed description can be found in [bib].
The specifications:
( (((! g1) U (u1 || [] ! g1)) /\ []( o1 -> ((! g1) U (u1 || [] ! g1)))) )
( (((! g1) U (u1 || [] ! g1)) /\ []( o1 -> ((! g1) U (u1 || [] ! g1)))) /\ (((! g2) U (u2 || [] ! g2)) /\ []( o2 -> ((! g2) U (u2 || [] ! g2)))) )
Automata generated by the translators:
The model:
Performance (Time/Memory):SPIN | TMP | LTL2BA | MODELLA | WDBA | |
Specification 1* | 7m09/1058 MB | 7m07/1058 MB | 7m07/1058 MB | 7m10/1061 MB | 4m55/779 MB |
Specification 2* | 17m57/2003 MB | 14m25/2003 MB | 14m23/2003 MB | 14m09/2003 MB | 5m17/788 MB |