diff --git a/prism/examples/pta/simple/auto b/prism/examples/pta/simple/auto
new file mode 100755
index 00000000..bad47d26
--- /dev/null
+++ b/prism/examples/pta/simple/auto
@@ -0,0 +1,3 @@
+#!/bin/csh
+
+prism formats09.nm formats09.pctl -prop 1 -aroptions refine=first
diff --git a/prism/examples/pta/simple/formats.nm b/prism/examples/pta/simple/formats09.nm
similarity index 72%
rename from prism/examples/pta/simple/formats.nm
rename to prism/examples/pta/simple/formats09.nm
index ce249ba3..2d5c1c55 100644
--- a/prism/examples/pta/simple/formats.nm
+++ b/prism/examples/pta/simple/formats09.nm
@@ -8,8 +8,7 @@ module M
 	x : clock;
 	y : clock;
 	
-	//[] s=0 -> 0.6 : (s'=1) + 0.4 : (s'=2)&(x'=0);
-	[] s=0 -> 0.3 : (s'=1) + 0.3 : (s'=1) + 0.2 : (s'=2)&(x'=0) + 0.2 : (s'=2)&(x'=0);
+	[] s=0 -> 0.6 : (s'=1) + 0.4 : (s'=2)&(x'=0);
 	[] s=1 & x=0 -> (s'=3);
 	[] s=1 & y>2 -> (s'=1)&(y'=0);
 	[] s=2 & x=0 & y=1 -> (s'=3)&(y'=0);
diff --git a/prism/examples/pta/simple/formats09.pctl b/prism/examples/pta/simple/formats09.pctl
new file mode 100644
index 00000000..bc96bfc5
--- /dev/null
+++ b/prism/examples/pta/simple/formats09.pctl
@@ -0,0 +1,3 @@
+Pmax=? [ F "target" ]
+
+// Rmin=? [ F "end" ]