Better testing for nesting in PTA digital clocks (+ test cases).

prism-tests/functionality/verify/ptas/notallowed/digital-nested.nm

@@ -0,0 +1,25 @@
+// Example showing that digital clocks can't do nested properties, from:
+// Marta Kwiatkowska, Gethin Norman, David Parker and Jeremy Sproston.
+// Performance Analysis of Probabilistic Timed Automata using Digital Clocks.
+// Formal Methods in System Design, 29, pages 33-78, Springer. August 2006.
+// (Fig 4, p.33)
+
+// The example is not actually used, since none of the implemented methods
+// can check nested properties
+
+pta
+
+module M
+
+	l : [0..1];
+	x : clock;
+
+	invariant
+	(l=0 => (x>=0 & x<=3)) &
+	(l=2 => true)
+	endinvariant
+
+	[]  l=0 & x>=3 -> (l'=1);
+	[]  l=0 & x<=3 -> (l'=1);
+	
+endmodule

prism-tests/functionality/verify/ptas/notallowed/digital-nested.nm.props

@@ -0,0 +1,20 @@
+// RESULT: Error:nested
+//P<1 [ F P<1 [ F<=1 l=1 ] ];
+
+// RESULT: Error:nested
+P<1 [ F P<1 [ F l=1 ] ];
+
+// RESULT: Error:nested
+P<1 [ F R<1 [ F l=1 ] ];
+
+// RESULT: Error:nested
+R<1 [ F P<1 [ F l=1 ] ];
+
+// RESULT: Error:nested
+R<1 [ F R<1 [ F l=1 ] ];
+
+// RESULT: false
+"inner": P<1 [ F l=1 ];
+
+// RESULT: Error:nested
+Pmax=? [ F "inner" ];

prism-tests/functionality/verify/ptas/notallowed/digital-nested.nm.props.args

@@ -0,0 +1 @@
+-ptamethod digital

prism/src/pta/DigitalClocks.java

@@ -350,7 +350,7 @@ public class DigitalClocks
 		}
 
 		// Check that there are no nested probabilistic operators
-		if (propertyToCheck.computeProbNesting() > 1) {
+		if (propertyToCheck.computeProbNesting(propertiesFile) > 1) {
 			throw new PrismLangException("Nested P/R operators are not allowed when using the digital clocks method", propertyToCheck);
 		}