From 786849d5232beb527547ca9046a2f663d5fe2912 Mon Sep 17 00:00:00 2001 From: Vojtech Forejt Date: Sat, 22 Oct 2011 00:39:43 +0000 Subject: [PATCH] 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 --- .../properties/GUIExperiment.java | 9 +- .../properties/GUIMultiProperties.java | 43 ++++-- .../properties/GUIPropertiesList.java | 131 ++++++++++++++++-- .../userinterface/properties/GUIProperty.java | 98 +++++++++++-- .../properties/GUIPropertyEditor.java | 21 ++- .../computation/ModelCheckThread.java | 7 +- .../computation/SimulateModelCheckThread.java | 2 +- 7 files changed, 270 insertions(+), 41 deletions(-) diff --git a/prism/src/userinterface/properties/GUIExperiment.java b/prism/src/userinterface/properties/GUIExperiment.java index f61b8201..91380bbb 100644 --- a/prism/src/userinterface/properties/GUIExperiment.java +++ b/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; diff --git a/prism/src/userinterface/properties/GUIMultiProperties.java b/prism/src/userinterface/properties/GUIMultiProperties.java index 5aaaacc5..29999e12 100644 --- a/prism/src/userinterface/properties/GUIMultiProperties.java +++ b/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 props = new ArrayList(); + 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) { diff --git a/prism/src/userinterface/properties/GUIPropertiesList.java b/prism/src/userinterface/properties/GUIPropertiesList.java index 1e0275de..22f2482d 100644 --- a/prism/src/userinterface/properties/GUIPropertiesList.java +++ b/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.*; @@ -95,6 +96,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 getAllNamedProperties() { + ArrayList ret = new ArrayList(); + 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 gps = getValidSelectedProperties(); + + //strings will contain all relevant named properties, first selected, then refernced + Vector strings = new Vector(); + + 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 referencedProps = new Vector(); + + //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 list = new ArrayList(); for (int i = 0; i < getNumProperties(); i++) { GUIProperty p = getProperty(i); - p.parse(parent.getParsedModel(), parent.getConstantsString(), parent.getLabelsString()); + 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()); diff --git a/prism/src/userinterface/properties/GUIProperty.java b/prism/src/userinterface/properties/GUIProperty.java index 1b38fb63..e265c3ad 100644 --- a/prism/src/userinterface/properties/GUIProperty.java +++ b/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,12 +95,17 @@ public class GUIProperty private String method; // Method used (verification, simulation) private String constantsString; // Constant values used + private String name; + private Vector 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; doingImage = IMAGE_DOING; @@ -105,6 +114,7 @@ public class GUIProperty this.propString = propString; expr = null; this.comment = comment; + this.name = name; result = null; parseError = ""; @@ -155,6 +165,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. + *

+ * If the property is not valid, returns {@code null}. + */ + public Vector getReferencedNames() + { + return this.referencedNames; + } public Expression getProperty() { @@ -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(); + (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); + } } diff --git a/prism/src/userinterface/properties/GUIPropertyEditor.java b/prism/src/userinterface/properties/GUIPropertyEditor.java index 926ab0e4..f2afd59d 100644 --- a/prism/src/userinterface/properties/GUIPropertyEditor.java +++ b/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"); diff --git a/prism/src/userinterface/properties/computation/ModelCheckThread.java b/prism/src/userinterface/properties/computation/ModelCheckThread.java index 17024190..3a8e6f2d 100644 --- a/prism/src/userinterface/properties/computation/ModelCheckThread.java +++ b/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(); diff --git a/prism/src/userinterface/properties/computation/SimulateModelCheckThread.java b/prism/src/userinterface/properties/computation/SimulateModelCheckThread.java index 59e14df6..298aaba1 100644 --- a/prism/src/userinterface/properties/computation/SimulateModelCheckThread.java +++ b/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)); } }