s14h
/
prism-accumulation
1
0
Fork 0
Code Releases Activity
Browse Source

Added option to verify PTAs in GUI (no experiments yet). 

git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@2191 bbc10eb1-c90d-0410-af57-cb519fbb1720
master
Dave Parker 15 years ago
parent
da9ca7124c
commit
e9545cac7c
3 changed files with 139 additions and 102 deletions
Whitespace
Show all changes Ignore whitespace when comparing lines Ignore changes in amount of whitespace Ignore changes in whitespace at EOL
Split View
Diff Options
Show Stats Download Patch File Download Diff File
  1. 18
      prism/src/prism/PrismCL.java
  2. 99
      prism/src/userinterface/properties/GUIMultiProperties.java
  3. 124
      prism/src/userinterface/properties/computation/ModelCheckThread.java

18
prism/src/prism/PrismCL.java
View File

@ -266,17 +266,17 @@ public class PrismCL
tmpLog.print(mfTmp.toString());
}
// decide if model construction is necessary
// Decide if model construction is necessary
boolean doBuild = true;
// if explicitly disabled...
// If explicitly disabled...
if (nobuild)
doBuild = false;
// no need if using approximate (simulation-based) model checking...
// No need if using approximate (simulation-based) model checking...
if (simulate)
doBuild = false;
// no need for PTA model checking (when not using digital clocks)...
else if (modulesFile.getModelType() == ModelType.PTA
&& !prism.getSettings().getString(PrismSettings.PRISM_PTA_METHOD).equals("Digital clocks"))
// No need if doing PTA model checking...
// (NB: PTA digital clocks excluded - has already been reduced to an MDP)
if (modulesFile.getModelType() == ModelType.PTA)
doBuild = false;
// do model construction (if necessary)
@ -396,12 +396,10 @@ public class PrismCL
// exact (non-appoximate) model checking
if (!simulate) {
// PTA model checking
if (modulesFile.getModelType() == ModelType.PTA
&& !prism.getSettings().getString(PrismSettings.PRISM_PTA_METHOD).equals(
"Digital clocks")) {
if (modulesFile.getModelType() == ModelType.PTA) {
res = prism.modelCheckPTA(modulesFile, propertiesFile, propertiesToCheck[j]);
}
// non-PTA model checking
// Non-PTA model checking
else {
res = prism.modelCheck(model, propertiesFile, propertiesToCheck[j]);
}

99
prism/src/userinterface/properties/GUIMultiProperties.java
View File

@ -61,14 +61,15 @@ public class GUIMultiProperties extends GUIPlugin implements MouseListener, List
public static final int WARN_INVALID_PROPS = 1;
public static final int NEVER_INVALID_PROPS = 2;
//ATTRIBUTES
// ATTRIBUTES
// current model (gets updated only by event listening to GUIModel)
// Current model (gets updated only by event listening to GUIModel)
private ModulesFile parsedModel;
private Model builtModel;
private Values lastBuildValues;
// Constants for model (updated by events or locally)
private Values mfConstants;
//state
// State
private boolean modified;
private boolean modifiedSinceBuild;
private boolean computing;
@ -77,10 +78,9 @@ public class GUIMultiProperties extends GUIPlugin implements MouseListener, List
private PropertiesFile parsedProperties;
private ArrayList<GUIProperty> propertiesToBeVerified;
private File activeFile;
private Values lastPFConstants;
private Values lastSimulateValues;
private Values pfConstants;
//gui
// GUI
private GUIPrismFileFilter propsFilter[];
private GUIPrismFileFilter textFilter[];
private JMenu propMenu;
@ -90,11 +90,10 @@ public class GUIMultiProperties extends GUIPlugin implements MouseListener, List
private JScrollPane expScroller;
private JLabel fileLabel;
private Vector clipboardVector;
private Action newProps, openProps, saveProps, savePropsAs, insertProps, verifySelected, newProperty, editProperty, newConstant, removeConstant, newLabel,
removeLabel, newExperiment, deleteExperiment, stopExperiment, viewResults, plotResults, exportResults, simulate, details;
//current properties
// Current properties
private GUIPropertiesList propList;
private GUIPropConstantList consTable;
private GUIPropLabelList labTable;
@ -103,7 +102,7 @@ public class GUIMultiProperties extends GUIPlugin implements MouseListener, List
private Font displayFontFast;
private Color backgroundFast, warningFast;
//CONSTRUCTORS
// CONSTRUCTORS
/** Creates a new instance of GUIMultiProperties */
public GUIMultiProperties(GUIPrism pr, GUISimulator simulator)
@ -184,14 +183,10 @@ public class GUIMultiProperties extends GUIPlugin implements MouseListener, List
protected void verifyAfterBuild()
{
verifyAfterReceiveBuildNotification = false;
// Re-enable GUI elements
propList.setEnabled(true);
consTable.setEnabled(true);
labTable.setEnabled(true);
// Start model check process
if (builtModel != null && parsedProperties != null && propertiesToBeVerified != null) {
Thread t = new ModelCheckThread(this, builtModel, parsedProperties, propertiesToBeVerified, lastBuildValues, lastPFConstants);
Thread t = new ModelCheckThread(this, builtModel, parsedProperties, propertiesToBeVerified, mfConstants, pfConstants);
t.setPriority(Thread.NORM_PRIORITY);
t.start();
}
@ -200,46 +195,54 @@ public class GUIMultiProperties extends GUIPlugin implements MouseListener, List
protected void verifyAfterParse()
{
ArrayList<GUIProperty> validGUIProperties;
Values buildValues;
UndefinedConstants uCon;
verifyAfterReceiveParseNotification = false;
// Get valid/selected properties
try {
// Get valid/selected properties
String propertiesString = getLabelsString() + "\n" + getConstantsString() + "\n" + propList.getValidSelectedString();
// Get PropertiesFile for valid/selected properties
parsedProperties = getPrism().parsePropertiesString(parsedModel, propertiesString);
// And get list of corresponding GUIProperty objects
validGUIProperties = propList.getValidSelectedProperties();
} catch (PrismException e) {
error(e.getMessage());
return;
}
// Query user for undefined constant values (if required)
try {
// Query user for undefined constant values (if required)
uCon = new UndefinedConstants(parsedModel, parsedProperties);
if (uCon.getMFNumUndefined() + uCon.getPFNumUndefined() > 0) {
int result = GUIConstantsPicker.defineConstantsWithDialog(this.getGUI(), uCon, lastBuildValues, lastPFConstants);
// Use previous constant values as defaults in dialog
int result = GUIConstantsPicker.defineConstantsWithDialog(this.getGUI(), uCon, mfConstants, pfConstants);
if (result != GUIConstantsPicker.VALUES_DONE)
return;
}
buildValues = uCon.getMFConstantValues();
lastPFConstants = uCon.getPFConstantValues();
parsedProperties.setUndefinedConstants(lastPFConstants);
// Store model constants (even though will be stored again after build)
// Don't set in model: this will be done during build process
mfConstants = uCon.getMFConstantValues();
// Store property constants and set in file
pfConstants = uCon.getPFConstantValues();
parsedProperties.setUndefinedConstants(pfConstants);
// Store properties to be verified
propertiesToBeVerified = validGUIProperties;
// If required, trigger build then verify
if (parsedModel.getModelType() != ModelType.PTA) {
verifyAfterReceiveBuildNotification = true;
notifyEventListeners(new GUIPropertiesEvent(GUIPropertiesEvent.REQUEST_MODEL_BUILD, mfConstants));
}
// If no build required (e.g. for PTAs), just do model checking now
else {
// Start model check process
parsedModel.setUndefinedConstants(mfConstants);
if (parsedProperties != null && propertiesToBeVerified != null) {
Thread t = new ModelCheckThread(this, parsedModel, parsedProperties, propertiesToBeVerified, mfConstants, pfConstants);
t.setPriority(Thread.NORM_PRIORITY);
t.start();
}
}
} catch (PrismException e) {
error(e.getMessage());
return;
}
// Disable GUI elements in Properties tab
propList.setEnabled(false);
consTable.setEnabled(false);
// Trigger build then verify
verifyAfterReceiveBuildNotification = true;
propertiesToBeVerified = validGUIProperties;
notifyEventListeners(new GUIPropertiesEvent(GUIPropertiesEvent.REQUEST_MODEL_BUILD, buildValues));
}
public void simulateAfterParse()
@ -285,15 +288,16 @@ public class GUIMultiProperties extends GUIPlugin implements MouseListener, List
try {
uCon = new UndefinedConstants(parsedModel, parsedProperties);
if (uCon.getMFNumUndefined() + uCon.getPFNumUndefined() > 0) {
int result = GUIConstantsPicker.defineConstantsWithDialog(this.getGUI(), uCon, lastSimulateValues, lastPFConstants);
// Use previous constant values as defaults in dialog
int result = GUIConstantsPicker.defineConstantsWithDialog(this.getGUI(), uCon, mfConstants, pfConstants);
if (result != GUIConstantsPicker.VALUES_DONE)
return;
}
lastSimulateValues = uCon.getMFConstantValues();
lastPFConstants = uCon.getPFConstantValues();
parsedModel.setUndefinedConstants(lastSimulateValues);
parsedProperties.setUndefinedConstants(lastPFConstants);
// Store model/property constants and set in files
mfConstants = uCon.getMFConstantValues();
pfConstants = uCon.getPFConstantValues();
parsedModel.setUndefinedConstants(mfConstants);
parsedProperties.setUndefinedConstants(pfConstants);
SimulationInformation info = GUISimulationPicker.defineSimulationWithDialog(this.getGUI(), parsedModel.getInitialValues(), parsedModel);
if (info == null)
@ -308,7 +312,7 @@ public class GUIMultiProperties extends GUIPlugin implements MouseListener, List
new GUISimulatorDistributionDialog(getGUI(), getPrism().getSimulator(), true).show(this, parsedModel, parsedProperties, validGUIProperties,
info);
} else {
Thread t = new SimulateModelCheckThread(this, parsedModel, parsedProperties, validGUIProperties, lastSimulateValues, lastPFConstants,
Thread t = new SimulateModelCheckThread(this, parsedModel, parsedProperties, validGUIProperties, mfConstants, pfConstants,
initialState, noIterations, maxPathLength, info);
t.setPriority(Thread.NORM_PRIORITY);
t.start();
@ -541,8 +545,10 @@ public class GUIMultiProperties extends GUIPlugin implements MouseListener, List
newProperty.setEnabled(!computing);
editProperty.setEnabled(!computing && propList.getSelectedProperties().size() > 0);
// constants list
consTable.setEnabled(!computing);
removeConstant.setEnabled(consTable.getSelectedRowCount() > 0);
// label list
labTable.setEnabled(!computing);
removeLabel.setEnabled(labTable.getSelectedRowCount() > 0);
// newExperiment: enabled if there is exactly one prop selected and it is valid
@ -1032,7 +1038,7 @@ public class GUIMultiProperties extends GUIPlugin implements MouseListener, List
} else if (me.getID() == GUIModelEvent.MODEL_BUILT) {
setBuiltModel(me.getModel());
if (me.getBuildValues() != null)
lastBuildValues = me.getBuildValues();
mfConstants = me.getBuildValues();
modifiedSinceBuild = false;
if (verifyAfterReceiveBuildNotification)
verifyAfterBuild();
@ -1820,7 +1826,6 @@ public class GUIMultiProperties extends GUIPlugin implements MouseListener, List
stopExperiment.putValue(Action.LONG_DESCRIPTION, "Stops the Experiment that is currently running");
stopExperiment.putValue(Action.SMALL_ICON, GUIPrism.getIconFromImage("smallStop.png"));
stopExperiment.setEnabled(false);
}
/**

124
prism/src/userinterface/properties/computation/ModelCheckThread.java
View File

@ -38,35 +38,57 @@ import userinterface.util.*;
import userinterface.properties.*;
/**
*
* @author ug60axh
* Thread that executes model checking of a property via PRISM.
*/
public class ModelCheckThread extends GUIComputationThread
{
// Access to GUI (to send notifications etc.)
private GUIMultiProperties parent;
// Model (in most cases, have a Model object; in others, e.g. PTA model checking,
// we just have the language-level model description, i.e. a ModulesFile).
// Currently exactly one-of m/mf is non-null
private Model m;
private PropertiesFile prFi;
private ModulesFile mf;
// Properties file and GUI properties (these are assumed to match)
// (Also need properties file for access to constants/labels/etc.)
private PropertiesFile pf;
private ArrayList<GUIProperty> guiProps;
// Values give to constants
private Values definedMFConstants;
private Values definedPFConstants;
/** Creates a new instance of ModelCheckThread */
public ModelCheckThread(GUIMultiProperties parent, Model m, PropertiesFile prFi, ArrayList<GUIProperty> guiProps, Values definedMFConstants, Values definedPFConstants)
/**
* Create a new instance of ModelCheckThread (where a Model has been built)
*/
public ModelCheckThread(GUIMultiProperties parent, Model m, PropertiesFile pf, ArrayList<GUIProperty> guiProps, Values definedMFConstants,
Values definedPFConstants)
{
super(parent);
this.parent = parent;
this.m = m;
this.prFi = prFi;
this.mf = null;
this.pf = pf;
this.guiProps = guiProps;
this.definedMFConstants = definedMFConstants;
this.definedPFConstants = definedPFConstants;
}
/**
* Create a new instance of ModelCheckThread (where no Model has been built, e.g. PTAs)
*/
public ModelCheckThread(GUIMultiProperties parent, ModulesFile mf, PropertiesFile pf, ArrayList<GUIProperty> guiProps, Values definedMFConstants,
Values definedPFConstants)
{
this(parent, (Model) null, pf, guiProps, definedMFConstants, definedPFConstants);
this.mf = mf;
}
public void run()
{
if(m == null) return;
//Notify user interface of the start of computation
if (m == null && mf == null)
return;
// Notify user interface of the start of computation
SwingUtilities.invokeLater(new Runnable()
{
public void run()
@ -76,54 +98,67 @@ public class ModelCheckThread extends GUIComputationThread
parent.notifyEventListeners(new GUIComputationEvent(GUIComputationEvent.COMPUTATION_START, parent));
}
});
Result result = null;
//Set icon for all properties to be verified to a clock
for(int i = 0; i < guiProps.size(); i++)
{
// Set icon for all properties to be verified to a clock
for (int i = 0; i < guiProps.size(); i++) {
GUIProperty gp = guiProps.get(i);
gp.setStatus(GUIProperty.STATUS_DOING);
parent.repaintList();
}
IconThread ic = new IconThread(null);
for(int i = 0; i < prFi.getNumProperties(); i++)
{
// get property
// Work through list of properties
for (int i = 0; i < pf.getNumProperties(); i++) {
// Get ith property
GUIProperty gp = guiProps.get(i);
// animate it's clock icon
// Animate it's clock icon
ic = new IconThread(gp);
ic.start();
// do model checking
try
{
// Do model checking
try {
// Print info to log
logln("\n-------------------------------------------");
logln("\nModel checking: " + prFi.getProperty(i));
if (definedMFConstants != null) if (definedMFConstants.getNumValues() > 0) logln("Model constants: " + definedMFConstants);
if (definedPFConstants != null) if (definedPFConstants.getNumValues() > 0) logln("Property constants: " + definedPFConstants);
result = prism.modelCheck(m, prFi, prFi.getProperty(i));
}
catch(PrismException e)
{
logln("\nModel checking: " + pf.getProperty(i));
if (definedMFConstants != null)
if (definedMFConstants.getNumValues() > 0)
logln("Model constants: " + definedMFConstants);
if (definedPFConstants != null)
if (definedPFConstants.getNumValues() > 0)
logln("Property constants: " + definedPFConstants);
// No model (PTA) case
if (m == null) {
if (mf.getModelType() != ModelType.PTA)
throw new PrismException("No model to verify");
result = prism.modelCheckPTA(mf, pf, pf.getProperty(i));
}
// Normal model checking
else {
result = prism.modelCheck(m, pf, pf.getProperty(i));
}
} catch (PrismException e) {
result = new Result(e);
error(e.getMessage());
}
ic.interrupt();
try
{
try {
ic.join();
} catch (InterruptedException e) {
}
catch(InterruptedException e)
{}
//while(!ic.canContinue){}
gp.setResult(result);
gp.setMethodString("Verification");
gp.setConstants(definedMFConstants, definedPFConstants);
parent.repaintList();
}
// Notify user interface of the end of computation
SwingUtilities.invokeLater(new Runnable()
{
public void run()
@ -136,11 +171,13 @@ public class ModelCheckThread extends GUIComputationThread
});
}
// Clock animation icon
class IconThread extends Thread
{
GUIProperty gp;
ImageIcon[] images;
boolean canContinue = false;
public IconThread(GUIProperty gp)
{
this.gp = gp;
@ -154,22 +191,19 @@ public class ModelCheckThread extends GUIComputationThread
images[6] = GUIPrism.getIconFromImage("smallClockAnim7.png");
images[7] = GUIPrism.getIconFromImage("smallClockAnim8.png");
}
public void run()
{
try
{
try {
int counter = 0;
while(!interrupted() && gp != null)
{
while (!interrupted() && gp != null) {
counter++;
counter = counter%8;
counter = counter % 8;
gp.setDoingImage(images[counter]);
parent.repaintList();
sleep(150);
}
}
catch(InterruptedException e)
{
} catch (InterruptedException e) {
}
canContinue = true;
}

Write Preview
Loading…
Cancel
Save