First version of support for named properties in GUI.

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

prism/src/userinterface/properties/GUIExperiment.java

@@ -106,12 +106,14 @@ public class GUIExperiment
 
 	public String getPropertyString()
 	{
-		return prop.getProperty(0).toString();
+		int i = prop.getNumProperties() - 1;
+		return prop.getProperty(i).toString();
 	}
 
 	public Type getPropertyType()
 	{
-		return prop.getProperty(0).getType();
+		int i = prop.getNumProperties() - 1;
+		return prop.getProperty(i).getType();
 	}
 
 	public ResultsCollection getResults()
@@ -217,7 +219,8 @@ public class GUIExperiment
 			Model model = null;
 
 			ModulesFile modulesFileToCheck;
-			Expression propertyToCheck = propertiesFile.getProperty(0);
+			int propertyIndex = propertiesFile.getNumProperties() - 1;
+			Expression propertyToCheck = propertiesFile.getProperty(propertyIndex);
 			SimulationInformation info = null;
 			boolean reuseInfo = false, reuseInfoAsked = false;
 

prism/src/userinterface/properties/GUIMultiProperties.java

@@ -202,7 +202,7 @@ public class GUIMultiProperties extends GUIPlugin implements MouseListener, List
 
 		try {
 			// Get valid/selected properties
-			String propertiesString = getLabelsString() + "\n" + getConstantsString() + "\n" + propList.getValidSelectedString();
+			String propertiesString = getLabelsString() + "\n" + getConstantsString() + "\n" + propList.getValidSelectedAndReferencedString();
 			// Get PropertiesFile for valid/selected properties
 			parsedProperties = getPrism().parsePropertiesString(parsedModel, propertiesString);
 			// And get list of corresponding GUIProperty objects
@@ -257,7 +257,7 @@ public class GUIMultiProperties extends GUIPlugin implements MouseListener, List
 		UndefinedConstants uCon;
 		try {
 			parsedProperties = getPrism().parsePropertiesString(parsedModel,
-					getLabelsString() + "\n" + getConstantsString() + "\n" + propList.getValidSelectedString());
+					getLabelsString() + "\n" + getConstantsString() + "\n" + propList.getValidSelectedAndReferencedString());
 			validGUIProperties = propList.getValidSelectedProperties();
 			if (validGUIProperties.size() == 0) {
 				error("None of the selected properties are suitable for simulation");
@@ -340,26 +340,42 @@ public class GUIMultiProperties extends GUIPlugin implements MouseListener, List
 		Type type;
 
 		try {
+			//get referenced named properties
+			String namedString = "";
+			//Add named properties
+			for (GUIProperty namedProp : this.propList.getAllNamedProperties()) {
+				if (gp.getReferencedNames().contains(namedProp.getName())) {
+					namedString += "\"" + namedProp.getName() + "\" : " + namedProp.getPropString() + "\n";
+				}
+			}
+			
 			// parse property to be used for experiment
-			parsedProperties = getPrism().parsePropertiesString(parsedModel, getLabelsString() + "\n" + getConstantsString() + "\n" + gp.getPropString());
+			parsedProperties = getPrism().parsePropertiesString(parsedModel, getLabelsString() + "\n" + getConstantsString() + "\n" + namedString + gp.getPropString());
 			if (parsedProperties.getNumProperties() <= 0) {
 				error("There are no properties selected");
 				return;
 			}
-			if (parsedProperties.getNumProperties() > 1) {
+			if (propList.getNumSelectedProperties() > 1) {
 				error("Experiments can only be created for a single property");
 				return;
 			}
 
 			// check the type of the property
-			type = parsedProperties.getProperty(0).getType();
+			int index = parsedProperties.getNumProperties() - 1;
+			type = parsedProperties.getProperty(index).getType();
 		} catch (PrismException e) {
 			error(e.getMessage());
 			return;
 		}
 
+		//get Property objects for sorting out undefined constants
+		ArrayList<Property> props = new ArrayList<Property>();
+		for (int i = 0; i < parsedProperties.getNumProperties(); i++) {
+			props.add(parsedProperties.getPropertyObject(i));
+		}
+		
 		// sort out undefined constants
-		UndefinedConstants uCon = new UndefinedConstants(parsedModel, parsedProperties, parsedProperties.getPropertyObject(0));
+		UndefinedConstants uCon = new UndefinedConstants(parsedModel, parsedProperties, props);
 		boolean showGraphDialog = false;
 		boolean useSimulation = false;
 		if (uCon.getMFNumUndefined() + uCon.getPFNumUndefined() == 0) {
@@ -455,7 +471,18 @@ public class GUIMultiProperties extends GUIPlugin implements MouseListener, List
 			GUIProperty gp = propList.getProperty(index);
 			gp.setBeingEdited(false);
 			if (pctl != null) {
-				gp.setPropString(pctl, parsedModel, getConstantsString(), getLabelsString());
+				if (pctl.matches("\"[^\"]*\"[ ]*:.*")) {
+					//the string contains property name
+					int start = pctl.indexOf('"') + 1;
+					int end = pctl.indexOf('"', start);
+					String name = pctl.substring(start,end);
+					int colon = pctl.indexOf(':') + 1;
+					pctl = pctl.substring(colon).trim();
+					gp.setPropStringAndName(pctl, name, parsedModel, getConstantsString(), getLabelsString());
+				} else {
+					gp.setPropStringAndName(pctl, null, parsedModel, getConstantsString(), getLabelsString());
+				}
+				
 				gp.setComment(comment);
 				setModified(true);
 			}
@@ -825,7 +852,7 @@ public class GUIMultiProperties extends GUIPlugin implements MouseListener, List
 					ArrayList listOfProperties = gcp.getProperties();
 					for (int i = 0; i < listOfProperties.size(); i++) {
 						GUIProperty property = (GUIProperty) listOfProperties.get(i);
-						propList.addProperty(property.getPropString(), property.getComment());
+						propList.addProperty(property.getName(), property.getPropString(), property.getComment());
 						setModified(true);
 					}
 				} catch (UnsupportedFlavorException e) {

prism/src/userinterface/properties/GUIPropertiesList.java

@@ -29,6 +29,7 @@ package userinterface.properties;
 
 import java.io.*;
 import java.util.*;
+import java.util.List;
 import java.awt.*;
 import java.awt.event.*;
 import javax.swing.*;
@@ -96,6 +97,35 @@ public class GUIPropertiesList extends JList implements KeyListener
 		return (GUIProperty) listModel.getElementAt(i);
 	}
 	
+	/**
+	 * Returns all properties in this list that have
+	 * non-null name.
+	 */
+	public List<GUIProperty> getAllNamedProperties() {
+		ArrayList<GUIProperty> ret = new ArrayList<GUIProperty>();
+		for (int i = 0; i < getNumProperties(); i++) {
+			if (getProperty(i).getName() != null)
+				ret.add(getProperty(i));
+		}
+		
+		return ret;
+	}
+	
+	/**
+	 * Looks up a property with the specified name and returns it. If
+	 * such a property does not exist, returns null;
+	 */
+	public GUIProperty getPropertyByName(String s) {
+		for (int i = 0; i < getNumProperties(); i++) {
+			GUIProperty p = getProperty(i);
+			if (p.getName() != null && p.getName().equals(s)) {
+				return p;
+			}
+		}
+		
+		return null;
+	}
+
 	/**
 	 * Check that all properties in the list are valid.
 	 */
@@ -164,16 +194,58 @@ public class GUIPropertiesList extends JList implements KeyListener
 	}
 
 	/**
-	 * Get a string comprising concatenation of all valid properties currently selected in the list.
+	 * Get a string comprising concatenation of all valid properties currently selected in the list
+	 * together with all properties these reference (even indirectly). The properties which are not
+	 * selected, but referenced, are guarranteed to be first in the string.
 	 */
-	public String getValidSelectedString()
+	public String getValidSelectedAndReferencedString()
 	{
 		String str = "";
 		ArrayList<GUIProperty> gps = getValidSelectedProperties();
+		
+		//strings will contain all relevant named properties, first selected, then refernced
+		Vector<String> strings = new Vector<String>(); 
+		
+		for (GUIProperty p : gps) { 
+			//add even null
+			strings.add(p.getName());
+		}
+		
+		for (GUIProperty p : gps) { 
+			for (String s : p.getReferencedNames())
+				if (!strings.contains(s))
+					strings.add(s);
+		}
+		
+		Vector<GUIProperty> referencedProps = new Vector<GUIProperty>();
+
+		//turn referenced strings to props.
+		int i = gps.size();
+		while (i < strings.size()) {
+			GUIProperty p = getPropertyByName(strings.get(i));
+			if (p != null) {
+				referencedProps.add(p);
+				for (String s : p.getReferencedNames())
+					if (!strings.contains(s))
+						strings.add(s);
+			} //we don't need to care about null case, parser will find an error later.
+			i++;
+		}
+		
+		//add all named properties
+		String namedString = "";
+		//Add named properties
+		for (GUIProperty p : referencedProps) {
+				namedString += "\"" + p.getName() + "\" : " + p.getPropString() + "\n";
+		}
+		
 		for (GUIProperty gp : gps) {
+			if (gp.getName() != null) {
+				str += "\"" + gp.getName() + "\" : ";
+			}
 			str += gp.getPropString() + "\n";
 		}
-		return str;
+		return namedString + str;
 	}
 
 	/**
@@ -238,21 +310,36 @@ public class GUIPropertiesList extends JList implements KeyListener
 	}
 
 	/* UPDATE METHODS */
-
 	public void addProperty(String propString, String comment)
+	{
+		if (propString.matches("\"[^\"]*\"[ ]*:.*")) {
+			//the string contains property name
+			int start = propString.indexOf('"') + 1;
+			int end = propString.indexOf('"', start);
+			String name = propString.substring(start,end);
+			int colon = propString.indexOf(':') + 1;
+			String actualPropString = propString.substring(colon).trim();
+			
+			addProperty(name, actualPropString, comment);
+		} else {
+			addProperty(null, propString, comment);
+		}
+	}
+
+	public void addProperty(String name, String propString, String comment)
 	{
 		counter++;
-		GUIProperty gp = new GUIProperty(prism, "PROPERTY" + counter, propString, comment);
-		gp.parse(parent.getParsedModel(), parent.getConstantsString(), parent.getLabelsString());
+		GUIProperty gp = new GUIProperty(prism, this, "PROPERTY" + counter, propString, name, comment);
 		listModel.addElement(gp);
+		validateProperties();
 	}
 
-	public void setProperty(int index, String propString, String comment)
+	public void setProperty(int index, String name, String propString, String comment)
 	{
 		counter++;
-		GUIProperty gp = new GUIProperty(prism, "PROPERTY" + counter, propString, comment);
-		gp.parse(parent.getParsedModel(), parent.getConstantsString(), parent.getLabelsString());
+		GUIProperty gp = new GUIProperty(prism, this, "PROPERTY" + counter, propString, name, comment);
 		listModel.setElementAt(gp, index);
+		validateProperties();
 	}
 
 	/** Used for pasting */
@@ -271,9 +358,10 @@ public class GUIPropertiesList extends JList implements KeyListener
 	public void addPropertiesFile(PropertiesFile pf)
 	{
 		for (int i = 0; i < pf.getNumProperties(); i++) {
+			String nam = pf.getPropertyName(i);
 			String str = pf.getProperty(i).toString();
 			String com = pf.getPropertyComment(i);
-			addProperty(str, com);
+			addProperty(nam, str, com);
 		}
 	}
 
@@ -282,6 +370,7 @@ public class GUIPropertiesList extends JList implements KeyListener
 		GUIProperty gp = getProperty(index);
 		if (!gp.isBeingEdited()) {
 			listModel.removeElementAt(index);
+			validateProperties();
 			return true;
 		} else
 			return false;
@@ -325,10 +414,28 @@ public class GUIPropertiesList extends JList implements KeyListener
 
 	public void validateProperties()
 	{
+		List<GUIProperty> list = new ArrayList<GUIProperty>();
 		for (int i = 0; i < getNumProperties(); i++) {
 			GUIProperty p = getProperty(i);
+			p.makeInvalid();
+			list.add(p);
+		}
+		
+		boolean changed;
+		do {
+			changed = false;
+			int i = 0;
+			while (i < list.size()) {
+				GUIProperty p = list.get(i);
 				p.parse(parent.getParsedModel(), parent.getConstantsString(), parent.getLabelsString());
+				if (p.isValid()) {
+					list.remove(i);
+					changed = true;
+				} else {
+					i++;
+				}
 			}
+		} while (changed && list.size() > 0);
 		// Force repaint because we modified a GUIProperty directly
 		repaint();
 	}
@@ -415,7 +522,7 @@ public class GUIPropertiesList extends JList implements KeyListener
 			toolTip = p.getToolTipText();
 
 			// text
-			setText(p.getPropString());
+			setText(p.toString());
 
 			// icon
 			setIcon(p.getImage());

prism/src/userinterface/properties/GUIProperty.java

@@ -28,11 +28,15 @@
 
 package userinterface.properties;
 
+import java.util.Vector;
+
 import javax.swing.*;
 
 import userinterface.GUIPrism;
 import parser.*;
 import parser.ast.*;
+import parser.visitor.FindAllProps;
+import parser.visitor.GetAllReferencedProperties;
 import prism.*;
 
 /**
@@ -91,11 +95,16 @@ public class GUIProperty
 
 	private String method; // Method used (verification, simulation)
 	private String constantsString; // Constant values used
+	private String name;
+	private Vector<String> referencedNames;
+	
+	private GUIPropertiesList propList; // to be able to get named properties
 
 	/** Creates a new instance of GUIProperty */
-	public GUIProperty(Prism prism, String id, String propString, String comment)
+	public GUIProperty(Prism prism, GUIPropertiesList propList, String id, String propString, String name, String comment)
 	{
 		this.prism = prism;
+		this.propList = propList;
 		
 		this.id = id;
 		status = STATUS_NOT_DONE;
@@ -105,6 +114,7 @@ public class GUIProperty
 		this.propString = propString;
 		expr = null;
 		this.comment = comment;
+		this.name = name;
 
 		result = null;
 		parseError = "";
@@ -156,6 +166,27 @@ public class GUIProperty
 		return propString;
 	}
 	
+	/**
+	 * Returns the name of this property, or {@code null} if the property
+	 * has no name.
+	 */
+	public String getName()
+	{
+		return this.name;
+	}
+	
+	/**
+	 * If the property is valid (see {@link #isValid()}), returns a
+	 * (potentialy empty) vector containing names of properties
+	 * this property references.
+	 * <p/>
+	 * If the property is not valid, returns {@code null}.
+	 */
+	public Vector<String> getReferencedNames()
+	{
+		return this.referencedNames;
+	}
+
 	public Expression getProperty()
 	{
 		return expr;
@@ -174,6 +205,16 @@ public class GUIProperty
 		return expr != null;
 	}
 
+	/**
+	 * Forgets the validity state of the property, i.e. {@link #isValid()} will
+	 * be returning {@code false} until property is parsed OK again.
+	 * @return
+	 */
+	public void makeInvalid() {
+		this.expr = null;
+		this.referencedNames = null;
+	}
+	
 	/**
 	 * Is this property both valid (i.e. parsed OK last time it was checked)
 	 * and suitable approximate verification through simulation?
@@ -232,7 +273,7 @@ public class GUIProperty
 
 	public String toString()
 	{
-		return propString;
+		return ((this.name != null) ? ("\"" + this.name + "\" : ") : "") + propString;
 	}
 
 	//UPDATE METHODS
@@ -247,11 +288,12 @@ public class GUIProperty
 		doingImage = image;
 	}
 
-	public void setPropString(String propString, ModulesFile m, String constantsString, String labelString)
+	public void setPropStringAndName(String propString, String name, ModulesFile m, String constantsString, String labelString)
 	{
 		this.propString = propString;
+		this.name = name;
 		setStatus(STATUS_NOT_DONE);
-		parse(m, constantsString, labelString);
+		propList.validateProperties();
 	}
 
 	public void setComment(String comment)
@@ -327,14 +369,27 @@ public class GUIProperty
 			} catch (PrismException e) {
 				couldBeNoConstantsOrLabels = true;
 			}
+			
+			String namedString = "";
+			int namedCount = 0;
+			//Add named properties
+			for (GUIProperty namedProp : this.propList.getAllNamedProperties()) {
+				
+				if (namedProp.isValid() &&
+						(this.name == null || !this.name.equals(namedProp.getName()))) {
+					namedCount++;
+					namedString += "\"" + namedProp.getName() + "\" : " + namedProp.getPropString() + "\n";
+				}
+			}
+			
 			//Parse all together
-			String withConsLabs = constantsString + "\n" + labelString + "\n" + propString;
+			String withConsLabs = constantsString + "\n" + labelString + "\n" + namedString + propString;
 			PropertiesFile ff = prism.parsePropertiesString(m, withConsLabs);
 			
 			//Validation of number of properties
-			if (ff.getNumProperties() == 0)
+			if (ff.getNumProperties() <= namedCount)
 				throw new PrismException("Empty Property");
-			else if (ff.getNumProperties() > 1)
+			else if (ff.getNumProperties() > namedCount + 1)
 				throw new PrismException("Contains Multiple Properties");
 
 			//Validation of constants and labels
@@ -350,16 +405,37 @@ public class GUIProperty
 					throw new PrismException("Contains labels");
 			}
 			//Now set the property
-			expr = ff.getProperty(0);
+			expr = ff.getProperty(namedCount);
 			parseError = "(Unexpected) no error!";
 			// if status was previously a parse error, reset status.
 			// otherwise, don't set status - reparse doesn't mean existing results should be lost
 			if (getStatus() == STATUS_PARSE_ERROR)
 				setStatus(STATUS_NOT_DONE);
+			
+			//get the referenced names
+			this.referencedNames = new Vector<String>();
+			(new GetAllReferencedProperties(this.referencedNames, m, ff)).visit(ff.getPropertyObject(namedCount));
+			
 		} catch (PrismException ex) {
-			expr = null;
+			this.expr = null;
+			this.referencedNames = null;
 			setStatus(STATUS_PARSE_ERROR);
 			parseError = ex.getMessage();
 		}
 	}
+	
+	@Override
+	public int hashCode()
+	{
+		return (this.propString != null) ? this.propString.length() : 0;
+	}
+	
+	@Override
+	public boolean equals(Object obj)
+	{
+		if (!(obj instanceof GUIProperty))
+			return false;
+		
+		return this.id.equals(((GUIProperty) obj).id);
+	}
 }

prism/src/userinterface/properties/GUIPropertyEditor.java

@@ -91,7 +91,10 @@ public class GUIPropertyEditor extends javax.swing.JDialog implements ActionList
 		else
 		{
 			this.id = prop.getID();
-			propertyText.setText(prop.getPropString());
+			
+			String namePart = (prop.getName() != null) ? ("\"" + prop.getName() + "\" : ") : "";
+			
+			propertyText.setText(namePart + prop.getPropString());
 			commentTextArea.setText(prop.getComment());
 		}
 		addActionListeners();
@@ -802,13 +805,23 @@ public class GUIPropertyEditor extends javax.swing.JDialog implements ActionList
 			noConstants = fConLab.getConstantList().size();
 			noLabels = fConLab.getLabelList().size();
 			
+			String namedString = "";
+			int namedCount = 0;
+			//Add named properties
+			for (GUIProperty namedProp : this.props.getPropList().getAllNamedProperties()) {
+				if (namedProp.isValid() && this.id != null && !this.id.equals(namedProp.getID())) {
+					namedCount++;
+					namedString += "\"" + namedProp.getName() + "\" : " + namedProp.getPropString() + "\n";
+				}
+			}
+			
 			//Parse all together
-			String withConsLabs = props.getConstantsString()+"\n"+props.getLabelsString()+"\n"+propertyText.getText();
+			String withConsLabs = props.getConstantsString()+"\n"+props.getLabelsString()+namedString+propertyText.getText();
 			PropertiesFile ff = props.getPrism().parsePropertiesString(parsedModel, withConsLabs);
 			
 			//Validation of number of properties
-			if(ff.getNumProperties() == 0) throw new PrismException("Empty property");
-			else if(ff.getNumProperties() > 1) throw new PrismException("Contains multiple properties");
+			if(ff.getNumProperties() <= namedCount) throw new PrismException("Empty property");
+			else if(ff.getNumProperties() > namedCount + 1) throw new PrismException("Contains multiple properties");
 			
 			//Validation of constants and labels
 			if(ff.getConstantList().size() != noConstants) throw new PrismException("Contains constants");

prism/src/userinterface/properties/computation/ModelCheckThread.java

@@ -114,11 +114,14 @@ public class ModelCheckThread extends GUIComputationThread
 
 		IconThread ic = new IconThread(null);
 
+		//numAuxiliary is the number of properties we don't check but that are contained because
+		//they are referenced. These are at the beginning of the file.
+		int numAuxiliary = propertiesFile.getNumProperties() - guiProps.size();
 		// Work through list of properties
-		for (int i = 0; i < propertiesFile.getNumProperties(); i++) {
+		for (int i = numAuxiliary; i < propertiesFile.getNumProperties(); i++) {
 
 			// Get ith property
-			GUIProperty gp = guiProps.get(i);
+			GUIProperty gp = guiProps.get(i - numAuxiliary);
 			// Animate it's clock icon
 			ic = new IconThread(gp);
 			ic.start();

prism/src/userinterface/properties/computation/SimulateModelCheckThread.java

@@ -120,7 +120,7 @@ public class SimulateModelCheckThread extends GUIComputationThread
 					logln(": " + properties.get(0));
 				} else {
 					logln(" " + pf.getNumProperties() + " properties:");
-					for (int i = 0; i < pf.getNumProperties(); i++) {
+					for (int i = 0; i < properties.size(); i++) {
 						logln(" " + properties.get(i));
 					}
 				}