diff --git a/prism/examples/pta/csma/des/args b/prism/examples/des/csma/args similarity index 100% rename from prism/examples/pta/csma/des/args rename to prism/examples/des/csma/args diff --git a/prism/examples/pta/csma/des/csma2.deslist b/prism/examples/des/csma/csma2.deslist similarity index 100% rename from prism/examples/pta/csma/des/csma2.deslist rename to prism/examples/des/csma/csma2.deslist diff --git a/prism/examples/pta/csma/des/csma4.deslist b/prism/examples/des/csma/csma4.deslist similarity index 100% rename from prism/examples/pta/csma/des/csma4.deslist rename to prism/examples/des/csma/csma4.deslist diff --git a/prism/examples/pta/csma/des/csmacd-bmax1-s1.des b/prism/examples/des/csma/csmacd-bmax1-s1.des similarity index 100% rename from prism/examples/pta/csma/des/csmacd-bmax1-s1.des rename to prism/examples/des/csma/csmacd-bmax1-s1.des diff --git a/prism/examples/pta/csma/des/csmacd-bmax1-s2.des b/prism/examples/des/csma/csmacd-bmax1-s2.des similarity index 100% rename from prism/examples/pta/csma/des/csmacd-bmax1-s2.des rename to prism/examples/des/csma/csmacd-bmax1-s2.des diff --git a/prism/examples/pta/csma/des/csmacd-bmax2-s1.des b/prism/examples/des/csma/csmacd-bmax2-s1.des similarity index 100% rename from prism/examples/pta/csma/des/csmacd-bmax2-s1.des rename to prism/examples/des/csma/csmacd-bmax2-s1.des diff --git a/prism/examples/pta/csma/des/csmacd-bmax2-s2.des b/prism/examples/des/csma/csmacd-bmax2-s2.des similarity index 100% rename from prism/examples/pta/csma/des/csmacd-bmax2-s2.des rename to prism/examples/des/csma/csmacd-bmax2-s2.des diff --git a/prism/examples/pta/csma/des/csmacd-bmax3-s1.des b/prism/examples/des/csma/csmacd-bmax3-s1.des similarity index 100% rename from prism/examples/pta/csma/des/csmacd-bmax3-s1.des rename to prism/examples/des/csma/csmacd-bmax3-s1.des diff --git a/prism/examples/pta/csma/des/csmacd-bmax3-s2.des b/prism/examples/des/csma/csmacd-bmax3-s2.des similarity index 100% rename from prism/examples/pta/csma/des/csmacd-bmax3-s2.des rename to prism/examples/des/csma/csmacd-bmax3-s2.des diff --git a/prism/examples/pta/csma/des/csmacd-bmax4-s1.des b/prism/examples/des/csma/csmacd-bmax4-s1.des similarity index 100% rename from prism/examples/pta/csma/des/csmacd-bmax4-s1.des rename to prism/examples/des/csma/csmacd-bmax4-s1.des diff --git a/prism/examples/pta/csma/des/csmacd-bmax4-s2.des b/prism/examples/des/csma/csmacd-bmax4-s2.des similarity index 100% rename from prism/examples/pta/csma/des/csmacd-bmax4-s2.des rename to prism/examples/des/csma/csmacd-bmax4-s2.des diff --git a/prism/examples/pta/csma/des/csmacd-bmax5-s1.des b/prism/examples/des/csma/csmacd-bmax5-s1.des similarity index 100% rename from prism/examples/pta/csma/des/csmacd-bmax5-s1.des rename to prism/examples/des/csma/csmacd-bmax5-s1.des diff --git a/prism/examples/pta/csma/des/csmacd-bmax5-s2.des b/prism/examples/des/csma/csmacd-bmax5-s2.des similarity index 100% rename from prism/examples/pta/csma/des/csmacd-bmax5-s2.des rename to prism/examples/des/csma/csmacd-bmax5-s2.des diff --git a/prism/examples/pta/csma/des/csmacd-bus.des b/prism/examples/des/csma/csmacd-bus.des similarity index 100% rename from prism/examples/pta/csma/des/csmacd-bus.des rename to prism/examples/des/csma/csmacd-bus.des diff --git a/prism/examples/pta/csma/des/csmacd-collision-counter.des b/prism/examples/des/csma/csmacd-collision-counter.des similarity index 100% rename from prism/examples/pta/csma/des/csmacd-collision-counter.des rename to prism/examples/des/csma/csmacd-collision-counter.des diff --git a/prism/examples/pta/csma/des/deadline2000.des b/prism/examples/des/csma/deadline2000.des similarity index 100% rename from prism/examples/pta/csma/des/deadline2000.des rename to prism/examples/des/csma/deadline2000.des diff --git a/prism/examples/pta/csma/des/deadline4000.des b/prism/examples/des/csma/deadline4000.des similarity index 100% rename from prism/examples/pta/csma/des/deadline4000.des rename to prism/examples/des/csma/deadline4000.des diff --git a/prism/examples/pta/csma/des/models b/prism/examples/des/csma/models similarity index 100% rename from prism/examples/pta/csma/des/models rename to prism/examples/des/csma/models diff --git a/prism/examples/pta/csma-prism.sh b/prism/examples/pta/csma-prism.sh index 90f1eb6b..3362c68b 100755 --- a/prism/examples/pta/csma-prism.sh +++ b/prism/examples/pta/csma-prism.sh @@ -1,3 +1,4 @@ +#!/bin/sh # abstract (time bounded) diff --git a/prism/examples/pta/csma/abst/auto b/prism/examples/pta/csma/abst/auto new file mode 100755 index 00000000..6940d1b2 --- /dev/null +++ b/prism/examples/pta/csma/abst/auto @@ -0,0 +1,11 @@ +#!/bin/csh + +prism csma.nm collisions.pctl -const bmax=2,K=4 -aroptions refine=all,nopre,opt +prism csma.nm collisions.pctl -const bmax=2,K=8 -aroptions refine=all,nopre,opt +prism csma.nm collisions.pctl -const bmax=4,K=4 -aroptions refine=all,nopre,opt +prism csma.nm collisions.pctl -const bmax=4,K=8 -aroptions refine=all,nopre,opt + +prism csma.nm time.pctl -const bmax=1,K=0 -aroptions refine=all,nopre,opt +prism csma.nm time.pctl -const bmax=2,K=0 -aroptions refine=all,nopre,opt +prism csma.nm time.pctl -const bmax=3,K=0 -aroptions refine=all,nopre,opt +prism csma.nm time.pctl -const bmax=4,K=0 -aroptions refine=all,nopre,opt \ No newline at end of file diff --git a/prism/examples/pta/csma/args b/prism/examples/pta/csma/full/args similarity index 100% rename from prism/examples/pta/csma/args rename to prism/examples/pta/csma/full/args diff --git a/prism/examples/pta/csma/full/auto b/prism/examples/pta/csma/full/auto new file mode 100755 index 00000000..81dcbab2 --- /dev/null +++ b/prism/examples/pta/csma/full/auto @@ -0,0 +1,7 @@ +#!/bin/csh + +prism csma.nm eventually.pctl -aroptions refine=all,nopre,opt -const bmax=1 + +prism csma.nm deadline.pctl -const bmax=1 -const T=1000 -aroptions refine=all,nopre,opt +prism csma.nm deadline.pctl -const bmax=1 -const T=2000 -aroptions refine=all,nopre,opt +prism csma.nm deadline.pctl -const bmax=1 -const T=3000 -aroptions refine=all,nopre,opt diff --git a/prism/examples/pta/csma/collisions.pctl b/prism/examples/pta/csma/full/collisions.pctl similarity index 100% rename from prism/examples/pta/csma/collisions.pctl rename to prism/examples/pta/csma/full/collisions.pctl diff --git a/prism/examples/pta/csma/csma-digital.nm b/prism/examples/pta/csma/full/csma-digital.nm similarity index 100% rename from prism/examples/pta/csma/csma-digital.nm rename to prism/examples/pta/csma/full/csma-digital.nm diff --git a/prism/examples/pta/csma/csma-slots.nm b/prism/examples/pta/csma/full/csma-slots.nm similarity index 100% rename from prism/examples/pta/csma/csma-slots.nm rename to prism/examples/pta/csma/full/csma-slots.nm diff --git a/prism/examples/pta/csma/csma.nm b/prism/examples/pta/csma/full/csma.nm similarity index 100% rename from prism/examples/pta/csma/csma.nm rename to prism/examples/pta/csma/full/csma.nm diff --git a/prism/examples/pta/csma/eventually.pctl b/prism/examples/pta/csma/full/eventually.pctl similarity index 100% rename from prism/examples/pta/csma/eventually.pctl rename to prism/examples/pta/csma/full/eventually.pctl diff --git a/prism/examples/pta/csma/models b/prism/examples/pta/csma/full/models similarity index 100% rename from prism/examples/pta/csma/models rename to prism/examples/pta/csma/full/models diff --git a/prism/examples/pta/csma/props b/prism/examples/pta/csma/full/props similarity index 100% rename from prism/examples/pta/csma/props rename to prism/examples/pta/csma/full/props diff --git a/prism/examples/pta/csma/time.pctl b/prism/examples/pta/csma/full/time.pctl similarity index 100% rename from prism/examples/pta/csma/time.pctl rename to prism/examples/pta/csma/full/time.pctl diff --git a/prism/examples/pta/firewire-prism.sh b/prism/examples/pta/firewire-prism.sh index cabaf92f..7db09c41 100755 --- a/prism/examples/pta/firewire-prism.sh +++ b/prism/examples/pta/firewire-prism.sh @@ -1,3 +1,4 @@ +#!/bin/sh # abst diff --git a/prism/examples/pta/repudiation-prism.sh b/prism/examples/pta/repudiation-prism.sh index ff1c8c8a..d114b159 100755 --- a/prism/examples/pta/repudiation-prism.sh +++ b/prism/examples/pta/repudiation-prism.sh @@ -1,13 +1,14 @@ +#!/bin/sh # honest -prism-explicit repudiation/honest/{repudiation.nm,eventually.pctl} -aroptions refine=all,opt -prism-explicit repudiation/honest/{repudiation.nm,deadline.pctl} -aroptions refine=all,opt -const T=40 -prism-explicit repudiation/honest/{repudiation.nm,deadline.pctl} -aroptions refine=all,opt -const T=80 -prism-explicit repudiation/honest/{repudiation.nm,deadline.pctl} -aroptions refine=all,opt -const T=100 +prism repudiation/honest/{repudiation.nm,eventually.pctl} -aroptions refine=all,opt +prism repudiation/honest/{repudiation.nm,deadline.pctl} -aroptions refine=all,opt -const T=40 +prism repudiation/honest/{repudiation.nm,deadline.pctl} -aroptions refine=all,opt -const T=80 +prism repudiation/honest/{repudiation.nm,deadline.pctl} -aroptions refine=all,opt -const T=100 # malicious -prism-explicit repudiation/malicious/{repudiation.nm,eventually.pctl} -aroptions refine=all,opt -prism-explicit repudiation/malicious/{repudiation.nm,deadline.pctl} -aroptions refine=all,opt -const T=5 -prism-explicit repudiation/malicious/{repudiation.nm,deadline.pctl} -aroptions refine=all,opt -const T=10 -prism-explicit repudiation/malicious/{repudiation.nm,deadline.pctl} -aroptions refine=all,opt -const T=20 +prism repudiation/malicious/{repudiation.nm,eventually.pctl} -aroptions refine=all,opt +prism repudiation/malicious/{repudiation.nm,deadline.pctl} -aroptions refine=all,opt -const T=5 +prism repudiation/malicious/{repudiation.nm,deadline.pctl} -aroptions refine=all,opt -const T=10 +prism repudiation/malicious/{repudiation.nm,deadline.pctl} -aroptions refine=all,opt -const T=20 diff --git a/prism/examples/pta/repudiation/honest/auto b/prism/examples/pta/repudiation/honest/auto new file mode 100755 index 00000000..5869f8d3 --- /dev/null +++ b/prism/examples/pta/repudiation/honest/auto @@ -0,0 +1,7 @@ +#!/bin/csh + +prism repudiation.nm eventually.pctl -aroptions refine=all,opt + +prism repudiation.nm deadline.pctl -aroptions refine=all,opt -const T=40 +prism repudiation.nm deadline.pctl -aroptions refine=all,opt -const T=80 +prism repudiation.nm deadline.pctl -aroptions refine=all,opt -const T=100 diff --git a/prism/examples/pta/repudiation/malicious/auto b/prism/examples/pta/repudiation/malicious/auto new file mode 100755 index 00000000..27f3bcc4 --- /dev/null +++ b/prism/examples/pta/repudiation/malicious/auto @@ -0,0 +1,7 @@ +#!/bin/csh + +prism repudiation.nm eventually.pctl -aroptions refine=all,opt + +prism repudiation.nm deadline.pctl -aroptions refine=all,opt -const T=5 +prism repudiation.nm deadline.pctl -aroptions refine=all,opt -const T=10 +prism repudiation.nm deadline.pctl -aroptions refine=all,opt -const T=20 diff --git a/prism/examples/pta/zeroconf-prism.sh b/prism/examples/pta/zeroconf-prism.sh index b7b6e8c4..1508a668 100755 --- a/prism/examples/pta/zeroconf-prism.sh +++ b/prism/examples/pta/zeroconf-prism.sh @@ -1,20 +1,20 @@ +#!/bin/sh # full (multi-variable) -prism-explicit zeroconf/{zeroconf.nm,incorrect.pctl} -aroptions refine=all,nopre,opt +prism zeroconf.nm incorrect.pctl -aroptions refine=all,nopre,opt -prism-explicit zeroconf/{zeroconf.nm,deadline.pctl} -const T=100 -aroptions refine=all,nopre,opt -prism-explicit zeroconf/{zeroconf.nm,deadline.pctl} -const T=150 -aroptions refine=all,nopre,opt -prism-explicit zeroconf/{zeroconf.nm,deadline.pctl} -const T=200 -aroptions refine=all,nopre,opt - -prism-explicit zeroconf/{zeroconf.nm,time.pctl} -aroptions refine=all,nopre,opt +prism zeroconf.nm deadline.pctl -const T=100 -aroptions refine=all,nopre,opt +prism zeroconf.nm deadline.pctl -const T=150 -aroptions refine=all,nopre,opt +prism zeroconf.nm deadline.pctl -const T=200 -aroptions refine=all,nopre,opt +prism zeroconf.nm time.pctl -aroptions refine=all,nopre,opt # simple (single variable) -prism-explicit zeroconf/{zeroconf-simple.nm,incorrect.pctl} -aroptions refine=all,nopre,opt +prism zeroconf-simple.nm incorrect.pctl -aroptions refine=all,nopre,opt -prism-explicit zeroconf/{zeroconf-simple.nm,deadline.pctl} -const T=100 -aroptions refine=all,nopre,opt -prism-explicit zeroconf/{zeroconf-simple.nm,deadline.pctl} -const T=150 -aroptions refine=all,nopre,opt -prism-explicit zeroconf/{zeroconf-simple.nm,deadline.pctl} -const T=200 -aroptions refine=all,nopre,opt +prism zeroconf-simple.nm deadline.pctl -const T=100 -aroptions refine=all,nopre,opt +prism zeroconf-simple.nm deadline.pctl -const T=150 -aroptions refine=all,nopre,opt +prism zeroconf-simple.nm deadline.pctl -const T=200 -aroptions refine=all,nopre,opt