diff --git a/prism/src/prism/Prism.java b/prism/src/prism/Prism.java index 6d41bf19..97504abf 100644 --- a/prism/src/prism/Prism.java +++ b/prism/src/prism/Prism.java @@ -1056,6 +1056,7 @@ public class Prism extends PrismComponent implements PrismSettingsListener /** * Get (exclusive) access to the PRISM parser. + * Not usually used externally - use the ready-made model/property parse methods instead. */ public static PrismParser getPrismParser() throws InterruptedException { @@ -1566,8 +1567,19 @@ public class Prism extends PrismComponent implements PrismSettingsListener } /** - * Parse a PRISM properties file. Typically, you need to pass in some info about the corresponding model - * (for access to constants, etc.). This is in the form of a ModelInfo object (e.g. a ModulesFile). If not required, this can be null. + * Parse a PRISM properties file, using the currently loaded model + * for context (i.e. definitions of variables, constants, labels, etc.). + * @param file File to read in + */ + public PropertiesFile parsePropertiesFile(File file) throws FileNotFoundException, PrismLangException + { + return parsePropertiesFile(currentModelInfo, file, true); + } + + /** + * Parse a PRISM properties file, using a specific ModelInfo object (e.g. ModulesFile) + * for context (i.e. definitions of variables, constants, labels, etc.). + * Usually, just use {@link #parsePropertiesFile(File)}, which uses the currently loaded model. * @param modelInfo Accompanying model info (null if not needed) * @param file File to read in */ @@ -1577,10 +1589,24 @@ public class Prism extends PrismComponent implements PrismSettingsListener } /** - * Parse a PRISM properties file. Typically, you need to pass in some info about the corresponding model - * (for access to constants, etc.). This is in the form of a ModelInfo object (e.g. a ModulesFile). If not required, this can be null. + * Parse a PRISM properties file, using the currently loaded model + * for context (i.e. definitions of variables, constants, labels, etc.). * You can also choose whether to do "tidy", i.e. post-parse checks and processing * (this must be done at some point but may want to postpone to allow parsing of files with errors). + * @param file File to read in + * @param tidy Whether or not to do "tidy" (post-parse checks and processing) + */ + public PropertiesFile parsePropertiesFile(File file, boolean tidy) throws FileNotFoundException, PrismLangException + { + return parsePropertiesFile(currentModelInfo, file, tidy); + } + + /** + * Parse a PRISM properties file, using a specific ModelInfo object (e.g. ModulesFile) + * for context (i.e. definitions of variables, constants, labels, etc.). + * You can also choose whether to do "tidy", i.e. post-parse checks and processing + * (this must be done at some point but may want to postpone to allow parsing of files with errors). + * Usually, just use {@link #parsePropertiesFile(File, boolean)}, which uses the currently loaded model. * @param modelInfo Accompanying model info (null if not needed) * @param file File to read in * @param tidy Whether or not to do "tidy" (post-parse checks and processing) @@ -1616,8 +1642,19 @@ public class Prism extends PrismComponent implements PrismSettingsListener } /** - * Parse a PRISM properties file form a string. Typically, you need to pass in some info about the corresponding model - * (for access to constants, etc.). This is in the form of a ModelInfo object (e.g. a ModulesFile). If not required, this can be null. + * Parse a PRISM properties file from a string, using the currently loaded model + * for context (i.e. definitions of variables, constants, labels, etc.). + * @param s String to parse + */ + public PropertiesFile parsePropertiesString(String s) throws PrismLangException + { + return parsePropertiesString(currentModelInfo, s); + } + + /** + * Parse a PRISM properties file from a string, using a specific ModelInfo object (e.g. ModulesFile) + * for context (i.e. definitions of variables, constants, labels, etc.). + * Usually, just use {@link #parsePropertiesString(String)}, which uses the currently loaded model. * @param modelInfo Accompanying model info (null if not needed) * @param s String to parse */ @@ -2139,7 +2176,7 @@ public class Prism extends PrismComponent implements PrismSettingsListener } /*// Create new model checker object and do model checking - PropertiesFile pf = parsePropertiesString(currentModelInfo, "filter(exists,!\"invariants\"); E[F!\"invariants\"]"); + PropertiesFile pf = parsePropertiesString("filter(exists,!\"invariants\"); E[F!\"invariants\"]"); if (!getExplicit()) { ModelChecker mc = new NondetModelChecker(this, currentModel, pf); if (((Boolean) mc.check(pf.getProperty(0)).getResult()).booleanValue()) { @@ -2871,7 +2908,7 @@ public class Prism extends PrismComponent implements PrismSettingsListener */ public Result modelCheck(String propertyString) throws PrismException { - PropertiesFile propertiesFile = parsePropertiesString(currentModelInfo, propertyString); + PropertiesFile propertiesFile = parsePropertiesString(propertyString); if (propertiesFile.getNumProperties() != 1) { throw new PrismException("There should be exactly one property to check (there are " + propertiesFile.getNumProperties() + ")"); } @@ -3794,7 +3831,7 @@ public class Prism extends PrismComponent implements PrismSettingsListener // Create a dummy properties file if none exist // (the symbolic model checkers rely on this to store e.g. model labels) if (propertiesFile == null) { - propertiesFile = parsePropertiesString(currentModelInfo, ""); + propertiesFile = parsePropertiesString(""); } // Create model checker StateModelChecker mc = StateModelChecker.createModelChecker(currentModelType, this, currentModel, propertiesFile); diff --git a/prism/src/prism/PrismCL.java b/prism/src/prism/PrismCL.java index d1c84bbc..f0644a12 100644 --- a/prism/src/prism/PrismCL.java +++ b/prism/src/prism/PrismCL.java @@ -591,10 +591,12 @@ public class PrismCL implements PrismModelListener if (importpepa) { mainLog.print("\nImporting PEPA file \"" + modelFilename + "\"...\n"); modulesFile = prism.importPepaFile(new File(modelFilename)); + prism.loadPRISMModel(modulesFile); } else if (importprismpp) { mainLog.print("\nImporting PRISM preprocessor file \"" + modelFilename + "\"...\n"); String prismppParamsList[] = ("? " + prismppParams).split(" "); modulesFile = prism.importPrismPreprocFile(new File(modelFilename), prismppParamsList); + prism.loadPRISMModel(modulesFile); } else if (importtrans) { mainLog.print("\nImporting model ("); mainLog.print(typeOverride == null ? "MDP" : typeOverride); @@ -616,6 +618,7 @@ public class PrismCL implements PrismModelListener } else { mainLog.print("\nParsing model file \"" + modelFilename + "\"...\n"); modulesFile = prism.parseModelFile(new File(modelFilename), typeOverride); + prism.loadPRISMModel(modulesFile); } } catch (FileNotFoundException e) { errorAndExit("File \"" + modelFilename + "\" not found"); @@ -629,11 +632,11 @@ public class PrismCL implements PrismModelListener // if properties file specified... if (propertiesFilename != null) { mainLog.print("\nParsing properties file \"" + propertiesFilename + "\"...\n"); - propertiesFile = prism.parsePropertiesFile(modulesFile, new File(propertiesFilename)); + propertiesFile = prism.parsePropertiesFile(new File(propertiesFilename)); } // if properties were given on command line... else if (!propertyString.equals("")) { - propertiesFile = prism.parsePropertiesString(modulesFile, propertyString); + propertiesFile = prism.parsePropertiesString(propertyString); } else { propertiesFile = null; } @@ -652,15 +655,6 @@ public class PrismCL implements PrismModelListener mainLog.println("(" + (i + 1) + ") " + propertiesFile.getPropertyObject(i)); } } - - // Load model into PRISM (if not done already) - try { - if (!importtrans) { - prism.loadPRISMModel(modulesFile); - } - } catch (PrismException e) { - errorAndExit(e.getMessage()); - } } /** @@ -972,6 +966,7 @@ public class PrismCL implements PrismModelListener modelType = prism.getModelType(); // Parse time specification, store as UndefinedConstant for constant T + // (NB: use "null" for model to avoid a potential name clash with T) String timeType = modelType.continuousTime() ? "double" : "int"; UndefinedConstants ucTransient = new UndefinedConstants(null, prism.parsePropertiesString(null, "const " + timeType + " T; T;")); try { diff --git a/prism/src/prism/PrismTest.java b/prism/src/prism/PrismTest.java index 110635c2..a67a0f53 100644 --- a/prism/src/prism/PrismTest.java +++ b/prism/src/prism/PrismTest.java @@ -64,12 +64,12 @@ public class PrismTest prism.loadPRISMModel(modulesFile); // Parse a prop, check on model 1 - propertiesFile = prism.parsePropertiesString(modulesFile, "P=?[F<=0.1 s1=1]"); + propertiesFile = prism.parsePropertiesString("P=?[F<=0.1 s1=1]"); result = prism.modelCheck(propertiesFile, propertiesFile.getPropertyObject(0)); System.out.println(result.getResult()); // Parse another prop, check on model 1 - propertiesFile = prism.parsePropertiesString(modulesFile, "P=?[F<=0.1 s1=1]"); + propertiesFile = prism.parsePropertiesString("P=?[F<=0.1 s1=1]"); result = prism.modelCheck(propertiesFile, propertiesFile.getPropertyObject(0)); System.out.println(result.getResult()); @@ -78,7 +78,7 @@ public class PrismTest prism.loadPRISMModel(modulesFile); // Parse a prop, check on model 2 - propertiesFile = prism.parsePropertiesString(modulesFile, "P=?[F<=0.1 s1=1]"); + propertiesFile = prism.parsePropertiesString("P=?[F<=0.1 s1=1]"); result = prism.modelCheck(propertiesFile, propertiesFile.getPropertyObject(0)); System.out.println(result.getResult()); diff --git a/prism/src/userinterface/properties/GUIMultiProperties.java b/prism/src/userinterface/properties/GUIMultiProperties.java index bab3eb0a..db664ab0 100644 --- a/prism/src/userinterface/properties/GUIMultiProperties.java +++ b/prism/src/userinterface/properties/GUIMultiProperties.java @@ -275,7 +275,7 @@ public class GUIMultiProperties extends GUIPlugin implements MouseListener, List // Get valid/selected properties String propertiesString = getLabelsString() + "\n" + getConstantsString() + "\n" + propList.getValidSelectedAndReferencedString(); // Get PropertiesFile for valid/selected properties - parsedProperties = getPrism().parsePropertiesString(parsedModel, propertiesString); + parsedProperties = getPrism().parsePropertiesString(propertiesString); // And get list of corresponding GUIProperty objects validGUIProperties = propList.getValidSelectedProperties(); // Query user for undefined constant values (if required) @@ -317,7 +317,7 @@ public class GUIMultiProperties extends GUIPlugin implements MouseListener, List ArrayList simulatableExprs; UndefinedConstants uCon; try { - parsedProperties = getPrism().parsePropertiesString(parsedModel, + parsedProperties = getPrism().parsePropertiesString( getLabelsString() + "\n" + getConstantsString() + "\n" + propList.getValidSelectedAndReferencedString()); validGUIProperties = propList.getValidSelectedProperties(); if (validGUIProperties.size() == 0) { @@ -411,7 +411,7 @@ public class GUIMultiProperties extends GUIPlugin implements MouseListener, List }*/ // parse property to be used for experiment - parsedProperties = getPrism().parsePropertiesString(parsedModel, + parsedProperties = getPrism().parsePropertiesString( getLabelsString() + "\n" + getConstantsString() + "\n" + propList.getValidSelectedAndReferencedString()); if (parsedProperties.getNumProperties() <= 0) { error("There are no properties selected"); @@ -750,7 +750,7 @@ public class GUIMultiProperties extends GUIPlugin implements MouseListener, List error("No file selected"); return; } - Thread t = new LoadPropertiesThread(this, parsedModel, file); + Thread t = new LoadPropertiesThread(this, file); t.setPriority(Thread.NORM_PRIORITY); t.start(); } @@ -835,7 +835,7 @@ public class GUIMultiProperties extends GUIPlugin implements MouseListener, List error("No file selected"); return; } - Thread t = new LoadPropertiesThread(this, parsedModel, file, true); + Thread t = new LoadPropertiesThread(this, file, true); t.setPriority(Thread.NORM_PRIORITY); t.start(); } else { @@ -1037,7 +1037,7 @@ public class GUIMultiProperties extends GUIPlugin implements MouseListener, List public void a_newProperty() { - GUIPropertyEditor ed = new GUIPropertyEditor(this, parsedModel, getInvalidPropertyStrategy()); + GUIPropertyEditor ed = new GUIPropertyEditor(this, getInvalidPropertyStrategy()); ed.show(); } @@ -1051,7 +1051,7 @@ public class GUIMultiProperties extends GUIPlugin implements MouseListener, List gp.setBeingEdited(true); // Force repaint because we modified the GUIProperty directly repaintList(); - GUIPropertyEditor ed = new GUIPropertyEditor(this, parsedModel, gp, getInvalidPropertyStrategy()); + GUIPropertyEditor ed = new GUIPropertyEditor(this, gp, getInvalidPropertyStrategy()); ed.show(); } } @@ -1126,7 +1126,7 @@ public class GUIMultiProperties extends GUIPlugin implements MouseListener, List exportLabelsAfterReceiveParseNotification = false; try { // Parse labels/constants - parsedProperties = getPrism().parsePropertiesString(parsedModel, getLabelsString() + "\n" + getConstantsString()); + parsedProperties = getPrism().parsePropertiesString(getLabelsString() + "\n" + getConstantsString()); // Query user for undefined constant values (if required) UndefinedConstants uCon = new UndefinedConstants(parsedModel, parsedProperties, true); if (uCon.getMFNumUndefined() + uCon.getPFNumUndefined() > 0) { @@ -1365,7 +1365,7 @@ public class GUIMultiProperties extends GUIPlugin implements MouseListener, List private void checkForPropertiesToLoad() { if (argsPropertiesFile != null) { - Thread t = new LoadPropertiesThread(this, parsedModel, new File(argsPropertiesFile)); + Thread t = new LoadPropertiesThread(this, new File(argsPropertiesFile)); t.setPriority(Thread.NORM_PRIORITY); t.start(); //we clear the variable to avoid loading property file every time a model is parsed. diff --git a/prism/src/userinterface/properties/GUIPropConstantList.java b/prism/src/userinterface/properties/GUIPropConstantList.java index 70cc1d50..4de6a8eb 100644 --- a/prism/src/userinterface/properties/GUIPropConstantList.java +++ b/prism/src/userinterface/properties/GUIPropConstantList.java @@ -358,7 +358,7 @@ public class GUIPropConstantList extends JTable { try { error = null; - parent.getPrism().parsePropertiesString(parent.getParsedModel(), parseableToString()); + parent.getPrism().parsePropertiesString(parseableToString()); } catch (PrismException e) { error = e; diff --git a/prism/src/userinterface/properties/GUIPropLabelList.java b/prism/src/userinterface/properties/GUIPropLabelList.java index 6735efef..7e174ce2 100644 --- a/prism/src/userinterface/properties/GUIPropLabelList.java +++ b/prism/src/userinterface/properties/GUIPropLabelList.java @@ -27,13 +27,19 @@ package userinterface.properties; -import java.util.*; -import java.awt.*; -import javax.swing.*; -import javax.swing.table.*; +import java.awt.Color; +import java.awt.Component; +import java.awt.Font; +import java.util.ArrayList; -import parser.ast.*; -import prism.*; +import javax.swing.CellEditor; +import javax.swing.JTable; +import javax.swing.table.AbstractTableModel; +import javax.swing.table.DefaultTableCellRenderer; + +import parser.ast.LabelList; +import parser.ast.PropertiesFile; +import prism.PrismException; public class GUIPropLabelList extends JTable { @@ -331,7 +337,7 @@ public class GUIPropLabelList extends JTable { try { error = null; - parent.getPrism().parsePropertiesString(parent.getParsedModel(), parent.getConstantsString()+"\n"+parseableToString()); + parent.getPrism().parsePropertiesString(parent.getConstantsString()+"\n"+parseableToString()); } catch (PrismException e) { error = e; diff --git a/prism/src/userinterface/properties/GUIPropertiesList.java b/prism/src/userinterface/properties/GUIPropertiesList.java index 0e0bf2da..d21e966e 100644 --- a/prism/src/userinterface/properties/GUIPropertiesList.java +++ b/prism/src/userinterface/properties/GUIPropertiesList.java @@ -428,7 +428,7 @@ public class GUIPropertiesList extends JList implements KeyListener int i = 0; while (i < list.size()) { GUIProperty p = list.get(i); - p.parse(parent.getParsedModel(), parent.getConstantsString(), parent.getLabelsString()); + p.parse(parent.getConstantsString(), parent.getLabelsString()); if (p.isValid()) { list.remove(i); changed = true; diff --git a/prism/src/userinterface/properties/GUIProperty.java b/prism/src/userinterface/properties/GUIProperty.java index 3c53c7b3..acfe1da9 100644 --- a/prism/src/userinterface/properties/GUIProperty.java +++ b/prism/src/userinterface/properties/GUIProperty.java @@ -31,14 +31,19 @@ package userinterface.properties; import java.util.Vector; -import javax.swing.*; +import javax.swing.ImageIcon; -import userinterface.GUIPrism; import param.BigRational; -import parser.*; -import parser.ast.*; -import parser.type.TypeVoid; -import prism.*; +import parser.Values; +import parser.ast.Expression; +import parser.ast.ModulesFile; +import parser.ast.PropertiesFile; +import prism.Interval; +import prism.Prism; +import prism.PrismException; +import prism.Result; +import prism.TileList; +import userinterface.GUIPrism; /** * Encapsulates a property in the list in the GUI "Properties" tab. @@ -356,7 +361,7 @@ public class GUIProperty } } - public void parse(ModulesFile m, String constantsString, String labelString) + public void parse(String constantsString, String labelString) { if (propString == null || constantsString == null || labelString == null) { expr = null; @@ -369,7 +374,7 @@ public class GUIProperty boolean couldBeNoConstantsOrLabels = false; PropertiesFile fConLab = null; try { - fConLab = prism.parsePropertiesString(m, constantsString + "\n" + labelString); + fConLab = prism.parsePropertiesString(constantsString + "\n" + labelString); } catch (PrismException e) { couldBeNoConstantsOrLabels = true; } @@ -388,7 +393,7 @@ public class GUIProperty //Parse all together String withConsLabs = constantsString + "\n" + labelString + "\n" + namedString + propString; - PropertiesFile ff = prism.parsePropertiesString(m, withConsLabs); + PropertiesFile ff = prism.parsePropertiesString(withConsLabs); //Validation of number of properties if (ff.getNumProperties() <= namedCount) diff --git a/prism/src/userinterface/properties/GUIPropertyEditor.java b/prism/src/userinterface/properties/GUIPropertyEditor.java index 6b1496d0..bdece711 100644 --- a/prism/src/userinterface/properties/GUIPropertyEditor.java +++ b/prism/src/userinterface/properties/GUIPropertyEditor.java @@ -51,7 +51,6 @@ public class GUIPropertyEditor extends javax.swing.JDialog implements ActionList private GUIPrism parent; private GUIMultiProperties props; - private ModulesFile parsedModel; private boolean dispose = false; private String id; private int propertyInvalidStrategy = GUIMultiProperties.WARN_INVALID_PROPS; @@ -62,9 +61,9 @@ public class GUIPropertyEditor extends javax.swing.JDialog implements ActionList * whether the dialog should be modal and a Vector of properties to be displayed * for user browsing/copying. */ - public GUIPropertyEditor(GUIMultiProperties props, ModulesFile parsedModel, int strategy) //Adding constructor + public GUIPropertyEditor(GUIMultiProperties props,int strategy) //Adding constructor { - this(props, parsedModel, null, strategy); + this(props, null, strategy); } /** Creates a new GUIPropertyEditor with its parent GUIPrism, a boolean stating @@ -72,12 +71,11 @@ public class GUIPropertyEditor extends javax.swing.JDialog implements ActionList * for user browsing/copying and a string showing the default value of the * property text box. */ - public GUIPropertyEditor(GUIMultiProperties props, ModulesFile parsedModel, GUIProperty prop, int strategy) //Editing constructor + public GUIPropertyEditor(GUIMultiProperties props, GUIProperty prop, int strategy) //Editing constructor { super(props.getGUI(), false); this.props = props; this.parent = props.getGUI(); - this.parsedModel = parsedModel; this.propertyInvalidStrategy = strategy; initComponents(); this.getRootPane().setDefaultButton(okayButton); @@ -808,7 +806,7 @@ public class GUIPropertyEditor extends javax.swing.JDialog implements ActionList try { //Parse constants and labels - PropertiesFile fConLab = props.getPrism().parsePropertiesString(parsedModel, props.getLabelsString()+"\n"+props.getConstantsString()); + PropertiesFile fConLab = props.getPrism().parsePropertiesString(props.getLabelsString()+"\n"+props.getConstantsString()); noConstants = fConLab.getConstantList().size(); noLabels = fConLab.getLabelList().size(); @@ -824,7 +822,7 @@ public class GUIPropertyEditor extends javax.swing.JDialog implements ActionList //Parse all together String withConsLabs = props.getConstantsString()+"\n"+props.getLabelsString()+namedString+propertyText.getText(); - PropertiesFile ff = props.getPrism().parsePropertiesString(parsedModel, withConsLabs); + PropertiesFile ff = props.getPrism().parsePropertiesString(withConsLabs); //Validation of number of properties if(ff.getNumProperties() <= namedCount) throw new PrismException("Empty property"); diff --git a/prism/src/userinterface/properties/computation/LoadPropertiesThread.java b/prism/src/userinterface/properties/computation/LoadPropertiesThread.java index 9c4824c6..58f5bcb3 100644 --- a/prism/src/userinterface/properties/computation/LoadPropertiesThread.java +++ b/prism/src/userinterface/properties/computation/LoadPropertiesThread.java @@ -38,7 +38,6 @@ import parser.ast.*; public class LoadPropertiesThread extends Thread { private GUIMultiProperties parent; - private ModulesFile mf; private Prism pri; private File file; private PropertiesFile props = null; @@ -46,15 +45,14 @@ public class LoadPropertiesThread extends Thread private Exception ex; /** Creates a new instance of LoadPropertiesThread */ - public LoadPropertiesThread(GUIMultiProperties parent, ModulesFile mf, File file) + public LoadPropertiesThread(GUIMultiProperties parent, File file) { - this(parent, mf, file, false); + this(parent, file, false); } - public LoadPropertiesThread(GUIMultiProperties parent, ModulesFile mf, File file, boolean isInsert) + public LoadPropertiesThread(GUIMultiProperties parent, File file, boolean isInsert) { this.parent = parent; - this.mf = mf; this.file = file; this.pri = parent.getPrism(); this.isInsert = isInsert; @@ -73,7 +71,7 @@ public class LoadPropertiesThread extends Thread // do parsing try { - props = pri.parsePropertiesFile(mf, file, false); + props = pri.parsePropertiesFile(file, false); } //If there was a problem with the loading, notify the interface. catch (FileNotFoundException e) { @@ -105,7 +103,6 @@ public class LoadPropertiesThread extends Thread parent.propertyInsertSuccessful(props); else parent.propertyLoadSuccessful(props, file); - //System.out.println("In invokeAndWait after propertyLoadSuccessful "); }}); } // catch and ignore any thread exceptions diff --git a/prism/src/userinterface/simulator/GUISimulator.java b/prism/src/userinterface/simulator/GUISimulator.java index 811f8433..0866af95 100644 --- a/prism/src/userinterface/simulator/GUISimulator.java +++ b/prism/src/userinterface/simulator/GUISimulator.java @@ -387,7 +387,7 @@ public class GUISimulator extends GUIPlugin implements MouseListener, ListSelect // get properties constants/labels PropertiesFile pf; try { - pf = getPrism().parsePropertiesString(parsedModel, guiProp.getConstantsString().toString() + guiProp.getLabelsString()); + pf = getPrism().parsePropertiesString(guiProp.getConstantsString().toString() + guiProp.getLabelsString()); } catch (PrismLangException e) { // ignore properties if they don't parse pf = null; //if any problems @@ -727,7 +727,7 @@ public class GUISimulator extends GUIPlugin implements MouseListener, ListSelect // get properties constants/labels PropertiesFile pf; try { - pf = getPrism().parsePropertiesString(parsedModel, guiProp.getConstantsString().toString() + guiProp.getLabelsString()); + pf = getPrism().parsePropertiesString(guiProp.getConstantsString().toString() + guiProp.getLabelsString()); } catch (PrismLangException e) { // ignore properties if they don't parse pf = null; //if any problems