From 5a3d94999b55754c136a3bdfd4393acc70e62c0a Mon Sep 17 00:00:00 2001
From: Dave Parker <dave.x.parker@gmail.com>
Date: Tue, 16 Jul 2019 00:22:35 +0100
Subject: [PATCH] Digital clocks: clock scaling searches properties/file for
 comparisons (+ test cases).

---
 .../verify/ptas/reach/propconst.nm.props      | 26 +++++++-
 prism/src/pta/DigitalClocks.java              | 61 +++++++++++++++----
 2 files changed, 75 insertions(+), 12 deletions(-)

diff --git a/prism-tests/functionality/verify/ptas/reach/propconst.nm.props b/prism-tests/functionality/verify/ptas/reach/propconst.nm.props
index 19444271..e0814217 100644
--- a/prism-tests/functionality/verify/ptas/reach/propconst.nm.props
+++ b/prism-tests/functionality/verify/ptas/reach/propconst.nm.props
@@ -1,12 +1,37 @@
 const int K = 2;
 const int L;
 
+label "x3" = x=3;
+
 // This tests clocks appearing in the property
 // (the use of digital clocks with -ex means that the expression
 //  is evaluated and all the types have to be correct)
 // RESULT: 1.0
 Pmax=? [ F x>=2 ];
 
+// This tests that property is traversed for clock scaling
+// (GCD should be 1 in this case)
+// RESULT: 1.0
+Pmax=? [ F x=3 ];
+
+// This also tests that property is traversed for clock scaling
+// (GCD is unaffected but clock max must be right to reach x=10)
+// RESULT: 1.0
+Pmax=? [ F x=10 ];
+
+// This tests that properties file labels are traversed for clock scaling
+// (GCD should be 1 in this case)
+// RESULT: 1.0
+Pmax=? [ F "x3" ];
+
+// This tests that property references are traversed for clock scaling
+// (GCD should be 1 in this case)
+// RESULT: 1.0
+Pmax=? [ F "p3" ];
+
+// RESULT: ?
+"p3":x=3;
+
 // This tests (defined) constants from the prop file
 // RESULT: 1.0
 Pmax=? [ F x>=K ];
@@ -14,4 +39,3 @@ Pmax=? [ F x>=K ];
 // This tests (undefined) constants from the prop file
 // RESULT: 1.0
 Pmax=? [ F x>=L ];
-
diff --git a/prism/src/pta/DigitalClocks.java b/prism/src/pta/DigitalClocks.java
index 291098da..4bf4f88f 100644
--- a/prism/src/pta/DigitalClocks.java
+++ b/prism/src/pta/DigitalClocks.java
@@ -157,9 +157,8 @@ public class DigitalClocks
 		}
 
 		// Extract information about clocks from the model
-		cci = new ComputeClockInformation();
-		modulesFile.accept(cci);
-		mainLog.println("Computed clock maximums: " + cci.clockMaxs);
+		cci = new ComputeClockInformation(modulesFile, propertiesFile, propertyToCheck);
+		mainLog.println("Computed clock maximums: " + cci.getClockMaxs());
 		if (doScaling) {
 			mainLog.println("Computed GCD: " + cci.getScaleFactor());
 		}
@@ -473,17 +472,31 @@ public class DigitalClocks
 	 */
 	class ComputeClockInformation extends ASTTraverse
 	{
+		// Model/property info
+		PropertiesFile propertiesFile = null;
+		LabelList labelList = null;
+		// Clock info
 		private Map<String, List<String>> clockLists;
 		private List<String> currentClockList;
 		private Map<String, Integer> clockMaxs;
 		private Set<Integer> allClockVals;
 		private int scaleFactor;
-
-		public ComputeClockInformation()
+		
+		public ComputeClockInformation(ModulesFile modulesFile, PropertiesFile propertiesFile, Expression propertyToCheck) throws PrismLangException
 		{
+			// Extract some info needed for traversal 
+			this.propertiesFile = propertiesFile;
+			labelList = (propertiesFile == null) ? null : propertiesFile.getLabelList();
+			// Set up storage
 			clockLists = new HashMap<String, List<String>>();
 			clockMaxs = new HashMap<String, Integer>();
 			allClockVals = new HashSet<Integer>();
+			// Traverse ModulesFile first (further storage created)
+			modulesFile.accept(this);
+			// Then property (but not whole property file, to maximise possible scaling)
+			propertyToCheck.accept(this);
+			// Finally, compute GCDs and scale factor
+			scaleFactor = computeGCD(allClockVals);
 		}
 
 		private void updateMax(String clock, int val)
@@ -505,6 +518,11 @@ public class DigitalClocks
 			return (i == null) ? -1 : i;
 		}
 
+		public Map<String, Integer> getClockMaxs()
+		{
+			return clockMaxs;
+		}
+
 		/**
 		 * Get the maximum value of a clock, scaled wrt. GCD (if required)
 		 * @param clock
@@ -545,12 +563,8 @@ public class DigitalClocks
 			return (y == 0) ? x : computeGCD(y, x % y);
 		}
 
-		public void visitPost(ModulesFile e) throws PrismLangException
-		{
-			// When have traversed the model, compute GCDs and scale factor
-			scaleFactor = computeGCD(allClockVals);
-		}
-
+		// AST traversal
+		
 		public void visitPre(parser.ast.Module e) throws PrismLangException
 		{
 			// Create new array to store clocks for this module
@@ -610,5 +624,30 @@ public class DigitalClocks
 				allClockVals.addAll(allVals);
 			}
 		}
+		
+		// Recurse on labels
+		public void visitPost(ExpressionLabel e) throws PrismLangException
+		{
+			if (labelList != null) {
+				int i = labelList.getLabelIndex(e.getName());
+				if (i != -1) {
+					labelList.getLabel(i).accept(this);
+				}
+			}
+		}
+		
+		// Recurse on property refs
+		public void visitPost(ExpressionProp e) throws PrismLangException
+		{
+			// If possible, look up property and recurse
+			if (propertiesFile != null) {
+				Property prop = propertiesFile.lookUpPropertyObjectByName(e.getName());
+				if (prop != null) {
+					prop.accept(this);
+				} else {
+					throw new PrismLangException("Unknown property reference " + e, e);
+				}
+			}
+		}
 	}
 }