Some tidying of PTA examples.

git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@1691 bbc10eb1-c90d-0410-af57-cb519fbb1720

prism/examples/pta/simple/auto

@@ -0,0 +1,3 @@
+#!/bin/csh
+
+prism formats09.nm formats09.pctl -prop 1 -aroptions refine=first

prism/examples/pta/simple/formats.nm → 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);

prism/examples/pta/simple/formats09.pctl

@@ -0,0 +1,3 @@
+Pmax=? [ F "target" ]
+
+// Rmin=? [ F "end" ]