Properties of State Spaces

Detailed Statistics

Back to main page

This page contains all generated state spaces together with the detailed statistics. State spaces are sorted according to tools which were used to generate them. For each tool we shortly report the used extraction method.


Tool Graphs     Selected graphs
SPIN 30 16
CADP 40 11
Murphi 13 8
mCRL 6 5
Divine 23 10
Maso 8 5
NuSMV 6 0
Other 19 0
Total 145 55

Because state spaces generated from simillar models are very simillar we have included only some state spaces in computation of overall statistics. The selected examples are marked by 'X'. The collumn 'Remarks' says what specific parameters (par), reduction (red), or model modifications (mod) have been used for generation of the specific graphs. POR means partial order reduction, MIN is strong bisimulation.

The summary of all reported parameters (and explanation of visualization) is here.

The state spaces can be downloaded by clicking on 'G'. The used format is very simple, each line contain (separated by spaces):

Note that some of these graphs are not simple (i.e. they cointain self-loops and multiedges). The reported statistics, however, consider simple versions of these graphs.

SPIN

Homepage http://spinroot.com/spin/whatispin.html
Specification language Promela (C-like protocol modelling language)
Extraction method Graphs were generated using BFS traversal of the state space (which is supported by version 4 of Spin). The pan.c file was preprocesed with flags '-DSAFETY -DNOCLAIM -DNOREDUCE -DCHECK -DVERBOSE -DSDUMP -DBFS' and the resulting file was slightly modified.
Examples from Spin distribution, Database of Promela models

Model Report Graph Size Remarks
Peterson protocol for N processes            
X petersonN G 30432 par: 3;
- petersonN.red G 26373 par: 3; red: POR;
Dining philosophers            
X phil5 G 54049 par: 5;
- phil5.red G 4275 par: 5; red: POR;
Leader election in unidirectional ring            
X leader G 15791 par: 5;
Snooping cache algorithm            
- snoopy G 61624
X snoopy.red G 14361 red: POR;
Flow control layer validation            
- pftp G 219167
X pftp.red G 137897 red: POR;
Bounded Retransmition Protocol            
X brp.red G 391312 red: POR;
Needham-Schroeder Public Key Protocol            
X n-s-original.red G 307218 red: POR; mod: original version;
- n-s-fixed.red G 376987 red: POR; mod: fixed version;
ITU-T multipoint communication service            
X smcs G 5904 par: 2;
- smcs.red G 1887 par: 2; red: POR;
Flight Guidance System            
X fgs G 57786
Concurrent sorting            
X sort G 107728 par: 7;
- sort6 G 22350 par: 6;
Model of cell-phone handoff strategy            
X mobile1 G 225670
- mobile2 G 25339 mod: simplified version;
- mobile1.red G 66812 red: POR;
- mobile2.red G 13924 red: POR; mod: simplified version;
Cambridge Ring Protocol            
X cambridge00 G 162530 par: 00; red: none;
- cambridge00.red G 7205 par: 00; red: POR;
- cambridge11.red G 482309 par: 11; red: POR;
Go-Back-N Sliding Window Protocol            
X sliding2 G 35861
ABP            
X test2-abp G 442
Token Ring            
- test2-ring3 G 350 par: 3;
X test2-ring-5 G 7744 par: 5;
Readers, writers            
X test2-rw6 G 936 par: 6;
Artificial example            
- counter G 4657

CADP

Homepage http://www.inrialpes.fr/vasy/cadp.html
Specification language LOTOS
Extraction method CADP toolkit can for given LOTOS input generate the state space in the bcg format (binary coded graph). This can be easily transformed into the text format.
Examples from CADP distribution (it contains several case studies done with CADP), VLTS benchmark suite (these examples were not included into statistics, because the VLTS page provides only bcg files without any information about the 'source' of these graphs (so a) we do not known whether these graphs are not from same/simillar sources as our other CADP examples, b) we cannot clasify them as toy/simple/complex)

