From c38ee3656207752af9c8be266ee9e4ae6080c255 Mon Sep 17 00:00:00 2001 From: Dave Parker Date: Thu, 21 Jan 2010 22:42:45 +0000 Subject: [PATCH] Some tidying of PTA examples. git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@1695 bbc10eb1-c90d-0410-af57-cb519fbb1720 --- .../examples/{pta/csma/des => des/csma}/args | 0 .../{pta/csma/des => des/csma}/csma2.deslist | 0 .../{pta/csma/des => des/csma}/csma4.deslist | 0 .../csma/des => des/csma}/csmacd-bmax1-s1.des | 0 .../csma/des => des/csma}/csmacd-bmax1-s2.des | 0 .../csma/des => des/csma}/csmacd-bmax2-s1.des | 0 .../csma/des => des/csma}/csmacd-bmax2-s2.des | 0 .../csma/des => des/csma}/csmacd-bmax3-s1.des | 0 .../csma/des => des/csma}/csmacd-bmax3-s2.des | 0 .../csma/des => des/csma}/csmacd-bmax4-s1.des | 0 .../csma/des => des/csma}/csmacd-bmax4-s2.des | 0 .../csma/des => des/csma}/csmacd-bmax5-s1.des | 0 .../csma/des => des/csma}/csmacd-bmax5-s2.des | 0 .../{pta/csma/des => des/csma}/csmacd-bus.des | 0 .../csma}/csmacd-collision-counter.des | 0 .../csma/des => des/csma}/deadline2000.des | 0 .../csma/des => des/csma}/deadline4000.des | 0 .../{pta/csma/des => des/csma}/models | 0 prism/examples/pta/csma-prism.sh | 1 + prism/examples/pta/csma/abst/auto | 11 ++++++++++ prism/examples/pta/csma/{ => full}/args | 0 prism/examples/pta/csma/full/auto | 7 +++++++ .../pta/csma/{ => full}/collisions.pctl | 0 .../pta/csma/{ => full}/csma-digital.nm | 0 .../pta/csma/{ => full}/csma-slots.nm | 0 prism/examples/pta/csma/{ => full}/csma.nm | 0 .../pta/csma/{ => full}/eventually.pctl | 0 prism/examples/pta/csma/{ => full}/models | 0 prism/examples/pta/csma/{ => full}/props | 0 prism/examples/pta/csma/{ => full}/time.pctl | 0 prism/examples/pta/firewire-prism.sh | 1 + prism/examples/pta/repudiation-prism.sh | 17 ++++++++-------- prism/examples/pta/repudiation/honest/auto | 7 +++++++ prism/examples/pta/repudiation/malicious/auto | 7 +++++++ prism/examples/pta/zeroconf-prism.sh | 20 +++++++++---------- 35 files changed, 53 insertions(+), 18 deletions(-) rename prism/examples/{pta/csma/des => des/csma}/args (100%) rename prism/examples/{pta/csma/des => des/csma}/csma2.deslist (100%) rename prism/examples/{pta/csma/des => des/csma}/csma4.deslist (100%) rename prism/examples/{pta/csma/des => des/csma}/csmacd-bmax1-s1.des (100%) rename prism/examples/{pta/csma/des => des/csma}/csmacd-bmax1-s2.des (100%) rename prism/examples/{pta/csma/des => des/csma}/csmacd-bmax2-s1.des (100%) rename prism/examples/{pta/csma/des => des/csma}/csmacd-bmax2-s2.des (100%) rename prism/examples/{pta/csma/des => des/csma}/csmacd-bmax3-s1.des (100%) rename prism/examples/{pta/csma/des => des/csma}/csmacd-bmax3-s2.des (100%) rename prism/examples/{pta/csma/des => des/csma}/csmacd-bmax4-s1.des (100%) rename prism/examples/{pta/csma/des => des/csma}/csmacd-bmax4-s2.des (100%) rename prism/examples/{pta/csma/des => des/csma}/csmacd-bmax5-s1.des (100%) rename prism/examples/{pta/csma/des => des/csma}/csmacd-bmax5-s2.des (100%) rename prism/examples/{pta/csma/des => des/csma}/csmacd-bus.des (100%) rename prism/examples/{pta/csma/des => des/csma}/csmacd-collision-counter.des (100%) rename prism/examples/{pta/csma/des => des/csma}/deadline2000.des (100%) rename prism/examples/{pta/csma/des => des/csma}/deadline4000.des (100%) rename prism/examples/{pta/csma/des => des/csma}/models (100%) create mode 100755 prism/examples/pta/csma/abst/auto rename prism/examples/pta/csma/{ => full}/args (100%) create mode 100755 prism/examples/pta/csma/full/auto rename prism/examples/pta/csma/{ => full}/collisions.pctl (100%) rename prism/examples/pta/csma/{ => full}/csma-digital.nm (100%) rename prism/examples/pta/csma/{ => full}/csma-slots.nm (100%) rename prism/examples/pta/csma/{ => full}/csma.nm (100%) rename prism/examples/pta/csma/{ => full}/eventually.pctl (100%) rename prism/examples/pta/csma/{ => full}/models (100%) rename prism/examples/pta/csma/{ => full}/props (100%) rename prism/examples/pta/csma/{ => full}/time.pctl (100%) create mode 100755 prism/examples/pta/repudiation/honest/auto create mode 100755 prism/examples/pta/repudiation/malicious/auto 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