Permalink
Find file Copy path
Fetching contributors…
Cannot retrieve contributors at this time
153 lines (152 sloc) 7.41 KB
PROD input, no options, FMS 10
../bin/its-reach -i test_models/fms10.net --quiet -t PROD
PROD input, DDD option
../bin/its-reach -i test_models/fms10.net --quiet -t PROD --ddd
PROD input, --no-garbage
../bin/its-reach -i test_models/fms10.net --quiet -t PROD --no-garbage
CAMI input, no JSON
../bin/its-reach -i test_models/election_2.cami -t CAMI --quiet
CAMI input, with JSON
../bin/its-reach -i test_models/election_2.cami -t CAMI --quiet --json-order test_models/election_2.json
PROD input, philo 100
../bin/its-reach -i test_models/philo100.net -t PROD --quiet
ROMEO input, no order
../bin/its-reach -i test_models/train4.xml -t ROMEO --quiet
ROMEO input, no order
../bin/its-reach -i test_models/train4.xml -t ROMEO --quiet --load-order test_models/train4.ord
ROMEO using BFS
../bin/its-reach -i test_models/train4.xml -t ROMEO --quiet --load-order test_models/train4.ord --fixpoint BFS
ROMEO using DFS
../bin/its-reach -i test_models/train4.xml -t ROMEO --quiet --load-order test_models/train4.ord --fixpoint DFS
COLOANE format for ITS (flat scalar)
cd test_models; ../../bin/its-reach -i votersMain.xml -t ITSXML --quiet ; cd ..
COLOANE format for ITS (scalar depth2)
cd test_models; ../../bin/its-reach -i votersMain.xml -t ITSXML --quiet -ssD2 5 ; cd ..
COLOANE format for ITS (scalar depth rec)
cd test_models; ../../bin/its-reach -i votersMain.xml -t ITSXML --quiet -ssDR 5 ; cd ..
COLOANE format for ITS (scalar depth shallow)
cd test_models; ../../bin/its-reach -i votersMain.xml -t ITSXML --quiet -ssDS 5 ; cd ..
ETF format
../bin/its-reach -i test_models/peterson.4.dve.etf -t ETF --quiet
DVE format, philos
../bin/its-reach -i test_models/phils.4.dve -t DVE --quiet
DVE format, peterson
../bin/its-reach -i test_models/peterson.4.dve -t DVE --quiet
DVE format, peterson, with provided order
../bin/its-reach -i test_models/peterson.4.dve -t DVE --load-order test_models/peterson.ord --quiet
DVE format, szymanski
../bin/its-reach -i test_models/szymanski.2.dve -t DVE --quiet
CAMI input, with deep JSON
../bin/its-reach -i test_models/election_2.cami -t CAMI --quiet --json-order test_models/election_2.h11.json
DVE format, hanoi BEEM version (pole state encoded)
../bin/its-reach -i test_models/hanoi.ori.1.dve -t DVE --quiet
DVE format, hanoi my own version (ring state encoded)
../bin/its-reach -i test_models/hanoi.1.dve -t DVE --quiet
DVE format, firewire model with synchronizations
../bin/its-reach -i test_models/firewire_link.2.dve -t DVE --quiet
DVE format, bakery mutex protocol
../bin/its-reach -i test_models/bakery.4.dve -t DVE --quiet
DVE format, train-gate controller, patched e[] w.r.t. BEEM distrib
../bin/its-reach -i test_models/train-gate.5.dve -t DVE --quiet
DVE format, fischer mutex, with abstraction predicate and commit states
../bin/its-reach -i test_models/fischer.1.dve -t DVE --quiet
DVE format, fischer mutex, with original BEEM source code (bitwise or trick for clocks)
../bin/its-reach -i test_models/fischer.1.dve -t DVE --quiet
DVE format, lup model, with a global var "loading" to simulate access to other process state
../bin/its-reach -i test_models/lup.1.dve -t DVE --quiet
DVE format, brp model, with bitwise AND and OR on bytes read from channel
../bin/its-reach -i test_models/brp.1.dve -t DVE --quiet
DVE format, exit model, with integers in bool expr rewritten to comparisons
../bin/its-reach -i test_models/exit.1.dve -t DVE --quiet
DVE format, loyd model instance 1
../bin/its-reach -i test_models/loyd.1.dve -t DVE --quiet
DVE format, frogs model
../bin/its-reach -i test_models/frogs.1.dve -t DVE --quiet
DVE format, reader-writer model
../bin/its-reach -i test_models/reader_writer.3.dve -t DVE --quiet
DVE format, lamport model
../bin/its-reach -i test_models/lamport.2.dve -t DVE --quiet
GAL format, file : bakery.gal
../bin/its-reach -i test_models/gal/bakery.gal -t GAL --quiet
GAL format, file : brp.gal
../bin/its-reach -i test_models/gal/brp.gal -t GAL --quiet
GAL format, file : loyd.gal
../bin/its-reach -i test_models/gal/loyd.gal -t GAL --quiet
GAL format, file : lup.gal
../bin/its-reach -i test_models/gal/lup.gal -t GAL --quiet
GAL format, file : phils.gal
../bin/its-reach -i test_models/gal/phils.gal -t GAL --quiet
GAL format, file : reader_writer.gal
../bin/its-reach -i test_models/gal/reader_writer.gal -t GAL --quiet
DVE format, adding model
../bin/its-reach -i test_models/adding.1.5.dve -t DVE --quiet
DVE format, hanoi my own version (with solution trace)
../bin/its-reach -i test_models/hanoi.1.dve -t DVE -reachable 'pos[0]=1&&pos[1]=1&&pos[2]=1&&pos[3]=1&&pos[4]=1&&pos[5]=1&&pos[6]=1&&pos[7]=1'
GAL format, train example translated from Romeo
../bin/its-reach -i test_models/gal/train4.gal -t GAL --quiet
Looking for many traces, frogs example
../bin/its-reach -i test_models/gal/frogs.gal -t GAL -reachable 'Check.state==1' -manywitness 5 --quiet
Looking for many traces, frogs example, with CGAL input
../bin/its-reach -i test_models/cgal/frogs.gal -t CGAL -reachable 'Check.state==1' -manywitness 5 --quiet
CGAL input, with several levels of depth
../bin/its-reach -i test_models/cgal/PhiloFork.gal -t CGAL --quiet
CGAL bakery
../bin/its-reach -t CGAL --quiet -i test_models/cgal/bakery.mod.gal
CGAL hanoi ori
../bin/its-reach -t CGAL --quiet -i test_models/cgal/hanoi_ori.mod.gal
GAL hanoi ori
../bin/its-reach -t GAL --quiet -i test_models/gal/hanoi_ori.gal
CGAL bakery
../bin/its-reach -t CGAL --quiet -i test_models/cgal/szymanski.flat.mod.gal
CGAL brp
../bin/its-reach -t CGAL --quiet -i test_models/cgal/brp.mod.gal
GAL lamport
../bin/its-reach -t GAL --quiet -i test_models/gal/lamport.gal
CGAL lamport
../bin/its-reach -t CGAL --quiet -i test_models/cgal/lamport.mod.gal
CGAL szymanski
../bin/its-reach -t CGAL --quiet -i test_models/cgal/szymanski.mod.gal
CGAL exit
../bin/its-reach -t CGAL --quiet -i test_models/cgal/exit.mod.gal
GAL exit
../bin/its-reach -t GAL --quiet -i test_models/gal/exit.gal
CGAL loyd
../bin/its-reach -t CGAL --quiet -i test_models/cgal/loyd.mod.gal
CGAL test
../bin/its-reach -t CGAL --quiet -i test_models/cgal/test.mod.gal
CGAL firewire
../bin/its-reach -t CGAL --quiet -i test_models/cgal/firewire.mod.gal
GAL firewire
../bin/its-reach -t GAL --quiet -i test_models/gal/firewire.gal
CGAL lup
../bin/its-reach -t CGAL --quiet -i test_models/cgal/lup.mod.gal
CGAL train4
../bin/its-reach -t CGAL --quiet -i test_models/cgal/train4.mod.gal
GAL fischer
../bin/its-reach -t GAL --quiet -i test_models/gal/fischer.gal
CGAL fischer
../bin/its-reach -t CGAL --quiet -i test_models/cgal/fischer.mod.gal
GAL peterson
../bin/its-reach -t GAL --quiet -i test_models/gal/peterson.gal
CGAL peterson
../bin/its-reach -t CGAL --quiet -i test_models/cgal/peterson.mod.gal
GAL train_gate
../bin/its-reach -t GAL --quiet -i test_models/gal/train_gate.gal
CGAL train_gate
../bin/its-reach -t CGAL --quiet -i test_models/cgal/train_gate.mod.gal
CGAL frogs
../bin/its-reach -t CGAL --quiet -i test_models/cgal/frogs.mod.gal
CGAL phils
../bin/its-reach -t CGAL --quiet -i test_models/cgal/phils.mod.gal
CGAL hanoi
../bin/its-reach -t CGAL --quiet -i test_models/cgal/hanoi.mod.gal
GAL hanoi
../bin/its-reach -t GAL --quiet -i test_models/gal/hanoi.gal
CGAL reader_writer
../bin/its-reach -t CGAL --quiet -i test_models/cgal/reader_writer.mod.gal
DVE elevator_planning 1
../bin/its-reach -t DVE --quiet -i test_models/elevator_planning.1.dve
DVE pgm_protocol 2
../bin/its-reach -t DVE --quiet -i test_models/pgm_protocol.2.dve
CGAL dhccp protocol test with trace
../bin/its-reach -i test_models/cgal/cache_l1.gal -t CGAL -reachable-file test_models/cgal/cache_l1.prop --quiet