diff --git a/examples/dtmc/crowds/crowds.pctl b/examples/dtmc/crowds/crowds.pctl
index a7c83e667..653da5713 100644
--- a/examples/dtmc/crowds/crowds.pctl
+++ b/examples/dtmc/crowds/crowds.pctl
@@ -1,3 +1,3 @@
-P=? [ F "observe0Greater1" ]
-P=? [ F "observeIGreater1" ]
-P=? [ F "observeOnlyTrueSender" ]
+P=? [ F observe0Greater1 ]
+P=? [ F observeIGreater1 ]
+P=? [ F observeOnlyTrueSender ]
diff --git a/examples/dtmc/die/die.pctl b/examples/dtmc/die/die.pctl
index b0eb88dcd..8deea6c43 100644
--- a/examples/dtmc/die/die.pctl
+++ b/examples/dtmc/die/die.pctl
@@ -1,4 +1,4 @@
-P=? [ F "one" ]
-P=? [ F "two" ]
-P=? [ F "three" ]
-R=? [ F "done" ]
+P=? [ F one ]
+P=? [ F two ]
+P=? [ F three ]
+R=? [ F done ]
diff --git a/examples/dtmc/synchronous_leader/leader.pctl b/examples/dtmc/synchronous_leader/leader.pctl
index e8b1899e6..b14536d80 100644
--- a/examples/dtmc/synchronous_leader/leader.pctl
+++ b/examples/dtmc/synchronous_leader/leader.pctl
@@ -1,3 +1,3 @@
-P=? [ F "elected" ]
-P=? [ F<=(4*(N+1)) "elected" ]
-R=? [ F "elected" ]
+P=? [ F elected ]
+P=? [ F<=(4*(N+1)) elected ]
+R=? [ F elected ]
diff --git a/examples/mdp/asynchronous_leader/leader.pctl b/examples/mdp/asynchronous_leader/leader.pctl
index 49e4dbeaa..bb8fb1b82 100644
--- a/examples/mdp/asynchronous_leader/leader.pctl
+++ b/examples/mdp/asynchronous_leader/leader.pctl
@@ -1,8 +1,8 @@
-Pmin=? [ F "elected" ]
+Pmin=? [ F elected ]
 
 const int K = 25;
-Pmin=? [ F<=K "elected" ]
-Pmax=? [ F<=K "elected" ]
+Pmin=? [ F<=K elected ]
+Pmax=? [ F<=K elected ]
 
-Rmin=? [ F "elected" ]
-Rmax=? [ F "elected" ]
+Rmin=? [ F elected ]
+Rmax=? [ F elected ]
diff --git a/examples/mdp/consensus/coin.pctl b/examples/mdp/consensus/coin.pctl
index 52a308559..aa371d50b 100644
--- a/examples/mdp/consensus/coin.pctl
+++ b/examples/mdp/consensus/coin.pctl
@@ -1,20 +1,20 @@
 // C1 (with probability 1, all N processes finish the protocol)
-Pmin=? [ F "finished" ]
+Pmin=? [ F finished ]
 
 // C2 (minimum probability that the protocol finishes with all coins equal to v) (v=1,2)
 // Results are same for v=1 and v=2 by symmetry
 // Analytic bound is (K-1)/(2*K)
-Pmin=? [ F "finished"&"all_coins_equal_0" ]
-Pmin=? [ F "finished"&"all_coins_equal_1" ]
+Pmin=? [ F finished & all_coins_equal_0 ]
+Pmin=? [ F finished & all_coins_equal_1 ]
 
 // Max probability of finishing protocol with coins not all equal
-Pmax=? [ F "finished"&!"agree" ]
+Pmax=? [ F finished & !agree ]
 
 // Min/max probability of finishing within k steps
-Pmin=? [ F<=k "finished" ]
-Pmax=? [ F<=k "finished" ]
+Pmin=? [ F<=k finished ]
+Pmax=? [ F<=k finished ]
 
 // Min/max expected steps to finish
-Rmin=? [ F "finished" ]
-Rmax=? [ F "finished" ]
+Rmin=? [ F finished ]
+Rmax=? [ F finished ]
 
diff --git a/examples/mdp/two_dice/two_dice.pctl b/examples/mdp/two_dice/two_dice.pctl
index 10cdff821..4ad376feb 100644
--- a/examples/mdp/two_dice/two_dice.pctl
+++ b/examples/mdp/two_dice/two_dice.pctl
@@ -1,13 +1,13 @@
-Pmin=? [ F "two" ]
-Pmax=? [ F "two" ]
-Pmin=? [ F "three" ]
-Pmax=? [ F "three" ]
-Pmin=? [ F "four" ]
-Pmax=? [ F "four" ]
-Pmin=? [ F "five" ]
-Pmax=? [ F "five" ]
-Pmin=? [ F "six" ]
-Pmax=? [ F "six" ]
+Pmin=? [ F two ]
+Pmax=? [ F two ]
+Pmin=? [ F three ]
+Pmax=? [ F three ]
+Pmin=? [ F four ]
+Pmax=? [ F four ]
+Pmin=? [ F five ]
+Pmax=? [ F five ]
+Pmin=? [ F six ]
+Pmax=? [ F six ]
 
-Rmin=? [ F "done" ]
-Rmax=? [ F "done" ]
+Rmin=? [ F done ]
+Rmax=? [ F done ]