From 753ff0e1fa3474bcd5c4eb2e4e6580a465751c07 Mon Sep 17 00:00:00 2001
From: Dave Parker <dave.x.parker@gmail.com>
Date: Fri, 3 Dec 2010 11:04:39 +0000
Subject: [PATCH] Small tidies in PTA examples.

git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@2317 bbc10eb1-c90d-0410-af57-cb519fbb1720
---
 prism-examples/pta/csma/abst/{args => .args}                 | 0
 prism-examples/pta/csma/abst/{models => .models}             | 0
 prism-examples/pta/csma/abst/{props => .props}               | 0
 prism-examples/pta/csma/full/{args => .args}                 | 0
 prism-examples/pta/csma/full/{models => .models}             | 0
 prism-examples/pta/csma/full/{props => .props}               | 0
 prism-examples/pta/csma/full/auto                            | 2 +-
 prism-examples/pta/firewire/abst/{args => .args}             | 0
 prism-examples/pta/firewire/abst/{models => .models}         | 0
 prism-examples/pta/firewire/abst/{props => .props}           | 0
 prism-examples/pta/firewire/abst/deadline-max.pctl           | 3 +--
 prism-examples/pta/firewire/abst/deadline.pctl               | 1 -
 prism-examples/pta/firewire/abst/eventually.pctl             | 1 -
 prism-examples/pta/firewire/abst/time.pctl                   | 1 -
 prism-examples/pta/firewire/impl/{args => .args}             | 0
 prism-examples/pta/firewire/impl/{models => .models}         | 0
 prism-examples/pta/firewire/impl/{props => .props}           | 0
 prism-examples/pta/firewire/impl/deadline.pctl               | 1 -
 prism-examples/pta/firewire/impl/eventually.pctl             | 1 -
 prism-examples/pta/repudiation/honest/{args => .args}        | 0
 prism-examples/pta/repudiation/honest/{models => .models}    | 0
 prism-examples/pta/repudiation/honest/{props => .props}      | 0
 prism-examples/pta/repudiation/honest/deadline.pctl          | 1 -
 prism-examples/pta/repudiation/honest/eventually.pctl        | 2 --
 prism-examples/pta/repudiation/malicious/{args => .args}     | 0
 prism-examples/pta/repudiation/malicious/{models => .models} | 0
 prism-examples/pta/repudiation/malicious/{props => .props}   | 0
 prism-examples/pta/repudiation/malicious/deadline.pctl       | 1 -
 prism-examples/pta/repudiation/malicious/eventually.pctl     | 2 --
 prism-examples/pta/zeroconf/{args => .args}                  | 0
 prism-examples/pta/zeroconf/{models => .models}              | 0
 prism-examples/pta/zeroconf/{props => .props}                | 0
 prism-examples/pta/zeroconf/time.pctl                        | 2 +-
 33 files changed, 3 insertions(+), 15 deletions(-)
 rename prism-examples/pta/csma/abst/{args => .args} (100%)
 rename prism-examples/pta/csma/abst/{models => .models} (100%)
 rename prism-examples/pta/csma/abst/{props => .props} (100%)
 rename prism-examples/pta/csma/full/{args => .args} (100%)
 rename prism-examples/pta/csma/full/{models => .models} (100%)
 rename prism-examples/pta/csma/full/{props => .props} (100%)
 rename prism-examples/pta/firewire/abst/{args => .args} (100%)
 rename prism-examples/pta/firewire/abst/{models => .models} (100%)
 rename prism-examples/pta/firewire/abst/{props => .props} (100%)
 rename prism-examples/pta/firewire/impl/{args => .args} (100%)
 rename prism-examples/pta/firewire/impl/{models => .models} (100%)
 rename prism-examples/pta/firewire/impl/{props => .props} (100%)
 rename prism-examples/pta/repudiation/honest/{args => .args} (100%)
 rename prism-examples/pta/repudiation/honest/{models => .models} (100%)
 rename prism-examples/pta/repudiation/honest/{props => .props} (100%)
 rename prism-examples/pta/repudiation/malicious/{args => .args} (100%)
 rename prism-examples/pta/repudiation/malicious/{models => .models} (100%)
 rename prism-examples/pta/repudiation/malicious/{props => .props} (100%)
 rename prism-examples/pta/zeroconf/{args => .args} (100%)
 rename prism-examples/pta/zeroconf/{models => .models} (100%)
 rename prism-examples/pta/zeroconf/{props => .props} (100%)