Model Report Graph Size Remarks
Directory-based cache coherency protocol            
X cache G 70643
- cache.min G 545 red: MIN;
Car overtaking protocol            
X overtaking G 56482
- overtaking.min G 1470 red: MIN;
Reliable multicast protocol            
X rel_rel G 113590
INRES protocol            
- inres_protocol_int_4 G 2811 mod: version 4;
X inres_protocol_int_6 G 7887 mod: version 6;
Dynamic Reconfiguration Protocol            
- spec G 22486
Philips' Bounded Retransmission Protocol            
X brp_protocol G 60381
- brp_protocol.min G 487 red: MIN;
- brp_service G 117 mod: service description;
Distributed Leader Election Algorithms            
- EXPERIMENT_03 G 95352
Plain Old Telephony System            
- pots G 4526
HAVi leader election protocol            
X HAVi_asyn G 5107 mod: asynchronous;
- HAVi_sync G 1199 mod: synchronous;
IEEE 1394 high performance serial bus            
- scen3_correct_2.2 G 3889 par: 2,2; mod: version 3, correct;
X scen1_orig_3 G 43172 par: 3; mod: version 1, original;
- scen2_correct_2 G 272868 par: 2; mod: version 2, correct;
CO4 protocol for distributed knowledge bases            
X co4-3-1 G 25496
- co4-1a-3 G 3193
- co4-5-1 G 41641
Cluster File System            
X site123medium G 11031
- cfs123 G 3585 red: MIN;
Invoicing case study            
- inv2d-p0-r1-a1 G 4642 par: 0,1,1;
X inv2d-p0-r2-a1 G 16110 par: 0,2,1;
- inv2d-p0-r1-a2 G 12973 par: 0,1,2;
Alternating bit            
X bitalt G 270
- bitalt_service G 510 mod: service;
VLTS benchmark suite            
- vasy_10_56 G 10849
- vasy_18_73 G 18746
- vasy_25_25 G 25217
- vasy_5_9 G 5486
- vasy_66_1302 G 66929
- vasy_69_520 G 69754
- vasy_8_24 G 8879
- vasy_8_38 G 8921
- vasy_0_1 G 289
- cwi_1_2 G 1952
- vasy_1_4 G 1183
- vasy_116_368 G 116456

Murphi

Homepage http://verify.stanford.edu/dill/murphi.html
Specification language Guarded commands language
Extraction method Murphi generates for each input a binary file which performs the state space traversal and is able to output visited states. In order to obtain the full state space, this binary was run with options '-nosym -nomultiset -ndl -p'.
Examples from Murphi distribution

Model Report Graph Size Remarks
Parallel sorting            
X sort5 G 3000 par: 5;
Peterson's mutual exclusion alg.            
X peterson3 G 882
Distributed quering lock            
X mcslock1 G 7597 par: 3; mod: version1;
- mcslock2 G 1098 par: 2; mod: version2;
Scalable Coherent Interface (SCI)            
- sci G 725 par: cachesize=2,nummemories=1;
- sci2 G 18059 par: cachesize=1,nummemories=2;
X sci3 G 38034 par: cachesize=1,nummemories=1; mod: all instructions enabled;
Cache coherence protocol            
- cache3 G 577 par: 2;
X cache4 G 15703 par: 3;
Hardware arbiter            
X arbiter G 1778
Needham-Schroeder protocol            
X ns G 980
Dash protocol            
X eadash G 1694 par: 2,1; mod: elementary abstract;
- ldash G 740 par: 2,1; mod: concrete;

mCRL

Homepage http://homepages.cwi.nl/~mcrl/
Specification language Process algebra
Extraction method MCRL tool (specifically program instantiator) can generate for a given input a text description of corresponding state space (here called automaton).
Examples from MCRL distribution, http://homepages.cwi.nl/~mcrl/lift/

Model Report Graph Size Remarks
Modular hef system            
X hef_wrong G 15349
Chatbox            
X chatbox G 65536
Onebit sliding window protocol            
X onebit G 319732
Link Layer Protocol of the IEEE-1394 Serial Bus            
X 1394-fin G 371804
Distributed Lift System            
- lift3-modif G 7369 par: 3;
X lift4-modif G 129849 par: 4;

Divine

Homepage -
Specification language Comunicating Extended Finite State Machines
Extraction method Divine (Distributed Verification Engine) is an environment for easy implementation of (distributed) model-checking algorithms. Divine is developed at our laboratory, at this moment it is not publicly available.
Examples from manual modelling

