From b62effdfeb9ac8fa9c5bf6ea35daaf0b8911384f Mon Sep 17 00:00:00 2001 From: Dave Parker Date: Thu, 21 Jan 2010 22:52:29 +0000 Subject: [PATCH] Some tidying of PTA examples. git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@1696 bbc10eb1-c90d-0410-af57-cb519fbb1720 --- .../firewire/des => des/firewire}/abs.des | 0 .../firewire/des => des/firewire}/abs1000.des | 0 .../firewire/des => des/firewire}/abs200.des | 0 .../firewire/des => des/firewire}/abs2000.des | 0 .../firewire/des => des/firewire}/abs400.des | 0 .../firewire/des => des/firewire}/abs500.des | 0 .../firewire/des => des/firewire}/abs600.des | 0 .../firewire/des => des/firewire}/abs800.des | 0 .../des => des/firewire}/deadline1000.des | 0 .../des => des/firewire}/deadline200.des | 0 .../des => des/firewire}/deadline2000.des | 0 .../des => des/firewire}/deadline250.des | 0 .../des => des/firewire}/deadline300.des | 0 .../des => des/firewire}/deadline400.des | 0 .../des => des/firewire}/deadline500.des | 0 .../des => des/firewire}/deadline600.des | 0 .../des => des/firewire}/deadline750.des | 0 .../des => des/firewire}/deadline800.des | 0 .../{pta/firewire/des => des/firewire}/n1.des | 0 .../{pta/firewire/des => des/firewire}/n2.des | 0 .../firewire/des => des/firewire}/w12.des | 0 .../firewire/des => des/firewire}/w21.des | 0 .../repudiation/des => des/repudiation}/args | 0 .../repudiation}/honest_deadline10.des | 0 .../repudiation}/honest_deadline100.des | 0 .../repudiation}/honest_deadline20.des | 0 .../repudiation}/honest_deadline4.des | 0 .../repudiation}/honest_deadline40.des | 0 .../repudiation}/honest_deadline6.des | 0 .../repudiation}/honest_deadline8.des | 0 .../repudiation}/honest_deadline80.des | 0 .../repudiation}/malicous_deadline10.des | 0 .../repudiation}/malicous_deadline100.des | 0 .../repudiation}/malicous_deadline20.des | 0 .../repudiation}/malicous_deadline4.des | 0 .../repudiation}/malicous_deadline40.des | 0 .../repudiation}/malicous_deadline5.des | 0 .../repudiation}/malicous_deadline6.des | 0 .../repudiation}/malicous_deadline8.des | 0 .../repudiation}/malicous_deadline80.des | 0 .../repudiation}/malicous_recipient.des | 0 .../malicous_recipient_complex.des | 0 .../des => des/repudiation}/models | 0 .../des => des/repudiation}/originator.des | 0 .../des => des/repudiation}/recipient.des | 0 .../repudiation.honest.100.deslist | 0 .../repudiation.honest.40.deslist | 0 .../repudiation.honest.80.deslist | 0 .../repudiation}/repudiation.honest.deslist | 0 .../des => des/zeroconf}/deadline10.des | 0 .../des => des/zeroconf}/deadline100.des | 0 .../des => des/zeroconf}/deadline15.des | 0 .../des => des/zeroconf}/deadline20.des | 0 .../des => des/zeroconf}/deadline25.des | 0 .../des => des/zeroconf}/deadline50.des | 0 .../des => des/zeroconf}/environment.des | 0 .../zeroconf/des => des/zeroconf}/sender4.des | 0 .../zeroconf/des => des/zeroconf}/simple4.des | 0 .../des => des/zeroconf}/simple4_deadline.des | 0 prism/examples/pta/csma-prism.sh | 24 ------------------- prism/examples/pta/firewire-prism.sh | 21 ---------------- prism/examples/pta/firewire/abst/auto | 9 +++++++ prism/examples/pta/firewire/impl/auto | 7 ++++++ prism/examples/pta/repudiation-prism.sh | 14 ----------- 64 files changed, 16 insertions(+), 59 deletions(-) rename prism/examples/{pta/firewire/des => des/firewire}/abs.des (100%) rename prism/examples/{pta/firewire/des => des/firewire}/abs1000.des (100%) rename prism/examples/{pta/firewire/des => des/firewire}/abs200.des (100%) rename prism/examples/{pta/firewire/des => des/firewire}/abs2000.des (100%) rename prism/examples/{pta/firewire/des => des/firewire}/abs400.des (100%) rename prism/examples/{pta/firewire/des => des/firewire}/abs500.des (100%) rename prism/examples/{pta/firewire/des => des/firewire}/abs600.des (100%) rename prism/examples/{pta/firewire/des => des/firewire}/abs800.des (100%) rename prism/examples/{pta/firewire/des => des/firewire}/deadline1000.des (100%) rename prism/examples/{pta/firewire/des => des/firewire}/deadline200.des (100%) rename prism/examples/{pta/firewire/des => des/firewire}/deadline2000.des (100%) rename prism/examples/{pta/firewire/des => des/firewire}/deadline250.des (100%) rename prism/examples/{pta/firewire/des => des/firewire}/deadline300.des (100%) rename prism/examples/{pta/firewire/des => des/firewire}/deadline400.des (100%) rename prism/examples/{pta/firewire/des => des/firewire}/deadline500.des (100%) rename prism/examples/{pta/firewire/des => des/firewire}/deadline600.des (100%) rename prism/examples/{pta/firewire/des => des/firewire}/deadline750.des (100%) rename prism/examples/{pta/firewire/des => des/firewire}/deadline800.des (100%) rename prism/examples/{pta/firewire/des => des/firewire}/n1.des (100%) rename prism/examples/{pta/firewire/des => des/firewire}/n2.des (100%) rename prism/examples/{pta/firewire/des => des/firewire}/w12.des (100%) rename prism/examples/{pta/firewire/des => des/firewire}/w21.des (100%) rename prism/examples/{pta/repudiation/des => des/repudiation}/args (100%) rename prism/examples/{pta/repudiation/des => des/repudiation}/honest_deadline10.des (100%) rename prism/examples/{pta/repudiation/des => des/repudiation}/honest_deadline100.des (100%) rename prism/examples/{pta/repudiation/des => des/repudiation}/honest_deadline20.des (100%) rename prism/examples/{pta/repudiation/des => des/repudiation}/honest_deadline4.des (100%) rename prism/examples/{pta/repudiation/des => des/repudiation}/honest_deadline40.des (100%) rename prism/examples/{pta/repudiation/des => des/repudiation}/honest_deadline6.des (100%) rename prism/examples/{pta/repudiation/des => des/repudiation}/honest_deadline8.des (100%) rename prism/examples/{pta/repudiation/des => des/repudiation}/honest_deadline80.des (100%) rename prism/examples/{pta/repudiation/des => des/repudiation}/malicous_deadline10.des (100%) rename prism/examples/{pta/repudiation/des => des/repudiation}/malicous_deadline100.des (100%) rename prism/examples/{pta/repudiation/des => des/repudiation}/malicous_deadline20.des (100%) rename prism/examples/{pta/repudiation/des => des/repudiation}/malicous_deadline4.des (100%) rename prism/examples/{pta/repudiation/des => des/repudiation}/malicous_deadline40.des (100%) rename prism/examples/{pta/repudiation/des => des/repudiation}/malicous_deadline5.des (100%) rename prism/examples/{pta/repudiation/des => des/repudiation}/malicous_deadline6.des (100%) rename prism/examples/{pta/repudiation/des => des/repudiation}/malicous_deadline8.des (100%) rename prism/examples/{pta/repudiation/des => des/repudiation}/malicous_deadline80.des (100%) rename prism/examples/{pta/repudiation/des => des/repudiation}/malicous_recipient.des (100%) rename prism/examples/{pta/repudiation/des => des/repudiation}/malicous_recipient_complex.des (100%) rename prism/examples/{pta/repudiation/des => des/repudiation}/models (100%) rename prism/examples/{pta/repudiation/des => des/repudiation}/originator.des (100%) rename prism/examples/{pta/repudiation/des => des/repudiation}/recipient.des (100%) rename prism/examples/{pta/repudiation/des => des/repudiation}/repudiation.honest.100.deslist (100%) rename prism/examples/{pta/repudiation/des => des/repudiation}/repudiation.honest.40.deslist (100%) rename prism/examples/{pta/repudiation/des => des/repudiation}/repudiation.honest.80.deslist (100%) rename prism/examples/{pta/repudiation/des => des/repudiation}/repudiation.honest.deslist (100%) rename prism/examples/{pta/zeroconf/des => des/zeroconf}/deadline10.des (100%) rename prism/examples/{pta/zeroconf/des => des/zeroconf}/deadline100.des (100%) rename prism/examples/{pta/zeroconf/des => des/zeroconf}/deadline15.des (100%) rename prism/examples/{pta/zeroconf/des => des/zeroconf}/deadline20.des (100%) rename prism/examples/{pta/zeroconf/des => des/zeroconf}/deadline25.des (100%) rename prism/examples/{pta/zeroconf/des => des/zeroconf}/deadline50.des (100%) rename prism/examples/{pta/zeroconf/des => des/zeroconf}/environment.des (100%) rename prism/examples/{pta/zeroconf/des => des/zeroconf}/sender4.des (100%) rename prism/examples/{pta/zeroconf/des => des/zeroconf}/simple4.des (100%) rename prism/examples/{pta/zeroconf/des => des/zeroconf}/simple4_deadline.des (100%) delete mode 100755 prism/examples/pta/csma-prism.sh delete mode 100755 prism/examples/pta/firewire-prism.sh create mode 100755 prism/examples/pta/firewire/abst/auto create mode 100755 prism/examples/pta/firewire/impl/auto delete mode 100755 prism/examples/pta/repudiation-prism.sh 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 -