diff --git a/prism-examples/pta/csma/abst/args b/prism-examples/pta/csma/abst/.args
similarity index 100%
rename from prism-examples/pta/csma/abst/args
rename to prism-examples/pta/csma/abst/.args
diff --git a/prism-examples/pta/csma/abst/models b/prism-examples/pta/csma/abst/.models
similarity index 100%
rename from prism-examples/pta/csma/abst/models
rename to prism-examples/pta/csma/abst/.models
diff --git a/prism-examples/pta/csma/abst/props b/prism-examples/pta/csma/abst/.props
similarity index 100%
rename from prism-examples/pta/csma/abst/props
rename to prism-examples/pta/csma/abst/.props
diff --git a/prism-examples/pta/csma/full/args b/prism-examples/pta/csma/full/.args
similarity index 100%
rename from prism-examples/pta/csma/full/args
rename to prism-examples/pta/csma/full/.args
diff --git a/prism-examples/pta/csma/full/models b/prism-examples/pta/csma/full/.models
similarity index 100%
rename from prism-examples/pta/csma/full/models
rename to prism-examples/pta/csma/full/.models
diff --git a/prism-examples/pta/csma/full/props b/prism-examples/pta/csma/full/.props
similarity index 100%
rename from prism-examples/pta/csma/full/props
rename to prism-examples/pta/csma/full/.props
diff --git a/prism-examples/pta/csma/full/auto b/prism-examples/pta/csma/full/auto
index 61845146..a1835eae 100755
--- a/prism-examples/pta/csma/full/auto
+++ b/prism-examples/pta/csma/full/auto
@@ -8,4 +8,4 @@ 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
+#prism csma.nm time.pctl -const bmax=4,K=0 -aroptions refine=all,nopre,opt
diff --git a/prism-examples/pta/firewire/abst/args b/prism-examples/pta/firewire/abst/.args
similarity index 100%
rename from prism-examples/pta/firewire/abst/args
rename to prism-examples/pta/firewire/abst/.args
diff --git a/prism-examples/pta/firewire/abst/models b/prism-examples/pta/firewire/abst/.models
similarity index 100%
rename from prism-examples/pta/firewire/abst/models
rename to prism-examples/pta/firewire/abst/.models
diff --git a/prism-examples/pta/firewire/abst/props b/prism-examples/pta/firewire/abst/.props
similarity index 100%
rename from prism-examples/pta/firewire/abst/props
rename to prism-examples/pta/firewire/abst/.props
diff --git a/prism-examples/pta/firewire/abst/deadline-max.pctl b/prism-examples/pta/firewire/abst/deadline-max.pctl
index 115754ec..9781fd29 100644
--- a/prism-examples/pta/firewire/abst/deadline-max.pctl
+++ b/prism-examples/pta/firewire/abst/deadline-max.pctl
@@ -1,3 +1,2 @@
-// Minimum probability that a leader has been elected by deadline T
+// Maximum probability that a leader has been elected by deadline T
 Pmax=? [ F "done_after" ]
-
diff --git a/prism-examples/pta/firewire/abst/deadline.pctl b/prism-examples/pta/firewire/abst/deadline.pctl
index 70823f35..7a57fc75 100644
--- a/prism-examples/pta/firewire/abst/deadline.pctl
+++ b/prism-examples/pta/firewire/abst/deadline.pctl
@@ -2,4 +2,3 @@ const int T;
 
 // Minimum probability that a leader has been elected by deadline T
 Pmin=? [ F<=T "done" ]
-
diff --git a/prism-examples/pta/firewire/abst/eventually.pctl b/prism-examples/pta/firewire/abst/eventually.pctl
index e43a1887..24fd0254 100644
--- a/prism-examples/pta/firewire/abst/eventually.pctl
+++ b/prism-examples/pta/firewire/abst/eventually.pctl
@@ -1,3 +1,2 @@
 // Minimum probability that a leader is eventually elected
 Pmin=? [ F "done" ]
-
diff --git a/prism-examples/pta/firewire/abst/time.pctl b/prism-examples/pta/firewire/abst/time.pctl
index 40759e49..3bc6504d 100644
--- a/prism-examples/pta/firewire/abst/time.pctl
+++ b/prism-examples/pta/firewire/abst/time.pctl
@@ -1,3 +1,2 @@
 // Maximum expected time to elect a leader
 R{"time"}min=? [ F "done" ]
-
diff --git a/prism-examples/pta/firewire/impl/args b/prism-examples/pta/firewire/impl/.args
similarity index 100%
rename from prism-examples/pta/firewire/impl/args
rename to prism-examples/pta/firewire/impl/.args
diff --git a/prism-examples/pta/firewire/impl/models b/prism-examples/pta/firewire/impl/.models
similarity index 100%
rename from prism-examples/pta/firewire/impl/models
rename to prism-examples/pta/firewire/impl/.models
diff --git a/prism-examples/pta/firewire/impl/props b/prism-examples/pta/firewire/impl/.props
similarity index 100%
rename from prism-examples/pta/firewire/impl/props
rename to prism-examples/pta/firewire/impl/.props
diff --git a/prism-examples/pta/firewire/impl/deadline.pctl b/prism-examples/pta/firewire/impl/deadline.pctl
index 70823f35..7a57fc75 100644
--- a/prism-examples/pta/firewire/impl/deadline.pctl
+++ b/prism-examples/pta/firewire/impl/deadline.pctl
@@ -2,4 +2,3 @@ const int T;
 
 // Minimum probability that a leader has been elected by deadline T
 Pmin=? [ F<=T "done" ]
