diff --git a/prism/examples/pta/csma/abst/deadline.pctl b/prism/examples/pta/csma/abst/deadline.pctl
index 2e10fffc..02149594 100644
--- a/prism/examples/pta/csma/abst/deadline.pctl
+++ b/prism/examples/pta/csma/abst/deadline.pctl
@@ -1,3 +1,3 @@
-const int T;
-
-Pmin=? [ F<=T "done" ]
+const int T;
+
+Pmin=? [ F<=T "done" ]
diff --git a/prism/examples/pta/csma/abst/eventually.pctl b/prism/examples/pta/csma/abst/eventually.pctl
index 686401e4..454ac18e 100644
--- a/prism/examples/pta/csma/abst/eventually.pctl
+++ b/prism/examples/pta/csma/abst/eventually.pctl
@@ -1,2 +1,2 @@
-Pmin=? [ F "done" ]
-
+Pmin=? [ F "done" ]
+
diff --git a/prism/examples/pta/csma/full/collisions.pctl b/prism/examples/pta/csma/full/collisions.pctl
index c0f7725a..9db83bc8 100644
--- a/prism/examples/pta/csma/full/collisions.pctl
+++ b/prism/examples/pta/csma/full/collisions.pctl
@@ -1 +1 @@
-Pmax=?[F "cmax" ]
+Pmax=?[F "cmax" ]
diff --git a/prism/examples/pta/csma/full/eventually.pctl b/prism/examples/pta/csma/full/eventually.pctl
index 14f4b145..3092cbc4 100644
--- a/prism/examples/pta/csma/full/eventually.pctl
+++ b/prism/examples/pta/csma/full/eventually.pctl
@@ -1,5 +1,5 @@
-Pmin=?[ F "s1_done"]
-Pmin=?[ F "s2_done"]
-Pmin=?[ F "done" ]
-Pmin=?[ F cd1=2 ]
-Pmax=?[ F cd1=2 ]
+Pmin=?[ F "s1_done"]
+Pmin=?[ F "s2_done"]
+Pmin=?[ F "done" ]
+Pmin=?[ F cd1=2 ]
+Pmax=?[ F cd1=2 ]
diff --git a/prism/examples/pta/csma/full/time.pctl b/prism/examples/pta/csma/full/time.pctl
index 8fb9f931..38cfc452 100644
--- a/prism/examples/pta/csma/full/time.pctl
+++ b/prism/examples/pta/csma/full/time.pctl
@@ -1,2 +1,2 @@
-R{"time"}min=? [ F "done" ]
-
+R{"time"}min=? [ F "done" ]
+
diff --git a/prism/examples/pta/firewire/abst/deadline-max.pctl b/prism/examples/pta/firewire/abst/deadline-max.pctl
index 9d089e3d..115754ec 100644
--- a/prism/examples/pta/firewire/abst/deadline-max.pctl
+++ b/prism/examples/pta/firewire/abst/deadline-max.pctl
@@ -1,3 +1,3 @@
-// Minimum probability that a leader has been elected by deadline T
-Pmax=? [ F "done_after" ]
-
+// Minimum 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 9c84acbc..70823f35 100644
--- a/prism/examples/pta/firewire/abst/deadline.pctl
+++ b/prism/examples/pta/firewire/abst/deadline.pctl
@@ -1,5 +1,5 @@
-const int T;
-
-// Minimum probability that a leader has been elected by deadline T
-Pmin=? [ F<=T "done" ]
-
+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 c173f95f..e43a1887 100644
--- a/prism/examples/pta/firewire/abst/eventually.pctl
+++ b/prism/examples/pta/firewire/abst/eventually.pctl
@@ -1,3 +1,3 @@
-// Minimum probability that a leader is eventually elected
-Pmin=? [ F "done" ]
-
+// 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 2c0f96c4..40759e49 100644
--- a/prism/examples/pta/firewire/abst/time.pctl
+++ b/prism/examples/pta/firewire/abst/time.pctl
@@ -1,3 +1,3 @@
-// Maximum expected time to elect a leader
-R{"time"}min=? [ F "done" ]
-
+// Maximum expected time to elect a leader
+R{"time"}min=? [ F "done" ]
+
diff --git a/prism/examples/pta/firewire/impl/deadline.pctl b/prism/examples/pta/firewire/impl/deadline.pctl
index 9c84acbc..70823f35 100644
--- a/prism/examples/pta/firewire/impl/deadline.pctl
+++ b/prism/examples/pta/firewire/impl/deadline.pctl
@@ -1,5 +1,5 @@
-const int T;
-
-// Minimum probability that a leader has been elected by deadline T
-Pmin=? [ F<=T "done" ]
-
+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 c173f95f..e43a1887 100644
--- a/prism/examples/pta/firewire/impl/eventually.pctl
+++ b/prism/examples/pta/firewire/impl/eventually.pctl
@@ -1,3 +1,3 @@
-// Minimum probability that a leader is eventually elected
-Pmin=? [ F "done" ]
-
+// Minimum probability that a leader is eventually elected
+Pmin=? [ F "done" ]
+
diff --git a/prism/examples/pta/firewire/impl/time.pctl b/prism/examples/pta/firewire/impl/time.pctl
index 2c0f96c4..40759e49 100644
--- a/prism/examples/pta/firewire/impl/time.pctl
+++ b/prism/examples/pta/firewire/impl/time.pctl
@@ -1,3 +1,3 @@
-// Maximum expected time to elect a leader
-R{"time"}min=? [ F "done" ]
-
+// Maximum expected time to elect a leader
+R{"time"}min=? [ F "done" ]
+
diff --git a/prism/examples/pta/repudiation/honest/deadline.pctl b/prism/examples/pta/repudiation/honest/deadline.pctl
index 7f4e3da4..93c25829 100644
--- a/prism/examples/pta/repudiation/honest/deadline.pctl
+++ b/prism/examples/pta/repudiation/honest/deadline.pctl
@@ -1,5 +1,5 @@
-const int T;
-
-// Minimum probability that protocol terminates successfully by the deadline
-Pmin=? [ F<T "terminated_successfully" ]
-
+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 3a1c1af5..0c37f266 100644
--- a/prism/examples/pta/repudiation/honest/eventually.pctl
+++ b/prism/examples/pta/repudiation/honest/eventually.pctl
@@ -1,4 +1,4 @@
-
-// Minimum probability that the protocol terminates successfully
-Pmin=? [ F "terminated_successfully" ]
-
+
+// Minimum probability that the protocol terminates successfully
+Pmin=? [ F "terminated_successfully" ]
+
diff --git a/prism/examples/pta/repudiation/malicious/deadline.pctl b/prism/examples/pta/repudiation/malicious/deadline.pctl
index ed146a64..8633995d 100644
--- a/prism/examples/pta/repudiation/malicious/deadline.pctl
+++ b/prism/examples/pta/repudiation/malicious/deadline.pctl
@@ -1,5 +1,5 @@
-const int T;
-
-// Maximum probability that malicious recepient gains information by deadline T
-Pmax=? [ F<T "gains_information" ]
-
+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 ce76a130..c001aa38 100644
--- a/prism/examples/pta/repudiation/malicious/eventually.pctl
+++ b/prism/examples/pta/repudiation/malicious/eventually.pctl
@@ -1,4 +1,4 @@
-
-// Maximum probability that malicious recepient gains information
-Pmax=? [ F "gains_information" ]
-
+
+// Maximum probability that malicious recepient gains information
+Pmax=? [ F "gains_information" ]
+
diff --git a/prism/examples/pta/simple/formats09.pctl b/prism/examples/pta/simple/formats09.pctl
index bc96bfc5..4e9c4643 100644
--- a/prism/examples/pta/simple/formats09.pctl
+++ b/prism/examples/pta/simple/formats09.pctl
@@ -1,3 +1,3 @@
-Pmax=? [ F "target" ]
-
-// Rmin=? [ F "end" ]
+Pmax=? [ F "target" ]
+
+// Rmin=? [ F "end" ]
diff --git a/prism/examples/pta/zeroconf/deadline.pctl b/prism/examples/pta/zeroconf/deadline.pctl
index 20ed7949..1ce8fbd9 100644
--- a/prism/examples/pta/zeroconf/deadline.pctl
+++ b/prism/examples/pta/zeroconf/deadline.pctl
@@ -1,5 +1,5 @@
-const int T;
-
-// Maximum probability of configuring incorrectly (using unfresh address) by time T
-Pmax=? [ F<=T "incorrect" ]
-
+const int T;
+
+// Maximum probability of configuring incorrectly (using unfresh address) by time T
+Pmax=? [ F<=T "incorrect" ]
+
diff --git a/prism/examples/pta/zeroconf/eventually.pctl b/prism/examples/pta/zeroconf/eventually.pctl
index 7a840397..6f4ff42f 100644
--- a/prism/examples/pta/zeroconf/eventually.pctl
+++ b/prism/examples/pta/zeroconf/eventually.pctl
@@ -1,3 +1,3 @@
-// Maximum probably use unfresh address
-Pmax=? [ F "done" ]
-
+// Maximum probably use unfresh address
+Pmax=? [ F "done" ]
+
diff --git a/prism/examples/pta/zeroconf/incorrect.pctl b/prism/examples/pta/zeroconf/incorrect.pctl
index 39917252..8d4affb7 100644
--- a/prism/examples/pta/zeroconf/incorrect.pctl
+++ b/prism/examples/pta/zeroconf/incorrect.pctl
@@ -1,3 +1,3 @@
-// Maximum probability of configuring incorrectly (using unfresh address)
-Pmax=? [ F "incorrect" ]
-
+// Maximum probability of configuring incorrectly (using unfresh address)
+Pmax=? [ F "incorrect" ]
+
diff --git a/prism/examples/pta/zeroconf/time.pctl b/prism/examples/pta/zeroconf/time.pctl
index 2c0f96c4..40759e49 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" ]
-
+// Maximum expected time to elect a leader
+R{"time"}min=? [ F "done" ]
+
diff --git a/prism/examples/pta/zeroconf/used.pctl b/prism/examples/pta/zeroconf/used.pctl
index 3cd422f0..a8f22c75 100644
--- a/prism/examples/pta/zeroconf/used.pctl
+++ b/prism/examples/pta/zeroconf/used.pctl
@@ -1 +1 @@
-P=?[ F s=2 & ip=2 ]
+P=?[ F s=2 & ip=2 ]
diff --git a/prism/examples/pta/zeroconf/zeroconf-full.pctl b/prism/examples/pta/zeroconf/zeroconf-full.pctl
index da9ac285..632d3c94 100644
--- a/prism/examples/pta/zeroconf/zeroconf-full.pctl
+++ b/prism/examples/pta/zeroconf/zeroconf-full.pctl
@@ -1,3 +1,3 @@
-Pmin=?[F "done"]
-Pmin=?[F "done_fresh"]
-Pmax=?[F "done_error"]
+Pmin=?[F "done"]
+Pmin=?[F "done_fresh"]
+Pmax=?[F "done_error"]