Some tidying of PTA examples.

git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@1696 bbc10eb1-c90d-0410-af57-cb519fbb1720
16 years ago · b62effdfeb
64 changed files with 16 additions and 59 deletions
--- a/prism/examples/pta/firewire/des/abs.des
+++ b/prism/examples/pta/firewire/des/abs.des
--- a/prism/examples/pta/firewire/des/abs1000.des
+++ b/prism/examples/pta/firewire/des/abs1000.des
--- a/prism/examples/pta/firewire/des/abs200.des
+++ b/prism/examples/pta/firewire/des/abs200.des
--- a/prism/examples/pta/firewire/des/abs2000.des
+++ b/prism/examples/pta/firewire/des/abs2000.des
--- a/prism/examples/pta/firewire/des/abs400.des
+++ b/prism/examples/pta/firewire/des/abs400.des
--- a/prism/examples/pta/firewire/des/abs500.des
+++ b/prism/examples/pta/firewire/des/abs500.des
--- a/prism/examples/pta/firewire/des/abs600.des
+++ b/prism/examples/pta/firewire/des/abs600.des
--- a/prism/examples/pta/firewire/des/abs800.des
+++ b/prism/examples/pta/firewire/des/abs800.des
--- a/prism/examples/pta/firewire/des/deadline1000.des
+++ b/prism/examples/pta/firewire/des/deadline1000.des
--- a/prism/examples/pta/firewire/des/deadline200.des
+++ b/prism/examples/pta/firewire/des/deadline200.des
--- a/prism/examples/pta/firewire/des/deadline2000.des
+++ b/prism/examples/pta/firewire/des/deadline2000.des
--- a/prism/examples/pta/firewire/des/deadline250.des
+++ b/prism/examples/pta/firewire/des/deadline250.des
--- a/prism/examples/pta/firewire/des/deadline300.des
+++ b/prism/examples/pta/firewire/des/deadline300.des
--- a/prism/examples/pta/firewire/des/deadline400.des
+++ b/prism/examples/pta/firewire/des/deadline400.des
--- a/prism/examples/pta/firewire/des/deadline500.des
+++ b/prism/examples/pta/firewire/des/deadline500.des
--- a/prism/examples/pta/firewire/des/deadline600.des
+++ b/prism/examples/pta/firewire/des/deadline600.des
--- a/prism/examples/pta/firewire/des/deadline750.des
+++ b/prism/examples/pta/firewire/des/deadline750.des
--- a/prism/examples/pta/firewire/des/deadline800.des
+++ b/prism/examples/pta/firewire/des/deadline800.des
--- a/prism/examples/pta/firewire/des/n1.des
+++ b/prism/examples/pta/firewire/des/n1.des
--- a/prism/examples/pta/firewire/des/n2.des
+++ b/prism/examples/pta/firewire/des/n2.des
--- a/prism/examples/pta/firewire/des/w12.des
+++ b/prism/examples/pta/firewire/des/w12.des
--- a/prism/examples/pta/firewire/des/w21.des
+++ b/prism/examples/pta/firewire/des/w21.des
--- a/prism/examples/pta/repudiation/des/args
+++ b/prism/examples/pta/repudiation/des/args
--- a/prism/examples/pta/repudiation/des/honest_deadline10.des
+++ b/prism/examples/pta/repudiation/des/honest_deadline10.des
--- a/prism/examples/pta/repudiation/des/honest_deadline100.des
+++ b/prism/examples/pta/repudiation/des/honest_deadline100.des
--- a/prism/examples/pta/repudiation/des/honest_deadline20.des
+++ b/prism/examples/pta/repudiation/des/honest_deadline20.des
--- a/prism/examples/pta/repudiation/des/honest_deadline4.des
+++ b/prism/examples/pta/repudiation/des/honest_deadline4.des
--- a/prism/examples/pta/repudiation/des/honest_deadline40.des
+++ b/prism/examples/pta/repudiation/des/honest_deadline40.des
--- a/prism/examples/pta/repudiation/des/honest_deadline6.des
+++ b/prism/examples/pta/repudiation/des/honest_deadline6.des
--- a/prism/examples/pta/repudiation/des/honest_deadline8.des
+++ b/prism/examples/pta/repudiation/des/honest_deadline8.des
--- a/prism/examples/pta/repudiation/des/honest_deadline80.des
+++ b/prism/examples/pta/repudiation/des/honest_deadline80.des
--- a/prism/examples/pta/repudiation/des/malicous_deadline10.des
+++ b/prism/examples/pta/repudiation/des/malicous_deadline10.des
--- a/prism/examples/pta/repudiation/des/malicous_deadline100.des
+++ b/prism/examples/pta/repudiation/des/malicous_deadline100.des
--- a/prism/examples/pta/repudiation/des/malicous_deadline20.des
+++ b/prism/examples/pta/repudiation/des/malicous_deadline20.des
--- a/prism/examples/pta/repudiation/des/malicous_deadline4.des
+++ b/prism/examples/pta/repudiation/des/malicous_deadline4.des
--- a/prism/examples/pta/repudiation/des/malicous_deadline40.des
+++ b/prism/examples/pta/repudiation/des/malicous_deadline40.des
--- a/prism/examples/pta/repudiation/des/malicous_deadline5.des
+++ b/prism/examples/pta/repudiation/des/malicous_deadline5.des
--- a/prism/examples/pta/repudiation/des/malicous_deadline6.des
+++ b/prism/examples/pta/repudiation/des/malicous_deadline6.des
--- a/prism/examples/pta/repudiation/des/malicous_deadline8.des
+++ b/prism/examples/pta/repudiation/des/malicous_deadline8.des
--- a/prism/examples/pta/repudiation/des/malicous_deadline80.des
+++ b/prism/examples/pta/repudiation/des/malicous_deadline80.des
--- a/prism/examples/pta/repudiation/des/malicous_recipient.des
+++ b/prism/examples/pta/repudiation/des/malicous_recipient.des
--- a/prism/examples/pta/repudiation/des/malicous_recipient_complex.des
+++ b/prism/examples/pta/repudiation/des/malicous_recipient_complex.des
--- a/prism/examples/pta/repudiation/des/models
+++ b/prism/examples/pta/repudiation/des/models
--- a/prism/examples/pta/repudiation/des/originator.des
+++ b/prism/examples/pta/repudiation/des/originator.des
--- a/prism/examples/pta/repudiation/des/recipient.des
+++ b/prism/examples/pta/repudiation/des/recipient.des
--- a/prism/examples/pta/repudiation/des/repudiation.honest.100.deslist
+++ b/prism/examples/pta/repudiation/des/repudiation.honest.100.deslist
--- a/prism/examples/pta/repudiation/des/repudiation.honest.40.deslist
+++ b/prism/examples/pta/repudiation/des/repudiation.honest.40.deslist
--- a/prism/examples/pta/repudiation/des/repudiation.honest.80.deslist
+++ b/prism/examples/pta/repudiation/des/repudiation.honest.80.deslist
--- a/prism/examples/pta/repudiation/des/repudiation.honest.deslist
+++ b/prism/examples/pta/repudiation/des/repudiation.honest.deslist
--- a/prism/examples/pta/zeroconf/des/deadline10.des
+++ b/prism/examples/pta/zeroconf/des/deadline10.des
--- a/prism/examples/pta/zeroconf/des/deadline100.des
+++ b/prism/examples/pta/zeroconf/des/deadline100.des
--- a/prism/examples/pta/zeroconf/des/deadline15.des
+++ b/prism/examples/pta/zeroconf/des/deadline15.des
--- a/prism/examples/pta/zeroconf/des/deadline20.des
+++ b/prism/examples/pta/zeroconf/des/deadline20.des
--- a/prism/examples/pta/zeroconf/des/deadline25.des
+++ b/prism/examples/pta/zeroconf/des/deadline25.des
--- a/prism/examples/pta/zeroconf/des/deadline50.des
+++ b/prism/examples/pta/zeroconf/des/deadline50.des
--- a/prism/examples/pta/zeroconf/des/environment.des
+++ b/prism/examples/pta/zeroconf/des/environment.des
--- a/prism/examples/pta/zeroconf/des/sender4.des
+++ b/prism/examples/pta/zeroconf/des/sender4.des
--- a/prism/examples/pta/zeroconf/des/simple4.des
+++ b/prism/examples/pta/zeroconf/des/simple4.des
--- a/prism/examples/pta/zeroconf/des/simple4_deadline.des
+++ b/prism/examples/pta/zeroconf/des/simple4_deadline.des
--- a/prism/examples/pta/csma-prism.sh
+++ b/prism/examples/pta/csma-prism.sh
@ -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
-
-
--- a/prism/examples/pta/firewire-prism.sh
+++ b/prism/examples/pta/firewire-prism.sh
@ -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
-
-
--- a/prism/examples/pta/firewire/abst/auto
+++ 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
--- a/prism/examples/pta/firewire/impl/auto
+++ 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
--- a/prism/examples/pta/repudiation-prism.sh
+++ b/prism/examples/pta/repudiation-prism.sh
@ -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
-