From dd7223d0dc82f6fcf094fb5afd4a24cffb45d24c Mon Sep 17 00:00:00 2001
From: Dave Parker <dave.x.parker@gmail.com>
Date: Sun, 14 Jul 2019 01:05:17 +0100
Subject: [PATCH] Better testing for nesting in PTA digital clocks (+ test
 cases).

---
 .../verify/ptas/notallowed/digital-nested.nm  | 25 +++++++++++++++++++
 .../ptas/notallowed/digital-nested.nm.props   | 20 +++++++++++++++
 .../notallowed/digital-nested.nm.props.args   |  1 +
 prism/src/pta/DigitalClocks.java              |  2 +-
 4 files changed, 47 insertions(+), 1 deletion(-)
 create mode 100644 prism-tests/functionality/verify/ptas/notallowed/digital-nested.nm
 create mode 100644 prism-tests/functionality/verify/ptas/notallowed/digital-nested.nm.props
 create mode 100644 prism-tests/functionality/verify/ptas/notallowed/digital-nested.nm.props.args

diff --git a/prism-tests/functionality/verify/ptas/notallowed/digital-nested.nm b/prism-tests/functionality/verify/ptas/notallowed/digital-nested.nm
new file mode 100644
index 00000000..b0e556aa
--- /dev/null
+++ b/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
diff --git a/prism-tests/functionality/verify/ptas/notallowed/digital-nested.nm.props b/prism-tests/functionality/verify/ptas/notallowed/digital-nested.nm.props
new file mode 100644
index 00000000..98067edc
--- /dev/null
+++ b/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" ];
diff --git a/prism-tests/functionality/verify/ptas/notallowed/digital-nested.nm.props.args b/prism-tests/functionality/verify/ptas/notallowed/digital-nested.nm.props.args
new file mode 100644
index 00000000..a99b03e6
--- /dev/null
+++ b/prism-tests/functionality/verify/ptas/notallowed/digital-nested.nm.props.args
@@ -0,0 +1 @@
+-ptamethod digital
diff --git a/prism/src/pta/DigitalClocks.java b/prism/src/pta/DigitalClocks.java
index f3636f1f..5ff825d2 100644
--- a/prism/src/pta/DigitalClocks.java
+++ b/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);
 		}