Model Report Graph Size Remarks
MSMIE protocol            
- msmie-1-1 G 275 par: 1,1;
X msmie-1-2 G 1241 par: 1,2;
- msmie-2-2 G 4127 par: 2,2;
Communication protocols            
X abp G 11268 mod: abp;
- simple1 G 1512 mod: sends ack repetedly;
- simple2 G 1980 mod: sends ack once;
- naive G 648 mod: naive;
- brp-err G 105 par: 2; mod: brp with error;
- brp G 2349 par: 2; mod: brp;
X brp5 G 6093 par: 5; mod: brp;
Dining philosophers            
X phil-basic-6 G 728 par: 6;
- phil-basic-8 G 6560 par: 8;
- phil-left-6 G 729 par: 6; mod: left handed;
- phil-return-6 G 728 par: 6; mod: with return;
- phil-room-6 G 5049 par: 6; mod: with room;
Cabbage, goat, wolf puzzle            
X farmer2 G 52
Coffe machine            
X machine G 1539
Bridge puzzle            
X bridge-4-5102025 G 7637
Jobshop scheduling            
X small G 145494
Shuffle puzzle            
X shuffle-3x3 G 181450 par: 3x3;
Elevator            
- el_naive4 G 64 par: 4; mod: naive strategy;
- el_smallest3 G 1279 par: 3; mod: smallest strategy;
X el_fifo3 G 12192 par: 3; mod: fifo strategy;

Maso

Homepage -
Specification language MASO (very simple assembler like language)
Extraction method This is a very simple tool used by author for generating input data algorithms described in his master thesis.
Examples from manual modelling

Model Report Graph Size Remarks
Alternating bit protocol            
X abp G 11268
Token ring            
X ring5 G 7680 par: 5;
Adding Puzzle            
- puzzle20 G 10869 par: 20;
- puzzle30 G 21489 par: 30;
X puzzle50 G 56561 par: 50;
Elevator            
- elevator1 G 142757 mod: without arrays;
X elevator2 G 643298 mod: with arrays;
Aquarium example            
X pako G 6561

NuSMV

Homepage http://nusmv.irst.itc.it/
Specification language smv input language
Extraction method The NuSMV is able to print all reachable states. In order to obtain transitions as well, one has to make a small modification in the corresponding function (print_states in compileEncode.c). Since there is not a unique initial state, we pick only one of them and then restrict the resulting state space to state reachable from this state.
Examples from NuSMV distribution

Model Report Graph Size Remarks
Distributed memory exclusion            
- dme1 G 6579
Synchronous arbiter            
- syncarb5 G 5120
Data driven pipeline            
- periodic G 1000
Alternating bit protocol            
- abp2 G 408
Snoopy cache            
- snoopy-fake G 288
Adder (circuit)            
- adder G 1152

Other

Homepage -
Specification language These are some non-model-checking graphs
Extraction method ad hoc
Examples from Stanford graph base, randomly generated

Model Report Graph Size Remarks
Five Letter Words            
- words G 4493
North American Cities            
- mile400 G 106 par: 400;
Roget's Thesaurus            
- roget G 946
Random            
- random_1_3 G 942 par: N=1000,M=3000;
- random_1_5 G 992 par: N=1000,M=5000;
- random_30_4 G 29435 par: N=30000,M=120000;
- random_30_6 G 29932 par: N=30000,M=180000;
- random_10_1.2 G 9996 par: N=10000,M=12000;
- random_10_1.4 G 10000 par: N=10000,M=14000;
- random_10_1.6 G 10000 par: N=10000,M=16000;
- random_10_1.8 G 10000 par: N=10000,M=18000;
- random_10_2 G 10000 par: N=10000,M=20000;
- random_10_2.2 G 10000 par: N=10000,M=22000;
- random_10_2.4 G 10000 par: N=10000,M=24000;
- random_10_2.6 G 10000 par: N=10000,M=26000;
- random_10_2.8 G 10000 par: N=10000,M=28000;
- random_10_3.5 G 10000 par: N=10000,M=35000;
- random_10_4 G 10000 par: N=10000,M=40000;
- random_10_5 G 10000 par: N=10000,M=5-000;