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" ]