diff --git a/prism/examples/pta/firewire/des/abs.des b/prism/examples/des/firewire/abs.des similarity index 100% rename from prism/examples/pta/firewire/des/abs.des rename to prism/examples/des/firewire/abs.des diff --git a/prism/examples/pta/firewire/des/abs1000.des b/prism/examples/des/firewire/abs1000.des similarity index 100% rename from prism/examples/pta/firewire/des/abs1000.des rename to prism/examples/des/firewire/abs1000.des diff --git a/prism/examples/pta/firewire/des/abs200.des b/prism/examples/des/firewire/abs200.des similarity index 100% rename from prism/examples/pta/firewire/des/abs200.des rename to prism/examples/des/firewire/abs200.des diff --git a/prism/examples/pta/firewire/des/abs2000.des b/prism/examples/des/firewire/abs2000.des similarity index 100% rename from prism/examples/pta/firewire/des/abs2000.des rename to prism/examples/des/firewire/abs2000.des diff --git a/prism/examples/pta/firewire/des/abs400.des b/prism/examples/des/firewire/abs400.des similarity index 100% rename from prism/examples/pta/firewire/des/abs400.des rename to prism/examples/des/firewire/abs400.des diff --git a/prism/examples/pta/firewire/des/abs500.des b/prism/examples/des/firewire/abs500.des similarity index 100% rename from prism/examples/pta/firewire/des/abs500.des rename to prism/examples/des/firewire/abs500.des diff --git a/prism/examples/pta/firewire/des/abs600.des b/prism/examples/des/firewire/abs600.des similarity index 100% rename from prism/examples/pta/firewire/des/abs600.des rename to prism/examples/des/firewire/abs600.des diff --git a/prism/examples/pta/firewire/des/abs800.des b/prism/examples/des/firewire/abs800.des similarity index 100% rename from prism/examples/pta/firewire/des/abs800.des rename to prism/examples/des/firewire/abs800.des diff --git a/prism/examples/pta/firewire/des/deadline1000.des b/prism/examples/des/firewire/deadline1000.des similarity index 100% rename from prism/examples/pta/firewire/des/deadline1000.des rename to prism/examples/des/firewire/deadline1000.des diff --git a/prism/examples/pta/firewire/des/deadline200.des b/prism/examples/des/firewire/deadline200.des similarity index 100% rename from prism/examples/pta/firewire/des/deadline200.des rename to prism/examples/des/firewire/deadline200.des diff --git a/prism/examples/pta/firewire/des/deadline2000.des b/prism/examples/des/firewire/deadline2000.des similarity index 100% rename from prism/examples/pta/firewire/des/deadline2000.des rename to prism/examples/des/firewire/deadline2000.des diff --git a/prism/examples/pta/firewire/des/deadline250.des b/prism/examples/des/firewire/deadline250.des similarity index 100% rename from prism/examples/pta/firewire/des/deadline250.des rename to prism/examples/des/firewire/deadline250.des diff --git a/prism/examples/pta/firewire/des/deadline300.des b/prism/examples/des/firewire/deadline300.des similarity index 100% rename from prism/examples/pta/firewire/des/deadline300.des rename to prism/examples/des/firewire/deadline300.des diff --git a/prism/examples/pta/firewire/des/deadline400.des b/prism/examples/des/firewire/deadline400.des similarity index 100% rename from prism/examples/pta/firewire/des/deadline400.des rename to prism/examples/des/firewire/deadline400.des diff --git a/prism/examples/pta/firewire/des/deadline500.des b/prism/examples/des/firewire/deadline500.des similarity index 100% rename from prism/examples/pta/firewire/des/deadline500.des rename to prism/examples/des/firewire/deadline500.des diff --git a/prism/examples/pta/firewire/des/deadline600.des b/prism/examples/des/firewire/deadline600.des similarity index 100% rename from prism/examples/pta/firewire/des/deadline600.des rename to prism/examples/des/firewire/deadline600.des diff --git a/prism/examples/pta/firewire/des/deadline750.des b/prism/examples/des/firewire/deadline750.des similarity index 100% rename from prism/examples/pta/firewire/des/deadline750.des rename to prism/examples/des/firewire/deadline750.des diff --git a/prism/examples/pta/firewire/des/deadline800.des b/prism/examples/des/firewire/deadline800.des similarity index 100% rename from prism/examples/pta/firewire/des/deadline800.des rename to prism/examples/des/firewire/deadline800.des diff --git a/prism/examples/pta/firewire/des/n1.des b/prism/examples/des/firewire/n1.des similarity index 100% rename from prism/examples/pta/firewire/des/n1.des rename to prism/examples/des/firewire/n1.des diff --git a/prism/examples/pta/firewire/des/n2.des b/prism/examples/des/firewire/n2.des similarity index 100% rename from prism/examples/pta/firewire/des/n2.des rename to prism/examples/des/firewire/n2.des diff --git a/prism/examples/pta/firewire/des/w12.des b/prism/examples/des/firewire/w12.des similarity index 100% rename from prism/examples/pta/firewire/des/w12.des rename to prism/examples/des/firewire/w12.des diff --git a/prism/examples/pta/firewire/des/w21.des b/prism/examples/des/firewire/w21.des similarity index 100% rename from prism/examples/pta/firewire/des/w21.des rename to prism/examples/des/firewire/w21.des diff --git a/prism/examples/pta/repudiation/des/args b/prism/examples/des/repudiation/args similarity index 100% rename from prism/examples/pta/repudiation/des/args rename to prism/examples/des/repudiation/args diff --git a/prism/examples/pta/repudiation/des/honest_deadline10.des b/prism/examples/des/repudiation/honest_deadline10.des similarity index 100% rename from prism/examples/pta/repudiation/des/honest_deadline10.des rename to prism/examples/des/repudiation/honest_deadline10.des diff --git a/prism/examples/pta/repudiation/des/honest_deadline100.des b/prism/examples/des/repudiation/honest_deadline100.des similarity index 100% rename from prism/examples/pta/repudiation/des/honest_deadline100.des rename to prism/examples/des/repudiation/honest_deadline100.des diff --git a/prism/examples/pta/repudiation/des/honest_deadline20.des b/prism/examples/des/repudiation/honest_deadline20.des similarity index 100% rename from prism/examples/pta/repudiation/des/honest_deadline20.des rename to prism/examples/des/repudiation/honest_deadline20.des diff --git a/prism/examples/pta/repudiation/des/honest_deadline4.des b/prism/examples/des/repudiation/honest_deadline4.des similarity index 100% rename from prism/examples/pta/repudiation/des/honest_deadline4.des rename to prism/examples/des/repudiation/honest_deadline4.des diff --git a/prism/examples/pta/repudiation/des/honest_deadline40.des b/prism/examples/des/repudiation/honest_deadline40.des similarity index 100% rename from prism/examples/pta/repudiation/des/honest_deadline40.des rename to prism/examples/des/repudiation/honest_deadline40.des diff --git a/prism/examples/pta/repudiation/des/honest_deadline6.des b/prism/examples/des/repudiation/honest_deadline6.des similarity index 100% rename from prism/examples/pta/repudiation/des/honest_deadline6.des rename to prism/examples/des/repudiation/honest_deadline6.des diff --git a/prism/examples/pta/repudiation/des/honest_deadline8.des b/prism/examples/des/repudiation/honest_deadline8.des similarity index 100% rename from prism/examples/pta/repudiation/des/honest_deadline8.des rename to prism/examples/des/repudiation/honest_deadline8.des diff --git a/prism/examples/pta/repudiation/des/honest_deadline80.des b/prism/examples/des/repudiation/honest_deadline80.des similarity index 100% rename from prism/examples/pta/repudiation/des/honest_deadline80.des rename to prism/examples/des/repudiation/honest_deadline80.des diff --git a/prism/examples/pta/repudiation/des/malicous_deadline10.des b/prism/examples/des/repudiation/malicous_deadline10.des similarity index 100% rename from prism/examples/pta/repudiation/des/malicous_deadline10.des rename to prism/examples/des/repudiation/malicous_deadline10.des diff --git a/prism/examples/pta/repudiation/des/malicous_deadline100.des b/prism/examples/des/repudiation/malicous_deadline100.des similarity index 100% rename from prism/examples/pta/repudiation/des/malicous_deadline100.des rename to prism/examples/des/repudiation/malicous_deadline100.des diff --git a/prism/examples/pta/repudiation/des/malicous_deadline20.des b/prism/examples/des/repudiation/malicous_deadline20.des similarity index 100% rename from prism/examples/pta/repudiation/des/malicous_deadline20.des rename to prism/examples/des/repudiation/malicous_deadline20.des diff --git a/prism/examples/pta/repudiation/des/malicous_deadline4.des b/prism/examples/des/repudiation/malicous_deadline4.des similarity index 100% rename from prism/examples/pta/repudiation/des/malicous_deadline4.des rename to prism/examples/des/repudiation/malicous_deadline4.des diff --git a/prism/examples/pta/repudiation/des/malicous_deadline40.des b/prism/examples/des/repudiation/malicous_deadline40.des similarity index 100% rename from prism/examples/pta/repudiation/des/malicous_deadline40.des rename to prism/examples/des/repudiation/malicous_deadline40.des diff --git a/prism/examples/pta/repudiation/des/malicous_deadline5.des b/prism/examples/des/repudiation/malicous_deadline5.des similarity index 100% rename from prism/examples/pta/repudiation/des/malicous_deadline5.des rename to prism/examples/des/repudiation/malicous_deadline5.des diff --git a/prism/examples/pta/repudiation/des/malicous_deadline6.des b/prism/examples/des/repudiation/malicous_deadline6.des similarity index 100% rename from prism/examples/pta/repudiation/des/malicous_deadline6.des rename to prism/examples/des/repudiation/malicous_deadline6.des diff --git a/prism/examples/pta/repudiation/des/malicous_deadline8.des b/prism/examples/des/repudiation/malicous_deadline8.des similarity index 100% rename from prism/examples/pta/repudiation/des/malicous_deadline8.des rename to prism/examples/des/repudiation/malicous_deadline8.des diff --git a/prism/examples/pta/repudiation/des/malicous_deadline80.des b/prism/examples/des/repudiation/malicous_deadline80.des similarity index 100% rename from prism/examples/pta/repudiation/des/malicous_deadline80.des rename to prism/examples/des/repudiation/malicous_deadline80.des diff --git a/prism/examples/pta/repudiation/des/malicous_recipient.des b/prism/examples/des/repudiation/malicous_recipient.des similarity index 100% rename from prism/examples/pta/repudiation/des/malicous_recipient.des rename to prism/examples/des/repudiation/malicous_recipient.des diff --git a/prism/examples/pta/repudiation/des/malicous_recipient_complex.des b/prism/examples/des/repudiation/malicous_recipient_complex.des similarity index 100% rename from prism/examples/pta/repudiation/des/malicous_recipient_complex.des rename to prism/examples/des/repudiation/malicous_recipient_complex.des diff --git a/prism/examples/pta/repudiation/des/models b/prism/examples/des/repudiation/models similarity index 100% rename from prism/examples/pta/repudiation/des/models rename to prism/examples/des/repudiation/models diff --git a/prism/examples/pta/repudiation/des/originator.des b/prism/examples/des/repudiation/originator.des similarity index 100% rename from prism/examples/pta/repudiation/des/originator.des rename to prism/examples/des/repudiation/originator.des diff --git a/prism/examples/pta/repudiation/des/recipient.des b/prism/examples/des/repudiation/recipient.des similarity index 100% rename from prism/examples/pta/repudiation/des/recipient.des rename to prism/examples/des/repudiation/recipient.des diff --git a/prism/examples/pta/repudiation/des/repudiation.honest.100.deslist b/prism/examples/des/repudiation/repudiation.honest.100.deslist similarity index 100% rename from prism/examples/pta/repudiation/des/repudiation.honest.100.deslist rename to prism/examples/des/repudiation/repudiation.honest.100.deslist diff --git a/prism/examples/pta/repudiation/des/repudiation.honest.40.deslist b/prism/examples/des/repudiation/repudiation.honest.40.deslist similarity index 100% rename from prism/examples/pta/repudiation/des/repudiation.honest.40.deslist rename to prism/examples/des/repudiation/repudiation.honest.40.deslist diff --git a/prism/examples/pta/repudiation/des/repudiation.honest.80.deslist b/prism/examples/des/repudiation/repudiation.honest.80.deslist similarity index 100% rename from prism/examples/pta/repudiation/des/repudiation.honest.80.deslist rename to prism/examples/des/repudiation/repudiation.honest.80.deslist diff --git a/prism/examples/pta/repudiation/des/repudiation.honest.deslist b/prism/examples/des/repudiation/repudiation.honest.deslist similarity index 100% rename from prism/examples/pta/repudiation/des/repudiation.honest.deslist rename to prism/examples/des/repudiation/repudiation.honest.deslist diff --git a/prism/examples/pta/zeroconf/des/deadline10.des b/prism/examples/des/zeroconf/deadline10.des similarity index 100% rename from prism/examples/pta/zeroconf/des/deadline10.des rename to prism/examples/des/zeroconf/deadline10.des diff --git a/prism/examples/pta/zeroconf/des/deadline100.des b/prism/examples/des/zeroconf/deadline100.des similarity index 100% rename from prism/examples/pta/zeroconf/des/deadline100.des rename to prism/examples/des/zeroconf/deadline100.des diff --git a/prism/examples/pta/zeroconf/des/deadline15.des b/prism/examples/des/zeroconf/deadline15.des similarity index 100% rename from prism/examples/pta/zeroconf/des/deadline15.des rename to prism/examples/des/zeroconf/deadline15.des diff --git a/prism/examples/pta/zeroconf/des/deadline20.des b/prism/examples/des/zeroconf/deadline20.des similarity index 100% rename from prism/examples/pta/zeroconf/des/deadline20.des rename to prism/examples/des/zeroconf/deadline20.des diff --git a/prism/examples/pta/zeroconf/des/deadline25.des b/prism/examples/des/zeroconf/deadline25.des similarity index 100% rename from prism/examples/pta/zeroconf/des/deadline25.des rename to prism/examples/des/zeroconf/deadline25.des diff --git a/prism/examples/pta/zeroconf/des/deadline50.des b/prism/examples/des/zeroconf/deadline50.des similarity index 100% rename from prism/examples/pta/zeroconf/des/deadline50.des rename to prism/examples/des/zeroconf/deadline50.des diff --git a/prism/examples/pta/zeroconf/des/environment.des b/prism/examples/des/zeroconf/environment.des similarity index 100% rename from prism/examples/pta/zeroconf/des/environment.des rename to prism/examples/des/zeroconf/environment.des diff --git a/prism/examples/pta/zeroconf/des/sender4.des b/prism/examples/des/zeroconf/sender4.des similarity index 100% rename from prism/examples/pta/zeroconf/des/sender4.des rename to prism/examples/des/zeroconf/sender4.des diff --git a/prism/examples/pta/zeroconf/des/simple4.des b/prism/examples/des/zeroconf/simple4.des similarity index 100% rename from prism/examples/pta/zeroconf/des/simple4.des rename to prism/examples/des/zeroconf/simple4.des diff --git a/prism/examples/pta/zeroconf/des/simple4_deadline.des b/prism/examples/des/zeroconf/simple4_deadline.des similarity index 100% rename from prism/examples/pta/zeroconf/des/simple4_deadline.des rename to prism/examples/des/zeroconf/simple4_deadline.des diff --git a/prism/examples/pta/csma-prism.sh b/prism/examples/pta/csma-prism.sh deleted file mode 100755 index 3362c68b..00000000 --- a/prism/examples/pta/csma-prism.sh +++ /dev/null @@ -1,24 +0,0 @@ -#!/bin/sh - -# abstract (time bounded) - -prism-explicit csma/abst/{csma.nm,eventually.pctl} -aroptions refine=all,nopre,opt -const bmax=1 - -prism-explicit csma/abst/{csma.nm,deadline.pctl} -const bmax=1 -const T=1000 -aroptions refine=all,nopre,opt -prism-explicit csma/abst/{csma.nm,deadline.pctl} -const bmax=1 -const T=2000 -aroptions refine=all,nopre,opt -prism-explicit csma/abst/{csma.nm,deadline.pctl} -const bmax=1 -const T=3000 -aroptions refine=all,nopre,opt - - -# full (collisions) - -prism-explicit csma/{csma.nm,collisions.pctl} -const bmax=2,K=4 -aroptions refine=all,nopre,opt -prism-explicit csma/{csma.nm,collisions.pctl} -const bmax=2,K=8 -aroptions refine=all,nopre,opt -prism-explicit csma/{csma.nm,collisions.pctl} -const bmax=4,K=4 -aroptions refine=all,nopre,opt -prism-explicit csma/{csma.nm,collisions.pctl} -const bmax=4,K=8 -aroptions refine=all,nopre,opt - -prism-explicit csma/{csma.nm,time.pctl} -const bmax=1,K=0 -aroptions refine=all,nopre,opt -prism-explicit csma/{csma.nm,time.pctl} -const bmax=2,K=0 -aroptions refine=all,nopre,opt -prism-explicit csma/{csma.nm,time.pctl} -const bmax=3,K=0 -aroptions refine=all,nopre,opt -prism-explicit csma/{csma.nm,time.pctl} -const bmax=4,K=0 -aroptions refine=all,nopre,opt - - diff --git a/prism/examples/pta/firewire-prism.sh b/prism/examples/pta/firewire-prism.sh deleted file mode 100755 index 7db09c41..00000000 --- a/prism/examples/pta/firewire-prism.sh +++ /dev/null @@ -1,21 +0,0 @@ -#!/bin/sh - -# abst - -prism-explicit firewire/abst/{firewire.nm,eventually.pctl} -const delay=360 -aroptions nopre,refine=all,opt - -prism-explicit firewire/abst/{firewire.nm,deadline.pctl} -const delay=360,T=5000 -aroptions nopre,refine=all,opt -prism-explicit firewire/abst/{firewire.nm,deadline.pctl} -const delay=360,T=10000 -aroptions nopre,refine=all,opt -prism-explicit firewire/abst/{firewire.nm,deadline.pctl} -const delay=360,T=20000 -aroptions nopre,refine=all,opt - -prism-explicit firewire/abst/{firewire.nm,time.pctl} -const delay=360 -aroptions nopre,refine=all,opt - -# impl - -prism-explicit firewire/impl/{firewire.nm,eventually.pctl} -const delay=360 -aroptions nopre,refine=all,opt - -prism-explicit firewire/impl/{firewire.nm,deadline.pctl} -const delay=360,T=2500 -aroptions nopre,refine=all,opt -prism-explicit firewire/impl/{firewire.nm,deadline.pctl} -const delay=360,T=5000 -aroptions nopre,refine=all,opt -prism-explicit firewire/impl/{firewire.nm,deadline.pctl} -const delay=360,T=7500 -aroptions nopre,refine=all,opt - - diff --git a/prism/examples/pta/firewire/abst/auto b/prism/examples/pta/firewire/abst/auto new file mode 100755 index 00000000..5c8f410d --- /dev/null +++ b/prism/examples/pta/firewire/abst/auto @@ -0,0 +1,9 @@ +#!/bin/csh + +prism firewire/abst/{firewire.nm,eventually.pctl} -const delay=360 -aroptions nopre,refine=all,opt + +prism firewire/abst/{firewire.nm,deadline.pctl} -const delay=360,T=5000 -aroptions nopre,refine=all,opt +prism firewire/abst/{firewire.nm,deadline.pctl} -const delay=360,T=10000 -aroptions nopre,refine=all,opt +prism firewire/abst/{firewire.nm,deadline.pctl} -const delay=360,T=20000 -aroptions nopre,refine=all,opt + +#prism firewire/abst/{firewire.nm,time.pctl} -const delay=360 -aroptions nopre,refine=all,opt diff --git a/prism/examples/pta/firewire/impl/auto b/prism/examples/pta/firewire/impl/auto new file mode 100755 index 00000000..5cffdb63 --- /dev/null +++ b/prism/examples/pta/firewire/impl/auto @@ -0,0 +1,7 @@ +#!/bin/csh + +prism firewire.nm eventually.pctl -const delay=360 -aroptions nopre,refine=all,opt + +prism firewire.nm deadline.pctl -const delay=360,T=2500 -aroptions nopre,refine=all,opt +prism firewire.nm deadline.pctl -const delay=360,T=5000 -aroptions nopre,refine=all,opt +prism firewire.nm deadline.pctl -const delay=360,T=7500 -aroptions nopre,refine=all,opt diff --git a/prism/examples/pta/repudiation-prism.sh b/prism/examples/pta/repudiation-prism.sh deleted file mode 100755 index d114b159..00000000 --- a/prism/examples/pta/repudiation-prism.sh +++ /dev/null @@ -1,14 +0,0 @@ -#!/bin/sh - -# honest -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 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 -