Some tidying of PTA examples.

git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@1695 bbc10eb1-c90d-0410-af57-cb519fbb1720

prism/examples/pta/csma-prism.sh

@@ -1,3 +1,4 @@
+#!/bin/sh
 
 # abstract (time bounded)
 

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

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

prism/examples/pta/firewire-prism.sh

@@ -1,3 +1,4 @@
+#!/bin/sh
 
 # abst
 

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
 

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

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

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