diff --git a/prism-examples/cluster/auto b/prism-examples/cluster/auto index 19b86a72..bb6ea925 100755 --- a/prism-examples/cluster/auto +++ b/prism-examples/cluster/auto @@ -1,5 +1,5 @@ #!/bin/csh -foreach N (4 8 16 32 64 128 256 512) +foreach N (4 8 16 32) #64 128 256 512) prism cluster.sm cluster.csl -const N=$N,T=10 -prop 1 -jor end diff --git a/prism-examples/dining_crypt/auto b/prism-examples/dining_crypt/auto index 9040379c..5447792f 100755 --- a/prism-examples/dining_crypt/auto +++ b/prism-examples/dining_crypt/auto @@ -5,10 +5,10 @@ prism dining_crypt4.nm correctness.pctl prism dining_crypt5.nm correctness.pctl prism dining_crypt6.nm correctness.pctl prism dining_crypt7.nm correctness.pctl -prism dining_crypt8.nm correctness.pctl -prism dining_crypt9.nm correctness.pctl -prism dining_crypt10.nm correctness.pctl -prism dining_crypt15.nm correctness.pctl +#prism dining_crypt8.nm correctness.pctl +#prism dining_crypt9.nm correctness.pctl +#prism dining_crypt10.nm correctness.pctl +#prism dining_crypt15.nm correctness.pctl prism dining_crypt3.nm anonymity.pctl -const k=0:7 -m -nopre -exportresults stdout prism dining_crypt4.nm anonymity.pctl -const k=0:15 -m -nopre -exportresults stdout @@ -16,7 +16,7 @@ prism dining_crypt4.nm anonymity.pctl -const k=0:15 -m -nopre -exportresults st prism dining_crypt5.nm anonymity.pctl -const k=0 -m -nopre prism dining_crypt6.nm anonymity.pctl -const k=1 -m -nopre prism dining_crypt7.nm anonymity.pctl -const k=0 -m -nopre -prism dining_crypt8.nm anonymity.pctl -const k=1 -m -nopre -prism dining_crypt9.nm anonymity.pctl -const k=0 -m -nopre -prism dining_crypt10.nm anonymity.pctl -const k=1 -m -nopre -prism dining_crypt15.nm anonymity.pctl -const k=0 -m -nopre +#prism dining_crypt8.nm anonymity.pctl -const k=1 -m -nopre +#prism dining_crypt9.nm anonymity.pctl -const k=0 -m -nopre +#prism dining_crypt10.nm anonymity.pctl -const k=1 -m -nopre +#prism dining_crypt15.nm anonymity.pctl -const k=0 -m -nopre diff --git a/prism-examples/embedded/auto b/prism-examples/embedded/auto index 4522c81b..4d27c725 100755 --- a/prism-examples/embedded/auto +++ b/prism-examples/embedded/auto @@ -1,20 +1,25 @@ #!/bin/csh -prism embedded.sm embedded_prob.csl -prop 1 -const MAX_COUNT=2,T=0:24 -s -prism embedded.sm embedded_prob.csl -prop 2 -const MAX_COUNT=2,T=0:24 -s -prism embedded.sm embedded_prob.csl -prop 3 -const MAX_COUNT=2,T=0:24 -s -prism embedded.sm embedded_prob.csl -prop 4 -const MAX_COUNT=2,T=0:24 -s +prism embedded.sm embedded.csl -prop 1 -const MAX_COUNT=2,T=12 -s +prism embedded.sm embedded.csl -prop 2 -const MAX_COUNT=2,T=12 -s +prism embedded.sm embedded.csl -prop 3 -const MAX_COUNT=2,T=12 -s +prism embedded.sm embedded.csl -prop 4 -const MAX_COUNT=2,T=12 -s +prism embedded.sm embedded.csl -prop 5 -const MAX_COUNT=2,T=12 -s -prism embedded.sm embedded_prob.csl -prop 5 -const MAX_COUNT=2,T=0:2:30 -s -prism embedded.sm embedded_prob.csl -prop 6 -const MAX_COUNT=2,T=0:2:30 -s -prism embedded.sm embedded_prob.csl -prop 7 -const MAX_COUNT=2,T=0:2:30 -s -prism embedded.sm embedded_prob.csl -prop 8 -const MAX_COUNT=2,T=0:2:30 -s +prism embedded.sm embedded.csl -prop 6 -const MAX_COUNT=2,T=14 -s -epsilon 1e-8 +prism embedded.sm embedded.csl -prop 7 -const MAX_COUNT=2,T=14 -s -epsilon 1e-8 +prism embedded.sm embedded.csl -prop 8 -const MAX_COUNT=2,T=14 -s -epsilon 1e-8 +prism embedded.sm embedded.csl -prop 9 -const MAX_COUNT=2,T=14 -s -epsilon 1e-8 +prism embedded.sm embedded.csl -prop 10 -const MAX_COUNT=2,T=14 -s -epsilon 1e-8 -prism embedded.sm embedded_prob.csl -prop 9 -const MAX_COUNT=2,T=0 -s -prism embedded.sm embedded_prob.csl -prop 10 -const MAX_COUNT=2,T=0 -s -prism embedded.sm embedded_prob.csl -prop 11 -const MAX_COUNT=2,T=0 -s -prism embedded.sm embedded_prob.csl -prop 12 -const MAX_COUNT=2,T=0 -s +prism embedded.sm embedded.csl -prop 11 -const MAX_COUNT=2,T=0 -s +prism embedded.sm embedded.csl -prop 12 -const MAX_COUNT=2,T=0 -s +prism embedded.sm embedded.csl -prop 13 -const MAX_COUNT=2,T=0 -s +prism embedded.sm embedded.csl -prop 14 -const MAX_COUNT=2,T=0 -s -prism embedded.sm embedded_exptime.csl -prop 1 -const MAX_COUNT=2,T=0:24 -s -epsilon 1e-8 +prism embedded.sm embedded.csl -prop 15 -const MAX_COUNT=2,T=12 -s -epsilon 1e-8 +prism embedded.sm embedded.csl -prop 16 -const MAX_COUNT=2,T=12 -s -epsilon 1e-8 +prism embedded.sm embedded.csl -prop 17 -const MAX_COUNT=2,T=12 -s -epsilon 1e-8 -prism embedded.sm embedded_exptime.csl -prop 2 -const MAX_COUNT=1:7,T=0 -s -gs -epsilon 1e-10 +prism embedded.sm embedded.csl -prop 18 -const MAX_COUNT=2,T=12 -s -epsilon 1e-8 +prism embedded.sm embedded.csl -prop 19 -const MAX_COUNT=2,T=12 -s -epsilon 1e-8 diff --git a/prism-examples/firewire/abst/auto b/prism-examples/firewire/abst/auto index 53557cc2..86de3804 100755 --- a/prism-examples/firewire/abst/auto +++ b/prism-examples/firewire/abst/auto @@ -4,6 +4,6 @@ prism firewire.nm liveness.pctl -m # deadline properties -foreach deadline (200 300 400 500 600 800 1000) +foreach deadline (200 300 400 500 600) # 800 1000) prism deadline.nm deadline.pctl -const deadline=$deadline -m end diff --git a/prism-examples/firewire/impl/auto b/prism-examples/firewire/impl/auto index 53557cc2..f9f807cd 100755 --- a/prism-examples/firewire/impl/auto +++ b/prism-examples/firewire/impl/auto @@ -4,6 +4,6 @@ prism firewire.nm liveness.pctl -m # deadline properties -foreach deadline (200 300 400 500 600 800 1000) +foreach deadline (200) # 300 400 500 600 800 1000) prism deadline.nm deadline.pctl -const deadline=$deadline -m end diff --git a/prism-examples/kanban/auto b/prism-examples/kanban/auto index 93b159d9..5bad928f 100755 --- a/prism-examples/kanban/auto +++ b/prism-examples/kanban/auto @@ -1,5 +1,5 @@ #!/bin/csh -foreach t (1 2 3 4 5 6 7 8) +foreach t (1 2 3 4) # 5 6 7 8) prism kanban.sm kanban.csl -const t=$t -jor end diff --git a/prism-examples/leader/asynchronous/auto b/prism-examples/leader/asynchronous/auto index b35a04a2..5d2fcd72 100755 --- a/prism-examples/leader/asynchronous/auto +++ b/prism-examples/leader/asynchronous/auto @@ -3,8 +3,8 @@ prism leader3.nm leader3.pctl -const K=1 -m prism leader4.nm leader4.pctl -const K=1 -m prism leader5.nm leader5.pctl -const K=1 -m -prism leader6.nm leader6.pctl -const K=1 -m -prism leader7.nm leader7.pctl -const K=1 -m -prism leader8.nm leader8.pctl -const K=1 -m -prism leader9.nm leader9.pctl -const K=1 -m -prism leader10.nm leader10.pctl -const K=1 -m +#prism leader6.nm leader6.pctl -const K=1 -m +#prism leader7.nm leader7.pctl -const K=1 -m +#prism leader8.nm leader8.pctl -const K=1 -m +#prism leader9.nm leader9.pctl -const K=1 -m +#prism leader10.nm leader10.pctl -const K=1 -m diff --git a/prism-examples/molecules/auto b/prism-examples/molecules/auto index 6fa9ba8f..e2c13e45 100755 --- a/prism-examples/molecules/auto +++ b/prism-examples/molecules/auto @@ -1,23 +1,23 @@ #!/bin/csh -prism nacl.sm nacl.csl -prop 1 -const T=0:0.001:0.006,i=4 -prism nacl.sm nacl.csl -prop 2 -const T=0:0.001:0.006,i=0 -prism nacl.sm nacl.csl -prop 3 -const T=0,i=0 -gs +prism nacl.sm nacl.csl -prop 1 -const N1=10,N2=10,T=0:0.001:0.006,i=4 +prism nacl.sm nacl.csl -prop 2 -const N1=10,N2=10,T=0:0.001:0.006,i=0 +prism nacl.sm nacl.csl -prop 3 -const N1=10,N2=10,T=0,i=0 -gs -prism knacl.sm knacl.csl -prop 1 -const T=0:0.001:0.006,i=4, -prism knacl.sm knacl.csl -prop 2 -const T=0:0.001:0.006,i=4, -prism knacl.sm knacl.csl -prop 3 -const T=0:0.001:0.006,i=0, -prism knacl.sm knacl.csl -prop 4 -const T=0:0.001:0.006,i=0, -prism knacl.sm knacl.csl -prop 5 -const T=0,i=0 -gs -prism knacl.sm knacl.csl -prop 6 -const T=0,i=0 -gs +prism knacl.sm knacl.csl -prop 1 -const N1=10,N2=10,N3=10,T=0:0.001:0.006,i=4, +prism knacl.sm knacl.csl -prop 2 -const N1=10,N2=10,N3=10,T=0:0.001:0.006,i=4, +prism knacl.sm knacl.csl -prop 3 -const N1=10,N2=10,N3=10,T=0:0.001:0.006,i=0, +prism knacl.sm knacl.csl -prop 4 -const N1=10,N2=10,N3=10,T=0:0.001:0.006,i=0, +prism knacl.sm knacl.csl -prop 5 -const N1=10,N2=10,N3=10,T=0,i=0 -gs +prism knacl.sm knacl.csl -prop 6 -const N1=10,N2=10,N3=10,T=0,i=0 -gs -prism mc.sm mc.csl -prop 1 -const T=0:0.001:0.006,i=4 -prism mc.sm mc.csl -prop 2 -const T=0:0.001:0.006,i=4 -prism mc.sm mc.csl -prop 3 -const T=0:0.001:0.006,i=4 -prism mc.sm mc.csl -prop 4 -const T=0:0.001:0.006,i=0 -prism mc.sm mc.csl -prop 5 -const T=0:0.001:0.006,i=0 -prism mc.sm mc.csl -prop 6 -const T=0:0.001:0.006,i=0 -prism mc.sm mc.csl -prop 7 -const T=0,i=0 -gs -prism mc.sm mc.csl -prop 8 -const T=0,i=0 -gs -prism mc.sm mc.csl -prop 9 -const T=0,i=0 -gs +prism mc.sm mc.csl -prop 1 -const N1=10,N2=10,T=0:0.001:0.006,i=4 +prism mc.sm mc.csl -prop 2 -const N1=10,N2=10,T=0:0.001:0.006,i=4 +prism mc.sm mc.csl -prop 3 -const N1=10,N2=10,T=0:0.001:0.006,i=4 +prism mc.sm mc.csl -prop 4 -const N1=10,N2=10,T=0:0.001:0.006,i=0 +prism mc.sm mc.csl -prop 5 -const N1=10,N2=10,T=0:0.001:0.006,i=0 +prism mc.sm mc.csl -prop 6 -const N1=10,N2=10,T=0:0.001:0.006,i=0 +prism mc.sm mc.csl -prop 7 -const N1=10,N2=10,T=0,i=0 -gs +prism mc.sm mc.csl -prop 8 -const N1=10,N2=10,T=0,i=0 -gs +prism mc.sm mc.csl -prop 9 -const N1=10,N2=10,T=0,i=0 -gs diff --git a/prism-examples/peer2peer/auto b/prism-examples/peer2peer/auto index ca1deac9..90f6f1b8 100755 --- a/prism-examples/peer2peer/auto +++ b/prism-examples/peer2peer/auto @@ -1,8 +1,8 @@ #!/bin/csh foreach N (4 5) - foreach K (4 5 6 7 8) - prism peer2peer"$N"_"$K".sm peer2peer.csl -fixdl -const T=0:0.01:1.5 + foreach K (4) # 5 6 7 8) + prism peer2peer"$N"_"$K".sm peer2peer.csl -fixdl -const T=1.1 end end diff --git a/prism-examples/phil/nofair/auto b/prism-examples/phil/nofair/auto index b50fe81b..15b0b6e4 100755 --- a/prism-examples/phil/nofair/auto +++ b/prism-examples/phil/nofair/auto @@ -2,8 +2,8 @@ prism phil-nofair3.nm phil.pctl -const K=1 -m prism phil-nofair4.nm phil.pctl -const K=1 -m -prism phil-nofair5.nm phil.pctl -const K=1 -m -prism phil-nofair6.nm phil.pctl -const K=1 -m +#prism phil-nofair5.nm phil.pctl -const K=1 -m +#prism phil-nofair6.nm phil.pctl -const K=1 -m #prism phil-nofair7.nm phil.pctl -const K=1 -m #prism phil-nofair8.nm phil.pctl -const K=1 -m #prism phil-nofair9.nm phil.pctl -const K=1 -m diff --git a/prism-examples/phil_lss/auto b/prism-examples/phil_lss/auto index 14545244..5a97513c 100755 --- a/prism-examples/phil_lss/auto +++ b/prism-examples/phil_lss/auto @@ -1,4 +1,4 @@ #!/bin/csh -prism phil_lss3.nm phil_lss3.pctl -const K=3:10,L=1 -m -prism phil_lss4.nm phil_lss4.pctl -const K=4:7,L=1 -m +prism phil_lss3.nm phil_lss3.pctl -const K=3:6,L=1 -m +#prism phil_lss4.nm phil_lss4.pctl -const K=4:5,L=1 -m diff --git a/prism-examples/polling/auto b/prism-examples/polling/auto index bcff58cc..c3b424a1 100755 --- a/prism-examples/polling/auto +++ b/prism-examples/polling/auto @@ -8,14 +8,14 @@ prism poll6.sm poll.csl -const T=50 prism poll7.sm poll.csl -const T=50 prism poll8.sm poll.csl -const T=50 prism poll9.sm poll.csl -const T=50 -prism poll10.sm poll.csl -const T=50 -prism poll11.sm poll.csl -const T=50 -prism poll12.sm poll.csl -const T=50 -prism poll13.sm poll.csl -const T=50 -prism poll14.sm poll.csl -const T=50 -prism poll15.sm poll.csl -const T=50 -prism poll16.sm poll.csl -const T=50 -prism poll17.sm poll.csl -const T=50 -prism poll18.sm poll.csl -const T=50 -prism poll19.sm poll.csl -const T=50 -prism poll20.sm poll.csl -const T=50 +#prism poll10.sm poll.csl -const T=50 +#prism poll11.sm poll.csl -const T=50 +#prism poll12.sm poll.csl -const T=50 +#prism poll13.sm poll.csl -const T=50 +#prism poll14.sm poll.csl -const T=50 +#prism poll15.sm poll.csl -const T=50 +#prism poll16.sm poll.csl -const T=50 +#prism poll17.sm poll.csl -const T=50 +#prism poll18.sm poll.csl -const T=50 +#prism poll19.sm poll.csl -const T=50 +#prism poll20.sm poll.csl -const T=50 diff --git a/prism-examples/rabin/auto b/prism-examples/rabin/auto index 4914802e..59425264 100755 --- a/prism-examples/rabin/auto +++ b/prism-examples/rabin/auto @@ -5,5 +5,5 @@ prism rabin4.nm rabin.pctl -fair prism rabin5.nm rabin.pctl -fair prism rabin6.nm rabin.pctl -fair prism rabin8.nm rabin.pctl -fair -prism rabin10.nm rabin.pctl -fair -prism rabin12.nm rabin.pctl -fair +#prism rabin10.nm rabin.pctl -fair +#prism rabin12.nm rabin.pctl -fair diff --git a/prism-examples/tandem/auto b/prism-examples/tandem/auto index f6dc807e..ded21445 100755 --- a/prism-examples/tandem/auto +++ b/prism-examples/tandem/auto @@ -1,5 +1,5 @@ #!/bin/csh -foreach c ( 3 7 15 31 63 127 255 511 1023 2047 4095 8191 ) +foreach c ( 3 7 15 31 63 127 255 ) #511 1023 2047 4095 8191 ) prism tandem.sm tandem.csl -const T=1,c=$c end