s14h
/
prism-accumulation
1
0
Fork 0
Code Releases Activity
Browse Source

Changed auto (commented out parts so run more quickly for testing. 

git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@692 bbc10eb1-c90d-0410-af57-cb519fbb1720
master
Dave Parker 18 years ago
parent
503854afac
commit
57c8b13c84
14 changed files with 74 additions and 69 deletions
Whitespace
Show all changes Ignore whitespace when comparing lines Ignore changes in amount of whitespace Ignore changes in whitespace at EOL
Split View
Diff Options
Show Stats Download Patch File Download Diff File
  1. 2
      prism-examples/cluster/auto
  2. 16
      prism-examples/dining_crypt/auto
  3. 33
      prism-examples/embedded/auto
  4. 2
      prism-examples/firewire/abst/auto
  5. 2
      prism-examples/firewire/impl/auto
  6. 2
      prism-examples/kanban/auto
  7. 10
      prism-examples/leader/asynchronous/auto
  8. 36
      prism-examples/molecules/auto
  9. 4
      prism-examples/peer2peer/auto
  10. 4
      prism-examples/phil/nofair/auto
  11. 4
      prism-examples/phil_lss/auto
  12. 22
      prism-examples/polling/auto
  13. 4
      prism-examples/rabin/auto
  14. 2
      prism-examples/tandem/auto

2
prism-examples/cluster/auto
View File

@ -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

16
prism-examples/dining_crypt/auto
View File

@ -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

33
prism-examples/embedded/auto
View File

@ -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

2
prism-examples/firewire/abst/auto
View File

@ -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

2
prism-examples/firewire/impl/auto
View File

@ -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

2
prism-examples/kanban/auto
View File

@ -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

10
prism-examples/leader/asynchronous/auto
View File

@ -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

36
prism-examples/molecules/auto
View File

@ -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

4
prism-examples/peer2peer/auto
View File

@ -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

4
prism-examples/phil/nofair/auto
View File

@ -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

4
prism-examples/phil_lss/auto
View File

@ -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

22
prism-examples/polling/auto
View File

@ -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

4
prism-examples/rabin/auto
View File

@ -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

2
prism-examples/tandem/auto
View File

@ -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
Write Preview
Loading…
Cancel
Save