-
diff --git a/prism-examples/pta/firewire/impl/eventually.pctl b/prism-examples/pta/firewire/impl/eventually.pctl
index e43a1887..24fd0254 100644
--- a/prism-examples/pta/firewire/impl/eventually.pctl
+++ b/prism-examples/pta/firewire/impl/eventually.pctl
@@ -1,3 +1,2 @@
 // Minimum probability that a leader is eventually elected
 Pmin=? [ F "done" ]
-
diff --git a/prism-examples/pta/repudiation/honest/args b/prism-examples/pta/repudiation/honest/.args
similarity index 100%
rename from prism-examples/pta/repudiation/honest/args
rename to prism-examples/pta/repudiation/honest/.args
diff --git a/prism-examples/pta/repudiation/honest/models b/prism-examples/pta/repudiation/honest/.models
similarity index 100%
rename from prism-examples/pta/repudiation/honest/models
rename to prism-examples/pta/repudiation/honest/.models
diff --git a/prism-examples/pta/repudiation/honest/props b/prism-examples/pta/repudiation/honest/.props
similarity index 100%
rename from prism-examples/pta/repudiation/honest/props
rename to prism-examples/pta/repudiation/honest/.props
diff --git a/prism-examples/pta/repudiation/honest/deadline.pctl b/prism-examples/pta/repudiation/honest/deadline.pctl
index 93c25829..4f08fce3 100644
--- a/prism-examples/pta/repudiation/honest/deadline.pctl
+++ b/prism-examples/pta/repudiation/honest/deadline.pctl
@@ -2,4 +2,3 @@ const int T;
 
 // Minimum probability that protocol terminates successfully by the deadline
 Pmin=? [ F<T "terminated_successfully" ]
-
diff --git a/prism-examples/pta/repudiation/honest/eventually.pctl b/prism-examples/pta/repudiation/honest/eventually.pctl
index 0c37f266..8e691a59 100644
--- a/prism-examples/pta/repudiation/honest/eventually.pctl
+++ b/prism-examples/pta/repudiation/honest/eventually.pctl
@@ -1,4 +1,2 @@
-
 // Minimum probability that the protocol terminates successfully
 Pmin=? [ F "terminated_successfully" ]
-
diff --git a/prism-examples/pta/repudiation/malicious/args b/prism-examples/pta/repudiation/malicious/.args
similarity index 100%
rename from prism-examples/pta/repudiation/malicious/args
rename to prism-examples/pta/repudiation/malicious/.args
diff --git a/prism-examples/pta/repudiation/malicious/models b/prism-examples/pta/repudiation/malicious/.models
similarity index 100%
rename from prism-examples/pta/repudiation/malicious/models
rename to prism-examples/pta/repudiation/malicious/.models
diff --git a/prism-examples/pta/repudiation/malicious/props b/prism-examples/pta/repudiation/malicious/.props
similarity index 100%
rename from prism-examples/pta/repudiation/malicious/props
rename to prism-examples/pta/repudiation/malicious/.props
diff --git a/prism-examples/pta/repudiation/malicious/deadline.pctl b/prism-examples/pta/repudiation/malicious/deadline.pctl
index 8633995d..33d9e56d 100644
--- a/prism-examples/pta/repudiation/malicious/deadline.pctl
+++ b/prism-examples/pta/repudiation/malicious/deadline.pctl
@@ -2,4 +2,3 @@ const int T;
 
 // Maximum probability that malicious recepient gains information by deadline T
 Pmax=? [ F<T "gains_information" ]
-
diff --git a/prism-examples/pta/repudiation/malicious/eventually.pctl b/prism-examples/pta/repudiation/malicious/eventually.pctl
index c001aa38..42164463 100644
--- a/prism-examples/pta/repudiation/malicious/eventually.pctl
+++ b/prism-examples/pta/repudiation/malicious/eventually.pctl
@@ -1,4 +1,2 @@
-
 // Maximum probability that malicious recepient gains information
 Pmax=? [ F "gains_information" ]
-
diff --git a/prism-examples/pta/zeroconf/args b/prism-examples/pta/zeroconf/.args
similarity index 100%
rename from prism-examples/pta/zeroconf/args
rename to prism-examples/pta/zeroconf/.args
diff --git a/prism-examples/pta/zeroconf/models b/prism-examples/pta/zeroconf/.models
similarity index 100%
rename from prism-examples/pta/zeroconf/models
rename to prism-examples/pta/zeroconf/.models
diff --git a/prism-examples/pta/zeroconf/props b/prism-examples/pta/zeroconf/.props
similarity index 100%
rename from prism-examples/pta/zeroconf/props
rename to prism-examples/pta/zeroconf/.props
diff --git a/prism-examples/pta/zeroconf/time.pctl b/prism-examples/pta/zeroconf/time.pctl
index 40759e49..405ecfc6 100644
--- a/prism-examples/pta/zeroconf/time.pctl
+++ b/prism-examples/pta/zeroconf/time.pctl
@@ -1,3 +1,3 @@
 // Maximum expected time to elect a leader
-R{"time"}min=? [ F "done" ]
+R{"time"}max=? [ F "done" ]