From 4f165146b1f1a901e868270c5dea42404655a1e5 Mon Sep 17 00:00:00 2001
From: Joachim Klein <klein@tcs.inf.tu-dresden.de>
Date: Thu, 30 Jun 2016 14:56:34 +0000
Subject: [PATCH] =?UTF-8?q?GUISimulator:=20reactivate=20the=20display=20of?=
 =?UTF-8?q?=20path=20formulae=20in=20the=20corresponding=20simulator=20tab?=
 =?UTF-8?q?=20[reported=20by=20Steffen=20M=C3=A4rcker]?=
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

Currently, properties that contain an undefined property constant are not displayed.
In the future it might be nice for the user to be asked to specify these constants,
preferably in an unobstrusive way, so that these path formulae can be displayed and
evaluated as well.


git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@11444 bbc10eb1-c90d-0410-af57-cb519fbb1720
---
 .../userinterface/simulator/GUISimulator.java | 48 +++++++++++++------
 1 file changed, 33 insertions(+), 15 deletions(-)

diff --git a/prism/src/userinterface/simulator/GUISimulator.java b/prism/src/userinterface/simulator/GUISimulator.java
index fa59531e..59a53c54 100644
--- a/prism/src/userinterface/simulator/GUISimulator.java
+++ b/prism/src/userinterface/simulator/GUISimulator.java
@@ -40,6 +40,7 @@ import java.awt.event.KeyEvent;
 import java.awt.event.MouseAdapter;
 import java.awt.event.MouseEvent;
 import java.awt.event.MouseListener;
+import java.util.Vector;
 
 import javax.swing.AbstractAction;
 import javax.swing.Action;
@@ -393,8 +394,9 @@ public class GUISimulator extends GUIPlugin implements MouseListener, ListSelect
 			}
 
 			// if necessary, get values for undefined constants from user
-			// (for now, just get contants needed for properties file labels)
-			// TODO: also get constants for any (path) props we need, when this is re-enabled
+			// (for now, just get constants needed for properties file labels)
+			// TODO: find a way to also get constants for any (path) props we need
+			//       (for path formulae display)
 			UndefinedConstants uCon = new UndefinedConstants(parsedModel, pf, true);
 			if (uCon.getMFNumUndefined() + uCon.getPFNumUndefined() > 0) {
 				int result = GUIConstantsPicker.defineConstantsWithDialog(getGUI(), uCon, lastConstants, lastPropertyConstants);
@@ -861,24 +863,40 @@ public class GUISimulator extends GUIPlugin implements MouseListener, ListSelect
 			}
 		}
 
-		// TODO: fix and re-enable this (note: should use passed in properties file)
-		// (and make sure user is queried for any necessary undefined constants too) 
-		// Path formulas
+		// Path formulae
+		// TODO: Currently, path formulae containing undefined property constants
+		// are ignored. It would be better if the user is queried
+		// for any necessary undefined constants, too.
 		GUISimPathFormulaeList thePathFormulaeList = (GUISimPathFormulaeList) pathFormulaeList;
 		thePathFormulaeList.clearList();
-		if (1 == 2)
-			if (pathActive) {
-				// Go through the property list from the Properties tab of GUI
-				GUIPropertiesList gpl = guiProp.getPropList();
-				for (int i = 0; i < gpl.getNumProperties(); i++) {
-					GUIProperty gp = gpl.getProperty(i);
-					// For properties which are simulate-able...
-					if (gp.isValidForSimulation()) {
-						// Add them to the list
-						thePathFormulaeList.addProperty(gp.getProperty(), propertiesFile);
+		if (pathActive) {
+			// Go through the property list from the Properties tab of GUI
+			GUIPropertiesList gpl = guiProp.getPropList();
+			for (int i = 0; i < gpl.getNumProperties(); i++) {
+				GUIProperty gp = gpl.getProperty(i);
+
+				// obtain constants in property
+				Vector<String> propertyConstants = gp.getProperty().getAllConstants();
+				boolean allConstantsDefined = true;
+				for (String propertyConstant : propertyConstants) {
+					if (!parsedModel.isDefinedConstant(propertyConstant) &&
+					    !propertiesFile.isDefinedConstant(propertyConstant)) {
+						// we found one that has not been defined in the model
+						// or the property file
+						allConstantsDefined = false;
+						break;
 					}
 				}
+
+				// If the property has no unresolved constants
+				// and is simulate-able...
+				if (allConstantsDefined &&
+				    gp.isValidForSimulation()) {
+					// Add them to the list
+					thePathFormulaeList.addProperty(gp.getProperty(), propertiesFile);
+				}
 			}
+		}
 	}
 
 	//METHODS TO IMPLEMENT THE GUIPLUGIN INTERFACE