From a218d09b2b541832af0bbec1e2275760b1dda63f Mon Sep 17 00:00:00 2001 From: Dave Parker Date: Thu, 9 Feb 2012 20:24:07 +0000 Subject: [PATCH] * Continued major changes to PRISM API - keeps track of model, builds when needed - takes care of explicit engine stuff too * Changes to deadlock handling: - new option for "fix deadlocks" (defaults to *true*) (and new switch -fixdl) - consistent deadlock handling everywhere, incl. GUI and experiments - changes to model-level deadlock storage (symbolic and explicit) * Explicit engine added as true engine, also available from GUI git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@4562 bbc10eb1-c90d-0410-af57-cb519fbb1720 --- prism/src/explicit/ConstructModel.java | 21 +- prism/src/explicit/DTMCEmbeddedSimple.java | 11 +- .../DTMCFromMDPMemorylessAdversary.java | 11 +- prism/src/explicit/DTMCSimple.java | 26 +- prism/src/explicit/DTMCUniformisedSimple.java | 11 +- prism/src/explicit/MDPSimple.java | 33 +- prism/src/explicit/MDPSparse.java | 27 +- prism/src/explicit/Model.java | 26 +- prism/src/explicit/ModelExplicit.java | 25 +- prism/src/explicit/PrismExplicit.java | 7 +- prism/src/explicit/STPGAbstrSimple.java | 39 +- prism/src/explicit/StateModelChecker.java | 2 +- prism/src/prism/ExplicitFiles2MTBDD.java | 2 +- prism/src/prism/ExplicitModel2MTBDD.java | 2 +- prism/src/prism/LTLModelChecker.java | 6 +- prism/src/prism/Model.java | 24 +- prism/src/prism/Modules2MTBDD.java | 4 +- prism/src/prism/NondetModel.java | 24 +- prism/src/prism/NondetModelChecker.java | 2 +- prism/src/prism/Prism.java | 952 ++++-- prism/src/prism/PrismCL.java | 342 +- prism/src/prism/PrismModelListener.java | 33 + prism/src/prism/PrismSettings.java | 20 +- prism/src/prism/ProbModel.java | 34 +- prism/src/prism/StateModelChecker.java | 2 +- .../userinterface/model/GUIModelEvent.java | 112 +- .../userinterface/model/GUIMultiModel.java | 699 ++-- .../model/GUIMultiModelHandler.java | 2888 ++++++++--------- .../model/computation/BuildModelThread.java | 231 +- .../computation/ComputeSteadyStateThread.java | 31 +- .../computation/ComputeTransientThread.java | 27 +- .../computation/ExportBuiltModelThread.java | 106 +- .../model/computation/ParseModelThread.java | 81 +- .../properties/GUIExperiment.java | 155 +- .../properties/GUIExperimentTable.java | 4 +- .../properties/GUIMultiProperties.java | 93 +- .../computation/ModelCheckThread.java | 77 +- .../computation/SimulateModelCheckThread.java | 58 +- 38 files changed, 3039 insertions(+), 3209 deletions(-) create mode 100644 prism/src/prism/PrismModelListener.java diff --git a/prism/src/explicit/ConstructModel.java b/prism/src/explicit/ConstructModel.java index 3b20a76c..20a6bd09 100644 --- a/prism/src/explicit/ConstructModel.java +++ b/prism/src/explicit/ConstructModel.java @@ -41,6 +41,12 @@ public class ConstructModel private SimulatorEngine engine; private PrismLog mainLog; + // Options: + // Find deadlocks during model construction? + private boolean findDeadlocks = true; + // Automatically fix deadlocks? + private boolean fixDeadlocks = true; + // Basic info needed about model // private ModelType modelType; @@ -58,6 +64,11 @@ public class ConstructModel return statesList; } + public void setFixDeadlocks(boolean b) + { + fixDeadlocks = b; + } + /** * Build the set of reachable states for a PRISM model language description and return. * @param modulesFile The PRISM model @@ -118,7 +129,6 @@ public class ConstructModel // Misc int i, j, nc, nt, src, dest; long timer, timerProgress; - boolean fixdl = false; // Don't support multiple initial states if (modulesFile.getInitialStates() != null) { @@ -249,12 +259,9 @@ public class ConstructModel mainLog.println(" done in " + ((System.currentTimeMillis() - timer) / 1000.0) + " secs."); //mainLog.println(states); - // Fix deadlocks (if required) - if (!justReach && fixdl) { - BitSet deadlocks = modelSimple.findDeadlocks(true); - if (deadlocks.cardinality() > 0) { - mainLog.println("Added self-loops in " + deadlocks.cardinality() + " states..."); - } + // Find/fix deadlocks (if required) + if (!justReach && findDeadlocks) { + modelSimple.findDeadlocks(fixDeadlocks); } boolean sort = true; diff --git a/prism/src/explicit/DTMCEmbeddedSimple.java b/prism/src/explicit/DTMCEmbeddedSimple.java index 659edfae..c10fc071 100644 --- a/prism/src/explicit/DTMCEmbeddedSimple.java +++ b/prism/src/explicit/DTMCEmbeddedSimple.java @@ -105,9 +105,9 @@ public class DTMCEmbeddedSimple extends DTMCExplicit return ctmc.isInitialState(i); } - public boolean isFixedDeadlockState(int i) + public boolean isDeadlockState(int i) { - return ctmc.isFixedDeadlockState(i); + return ctmc.isDeadlockState(i); } public List getStatesList() @@ -146,20 +146,19 @@ public class DTMCEmbeddedSimple extends DTMCExplicit return 1; } - public void checkForDeadlocks() throws PrismException + public void findDeadlocks(boolean fix) throws PrismException { // No deadlocks by definition } - public void checkForDeadlocks(BitSet except) throws PrismException + public void checkForDeadlocks() throws PrismException { // No deadlocks by definition } - public BitSet findDeadlocks(boolean fix) throws PrismException + public void checkForDeadlocks(BitSet except) throws PrismException { // No deadlocks by definition - return new BitSet(); } @Override diff --git a/prism/src/explicit/DTMCFromMDPMemorylessAdversary.java b/prism/src/explicit/DTMCFromMDPMemorylessAdversary.java index b477ad36..32fcc55d 100644 --- a/prism/src/explicit/DTMCFromMDPMemorylessAdversary.java +++ b/prism/src/explicit/DTMCFromMDPMemorylessAdversary.java @@ -97,9 +97,9 @@ public class DTMCFromMDPMemorylessAdversary extends DTMCExplicit return mdp.isInitialState(i); } - public boolean isFixedDeadlockState(int i) + public boolean isDeadlockState(int i) { - return mdp.isFixedDeadlockState(i); + return mdp.isDeadlockState(i); } public List getStatesList() @@ -138,20 +138,19 @@ public class DTMCFromMDPMemorylessAdversary extends DTMCExplicit return 1; } - public void checkForDeadlocks() throws PrismException + public void findDeadlocks(boolean fix) throws PrismException { // No deadlocks by definition } - public void checkForDeadlocks(BitSet except) throws PrismException + public void checkForDeadlocks() throws PrismException { // No deadlocks by definition } - public BitSet findDeadlocks(boolean fix) throws PrismException + public void checkForDeadlocks(BitSet except) throws PrismException { // No deadlocks by definition - return new BitSet(); } @Override diff --git a/prism/src/explicit/DTMCSimple.java b/prism/src/explicit/DTMCSimple.java index 12d563f7..f311fc7a 100644 --- a/prism/src/explicit/DTMCSimple.java +++ b/prism/src/explicit/DTMCSimple.java @@ -238,30 +238,24 @@ public class DTMCSimple extends DTMCExplicit implements ModelSimple } @Override - public void checkForDeadlocks(BitSet except) throws PrismException + public void findDeadlocks(boolean fix) throws PrismException { for (int i = 0; i < numStates; i++) { - if (trans.get(i).isEmpty() && (except == null || !except.get(i))) - throw new PrismException("DTMC has a deadlock in state " + i); + if (trans.get(i).isEmpty()) { + addDeadlockState(i); + if (fix) + setProbability(i, i, 1.0); + } } } @Override - public BitSet findDeadlocks(boolean fix) throws PrismException + public void checkForDeadlocks(BitSet except) throws PrismException { - int i; - BitSet deadlocks = new BitSet(); - for (i = 0; i < numStates; i++) { - if (trans.get(i).isEmpty()) - deadlocks.set(i); - } - if (fix) { - for (i = deadlocks.nextSetBit(0); i >= 0; i = deadlocks.nextSetBit(i + 1)) { - setProbability(i, i, 1.0); - addFixedDeadlockState(i); - } + for (int i = 0; i < numStates; i++) { + if (trans.get(i).isEmpty() && (except == null || !except.get(i))) + throw new PrismException("DTMC has a deadlock in state " + i); } - return deadlocks; } // Accessors (for DTMC) diff --git a/prism/src/explicit/DTMCUniformisedSimple.java b/prism/src/explicit/DTMCUniformisedSimple.java index 5e386488..ed941e1c 100644 --- a/prism/src/explicit/DTMCUniformisedSimple.java +++ b/prism/src/explicit/DTMCUniformisedSimple.java @@ -114,9 +114,9 @@ public class DTMCUniformisedSimple extends DTMCExplicit return ctmc.isInitialState(i); } - public boolean isFixedDeadlockState(int i) + public boolean isDeadlockState(int i) { - return ctmc.isFixedDeadlockState(i); + return ctmc.isDeadlockState(i); } public List getStatesList() @@ -158,20 +158,19 @@ public class DTMCUniformisedSimple extends DTMCExplicit return 1; } - public void checkForDeadlocks() throws PrismException + public void findDeadlocks(boolean fix) throws PrismException { // No deadlocks by definition } - public void checkForDeadlocks(BitSet except) throws PrismException + public void checkForDeadlocks() throws PrismException { // No deadlocks by definition } - public BitSet findDeadlocks(boolean fix) throws PrismException + public void checkForDeadlocks(BitSet except) throws PrismException { // No deadlocks by definition - return new BitSet(); } @Override diff --git a/prism/src/explicit/MDPSimple.java b/prism/src/explicit/MDPSimple.java index 13301dba..d1f10130 100644 --- a/prism/src/explicit/MDPSimple.java +++ b/prism/src/explicit/MDPSimple.java @@ -426,33 +426,28 @@ public class MDPSimple extends MDPExplicit implements ModelSimple } @Override - public void checkForDeadlocks(BitSet except) throws PrismException + public void findDeadlocks(boolean fix) throws PrismException { for (int i = 0; i < numStates; i++) { - if (trans.get(i).isEmpty() && (except == null || !except.get(i))) - throw new PrismException("MDP has a deadlock in state " + i); + // Note that no distributions is a deadlock, not an empty distribution + if (trans.get(i).isEmpty()) { + addDeadlockState(i); + if (fix) { + Distribution distr = new Distribution(); + distr.add(i, 1.0); + addChoice(i, distr); + } + } } } @Override - public BitSet findDeadlocks(boolean fix) throws PrismException + public void checkForDeadlocks(BitSet except) throws PrismException { - int i; - BitSet deadlocks = new BitSet(); - for (i = 0; i < numStates; i++) { - // Note that no distributions is a deadlock, not an empty distribution - if (trans.get(i).isEmpty()) - deadlocks.set(i); - } - if (fix) { - for (i = deadlocks.nextSetBit(0); i >= 0; i = deadlocks.nextSetBit(i + 1)) { - Distribution distr = new Distribution(); - distr.add(i, 1.0); - addChoice(i, distr); - addFixedDeadlockState(i); - } + for (int i = 0; i < numStates; i++) { + if (trans.get(i).isEmpty() && (except == null || !except.get(i))) + throw new PrismException("MDP has a deadlock in state " + i); } - return deadlocks; } // Accessors (for MDP) diff --git a/prism/src/explicit/MDPSparse.java b/prism/src/explicit/MDPSparse.java index 8774bc36..b2b9dfd2 100644 --- a/prism/src/explicit/MDPSparse.java +++ b/prism/src/explicit/MDPSparse.java @@ -439,29 +439,26 @@ public class MDPSparse extends MDPExplicit } @Override - public void checkForDeadlocks(BitSet except) throws PrismException + public void findDeadlocks(boolean fix) throws PrismException { for (int i = 0; i < numStates; i++) { - if (getNumChoices(i) == 0 && (except == null || !except.get(i))) - throw new PrismException("MDP has a deadlock in state " + i); + // Note that no distributions is a deadlock, not an empty distribution + if (getNumChoices(i) == 0) { + addDeadlockState(i); + if (fix) { + throw new PrismException("Can't fix deadlocks in an MDPSparse since it cannot be modified after construction"); + } + } } } @Override - public BitSet findDeadlocks(boolean fix) throws PrismException + public void checkForDeadlocks(BitSet except) throws PrismException { - int i; - BitSet deadlocks = new BitSet(); - for (i = 0; i < numStates; i++) { - // Note that no distributions is a deadlock, not an empty distribution - if (getNumChoices(i) == 0) - deadlocks.set(i); - } - if (fix) { - // TODO disallow this call? - throw new RuntimeException("Can't modify this model"); + for (int i = 0; i < numStates; i++) { + if (getNumChoices(i) == 0 && (except == null || !except.get(i))) + throw new PrismException("MDP has a deadlock in state " + i); } - return deadlocks; } // Accessors (for MDP) diff --git a/prism/src/explicit/Model.java b/prism/src/explicit/Model.java index 61878ab1..a1a5cd50 100644 --- a/prism/src/explicit/Model.java +++ b/prism/src/explicit/Model.java @@ -75,11 +75,16 @@ public interface Model public boolean isInitialState(int i); /** - * Check whether a state is a "fixed" deadlock, i.e. a state that was - * originally a deadlock but has been fixed through the addition of a self-loop, - * or a state that is still a deadlock but in a model where this acceptable, e.g. a CTMC. + * Get the number of states that are/were deadlocks. + * (Such states may have been fixed at build-time by adding self-loops) */ - public boolean isFixedDeadlockState(int i); + public int getNumDeadlockStates(); + + /** + * Check whether a state is/was deadlock. + * (Such states may have been fixed at build-time by adding self-loops) + */ + public boolean isDeadlockState(int i); /** * Get access to an (optional) list of states. @@ -121,16 +126,17 @@ public interface Model public int getNumChoices(int s); /** - * Checks for deadlocks and throws an exception if any exist. + * Find all deadlock states and store this information in the model. + * If requested (if fix=true) and if needed (i.e. for DTMCs/CTMCs), + * fix deadlocks by adding self-loops in these states. + * The set of deadlocks (before any possible fixing) can be obtained from {@link #getDeadlocks()}. */ - public void checkForDeadlocks() throws PrismException; + public void findDeadlocks(boolean fix) throws PrismException; /** - * Find all deadlocks and return a BitSet of these states. - * If requested (if fix=true), then add self-loops in these states - * (and update the "fixed" deadlock information). + * Checks for deadlocks and throws an exception if any exist. */ - public BitSet findDeadlocks(boolean fix) throws PrismException; + public void checkForDeadlocks() throws PrismException; /** * Checks for deadlocks and throws an exception if any exist. diff --git a/prism/src/explicit/ModelExplicit.java b/prism/src/explicit/ModelExplicit.java index aeabbedb..12c18f8f 100644 --- a/prism/src/explicit/ModelExplicit.java +++ b/prism/src/explicit/ModelExplicit.java @@ -46,11 +46,10 @@ public abstract class ModelExplicit implements Model // Initial states protected List initialStates; // TODO: should be a (linkedhash?) set really /** - * States with deadlocks that have been "fixed", i.e. a state that was - * originally a deadlock but has been fixed through the addition of a self-loop, - * or a state that is still a deadlock but in a model where this acceptable, e.g. a CTMC. + * States that are/were deadlocks. Where requested and where appropriate (DTMCs/MDPs), + * these states may have been fixed at build time by adding self-loops. */ - protected TreeSet deadlocksFixed; + protected TreeSet deadlocks; // State info (read only, just a pointer) protected List statesList; // Constant info (read only, just a pointer) @@ -99,7 +98,7 @@ public abstract class ModelExplicit implements Model { this.numStates = numStates; initialStates = new ArrayList(); - deadlocksFixed = new TreeSet(); + deadlocks = new TreeSet(); statesList = null; } @@ -112,11 +111,11 @@ public abstract class ModelExplicit implements Model } /** - * Add a state to the list of "fixed" deadlock states. + * Add a state to the list of deadlock states. */ - public void addFixedDeadlockState(int i) + public void addDeadlockState(int i) { - deadlocksFixed.add(i); + deadlocks.add(i); } /** @@ -176,9 +175,15 @@ public abstract class ModelExplicit implements Model } @Override - public boolean isFixedDeadlockState(int i) + public int getNumDeadlockStates() { - return deadlocksFixed.contains(i); + return deadlocks.size(); + } + + @Override + public boolean isDeadlockState(int i) + { + return deadlocks.contains(i); } @Override diff --git a/prism/src/explicit/PrismExplicit.java b/prism/src/explicit/PrismExplicit.java index 8628ca38..b29ba768 100644 --- a/prism/src/explicit/PrismExplicit.java +++ b/prism/src/explicit/PrismExplicit.java @@ -53,7 +53,7 @@ public class PrismExplicit } /** - * Build a model from a PRISM modelling language description, storing it explicitly., + * Build a model from a PRISM modelling language description, storing it explicitly. * It is assumed that all constants in the model file have been defined by now. * @param modulesFile Model to build * @param simEngine PRISM simulator engine (for model exploration) @@ -174,7 +174,7 @@ public class PrismExplicit try { statesList = new StateValues(TypeBool.getInstance(), new Boolean(true), model); } catch (PrismLangException e) { - // Can't go wrong - type always + // Can't go wrong - type always fine } if (exportType != Prism.EXPORT_MATLAB) statesList.print(tmpLog); @@ -253,6 +253,9 @@ public class PrismExplicit StateValues probs = null; PrismLog tmpLog; + if (!(model.getModelType() == ModelType.CTMC || model.getModelType() == ModelType.DTMC)) + throw new PrismException("Steady-state probabilities only computed for DTMCs/CTMCs"); + // no specific states format for MRMC if (exportType == Prism.EXPORT_MRMC) exportType = Prism.EXPORT_PLAIN; // rows format does not apply to states output diff --git a/prism/src/explicit/STPGAbstrSimple.java b/prism/src/explicit/STPGAbstrSimple.java index b11f8a62..a6ea8332 100644 --- a/prism/src/explicit/STPGAbstrSimple.java +++ b/prism/src/explicit/STPGAbstrSimple.java @@ -323,36 +323,31 @@ public class STPGAbstrSimple extends ModelExplicit implements STPG, ModelSimple } @Override - public void checkForDeadlocks(BitSet except) throws PrismException + public void findDeadlocks(boolean fix) throws PrismException { for (int i = 0; i < numStates; i++) { - if (trans.get(i).isEmpty() && (except == null || !except.get(i))) - throw new PrismException("STPG has a deadlock in state " + i); + // Note that no distributions is a deadlock, not an empty distribution + if (trans.get(i).isEmpty()) { + addDeadlockState(i); + if (fix) { + DistributionSet distrs = newDistributionSet(null); + Distribution distr = new Distribution(); + distr.add(i, 1.0); + distrs.add(distr); + addDistributionSet(i, distrs); + } + } } - // TODO: Check for empty distributions sets too? } @Override - public BitSet findDeadlocks(boolean fix) throws PrismException + public void checkForDeadlocks(BitSet except) throws PrismException { - int i; - BitSet deadlocks = new BitSet(); - for (i = 0; i < numStates; i++) { - // Note that no distributions is a deadlock, not an empty distribution - if (trans.get(i).isEmpty()) - deadlocks.set(i); - } - if (fix) { - for (i = deadlocks.nextSetBit(0); i >= 0; i = deadlocks.nextSetBit(i + 1)) { - DistributionSet distrs = newDistributionSet(null); - Distribution distr = new Distribution(); - distr.add(i, 1.0); - distrs.add(distr); - addDistributionSet(i, distrs); - addFixedDeadlockState(i); - } + for (int i = 0; i < numStates; i++) { + if (trans.get(i).isEmpty() && (except == null || !except.get(i))) + throw new PrismException("STPG has a deadlock in state " + i); } - return deadlocks; + // TODO: Check for empty distributions sets too? } @Override diff --git a/prism/src/explicit/StateModelChecker.java b/prism/src/explicit/StateModelChecker.java index 11a1c4f4..378295ba 100644 --- a/prism/src/explicit/StateModelChecker.java +++ b/prism/src/explicit/StateModelChecker.java @@ -343,7 +343,7 @@ public class StateModelChecker int numStates = model.getNumStates(); BitSet bs = new BitSet(numStates); for (i = 0; i < numStates; i++) { - bs.set(i, model.isFixedDeadlockState(i)); + bs.set(i, model.isDeadlockState(i)); } return StateValues.createFromBitSet(bs, model); } else if (expr.getName().equals("init")) { diff --git a/prism/src/prism/ExplicitFiles2MTBDD.java b/prism/src/prism/ExplicitFiles2MTBDD.java index 0e926472..41a0bcfe 100644 --- a/prism/src/prism/ExplicitFiles2MTBDD.java +++ b/prism/src/prism/ExplicitFiles2MTBDD.java @@ -466,7 +466,7 @@ public class ExplicitFiles2MTBDD } // find any deadlocks - model.findDeadlocks(); + model.findDeadlocks(prism.getFixDeadlocks()); // deref spare dds JDD.Deref(moduleIdentities[0]); diff --git a/prism/src/prism/ExplicitModel2MTBDD.java b/prism/src/prism/ExplicitModel2MTBDD.java index 80aaec49..4ebd3da0 100644 --- a/prism/src/prism/ExplicitModel2MTBDD.java +++ b/prism/src/prism/ExplicitModel2MTBDD.java @@ -235,7 +235,7 @@ public class ExplicitModel2MTBDD } // Find any deadlocks - model.findDeadlocks(); + model.findDeadlocks(prism.getFixDeadlocks()); // Deref spare dds if (modelType == ModelType.MDP) { diff --git a/prism/src/prism/LTLModelChecker.java b/prism/src/prism/LTLModelChecker.java index ff671da2..9252f4e3 100644 --- a/prism/src/prism/LTLModelChecker.java +++ b/prism/src/prism/LTLModelChecker.java @@ -293,8 +293,9 @@ public class LTLModelChecker // Do reachability/etc. for the new model modelProd.doReachability(prism.getExtraReachInfo()); modelProd.filterReachableStates(); - modelProd.findDeadlocks(); + modelProd.findDeadlocks(false); if (modelProd.getDeadlockStates().size() > 0) { + // Assuming original model has no deadlocks, neither should product throw new PrismException("Model-DRA product has deadlock states"); } @@ -508,8 +509,9 @@ public class LTLModelChecker // Do reachability/etc. for the new model modelProd.doReachability(prism.getExtraReachInfo()); modelProd.filterReachableStates(); - modelProd.findDeadlocks(); + modelProd.findDeadlocks(false); if (modelProd.getDeadlockStates().size() > 0) { + // Assuming original model has no deadlocks, neither should product throw new PrismException("Model-DRA product has deadlock states"); } diff --git a/prism/src/prism/Model.java b/prism/src/prism/Model.java index 23a9d901..415f2cf1 100644 --- a/prism/src/prism/Model.java +++ b/prism/src/prism/Model.java @@ -57,7 +57,13 @@ public interface Model int convertBddToIndex(JDDNode dd); StateList getReachableStates(); + + /** + * Get a StateList storing the set of states that are/were deadlocks. + * (Such states may have been fixed at build-time by adding self-loops) + */ StateList getDeadlockStates(); + StateList getStartStates(); int getNumRewardStructs(); long getNumStates(); @@ -71,8 +77,13 @@ public interface Model JDDNode getTrans01(); JDDNode getStart(); JDDNode getReach(); + + /** + * Get a BDD storing the set of states that are/were deadlocks. + * (Such states may have been fixed at build-time by adding self-loops) + */ JDDNode getDeadlocks(); - JDDNode getFixedDeadlocks(); + JDDNode getStateRewards(); JDDNode getStateRewards(int i); JDDNode getStateRewards(String s); @@ -108,8 +119,15 @@ public interface Model void setTransActions(JDDNode transActions); // MDPs only void setTransPerAction(JDDNode[] transPerAction); // D/CTMCs only void filterReachableStates(); - void findDeadlocks(); - void fixDeadlocks(); + + /** + * Find all deadlock states and store this information in the model. + * If requested (if fix=true) and if needed (i.e. for DTMCs/CTMCs), + * fix deadlocks by adding self-loops in these states. + * The set of deadlocks (before any possible fixing) can be obtained from {@link #getDeadlocks()}. + */ + void findDeadlocks(boolean fix); + void printTrans(); void printTrans01(); public void printTransInfo(PrismLog log); diff --git a/prism/src/prism/Modules2MTBDD.java b/prism/src/prism/Modules2MTBDD.java index bdcd7014..4abe2ccf 100644 --- a/prism/src/prism/Modules2MTBDD.java +++ b/prism/src/prism/Modules2MTBDD.java @@ -304,8 +304,8 @@ public class Modules2MTBDD // symmetrification if (doSymmetry) doSymmetry(model); - // find any deadlocks - model.findDeadlocks(); + // find/fix any deadlocks + model.findDeadlocks(prism.getFixDeadlocks()); // deref spare dds globalDDRowVars.derefAll(); diff --git a/prism/src/prism/NondetModel.java b/prism/src/prism/NondetModel.java index ea3b827d..0a47db5c 100644 --- a/prism/src/prism/NondetModel.java +++ b/prism/src/prism/NondetModel.java @@ -206,9 +206,8 @@ public class NondetModel extends ProbModel numChoices = ((Math.pow(2, getNumDDNondetVars())) * numStates) - d; } - // identify any deadlock states - - public void findDeadlocks() + @Override + public void findDeadlocks(boolean fix) { // find states with at least one transition JDD.Ref(trans01); @@ -218,22 +217,15 @@ public class NondetModel extends ProbModel // find reachable states with no transitions JDD.Ref(reach); deadlocks = JDD.And(reach, JDD.Not(deadlocks)); - } - - // remove deadlocks by adding self-loops - - public void fixDeadlocks() - { - JDDNode tmp; - double d; - - if (!deadlocks.equals(JDD.ZERO)) { + + if (fix && !deadlocks.equals(JDD.ZERO)) { // remove deadlocks by adding self-loops to trans // (also update transInd (if necessary) at same time) // (note: we don't need to update transActions since // action-less transitions are encoded as 0 anyway) // (note: would need to update transPerAction[0] // but this is not stored for MDPs) + JDDNode tmp; JDD.Ref(deadlocks); tmp = JDD.SetVectorElement(JDD.Constant(0), allDDNondetVars, 0, 1); tmp = JDD.And(tmp, JDD.Identity(allDDRowVars, allDDColVars)); @@ -247,10 +239,6 @@ public class NondetModel extends ProbModel transInd = JDD.Or(transInd, JDD.ThereExists(tmp, allDDColVars)); } JDD.Deref(tmp); - // update lists of deadlocks - JDD.Deref(fixdl); - fixdl = deadlocks; - deadlocks = JDD.Constant(0); // update mask JDD.Deref(nondetMask); JDD.Ref(trans01); @@ -258,7 +246,7 @@ public class NondetModel extends ProbModel nondetMask = JDD.And(JDD.Not(JDD.ThereExists(trans01, allDDColVars)), reach); // update model stats numTransitions = JDD.GetNumMinterms(trans01, getNumDDVarsInTrans()); - d = JDD.GetNumMinterms(nondetMask, getNumDDRowVars() + getNumDDNondetVars()); + double d = JDD.GetNumMinterms(nondetMask, getNumDDRowVars() + getNumDDNondetVars()); numChoices = ((Math.pow(2, getNumDDNondetVars())) * numStates) - d; } } diff --git a/prism/src/prism/NondetModelChecker.java b/prism/src/prism/NondetModelChecker.java index a50986b6..828c3e1b 100644 --- a/prism/src/prism/NondetModelChecker.java +++ b/prism/src/prism/NondetModelChecker.java @@ -440,7 +440,7 @@ public class NondetModelChecker extends NonProbModelChecker if (prism.getExportProductTrans()) { try { mainLog.println("\nExporting product transition matrix to file \"" + prism.getExportProductTransFilename() + "\"..."); - prism.exportTransToFile(modelProduct, true, Prism.EXPORT_PLAIN, new File(prism.getExportProductTransFilename())); + modelProduct.exportToFile(Prism.EXPORT_PLAIN, true, new File(prism.getExportProductTransFilename())); } catch (FileNotFoundException e) { mainLog.printWarning("Could not export product transition matrix to file \"" + prism.getExportProductTransFilename() + "\""); } diff --git a/prism/src/prism/Prism.java b/prism/src/prism/Prism.java index f9cabc4e..d73fd5ff 100644 --- a/prism/src/prism/Prism.java +++ b/prism/src/prism/Prism.java @@ -1,6 +1,5 @@ //============================================================================== // -// Copyright (c) 2002- // Authors: // * Dave Parker (University of Oxford, formerly University of Birmingham) // * Andrew Hinton (University of Birmingham) @@ -39,6 +38,7 @@ import sparse.*; import hybrid.*; import parser.*; import parser.ast.*; +import parser.type.TypeBool; import simulator.*; import simulator.method.SimulationMethod; import pta.*; @@ -64,7 +64,8 @@ public class Prism implements PrismSettingsListener public static final int MTBDD = 1; public static final int SPARSE = 2; public static final int HYBRID = 3; - private static String[] engineStrings = { "?", "MTBDD", "Sparse", "Hybrid" }; + public static final int EXPLICIT = 4; + private static String[] engineStrings = { "?", "MTBDD", "Sparse", "Hybrid", "Explicit" }; // methods for solving linear equation systems public static final int POWER = 1; @@ -115,7 +116,6 @@ public class Prism implements PrismSettingsListener // Main PRISM settings private PrismSettings settings; - // Some additional settings (here because not available from main options panel in GUI) // Export target state info? protected boolean exportTarget; protected String exportTargetFilename; @@ -164,14 +164,35 @@ public class Prism implements PrismSettingsListener private ExplicitModel2MTBDD expm2mtbdd = null; private SimulatorEngine theSimulator = null; + //------------------------------------------------------------------------------ + // Event listeners + //------------------------------------------------------------------------------ + + private List modelListeners; + //------------------------------------------------------------------------------ // State //------------------------------------------------------------------------------ + private enum ModelSource { + PRISM_MODEL, EXPLICIT_FILES, BUILT_MODEL + } + // Info about currently loaded model, if any - private ModulesFile currentModulesFile = null; + // Model source + private ModelSource currentModelSource = ModelSource.PRISM_MODEL; + // Model type private ModelType currentModelType = null; + // PRISM model (null if none loaded, or built model given directly) + private ModulesFile currentModulesFile = null; + // Constants to be defined for PRISM model + private Values currentDefinedMFConstants = null; + // Built model storage - symbolic or explicit - at most one is non-null private Model currentModel = null; + private explicit.Model currentModelExpl = null; + // Are we doing digital clocks translation for PTAs? + boolean digital = false; + // Has the CUDD library been initialised yet? private boolean cuddStarted = false; @@ -203,10 +224,12 @@ public class Prism implements PrismSettingsListener mainLog.printWarning("Failed to create new PRISM settings file."); } } - // add this Prism object as a listener + // add this Prism object as a results listener settings.addSettingsListener(this); + // create list of model listeners + modelListeners = new ArrayList(); - // default values for miscellaneous options + // default values for miscellaneous options exportTarget = false; exportTargetFilename = null; exportProductTrans = false; @@ -283,6 +306,11 @@ public class Prism implements PrismSettingsListener settings.set(PrismSettings.PRISM_PROB1, b); } + public void setFixDeadlocks(boolean b) throws PrismException + { + settings.set(PrismSettings.PRISM_FIX_DEADLOCKS, b); + } + public void setDoProbChecks(boolean b) throws PrismException { settings.set(PrismSettings.PRISM_DO_PROB_CHECKS, b); @@ -475,6 +503,19 @@ public class Prism implements PrismSettingsListener return settings.getInteger(PrismSettings.PRISM_ENGINE) + 1; } //note the correction + /** + * Is the current engine "Explicit"? + */ + public boolean getExplicit() + { + return getEngine() == Prism.EXPLICIT; + } + + public boolean getFixDeadlocks() + { + return settings.getBoolean(PrismSettings.PRISM_FIX_DEADLOCKS); + } + public boolean getDoProbChecks() { return settings.getBoolean(PrismSettings.PRISM_DO_PROB_CHECKS); @@ -662,6 +703,11 @@ public class Prism implements PrismSettingsListener return sumRoundOff; } + public void addModelListener(PrismModelListener listener) + { + modelListeners.add(listener); + } + // String methods for options public static String getEngineString(int engine) @@ -1314,28 +1360,46 @@ public class Prism implements PrismSettingsListener */ public void loadPRISMModel(ModulesFile modulesFile) { + currentModelSource = ModelSource.PRISM_MODEL; // Store PRISM model currentModulesFile = modulesFile; // Reset dependent info currentModelType = currentModulesFile == null ? null : currentModulesFile.getModelType(); + currentDefinedMFConstants = null; currentModel = null; + currentModelExpl = null; + + // Print basic model info + // TODO: move? + mainLog.println("\nType: " + currentModulesFile.getModelType()); + mainLog.print("Modules: "); + for (int i = 0; i < currentModulesFile.getNumModules(); i++) { + mainLog.print(currentModulesFile.getModuleName(i) + " "); + } + mainLog.println(); + mainLog.print("Variables: "); + for (int i = 0; i < currentModulesFile.getNumVars(); i++) { + mainLog.print(currentModulesFile.getVarName(i) + " "); + } + mainLog.println(); } /** - * Set any undefined constants for the currently loaded PRISM model. - * @param modulesFile The PRISM model + * Set any undefined constants for the currently loaded PRISM model + * (assuming they have changed since the last time this was called). + * @param definedMFConstants The constant values */ public void setPRISMModelConstants(Values definedMFConstants) throws PrismLangException { - // If non-null/non-empty, print new model constants to log - if (definedMFConstants != null && definedMFConstants.getNumValues() > 0) - mainLog.println("\nModel constants: " + definedMFConstants); + if (currentDefinedMFConstants != null && currentDefinedMFConstants.equals(definedMFConstants)) + return; - // Set constant values in stored ModulesFile + // Store constants here and in ModulesFile + currentDefinedMFConstants = definedMFConstants; currentModulesFile.setUndefinedConstants(definedMFConstants); - // Reset dependent info currentModel = null; + currentModelExpl = null; } /** @@ -1346,30 +1410,77 @@ public class Prism implements PrismSettingsListener */ public void loadPRISMModelAndBuiltModel(ModulesFile modulesFile, Model model) { + currentModelSource = ModelSource.PRISM_MODEL; // Store model info currentModulesFile = modulesFile; currentModel = model; // Reset dependent info currentModelType = currentModulesFile == null ? null : currentModulesFile.getModelType(); + currentDefinedMFConstants = null; + currentModelExpl = null; } /** * Load a (built) model, without an accompanying (parsed) PRISM model. * The model will be stored and used for subsequent model checking etc. * Pass in null to clear storage of the current model. - * @param modulesFile The PRISM model + * @param model The built model */ public void loadBuiltModel(Model model) { + currentModelSource = ModelSource.BUILT_MODEL; // Store model info currentModulesFile = null; currentModel = model; // Reset dependent info currentModelType = currentModel == null ? null : currentModel.getModelType(); + currentDefinedMFConstants = null; + currentModelExpl = null; + } + + /** + * Load files containing an explicit list of transitions/etc. for subsequent model building. + * A corresponding ModulesFile object is created and returned. + * @param statesFile File containing a list of states (optional, can be null) + * @param transFile File containing the list of transitions (required) + * @param labelsFile File containing label definitions (optional, can be null) + * @param typeOverride Type of model to be built (optional, use null if not required) + */ + public ModulesFile loadModelFromExplicitFiles(File statesFile, File transFile, File labelsFile, ModelType typeOverride) throws PrismException + { + currentModelSource = ModelSource.EXPLICIT_FILES; + // Create ExplicitFiles2MTBDD object and build state space + expf2mtbdd = new ExplicitFiles2MTBDD(this, statesFile, transFile, labelsFile, typeOverride); + currentModulesFile = expf2mtbdd.buildStates(); + // Reset dependent info + currentModelType = currentModulesFile == null ? null : currentModulesFile.getModelType(); + currentDefinedMFConstants = null; + currentModel = null; + currentModelExpl = null; + + return currentModulesFile; + } + + /** + * Get the type of the currently stored model. + * @return + */ + public ModelType getModelType() + { + return currentModelType; + } + + /** + * Get the currently stored (parsed) PRISM model. + * @return + */ + public ModulesFile getPRISMModel() + { + return currentModulesFile; } /** - * Get the currently stored built model. + * Get the currently stored built (symbolic) model. * @return */ public Model getBuiltModel() @@ -1378,104 +1489,173 @@ public class Prism implements PrismSettingsListener } /** - * Print basic info about the currently stored built model (type, modules, variables, etc.) - * See also {@link #printBuiltModelStats()}. + * Get the currently stored built explicit model. + * @return + */ + public explicit.Model getBuiltModelExplicit() + { + return currentModelExpl; + } + + /** + * Returns true if the current model is of a type that can be built (e.g. not a PTA). */ - public void printBuiltModelInfo() + public boolean modelCanBeBuilt() { - int i; - mainLog.println("\nType: " + currentModel.getModelType()); - mainLog.print("Modules: "); - for (i = 0; i < currentModel.getNumModules(); i++) { - mainLog.print(currentModel.getModuleName(i) + " "); - } - mainLog.println(); - mainLog.print("Variables: "); - for (i = 0; i < currentModel.getNumVars(); i++) { - mainLog.print(currentModel.getVarName(i) + " "); - } - mainLog.println(); + if (currentModelType == ModelType.PTA) + return false; + return true; } - + /** - * Print stats for the currently stored built model (number of states, transitions, etc.) + * Returns true if the current model has been built (for the currently selected engine). */ - public void printBuiltModelStats() + public boolean modelIsBuilt() { - currentModel.printTransInfo(mainLog, getExtraDDInfo()); + return (getExplicit() ? (currentModelExpl != null) : (currentModel != null)); } - + /** * Build the currently loaded PRISM model and store for later use. - * The build model can be accessed subsequently via {@link #getBuiltModel()}. - * Reachability and model construction are done symbolically, i.e. using (MT)BDDs. + * The built model can be accessed subsequently via either + * {@link #getBuiltModel()} or {@link #getBuiltModelExplicit()}, + * depending on the engine currently selected. + * Only call this to explicitly force a built; normally it is done automatically. */ public void buildModel() throws PrismException { - long l; // timer - Modules2MTBDD mod2mtbdd = null; - - if (currentModulesFile == null) - throw new PrismException("There is no currently loaded PRISM model to build"); - - if (currentModelType == ModelType.PTA) { - throw new PrismException("You cannot build a PTA model explicitly, only perform model checking"); - } - - mainLog.print("\nBuilding model...\n"); - - // create translator - mod2mtbdd = new Modules2MTBDD(this, currentModulesFile); - - // build model - l = System.currentTimeMillis(); - currentModel = mod2mtbdd.translate(); - l = System.currentTimeMillis() - l; - - mainLog.println("\nTime for model construction: " + l / 1000.0 + " seconds."); + mainLog.printSeparator(); + doBuildModel(); } /** - * Builds a ModulesFile from files containing an explicit list of transitions/etc. - * This is step 1 of the process; {@link #buildExplicitModel} should be called subsequently. - * @param statesFile File containing a list of states (optional, can be null) - * @param transFile File containing the list of transitions (required) - * @param labelsFile File containing label definitions (optional, can be null) - * @param typeOverride Type of model to be built (optional, use null if not required) - * @throws PrismException + * Build the currently loaded PRISM model, if it needs to be done, + * i.e. if it has not been constructed yet for the current engine. */ - public ModulesFile parseModelFromExplicitFiles(File statesFile, File transFile, File labelsFile, ModelType typeOverride) throws PrismException + public void buildModelIfRequired() throws PrismException { - // create ExplicitFiles2MTBDD object - expf2mtbdd = new ExplicitFiles2MTBDD(this, statesFile, transFile, labelsFile, typeOverride); - - // build state space - return expf2mtbdd.buildStates(); + if (!modelIsBuilt()) + doBuildModel(); } /** - * Builds a model from files containing an explicit list of transitions/etc. - * This is step 2 of the process; {@link #parseExplicitModel} should have been called first. + * Build the currently loaded PRISM model and store for later use. + * The built model can be accessed subsequently via either + * {@link #getBuiltModel()} or {@link #getBuiltModelExplicit()}, + * depending on the engine currently selected. */ - public Model buildModelFromExplicitFiles() throws PrismException + private void doBuildModel() throws PrismException { long l; // timer - Model model; - // check ExplicitFiles2MTBDD object created - if (expf2mtbdd == null) - throw new PrismException("ExplicitFiles2MTBDD object never created"); + try { + if (currentModulesFile == null) + throw new PrismException("There is no currently loaded PRISM model to build"); - mainLog.print("\nBuilding model...\n"); + if (currentModelType == ModelType.PTA) { + throw new PrismException("You cannot build a PTA model explicitly, only perform model checking"); + } - // build model - l = System.currentTimeMillis(); - model = expf2mtbdd.buildModel(); - l = System.currentTimeMillis() - l; + mainLog.print("\nBuilding model...\n"); + if (currentDefinedMFConstants != null && currentDefinedMFConstants.getNumValues() > 0) + mainLog.println("Model constants: " + currentDefinedMFConstants); + + // Build model + l = System.currentTimeMillis(); + switch (currentModelSource) { + case PRISM_MODEL: + if (!getExplicit()) { + Modules2MTBDD mod2mtbdd = new Modules2MTBDD(this, currentModulesFile); + currentModel = mod2mtbdd.translate(); + currentModelExpl = null; + } else { + ConstructModel constructModel = new ConstructModel(getSimulator(), mainLog); + constructModel.setFixDeadlocks(getFixDeadlocks()); + currentModelExpl = constructModel.constructModel(currentModulesFile, false, true); + currentModel = null; + } + // if (...) ... currentModel = buildModelExplicit(currentModulesFile); + break; + case EXPLICIT_FILES: + if (!getExplicit()) { + // check ExplicitFiles2MTBDD object created + if (expf2mtbdd == null) + throw new PrismException("ExplicitFiles2MTBDD object never created"); + currentModel = expf2mtbdd.buildModel(); + } else { + // TODO: add using model.buildFromPrismExplicit(...); + throw new PrismException("Explicit import not yet supported for explicit engine"); + } + break; + default: + throw new PrismException("Don't know how to build model from source " + currentModelSource); + } + l = System.currentTimeMillis() - l; + mainLog.println("\nTime for model construction: " + l / 1000.0 + " seconds."); + + // Deal with deadlocks + if (!getExplicit()) { + StateList deadlocks = currentModel.getDeadlockStates(); + if (deadlocks.size() > 0) { + if (digital) { + // For digital clocks, by construction, deadlocks can only occur from timelocks (and are not allowed) + throw new PrismException("Timelock in PTA, e.g. in state (" + deadlocks.getFirstAsValues() + ")"); + } + if (getFixDeadlocks()) { + mainLog.printWarning("Deadlocks detected and fixed in " + deadlocks.size() + " states"); + } else { + currentModel.printTransInfo(mainLog, getExtraDDInfo()); + mainLog.print("\n" + deadlocks.size() + " deadlock states found"); + if (!getVerbose() && deadlocks.size() > 10) { + mainLog.print(". The first 10 are below. Use verbose mode to view them all.\n"); + deadlocks.print(mainLog, 10); + } else { + mainLog.print(":\n"); + deadlocks.print(mainLog); + } + mainLog.print("\nTip: Use the \"fix deadlocks\" option to automatically add self-loops in deadlock states.\n"); + throw new PrismException("Model contains " + deadlocks.size() + " deadlock states"); + } + } + } else { + if (currentModelExpl.getNumDeadlockStates() > 0) { + if (digital) { + // For digital clocks, by construction, deadlocks can only occur from timelocks (and are not allowed) + throw new PrismException("Timelock in PTA"); + // TODO: find states, like for symbolic engines + } + if (getFixDeadlocks()) { + mainLog.printWarning("Deadlocks detected and fixed in " + currentModelExpl.getNumDeadlockStates() + " states"); + } else { + throw new PrismException("Model contains " + currentModelExpl.getNumDeadlockStates() + " deadlock states"); + } + } + } - mainLog.println("\nTime for model construction: " + l / 1000.0 + " seconds."); + // Print model stats + mainLog.println(); + if (!getExplicit()) { + mainLog.println("Type: " + currentModel.getModelType()); + currentModel.printTransInfo(mainLog, getExtraDDInfo()); + } else { + mainLog.println("Type: " + currentModelExpl.getModelType()); + mainLog.print(currentModelExpl.infoStringTable()); + } - return model; + // Notify model listeners of build success + for (PrismModelListener listener : modelListeners) { + if (listener != null) + listener.notifyModelBuildSuccessful(); + } + } catch (PrismException e) { + // Notify model listeners of build failure + for (PrismModelListener listener : modelListeners) { + if (listener != null) + listener.notifyModelBuildFailed(e); + } + // Throw exception anyway + throw e; + } } /** @@ -1497,6 +1677,8 @@ public class Prism implements PrismSettingsListener } mainLog.print("\nBuilding model...\n"); + if (currentDefinedMFConstants != null && currentDefinedMFConstants.getNumValues() > 0) + mainLog.println("Model constants: " + currentDefinedMFConstants); constructModel = new ConstructModel(getSimulator(), mainLog); modelExpl = constructModel.constructModel(modulesFile); @@ -1515,6 +1697,35 @@ public class Prism implements PrismSettingsListener return model; } + /** + * Export the currently loaded and parsed PRISM model to a file. + * @param file File to export to + */ + public void exportPRISMModel(File file) throws FileNotFoundException, PrismException + { + mainLog.print("\nExporting parsed PRISM file "); + mainLog.println(getDestinationStringForFile(file)); + PrismLog tmpLog = getPrismLogForFile(file); + tmpLog.print(currentModulesFile.toString()); + } + + /** + * Export the currently loaded and parsed PRISM model to a file, + * after expanding all constants to their actual, defined values. + * @param file File to export to + */ + public void exportPRISMModelWithExpandedConstants(File file) throws FileNotFoundException, PrismException + { + mainLog.print("\nExporting parsed PRISM file (with constant expansion) "); + mainLog.println(getDestinationStringForFile(file)); + PrismLog tmpLog = getPrismLogForFile(file); + ModulesFile mfTmp = (ModulesFile) currentModulesFile.deepCopy(); + mfTmp = (ModulesFile) mfTmp.replaceConstants(currentModulesFile.getConstantValues()); + // NB: Don't use simplify() here because doesn't work for the purposes of printing out + // (e.g. loss of parentheses causes precedence problems) + tmpLog.print(mfTmp.toString()); + } + /** * Export the currently loaded model's transition matrix to a Spy file. * @param file File to export to @@ -1524,9 +1735,11 @@ public class Prism implements PrismSettingsListener int depth; JDDNode tmp; + if (getExplicit()) + throw new PrismException("Export to Spy file not yet supported by explicit engine"); + // Build model, if necessary - if (currentModel == null) - buildModel(currentModulesFile); + buildModelIfRequired(); mainLog.println("\nExporting to spy file \"" + file + "\"..."); @@ -1553,9 +1766,11 @@ public class Prism implements PrismSettingsListener */ public void exportToDotFile(File file) throws FileNotFoundException, PrismException { + if (getExplicit()) + throw new PrismException("Export to Dot file not yet supported by explicit engine"); + // Build model, if necessary - if (currentModel == null) - buildModel(currentModulesFile); + buildModelIfRequired(); mainLog.println("\nExporting to dot file \"" + file + "\"..."); @@ -1598,8 +1813,7 @@ public class Prism implements PrismSettingsListener } // Build model, if necessary - if (currentModel == null) - buildModel(currentModulesFile); + buildModelIfRequired(); // print message mainLog.print("\nExporting transition matrix "); @@ -1623,26 +1837,30 @@ public class Prism implements PrismSettingsListener mainLog.print("in Dot format (with states) "); break; } - if (file != null) - mainLog.println("to file \"" + file + "\"..."); - else - mainLog.println("below:"); + mainLog.println(getDestinationStringForFile(file)); // do export - currentModel.exportToFile(exportType, ordered, file); + if (!getExplicit()) { + currentModel.exportToFile(exportType, ordered, file); + } else { + PrismLog tmpLog = getPrismLogForFile(file); + switch (exportType) { + case Prism.EXPORT_PLAIN: + currentModelExpl.exportToPrismExplicitTra(tmpLog); + break; + case Prism.EXPORT_MATLAB: + case Prism.EXPORT_DOT: + case Prism.EXPORT_MRMC: + case Prism.EXPORT_ROWS: + case Prism.EXPORT_DOT_STATES: + throw new PrismException("Export not yet supported"); // TODO + } + } // for export to dot with states, need to do a bit more - if (exportType == EXPORT_DOT_STATES) { + if (!getExplicit() && exportType == EXPORT_DOT_STATES) { // open (appending to) existing new file log or use main log - PrismLog tmpLog; - if (file != null) { - tmpLog = new PrismFileLog(file.getPath(), true); - if (!tmpLog.ready()) { - throw new FileNotFoundException(); - } - } else { - tmpLog = mainLog; - } + PrismLog tmpLog = getPrismLogForFile(file, true); // insert states info into dot file currentModel.getReachableStates().printDot(tmpLog); // print footer @@ -1666,13 +1884,15 @@ public class Prism implements PrismSettingsListener { String s; + if (getExplicit()) + throw new PrismException("Export of state rewards not yet supported by explicit engine"); + // rows format does not apply to vectors if (exportType == EXPORT_ROWS) exportType = EXPORT_PLAIN; // Build model, if necessary - if (currentModel == null) - buildModel(currentModulesFile); + buildModelIfRequired(); // print message mainLog.print("\nExporting state rewards vector "); @@ -1687,10 +1907,7 @@ public class Prism implements PrismSettingsListener mainLog.print("in MRMC format "); break; } - if (file != null) - mainLog.println("to file \"" + file + "\"..."); - else - mainLog.println("below:"); + mainLog.println(getDestinationStringForFile(file)); // do export s = currentModel.exportStateRewardsToFile(exportType, file); @@ -1713,6 +1930,9 @@ public class Prism implements PrismSettingsListener { String s; + if (getExplicit()) + throw new PrismException("Export of transition rewards not yet supported by explicit engine"); + // can only do ordered version of export for MDPs if (currentModelType == ModelType.MDP) { if (!ordered) @@ -1733,8 +1953,7 @@ public class Prism implements PrismSettingsListener } // Build model, if necessary - if (currentModel == null) - buildModel(currentModulesFile); + buildModelIfRequired(); // print message mainLog.print("\nExporting transition rewards matrix "); @@ -1752,10 +1971,7 @@ public class Prism implements PrismSettingsListener mainLog.print("in rows format "); break; } - if (file != null) - mainLog.println("to file \"" + file + "\"..."); - else - mainLog.println("below:"); + mainLog.println(getDestinationStringForFile(file)); // do export s = currentModel.exportTransRewardsToFile(exportType, ordered, file); @@ -1780,6 +1996,9 @@ public class Prism implements PrismSettingsListener Vector bsccs; JDDNode not, bscc; + if (getExplicit()) + throw new PrismException("Export of BSCCs not yet supported by explicit engine"); + // no specific states format for MRMC if (exportType == EXPORT_MRMC) exportType = EXPORT_PLAIN; @@ -1788,8 +2007,7 @@ public class Prism implements PrismSettingsListener exportType = EXPORT_PLAIN; // Build model, if necessary - if (currentModel == null) - buildModel(currentModulesFile); + buildModelIfRequired(); // Compute BSCCs mainLog.println("\nComputing BSCCs..."); @@ -1811,20 +2029,10 @@ public class Prism implements PrismSettingsListener mainLog.print("in Matlab format "); break; } - if (file != null) - mainLog.println("to file \"" + file + "\"..."); - else - mainLog.println("below:"); + mainLog.println(getDestinationStringForFile(file)); // create new file log or use main log - if (file != null) { - tmpLog = new PrismFileLog(file.getPath()); - if (!tmpLog.ready()) { - throw new FileNotFoundException(); - } - } else { - tmpLog = mainLog; - } + tmpLog = getPrismLogForFile(file); // print header: list of model vars if (exportType == EXPORT_MATLAB) @@ -1878,10 +2086,13 @@ public class Prism implements PrismSettingsListener int i, n; LabelList ll; Expression expr; - StateModelChecker mc = null; + prism.StateModelChecker mc = null; JDDNode dd, labels[]; String labelNames[]; + if (getExplicit()) + throw new PrismException("Export of labels not yet supported by explicit engine"); + // get label list and size if (propertiesFile == null) { ll = currentModulesFile.getLabelList(); @@ -1892,23 +2103,19 @@ public class Prism implements PrismSettingsListener } // Build model, if necessary - if (currentModel == null) - buildModel(currentModulesFile); + buildModelIfRequired(); // print message mainLog.print("\nExporting labels and satisfying states "); - if (file != null) - mainLog.println("to file \"" + file + "\"..."); - else - mainLog.println("below:"); + mainLog.println(getDestinationStringForFile(file)); // convert labels to bdds if (n > 0) { - mc = new StateModelChecker(this, currentModel, propertiesFile); + mc = new prism.StateModelChecker(this, currentModel, propertiesFile); } labels = new JDDNode[n + 2]; labels[0] = currentModel.getStart(); - labels[1] = currentModel.getFixedDeadlocks(); + labels[1] = currentModel.getDeadlocks(); for (i = 0; i < n; i++) { expr = ll.getLabel(i); dd = mc.checkExpressionDD(expr); @@ -1953,8 +2160,7 @@ public class Prism implements PrismSettingsListener exportType = EXPORT_PLAIN; // Build model, if necessary - if (currentModel == null) - buildModel(currentModulesFile); + buildModelIfRequired(); // print message mainLog.print("\nExporting list of reachable states "); @@ -1966,28 +2172,18 @@ public class Prism implements PrismSettingsListener mainLog.print("in Matlab format "); break; } - if (file != null) - mainLog.println("to file \"" + file + "\"..."); - else - mainLog.println("below:"); + mainLog.println(getDestinationStringForFile(file)); // create new file log or use main log - if (file != null) { - tmpLog = new PrismFileLog(file.getPath()); - if (!tmpLog.ready()) { - throw new FileNotFoundException(); - } - } else { - tmpLog = mainLog; - } + tmpLog = getPrismLogForFile(file); // print header: list of model vars if (exportType == EXPORT_MATLAB) tmpLog.print("% "); tmpLog.print("("); - for (i = 0; i < currentModel.getNumVars(); i++) { - tmpLog.print(currentModel.getVarName(i)); - if (i < currentModel.getNumVars() - 1) + for (i = 0; i < currentModulesFile.getNumVars(); i++) { + tmpLog.print(currentModulesFile.getVarName(i)); + if (i < currentModulesFile.getNumVars() - 1) tmpLog.print(","); } tmpLog.println(")"); @@ -1995,10 +2191,23 @@ public class Prism implements PrismSettingsListener tmpLog.println("states=["); // print states - if (exportType != EXPORT_MATLAB) - currentModel.getReachableStates().print(tmpLog); - else - currentModel.getReachableStates().printMatlab(tmpLog); + if (!getExplicit()) { + if (exportType != EXPORT_MATLAB) + currentModel.getReachableStates().print(tmpLog); + else + currentModel.getReachableStates().printMatlab(tmpLog); + } else { + explicit.StateValues statesList = null; + try { + statesList = new explicit.StateValues(TypeBool.getInstance(), new Boolean(true), currentModelExpl); + } catch (PrismLangException e) { + // Can't go wrong - type always fine + } + if (exportType != Prism.EXPORT_MATLAB) + statesList.print(tmpLog); + else + statesList.print(tmpLog, true, true, true, true); + } // print footer if (exportType == EXPORT_MATLAB) @@ -2013,60 +2222,118 @@ public class Prism implements PrismSettingsListener * Perform model checking of a property on the currently loaded model and return result. * @param propertiesFile Parent property file of property (for labels/constants/...) * @param expr The property to check + * @param definedPFConstants Optional values info for properties file (to display in log) */ - public Result modelCheck(PropertiesFile propertiesFile, Expression expr) throws PrismException, PrismLangException + public Result modelCheck(PropertiesFile propertiesFile, Expression expr, Values definedPFConstants) throws PrismException, PrismLangException { - ModelChecker mc = null; - Result res; + Result res = null; + + if (!digital) // TODO: if "non-nested" + mainLog.printSeparator(); + mainLog.println("\nModel checking: " + expr); + if (currentDefinedMFConstants != null && currentDefinedMFConstants.getNumValues() > 0) + mainLog.println("Model constants: " + currentDefinedMFConstants); + if (definedPFConstants != null && definedPFConstants.getNumValues() > 0) + mainLog.println("Property constants: " + definedPFConstants); // Check that property is valid for the current model type expr.checkValid(currentModelType); - // Build model, if necessary - if (currentModel == null) - buildModel(currentModulesFile); - - // Create new model checker object - switch (currentModelType) { - case DTMC: - mc = new ProbModelChecker(this, currentModel, propertiesFile); - break; - case MDP: - mc = new NondetModelChecker(this, currentModel, propertiesFile); - break; - case CTMC: - mc = new StochModelChecker(this, currentModel, propertiesFile); - break; - default: - throw new PrismException("Unknown model type " + currentModelType); + // For PTAs... + if (currentModelType == ModelType.PTA) { + return modelCheckPTA(propertiesFile, expr, definedPFConstants); } - // Do model checking - res = mc.check(expr); + // Build model, if necessary + buildModelIfRequired(); + + // Create new model checker object and do model checking + if (!getExplicit()) { + ModelChecker mc = null; + switch (currentModelType) { + case DTMC: + mc = new ProbModelChecker(this, currentModel, propertiesFile); + break; + case MDP: + mc = new NondetModelChecker(this, currentModel, propertiesFile); + break; + case CTMC: + mc = new StochModelChecker(this, currentModel, propertiesFile); + break; + default: + throw new PrismException("Unknown model type " + currentModelType); + } + res = mc.check(expr); + } else { + explicit.StateModelChecker mc = null; + switch (currentModelType) { + case DTMC: + mc = new DTMCModelChecker(); + break; + case MDP: + mc = new MDPModelChecker(); + break; + case CTMC: + mc = new CTMCModelChecker(); + break; + case CTMDP: + mc = new CTMDPModelChecker(); + break; + case STPG: + mc = new STPGModelChecker(); + break; + default: + throw new PrismException("Unknown model type " + currentModelType); + } + mc.setLog(mainLog); + mc.setSettings(settings); + mc.setModulesFileAndPropertiesFile(currentModulesFile, propertiesFile); + res = mc.check(currentModelExpl, expr); + } // Return result return res; } /** - * Perform model checking of a property on a PTA model and return result. - * @param modulesFile The PTA model (language-level) + * Perform model checking of a property on the currently loaded PTA PRISM model and return result. * @param propertiesFile Parent property file of property (for labels/constants/...) - * @param expr The property + * @param expr The property to check + * @param definedPFConstants Optional values info for properties file (to display in log) */ - public Result modelCheckPTA(ModulesFile modulesFile, PropertiesFile propertiesFile, Expression expr) throws PrismException, PrismLangException + public Result modelCheckPTA(PropertiesFile propertiesFile, Expression expr, Values definedPFConstants) throws PrismException, PrismLangException { - PTAModelChecker mcPta; - Result res; - // Check that property is valid for this model type // and create new model checker object - expr.checkValid(modulesFile.getModelType()); - mcPta = new PTAModelChecker(this, modulesFile, propertiesFile); - // Do model checking - res = mcPta.check(expr); + expr.checkValid(currentModelType); - return res; + // Digital clocks translation + if (settings.getString(PrismSettings.PRISM_PTA_METHOD).equals("Digital clocks")) { + digital = true; + ModulesFile oldModulesFile = currentModulesFile; + try { + DigitalClocks dc = new DigitalClocks(this); + dc.translate(oldModulesFile, propertiesFile, expr); + currentModulesFile = dc.getNewModulesFile(); + currentModulesFile.setUndefinedConstants(oldModulesFile.getConstantValues()); + currentModelType = ModelType.MDP; + /*if (exportprism) { + + }*/ + // TODO doPrismLangExports(modulesFileToCheck); + return modelCheck(propertiesFile, expr, definedPFConstants); + } finally { + digital = false; + currentModulesFile = oldModulesFile; + currentModelType = ModelType.PTA; + } + } + // Other methods + else { + PTAModelChecker mcPta; + mcPta = new PTAModelChecker(this, currentModulesFile, propertiesFile); + return mcPta.check(expr); + } } /** @@ -2080,57 +2347,79 @@ public class Prism implements PrismSettingsListener } /** - * Perform approximate model checking of a property on a model, using the simulator. + * Perform approximate model checking of a property on the currently loaded model, using the simulator. * Sampling starts from the initial state provided or, if null, the default * initial state is used, selecting randomly (each time) if there are more than one. * Returns a Result object, except in case of error, where an Exception is thrown. * Note: All constants in the model/property files must have already been defined. - * @param modulesFile Model for simulation, constants defined - * @param propertiesFile Properties file containing property to check, constants defined + * @param propertiesFile Parent property file of property (for labels/constants/...) * @param expr The property to check + * @param definedPFConstants Optional values info for properties file (to display in log) * @param initialState Initial state (if null, use default, selecting randomly if needed) * @param maxPathLength The maximum path length for sampling * @param simMethod Object specifying details of method to use for simulation */ - public Result modelCheckSimulator(ModulesFile modulesFile, PropertiesFile propertiesFile, Expression expr, State initialState, int maxPathLength, + public Result modelCheckSimulator(PropertiesFile propertiesFile, Expression expr, Values definedPFConstants, State initialState, int maxPathLength, SimulationMethod simMethod) throws PrismException { Object res = null; + mainLog.printSeparator(); + mainLog.println("\nSimulating: " + expr); + if (currentDefinedMFConstants != null && currentDefinedMFConstants.getNumValues() > 0) + mainLog.println("Model constants: " + currentDefinedMFConstants); + if (definedPFConstants != null && definedPFConstants.getNumValues() > 0) + mainLog.println("Property constants: " + definedPFConstants); + // Check that property is valid for this model type - expr.checkValid(modulesFile.getModelType()); + expr.checkValid(currentModelType); // Do model checking - res = getSimulator().modelCheckSingleProperty(modulesFile, propertiesFile, expr, initialState, maxPathLength, simMethod); + res = getSimulator().modelCheckSingleProperty(currentModulesFile, propertiesFile, expr, initialState, maxPathLength, simMethod); return new Result(res); } /** - * Perform approximate model checking of several properties (simultaneously) on a model, using the simulator. + * Perform approximate model checking of several properties (simultaneously) on the currently loaded model, using the simulator. * Sampling starts from the initial state provided or, if null, the default * initial state is used, selecting randomly (each time) if there are more than one. * Returns an array of results, some of which may be Exception objects if there were errors. * In the case of an error which affects all properties, an exception is thrown. * Note: All constants in the model/property files must have already been defined. - * @param modulesFile Model for simulation, constants defined - * @param propertiesFile Properties file containing properties to check, constants defined + * @param propertiesFile Parent property file of property (for labels/constants/...) * @param exprs The properties to check + * @param definedPFConstants Optional values info for properties file (to display in log) * @param initialState Initial state (if null, use default, selecting randomly if needed) * @param maxPathLength The maximum path length for sampling * @param simMethod Object specifying details of method to use for simulation */ - public Result[] modelCheckSimulatorSimultaneously(ModulesFile modulesFile, PropertiesFile propertiesFile, List exprs, State initialState, + public Result[] modelCheckSimulatorSimultaneously(PropertiesFile propertiesFile, List exprs, Values definedPFConstants, State initialState, int maxPathLength, SimulationMethod simMethod) throws PrismException { Object[] res = null; + mainLog.printSeparator(); + mainLog.print("\nSimulating"); + if (exprs.size() == 1) { + mainLog.println(": " + exprs.get(0)); + } else { + mainLog.println(" " + exprs.size() + " properties:"); + for (int i = 0; i < exprs.size(); i++) { + mainLog.println(" " + exprs.get(i)); + } + } + if (currentDefinedMFConstants != null && currentDefinedMFConstants.getNumValues() > 0) + mainLog.println("Model constants: " + currentDefinedMFConstants); + if (definedPFConstants != null && definedPFConstants.getNumValues() > 0) + mainLog.println("Property constants: " + definedPFConstants); + // Check that properties are valid for this model type for (Expression expr : exprs) - expr.checkValid(modulesFile.getModelType()); + expr.checkValid(currentModelType); // Do model checking - res = getSimulator().modelCheckMultipleProperties(modulesFile, propertiesFile, exprs, initialState, maxPathLength, simMethod); + res = getSimulator().modelCheckMultipleProperties(currentModulesFile, propertiesFile, exprs, initialState, maxPathLength, simMethod); Result[] resArray = new Result[res.length]; for (int i = 0; i < res.length; i++) @@ -2139,8 +2428,7 @@ public class Prism implements PrismSettingsListener } /** - * Perform an approximate model checking experiment on a model, using the simulator. - * Perform an approximate model checking experiment on a model, using the simulator + * Perform an approximate model checking experiment on the currently loaded model, using the simulator. * (specified by values for undefined constants from the property only). * Sampling starts from the initial state provided or, if null, the default * initial state is used, selecting randomly (each time) if there are more than one. @@ -2148,7 +2436,6 @@ public class Prism implements PrismSettingsListener * some of which may be Exception objects if there were errors. * In the case of an error which affects all properties, an exception is thrown. * Note: All constants in the model file must have already been defined. - * @param modulesFile Model for simulation, constants defined * @param propertiesFile Properties file containing property to check, constants defined * @param undefinedConstants Details of constant ranges defining the experiment * @param resultsCollection Where to store the results @@ -2159,11 +2446,11 @@ public class Prism implements PrismSettingsListener * @throws PrismException if something goes wrong with the sampling algorithm * @throws InterruptedException if the thread is interrupted */ - public void modelCheckSimulatorExperiment(ModulesFile modulesFile, PropertiesFile propertiesFile, UndefinedConstants undefinedConstants, - ResultsCollection results, Expression propertyToCheck, State initialState, int pathLength, SimulationMethod simMethod) throws PrismException, - InterruptedException + public void modelCheckSimulatorExperiment(PropertiesFile propertiesFile, UndefinedConstants undefinedConstants, ResultsCollection results, + Expression propertyToCheck, State initialState, int pathLength, SimulationMethod simMethod) throws PrismException, InterruptedException { - getSimulator().modelCheckExperiment(modulesFile, propertiesFile, undefinedConstants, results, propertyToCheck, initialState, pathLength, simMethod); + getSimulator().modelCheckExperiment(currentModulesFile, propertiesFile, undefinedConstants, results, propertyToCheck, initialState, pathLength, + simMethod); } /** @@ -2193,22 +2480,26 @@ public class Prism implements PrismSettingsListener * Output probability distribution to a file (or, if file is null, to log). * The exportType should be EXPORT_PLAIN or EXPORT_MATLAB. */ - public void doSteadyState(int exportType, File fileOut) throws PrismException + public void doSteadyState(int exportType, File file) throws PrismException { long l = 0; // timer ModelChecker mc = null; StateValues probs = null; + explicit.StateValues probsExpl = null; PrismLog tmpLog; if (!(currentModelType == ModelType.CTMC || currentModelType == ModelType.DTMC)) throw new PrismException("Steady-state probabilities only computed for DTMCs/CTMCs"); - if (fileOut != null && getEngine() == MTBDD) - throw new PrismException("Steady-state probability export only supported for sparse/hybrid engines"); + if (file != null && getEngine() == MTBDD) + throw new PrismException("Steady-state probability export not supported for MTBDD engine"); + // TODO: auto-switch? + + mainLog.printSeparator(); + mainLog.println("\nComputing steady-state probabilities..."); // Build model, if necessary - if (currentModel == null) - buildModel(currentModulesFile); + buildModelIfRequired(); // no specific states format for MRMC if (exportType == EXPORT_MRMC) @@ -2217,17 +2508,29 @@ public class Prism implements PrismSettingsListener if (exportType == EXPORT_ROWS) exportType = EXPORT_PLAIN; - mainLog.println("\nComputing steady-state probabilities..."); l = System.currentTimeMillis(); - if (currentModel.getModelType() == ModelType.DTMC) { - mc = new ProbModelChecker(this, currentModel, null); - probs = ((ProbModelChecker) mc).doSteadyState(); - } else if (currentModel.getModelType() == ModelType.CTMC) { - mc = new StochModelChecker(this, currentModel, null); - probs = ((StochModelChecker) mc).doSteadyState(); + if (!getExplicit()) { + if (currentModel.getModelType() == ModelType.DTMC) { + mc = new ProbModelChecker(this, currentModel, null); + probs = ((ProbModelChecker) mc).doSteadyState(); + } else if (currentModel.getModelType() == ModelType.CTMC) { + mc = new StochModelChecker(this, currentModel, null); + probs = ((StochModelChecker) mc).doSteadyState(); + } else { + throw new PrismException("Steady-state probabilities only computed for DTMCs/CTMCs"); + } } else { - throw new PrismException("Steady-state probabilities only computed for DTMCs/CTMCs"); + if (currentModelExpl.getModelType() == ModelType.DTMC) { + DTMCModelChecker mcDTMC = new DTMCModelChecker(); + mcDTMC.setLog(mainLog); + mcDTMC.setSettings(settings); + probsExpl = mcDTMC.doSteadyState((DTMC) currentModelExpl, null); + } else if (currentModelType == ModelType.CTMC) { + throw new PrismException("Not implemented yet"); // TODO + } else { + throw new PrismException("Steady-state probabilities only computed for DTMCs/CTMCs"); + } } l = System.currentTimeMillis() - l; @@ -2242,30 +2545,26 @@ public class Prism implements PrismSettingsListener mainLog.print("in Matlab format "); break; } - if (fileOut != null) - mainLog.println("to file \"" + fileOut + "\"..."); - else - mainLog.println("below:"); + mainLog.println(getDestinationStringForFile(file)); // create new file log or use main log - if (fileOut != null) { - tmpLog = new PrismFileLog(fileOut.getPath()); - if (!tmpLog.ready()) { - throw new PrismException("Could not open file \"" + fileOut + "\" for output"); - } - } else { - tmpLog = mainLog; - } + tmpLog = getPrismLogForFile(file); // print out or export probabilities - probs.print(tmpLog, fileOut == null, exportType == EXPORT_MATLAB, fileOut == null); + if (!getExplicit()) + probs.print(tmpLog, file == null, exportType == EXPORT_MATLAB, file == null); + else + probsExpl.print(tmpLog, file == null, exportType == EXPORT_MATLAB, file == null, true); // print out computation time mainLog.println("\nTime for steady-state probability computation: " + l / 1000.0 + " seconds."); // tidy up - probs.clear(); - if (fileOut != null) + if (!getExplicit()) + probs.clear(); + else + probsExpl.clear(); + if (file != null) tmpLog.close(); } @@ -2284,11 +2583,12 @@ public class Prism implements PrismSettingsListener * The exportType should be EXPORT_PLAIN or EXPORT_MATLAB. * Optionally (if non-null), read in the initial probability distribution from a file. */ - public void doTransient(double time, int exportType, File fileOut, File fileIn) throws PrismException + public void doTransient(double time, int exportType, File file, File fileIn) throws PrismException { long l = 0; // timer ModelChecker mc = null; StateValues probs = null; + explicit.StateValues probsExpl = null; PrismLog tmpLog; if (!(currentModelType == ModelType.CTMC || currentModelType == ModelType.DTMC)) @@ -2297,12 +2597,18 @@ public class Prism implements PrismSettingsListener if (time < 0) throw new PrismException("Cannot compute transient probabilities for negative time value"); - if (fileOut != null && getEngine() == MTBDD) + if (file != null && getEngine() == MTBDD) throw new PrismException("Transient probability export only supported for sparse/hybrid engines"); + mainLog.printSeparator(); + if (currentModelType.continuousTime()) { + mainLog.println("\nComputing transient probabilities (time = " + time + ")..."); + } else { + mainLog.println("\nComputing transient probabilities (time = " + (int) time + ")..."); + } + // Build model, if necessary - if (currentModel == null) - buildModel(currentModulesFile); + buildModelIfRequired(); // no specific states format for MRMC if (exportType == EXPORT_MRMC) @@ -2313,14 +2619,25 @@ public class Prism implements PrismSettingsListener l = System.currentTimeMillis(); - if (currentModelType == ModelType.DTMC) { - mainLog.println("\nComputing transient probabilities (time = " + (int) time + ")..."); - mc = new ProbModelChecker(this, currentModel, null); - probs = ((ProbModelChecker) mc).doTransient((int) time, fileIn); + if (!getExplicit()) { + if (currentModelType == ModelType.DTMC) { + mc = new ProbModelChecker(this, currentModel, null); + probs = ((ProbModelChecker) mc).doTransient((int) time, fileIn); + } else { + mc = new StochModelChecker(this, currentModel, null); + probs = ((StochModelChecker) mc).doTransient(time, fileIn); + } } else { - mainLog.println("\nComputing transient probabilities (time = " + time + ")..."); - mc = new StochModelChecker(this, currentModel, null); - probs = ((StochModelChecker) mc).doTransient(time, fileIn); + if (currentModelType == ModelType.DTMC) { + throw new PrismException("Not implemented yet"); // TODO + } else if (currentModelType == ModelType.CTMC) { + CTMCModelChecker mcCTMC = new CTMCModelChecker(); + mcCTMC.setLog(mainLog); + mcCTMC.setSettings(settings); + probsExpl = mcCTMC.doTransient((CTMC) currentModelExpl, time, fileIn); + } else { + throw new PrismException("Transient probabilities only computed for DTMCs/CTMCs"); + } } l = System.currentTimeMillis() - l; @@ -2335,30 +2652,26 @@ public class Prism implements PrismSettingsListener mainLog.print("in Matlab format "); break; } - if (fileOut != null) - mainLog.println("to file \"" + fileOut + "\"..."); - else - mainLog.println("below:"); + mainLog.println(getDestinationStringForFile(file)); // create new file log or use main log - if (fileOut != null) { - tmpLog = new PrismFileLog(fileOut.getPath()); - if (!tmpLog.ready()) { - throw new PrismException("Could not open file \"" + fileOut + "\" for output"); - } - } else { - tmpLog = mainLog; - } + tmpLog = getPrismLogForFile(file); // print out or export probabilities - probs.print(tmpLog, fileOut == null, exportType == EXPORT_MATLAB, fileOut == null); + if (!getExplicit()) + probs.print(tmpLog, file == null, exportType == EXPORT_MATLAB, file == null); + else + probsExpl.print(tmpLog, file == null, exportType == EXPORT_MATLAB, file == null, true); // print out computation time mainLog.println("\nTime for transient probability computation: " + l / 1000.0 + " seconds."); // tidy up - probs.clear(); - if (fileOut != null) + if (!getExplicit()) + probs.clear(); + else + probsExpl.clear(); + if (file != null) tmpLog.close(); } @@ -2369,9 +2682,11 @@ public class Prism implements PrismSettingsListener { if (currentModel != null) currentModel.clear(); + // TODO: if (currentModelExpl != null) + //currentModelExpl.clear(); loadBuiltModel(null); } - + /** * Clear up and close down. */ @@ -2398,6 +2713,49 @@ public class Prism implements PrismSettingsListener } } + /** + * Either create a new PrismFileLog for {@code file} or, + * if {@code file} is null, return {@code mainLog}. + * Throws a {@code PrismException} if there is a problem opening the file. + */ + private PrismLog getPrismLogForFile(File file) throws PrismException + { + return getPrismLogForFile(file, false); + } + + /** + * Either create a new PrismFileLog for {@code file} or, + * if {@code file} is null, return {@code mainLog}. + * Throws a {@code PrismException} if there is a problem opening the file. + * If {@code append} is true, file should be opened in "append" mode. + */ + private PrismLog getPrismLogForFile(File file, boolean append) throws PrismException + { + // create new file log or use main log + PrismLog tmpLog; + if (file != null) { + tmpLog = new PrismFileLog(file.getPath(), append); + if (!tmpLog.ready()) { + throw new PrismException("Could not open file \"" + file + "\" for output"); + } + } else { + tmpLog = mainLog; + } + return tmpLog; + } + + /** + * Get a string describing the output destination specified by a File: + * "to file \"filename\"..." if non-null; "below:" if null + * Either create a new PrismFileLog for {@code file} or, + * if {@code file} is null, return {@code mainLog}. + * Throws a {@code PrismException} if there is a problem opening the file. + */ + private String getDestinationStringForFile(File file) throws PrismException + { + return (file == null) ? "below:" : "to file \"" + file + "\"..."; + } + //------------------------------------------------------------------------------ // Old API methods, supported via new one //------------------------------------------------------------------------------ @@ -2579,7 +2937,51 @@ public class Prism implements PrismSettingsListener public Result modelCheck(Model model, PropertiesFile propertiesFile, Expression expr) throws PrismException, PrismLangException { loadBuiltModel(model); - return modelCheck(propertiesFile, expr); + return modelCheck(propertiesFile, expr, null); + } + + /** + * Old API: + * Load a PRISM PTA model, perform model checking of a property on it and return result. + * @param modulesFile The corresponding (parsed) PRISM model (for the labels) + * @param propertiesFile Parent property file of property (for labels/constants/...) + * @param expr The property to check + */ + public Result modelCheckPTA(ModulesFile modulesFile, PropertiesFile propertiesFile, Expression expr) throws PrismException, PrismLangException + { + loadPRISMModel(modulesFile); + return modelCheckPTA(propertiesFile, expr, null); + } + + /** + * Old API: + */ + public Result modelCheckSimulator(ModulesFile modulesFile, PropertiesFile propertiesFile, Expression expr, State initialState, int maxPathLength, + SimulationMethod simMethod) throws PrismException + { + loadPRISMModel(modulesFile); + return modelCheckSimulator(propertiesFile, expr, null, initialState, maxPathLength, simMethod); + } + + /** + * Old API: + */ + public Result[] modelCheckSimulatorSimultaneously(ModulesFile modulesFile, PropertiesFile propertiesFile, List exprs, State initialState, + int maxPathLength, SimulationMethod simMethod) throws PrismException + { + loadPRISMModel(modulesFile); + return modelCheckSimulatorSimultaneously(propertiesFile, exprs, null, initialState, maxPathLength, simMethod); + } + + /** + * Old API: + */ + public void modelCheckSimulatorExperiment(ModulesFile modulesFile, PropertiesFile propertiesFile, UndefinedConstants undefinedConstants, + ResultsCollection results, Expression propertyToCheck, State initialState, int pathLength, SimulationMethod simMethod) throws PrismException, + InterruptedException + { + loadPRISMModel(modulesFile); + modelCheckSimulatorExperiment(propertiesFile, undefinedConstants, results, propertyToCheck, initialState, pathLength, simMethod); } /** @@ -2598,10 +3000,10 @@ public class Prism implements PrismSettingsListener * Output probability distribution to a file (or, if file is null, to log). * The exportType should be EXPORT_PLAIN or EXPORT_MATLAB. */ - public void doSteadyState(Model model, int exportType, File fileOut) throws PrismException + public void doSteadyState(Model model, int exportType, File file) throws PrismException { loadBuiltModel(model); - doSteadyState(exportType, fileOut); + doSteadyState(exportType, file); } /** @@ -2621,10 +3023,10 @@ public class Prism implements PrismSettingsListener * The exportType should be EXPORT_PLAIN or EXPORT_MATLAB. * Optionally (if non-null), read in the initial probability distribution from a file. */ - public void doTransient(Model model, double time, int exportType, File fileOut, File fileIn) throws PrismException + public void doTransient(Model model, double time, int exportType, File file, File fileIn) throws PrismException { loadBuiltModel(model); - doTransient(time, exportType, fileOut, fileIn); + doTransient(time, exportType, file, fileIn); } } diff --git a/prism/src/prism/PrismCL.java b/prism/src/prism/PrismCL.java index 92cfaab6..d13affd2 100644 --- a/prism/src/prism/PrismCL.java +++ b/prism/src/prism/PrismCL.java @@ -31,17 +31,13 @@ import java.util.*; import parser.*; import parser.ast.*; -import pta.*; import simulator.method.*; -import explicit.PrismExplicit; // prism - command line version public class PrismCL { // flags - private boolean verbose; - private boolean fixdl = false; private boolean importpepa = false; private boolean importprismpp = false; private boolean importtrans = false; @@ -72,7 +68,6 @@ public class PrismCL private boolean simpath = false; private ModelType typeOverride = null; private boolean orderingOverride = false; - private boolean explicit = false; private boolean explicitbuild = false; private boolean explicitbuildtest = false; private boolean nobuild = false; @@ -138,13 +133,6 @@ public class PrismCL private Values definedMFConstants; private Values definedPFConstants; - // built (symbolic) model storage - private Model model = null; - - // built (explicit) model storage - private PrismExplicit prismExpl = null; - private explicit.Model modelExpl; - // results private ResultsCollection results[] = null; @@ -175,18 +163,14 @@ public class PrismCL public void run(String[] args) { int i, j, k; - ModulesFile modulesFileToCheck; Result res; // Initialise initialise(args); - // Parse model/properties + // Parse/load model/properties doParsing(); - // Load model into PRISM - prism.loadPRISMModel(modulesFile); - // Sort out properties to check sortProperties(); @@ -240,7 +224,7 @@ public class PrismCL continue; } - // if requested, generate a random path with simulator (and then skip anything else) + // if requested, generate a random path with the simulator if (simpath) { try { if (!simMaxPathGiven) @@ -255,65 +239,23 @@ public class PrismCL for (j = 0; j < numPropertiesToCheck; j++) { undefinedConstants[j].iterateModel(); } - continue; } - // Do any requested exports of PRISM code - // (except for PTA digital clocks case - postpone this) - if (!(modulesFile.getModelType() == ModelType.PTA && prism.getSettings().getString(PrismSettings.PRISM_PTA_METHOD).equals("Digital clocks"))) { - doPrismLangExports(modulesFile); - } + // Do any exports of code/model + doPrismLangExports(); + doExports(); - // Decide if model construction is necessary - boolean doBuild = true; - // If explicitly disabled... - if (nobuild) - doBuild = false; - // No need if using approximate (simulation-based) model checking... - if (simulate) - doBuild = false; - // No need if doing PTA model checking... - // (even if needed for digital clocks, will be done later) - if (modulesFile.getModelType() == ModelType.PTA) - doBuild = false; - - // do model construction (if necessary) - if (doBuild) { - // build model - try { - buildModel(modulesFile, false); - } catch (PrismException e) { - // in case of error, report it, store as result for any properties, and go on to the next model - error(e.getMessage()); - try { - for (j = 0; j < numPropertiesToCheck; j++) { - results[j].setMultipleErrors(definedMFConstants, null, e); - } - } catch (PrismException e2) { - error("Problem storing results"); - } - // iterate to next model - undefinedMFConstants.iterateModel(); - for (j = 0; j < numPropertiesToCheck; j++) { - undefinedConstants[j].iterateModel(); - } - continue; - } - - // Do any exports - doExports(); + // Do steady-state/transient probability computation, if required + doSteadyState(); + doTransient(); - // Do steady-state/transient probability computation, if required - doSteadyState(); - doTransient(); - } - - // work through list of properties to be checked + // Work through list of properties to be checked for (j = 0; j < numPropertiesToCheck; j++) { // for simulation we can do multiple values of property constants simultaneously if (simulate && undefinedConstants[j].getNumPropertyIterations() > 1) { try { + // TODO: remove output mainLog.printSeparator(); mainLog.println("\nSimulating: " + propertiesToCheck.get(j)); if (definedMFConstants != null) @@ -321,7 +263,7 @@ public class PrismCL mainLog.println("Model constants: " + definedMFConstants); mainLog.println("Property constants: " + undefinedConstants[j].getPFDefinedConstantsString()); simMethod = processSimulationOptions(propertiesToCheck.get(j).getExpression()); - prism.modelCheckSimulatorExperiment(modulesFile, propertiesFile, undefinedConstants[j], results[j], propertiesToCheck.get(j).getExpression(), null, + prism.modelCheckSimulatorExperiment(propertiesFile, undefinedConstants[j], results[j], propertiesToCheck.get(j).getExpression(), null, simMaxPath, simMethod); } catch (PrismException e) { // in case of (overall) error, report it, store as result for property, and proceed @@ -341,54 +283,19 @@ public class PrismCL for (k = 0; k < undefinedConstants[j].getNumPropertyIterations(); k++) { try { - // set values for PropertiesFile constants + // Set values for PropertiesFile constants if (propertiesFile != null) { definedPFConstants = undefinedConstants[j].getPFConstantValues(); propertiesFile.setSomeUndefinedConstants(definedPFConstants); } - - // log output - mainLog.printSeparator(); - mainLog.println("\n" + (simulate ? "Simulating" : "Model checking") + ": " + propertiesToCheck.get(j)); - if (definedMFConstants != null) - if (definedMFConstants.getNumValues() > 0) - mainLog.println("Model constants: " + definedMFConstants); - if (definedPFConstants != null) - if (definedPFConstants.getNumValues() > 0) - mainLog.println("Property constants: " + definedPFConstants); - - // for PTAs via digital clocks, do model translation and build - if (modulesFile.getModelType() == ModelType.PTA - && prism.getSettings().getString(PrismSettings.PRISM_PTA_METHOD).equals("Digital clocks")) { - DigitalClocks dc = new DigitalClocks(prism); - dc.translate(modulesFile, propertiesFile, propertiesToCheck.get(j).getExpression()); - modulesFileToCheck = dc.getNewModulesFile(); - modulesFileToCheck.setUndefinedConstants(modulesFile.getConstantValues()); - doPrismLangExports(modulesFileToCheck); - buildModel(modulesFileToCheck, true); - } else { - modulesFileToCheck = modulesFile; - } - - // exact (non-approximate) model checking + // Normal model checking if (!simulate) { - // PTA model checking - if (modulesFileToCheck.getModelType() == ModelType.PTA) { - res = prism.modelCheckPTA(modulesFileToCheck, propertiesFile, propertiesToCheck.get(j).getExpression()); - } - // Non-PTA model checking - else { - if (!explicit) { - res = prism.modelCheck(propertiesFile, propertiesToCheck.get(j).getExpression()); - } else { - res = prismExpl.modelCheck(modelExpl, modulesFileToCheck, propertiesFile, propertiesToCheck.get(j).getExpression()); - } - } + res = prism.modelCheck(propertiesFile, propertiesToCheck.get(j).getExpression(), definedPFConstants); } - // approximate (simulation-based) model checking + // Approximate (simulation-based) model checking else { simMethod = processSimulationOptions(propertiesToCheck.get(j).getExpression()); - res = prism.modelCheckSimulator(modulesFileToCheck, propertiesFile, propertiesToCheck.get(j).getExpression(), null, simMaxPath, simMethod); + res = prism.modelCheckSimulator(propertiesFile, propertiesToCheck.get(j).getExpression(), definedPFConstants, null, simMaxPath, simMethod); simMethod.reset(); } } catch (PrismException e) { @@ -434,6 +341,15 @@ public class PrismCL } } + // Explicitly request a build if necessary + if (propertiesToCheck.size() == 0 && !simpath && !nobuild && prism.modelCanBeBuilt() && !prism.modelIsBuilt()) { + try { + prism.buildModel(); + } catch (PrismException e) { + error(e.getMessage()); + } + } + // clear model prism.clearBuiltModel(); @@ -496,7 +412,6 @@ public class PrismCL // create prism object(s) prism = new Prism(mainLog, techLog); - prismExpl = new PrismExplicit(mainLog, prism.getSettings()); // parse command line arguments parseArguments(args); @@ -509,16 +424,13 @@ public class PrismCL // do some processing of the options processOptions(); - - // store verbosity option locally - verbose = prism.getVerbose(); } catch (PrismException e) { errorAndExit(e.getMessage()); } } /** - * Parse model and properties. + * Parse model and properties, load model into PRISM. */ private void doParsing() { @@ -548,7 +460,7 @@ public class PrismCL lf = new File(importLabelsFilename); } mainLog.println("..."); - modulesFile = prism.parseModelFromExplicitFiles(sf, new File(modelFilename), lf, typeOverride); + modulesFile = prism.loadModelFromExplicitFiles(sf, new File(modelFilename), lf, typeOverride); } else { mainLog.print("\nParsing model file \"" + modelFilename + "\"...\n"); modulesFile = prism.parseModelFile(new File(modelFilename), typeOverride); @@ -581,12 +493,17 @@ public class PrismCL // print out properties (if any) - if (propertiesFile == null) - return; - mainLog.print("\n" + propertiesFile.getNumProperties()); - mainLog.print(" propert" + ((propertiesFile.getNumProperties() == 1) ? "y" : "ies") + ":\n"); - for (i = 0; i < propertiesFile.getNumProperties(); i++) { - mainLog.println("(" + (i + 1) + ") " + propertiesFile.getPropertyObject(i)); + if (propertiesFile != null) { + mainLog.print("\n" + propertiesFile.getNumProperties()); + mainLog.print(" propert" + ((propertiesFile.getNumProperties() == 1) ? "y" : "ies") + ":\n"); + for (i = 0; i < propertiesFile.getNumProperties(); i++) { + mainLog.println("(" + (i + 1) + ") " + propertiesFile.getPropertyObject(i)); + } + } + + // Load model into PRISM (if not done already) + if (!importtrans) { + prism.loadPRISMModel(modulesFile); } } @@ -633,41 +550,34 @@ public class PrismCL /** * Do any exports of PRISM code that have been requested. */ - private void doPrismLangExports(ModulesFile modulesFileToExport) + private void doPrismLangExports() { - // output final prism model here if required + // output parsed prism model here if required if (exportprism) { - mainLog.print("\nExporting parsed PRISM file "); - if (!exportPrismFilename.equals("stdout")) - mainLog.println("to file \"" + exportPrismFilename + "\"..."); - else - mainLog.println("below:"); - PrismFileLog tmpLog = new PrismFileLog(exportPrismFilename); - if (!tmpLog.ready()) { - errorAndExit("Couldn't open file \"" + exportPrismFilename + "\" for output"); + try { + File f = (exportPrismFilename.equals("stdout")) ? null : new File(exportPrismFilename); + prism.exportPRISMModel(f); + } + // in case of error, report it and proceed + catch (FileNotFoundException e) { + error("Couldn't open file \"" + exportPrismFilename + "\" for output"); + } catch (PrismException e) { + error(e.getMessage()); } - tmpLog.print(modulesFileToExport.toString()); } + + // output parsed prism model, with constants, here if required if (exportprismconst) { - mainLog.print("\nExporting parsed PRISM file (with constant expansion) "); - if (!exportPrismConstFilename.equals("stdout")) - mainLog.println("to file \"" + exportPrismConstFilename + "\"..."); - else - mainLog.println("below:"); - PrismFileLog tmpLog = new PrismFileLog(exportPrismConstFilename); - if (!tmpLog.ready()) { - errorAndExit("Couldn't open file \"" + exportPrismConstFilename + "\" for output"); - } - ModulesFile mfTmp = (ModulesFile) modulesFileToExport.deepCopy(); try { - mfTmp = (ModulesFile) mfTmp.replaceConstants(modulesFileToExport.getConstantValues()); - mfTmp = (ModulesFile) mfTmp.replaceConstants(definedMFConstants); - // NB: Don't use simplify() here because doesn't work for the purposes of printing out - // (e.g. loss of parethenses causes precedence problems) - } catch (PrismLangException e) { + File f = (exportPrismConstFilename.equals("stdout")) ? null : new File(exportPrismConstFilename); + prism.exportPRISMModelWithExpandedConstants(f); + } + // in case of error, report it and proceed + catch (FileNotFoundException e) { + error("Couldn't open file \"" + exportPrismConstFilename + "\" for output"); + } catch (PrismException e) { error(e.getMessage()); } - tmpLog.print(mfTmp.toString()); } } @@ -680,92 +590,9 @@ public class PrismCL */ private void buildModel(ModulesFile modulesFileToBuild, boolean digital) throws PrismException { + // TODO + /* StateList states; - int i; - - mainLog.printSeparator(); - - // build model - if (!explicit) { - if (importtrans) { - model = prism.buildModelFromExplicitFiles(); - } else if (explicitbuild) { - model = prism.buildModelExplicit(modulesFileToBuild); - } else { - model = prism.buildModel(modulesFileToBuild); - } - modelExpl = null; - } else { - if (importtrans) { - // TODO: add -importtrans case using model.buildFromPrismExplicit(...); - throw new PrismException("Explicit import not yet supported for explicit engine"); - } else { - modelExpl = prismExpl.buildModel(modulesFileToBuild, prism.getSimulator()); - } - model = null; - } - - // Print model info - mainLog.println(); - if (!explicit) { - prism.printBuiltModelInfo(); - } else { - mainLog.println("\nType: " + modelExpl.getModelType()); - } - - // check for deadlocks - if (!explicit) { - states = model.getDeadlockStates(); - if (states != null && states.size() > 0) { - // for pta models (via digital clocks) - if (digital) { - // by construction, these can only occur from timelocks - throw new PrismException("Timelock in PTA, e.g. in state (" + states.getFirstAsValues() + ")"); - } - // if requested, remove them - else if (fixdl) { - mainLog.printWarning(states.size() + " deadlock states detected; adding self-loops in these states..."); - model.fixDeadlocks(); - } - // otherwise print error and bail out - else { - mainLog.println(); - model.printTransInfo(mainLog, prism.getExtraDDInfo()); - mainLog.print("\nError: Model contains " + states.size() + " deadlock states"); - if (!verbose && states.size() > 10) { - mainLog.print(".\nThe first 10 deadlock states are displayed below. To view them all use the -v switch.\n"); - states.print(mainLog, 10); - } else { - mainLog.print(":\n"); - states.print(mainLog); - } - mainLog.print("\nTip: Use the -fixdl switch to automatically add self-loops in deadlock states.\n"); - model.clear(); - exit(1); - } - } - } else { - BitSet deadlocks = modelExpl.findDeadlocks(fixdl); - if (deadlocks.cardinality() > 0) { - if (fixdl) { - mainLog.println("Added self-loops in " + deadlocks.cardinality() + " states..."); - } else { - mainLog.println(); - mainLog.print("\nError: Model contains " + deadlocks.size() + " deadlock states"); - mainLog.print("\nTip: Use the -fixdl switch to automatically add self-loops in deadlock states.\n"); - exit(1); - } - } - } - - // Print model stats - mainLog.println(); - if (!explicit) { - prism.printBuiltModelStats(); - } else { - mainLog.print(modelExpl.infoStringTable()); - } - // If enabled, also construct model explicitly and compare (for testing purposes) if (explicitbuildtest) { String tmpFile = "'"; @@ -798,7 +625,7 @@ public class PrismCL } catch (IOException e) { throw new PrismException("Could not create temporary file \"" + tmpFile + "\""); } - } + }*/ } // do any exporting requested @@ -809,11 +636,7 @@ public class PrismCL if (exporttrans) { try { File f = (exportTransFilename.equals("stdout")) ? null : new File(exportTransFilename); - if (explicit) { - prismExpl.exportTransToFile(modelExpl, exportordered, exportType, f); - } else { - prism.exportTransToFile(exportordered, exportType, f); - } + prism.exportTransToFile(exportordered, exportType, f); } // in case of error, report it and proceed catch (FileNotFoundException e) { @@ -858,11 +681,7 @@ public class PrismCL if (exportstates) { try { File f = (exportStatesFilename.equals("stdout")) ? null : new File(exportStatesFilename); - if (explicit) { - prismExpl.exportStatesToFile(modulesFile, modelExpl, exportType, f); - } else { - prism.exportStatesToFile(exportType, f); - } + prism.exportStatesToFile(exportType, f); } // in case of error, report it and proceed catch (FileNotFoundException e) { @@ -973,13 +792,8 @@ public class PrismCL exportSteadyStateFile = null; else exportSteadyStateFile = new File(exportSteadyStateFilename); - // Compute steady-state probabilities - if (explicit) { - prismExpl.doSteadyState(modelExpl, exportType, exportSteadyStateFile); - } else { - prism.doSteadyState(exportType, exportSteadyStateFile); - } + prism.doSteadyState(exportType, exportSteadyStateFile); } catch (PrismException e) { // In case of error, report it and proceed error(e.getMessage()); @@ -1006,11 +820,7 @@ public class PrismCL exportTransientFile = new File(exportTransientFilename); // Determine model type - if (explicit) { - modelType = modelExpl.getModelType(); - } else { - modelType = prism.getBuiltModel().getModelType(); - } + modelType = prism.getModelType(); // Compute transient probabilities if (modelType == ModelType.CTMC) { @@ -1019,22 +829,14 @@ public class PrismCL } catch (NumberFormatException e) { throw new PrismException("Invalid value \"" + transientTime + "\" for transient probability computation"); } - if (explicit) { - prismExpl.doTransient(modelExpl, d, exportType, exportTransientFile, importinitdist ? new File(importInitDistFilename) : null); - } else { - prism.doTransient(d, exportType, exportTransientFile, importinitdist ? new File(importInitDistFilename) : null); - } + prism.doTransient(d, exportType, exportTransientFile, importinitdist ? new File(importInitDistFilename) : null); } else if (modelType == ModelType.DTMC) { try { i = Integer.parseInt(transientTime); } catch (NumberFormatException e) { throw new PrismException("Invalid value \"" + transientTime + "\" for transient probability computation"); } - if (explicit) { - prismExpl.doTransient(modelExpl, i, exportType, exportTransientFile, importinitdist ? new File(importInitDistFilename) : null); - } else { - prism.doTransient(i, exportType, exportTransientFile, importinitdist ? new File(importInitDistFilename) : null); - } + prism.doTransient(i, exportType, exportTransientFile, importinitdist ? new File(importInitDistFilename) : null); } else { mainLog.printWarning("Transient probabilities only computed for DTMCs/CTMCs."); } @@ -1606,14 +1408,6 @@ public class PrismCL else if (sw.equals("modpoliter")) { prism.setMDPSolnMethod(Prism.MDP_MODPOLITER); } - // fix deadlocks - else if (sw.equals("fixdl")) { - fixdl = true; - } - // enable explicit-state engine - else if (sw.equals("explicit") || sw.equals("ex")) { - explicit = true; - } // explicit-state model construction else if (sw.equals("explicitbuild")) { explicitbuild = true; @@ -1743,7 +1537,7 @@ public class PrismCL } // explicit overrides explicit build - if (explicit) { + if (prism.getExplicit()) { explicitbuild = false; } diff --git a/prism/src/prism/PrismModelListener.java b/prism/src/prism/PrismModelListener.java new file mode 100644 index 00000000..41109c41 --- /dev/null +++ b/prism/src/prism/PrismModelListener.java @@ -0,0 +1,33 @@ +//============================================================================== +// +// Copyright (c) 2002- +// Authors: +// * Dave Parker (University of Oxford) +// +//------------------------------------------------------------------------------ +// +// This file is part of PRISM. +// +// PRISM is free software; you can redistribute it and/or modify +// it under the terms of the GNU General Public License as published by +// the Free Software Foundation; either version 2 of the License, or +// (at your option) any later version. +// +// PRISM is distributed in the hope that it will be useful, +// but WITHOUT ANY WARRANTY; without even the implied warranty of +// MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the +// GNU General Public License for more details. +// +// You should have received a copy of the GNU General Public License +// along with PRISM; if not, write to the Free Software Foundation, +// Inc., 59 Temple Place, Suite 330, Boston, MA 02111-1307 USA +// +//============================================================================== + +package prism; + +public interface PrismModelListener +{ + public void notifyModelBuildSuccessful(); + public void notifyModelBuildFailed(PrismException e); +} diff --git a/prism/src/prism/PrismSettings.java b/prism/src/prism/PrismSettings.java index 5ff41f86..013bf5ac 100644 --- a/prism/src/prism/PrismSettings.java +++ b/prism/src/prism/PrismSettings.java @@ -74,6 +74,7 @@ public class PrismSettings implements Observer public static final String PRISM_PRECOMPUTATION = "prism.precomputation"; public static final String PRISM_PROB0 = "prism.prob0"; public static final String PRISM_PROB1 = "prism.prob1"; + public static final String PRISM_FIX_DEADLOCKS = "prism.fixDeadlocks"; public static final String PRISM_DO_PROB_CHECKS = "prism.doProbChecks"; public static final String PRISM_COMPACT = "prism.compact"; public static final String PRISM_LIN_EQ_METHOD = "prism.linEqMethod";//"prism.iterativeMethod"; @@ -187,8 +188,8 @@ public class PrismSettings implements Observer //==================================================================================================================================================================================================================================================================================================================================== // ENGINES/METHODS: - { CHOICE_TYPE, PRISM_ENGINE, "Engine", "2.1", "Hybrid", "MTBDD,Sparse,Hybrid", - "Which engine (hybrid, sparse or MTBDD) should be used for model checking." }, + { CHOICE_TYPE, PRISM_ENGINE, "Engine", "2.1", "Hybrid", "MTBDD,Sparse,Hybrid,Explicit", + "Which engine (hybrid, sparse, MTBDD, explicit) should be used for model checking." }, { CHOICE_TYPE, PRISM_PTA_METHOD, "PTA model checking method", "3.3", "Stochastic games", "Digital clocks,Stochastic games", "Which method to use for model checking of PTAs." }, // NUMERICAL SOLUTION OPTIONS: @@ -213,6 +214,8 @@ public class PrismSettings implements Observer "Whether to use model checking precomputation algorithm Prob1 (if precomputation enabled)." }, { BOOLEAN_TYPE, PRISM_FAIRNESS, "Use fairness", "2.1", new Boolean(false), "", "Constrain to fair adversaries when model checking MDPs." }, + { BOOLEAN_TYPE, PRISM_FIX_DEADLOCKS, "Automatically fix deadlocks", "4.0.3", new Boolean(true), "", + "Automatically fix deadlocks, where necessary, when constructing probabilistic models." }, { BOOLEAN_TYPE, PRISM_DO_PROB_CHECKS, "Do probability/rate checks", "2.1", new Boolean(true), "", "Perform sanity checks on model probabilities/rates when constructing probabilistic models." }, { BOOLEAN_TYPE, PRISM_DO_SS_DETECTION, "Use steady-state detection", "2.1", new Boolean(true), "0,", @@ -738,6 +741,9 @@ public class PrismSettings implements Observer else if (sw.equals("hybrid") || sw.equals("h")) { set(PRISM_ENGINE, "Hybrid"); } + else if (sw.equals("explicit") || sw.equals("ex")) { + set(PRISM_ENGINE, "Explicit"); + } // PTA model checking methods else if (sw.equals("ptamethod")) { if (i < args.length - 1) { @@ -845,6 +851,13 @@ public class PrismSettings implements Observer else if (sw.equals("noprob1")) { set(PRISM_PROB1, false); } + // Fix deadlocks on/off + else if (sw.equals("fixdl")) { + set(PRISM_FIX_DEADLOCKS, true); + } + else if (sw.equals("nofixdl")) { + set(PRISM_FIX_DEADLOCKS, false); + } // Fairness on/off else if (sw.equals("fair")) { set(PRISM_FAIRNESS, true); @@ -1073,7 +1086,8 @@ public class PrismSettings implements Observer mainLog.println("-noprob1 ....................... Skip precomputation algorithm Prob1 (where optional)"); mainLog.println("-fair .......................... Use fairness (for model checking of MDPs)"); mainLog.println("-nofair ........................ Don't use fairness (for model checking of MDPs) [default]"); - mainLog.println("-fixdl ......................... Automatically put self-loops in deadlock states"); + mainLog.println("-fixdl ......................... Automatically put self-loops in deadlock states [default]"); + mainLog.println("-nofixdl ....................... Do not automatically put self-loops in deadlock states"); mainLog.println("-noprobchecks .................. Disable checks on model probabilities/rates"); mainLog.println("-zerorewardcheck ............... Check for absence of zero-reward loops"); mainLog.println("-nossdetect .................... Disable steady-state detection for CTMC transient computations"); diff --git a/prism/src/prism/ProbModel.java b/prism/src/prism/ProbModel.java index 3774145c..e1f78569 100644 --- a/prism/src/prism/ProbModel.java +++ b/prism/src/prism/ProbModel.java @@ -69,8 +69,7 @@ public class ProbModel implements Model protected JDDNode trans01; // 0-1 transition matrix dd protected JDDNode start; // start state dd protected JDDNode reach; // reachable states dd - protected JDDNode deadlocks; // deadlock states dd - protected JDDNode fixdl; // fixed deadlock states dd + protected JDDNode deadlocks; // deadlock states dd (may have been fixed) protected JDDNode stateRewards[]; // state rewards dds protected JDDNode transRewards[]; // transition rewards dds protected JDDNode transActions; // dd for transition action labels (MDPs) @@ -212,6 +211,7 @@ public class ProbModel implements Model return new StateListMTBDD(reach, this); } + @Override public StateList getDeadlockStates() { return new StateListMTBDD(deadlocks, this); @@ -244,16 +244,12 @@ public class ProbModel implements Model return reach; } + @Override public JDDNode getDeadlocks() { return deadlocks; } - public JDDNode getFixedDeadlocks() - { - return fixdl; - } - public JDDNode getStateRewards() { return getStateRewards(0); @@ -396,7 +392,7 @@ public class ProbModel implements Model trans = tr; start = s; - fixdl = JDD.Constant(0); + deadlocks = null; stateRewards = sr; transRewards = trr; numRewardStructs = stateRewards.length; // which should == transRewards.length @@ -601,9 +597,8 @@ public class ProbModel implements Model numTransitions = JDD.GetNumMinterms(trans01, getNumDDVarsInTrans()); } - // identify any deadlock states - - public void findDeadlocks() + @Override + public void findDeadlocks(boolean fix) { // find states with at least one transition JDD.Ref(trans01); @@ -612,17 +607,11 @@ public class ProbModel implements Model // find reachable states with no transitions JDD.Ref(reach); deadlocks = JDD.And(reach, JDD.Not(deadlocks)); - } - - // remove deadlocks by adding self-loops - - public void fixDeadlocks() - { - JDDNode tmp; - - if (!deadlocks.equals(JDD.ZERO)) { + + if (fix && !deadlocks.equals(JDD.ZERO)) { // remove deadlocks by adding self-loops // also update transPerAction info, if present + JDDNode tmp; JDD.Ref(deadlocks); tmp = JDD.And(deadlocks, JDD.Identity(allDDRowVars, allDDColVars)); JDD.Ref(tmp); @@ -634,10 +623,6 @@ public class ProbModel implements Model transPerAction[0] = JDD.Apply(JDD.PLUS, transPerAction[0], tmp); } JDD.Deref(tmp); - // update lists of deadlocks - JDD.Deref(fixdl); - fixdl = deadlocks; - deadlocks = JDD.Constant(0); // update model stats numTransitions = JDD.GetNumMinterms(trans01, getNumDDVarsInTrans()); } @@ -883,7 +868,6 @@ public class ProbModel implements Model JDD.Deref(reach); if (deadlocks != null) JDD.Deref(deadlocks); - JDD.Deref(fixdl); for (int i = 0; i < numRewardStructs; i++) { JDD.Deref(stateRewards[i]); JDD.Deref(transRewards[i]); diff --git a/prism/src/prism/StateModelChecker.java b/prism/src/prism/StateModelChecker.java index f0a7cef7..328a94de 100644 --- a/prism/src/prism/StateModelChecker.java +++ b/prism/src/prism/StateModelChecker.java @@ -976,7 +976,7 @@ public class StateModelChecker implements ModelChecker // treat special cases if (expr.getName().equals("deadlock")) { - dd = model.getFixedDeadlocks(); + dd = model.getDeadlocks(); JDD.Ref(dd); return new StateValuesMTBDD(dd, model); } else if (expr.getName().equals("init")) { diff --git a/prism/src/userinterface/model/GUIModelEvent.java b/prism/src/userinterface/model/GUIModelEvent.java index 0f89c281..9e89ea65 100644 --- a/prism/src/userinterface/model/GUIModelEvent.java +++ b/prism/src/userinterface/model/GUIModelEvent.java @@ -27,73 +27,55 @@ package userinterface.model; -import parser.ast.ModulesFile; -import prism.Model; import parser.Values; -import userinterface.util.*; +import parser.ast.ModulesFile; +import userinterface.util.GUIEvent; public class GUIModelEvent extends GUIEvent { - //CONSTANTS - public static final int NEW_MODEL = 0; //when no parsed or built model - public static final int LOAD_MODEL = 1; //when model is loaded into text editor - public static final int IMPORT_MODEL = 2; //when model is imported into text editor - public static final int MODEL_PARSED = 3; // when parsed model exists - public static final int MODIFIED_SINCE_SAVE = 4; //when text is modified - public static final int SAVE_MODEL = 5; //when text is saved to file - public static final int MODEL_BUILT = 6; //when built model exists - public static final int MODEL_PARSE_FAILED = 7; //when a failed model parse happens - public static final int MODEL_BUILD_FAILED = 8; //when a failed model build happens - public static final int NEW_LOAD_NOT_RELOAD_MODEL = 9; - - //DATA ATTRIBUTES - private ModulesFile file; - private Model model; - private Values buildValues; - - /** Creates a new instance of GUIModelEvent */ - public GUIModelEvent(int id, ModulesFile file) - { - super(id); - this.file = file; - this.model = null; - } - - public GUIModelEvent(int id, Model model) - { - super(id); - this.model = model; - this.file = null; - } - - public GUIModelEvent(int id, Model model, Values buildValues) - { - super(id); - this.model = model; - this.file = null; - this.buildValues = buildValues; - } - - public GUIModelEvent(int id) - { - super(id); - this.model = null; - this.file = null; - } - - public ModulesFile getModulesFile() - { - return file; - } - - public Model getModel() - { - return model; - } - - public Values getBuildValues() - { - return buildValues; - } - + // CONSTANTS + public static final int NEW_MODEL = 0; //when no parsed or built model + public static final int LOAD_MODEL = 1; //when model is loaded into text editor + public static final int IMPORT_MODEL = 2; //when model is imported into text editor + public static final int MODEL_PARSED = 3; // when parsed model exists + public static final int MODIFIED_SINCE_SAVE = 4; //when text is modified + public static final int SAVE_MODEL = 5; //when text is saved to file + public static final int MODEL_BUILT = 6; //when built model exists + public static final int MODEL_PARSE_FAILED = 7; //when a failed model parse happens + public static final int MODEL_BUILD_FAILED = 8; //when a failed model build happens + public static final int NEW_LOAD_NOT_RELOAD_MODEL = 9; + + // DATA ATTRIBUTES + private ModulesFile file; + private Values buildValues; + + /** Creates a new instance of GUIModelEvent */ + public GUIModelEvent(int id, ModulesFile file) + { + super(id); + this.file = file; + } + + public GUIModelEvent(int id, Values buildValues) + { + super(id); + this.file = null; + this.buildValues = buildValues; + } + + public GUIModelEvent(int id) + { + super(id); + this.file = null; + } + + public ModulesFile getModulesFile() + { + return file; + } + + public Values getBuildValues() + { + return buildValues; + } } diff --git a/prism/src/userinterface/model/GUIMultiModel.java b/prism/src/userinterface/model/GUIMultiModel.java index 72062506..2fc6f87e 100644 --- a/prism/src/userinterface/model/GUIMultiModel.java +++ b/prism/src/userinterface/model/GUIMultiModel.java @@ -41,24 +41,22 @@ public class GUIMultiModel extends GUIPlugin implements PrismSettingsListener { //Constants public static final boolean GM_ENABLED = false; - + public static final int CONTINUE = 0; - public static final int CANCEL = 1; - - public static final int FILTER_PRISM_MODEL = 0; + public static final int CANCEL = 1; + + public static final int FILTER_PRISM_MODEL = 0; public static final int FILTER_PEPA_MODEL = 1; public static final int FILTER_GRAPHIC_MODEL = 2; - + //GUI private JLabel fileLabel; private JMenu modelMenu, newMenu, viewMenu, exportMenu, computeMenu; private JMenu exportStatesMenu, exportTransMenu, exportStateRewardsMenu, exportTransRewardsMenu; - private AbstractAction viewStates, viewTrans, viewStateRewards, viewTransRewards, viewPrismCode, - computeSS, computeTr, newPRISMModel, newGraphicModel, - newPEPAModel, loadModel, reloadModel, saveModel, saveAsModel, parseModel, buildModel, - exportStatesPlain, exportStatesMatlab, exportTransPlain, exportTransMatlab, exportTransDot, exportTransDotStates, exportTransMRMC, - exportStateRewardsPlain, exportStateRewardsMatlab, exportStateRewardsMRMC, - exportTransRewardsPlain, exportTransRewardsMatlab, exportTransRewardsMRMC; + private AbstractAction viewStates, viewTrans, viewStateRewards, viewTransRewards, viewPrismCode, computeSS, computeTr, newPRISMModel, newGraphicModel, + newPEPAModel, loadModel, reloadModel, saveModel, saveAsModel, parseModel, buildModel, exportStatesPlain, exportStatesMatlab, exportTransPlain, + exportTransMatlab, exportTransDot, exportTransDotStates, exportTransMRMC, exportStateRewardsPlain, exportStateRewardsMatlab, + exportStateRewardsMRMC, exportTransRewardsPlain, exportTransRewardsMatlab, exportTransRewardsMRMC; private JPopupMenu popup; //Contents private GUIMultiModelHandler handler; @@ -69,10 +67,7 @@ public class GUIMultiModel extends GUIPlugin implements PrismSettingsListener //State private boolean computing = false; private boolean initialised = false; - - //Options - //private GUIMultiModelOptions op; - + /** Creates a new instance of GUIMultiModel */ public GUIMultiModel(GUIPrism pr) { @@ -81,9 +76,8 @@ public class GUIMultiModel extends GUIPlugin implements PrismSettingsListener initComponents(); initialised = true; doEnables(); - //op = new GUIMultiModelOptions(handler); } - + public void takeCLArgs(String args[]) { if (args.length > 0) { @@ -92,36 +86,44 @@ public class GUIMultiModel extends GUIPlugin implements PrismSettingsListener handler.loadModel(f, false); // set the default directory of the file chooser File dir = f.getParentFile(); - if (dir == null) dir = new File("."); + if (dir == null) + dir = new File("."); getGUI().getChooser().setCurrentDirectory(dir); } } - + public GUIMultiModelHandler getHandler() { return handler; } - + public JPopupMenu getPopup() { return popup; } - + public void doEnables() { // do nothing if not initialised yet - if (!initialised) return; + if (!initialised) + return; // setup file label int mode = handler.getModelMode(); String s = ""; - switch(mode) - { - case GUIMultiModelHandler.PRISM_MODE: s+="PRISM Model File: "; break; - case GUIMultiModelHandler.PEPA_MODE: s+="PEPA Model File: "; break; - case GUIMultiModelHandler.GRAPHIC_MODE: s+="PRISM Graphic Model File: ";break; + switch (mode) { + case GUIMultiModelHandler.PRISM_MODE: + s += "PRISM Model File: "; + break; + case GUIMultiModelHandler.PEPA_MODE: + s += "PEPA Model File: "; + break; + case GUIMultiModelHandler.GRAPHIC_MODE: + s += "PRISM Graphic Model File: "; + break; } s += handler.getActiveFileName(); - if (handler.modified()) s += "*"; + if (handler.modified()) + s += "*"; fileLabel.setText(s); // model menu newPRISMModel.setEnabled(!computing); @@ -154,47 +156,54 @@ public class GUIMultiModel extends GUIPlugin implements PrismSettingsListener exportTransRewardsMatlab.setEnabled(!computing); exportTransRewardsMRMC.setEnabled(!computing); } - + public int doModificationCheck() { - if (!handler.modified()) return CONTINUE; - if (!handler.hasActiveFile()) - { - String[] selection = {"Yes", "No", "Cancel"}; + if (!handler.modified()) + return CONTINUE; + if (!handler.hasActiveFile()) { + String[] selection = { "Yes", "No", "Cancel" }; int selectionNo = -1; - selectionNo = optionPane("Model has been modified.\nDo you wish to save it?", "Question", JOptionPane.OK_CANCEL_OPTION, JOptionPane.QUESTION_MESSAGE, selection, selection[0]); - switch(selectionNo) - { - case 0: return a_saveModelAs(); - case 1: return CONTINUE; - case 2: return CANCEL; - default: return CANCEL; + selectionNo = optionPane("Model has been modified.\nDo you wish to save it?", "Question", JOptionPane.OK_CANCEL_OPTION, + JOptionPane.QUESTION_MESSAGE, selection, selection[0]); + switch (selectionNo) { + case 0: + return a_saveModelAs(); + case 1: + return CONTINUE; + case 2: + return CANCEL; + default: + return CANCEL; } - } - else - { - String[] selection = {"Yes", "No", "Save As...", "Cancel"}; + } else { + String[] selection = { "Yes", "No", "Save As...", "Cancel" }; int selectionNo = -1; - selectionNo = optionPane("Model has been modified.\nDo you wish to save it?", "Question", JOptionPane.OK_CANCEL_OPTION, JOptionPane.QUESTION_MESSAGE, selection, selection[0]); - switch(selectionNo) - { - case 0: return a_saveModel(); - case 1: return CONTINUE; - case 2: return a_saveModelAs(); - case 3: return CANCEL; - default: return CANCEL; + selectionNo = optionPane("Model has been modified.\nDo you wish to save it?", "Question", JOptionPane.OK_CANCEL_OPTION, + JOptionPane.QUESTION_MESSAGE, selection, selection[0]); + switch (selectionNo) { + case 0: + return a_saveModel(); + case 1: + return CONTINUE; + case 2: + return a_saveModelAs(); + case 3: + return CANCEL; + default: + return CANCEL; } } } - + public void showModel(String modelString) { JDialog diag = new JDialog(getGUI(), false); - + diag.setTitle("Parsed PRISM Model"); GUITextModelEditor edit = new GUITextModelEditor(modelString, handler); edit.setEditable(false); - edit.setBackground(new Color(224,255,255)); + edit.setBackground(new Color(224, 255, 255)); /* PrismEditorKit kit = new PrismEditorKit(); edit.setEditorKitForContentType("text/prism", kit); @@ -202,52 +211,57 @@ public class GUIMultiModel extends GUIPlugin implements PrismSettingsListener edit.setPreferredSize(new Dimension(1000,300)); edit.setText(modelString); edit.setFont(new Font("monospaced", Font.PLAIN, 12));*/ - + JScrollPane scro = new JScrollPane(); - scro.setPreferredSize(new Dimension(640,300)); + scro.setPreferredSize(new Dimension(640, 300)); scro.setViewportView(edit); diag.getContentPane().add(scro); - + diag.setDefaultCloseOperation(JDialog.DISPOSE_ON_CLOSE); diag.pack(); diag.setLocationRelativeTo(getGUI()); // centre diag.show(); } - + //Action methods - + protected void a_newPRISMModel() { int cont = doModificationCheck(); - if(cont == CONTINUE) handler.newPRISMModel(); + if (cont == CONTINUE) + handler.newPRISMModel(); } - + protected void a_newPEPAModel() { int cont = doModificationCheck(); - if(cont == CONTINUE) handler.newPEPAModel(); + if (cont == CONTINUE) + handler.newPEPAModel(); } - + protected void a_newGraphicModel() { int cont = doModificationCheck(); - if(cont == CONTINUE) handler.newGraphicModel(); + if (cont == CONTINUE) + handler.newGraphicModel(); } - + protected void a_openModel() { int cont = doModificationCheck(); - if(cont == CONTINUE) - { + if (cont == CONTINUE) { int filterIndex; - switch(handler.getModelMode()) - { - case GUIMultiModelHandler.PEPA_MODE: filterIndex = FILTER_PEPA_MODEL; break; - case GUIMultiModelHandler.GRAPHIC_MODE: filterIndex = FILTER_GRAPHIC_MODEL; break; - default: filterIndex = FILTER_PRISM_MODEL; + switch (handler.getModelMode()) { + case GUIMultiModelHandler.PEPA_MODE: + filterIndex = FILTER_PEPA_MODEL; + break; + case GUIMultiModelHandler.GRAPHIC_MODE: + filterIndex = FILTER_GRAPHIC_MODEL; + break; + default: + filterIndex = FILTER_PRISM_MODEL; } - if (showOpenFileDialog(modelFilters, modelFilters[filterIndex]) == JFileChooser.APPROVE_OPTION) - { + if (showOpenFileDialog(modelFilters, modelFilters[filterIndex]) == JFileChooser.APPROVE_OPTION) { File file = getChooserFile(); if (file == null) { error("No file selected"); @@ -257,34 +271,36 @@ public class GUIMultiModel extends GUIPlugin implements PrismSettingsListener } } } - + protected void a_reloadModel() { int cont = doModificationCheck(); - if(cont == CONTINUE) handler.reloadActiveFile(); + if (cont == CONTINUE) + handler.reloadActiveFile(); } - + protected int a_saveModel() { - if(!handler.hasActiveFile()) - { + if (!handler.hasActiveFile()) { return a_saveModelAs(); - } - else - { + } else { return handler.saveToActiveFile(); } } - + protected int a_saveModelAs() { int mode = handler.getModelMode(); int filterIndex; - switch(mode) - { - case GUIMultiModelHandler.PEPA_MODE: filterIndex = FILTER_PEPA_MODEL; break; - case GUIMultiModelHandler.GRAPHIC_MODE: filterIndex = FILTER_GRAPHIC_MODEL; break; - default: filterIndex = FILTER_PRISM_MODEL; + switch (mode) { + case GUIMultiModelHandler.PEPA_MODE: + filterIndex = FILTER_PEPA_MODEL; + break; + case GUIMultiModelHandler.GRAPHIC_MODE: + filterIndex = FILTER_GRAPHIC_MODEL; + break; + default: + filterIndex = FILTER_PRISM_MODEL; } if (showSaveFileDialog(modelFilters, modelFilters[filterIndex]) != JFileChooser.APPROVE_OPTION) { return CANCEL; @@ -292,12 +308,12 @@ public class GUIMultiModel extends GUIPlugin implements PrismSettingsListener // do save return handler.saveToFile(getChooserFile()); } - + protected void a_refreshParseTree() { handler.requestParse(true); } - + protected void a_build() { // Reset warnings counter @@ -305,48 +321,52 @@ public class GUIMultiModel extends GUIPlugin implements PrismSettingsListener // Request build handler.forceBuild(); } - /* - protected void a_build(Values mfUndefined) - { - handler.forceBuild(mfUndefined); - }*/ - + protected void a_exportBuildAs(int exportEntity, int exportType) { int res = JFileChooser.CANCEL_OPTION; - + // pop up dialog to select file switch (exportType) { - case Prism.EXPORT_DOT: res = showSaveFileDialog(dotFilter, dotFilter[0]); break; - case Prism.EXPORT_DOT_STATES: res = showSaveFileDialog(dotFilter, dotFilter[0]); break; - case Prism.EXPORT_MATLAB: res = showSaveFileDialog(matlabFilter, matlabFilter[0]); break; - default: res = showSaveFileDialog(textFilter, textFilter[0]); break; + case Prism.EXPORT_DOT: + res = showSaveFileDialog(dotFilter, dotFilter[0]); + break; + case Prism.EXPORT_DOT_STATES: + res = showSaveFileDialog(dotFilter, dotFilter[0]); + break; + case Prism.EXPORT_MATLAB: + res = showSaveFileDialog(matlabFilter, matlabFilter[0]); + break; + default: + res = showSaveFileDialog(textFilter, textFilter[0]); + break; } - if (res != JFileChooser.APPROVE_OPTION) return; + if (res != JFileChooser.APPROVE_OPTION) + return; // Reset warnings counter getPrism().getMainLog().resetNumberOfWarnings(); - // do export... - handler.exportBuild(exportEntity, exportType, getChooserFile()); + // Do export... + handler.export(exportEntity, exportType, getChooserFile()); } - + protected void a_viewBuild(int exportEntity, int exportType) { // Reset warnings counter getPrism().getMainLog().resetNumberOfWarnings(); // Do view... - handler.exportBuild(exportEntity, exportType, null); - } - -// protected void a_viewStates() -// { -// handler.requestViewStates(); -// } - + handler.export(exportEntity, exportType, null); + } + + // protected void a_viewStates() + // { + // handler.requestViewStates(); + // } + protected void a_viewCurrentModelBuild() { handler.requestViewModel(); } - + protected void a_computeSteadyState() { // Reset warnings counter @@ -354,7 +374,7 @@ public class GUIMultiModel extends GUIPlugin implements PrismSettingsListener // Do steady-state handler.computeSteadyState(); } - + protected void a_computeTransient() { // Reset warnings counter @@ -365,52 +385,56 @@ public class GUIMultiModel extends GUIPlugin implements PrismSettingsListener handler.computeTransient(GUITransientTime.getTime()); } } - + protected void a_convertToPrismTextModel() { int cont = doModificationCheck(); - if(cont == CONTINUE && (handler.getModelMode() != GUIMultiModelHandler.PRISM_MODE)) - { - String[]selection = {"Yes", "No", "Cancel"}; + if (cont == CONTINUE && (handler.getModelMode() != GUIMultiModelHandler.PRISM_MODE)) { + String[] selection = { "Yes", "No", "Cancel" }; int selectionNo = -1; - selectionNo = optionPane("WARNING: This is a one way operation. Continue?", "Question", JOptionPane.OK_CANCEL_OPTION, JOptionPane.QUESTION_MESSAGE, selection, selection[0]); - switch(selectionNo) - { - case 0: handler.convertViewToPRISM(); break; + selectionNo = optionPane("WARNING: This is a one way operation. Continue?", "Question", JOptionPane.OK_CANCEL_OPTION, JOptionPane.QUESTION_MESSAGE, + selection, selection[0]); + switch (selectionNo) { + case 0: + handler.convertViewToPRISM(); + break; } } } - + protected void a_convertToPrismGraphicModel() { int cont = doModificationCheck(); - if(cont == CONTINUE && (handler.getModelMode() != GUIMultiModelHandler.GRAPHIC_MODE)) - { - String[]selection = {"Yes", "No", "Cancel"}; + if (cont == CONTINUE && (handler.getModelMode() != GUIMultiModelHandler.GRAPHIC_MODE)) { + String[] selection = { "Yes", "No", "Cancel" }; int selectionNo = -1; - selectionNo = optionPane("WARNING: This is a one way operation. Continue?", "Question", JOptionPane.OK_CANCEL_OPTION, JOptionPane.QUESTION_MESSAGE, selection, selection[0]); - switch(selectionNo) - { - case 0: handler.convertViewToGraphic(); break; + selectionNo = optionPane("WARNING: This is a one way operation. Continue?", "Question", JOptionPane.OK_CANCEL_OPTION, JOptionPane.QUESTION_MESSAGE, + selection, selection[0]); + switch (selectionNo) { + case 0: + handler.convertViewToGraphic(); + break; } } } - + protected void a_convertToPepaGraphicModel() { int cont = doModificationCheck(); - if(cont == CONTINUE && (handler.getModelMode() != GUIMultiModelHandler.PEPA_MODE)) - { - String[]selection = {"Yes", "No", "Cancel"}; + if (cont == CONTINUE && (handler.getModelMode() != GUIMultiModelHandler.PEPA_MODE)) { + String[] selection = { "Yes", "No", "Cancel" }; int selectionNo = -1; - selectionNo = optionPane("WARNING: This is a one way operation. Continue?", "Question", JOptionPane.OK_CANCEL_OPTION, JOptionPane.QUESTION_MESSAGE, selection, selection[0]); - switch(selectionNo) - { - case 0: handler.convertViewToPEPA(); break; + selectionNo = optionPane("WARNING: This is a one way operation. Continue?", "Question", JOptionPane.OK_CANCEL_OPTION, JOptionPane.QUESTION_MESSAGE, + selection, selection[0]); + switch (selectionNo) { + case 0: + handler.convertViewToPEPA(); + break; } } } - + + @SuppressWarnings("serial") private void setupActions() { newPRISMModel = new AbstractAction() @@ -426,7 +450,7 @@ public class GUIMultiModel extends GUIPlugin implements PrismSettingsListener newPRISMModel.putValue(Action.NAME, "PRISM model"); newPRISMModel.putValue(Action.SMALL_ICON, GUIPrism.getIconFromImage("smallFilePrism.png")); newPRISMModel.putValue(Action.ACCELERATOR_KEY, KeyStroke.getKeyStroke(KeyEvent.VK_N, Toolkit.getDefaultToolkit().getMenuShortcutKeyMask())); - + newGraphicModel = new AbstractAction() { public void actionPerformed(ActionEvent e) @@ -440,7 +464,7 @@ public class GUIMultiModel extends GUIPlugin implements PrismSettingsListener newGraphicModel.putValue(Action.MNEMONIC_KEY, new Integer(KeyEvent.VK_G)); newGraphicModel.putValue(Action.NAME, "Graphical PRISM model"); //newGraphicModel.putValue(Action.SMALL_ICON, GUIPrism.getIconFromImage("smallFileGraphic.png")); - + newPEPAModel = new AbstractAction() { public void actionPerformed(ActionEvent e) @@ -454,8 +478,7 @@ public class GUIMultiModel extends GUIPlugin implements PrismSettingsListener newPEPAModel.putValue(Action.MNEMONIC_KEY, new Integer(KeyEvent.VK_E)); newPEPAModel.putValue(Action.NAME, "PEPA model"); newPEPAModel.putValue(Action.SMALL_ICON, GUIPrism.getIconFromImage("smallFilePepa.png")); - - + loadModel = new AbstractAction() { public void actionPerformed(ActionEvent e) @@ -463,17 +486,20 @@ public class GUIMultiModel extends GUIPlugin implements PrismSettingsListener //do actions later //System.out.println("realised open action"); a_openModel(); - + } }; - loadModel.putValue(Action.LONG_DESCRIPTION, "Brings up a file loading dialogue and loads the file into the editor. The editor will change mode according to the format of the file. The loaded file is active for saving."); + loadModel + .putValue( + Action.LONG_DESCRIPTION, + "Brings up a file loading dialogue and loads the file into the editor. The editor will change mode according to the format of the file. The loaded file is active for saving."); //loadModel.putValue(Action.SHORT_DESCRIPTION, "Open Model"); loadModel.putValue(Action.MNEMONIC_KEY, new Integer(KeyEvent.VK_O)); loadModel.putValue(Action.NAME, "Open model..."); //loadModel.putValue(Action.ACTION_COMMAND_KEY, loadModel.putValue(Action.SMALL_ICON, GUIPrism.getIconFromImage("smallOpen.png")); loadModel.putValue(Action.ACCELERATOR_KEY, KeyStroke.getKeyStroke(KeyEvent.VK_O, Toolkit.getDefaultToolkit().getMenuShortcutKeyMask())); - + reloadModel = new AbstractAction() { public void actionPerformed(ActionEvent e) @@ -488,7 +514,7 @@ public class GUIMultiModel extends GUIPlugin implements PrismSettingsListener //loadModel.putValue(Action.ACTION_COMMAND_KEY, reloadModel.putValue(Action.SMALL_ICON, GUIPrism.getIconFromImage("smallReload.png")); reloadModel.putValue(Action.ACCELERATOR_KEY, KeyStroke.getKeyStroke(KeyEvent.VK_R, Toolkit.getDefaultToolkit().getMenuShortcutKeyMask())); - + saveModel = new AbstractAction() { public void actionPerformed(ActionEvent e) @@ -496,14 +522,15 @@ public class GUIMultiModel extends GUIPlugin implements PrismSettingsListener a_saveModel(); } }; - saveModel.putValue(Action.LONG_DESCRIPTION, "Brings up a file saving dialogue and saves the current text editor to the active file or to a new file. The saved file becomes active"); + saveModel.putValue(Action.LONG_DESCRIPTION, + "Brings up a file saving dialogue and saves the current text editor to the active file or to a new file. The saved file becomes active"); //saveModel.putValue(Action.SHORT_DESCRIPTION, "Save Model"); saveModel.putValue(Action.MNEMONIC_KEY, new Integer(KeyEvent.VK_S)); saveModel.putValue(Action.NAME, "Save model"); saveModel.putValue(Action.ACCELERATOR_KEY, KeyStroke.getKeyStroke(KeyEvent.VK_S, Toolkit.getDefaultToolkit().getMenuShortcutKeyMask())); //saveModel.putValue(Action.ACTION_COMMAND_KEY, saveModel.putValue(Action.SMALL_ICON, GUIPrism.getIconFromImage("smallSave.png")); - + saveAsModel = new AbstractAction() { public void actionPerformed(ActionEvent e) @@ -511,13 +538,14 @@ public class GUIMultiModel extends GUIPlugin implements PrismSettingsListener a_saveModelAs(); } }; - saveAsModel.putValue(Action.LONG_DESCRIPTION, "Brings up a file saving dialogue and saves the current text editor to a new file. The saved file becomes active"); + saveAsModel.putValue(Action.LONG_DESCRIPTION, + "Brings up a file saving dialogue and saves the current text editor to a new file. The saved file becomes active"); //saveAsModel.putValue(Action.SHORT_DESCRIPTION, "Save Model As..."); saveAsModel.putValue(Action.MNEMONIC_KEY, new Integer(KeyEvent.VK_A)); saveAsModel.putValue(Action.NAME, "Save model as..."); //saveAsModel.putValue(Action.ACTION_COMMAND_KEY, saveAsModel.putValue(Action.SMALL_ICON, GUIPrism.getIconFromImage("smallSaveAs.png")); - + parseModel = new AbstractAction() { public void actionPerformed(ActionEvent e) @@ -544,98 +572,163 @@ public class GUIMultiModel extends GUIPlugin implements PrismSettingsListener buildModel.putValue(Action.NAME, "Build model"); buildModel.putValue(Action.SMALL_ICON, GUIPrism.getIconFromImage("smallBuild.png")); buildModel.putValue(Action.ACCELERATOR_KEY, KeyStroke.getKeyStroke(KeyEvent.VK_F3, 0)); - - exportStatesPlain = new AbstractAction() { public void actionPerformed(ActionEvent e) { - a_exportBuildAs(GUIMultiModelHandler.STATES_EXPORT, Prism.EXPORT_PLAIN); } }; + + exportStatesPlain = new AbstractAction() + { + public void actionPerformed(ActionEvent e) + { + a_exportBuildAs(GUIMultiModelHandler.STATES_EXPORT, Prism.EXPORT_PLAIN); + } + }; exportStatesPlain.putValue(Action.LONG_DESCRIPTION, "Exports the reachable states to a plain text file"); exportStatesPlain.putValue(Action.MNEMONIC_KEY, new Integer(KeyEvent.VK_P)); exportStatesPlain.putValue(Action.NAME, "Plain text file"); exportStatesPlain.putValue(Action.SMALL_ICON, GUIPrism.getIconFromImage("smallFileText.png")); - - exportStatesMatlab = new AbstractAction() { public void actionPerformed(ActionEvent e) { - a_exportBuildAs(GUIMultiModelHandler.STATES_EXPORT, Prism.EXPORT_MATLAB); } }; + + exportStatesMatlab = new AbstractAction() + { + public void actionPerformed(ActionEvent e) + { + a_exportBuildAs(GUIMultiModelHandler.STATES_EXPORT, Prism.EXPORT_MATLAB); + } + }; exportStatesMatlab.putValue(Action.LONG_DESCRIPTION, "Exports the reachable states to a Matlab file"); exportStatesMatlab.putValue(Action.MNEMONIC_KEY, new Integer(KeyEvent.VK_M)); exportStatesMatlab.putValue(Action.NAME, "Matlab file"); exportStatesMatlab.putValue(Action.SMALL_ICON, GUIPrism.getIconFromImage("smallFileMatlab.png")); - - exportTransPlain = new AbstractAction() { public void actionPerformed(ActionEvent e) { - a_exportBuildAs(GUIMultiModelHandler.TRANS_EXPORT, Prism.EXPORT_PLAIN); } }; + + exportTransPlain = new AbstractAction() + { + public void actionPerformed(ActionEvent e) + { + a_exportBuildAs(GUIMultiModelHandler.TRANS_EXPORT, Prism.EXPORT_PLAIN); + } + }; exportTransPlain.putValue(Action.LONG_DESCRIPTION, "Exports the transition matrix to a plain text file"); exportTransPlain.putValue(Action.MNEMONIC_KEY, new Integer(KeyEvent.VK_P)); exportTransPlain.putValue(Action.NAME, "Plain text file"); exportTransPlain.putValue(Action.SMALL_ICON, GUIPrism.getIconFromImage("smallFileText.png")); - - exportTransMatlab = new AbstractAction() { public void actionPerformed(ActionEvent e) { - a_exportBuildAs(GUIMultiModelHandler.TRANS_EXPORT, Prism.EXPORT_MATLAB); } }; + + exportTransMatlab = new AbstractAction() + { + public void actionPerformed(ActionEvent e) + { + a_exportBuildAs(GUIMultiModelHandler.TRANS_EXPORT, Prism.EXPORT_MATLAB); + } + }; exportTransMatlab.putValue(Action.LONG_DESCRIPTION, "Exports the transition matrix to a Matlab file"); exportTransMatlab.putValue(Action.MNEMONIC_KEY, new Integer(KeyEvent.VK_M)); exportTransMatlab.putValue(Action.NAME, "Matlab file"); exportTransMatlab.putValue(Action.SMALL_ICON, GUIPrism.getIconFromImage("smallFileMatlab.png")); - - exportTransDot = new AbstractAction() { public void actionPerformed(ActionEvent e) { - a_exportBuildAs(GUIMultiModelHandler.TRANS_EXPORT, Prism.EXPORT_DOT); } }; + + exportTransDot = new AbstractAction() + { + public void actionPerformed(ActionEvent e) + { + a_exportBuildAs(GUIMultiModelHandler.TRANS_EXPORT, Prism.EXPORT_DOT); + } + }; exportTransDot.putValue(Action.LONG_DESCRIPTION, "Exports the transition matrix graph to a Dot file"); exportTransDot.putValue(Action.MNEMONIC_KEY, new Integer(KeyEvent.VK_D)); exportTransDot.putValue(Action.NAME, "Dot file"); exportTransDot.putValue(Action.SMALL_ICON, GUIPrism.getIconFromImage("smallFileDot.png")); - - exportTransDotStates = new AbstractAction() { public void actionPerformed(ActionEvent e) { - a_exportBuildAs(GUIMultiModelHandler.TRANS_EXPORT, Prism.EXPORT_DOT_STATES); } }; + + exportTransDotStates = new AbstractAction() + { + public void actionPerformed(ActionEvent e) + { + a_exportBuildAs(GUIMultiModelHandler.TRANS_EXPORT, Prism.EXPORT_DOT_STATES); + } + }; exportTransDotStates.putValue(Action.LONG_DESCRIPTION, "Exports the transition matrix graph to a Dot file (with states)"); exportTransDotStates.putValue(Action.MNEMONIC_KEY, new Integer(KeyEvent.VK_S)); exportTransDotStates.putValue(Action.NAME, "Dot file (with states)"); exportTransDotStates.putValue(Action.SMALL_ICON, GUIPrism.getIconFromImage("smallFileDot.png")); - - exportTransMRMC = new AbstractAction() { public void actionPerformed(ActionEvent e) { - a_exportBuildAs(GUIMultiModelHandler.TRANS_EXPORT, Prism.EXPORT_MRMC); } }; + + exportTransMRMC = new AbstractAction() + { + public void actionPerformed(ActionEvent e) + { + a_exportBuildAs(GUIMultiModelHandler.TRANS_EXPORT, Prism.EXPORT_MRMC); + } + }; exportTransMRMC.putValue(Action.LONG_DESCRIPTION, "Exports the transition matrix to a MRMC file"); exportTransMRMC.putValue(Action.MNEMONIC_KEY, new Integer(KeyEvent.VK_R)); exportTransMRMC.putValue(Action.NAME, "MRMC file"); exportTransMRMC.putValue(Action.SMALL_ICON, GUIPrism.getIconFromImage("smallFileText.png")); - - exportStateRewardsPlain = new AbstractAction() { public void actionPerformed(ActionEvent e) { - a_exportBuildAs(GUIMultiModelHandler.STATE_REWARDS_EXPORT, Prism.EXPORT_PLAIN); } }; + + exportStateRewardsPlain = new AbstractAction() + { + public void actionPerformed(ActionEvent e) + { + a_exportBuildAs(GUIMultiModelHandler.STATE_REWARDS_EXPORT, Prism.EXPORT_PLAIN); + } + }; exportStateRewardsPlain.putValue(Action.LONG_DESCRIPTION, "Exports the state rewards vector to a plain text file"); exportStateRewardsPlain.putValue(Action.MNEMONIC_KEY, new Integer(KeyEvent.VK_P)); exportStateRewardsPlain.putValue(Action.NAME, "Plain text file"); exportStateRewardsPlain.putValue(Action.SMALL_ICON, GUIPrism.getIconFromImage("smallFileText.png")); - - exportStateRewardsMatlab = new AbstractAction() { public void actionPerformed(ActionEvent e) { - a_exportBuildAs(GUIMultiModelHandler.STATE_REWARDS_EXPORT, Prism.EXPORT_MATLAB); } }; + + exportStateRewardsMatlab = new AbstractAction() + { + public void actionPerformed(ActionEvent e) + { + a_exportBuildAs(GUIMultiModelHandler.STATE_REWARDS_EXPORT, Prism.EXPORT_MATLAB); + } + }; exportStateRewardsMatlab.putValue(Action.LONG_DESCRIPTION, "Exports the state rewards vector to a Matlab file"); exportStateRewardsMatlab.putValue(Action.MNEMONIC_KEY, new Integer(KeyEvent.VK_M)); exportStateRewardsMatlab.putValue(Action.NAME, "Matlab file"); exportStateRewardsMatlab.putValue(Action.SMALL_ICON, GUIPrism.getIconFromImage("smallFileMatlab.png")); - - exportStateRewardsMRMC = new AbstractAction() { public void actionPerformed(ActionEvent e) { - a_exportBuildAs(GUIMultiModelHandler.STATE_REWARDS_EXPORT, Prism.EXPORT_MRMC); } }; + + exportStateRewardsMRMC = new AbstractAction() + { + public void actionPerformed(ActionEvent e) + { + a_exportBuildAs(GUIMultiModelHandler.STATE_REWARDS_EXPORT, Prism.EXPORT_MRMC); + } + }; exportStateRewardsMRMC.putValue(Action.LONG_DESCRIPTION, "Exports the state rewards vector graph to a MRMC file"); exportStateRewardsMRMC.putValue(Action.MNEMONIC_KEY, new Integer(KeyEvent.VK_R)); exportStateRewardsMRMC.putValue(Action.NAME, "MRMC file"); exportStateRewardsMRMC.putValue(Action.SMALL_ICON, GUIPrism.getIconFromImage("smallFileText.png")); - - exportTransRewardsPlain = new AbstractAction() { public void actionPerformed(ActionEvent e) { - a_exportBuildAs(GUIMultiModelHandler.TRANS_REWARDS_EXPORT, Prism.EXPORT_PLAIN); } }; + + exportTransRewardsPlain = new AbstractAction() + { + public void actionPerformed(ActionEvent e) + { + a_exportBuildAs(GUIMultiModelHandler.TRANS_REWARDS_EXPORT, Prism.EXPORT_PLAIN); + } + }; exportTransRewardsPlain.putValue(Action.LONG_DESCRIPTION, "Exports the transition rewards matrix to a plain text file"); exportTransRewardsPlain.putValue(Action.MNEMONIC_KEY, new Integer(KeyEvent.VK_P)); exportTransRewardsPlain.putValue(Action.NAME, "Plain text file"); exportTransRewardsPlain.putValue(Action.SMALL_ICON, GUIPrism.getIconFromImage("smallFileText.png")); - - exportTransRewardsMatlab = new AbstractAction() { public void actionPerformed(ActionEvent e) { - a_exportBuildAs(GUIMultiModelHandler.TRANS_REWARDS_EXPORT, Prism.EXPORT_MATLAB); } }; + + exportTransRewardsMatlab = new AbstractAction() + { + public void actionPerformed(ActionEvent e) + { + a_exportBuildAs(GUIMultiModelHandler.TRANS_REWARDS_EXPORT, Prism.EXPORT_MATLAB); + } + }; exportTransRewardsMatlab.putValue(Action.LONG_DESCRIPTION, "Exports the transition rewards matrix to a Matlab file"); exportTransRewardsMatlab.putValue(Action.MNEMONIC_KEY, new Integer(KeyEvent.VK_M)); exportTransRewardsMatlab.putValue(Action.NAME, "Matlab file"); exportTransRewardsMatlab.putValue(Action.SMALL_ICON, GUIPrism.getIconFromImage("smallFileMatlab.png")); - - exportTransRewardsMRMC = new AbstractAction() { public void actionPerformed(ActionEvent e) { - a_exportBuildAs(GUIMultiModelHandler.TRANS_REWARDS_EXPORT, Prism.EXPORT_MRMC); } }; + + exportTransRewardsMRMC = new AbstractAction() + { + public void actionPerformed(ActionEvent e) + { + a_exportBuildAs(GUIMultiModelHandler.TRANS_REWARDS_EXPORT, Prism.EXPORT_MRMC); + } + }; exportTransRewardsMRMC.putValue(Action.LONG_DESCRIPTION, "Exports the transition rewards matrix to a MRMC file"); exportTransRewardsMRMC.putValue(Action.MNEMONIC_KEY, new Integer(KeyEvent.VK_R)); exportTransRewardsMRMC.putValue(Action.NAME, "MRMC file"); exportTransRewardsMRMC.putValue(Action.SMALL_ICON, GUIPrism.getIconFromImage("smallFileText.png")); - + computeSS = new AbstractAction() { public void actionPerformed(ActionEvent e) @@ -649,7 +742,7 @@ public class GUIMultiModel extends GUIPlugin implements PrismSettingsListener computeSS.putValue(Action.NAME, "Steady-state probabilities"); computeSS.putValue(Action.SMALL_ICON, GUIPrism.getIconFromImage("smallSteadyState.png")); computeSS.putValue(Action.ACCELERATOR_KEY, KeyStroke.getKeyStroke(KeyEvent.VK_F4, 0)); - + computeTr = new AbstractAction() { public void actionPerformed(ActionEvent e) @@ -663,35 +756,55 @@ public class GUIMultiModel extends GUIPlugin implements PrismSettingsListener computeTr.putValue(Action.NAME, "Transient probabilities"); computeTr.putValue(Action.SMALL_ICON, GUIPrism.getIconFromImage("smallClockAnim1.png")); computeTr.putValue(Action.ACCELERATOR_KEY, KeyStroke.getKeyStroke(KeyEvent.VK_F4, KeyEvent.CTRL_DOWN_MASK)); - - viewStates = new AbstractAction() { public void actionPerformed(ActionEvent e) { - a_viewBuild(GUIMultiModelHandler.STATES_EXPORT, Prism.EXPORT_PLAIN); } }; + + viewStates = new AbstractAction() + { + public void actionPerformed(ActionEvent e) + { + a_viewBuild(GUIMultiModelHandler.STATES_EXPORT, Prism.EXPORT_PLAIN); + } + }; viewStates.putValue(Action.LONG_DESCRIPTION, "Print the reachable states to the log"); viewStates.putValue(Action.MNEMONIC_KEY, new Integer(KeyEvent.VK_S)); viewStates.putValue(Action.NAME, "States"); viewStates.putValue(Action.SMALL_ICON, GUIPrism.getIconFromImage("smallStates.png")); - - viewTrans = new AbstractAction() { public void actionPerformed(ActionEvent e) { - a_viewBuild(GUIMultiModelHandler.TRANS_EXPORT, Prism.EXPORT_PLAIN); } }; + + viewTrans = new AbstractAction() + { + public void actionPerformed(ActionEvent e) + { + a_viewBuild(GUIMultiModelHandler.TRANS_EXPORT, Prism.EXPORT_PLAIN); + } + }; viewTrans.putValue(Action.LONG_DESCRIPTION, "Print the transition matrix to the log"); viewTrans.putValue(Action.MNEMONIC_KEY, new Integer(KeyEvent.VK_T)); viewTrans.putValue(Action.NAME, "Transition matrix"); viewTrans.putValue(Action.SMALL_ICON, GUIPrism.getIconFromImage("smallMatrix.png")); - - viewStateRewards = new AbstractAction() { public void actionPerformed(ActionEvent e) { - a_viewBuild(GUIMultiModelHandler.STATE_REWARDS_EXPORT, Prism.EXPORT_PLAIN); } }; + + viewStateRewards = new AbstractAction() + { + public void actionPerformed(ActionEvent e) + { + a_viewBuild(GUIMultiModelHandler.STATE_REWARDS_EXPORT, Prism.EXPORT_PLAIN); + } + }; viewStateRewards.putValue(Action.LONG_DESCRIPTION, "Print the state rewards to the log"); viewStateRewards.putValue(Action.MNEMONIC_KEY, new Integer(KeyEvent.VK_R)); viewStateRewards.putValue(Action.NAME, "State rewards"); viewStateRewards.putValue(Action.SMALL_ICON, GUIPrism.getIconFromImage("smallStates.png")); - - viewTransRewards = new AbstractAction() { public void actionPerformed(ActionEvent e) { - a_viewBuild(GUIMultiModelHandler.TRANS_REWARDS_EXPORT, Prism.EXPORT_PLAIN); } }; + + viewTransRewards = new AbstractAction() + { + public void actionPerformed(ActionEvent e) + { + a_viewBuild(GUIMultiModelHandler.TRANS_REWARDS_EXPORT, Prism.EXPORT_PLAIN); + } + }; viewTransRewards.putValue(Action.LONG_DESCRIPTION, "Print the transition rewards to the log"); viewTransRewards.putValue(Action.MNEMONIC_KEY, new Integer(KeyEvent.VK_E)); viewTransRewards.putValue(Action.NAME, "Transition rewards"); viewTransRewards.putValue(Action.SMALL_ICON, GUIPrism.getIconFromImage("smallMatrix.png")); - + viewPrismCode = new AbstractAction() { public void actionPerformed(ActionEvent e) @@ -704,107 +817,88 @@ public class GUIMultiModel extends GUIPlugin implements PrismSettingsListener viewPrismCode.putValue(Action.NAME, "Parsed PRISM model"); viewPrismCode.putValue(Action.SMALL_ICON, GUIPrism.getIconFromImage("smallFilePrism.png")); } - + //Required to be a GUIPlugin: - + public boolean displaysTab() { return true; } - + public JMenu getMenu() { return modelMenu; } - + public String getTabText() { return "Model"; } - + public JToolBar getToolBar() { return null; } - + public String getXMLIDTag() { return ""; } - + public Object getXMLSaveTree() { return null; } - + public void loadXML(Object c) { - + } - + // if return value is true, event should not be passed on to any more listeners - + public boolean processGUIEvent(GUIEvent e) { - if(e instanceof userinterface.properties.GUIPropertiesEvent) - { - if(e.getID() == userinterface.properties.GUIPropertiesEvent.REQUEST_MODEL_BUILD) - { - handler.requestBuild(((userinterface.properties.GUIPropertiesEvent)e).getBuildValues(), false); - } - else if(e.getID() == userinterface.properties.GUIPropertiesEvent.REQUEST_MODEL_PARSE) - { + if (e instanceof userinterface.properties.GUIPropertiesEvent) { + if (e.getID() == userinterface.properties.GUIPropertiesEvent.REQUEST_MODEL_PARSE) { handler.requestParse(false); } - } - else if(e instanceof GUIClipboardEvent && super.getGUI().getFocussedPlugin() == this) - { - GUIClipboardEvent ce = (GUIClipboardEvent)e; - if(ce.getComponent() == this) - { + } else if (e instanceof GUIClipboardEvent && super.getGUI().getFocussedPlugin() == this) { + GUIClipboardEvent ce = (GUIClipboardEvent) e; + if (ce.getComponent() == this) { int id = ce.getID(); - if(id == GUIClipboardEvent.CUT) + if (id == GUIClipboardEvent.CUT) handler.cut(); - else if(id == GUIClipboardEvent.COPY) + else if (id == GUIClipboardEvent.COPY) handler.copy(); - else if(id == GUIClipboardEvent.PASTE) + else if (id == GUIClipboardEvent.PASTE) handler.paste(); - else if(id == GUIClipboardEvent.DELETE) + else if (id == GUIClipboardEvent.DELETE) handler.delete(); - else if(id == GUIClipboardEvent.SELECT_ALL) + else if (id == GUIClipboardEvent.SELECT_ALL) handler.selectAll(); - else if(id == GUIClipboardEvent.UNDO) + else if (id == GUIClipboardEvent.UNDO) handler.undo(); - else if(id == GUIClipboardEvent.REDO) + else if (id == GUIClipboardEvent.REDO) handler.redo(); - + } - } - else if(e instanceof GUIComputationEvent) - { - if(e.getID() == GUIComputationEvent.COMPUTATION_START) - { + } else if (e instanceof GUIComputationEvent) { + if (e.getID() == GUIComputationEvent.COMPUTATION_START) { computing = true; doEnables(); selectionChangeHandler.notifyListeners(new GUIEvent(1)); - } - else if(e.getID() == GUIComputationEvent.COMPUTATION_DONE) - { + } else if (e.getID() == GUIComputationEvent.COMPUTATION_DONE) { computing = false; doEnables(); selectionChangeHandler.notifyListeners(new GUIEvent(1)); - } - else if(e.getID() == GUIComputationEvent.COMPUTATION_ERROR) - { + } else if (e.getID() == GUIComputationEvent.COMPUTATION_ERROR) { computing = false; doEnables(); selectionChangeHandler.notifyListeners(new GUIEvent(1)); } - } - else if (e instanceof GUIExitEvent) - { - if(e.getID() == GUIExitEvent.REQUEST_EXIT) - { + } else if (e instanceof GUIExitEvent) { + if (e.getID() == GUIExitEvent.REQUEST_EXIT) { if (doModificationCheck() != CONTINUE) { notifyEventListeners(new GUIExitEvent(GUIExitEvent.CANCEL_EXIT)); return true; @@ -813,7 +907,7 @@ public class GUIMultiModel extends GUIPlugin implements PrismSettingsListener } return false; } - + private JMenu initExportMenu() { JMenu exportMenu = new JMenu("Export"); @@ -850,7 +944,7 @@ public class GUIMultiModel extends GUIPlugin implements PrismSettingsListener exportMenu.add(exportTransRewardsMenu); return exportMenu; } - + private JMenu initViewMenu() { JMenu viewMenu = new JMenu("View"); @@ -863,7 +957,7 @@ public class GUIMultiModel extends GUIPlugin implements PrismSettingsListener viewMenu.add(viewPrismCode); return viewMenu; } - + private JMenu initComputeMenu() { JMenu computeMenu = new JMenu("Compute"); @@ -873,16 +967,16 @@ public class GUIMultiModel extends GUIPlugin implements PrismSettingsListener computeMenu.add(computeTr); return computeMenu; } - + private void initComponents() { setupActions(); - + modelMenu = new JMenu("Model"); exportMenu = initExportMenu(); viewMenu = initViewMenu(); - computeMenu = initComputeMenu(); - + computeMenu = initComputeMenu(); + JPanel topPanel = new JPanel(); { fileLabel = new JLabel(); @@ -891,20 +985,21 @@ public class GUIMultiModel extends GUIPlugin implements PrismSettingsListener fileLabel.setBorder(new javax.swing.border.EtchedBorder()); fileLabel.setMinimumSize(new java.awt.Dimension(40, 25)); } - + //progress = new JProgressBar(0, 100); topPanel.setLayout(new BorderLayout()); handler = new GUIMultiModelHandler(this); //topPanel.add(progress, BorderLayout.WEST); - topPanel.add(fileLabel,BorderLayout.NORTH); - topPanel.add(handler,BorderLayout.CENTER); + topPanel.add(fileLabel, BorderLayout.NORTH); + topPanel.add(handler, BorderLayout.CENTER); } - + newMenu = new JMenu("New"); newMenu.setMnemonic('N'); newMenu.setIcon(GUIPrism.getIconFromImage("smallNew.png")); newMenu.add(newPRISMModel); - if (GM_ENABLED) newMenu.add(newGraphicModel); + if (GM_ENABLED) + newMenu.add(newGraphicModel); newMenu.add(newPEPAModel); modelMenu.add(newMenu); modelMenu.add(new JSeparator()); @@ -918,27 +1013,29 @@ public class GUIMultiModel extends GUIPlugin implements PrismSettingsListener modelMenu.add(parseModel); modelMenu.add(buildModel); modelMenu.add(new JSeparator()); - + modelMenu.add(exportMenu); - + modelMenu.add(viewMenu); - + modelMenu.add(computeMenu); - + popup = new JPopupMenu(); { popup.add(parseModel); popup.add(buildModel); popup.add(viewPrismCode); } - - modelFilters = new GUIPrismFileFilter[GM_ENABLED?3:2]; + + modelFilters = new GUIPrismFileFilter[GM_ENABLED ? 3 : 2]; modelFilters[FILTER_PRISM_MODEL] = new GUIPrismFileFilter("PRISM models (*.pm, *.nm, *.sm)"); modelFilters[FILTER_PRISM_MODEL].addExtension("pm"); modelFilters[FILTER_PRISM_MODEL].addExtension("nm"); modelFilters[FILTER_PRISM_MODEL].addExtension("sm"); - if (GM_ENABLED) modelFilters[FILTER_GRAPHIC_MODEL] = new GUIPrismFileFilter("Graphical PRISM models (*.gm)"); - if (GM_ENABLED) modelFilters[FILTER_GRAPHIC_MODEL].addExtension("gm"); + if (GM_ENABLED) + modelFilters[FILTER_GRAPHIC_MODEL] = new GUIPrismFileFilter("Graphical PRISM models (*.gm)"); + if (GM_ENABLED) + modelFilters[FILTER_GRAPHIC_MODEL].addExtension("gm"); modelFilters[FILTER_PEPA_MODEL] = new GUIPrismFileFilter("PEPA models (*.pepa)"); modelFilters[FILTER_PEPA_MODEL].addExtension("pepa"); textFilter = new GUIPrismFileFilter[3]; @@ -954,60 +1051,64 @@ public class GUIMultiModel extends GUIPlugin implements PrismSettingsListener dotFilter = new GUIPrismFileFilter[1]; dotFilter[0] = new GUIPrismFileFilter("Dot files (*.dot)"); dotFilter[0].addExtension("dot"); - - - + setLayout(new BorderLayout()); add(topPanel, BorderLayout.CENTER); - + doEnables(); } - + public OptionsPanel getOptions() { return null; - } - - public void notifySettings(PrismSettings settings) - { - //System.out.println("model notifySettings called"); - handler.notifySettings(settings); - - repaint(); - } + } + + public void notifySettings(PrismSettings settings) + { + //System.out.println("model notifySettings called"); + handler.notifySettings(settings); + + repaint(); + } @Override - public GUIUndoManager getUndoManager() + public GUIUndoManager getUndoManager() { return handler.getUndoManager(); } @Override - public boolean canDoClipBoardAction(Action action) { + public boolean canDoClipBoardAction(Action action) + { // TODO Auto-generated method stub if (computing) return false; - + return handler.canDoClipBoardAction(action); } - public AbstractAction getParseModel() { + public AbstractAction getParseModel() + { return parseModel; } - public AbstractAction getBuildModel() { + public AbstractAction getBuildModel() + { return buildModel; } - public JMenu getViewMenu() { + public JMenu getViewMenu() + { return initViewMenu(); } - public JMenu getExportMenu() { + public JMenu getExportMenu() + { return initExportMenu(); } - public JMenu getComputeMenu() { + public JMenu getComputeMenu() + { return initComputeMenu(); - } + } } diff --git a/prism/src/userinterface/model/GUIMultiModelHandler.java b/prism/src/userinterface/model/GUIMultiModelHandler.java index c5fa525b..7f382d64 100644 --- a/prism/src/userinterface/model/GUIMultiModelHandler.java +++ b/prism/src/userinterface/model/GUIMultiModelHandler.java @@ -29,6 +29,9 @@ package userinterface.model; import javax.swing.*; import javax.swing.border.*; + +import com.sun.tools.internal.ws.wsdl.document.jaxws.Exception; + import java.awt.*; import java.io.*; import parser.*; @@ -40,1509 +43,1422 @@ import userinterface.model.computation.*; import userinterface.*; import userinterface.util.*; -public class GUIMultiModelHandler extends JPanel +@SuppressWarnings("serial") +public class GUIMultiModelHandler extends JPanel implements PrismModelListener { - //Constants - public static final int GRAPHIC_MODE = 3; - public static final int PRISM_MODE = 1; - public static final int PEPA_MODE = 2; - + //Constants + public static final int GRAPHIC_MODE = 3; + public static final int PRISM_MODE = 1; + public static final int PEPA_MODE = 2; + // export entity types - public static final int TRANS_EXPORT = 1; - public static final int STATE_REWARDS_EXPORT = 2; - public static final int TRANS_REWARDS_EXPORT = 3; - public static final int STATES_EXPORT = 4; - - public static final int DEFAULT_WAIT = 1000; - - private GUIMultiModel theModel; - private GUIMultiModelTree tree; - private GUIModelEditor editor; - - // State - private int currentMode; - private boolean modified; - private boolean modifiedSinceBuild; - private boolean modifiedSinceParse; - private File activeFile; - private ModulesFile parsedModel; - private Model builtModel; - private Values lastBuildValues = null; - //tosettings: private boolean isAutoParse = true; - private boolean busy = false; - //tosettings: private boolean isSwitchOnLarge = true; //now model.autoManual - //tosettings: private int autoParseWaitTime = DEFAULT_WAIT; - - //Options (these are synchronised with those in PrismSettings, - // they are here for speed) - private boolean autoParseFast; - private int parseWaitTimeFast; - - private Font prismEditorFontFast; - private Color prismEditorColourFast; - private Color prismEditorBGColourFast; - - private Style prismEditorNumericFast = Style.defaultStyle(); - private Style prismEditorVariableFast = Style.defaultStyle(); - private Style prismEditorKeywordFast = Style.defaultStyle(); - private Style prismEditorCommentFast = Style.defaultStyle(); - - private Font pepaEditorFontFast; - private Color pepaEditorColourFast; - private Color pepaEditorBGColourFast; - - private Style pepaEditorCommentFast = Style.defaultStyle(); - - //Modification Parse updater - private WaitParseThread waiter; - private boolean parsing= false; - private boolean parseAfterParse=false; - - private String lastError; - - private boolean buildAfterReceiveParseNotification = false; - private boolean exportAfterReceiveParseNotification = false; - private boolean exportAfterReceiveBuildNotification = false; - private boolean computeSSAfterReceiveParseNotification = false; - private boolean computeSSAfterReceiveBuildNotification = false; - private boolean computeTransientAfterReceiveParseNotification = false; - private boolean computeTransientAfterReceiveBuildNotification = false; - private int exportEntity = 0; + public static final int TRANS_EXPORT = 1; + public static final int STATE_REWARDS_EXPORT = 2; + public static final int TRANS_REWARDS_EXPORT = 3; + public static final int STATES_EXPORT = 4; + + public static final int DEFAULT_WAIT = 1000; + + private GUIMultiModel theModel; + private GUIMultiModelTree tree; + private GUIModelEditor editor; + private Prism prism; + + // State + private int currentMode; + private boolean modified; + private boolean modifiedSinceBuild; + private boolean modifiedSinceParse; + private File activeFile; + private ModulesFile parsedModel; + private Values lastMFConstants = null; + private PrismException lastBuildError = null; + //tosettings: private boolean isAutoParse = true; + private boolean busy = false; + //tosettings: private boolean isSwitchOnLarge = true; //now model.autoManual + //tosettings: private int autoParseWaitTime = DEFAULT_WAIT; + + // Options (these are synchronised with those in PrismSettings, they are here for speed) + private boolean autoParseFast; + private int parseWaitTimeFast; + + private Font prismEditorFontFast; + private Color prismEditorColourFast; + private Color prismEditorBGColourFast; + + private Style prismEditorNumericFast = Style.defaultStyle(); + private Style prismEditorVariableFast = Style.defaultStyle(); + private Style prismEditorKeywordFast = Style.defaultStyle(); + private Style prismEditorCommentFast = Style.defaultStyle(); + + private Font pepaEditorFontFast; + private Color pepaEditorColourFast; + private Color pepaEditorBGColourFast; + + private Style pepaEditorCommentFast = Style.defaultStyle(); + + // Modification Parse updater + private WaitParseThread waiter; + private boolean parsing = false; + private boolean parseAfterParse = false; + + private String lastError; + + private boolean buildAfterReceiveParseNotification = false; + private boolean exportAfterReceiveParseNotification = false; + private boolean computeSSAfterReceiveParseNotification = false; + private boolean computeTransientAfterReceiveParseNotification = false; + private int exportEntity = 0; private int exportType = Prism.EXPORT_PLAIN; - private File exportFile = null; + private File exportFile = null; private double transientTime; - - //GUI - private JSplitPane splitter, graphicalSplitter; - private JPanel leftHandSide, treeAndBuild; - private PropertyTable graphicalProperties; - private PropertyTableModel graphicalPropModel; - - private JLabel builtNoStates, builtNoInitStates, builtNoTransitions; - - /** Creates a new instance of GUIMultiModelHandler */ - public GUIMultiModelHandler(GUIMultiModel theModel) - { - super(); - this.theModel = theModel; - - waiter = new WaitParseThread(DEFAULT_WAIT,this); - editor = new GUITextModelEditor("", this); - tree = new GUIMultiModelTree(this); - splitter = new JSplitPane(); - - initComponents(); - newPRISMModel(); - //splitter.setDividerLocation(0); - //splitter.setLastDividerLocation(200); - - notifySettings(theModel.getPrism().getSettings()); - - splitter.setBorder(null); - - setBorder(new EmptyBorder(5, 5, 5, 5)); - } - - // Initialisation of GUI components - private void initComponents() - { - treeAndBuild = new JPanel(); - JPanel topLeft = new JPanel(); - topLeft.setLayout(new BorderLayout()); - topLeft.add(tree, BorderLayout.CENTER); - JPanel innerBottomLeft = new JPanel(new BorderLayout()); - innerBottomLeft.setBorder(new CompoundBorder(new EmptyBorder(5,0,0,0),new TitledBorder("Built Model"))); - //JToolBar bar = new JToolBar(); - //bar.setFloatable(false); - //JButton but = new JButton(buildModel); - //but.setText("Build Model"); - //bar.add(but); - //bar.add(buildModel); - JPanel buildPane = new JPanel(new GridLayout(3,2,5,5)); - - JLabel statesLabel = new JLabel("States:"); - statesLabel.setFont(statesLabel.getFont().deriveFont(Font.BOLD)); - statesLabel.setHorizontalAlignment(JLabel.RIGHT); - - builtNoStates = new JLabel("..."); - - JLabel initStatesLabel = new JLabel("Initial states:"); - initStatesLabel.setFont(initStatesLabel.getFont().deriveFont(Font.BOLD)); - initStatesLabel.setHorizontalAlignment(JLabel.RIGHT); - - builtNoInitStates = new JLabel("..."); - - JLabel transLabel = new JLabel("Transitions:"); - transLabel.setFont(transLabel.getFont().deriveFont(Font.BOLD)); - transLabel.setHorizontalAlignment(JLabel.RIGHT); - - builtNoTransitions = new JLabel("..."); - - buildPane.add(statesLabel); - buildPane.add(builtNoStates); - buildPane.add(initStatesLabel); - buildPane.add(builtNoInitStates); - buildPane.add(transLabel); - buildPane.add(builtNoTransitions); - - //buildPane.setPreferredSize(new Dimension(250, 40)); - //buildPane.setMaximumSize(new Dimension(2000, 40)); - buildPane.setBorder(new EmptyBorder(5,5,5,5)); - //bottomLeft.add(bar, BorderLayout.NORTH); - innerBottomLeft.add(buildPane, BorderLayout.CENTER); - treeAndBuild.setLayout(new BorderLayout()); - treeAndBuild.add(topLeft, BorderLayout.CENTER); - treeAndBuild.add(innerBottomLeft, BorderLayout.SOUTH); - treeAndBuild.setBorder(new EmptyBorder(0,0,0,5)); - splitter.setOrientation(JSplitPane.HORIZONTAL_SPLIT); - - leftHandSide = new JPanel(); - leftHandSide.setLayout(new BorderLayout()); - - leftHandSide.add(treeAndBuild, BorderLayout.CENTER); - - graphicalPropModel = new PropertyTableModel(); - graphicalProperties = new PropertyTable(graphicalPropModel); //not used initially - - splitter.setLeftComponent(leftHandSide); - - splitter.setRightComponent(editor); - splitter.setDividerLocation(0.5); - splitter.setOneTouchExpandable(true); - setLayout(new BorderLayout()); - add(splitter, BorderLayout.CENTER); - } - - private void swapToGraphic() - { - int splitterPos = splitter.getDividerLocation(); - leftHandSide.remove(treeAndBuild); - graphicalSplitter = new JSplitPane(); - { - graphicalSplitter.setTopComponent(treeAndBuild); - JPanel pan = new JPanel(); - pan.setBorder(new TitledBorder("Properties")); - pan.setLayout(new BorderLayout()); - pan.add(graphicalProperties, BorderLayout.CENTER); - graphicalSplitter.setBottomComponent(pan); - } - - graphicalSplitter.setOneTouchExpandable(true); - graphicalSplitter.setOrientation(JSplitPane.VERTICAL_SPLIT); - graphicalSplitter.setDividerSize(8); - graphicalSplitter.setResizeWeight(1); - - - leftHandSide.add(graphicalSplitter, BorderLayout.CENTER); - - int position = (int)(leftHandSide.getHeight() * 0.5); - graphicalSplitter.setDividerLocation(position); - splitter.setDividerLocation(splitterPos); - } - - private void swapFromGraphic() - { - int splitterPos = splitter.getDividerLocation(); - - if(graphicalSplitter != null) - leftHandSide.remove(graphicalSplitter); - leftHandSide.add(treeAndBuild, BorderLayout.CENTER); - - splitter.setDividerLocation(splitterPos); - } - - // New model... - - public void newPRISMModel() - { - activeFile = null; - modified = false; - modifiedSinceParse = false; - modifiedSinceBuild = false; - parsedModel = null; - setBuiltModel(null,null); - if(currentMode == PRISM_MODE) - { - editor.newModel(); - } - else if(currentMode == GRAPHIC_MODE) - { - editor = new GUITextModelEditor("", this); - editor.newModel(); - splitter.setRightComponent(editor); - swapFromGraphic(); - } - else - { - editor = new GUITextModelEditor("", this); - editor.newModel(); - splitter.setRightComponent(editor); - } - tree.newTree(false); - tree.update(parsedModel); - currentMode = PRISM_MODE; - theModel.doEnables(); - lastError = ""; - theModel.notifyEventListeners(new GUIModelEvent(GUIModelEvent.NEW_MODEL)); - theModel.notifyEventListeners(new GUIModelEvent(GUIModelEvent.NEW_LOAD_NOT_RELOAD_MODEL)); - } - - public void newPEPAModel() - { - activeFile = null; - modified = false; - modifiedSinceBuild = false; - modifiedSinceParse = false; - parsedModel = null; - setBuiltModel(null,null); - if(currentMode == PEPA_MODE) - { - editor.newModel(); - } - else if(currentMode == GRAPHIC_MODE) - { - //editor = new GUIPepaModelEditor(this); - editor.newModel(); - //splitter.setRightComponent(editor); - swapFromGraphic(); - } - else - { - //editor = new GUIPepaModelEditor(this); - editor.newModel(); - //splitter.setRightComponent(editor); - } - tree.newTree(false); - tree.update(parsedModel); - currentMode = PEPA_MODE; - theModel.doEnables(); - lastError = ""; - theModel.notifyEventListeners(new GUIModelEvent(GUIModelEvent.NEW_MODEL)); - theModel.notifyEventListeners(new GUIModelEvent(GUIModelEvent.NEW_LOAD_NOT_RELOAD_MODEL)); - } - - public void newGraphicModel() - { - activeFile = null; - modified = false; - modifiedSinceBuild = false; - modifiedSinceParse = false; - parsedModel = null; - setBuiltModel(null,null); - if(currentMode == GRAPHIC_MODE) - { - editor.newModel(); - } - else - { - editor = new GUIGraphicModelEditor(this, tree, graphicalPropModel); - editor.newModel(); - splitter.setRightComponent(editor); - ((GUIGraphicModelEditor)editor).initialSplitterPosition((int)(getHeight()*0.9)); - swapToGraphic(); - } - tree.newTree(true); - tree.update(parsedModel); - currentMode = GRAPHIC_MODE; - theModel.doEnables(); - lastError = ""; - theModel.notifyEventListeners(new GUIModelEvent(GUIModelEvent.NEW_MODEL)); - theModel.notifyEventListeners(new GUIModelEvent(GUIModelEvent.NEW_LOAD_NOT_RELOAD_MODEL)); - } - - // Conversions... (not used) - - public void convertViewToPRISM() - { - theModel.doEnables(); - } - - public void convertViewToPEPA()//dummy dummy dummy - { - theModel.doEnables(); - } - - public void convertViewToGraphic()//dummy dummy dummy - { - theModel.doEnables(); - } - - // Load model... - - public void loadModel(File f) - { loadModel(f, true); } - - public void loadModel(File f, boolean inBackground) - { + + // GUI + private JSplitPane splitter, graphicalSplitter; + private JPanel leftHandSide, treeAndBuild; + private PropertyTable graphicalProperties; + private PropertyTableModel graphicalPropModel; + + private JLabel builtNoStates, builtNoInitStates, builtNoTransitions; + + /** Creates a new instance of GUIMultiModelHandler */ + public GUIMultiModelHandler(GUIMultiModel theModel) + { + super(); + this.theModel = theModel; + prism = theModel.getPrism(); + prism.addModelListener(this); + + waiter = new WaitParseThread(DEFAULT_WAIT, this); + editor = new GUITextModelEditor("", this); + tree = new GUIMultiModelTree(this); + splitter = new JSplitPane(); + + initComponents(); + newPRISMModel(); + //splitter.setDividerLocation(0); + //splitter.setLastDividerLocation(200); + + notifySettings(theModel.getPrism().getSettings()); + + splitter.setBorder(null); + + setBorder(new EmptyBorder(5, 5, 5, 5)); + } + + // Initialisation of GUI components + private void initComponents() + { + treeAndBuild = new JPanel(); + JPanel topLeft = new JPanel(); + topLeft.setLayout(new BorderLayout()); + topLeft.add(tree, BorderLayout.CENTER); + JPanel innerBottomLeft = new JPanel(new BorderLayout()); + innerBottomLeft.setBorder(new CompoundBorder(new EmptyBorder(5, 0, 0, 0), new TitledBorder("Built Model"))); + //JToolBar bar = new JToolBar(); + //bar.setFloatable(false); + //JButton but = new JButton(buildModel); + //but.setText("Build Model"); + //bar.add(but); + //bar.add(buildModel); + JPanel buildPane = new JPanel(new GridLayout(3, 2, 5, 5)); + + JLabel statesLabel = new JLabel("States:"); + statesLabel.setFont(statesLabel.getFont().deriveFont(Font.BOLD)); + statesLabel.setHorizontalAlignment(JLabel.RIGHT); + + builtNoStates = new JLabel("..."); + + JLabel initStatesLabel = new JLabel("Initial states:"); + initStatesLabel.setFont(initStatesLabel.getFont().deriveFont(Font.BOLD)); + initStatesLabel.setHorizontalAlignment(JLabel.RIGHT); + + builtNoInitStates = new JLabel("..."); + + JLabel transLabel = new JLabel("Transitions:"); + transLabel.setFont(transLabel.getFont().deriveFont(Font.BOLD)); + transLabel.setHorizontalAlignment(JLabel.RIGHT); + + builtNoTransitions = new JLabel("..."); + + buildPane.add(statesLabel); + buildPane.add(builtNoStates); + buildPane.add(initStatesLabel); + buildPane.add(builtNoInitStates); + buildPane.add(transLabel); + buildPane.add(builtNoTransitions); + + //buildPane.setPreferredSize(new Dimension(250, 40)); + //buildPane.setMaximumSize(new Dimension(2000, 40)); + buildPane.setBorder(new EmptyBorder(5, 5, 5, 5)); + //bottomLeft.add(bar, BorderLayout.NORTH); + innerBottomLeft.add(buildPane, BorderLayout.CENTER); + treeAndBuild.setLayout(new BorderLayout()); + treeAndBuild.add(topLeft, BorderLayout.CENTER); + treeAndBuild.add(innerBottomLeft, BorderLayout.SOUTH); + treeAndBuild.setBorder(new EmptyBorder(0, 0, 0, 5)); + splitter.setOrientation(JSplitPane.HORIZONTAL_SPLIT); + + leftHandSide = new JPanel(); + leftHandSide.setLayout(new BorderLayout()); + + leftHandSide.add(treeAndBuild, BorderLayout.CENTER); + + graphicalPropModel = new PropertyTableModel(); + graphicalProperties = new PropertyTable(graphicalPropModel); //not used initially + + splitter.setLeftComponent(leftHandSide); + + splitter.setRightComponent(editor); + splitter.setDividerLocation(0.5); + splitter.setOneTouchExpandable(true); + setLayout(new BorderLayout()); + add(splitter, BorderLayout.CENTER); + } + + private void swapToGraphic() + { + int splitterPos = splitter.getDividerLocation(); + leftHandSide.remove(treeAndBuild); + graphicalSplitter = new JSplitPane(); + { + graphicalSplitter.setTopComponent(treeAndBuild); + JPanel pan = new JPanel(); + pan.setBorder(new TitledBorder("Properties")); + pan.setLayout(new BorderLayout()); + pan.add(graphicalProperties, BorderLayout.CENTER); + graphicalSplitter.setBottomComponent(pan); + } + + graphicalSplitter.setOneTouchExpandable(true); + graphicalSplitter.setOrientation(JSplitPane.VERTICAL_SPLIT); + graphicalSplitter.setDividerSize(8); + graphicalSplitter.setResizeWeight(1); + + leftHandSide.add(graphicalSplitter, BorderLayout.CENTER); + + int position = (int) (leftHandSide.getHeight() * 0.5); + graphicalSplitter.setDividerLocation(position); + splitter.setDividerLocation(splitterPos); + } + + private void swapFromGraphic() + { + int splitterPos = splitter.getDividerLocation(); + + if (graphicalSplitter != null) + leftHandSide.remove(graphicalSplitter); + leftHandSide.add(treeAndBuild, BorderLayout.CENTER); + + splitter.setDividerLocation(splitterPos); + } + + // New model... + + public void newPRISMModel() + { + activeFile = null; + modified = false; + modifiedSinceParse = false; + modifiedSinceBuild = false; + parsedModel = null; + updateBuiltModelDisplay(); + if (currentMode == PRISM_MODE) { + editor.newModel(); + } else if (currentMode == GRAPHIC_MODE) { + editor = new GUITextModelEditor("", this); + editor.newModel(); + splitter.setRightComponent(editor); + swapFromGraphic(); + } else { + editor = new GUITextModelEditor("", this); + editor.newModel(); + splitter.setRightComponent(editor); + } + tree.newTree(false); + tree.update(parsedModel); + currentMode = PRISM_MODE; + theModel.doEnables(); + lastError = ""; + theModel.notifyEventListeners(new GUIModelEvent(GUIModelEvent.NEW_MODEL)); + theModel.notifyEventListeners(new GUIModelEvent(GUIModelEvent.NEW_LOAD_NOT_RELOAD_MODEL)); + } + + public void newPEPAModel() + { + activeFile = null; + modified = false; + modifiedSinceBuild = false; + modifiedSinceParse = false; + parsedModel = null; + updateBuiltModelDisplay(); + if (currentMode == PEPA_MODE) { + editor.newModel(); + } else if (currentMode == GRAPHIC_MODE) { + //editor = new GUIPepaModelEditor(this); + editor.newModel(); + //splitter.setRightComponent(editor); + swapFromGraphic(); + } else { + //editor = new GUIPepaModelEditor(this); + editor.newModel(); + //splitter.setRightComponent(editor); + } + tree.newTree(false); + tree.update(parsedModel); + currentMode = PEPA_MODE; + theModel.doEnables(); + lastError = ""; + theModel.notifyEventListeners(new GUIModelEvent(GUIModelEvent.NEW_MODEL)); + theModel.notifyEventListeners(new GUIModelEvent(GUIModelEvent.NEW_LOAD_NOT_RELOAD_MODEL)); + } + + public void newGraphicModel() + { + activeFile = null; + modified = false; + modifiedSinceBuild = false; + modifiedSinceParse = false; + parsedModel = null; + updateBuiltModelDisplay(); + if (currentMode == GRAPHIC_MODE) { + editor.newModel(); + } else { + editor = new GUIGraphicModelEditor(this, tree, graphicalPropModel); + editor.newModel(); + splitter.setRightComponent(editor); + ((GUIGraphicModelEditor) editor).initialSplitterPosition((int) (getHeight() * 0.9)); + swapToGraphic(); + } + tree.newTree(true); + tree.update(parsedModel); + currentMode = GRAPHIC_MODE; + theModel.doEnables(); + lastError = ""; + theModel.notifyEventListeners(new GUIModelEvent(GUIModelEvent.NEW_MODEL)); + theModel.notifyEventListeners(new GUIModelEvent(GUIModelEvent.NEW_LOAD_NOT_RELOAD_MODEL)); + } + + // Conversions... (not used) + + public void convertViewToPRISM() + { + theModel.doEnables(); + } + + public void convertViewToPEPA()//dummy dummy dummy + { + theModel.doEnables(); + } + + public void convertViewToGraphic()//dummy dummy dummy + { + theModel.doEnables(); + } + + // Load model... + + public void loadModel(File f) + { + loadModel(f, true); + } + + public void loadModel(File f, boolean inBackground) + { // guess model type based on extension String name = f.getName(); - if(name.endsWith("pm") | name.endsWith("nm") | name.endsWith("sm")) loadPRISMModel(f, inBackground); - else if(name.endsWith("pepa")) loadPEPAModel(f, inBackground); - else if(GUIMultiModel.GM_ENABLED && name.endsWith("gm")) loadGraphicModel(f, inBackground); - else loadPRISMModel(f, inBackground); - } - - public void loadPRISMModel(File f) - { loadPRISMModel(f, true); } - - public void loadPRISMModel(File f, boolean inBackground) - { - lastError = ""; - Thread t = new LoadPRISMModelThread(this, editor, f, false); - t.start(); - if (!inBackground) try - { t.join(); } catch (InterruptedException e) - {} - theModel.doEnables(); - } - - public synchronized void prismModelLoaded(GUITextModelEditor edit, File f, boolean replaceEditor) - { - theModel.notifyEventListeners(new GUIModelEvent(GUIModelEvent.NEW_MODEL)); - theModel.notifyEventListeners(new GUIModelEvent(GUIModelEvent.NEW_LOAD_NOT_RELOAD_MODEL)); - activeFile = f; - modified = false; - modifiedSinceBuild = false; - modifiedSinceParse = false; - parsedModel = null; - setBuiltModel(null,null); - if(replaceEditor) - { - editor = edit; - splitter.setRightComponent(editor); - } - tree.newTree(false); - tree.update(parsedModel); - tree.makeNotUpToDate(); - if(currentMode == GRAPHIC_MODE) - { - swapFromGraphic(); - } - - currentMode = PRISM_MODE; - - checkSwitchAutoParse(); - lastError = ""; - new ParseModelThread(this, editor.getParseText(), false, isAutoParse()).start(); - tree.startParsing(); - parsing = true; - theModel.doEnables(); - theModel.tabToFront(); - } - - public void loadPEPAModel(File f) - { loadPEPAModel(f, true); } - - public void loadPEPAModel(File f, boolean inBackground) - { - lastError = ""; - Thread t = new LoadPEPAModelThread(this, editor, f, false); - t.start(); - if (!inBackground) try - { t.join(); } catch (InterruptedException e) - {} - theModel.doEnables(); - } - - public synchronized void pepaModelLoaded(GUIPepaModelEditor edit, File f, boolean replaceEditor) - { - theModel.notifyEventListeners(new GUIModelEvent(GUIModelEvent.NEW_MODEL)); - theModel.notifyEventListeners(new GUIModelEvent(GUIModelEvent.NEW_LOAD_NOT_RELOAD_MODEL)); - activeFile = f; - modified = false; - modifiedSinceBuild = false; - modifiedSinceParse = false; - parsedModel = null; - setBuiltModel(null,null); - if(replaceEditor) - { - editor = edit; - splitter.setRightComponent(editor); - } - tree.newTree(false); - tree.update(parsedModel); - tree.makeNotUpToDate(); - if(currentMode == GRAPHIC_MODE) - { - swapFromGraphic(); - } - currentMode = PEPA_MODE; - - checkSwitchAutoParse(); - lastError = ""; - new ParseModelThread(this, editor.getParseText(), true, isAutoParse()).start(); - tree.startParsing(); - theModel.doEnables(); - theModel.tabToFront(); - } - - public void loadGraphicModel(File f) - { loadGraphicModel(f, true); } - - public void loadGraphicModel(File f, boolean inBackground) - { - lastError = ""; - Thread t = new LoadGraphicModelThread(this, f); - t.start(); - if (!inBackground) try - { t.join(); } catch (InterruptedException e) - {} - theModel.doEnables(); - } - - public synchronized void graphicModelLoaded(GUIGraphicModelEditor edit, File f) - { - theModel.notifyEventListeners(new GUIModelEvent(GUIModelEvent.NEW_MODEL)); - theModel.notifyEventListeners(new GUIModelEvent(GUIModelEvent.NEW_LOAD_NOT_RELOAD_MODEL)); - activeFile = f; - modified = false; - modifiedSinceBuild = false; - modifiedSinceParse = false; - parsedModel = null; - setBuiltModel(null,null); - - editor = edit; - splitter.setRightComponent(editor); - - tree.update(parsedModel); - tree.makeNotUpToDate(); - - int pos = splitter.getDividerLocation(); - - splitter.setRightComponent(editor); - ((GUIGraphicModelEditor)editor).initialSplitterPosition((int)(getHeight()*0.9)); - if(currentMode != GRAPHIC_MODE) - swapToGraphic(); - - splitter.setDividerLocation(pos); - - currentMode = GRAPHIC_MODE; - - checkSwitchAutoParse(); - lastError = ""; - new ParseModelThread(this, editor.getParseText(), false, isAutoParse()).start(); - tree.startParsing(); - theModel.doEnables(); - theModel.tabToFront(); - } - - private void checkSwitchAutoParse() - { - if(isSwitchOnLarge() && isAutoParse()) - { - if(currentMode == PRISM_MODE || currentMode == PEPA_MODE) - { - if(editor.getParseText().length() > 25000) //500 lines at 50char per line - { - setAutoParse(false); - } - } - } - } - - // Reload model... - - public void reloadActiveFile() - { - if(activeFile != null) - { - if(currentMode == PRISM_MODE) - { - new LoadPRISMModelThread(this, editor, activeFile, true).start(); - } - else if(currentMode == PEPA_MODE) - { - new LoadPEPAModelThread(this, editor, activeFile, true).start(); - } - else if(currentMode == GRAPHIC_MODE) - { - new LoadGraphicModelThread(this, activeFile).start(); - } - } - theModel.doEnables(); - } - - public synchronized void prismModelReLoaded(File f) - { - theModel.notifyEventListeners(new GUIModelEvent(GUIModelEvent.NEW_MODEL)); - activeFile = f; - modified =false; - parsedModel = null; - modifiedSinceParse = false; - setBuiltModel(null,null); - modifiedSinceBuild = false; - currentMode = PRISM_MODE; - checkSwitchAutoParse(); - if(!parsing) - { - parsing = true; - tree.makeNotUpToDate(); - - lastError = ""; - new ParseModelThread(this, editor.getParseText(), false, isAutoParse()).start(); - tree.startParsing(); - } - else - { - parseAfterParse = true; - } - theModel.doEnables(); - theModel.tabToFront(); - } - - public synchronized void pepaModelReLoaded(File f) - { - theModel.notifyEventListeners(new GUIModelEvent(GUIModelEvent.NEW_MODEL)); - activeFile = f; - modified =false; - parsedModel = null; - modifiedSinceParse = false; - setBuiltModel(null,null); - modifiedSinceBuild = false; - currentMode = PEPA_MODE; - checkSwitchAutoParse(); - if(!parsing) - { - parsing = true; - tree.makeNotUpToDate(); - - lastError = ""; - new ParseModelThread(this, editor.getParseText(), true, isAutoParse()).start(); - tree.startParsing(); - } - else - { - parseAfterParse = true; - } - theModel.doEnables(); - theModel.tabToFront(); - } - - public synchronized void graphicModelReLoaded(File f) - { - theModel.notifyEventListeners(new GUIModelEvent(GUIModelEvent.NEW_MODEL)); - activeFile = f; - modified = false; - parsedModel = null; - modifiedSinceParse =false; - setBuiltModel(null,null); - modifiedSinceBuild = false; - currentMode = GRAPHIC_MODE; - checkSwitchAutoParse(); - if(!parsing) - { - parsing = true; - tree.makeNotUpToDate(); - - lastError = ""; - new ParseModelThread(this, editor.getParseText(), true, isAutoParse()).start(); - tree.startParsing(); - } - else - { - parseAfterParse = true; - } - - - theModel.doEnables(); - theModel.tabToFront(); - } - - // Save model... - - public int saveToActiveFile() - { return saveToFile(activeFile); } - - public int saveToFile(File f) - { - if (currentMode == PRISM_MODE || currentMode == PEPA_MODE) - { - try - { - theModel.setTaskBarText("Saving model..."); - if (currentMode == PRISM_MODE) ((GUITextModelEditor)editor).write(new FileWriter(f)); - else ((GUIPepaModelEditor)editor).write(new FileWriter(f)); - } - catch(IOException e) - { - theModel.setTaskBarText("Saving model... error."); - theModel.error("Could not save to file \"" + f + "\""); - return theModel.CANCEL; - } - catch(ClassCastException e) - { - theModel.setTaskBarText("Saving model... error."); - theModel.error("Could not save to file \"" + f + "\""); - return theModel.CANCEL; - } - theModel.setTaskBarText("Saving model... done."); - if (currentMode == PRISM_MODE) prismFileWasSaved(f); else pepaFileWasSaved(f); - return theModel.CONTINUE; - } - else - { - new SaveGraphicModelThread(f, this, editor).start(); - return theModel.CONTINUE; - } - } - - public void prismFileWasSaved(File f) - { - //possibly to handle switching - activeFile = f; - modified = false; - tree.update(parsedModel); - theModel.doEnables(); - } - - public void pepaFileWasSaved(File f) - { - //possibly to handle switching - activeFile = f; - modified = false; - tree.update(parsedModel); - theModel.doEnables(); - } - - public void graphicFileWasSaved(File f) - { - //possibly to handle switching - activeFile = f; - modified = false; - tree.update(parsedModel); - theModel.doEnables(); - } - - // Parse model... - - public void requestParse(boolean force) - { - // only do a parse if we need to (or have been asked to) - if(modifiedSinceParse || parsedModel == null || force) - { - if(!parsing) - { - lastError = ""; - tree.makeNotUpToDate(); - new ParseModelThread(this, editor.getParseText(), currentMode == PEPA_MODE, false).start(); - tree.startParsing(); - parsing = true; - } - else - { - parseAfterParse = true; - } - theModel.doEnables(); - } - // otherwise use last successful parse - else - { - modelParsedSuccessful(parsedModel); - } - } - - public synchronized void modelParsedSuccessful(ModulesFile m) - { - tree.stopParsing(); - parsing = false; - parsedModel = m; - modifiedSinceParse = false; - lastError = "Parse Successful"; - - editor.modelParseSuccessful(); - - if(parseAfterParse) - { - parseAfterParse = false; - tree.makeNotUpToDate(); - //start a new parse thread - if(isAutoParse()) - { - if(waiter != null) - { - waiter.interrupt(); - } - waiter = new WaitParseThread(DEFAULT_WAIT,this); - waiter.start(); - //Funky thread waiting stuff - } - } - else if (buildAfterReceiveParseNotification) - { - buildAfterParse(); - } - else if (exportAfterReceiveParseNotification) - { - exportAfterParse(); - } - else if (computeSSAfterReceiveParseNotification) - { - computeSteadyStateAfterParse(); - } - else if (computeTransientAfterReceiveParseNotification) - { - computeTransientAfterParse(); - } - else - { - tree.update(parsedModel); - } - tree.repaint(); - theModel.doEnables(); - theModel.notifyEventListeners(new GUIModelEvent(GUIModelEvent.MODEL_PARSED, parsedModel)); - } - - public synchronized void modelParseFailed(PrismLangException parserError, boolean background) - { - lastError = parserError.getMessage(); - - editor.modelParseFailed(parserError, background); - - tree.stopParsing(); - parsing = false; - tree.lastParseFailed(); - if(parseAfterParse) - { - parseAfterParse = false; - tree.makeNotUpToDate(); - //start a new parse thread - if(isAutoParse()) - { - if(waiter != null) - { - waiter.interrupt(); - } - waiter = new WaitParseThread(DEFAULT_WAIT,this); - waiter.start(); - //Funky thread waiting stuff - } - } - else - { - buildAfterReceiveParseNotification = false; - exportAfterReceiveParseNotification = false; - computeSSAfterReceiveParseNotification = false; - computeTransientAfterReceiveParseNotification = false; - } - tree.repaint(); - theModel.doEnables(); - theModel.notifyEventListeners(new GUIModelEvent(GUIModelEvent.MODEL_PARSE_FAILED)); - } - - // Build model... - - public void forceBuild() - { - // set flag - buildAfterReceiveParseNotification = true; - // do a parse if necessary - requestParse(false); - } - - private void buildAfterParse() - { - UndefinedConstants unC; - Values buildValues = null; - - // switch off flag - buildAfterReceiveParseNotification = false; - // get values for undefined consts - unC = new UndefinedConstants(parsedModel, null); - if(unC.getMFNumUndefined() > 0) - { - int result = GUIConstantsPicker.defineConstantsWithDialog(theModel.getGUI(), unC, lastBuildValues, null); - if (result != GUIConstantsPicker.VALUES_DONE) return; - } - buildValues = unC.getMFConstantValues(); - // request build - requestBuild(buildValues, true); - } - - public void requestBuild(Values buildValues, boolean force) - { - // only do a build if we need to (or we are asked to) - if (modifiedSinceBuild || builtModel == null || (buildValues!=null && !buildValues.equals(lastBuildValues)) || force) - { - setBuiltModel(null, null); - new BuildModelThread(this, parsedModel, buildValues, false).start(); - } - // otherwise use last successful build - else - { - modelBuildSuccessful(builtModel, lastBuildValues, false); - } - } - - public synchronized void modelBuildSuccessful(Model m, Values lbv) - { modelBuildSuccessful(m, lbv, true); } - - public synchronized void modelBuildSuccessful(Model m, Values lbv, boolean clearOld) - { - modifiedSinceParse = false; - modifiedSinceBuild = false; - setBuiltModel(m, lbv, clearOld); - - if (exportAfterReceiveBuildNotification) - { - exportAfterBuild(); - } - else if(computeSSAfterReceiveBuildNotification) - { - computeSteadyStateAfterBuild(); - } - else if(computeTransientAfterReceiveBuildNotification) - { - computeTransientAfterBuild(); - } - theModel.doEnables(); - theModel.notifyEventListeners(new GUIModelEvent(GUIModelEvent.MODEL_BUILT, builtModel, lastBuildValues)); - } - - public synchronized void modelBuildFailed(PrismException e) - { - if (e != null && e instanceof PrismLangException) editor.modelParseFailed((PrismLangException)e, false); - - if(exportAfterReceiveBuildNotification) - { - exportAfterReceiveBuildNotification = false; - } - else if(computeSSAfterReceiveBuildNotification) - { - computeSSAfterReceiveBuildNotification = false; - } - else if(computeTransientAfterReceiveBuildNotification) - { - computeTransientAfterReceiveBuildNotification = false; - } - theModel.doEnables(); - theModel.notifyEventListeners(new GUIModelEvent(GUIModelEvent.MODEL_BUILD_FAILED)); - } - - public synchronized void setBuiltModel(Model m, Values lbv) - { setBuiltModel(m, lbv, true); } - - public synchronized void setBuiltModel(Model m, Values lbv, boolean clearOld) - { - // clear old model (unless asked not to) - if (clearOld && builtModel != null) - { - builtModel.clear(); - } - // store info - builtModel = m; - lastBuildValues = lbv; - // update display - if(builtModel != null) - { - this.builtNoStates.setText(""+m.getNumStatesString()); - this.builtNoInitStates.setText(""+m.getNumStartStates()); - this.builtNoTransitions.setText(""+m.getNumTransitionsString()); - } else - { - this.builtNoStates.setText("..."); - this.builtNoInitStates.setText("..."); - this.builtNoTransitions.setText("..."); - } - } - - // Export model... - - public void exportBuild(int entity, int type, File f) - { - // set flags/store info - exportAfterReceiveParseNotification = true; - exportEntity = entity; - exportType = type; - exportFile = f; - // do a parse if necessary - requestParse(false); - } - - private void exportAfterParse() - { - UndefinedConstants unC; - Values buildValues = null; - - // switch off flag - exportAfterReceiveParseNotification = false; - // get values for undefined consts - unC = new UndefinedConstants(parsedModel, null); - if(unC.getMFNumUndefined() > 0) - { - int result = GUIConstantsPicker.defineConstantsWithDialog(theModel.getGUI(), unC, lastBuildValues, null); - if (result != GUIConstantsPicker.VALUES_DONE) return; - } - buildValues = unC.getMFConstantValues(); - // request build - exportAfterReceiveBuildNotification = true; - requestBuild(buildValues, false); - } - - private void exportAfterBuild() - { - exportAfterReceiveBuildNotification = false; - new ExportBuiltModelThread(this, builtModel, exportEntity, exportType, exportFile).start(); - // if export is being done to log, switch view to log - if (exportFile == null) theModel.logToFront(); - } - - // Compute steady-state... - - public void computeSteadyState() - { - // set flags/store info - computeSSAfterReceiveParseNotification = true; - // do a parse if necessary - requestParse(false); - } - - private void computeSteadyStateAfterParse() - { - UndefinedConstants unC; - Values buildValues = null; - - // switch off flag - computeSSAfterReceiveParseNotification = false; - // get values for undefined consts - unC = new UndefinedConstants(parsedModel, null); - if(unC.getMFNumUndefined() > 0) - { - int result = GUIConstantsPicker.defineConstantsWithDialog(theModel.getGUI(), unC, lastBuildValues, null); - if (result != GUIConstantsPicker.VALUES_DONE) return; - } - buildValues = unC.getMFConstantValues(); - // request build - computeSSAfterReceiveBuildNotification = true; - requestBuild(buildValues, false); - } - - private void computeSteadyStateAfterBuild() - { - computeSSAfterReceiveBuildNotification = false; - theModel.logToFront(); - new ComputeSteadyStateThread(this, builtModel).start(); - } - - // Compute transient probabilities... - - public void computeTransient(double time) - { - // set flags/store info - computeTransientAfterReceiveParseNotification = true; - transientTime = time; - // do a parse if necessary - requestParse(false); - } - - private void computeTransientAfterParse() - { - UndefinedConstants unC; - Values buildValues = null; - - // switch off flag - computeTransientAfterReceiveParseNotification = false; - // get values for undefined consts - unC = new UndefinedConstants(parsedModel, null); - if(unC.getMFNumUndefined() > 0) - { - int result = GUIConstantsPicker.defineConstantsWithDialog(theModel.getGUI(), unC, lastBuildValues, null); - if (result != GUIConstantsPicker.VALUES_DONE) return; - } - buildValues = unC.getMFConstantValues(); - // request build - computeTransientAfterReceiveBuildNotification = true; - requestBuild(buildValues, false); - } - - private void computeTransientAfterBuild() - { - computeTransientAfterReceiveBuildNotification = false; - theModel.logToFront(); - new ComputeTransientThread(this, builtModel, transientTime).start(); - } - - public void requestViewModel() - { - if(parsedModel != null) - { - theModel.showModel(parsedModel.toString()); - } - theModel.doEnables(); - } - - public void hasModified(boolean attemptReparse) - { - modified = true; - if(isBusy()) - { - theModel.doEnables(); - return; - } - - tree.makeNotUpToDate(); - theModel.notifyEventListeners(new GUIModelEvent(GUIModelEvent.MODIFIED_SINCE_SAVE)); - if(hasBuild()) modifiedSinceBuild = true; - modifiedSinceParse = true; - - - - if(!parsing) - { - if(isAutoParse() && attemptReparse) - { - if(waiter != null) - { - waiter.interrupt(); - } - waiter = new WaitParseThread(DEFAULT_WAIT,this); - waiter.start(); - //Funky thread waiting stuff - } - } - else - { - parseAfterParse = true; - } - theModel.doEnables(); - } - - public void undo() - { - editor.undo(); - } - - public void redo() - { - editor.redo(); - } - - public void cut() - { - editor.cut(); - } - - public void copy() - { - editor.copy(); - } - - public void paste() - { - editor.paste(); - } - - public void delete() - { - editor.delete(); - } - - public void selectAll() - { - editor.selectAll(); - } - - //Access methods - - public synchronized int getModelMode() - { - return currentMode; - } - - public synchronized boolean hasActiveFile() - { - return activeFile != null; - } - - public synchronized boolean modifiedSinceBuild() - { - return modifiedSinceBuild; - } - - public synchronized boolean hasBuild() - { - return builtModel != null; - } - - public synchronized boolean modified() - { - return modified; - } - - public synchronized String getActiveFileName() - { - if(hasActiveFile()) - { - return activeFile.getPath(); - } - else return ""; - } - - public synchronized String getShortActiveFileName() - { - if(hasActiveFile()) - { - return activeFile.getName(); - } - else return ""; - } - - public synchronized boolean isAutoParse() - { - //tosettings: return isAutoParse; - //return theModel.getPrism().getSettings().getBoolean(PrismSettings.MODEL_AUTO_PARSE, true); - return autoParseFast; - } - - public synchronized void setAutoParse(boolean b) - { - // Set flag - //isAutoParse = b; - autoParseFast = b; - try - { - theModel.getPrism().getSettings().set(PrismSettings.MODEL_AUTO_PARSE, b); - } - catch(PrismException e) - { - - } - // If the flag has just been switched ON, do a parse... - if (!b) return; - tree.makeNotUpToDate(); - theModel.notifyEventListeners(new GUIModelEvent(GUIModelEvent.MODIFIED_SINCE_SAVE)); - if(hasBuild()) modifiedSinceBuild = true; - - if(!parsing) - { - if(isAutoParse()) - { - if(waiter != null) - { - waiter.interrupt(); - } - waiter = new WaitParseThread(DEFAULT_WAIT,this); - waiter.start(); - //Funky thread waiting stuff - } - } - else - { - parseAfterParse = true; - } - theModel.doEnables(); - } - - public synchronized boolean isSwitchOnLarge() - { - //tosettings: return isSwitchOnLarge; - return theModel.getPrism().getSettings().getBoolean(PrismSettings.MODEL_AUTO_MANUAL); - } - - public synchronized int getAutoParseWaitTime() - { - //tosettings: return this.autoParseWaitTime; - //return theModel.getPrism().getSettings().getInteger(PrismSettings.MODEL_PARSE_DELAY, DEFAULT_WAIT); - return parseWaitTimeFast; - } - - public synchronized void setAutoParseWaitTime(int t) - { - //tosettings: autoParseWaitTime = t; - parseWaitTimeFast = t; - try - { - theModel.getPrism().getSettings().set(PrismSettings.MODEL_PARSE_DELAY, t); - } - catch(PrismException e) - { - //do nothing - } - } - - public synchronized void setSwitchOnLarge(boolean b) - { - //isSwitchOnLarge = b; - try - { - theModel.getPrism().getSettings().set(PrismSettings.MODEL_AUTO_MANUAL, b); - } - catch(PrismException e) - { - //do nothing - } - } - - public synchronized ModelType getParsedModelType() - { - if(parsedModel != null) - { - return parsedModel.getModelType(); - } - else return ModelType.MDP; - } - - public synchronized String getParseErrorMessage() - { - return lastError; - } - - - //Access to the top level plugin for communication with the rest of the gui - public GUIPlugin getGUIPlugin() - { - return theModel; - } - - public int getParseState() - { - return tree.getParseSynchState(); - } - - public GUIMultiModelTree getTree() - { - return tree; - } - - public PropertyTableModel getPropModel() - { - return graphicalPropModel; - } - - /** - * Getter for property busy. - * @return Value of property busy. - */ - public boolean isBusy() - { - return busy; - } - - /** - * Setter for property busy. - * @param busy New value of property busy. - */ - public void setBusy(boolean busy) - { - this.busy = busy; - } - - public void notifySettings(PrismSettings settings) - { - autoParseFast = settings.getBoolean(PrismSettings.MODEL_AUTO_PARSE); - parseWaitTimeFast = settings.getInteger(PrismSettings.MODEL_PARSE_DELAY); - prismEditorFontFast = settings.getFontColorPair(PrismSettings.MODEL_PRISM_EDITOR_FONT).f; - if(editor instanceof GUITextModelEditor) - ((GUITextModelEditor)editor).setEditorFont(prismEditorFontFast); - prismEditorColourFast = settings.getFontColorPair(PrismSettings.MODEL_PRISM_EDITOR_FONT).c; - - prismEditorBGColourFast = settings.getColor(PrismSettings.MODEL_PRISM_EDITOR_BG_COLOUR); - if(editor instanceof GUITextModelEditor) - ((GUITextModelEditor)editor).setEditorBackground(prismEditorBGColourFast); - int stt; - switch(settings.getInteger(PrismSettings.MODEL_PRISM_EDITOR_NUMERIC_STYLE)) + if (name.endsWith("pm") | name.endsWith("nm") | name.endsWith("sm")) + loadPRISMModel(f, inBackground); + else if (name.endsWith("pepa")) + loadPEPAModel(f, inBackground); + else if (GUIMultiModel.GM_ENABLED && name.endsWith("gm")) + loadGraphicModel(f, inBackground); + else + loadPRISMModel(f, inBackground); + } + + public void loadPRISMModel(File f) + { + loadPRISMModel(f, true); + } + + public void loadPRISMModel(File f, boolean inBackground) + { + lastError = ""; + Thread t = new LoadPRISMModelThread(this, editor, f, false); + t.start(); + if (!inBackground) + try { + t.join(); + } catch (InterruptedException e) { + } + theModel.doEnables(); + } + + public synchronized void prismModelLoaded(GUITextModelEditor edit, File f, boolean replaceEditor) + { + theModel.notifyEventListeners(new GUIModelEvent(GUIModelEvent.NEW_MODEL)); + theModel.notifyEventListeners(new GUIModelEvent(GUIModelEvent.NEW_LOAD_NOT_RELOAD_MODEL)); + activeFile = f; + modified = false; + modifiedSinceBuild = false; + modifiedSinceParse = false; + parsedModel = null; + updateBuiltModelDisplay(); + if (replaceEditor) { + editor = edit; + splitter.setRightComponent(editor); + } + tree.newTree(false); + tree.update(parsedModel); + tree.makeNotUpToDate(); + if (currentMode == GRAPHIC_MODE) { + swapFromGraphic(); + } + + currentMode = PRISM_MODE; + + checkSwitchAutoParse(); + lastError = ""; + new ParseModelThread(this, editor.getParseText(), false, isAutoParse()).start(); + tree.startParsing(); + parsing = true; + theModel.doEnables(); + theModel.tabToFront(); + } + + public void loadPEPAModel(File f) + { + loadPEPAModel(f, true); + } + + public void loadPEPAModel(File f, boolean inBackground) + { + lastError = ""; + Thread t = new LoadPEPAModelThread(this, editor, f, false); + t.start(); + if (!inBackground) + try { + t.join(); + } catch (InterruptedException e) { + } + theModel.doEnables(); + } + + public synchronized void pepaModelLoaded(GUIPepaModelEditor edit, File f, boolean replaceEditor) + { + theModel.notifyEventListeners(new GUIModelEvent(GUIModelEvent.NEW_MODEL)); + theModel.notifyEventListeners(new GUIModelEvent(GUIModelEvent.NEW_LOAD_NOT_RELOAD_MODEL)); + activeFile = f; + modified = false; + modifiedSinceBuild = false; + modifiedSinceParse = false; + parsedModel = null; + updateBuiltModelDisplay(); + if (replaceEditor) { + editor = edit; + splitter.setRightComponent(editor); + } + tree.newTree(false); + tree.update(parsedModel); + tree.makeNotUpToDate(); + if (currentMode == GRAPHIC_MODE) { + swapFromGraphic(); + } + currentMode = PEPA_MODE; + + checkSwitchAutoParse(); + lastError = ""; + new ParseModelThread(this, editor.getParseText(), true, isAutoParse()).start(); + tree.startParsing(); + theModel.doEnables(); + theModel.tabToFront(); + } + + public void loadGraphicModel(File f) + { + loadGraphicModel(f, true); + } + + public void loadGraphicModel(File f, boolean inBackground) + { + lastError = ""; + Thread t = new LoadGraphicModelThread(this, f); + t.start(); + if (!inBackground) + try { + t.join(); + } catch (InterruptedException e) { + } + theModel.doEnables(); + } + + public synchronized void graphicModelLoaded(GUIGraphicModelEditor edit, File f) + { + theModel.notifyEventListeners(new GUIModelEvent(GUIModelEvent.NEW_MODEL)); + theModel.notifyEventListeners(new GUIModelEvent(GUIModelEvent.NEW_LOAD_NOT_RELOAD_MODEL)); + activeFile = f; + modified = false; + modifiedSinceBuild = false; + modifiedSinceParse = false; + parsedModel = null; + updateBuiltModelDisplay(); + + editor = edit; + splitter.setRightComponent(editor); + + tree.update(parsedModel); + tree.makeNotUpToDate(); + + int pos = splitter.getDividerLocation(); + + splitter.setRightComponent(editor); + ((GUIGraphicModelEditor) editor).initialSplitterPosition((int) (getHeight() * 0.9)); + if (currentMode != GRAPHIC_MODE) + swapToGraphic(); + + splitter.setDividerLocation(pos); + + currentMode = GRAPHIC_MODE; + + checkSwitchAutoParse(); + lastError = ""; + new ParseModelThread(this, editor.getParseText(), false, isAutoParse()).start(); + tree.startParsing(); + theModel.doEnables(); + theModel.tabToFront(); + } + + private void checkSwitchAutoParse() + { + if (isSwitchOnLarge() && isAutoParse()) { + if (currentMode == PRISM_MODE || currentMode == PEPA_MODE) { + if (editor.getParseText().length() > 25000) //500 lines at 50char per line + { + setAutoParse(false); + } + } + } + } + + // Reload model... + + public void reloadActiveFile() + { + if (activeFile != null) { + if (currentMode == PRISM_MODE) { + new LoadPRISMModelThread(this, editor, activeFile, true).start(); + } else if (currentMode == PEPA_MODE) { + new LoadPEPAModelThread(this, editor, activeFile, true).start(); + } else if (currentMode == GRAPHIC_MODE) { + new LoadGraphicModelThread(this, activeFile).start(); + } + } + theModel.doEnables(); + } + + public synchronized void prismModelReLoaded(File f) + { + theModel.notifyEventListeners(new GUIModelEvent(GUIModelEvent.NEW_MODEL)); + activeFile = f; + modified = false; + parsedModel = null; + modifiedSinceParse = false; + modifiedSinceBuild = false; + updateBuiltModelDisplay(); + currentMode = PRISM_MODE; + checkSwitchAutoParse(); + if (!parsing) { + parsing = true; + tree.makeNotUpToDate(); + + lastError = ""; + new ParseModelThread(this, editor.getParseText(), false, isAutoParse()).start(); + tree.startParsing(); + } else { + parseAfterParse = true; + } + theModel.doEnables(); + theModel.tabToFront(); + } + + public synchronized void pepaModelReLoaded(File f) + { + theModel.notifyEventListeners(new GUIModelEvent(GUIModelEvent.NEW_MODEL)); + activeFile = f; + modified = false; + parsedModel = null; + modifiedSinceParse = false; + modifiedSinceBuild = false; + updateBuiltModelDisplay(); + currentMode = PEPA_MODE; + checkSwitchAutoParse(); + if (!parsing) { + parsing = true; + tree.makeNotUpToDate(); + + lastError = ""; + new ParseModelThread(this, editor.getParseText(), true, isAutoParse()).start(); + tree.startParsing(); + } else { + parseAfterParse = true; + } + theModel.doEnables(); + theModel.tabToFront(); + } + + public synchronized void graphicModelReLoaded(File f) + { + theModel.notifyEventListeners(new GUIModelEvent(GUIModelEvent.NEW_MODEL)); + activeFile = f; + modified = false; + parsedModel = null; + modifiedSinceParse = false; + modifiedSinceBuild = false; + updateBuiltModelDisplay(); + currentMode = GRAPHIC_MODE; + checkSwitchAutoParse(); + if (!parsing) { + parsing = true; + tree.makeNotUpToDate(); + + lastError = ""; + new ParseModelThread(this, editor.getParseText(), true, isAutoParse()).start(); + tree.startParsing(); + } else { + parseAfterParse = true; + } + + theModel.doEnables(); + theModel.tabToFront(); + } + + // Save model... + + public int saveToActiveFile() + { + return saveToFile(activeFile); + } + + public int saveToFile(File f) + { + if (currentMode == PRISM_MODE || currentMode == PEPA_MODE) { + try { + theModel.setTaskBarText("Saving model..."); + if (currentMode == PRISM_MODE) + ((GUITextModelEditor) editor).write(new FileWriter(f)); + else + ((GUIPepaModelEditor) editor).write(new FileWriter(f)); + } catch (IOException e) { + theModel.setTaskBarText("Saving model... error."); + theModel.error("Could not save to file \"" + f + "\""); + return GUIMultiModel.CANCEL; + } catch (ClassCastException e) { + theModel.setTaskBarText("Saving model... error."); + theModel.error("Could not save to file \"" + f + "\""); + return GUIMultiModel.CANCEL; + } + theModel.setTaskBarText("Saving model... done."); + if (currentMode == PRISM_MODE) + prismFileWasSaved(f); + else + pepaFileWasSaved(f); + return GUIMultiModel.CONTINUE; + } else { + new SaveGraphicModelThread(f, this, editor).start(); + return GUIMultiModel.CONTINUE; + } + } + + public void prismFileWasSaved(File f) + { + //possibly to handle switching + activeFile = f; + modified = false; + tree.update(parsedModel); + theModel.doEnables(); + } + + public void pepaFileWasSaved(File f) + { + //possibly to handle switching + activeFile = f; + modified = false; + tree.update(parsedModel); + theModel.doEnables(); + } + + public void graphicFileWasSaved(File f) + { + //possibly to handle switching + activeFile = f; + modified = false; + tree.update(parsedModel); + theModel.doEnables(); + } + + // Parse model... + + public void requestParse(boolean force) + { + // only do a parse if we need to (or have been asked to) + if (modifiedSinceParse || parsedModel == null || force) { + if (!parsing) { + lastError = ""; + tree.makeNotUpToDate(); + new ParseModelThread(this, editor.getParseText(), currentMode == PEPA_MODE, false).start(); + tree.startParsing(); + parsing = true; + } else { + parseAfterParse = true; + } + theModel.doEnables(); + } + // otherwise use last successful parse + else { + modelParsedSuccessful(parsedModel); + } + } + + public synchronized void modelParsedSuccessful(ModulesFile m) + { + tree.stopParsing(); + parsing = false; + parsedModel = m; + modifiedSinceParse = false; + lastError = "Parse Successful"; + + editor.modelParseSuccessful(); + + if (parseAfterParse) { + parseAfterParse = false; + tree.makeNotUpToDate(); + //start a new parse thread + if (isAutoParse()) { + if (waiter != null) { + waiter.interrupt(); + } + waiter = new WaitParseThread(DEFAULT_WAIT, this); + waiter.start(); + //Funky thread waiting stuff + } + } else if (buildAfterReceiveParseNotification) { + buildAfterParse(); + } else if (exportAfterReceiveParseNotification) { + exportAfterParse(); + } else if (computeSSAfterReceiveParseNotification) { + computeSteadyStateAfterParse(); + } else if (computeTransientAfterReceiveParseNotification) { + computeTransientAfterParse(); + } else { + tree.update(parsedModel); + } + tree.repaint(); + theModel.doEnables(); + theModel.notifyEventListeners(new GUIModelEvent(GUIModelEvent.MODEL_PARSED, parsedModel)); + } + + public synchronized void modelParseFailed(PrismLangException parserError, boolean background) + { + lastError = parserError.getMessage(); + + editor.modelParseFailed(parserError, background); + + tree.stopParsing(); + parsing = false; + tree.lastParseFailed(); + if (parseAfterParse) { + parseAfterParse = false; + tree.makeNotUpToDate(); + //start a new parse thread + if (isAutoParse()) { + if (waiter != null) { + waiter.interrupt(); + } + waiter = new WaitParseThread(DEFAULT_WAIT, this); + waiter.start(); + //Funky thread waiting stuff + } + } else { + buildAfterReceiveParseNotification = false; + exportAfterReceiveParseNotification = false; + computeSSAfterReceiveParseNotification = false; + computeTransientAfterReceiveParseNotification = false; + } + tree.repaint(); + theModel.doEnables(); + theModel.notifyEventListeners(new GUIModelEvent(GUIModelEvent.MODEL_PARSE_FAILED)); + } + + // Build model... + + public void forceBuild() + { + // set flag + buildAfterReceiveParseNotification = true; + // do a parse if necessary + requestParse(false); + } + + private void buildAfterParse() + { + UndefinedConstants unC; + + // switch off flag + buildAfterReceiveParseNotification = false; + // get values for undefined consts + unC = new UndefinedConstants(parsedModel, null); + if (unC.getMFNumUndefined() > 0) { + int result = GUIConstantsPicker.defineConstantsWithDialog(theModel.getGUI(), unC, lastMFConstants, null); + if (result != GUIConstantsPicker.VALUES_DONE) + return; + lastMFConstants = unC.getMFConstantValues(); + } + try { + prism.setPRISMModelConstants(unC.getMFConstantValues()); + } catch (PrismException e) { + theModel.error(e.getMessage()); + return; + } + new BuildModelThread(this).start(); + } + + public synchronized void notifyModelBuildSuccessful() + { + // Deal with a model build success + // Put this in an invokeLater(...) so can be called from another thread + SwingUtilities.invokeLater(new Runnable() { - case 0: stt = Font.PLAIN; break; - case 1: stt = Font.ITALIC; break; - case 2: stt = Font.BOLD; break; - default: stt = Font.BOLD | Font.ITALIC; break; + public void run() + { + updateBuiltModelDisplay(); + theModel.doEnables(); + theModel.notifyEventListeners(new GUIModelEvent(GUIModelEvent.MODEL_BUILT, lastMFConstants)); + } + }); + } + + private void updateBuiltModelDisplay() + { + Model m = prism.getBuiltModel(); + // TODO: explicit case + if (m != null) { + builtNoStates.setText("" + m.getNumStatesString()); + builtNoInitStates.setText("" + m.getNumStartStates()); + builtNoTransitions.setText("" + m.getNumTransitionsString()); + } else { + builtNoStates.setText("?"); + builtNoInitStates.setText("?"); + builtNoTransitions.setText("?"); } - prismEditorNumericFast = new Style(settings.getColor(PrismSettings.MODEL_PRISM_EDITOR_NUMERIC_COLOUR), stt); - - switch(settings.getInteger(PrismSettings.MODEL_PRISM_EDITOR_IDENTIFIER_STYLE)) + } + + public synchronized void notifyModelBuildFailed(PrismException e) + { + // Deal with a model build failure + // Put this in an invokeLater(...) so can be called from another thread + lastBuildError = e; + SwingUtilities.invokeLater(new Runnable() { - case 0: stt = Font.PLAIN; break; - case 1: stt = Font.ITALIC; break; - case 2: stt = Font.BOLD; break; - default: stt = Font.BOLD | Font.ITALIC; break; + public void run() + { + if (lastBuildError != null && lastBuildError instanceof PrismLangException) { + editor.modelParseFailed((PrismLangException) lastBuildError, false); + theModel.tabToFront(); + } + updateBuiltModelDisplay(); + theModel.doEnables(); + theModel.notifyEventListeners(new GUIModelEvent(GUIModelEvent.MODEL_BUILD_FAILED)); + } + }); + } + + // Export model... + + public void export(int entity, int type, File f) + { + // set flags/store info + exportAfterReceiveParseNotification = true; + exportEntity = entity; + exportType = type; + exportFile = f; + // do a parse if necessary + requestParse(false); + } + + private void exportAfterParse() + { + UndefinedConstants unC; + + // switch off flag + exportAfterReceiveParseNotification = false; + // get values for undefined consts + unC = new UndefinedConstants(parsedModel, null); + if (unC.getMFNumUndefined() > 0) { + int result = GUIConstantsPicker.defineConstantsWithDialog(theModel.getGUI(), unC, lastMFConstants, null); + if (result != GUIConstantsPicker.VALUES_DONE) + return; + lastMFConstants = unC.getMFConstantValues(); + } + try { + prism.setPRISMModelConstants(unC.getMFConstantValues()); + } catch (PrismException e) { + theModel.error(e.getMessage()); + return; + } + // if export is being done to log, switch view to log + if (exportFile == null) + theModel.logToFront(); + new ExportBuiltModelThread(this, exportEntity, exportType, exportFile).start(); + } + + // Compute steady-state... + + public void computeSteadyState() + { + // set flags/store info + computeSSAfterReceiveParseNotification = true; + // do a parse if necessary + requestParse(false); + } + + private void computeSteadyStateAfterParse() + { + UndefinedConstants unC; + + // switch off flag + computeSSAfterReceiveParseNotification = false; + // get values for undefined consts + unC = new UndefinedConstants(parsedModel, null); + if (unC.getMFNumUndefined() > 0) { + int result = GUIConstantsPicker.defineConstantsWithDialog(theModel.getGUI(), unC, lastMFConstants, null); + if (result != GUIConstantsPicker.VALUES_DONE) + return; + lastMFConstants = unC.getMFConstantValues(); + } + try { + prism.setPRISMModelConstants(unC.getMFConstantValues()); + } catch (PrismException e) { + theModel.error(e.getMessage()); + return; + } + theModel.logToFront(); + new ComputeSteadyStateThread(this).start(); + } + + // Compute transient probabilities... + + public void computeTransient(double time) + { + // set flags/store info + computeTransientAfterReceiveParseNotification = true; + transientTime = time; + // do a parse if necessary + requestParse(false); + } + + private void computeTransientAfterParse() + { + UndefinedConstants unC; + + // switch off flag + computeTransientAfterReceiveParseNotification = false; + // get values for undefined consts + unC = new UndefinedConstants(parsedModel, null); + if (unC.getMFNumUndefined() > 0) { + int result = GUIConstantsPicker.defineConstantsWithDialog(theModel.getGUI(), unC, lastMFConstants, null); + if (result != GUIConstantsPicker.VALUES_DONE) + return; + lastMFConstants = unC.getMFConstantValues(); + } + try { + prism.setPRISMModelConstants(unC.getMFConstantValues()); + } catch (PrismException e) { + theModel.error(e.getMessage()); + return; + } + theModel.logToFront(); + new ComputeTransientThread(this, transientTime).start(); + } + + public void requestViewModel() + { + if (parsedModel != null) { + theModel.showModel(parsedModel.toString()); + } + theModel.doEnables(); + } + + public void hasModified(boolean attemptReparse) + { + modified = true; + if (isBusy()) { + theModel.doEnables(); + return; + } + + tree.makeNotUpToDate(); + theModel.notifyEventListeners(new GUIModelEvent(GUIModelEvent.MODIFIED_SINCE_SAVE)); + if (hasBuild()) + modifiedSinceBuild = true; + modifiedSinceParse = true; + + if (!parsing) { + if (isAutoParse() && attemptReparse) { + if (waiter != null) { + waiter.interrupt(); + } + waiter = new WaitParseThread(DEFAULT_WAIT, this); + waiter.start(); + //Funky thread waiting stuff + } + } else { + parseAfterParse = true; + } + theModel.doEnables(); + } + + public void undo() + { + editor.undo(); + } + + public void redo() + { + editor.redo(); + } + + public void cut() + { + editor.cut(); + } + + public void copy() + { + editor.copy(); + } + + public void paste() + { + editor.paste(); + } + + public void delete() + { + editor.delete(); + } + + public void selectAll() + { + editor.selectAll(); + } + + //Access methods + + public synchronized int getModelMode() + { + return currentMode; + } + + public synchronized boolean hasActiveFile() + { + return activeFile != null; + } + + public synchronized boolean hasBuild() + { + return prism.getBuiltModel() != null; + } + + public synchronized boolean modified() + { + return modified; + } + + public synchronized String getActiveFileName() + { + if (hasActiveFile()) { + return activeFile.getPath(); + } else + return ""; + } + + public synchronized String getShortActiveFileName() + { + if (hasActiveFile()) { + return activeFile.getName(); + } else + return ""; + } + + public synchronized boolean isAutoParse() + { + //tosettings: return isAutoParse; + //return theModel.getPrism().getSettings().getBoolean(PrismSettings.MODEL_AUTO_PARSE, true); + return autoParseFast; + } + + public synchronized void setAutoParse(boolean b) + { + // Set flag + //isAutoParse = b; + autoParseFast = b; + try { + theModel.getPrism().getSettings().set(PrismSettings.MODEL_AUTO_PARSE, b); + } catch (PrismException e) { + + } + // If the flag has just been switched ON, do a parse... + if (!b) + return; + tree.makeNotUpToDate(); + theModel.notifyEventListeners(new GUIModelEvent(GUIModelEvent.MODIFIED_SINCE_SAVE)); + if (hasBuild()) + modifiedSinceBuild = true; + + if (!parsing) { + if (isAutoParse()) { + if (waiter != null) { + waiter.interrupt(); + } + waiter = new WaitParseThread(DEFAULT_WAIT, this); + waiter.start(); + //Funky thread waiting stuff + } + } else { + parseAfterParse = true; + } + theModel.doEnables(); + } + + public synchronized boolean isSwitchOnLarge() + { + //tosettings: return isSwitchOnLarge; + return theModel.getPrism().getSettings().getBoolean(PrismSettings.MODEL_AUTO_MANUAL); + } + + public synchronized int getAutoParseWaitTime() + { + //tosettings: return this.autoParseWaitTime; + //return theModel.getPrism().getSettings().getInteger(PrismSettings.MODEL_PARSE_DELAY, DEFAULT_WAIT); + return parseWaitTimeFast; + } + + public synchronized void setAutoParseWaitTime(int t) + { + //tosettings: autoParseWaitTime = t; + parseWaitTimeFast = t; + try { + theModel.getPrism().getSettings().set(PrismSettings.MODEL_PARSE_DELAY, t); + } catch (PrismException e) { + //do nothing + } + } + + public synchronized void setSwitchOnLarge(boolean b) + { + //isSwitchOnLarge = b; + try { + theModel.getPrism().getSettings().set(PrismSettings.MODEL_AUTO_MANUAL, b); + } catch (PrismException e) { + //do nothing + } + } + + public synchronized ModelType getParsedModelType() + { + if (parsedModel != null) { + return parsedModel.getModelType(); + } else + return ModelType.MDP; + } + + public synchronized String getParseErrorMessage() + { + return lastError; + } + + //Access to the top level plugin for communication with the rest of the gui + public GUIPlugin getGUIPlugin() + { + return theModel; + } + + public int getParseState() + { + return tree.getParseSynchState(); + } + + public GUIMultiModelTree getTree() + { + return tree; + } + + public PropertyTableModel getPropModel() + { + return graphicalPropModel; + } + + /** + * Getter for property busy. + * @return Value of property busy. + */ + public boolean isBusy() + { + return busy; + } + + /** + * Setter for property busy. + * @param busy New value of property busy. + */ + public void setBusy(boolean busy) + { + this.busy = busy; + } + + public void notifySettings(PrismSettings settings) + { + autoParseFast = settings.getBoolean(PrismSettings.MODEL_AUTO_PARSE); + parseWaitTimeFast = settings.getInteger(PrismSettings.MODEL_PARSE_DELAY); + prismEditorFontFast = settings.getFontColorPair(PrismSettings.MODEL_PRISM_EDITOR_FONT).f; + if (editor instanceof GUITextModelEditor) + ((GUITextModelEditor) editor).setEditorFont(prismEditorFontFast); + prismEditorColourFast = settings.getFontColorPair(PrismSettings.MODEL_PRISM_EDITOR_FONT).c; + + prismEditorBGColourFast = settings.getColor(PrismSettings.MODEL_PRISM_EDITOR_BG_COLOUR); + if (editor instanceof GUITextModelEditor) + ((GUITextModelEditor) editor).setEditorBackground(prismEditorBGColourFast); + int stt; + switch (settings.getInteger(PrismSettings.MODEL_PRISM_EDITOR_NUMERIC_STYLE)) { + case 0: + stt = Font.PLAIN; + break; + case 1: + stt = Font.ITALIC; + break; + case 2: + stt = Font.BOLD; + break; + default: + stt = Font.BOLD | Font.ITALIC; + break; + } + prismEditorNumericFast = new Style(settings.getColor(PrismSettings.MODEL_PRISM_EDITOR_NUMERIC_COLOUR), stt); + + switch (settings.getInteger(PrismSettings.MODEL_PRISM_EDITOR_IDENTIFIER_STYLE)) { + case 0: + stt = Font.PLAIN; + break; + case 1: + stt = Font.ITALIC; + break; + case 2: + stt = Font.BOLD; + break; + default: + stt = Font.BOLD | Font.ITALIC; + break; } - prismEditorVariableFast = new Style(settings.getColor(PrismSettings.MODEL_PRISM_EDITOR_IDENTIFIER_COLOUR), stt); - switch(settings.getInteger(PrismSettings.MODEL_PRISM_EDITOR_KEYWORD_STYLE)) + prismEditorVariableFast = new Style(settings.getColor(PrismSettings.MODEL_PRISM_EDITOR_IDENTIFIER_COLOUR), stt); + switch (settings.getInteger(PrismSettings.MODEL_PRISM_EDITOR_KEYWORD_STYLE)) { + case 0: + stt = Font.PLAIN; + break; + case 1: + stt = Font.ITALIC; + break; + case 2: + stt = Font.BOLD; + break; + default: + stt = Font.BOLD | Font.ITALIC; + break; + } + prismEditorKeywordFast = new Style(settings.getColor(PrismSettings.MODEL_PRISM_EDITOR_KEYWORD_COLOUR), stt); + switch (settings.getInteger(PrismSettings.MODEL_PRISM_EDITOR_COMMENT_STYLE)) { + case 0: + stt = Font.PLAIN; + break; + case 1: + stt = Font.ITALIC; + break; + case 2: + stt = Font.BOLD; + break; + default: + stt = Font.BOLD | Font.ITALIC; + break; + } + prismEditorCommentFast = new Style(settings.getColor(PrismSettings.MODEL_PRISM_EDITOR_COMMENT_COLOUR), stt); + + pepaEditorFontFast = settings.getFontColorPair(PrismSettings.MODEL_PEPA_EDITOR_FONT).f; + if (editor instanceof GUIPepaModelEditor) + ((GUIPepaModelEditor) editor).setEditorFont(pepaEditorFontFast); + pepaEditorColourFast = settings.getColor(PrismSettings.MODEL_PEPA_EDITOR_COMMENT_COLOUR); + pepaEditorBGColourFast = settings.getColor(PrismSettings.MODEL_PEPA_EDITOR_BG_COLOUR); + if (editor instanceof GUIPepaModelEditor) + ((GUIPepaModelEditor) editor).setEditorBackground(pepaEditorBGColourFast); + pepaEditorCommentFast = new Style(settings.getColor(PrismSettings.MODEL_PEPA_EDITOR_COMMENT_COLOUR), + settings.getInteger(PrismSettings.MODEL_PEPA_EDITOR_COMMENT_STYLE)); + } + + /** + * Getter for property autoParseFast. + * @return Value of property autoParseFast. + */ + public boolean isAutoParseFast() + { + return autoParseFast; + } + + /** + * Getter for property parseWaitTimeFast. + * @return Value of property parseWaitTimeFast. + */ + public int getParseWaitTimeFast() + { + return parseWaitTimeFast; + } + + /** + * Getter for property prismEditorFontFast. + * @return Value of property prismEditorFontFast. + */ + public java.awt.Font getPrismEditorFontFast() + { + return prismEditorFontFast; + } + + /** + * Getter for property prismEditorColourFast. + * @return Value of property prismEditorColourFast. + */ + public java.awt.Color getPrismEditorColourFast() + { + return prismEditorColourFast; + } + + /** + * Getter for property prismEditorBGColourFast. + * @return Value of property prismEditorBGColourFast. + */ + public java.awt.Color getPrismEditorBGColourFast() + { + return prismEditorBGColourFast; + } + + /** + * Getter for property pepaEditorFontFast. + * @return Value of property pepaEditorFontFast. + */ + public java.awt.Font getPepaEditorFontFast() + { + return pepaEditorFontFast; + } + + /** + * Getter for property pepaEditorColourFast. + * @return Value of property pepaEditorColourFast. + */ + public java.awt.Color getPepaEditorColourFast() + { + return pepaEditorColourFast; + } + + /** + * Getter for property pepaEditorBGColourFast. + * @return Value of property pepaEditorBGColourFast. + */ + public java.awt.Color getPepaEditorBGColourFast() + { + return pepaEditorBGColourFast; + } + + /** + * Getter for property prismEditorNumericFast. + * @return Value of property prismEditorNumericFast. + */ + public userinterface.model.Style getPrismEditorNumericFast() + { + return prismEditorNumericFast; + } + + /** + * Getter for property prismEditorVariableFast. + * @return Value of property prismEditorVariableFast. + */ + public userinterface.model.Style getPrismEditorVariableFast() + { + return prismEditorVariableFast; + } + + /** + * Getter for property prismEditorKeywordFast. + * @return Value of property prismEditorKeywordFast. + */ + public userinterface.model.Style getPrismEditorKeywordFast() + { + return prismEditorKeywordFast; + } + + /** + * Getter for property prismEditorCommentFast. + * @return Value of property prismEditorCommentFast. + */ + public userinterface.model.Style getPrismEditorCommentFast() + { + return prismEditorCommentFast; + } + + /** + * Getter for property pepaEditorCommentFast. + * @return Value of property pepaEditorCommentFast. + */ + public userinterface.model.Style getPepaEditorCommentFast() + { + return pepaEditorCommentFast; + } + + class WaitParseThread extends Thread + { + int time; + GUIMultiModelHandler handler; + ParseModelThread parseThread; + + public WaitParseThread(int time, GUIMultiModelHandler handler) { - case 0: stt = Font.PLAIN; break; - case 1: stt = Font.ITALIC; break; - case 2: stt = Font.BOLD; break; - default: stt = Font.BOLD | Font.ITALIC; break; + this.time = time; + this.handler = handler; } - prismEditorKeywordFast = new Style(settings.getColor(PrismSettings.MODEL_PRISM_EDITOR_KEYWORD_COLOUR), stt); - switch(settings.getInteger(PrismSettings.MODEL_PRISM_EDITOR_COMMENT_STYLE)) + + public void run() { - case 0: stt = Font.PLAIN; break; - case 1: stt = Font.ITALIC; break; - case 2: stt = Font.BOLD; break; - default: stt = Font.BOLD | Font.ITALIC; break; + try { + sleep(time); + parseThread = new ParseModelThread(handler, editor.getParseText(), currentMode == PEPA_MODE, isAutoParse()); + parsing = true; + tree.startParsing(); + parseThread.start(); + } catch (InterruptedException e) { + } } - prismEditorCommentFast = new Style(settings.getColor(PrismSettings.MODEL_PRISM_EDITOR_COMMENT_COLOUR), stt); - - pepaEditorFontFast = settings.getFontColorPair(PrismSettings.MODEL_PEPA_EDITOR_FONT).f; - if(editor instanceof GUIPepaModelEditor) - ((GUIPepaModelEditor)editor).setEditorFont(pepaEditorFontFast); - pepaEditorColourFast = settings.getColor(PrismSettings.MODEL_PEPA_EDITOR_COMMENT_COLOUR); - pepaEditorBGColourFast = settings.getColor(PrismSettings.MODEL_PEPA_EDITOR_BG_COLOUR); - if(editor instanceof GUIPepaModelEditor) - ((GUIPepaModelEditor)editor).setEditorBackground(pepaEditorBGColourFast); - pepaEditorCommentFast = new Style(settings.getColor(PrismSettings.MODEL_PEPA_EDITOR_COMMENT_COLOUR), settings.getInteger(PrismSettings.MODEL_PEPA_EDITOR_COMMENT_STYLE)); - } - - /** - * Getter for property autoParseFast. - * @return Value of property autoParseFast. - */ - public boolean isAutoParseFast() - { - return autoParseFast; - } - - /** - * Getter for property parseWaitTimeFast. - * @return Value of property parseWaitTimeFast. - */ - public int getParseWaitTimeFast() - { - return parseWaitTimeFast; - } - - /** - * Getter for property prismEditorFontFast. - * @return Value of property prismEditorFontFast. - */ - public java.awt.Font getPrismEditorFontFast() - { - return prismEditorFontFast; - } - - /** - * Getter for property prismEditorColourFast. - * @return Value of property prismEditorColourFast. - */ - public java.awt.Color getPrismEditorColourFast() - { - return prismEditorColourFast; - } - - /** - * Getter for property prismEditorBGColourFast. - * @return Value of property prismEditorBGColourFast. - */ - public java.awt.Color getPrismEditorBGColourFast() - { - return prismEditorBGColourFast; - } - - /** - * Getter for property pepaEditorFontFast. - * @return Value of property pepaEditorFontFast. - */ - public java.awt.Font getPepaEditorFontFast() - { - return pepaEditorFontFast; - } - - /** - * Getter for property pepaEditorColourFast. - * @return Value of property pepaEditorColourFast. - */ - public java.awt.Color getPepaEditorColourFast() - { - return pepaEditorColourFast; - } - - /** - * Getter for property pepaEditorBGColourFast. - * @return Value of property pepaEditorBGColourFast. - */ - public java.awt.Color getPepaEditorBGColourFast() - { - return pepaEditorBGColourFast; - } - - /** - * Getter for property prismEditorNumericFast. - * @return Value of property prismEditorNumericFast. - */ - public userinterface.model.Style getPrismEditorNumericFast() - { - return prismEditorNumericFast; - } - - /** - * Getter for property prismEditorVariableFast. - * @return Value of property prismEditorVariableFast. - */ - public userinterface.model.Style getPrismEditorVariableFast() - { - return prismEditorVariableFast; - } - - /** - * Getter for property prismEditorKeywordFast. - * @return Value of property prismEditorKeywordFast. - */ - public userinterface.model.Style getPrismEditorKeywordFast() - { - return prismEditorKeywordFast; - } - - /** - * Getter for property prismEditorCommentFast. - * @return Value of property prismEditorCommentFast. - */ - public userinterface.model.Style getPrismEditorCommentFast() - { - return prismEditorCommentFast; - } - - - /** - * Getter for property pepaEditorCommentFast. - * @return Value of property pepaEditorCommentFast. - */ - public userinterface.model.Style getPepaEditorCommentFast() - { - return pepaEditorCommentFast; - } - - class WaitParseThread extends Thread - { - int time; - GUIMultiModelHandler handler; - ParseModelThread parseThread; - - public WaitParseThread(int time, GUIMultiModelHandler handler) - { - this.time = time; - this.handler = handler; - } - - public void run() - { - try - { - sleep(time); - parseThread = new ParseModelThread(handler, editor.getParseText(), currentMode == PEPA_MODE, isAutoParse()); - parsing = true; - tree.startParsing(); - parseThread.start(); - } - catch(InterruptedException e) - { - } - } - } - - public GUIUndoManager getUndoManager() - { - return editor.getUndoManager(); - } - - public boolean canDoClipBoardAction(Action action) { - // TODO Auto-generated method stub + } + + public GUIUndoManager getUndoManager() + { + return editor.getUndoManager(); + } + + public boolean canDoClipBoardAction(Action action) + { return editor.canDoClipBoardAction(action); } - public void jumpToError() { + public void jumpToError() + { if (editor != null && editor instanceof GUITextModelEditor) - ((GUITextModelEditor)editor).jumpToError(); + ((GUITextModelEditor) editor).jumpToError(); } - - + } diff --git a/prism/src/userinterface/model/computation/BuildModelThread.java b/prism/src/userinterface/model/computation/BuildModelThread.java index 68530b3b..51a17527 100644 --- a/prism/src/userinterface/model/computation/BuildModelThread.java +++ b/prism/src/userinterface/model/computation/BuildModelThread.java @@ -31,222 +31,63 @@ import javax.swing.*; import userinterface.*; import userinterface.model.*; -import parser.*; -import parser.ast.*; import prism.*; import userinterface.util.*; +/** + * Thread that performs model construction, whether needed or not. + */ public class BuildModelThread extends GUIComputationThread { + @SuppressWarnings("unused") private GUIMultiModelHandler handler; - private String buildThis; - private boolean isPepa; - private ModulesFile mod; - private Model model; - private Values buildValues; - private boolean forceShow; - private String errMsg; - private PrismLangException parseError; - private PrismException buildError; - private StateList deadlocks; - + /** Creates a new instance of BuildModelThread */ -// public BuildModelThread(GUIMultiModelHandler handler, String buildThis, boolean isPepa, Values buildValues, boolean forceShow) -// { -// this.handler = handler; -// this.buildThis = buildThis; -// this.isPepa = isPepa; -// this.buildValues = buildValues; -// plug = handler.getGUIPlugin(); -// this.forceShow = forceShow; -// } - - public BuildModelThread(GUIMultiModelHandler handler, ModulesFile buildParse, Values buildValues, boolean forceShow) + public BuildModelThread(GUIMultiModelHandler handler) { super(handler.getGUIPlugin()); this.handler = handler; - this.buildThis = null; - this.mod = buildParse; - this.buildValues = buildValues; - this.forceShow = forceShow; - } public void run() { - //Notify user interface of the start of computation - SwingUtilities.invokeLater(new Runnable() { public void run() { - plug.startProgress(); - plug.notifyEventListeners(new GUIComputationEvent(GUIComputationEvent.COMPUTATION_START, plug)); - }}); - - //If need to do parse first... - if(buildThis!=null) + // Notify user interface of the start of computation + SwingUtilities.invokeLater(new Runnable() { - SwingUtilities.invokeLater(new Runnable() { public void run() { - plug.setTaskBarText("Parsing model..."); - }}); - - // do parsing - try { - // normal prism mode - if(!isPepa) { - mod = prism.parseModelString(buildThis); - } - // pepa mode - else { - mod = prism.importPepaString(buildThis); - } - } - catch (PrismLangException e) { - parseError = e; - SwingUtilities.invokeLater(new Runnable() { public void run() { - plug.stopProgress(); - plug.notifyEventListeners(new GUIComputationEvent(GUIComputationEvent.COMPUTATION_ERROR, plug)); - plug.setTaskBarText("Parsing model... error."); - error(parseError.getMessage()); - handler.modelParseFailed(parseError, false); - handler.modelBuildFailed(null); - }}); - return; - } - catch (PrismException e) { - throw new RuntimeException("Unexpected PrismException: " + e.getMessage()); - } - - //If we are here, the parse was successful, notify the interface - SwingUtilities.invokeLater(new Runnable() { public void run() { - plug.setTaskBarText("Parsing model... done."); - handler.modelParsedSuccessful(mod); - }}); - - //give it a break so user can see the ...done before the building model... - try { sleep(100); } catch(InterruptedException e) {} - } - - // Check whether there are any undefined constants... - // ...and if there are, get values for them - UndefinedConstants unC = new UndefinedConstants(mod, null); - if(unC.getMFNumUndefined() > 0) - { - if(forceShow || (buildValues == null)) + public void run() { - // notify interface - SwingUtilities.invokeLater(new Runnable() { public void run() { - plug.setTaskBarText("Defining constants..."); - }}); - - // show dialog - int result = GUIConstantsPicker.defineConstantsWithDialog(handler.getGUIPlugin().getGUI(), unC, buildValues, null); - - // if build cancelled... - if(result != GUIConstantsPicker.VALUES_DONE) { - SwingUtilities.invokeLater(new Runnable() { public void run() { - plug.stopProgress(); - plug.notifyEventListeners(new GUIComputationEvent(GUIComputationEvent.COMPUTATION_ERROR, plug)); - plug.setTaskBarText("Building model... cancelled."); - handler.modelBuildFailed(new PrismException("")); - }}); - return; - } - - // get build values - buildValues = unC.getMFConstantValues(); + plug.startProgress(); + plug.notifyEventListeners(new GUIComputationEvent(GUIComputationEvent.COMPUTATION_START, plug)); + plug.setTaskBarText("Building model..."); } - - // notify interface - SwingUtilities.invokeLater(new Runnable() { public void run() { - plug.setTaskBarText("Defining constants... done."); - }}); - } - else { - // create an empty values object - buildValues = new Values(); - } - - if (buildValues != null) if (buildValues.getNumValues() > 0) logln("\nModel constants: " + buildValues); - - // set undefined constants - try { - mod.setUndefinedConstants(buildValues); - } - catch (PrismException e) { - buildError = e; - errMsg = e.getMessage(); - SwingUtilities.invokeLater(new Runnable() { public void run() { - plug.stopProgress(); - plug.notifyEventListeners(new GUIComputationEvent(GUIComputationEvent.COMPUTATION_ERROR, plug)); - plug.setTaskBarText("Building model... error."); - error(errMsg); - handler.modelBuildFailed(buildError); - }}); - return; - } - - // notify interface - SwingUtilities.invokeLater(new Runnable() { public void run() { - plug.setTaskBarText("Building model..."); - }}); - - // do build + }); + + // Do build try { - logSeparator(); - model = prism.buildModel(mod); - } - catch (PrismException e) { - buildError = e; - errMsg = e.getMessage(); - SwingUtilities.invokeLater(new Runnable() { public void run() { - plug.stopProgress(); - plug.notifyEventListeners(new GUIComputationEvent(GUIComputationEvent.COMPUTATION_ERROR, plug)); - plug.setTaskBarText("Building model... error."); - error(errMsg); - handler.modelBuildFailed(buildError); - }}); - return; - } - - // Check for Deadlocks - deadlocks = model.getDeadlockStates(); - if (deadlocks != null) if (deadlocks.size() > 0) { - String[] options = {"Continue", "Display deadlocks"}; - int choice = plug.question("Error", "Error: Model contains deadlock states.\nAdd self-loops to these states and continue?\nOr stop and display deadlock states in log?", options); - if (choice == 0) { - logWarning(deadlocks.size() + " deadlock states detected; adding self-loops in these states..."); - model.fixDeadlocks(); - } - else { - model.printTransInfo(plug.getGUI().getLog()); - log("\nError: Model contains " + deadlocks.size() + " deadlock states"); - if (deadlocks.size() > 10) { - log(".\nThe first 10 deadlock states are displayed below.\n"); - deadlocks.print(plug.getGUI().getLog(), 10); - } else { - log(":\n"); - deadlocks.print(plug.getGUI().getLog()); - } - model.clear(); - - SwingUtilities.invokeLater(new Runnable() { public void run() { - plug.stopProgress(); + prism.buildModel(); + } catch (PrismException e) { + error(e.getMessage()); + SwingUtilities.invokeLater(new Runnable() + { + public void run() + { + plug.stopProgress(); plug.notifyEventListeners(new GUIComputationEvent(GUIComputationEvent.COMPUTATION_ERROR, plug)); plug.setTaskBarText("Building model... error."); - handler.modelBuildFailed(new PrismException("")); - plug.logToFront(); - }}); - return; - } + } + }); + return; } - logln(); - model.printTransInfo(plug.getGUI().getLog()); - - //If we are here, the build was successful, notify the interface - SwingUtilities.invokeLater(new Runnable() { public void run() { - plug.stopProgress(); - plug.setTaskBarText("Building model... done."); - plug.notifyEventListeners(new GUIComputationEvent(GUIComputationEvent.COMPUTATION_DONE, plug)); - handler.modelBuildSuccessful(model, buildValues); - }}); + // If we are here, the build was successful, notify the interface + SwingUtilities.invokeLater(new Runnable() + { + public void run() + { + plug.stopProgress(); + plug.setTaskBarText("Building model... done."); + plug.notifyEventListeners(new GUIComputationEvent(GUIComputationEvent.COMPUTATION_DONE, plug)); + } + }); } } diff --git a/prism/src/userinterface/model/computation/ComputeSteadyStateThread.java b/prism/src/userinterface/model/computation/ComputeSteadyStateThread.java index 738457d7..02738689 100644 --- a/prism/src/userinterface/model/computation/ComputeSteadyStateThread.java +++ b/prism/src/userinterface/model/computation/ComputeSteadyStateThread.java @@ -26,28 +26,31 @@ //============================================================================== package userinterface.model.computation; + import javax.swing.*; import userinterface.*; import userinterface.model.*; import prism.*; import userinterface.util.*; +/** + * Thread that performs steady-state probability computation on a model. + */ public class ComputeSteadyStateThread extends GUIComputationThread { + @SuppressWarnings("unused") private GUIMultiModelHandler handler; - private Model computeThis; - + /** Creates a new instance of ComputeSteadyStateThread */ - public ComputeSteadyStateThread(GUIMultiModelHandler handler, Model computeThis) + public ComputeSteadyStateThread(GUIMultiModelHandler handler) { super(handler.getGUIPlugin()); this.handler = handler; - this.computeThis = computeThis; } - + public void run() { - //notify the interface that we are starting computation + // Notify the interface that we are starting computation SwingUtilities.invokeLater(new Runnable() { public void run() @@ -57,15 +60,11 @@ public class ComputeSteadyStateThread extends GUIComputationThread plug.setTaskBarText("Computing steady-state probabilities..."); } }); - - //Do Computation + + // Do Computation try { - if (!(computeThis.getModelType() == ModelType.CTMC || computeThis.getModelType() == ModelType.DTMC)) - throw new PrismException("Can only compute steady-state probabilities for CTMCs"); - prism.doSteadyState(computeThis); - } - catch(PrismException e) - { + prism.doSteadyState(); + } catch (PrismException e) { error(e.getMessage()); SwingUtilities.invokeLater(new Runnable() { @@ -78,8 +77,8 @@ public class ComputeSteadyStateThread extends GUIComputationThread }); return; } - - //If we get here, computation was successful + + // If we get here, computation was successful SwingUtilities.invokeLater(new Runnable() { public void run() diff --git a/prism/src/userinterface/model/computation/ComputeTransientThread.java b/prism/src/userinterface/model/computation/ComputeTransientThread.java index f7f9d6b5..7ee186ad 100644 --- a/prism/src/userinterface/model/computation/ComputeTransientThread.java +++ b/prism/src/userinterface/model/computation/ComputeTransientThread.java @@ -26,30 +26,33 @@ //============================================================================== package userinterface.model.computation; + import javax.swing.*; import userinterface.*; import userinterface.model.*; import prism.*; import userinterface.util.*; +/** + * Thread that performs transient probability computation on a model. + */ public class ComputeTransientThread extends GUIComputationThread { + @SuppressWarnings("unused") private GUIMultiModelHandler handler; - private Model computeThis; private double transientTime; - + /** Creates a new instance of ComputeTransientThread */ - public ComputeTransientThread(GUIMultiModelHandler handler, Model computeThis, double transientTime) + public ComputeTransientThread(GUIMultiModelHandler handler, double transientTime) { super(handler.getGUIPlugin()); this.handler = handler; - this.computeThis = computeThis; this.transientTime = transientTime; } - + public void run() { - //notify the interface that we are starting computation + // Notify the interface that we are starting computation SwingUtilities.invokeLater(new Runnable() { public void run() @@ -60,14 +63,10 @@ public class ComputeTransientThread extends GUIComputationThread } }); - //Do Computation + // Do Computation try { - if (!(computeThis.getModelType() == ModelType.CTMC || computeThis.getModelType() == ModelType.DTMC)) - throw new PrismException("Can only compute transient probabilities for DTMCs/CTMCs"); - plug.getPrism().doTransient(computeThis, transientTime); - } - catch(PrismException e) - { + prism.doTransient(transientTime); + } catch (PrismException e) { error(e.getMessage()); SwingUtilities.invokeLater(new Runnable() { @@ -80,7 +79,7 @@ public class ComputeTransientThread extends GUIComputationThread }); return; } - + //If we get here, computation was successful SwingUtilities.invokeLater(new Runnable() { diff --git a/prism/src/userinterface/model/computation/ExportBuiltModelThread.java b/prism/src/userinterface/model/computation/ExportBuiltModelThread.java index b1fbff7e..8dcfea48 100644 --- a/prism/src/userinterface/model/computation/ExportBuiltModelThread.java +++ b/prism/src/userinterface/model/computation/ExportBuiltModelThread.java @@ -35,85 +35,97 @@ import userinterface.*; import userinterface.model.*; import userinterface.util.*; +/** + * Thread that performs export of a built model. + */ public class ExportBuiltModelThread extends GUIComputationThread { + @SuppressWarnings("unused") private GUIMultiModelHandler handler; - private Model m; private int exportEntity; private int exportType; private File exportFile; - private Exception e; - + /** Creates a new instance of ExportBuiltModelThread */ - public ExportBuiltModelThread(GUIMultiModelHandler handler, Model m, int entity, int type, File f) + public ExportBuiltModelThread(GUIMultiModelHandler handler, int entity, int type, File f) { super(handler.getGUIPlugin()); this.handler = handler; - this.m = m; this.exportEntity = entity; this.exportType = type; this.exportFile = f; } - + public void run() { - try - { - //notify the interface of the start of computation - SwingUtilities.invokeAndWait(new Runnable() { public void run() { - plug.startProgress(); - plug.notifyEventListeners(new GUIComputationEvent(GUIComputationEvent.COMPUTATION_START, plug)); - plug.setTaskBarText("Exporting..."); - }}); - - //Do export + try { + // Notify the interface of the start of computation + SwingUtilities.invokeAndWait(new Runnable() + { + public void run() + { + plug.startProgress(); + plug.setTaskBarText("Exporting..."); + plug.notifyEventListeners(new GUIComputationEvent(GUIComputationEvent.COMPUTATION_START, plug)); + } + }); + + // Do export try { switch (exportEntity) { case GUIMultiModelHandler.STATES_EXPORT: - prism.exportStatesToFile(m, exportType, exportFile); + prism.exportStatesToFile(exportType, exportFile); break; case GUIMultiModelHandler.TRANS_EXPORT: - prism.exportTransToFile(m, true, exportType, exportFile); + prism.exportTransToFile(true, exportType, exportFile); break; case GUIMultiModelHandler.STATE_REWARDS_EXPORT: - prism.exportStateRewardsToFile(m, exportType, exportFile); + prism.exportStateRewardsToFile(exportType, exportFile); break; case GUIMultiModelHandler.TRANS_REWARDS_EXPORT: - prism.exportTransRewardsToFile(m, true, exportType, exportFile); + prism.exportTransRewardsToFile(true, exportType, exportFile); break; } - } - catch(FileNotFoundException e) - { - SwingUtilities.invokeAndWait(new Runnable() { public void run() { - plug.stopProgress(); - plug.notifyEventListeners(new GUIComputationEvent(GUIComputationEvent.COMPUTATION_ERROR, plug)); - plug.setTaskBarText("Exporting... error."); - error("Could not export to file \"" + exportFile + "\""); - }}); + } catch (FileNotFoundException e) { + SwingUtilities.invokeAndWait(new Runnable() + { + public void run() + { + plug.stopProgress(); + plug.setTaskBarText("Exporting... error."); + plug.notifyEventListeners(new GUIComputationEvent(GUIComputationEvent.COMPUTATION_ERROR, plug)); + error("Could not export to file \"" + exportFile + "\""); + } + }); return; - } - catch(PrismException e2) - { - this.e = e2; - SwingUtilities.invokeAndWait(new Runnable() { public void run() { - plug.stopProgress(); - plug.notifyEventListeners(new GUIComputationEvent(GUIComputationEvent.COMPUTATION_ERROR, plug)); - plug.setTaskBarText("Exporting... error."); - error(e.getMessage()); - }}); + } catch (PrismException e2) { + error(e2.getMessage()); + SwingUtilities.invokeAndWait(new Runnable() + { + public void run() + { + plug.stopProgress(); + plug.setTaskBarText("Exporting... error."); + plug.notifyEventListeners(new GUIComputationEvent(GUIComputationEvent.COMPUTATION_ERROR, plug)); + } + }); return; } - + //If we get here export was successful, notify interface - SwingUtilities.invokeAndWait(new Runnable() { public void run() { - plug.stopProgress(); - plug.setTaskBarText("Exporting... done."); - plug.notifyEventListeners(new GUIComputationEvent(GUIComputationEvent.COMPUTATION_DONE, plug)); - }}); + SwingUtilities.invokeAndWait(new Runnable() + { + public void run() + { + plug.stopProgress(); + plug.setTaskBarText("Exporting... done."); + plug.notifyEventListeners(new GUIComputationEvent(GUIComputationEvent.COMPUTATION_DONE, plug)); + } + }); } // catch and ignore any thread exceptions - catch (java.lang.InterruptedException e) {} - catch (java.lang.reflect.InvocationTargetException e) {} + catch (java.lang.InterruptedException e) { + } catch (java.lang.reflect.InvocationTargetException e) { + } } } diff --git a/prism/src/userinterface/model/computation/ParseModelThread.java b/prism/src/userinterface/model/computation/ParseModelThread.java index 582f657f..7cbf7058 100644 --- a/prism/src/userinterface/model/computation/ParseModelThread.java +++ b/prism/src/userinterface/model/computation/ParseModelThread.java @@ -47,7 +47,7 @@ public class ParseModelThread extends GUIComputationThread static int counter = 0; int id; long before; - + /** Creates a new instance of ParseModelThread */ public ParseModelThread(GUIMultiModelHandler handler, String parseThis, boolean isPepa, boolean background) { @@ -62,54 +62,69 @@ public class ParseModelThread extends GUIComputationThread public void run() { - //Notify user interface of the start of computation - SwingUtilities.invokeLater(new Runnable() { public void run() { - if(!background)plug.startProgress(); - plug.notifyEventListeners(new GUIComputationEvent(GUIComputationEvent.COMPUTATION_START, plug)); - if(!background)plug.setTaskBarText("Parsing model..."); - }}); + // Notify user interface of the start of computation + SwingUtilities.invokeLater(new Runnable() + { + public void run() + { + if (!background) + plug.startProgress(); + plug.notifyEventListeners(new GUIComputationEvent(GUIComputationEvent.COMPUTATION_START, plug)); + if (!background) + plug.setTaskBarText("Parsing model..."); + } + }); // do parsing try { // normal prism mode - if(!isPepa) { - if(!background) plug.log("\nParsing model...\n"); + if (!isPepa) { + if (!background) + plug.log("\nParsing model...\n"); mod = prism.parseModelString(parseThis); } // pepa mode else { - if(!background) plug.log("\nParsing PEPA model...\n"); + if (!background) + plug.log("\nParsing PEPA model...\n"); mod = prism.importPepaString(parseThis); } - } - catch (PrismLangException err) { + // Load into PRISM once done + prism.loadPRISMModel(mod); + } catch (PrismLangException err) { parseError = err; errMsg = err.getMessage(); - SwingUtilities.invokeLater(new Runnable() - { - public void run() - { - if(!background) plug.stopProgress(); + SwingUtilities.invokeLater(new Runnable() + { + public void run() + { + if (!background) + plug.stopProgress(); plug.notifyEventListeners(new GUIComputationEvent(GUIComputationEvent.COMPUTATION_ERROR, plug)); - if(!background) plug.setTaskBarText("Parsing model... error."); - if(!background) error(errMsg); - handler.modelParseFailed(parseError, background); + if (!background) + plug.setTaskBarText("Parsing model... error."); + if (!background) + error(errMsg); + handler.modelParseFailed(parseError, background); } }); return; + } catch (PrismException e) { + throw new RuntimeException("Unexpected PrismException: " + e.getMessage()); } - catch (PrismException e) { - throw new RuntimeException("Unexpected PrismException: " + e.getMessage()); - } - - //If we get here, the parse has been successful, notify the interface and tell the handler. - SwingUtilities.invokeLater(new Runnable() { public void run() { - if(!background) plug.stopProgress(); - if(!background) plug.setTaskBarText("Parsing model... done."); - plug.notifyEventListeners(new GUIComputationEvent(GUIComputationEvent.COMPUTATION_DONE, plug)); - handler.modelParsedSuccessful(mod); - }}); + + // If we get here, the parse has been successful, notify the interface and tell the handler. + SwingUtilities.invokeLater(new Runnable() + { + public void run() + { + if (!background) + plug.stopProgress(); + if (!background) + plug.setTaskBarText("Parsing model... done."); + plug.notifyEventListeners(new GUIComputationEvent(GUIComputationEvent.COMPUTATION_DONE, plug)); + handler.modelParsedSuccessful(mod); + } + }); } } - - diff --git a/prism/src/userinterface/properties/GUIExperiment.java b/prism/src/userinterface/properties/GUIExperiment.java index e2d1ac8e..5e44334f 100644 --- a/prism/src/userinterface/properties/GUIExperiment.java +++ b/prism/src/userinterface/properties/GUIExperiment.java @@ -32,14 +32,11 @@ import parser.*; import parser.ast.*; import parser.type.*; import prism.*; -import pta.DigitalClocks; +import userinterface.*; import javax.swing.*; - -import userinterface.*; import java.util.*; import userinterface.util.*; -import userinterface.simulator.networking.*; public class GUIExperiment { @@ -48,7 +45,6 @@ public class GUIExperiment private prism.ResultsCollection results; private boolean finished = false; - private ModulesFile mod; private UndefinedConstants cons; private PropertiesFile prop; //contains 1 property only @@ -63,14 +59,12 @@ public class GUIExperiment private Result res; /** Creates a new instance of GUIExperiment */ - public GUIExperiment(GUIExperimentTable table, GUIMultiProperties guiProp, PropertiesFile prop, UndefinedConstants cons, ModulesFile mod, - boolean useSimulation) + public GUIExperiment(GUIExperimentTable table, GUIMultiProperties guiProp, PropertiesFile prop, UndefinedConstants cons, boolean useSimulation) { this.table = table; this.guiProp = guiProp; this.prop = prop; this.cons = cons; - this.mod = mod; this.useSimulation = useSimulation; results = new prism.ResultsCollection(cons, prop.getProperty(0).getResultName()); @@ -139,7 +133,7 @@ public class GUIExperiment public void startExperiment() { - theThread = new ExperimentThread(guiProp, this, cons, mod, prop); + theThread = new ExperimentThread(guiProp, cons, prop); running = true; theThread.start(); } @@ -197,27 +191,18 @@ public class GUIExperiment class ExperimentThread extends GUIComputationThread { private UndefinedConstants undefinedConstants; - private ModulesFile modulesFile; private PropertiesFile propertiesFile; - private GUIExperiment exp; - public ExperimentThread(GUIMultiProperties guiProp, GUIExperiment exp, UndefinedConstants undefinedConstants, ModulesFile modulesFile, - PropertiesFile propertiesFile) + public ExperimentThread(GUIMultiProperties guiProp, UndefinedConstants undefinedConstants, PropertiesFile propertiesFile) { super(guiProp); - this.exp = exp; this.undefinedConstants = undefinedConstants; - this.modulesFile = modulesFile; this.propertiesFile = propertiesFile; } public void run() { int i, k; - boolean clear = true; - Model model = null; - - ModulesFile modulesFileToCheck; int propertyIndex = propertiesFile.getNumProperties() - 1; Expression propertyToCheck = propertiesFile.getProperty(propertyIndex); SimulationInformation info = null; @@ -240,14 +225,11 @@ public class GUIExperiment }); for (i = 0; i < undefinedConstants.getNumModelIterations(); i++) { - definedMFConstants = undefinedConstants.getMFConstantValues(); - if (definedMFConstants != null) - if (definedMFConstants.getNumValues() > 0) - logln("\nModel constants: " + definedMFConstants); // set values for ModulesFile constants try { - modulesFile.setUndefinedConstants(definedMFConstants); + definedMFConstants = undefinedConstants.getMFConstantValues(); + prism.setPRISMModelConstants(definedMFConstants); } catch (PrismException e) { // in case of error, report it (in log only), store as result, and go on to the next model errorLog(e.getMessage()); @@ -260,46 +242,12 @@ public class GUIExperiment continue; } - // only do explicit model construction if necessary - if (!useSimulation && modulesFile.getModelType() != ModelType.PTA) { - - // build model - try { - logSeparator(); - model = prism.buildModel(modulesFile); - clear = false; - } catch (PrismException e) { - // in case of error, report it (in log only), store as result, and go on to the next model - errorLog(e.getMessage()); - try { - setMultipleErrors(definedMFConstants, null, e); - } catch (PrismException e2) { - error("Problem storing results"); - } - undefinedConstants.iterateModel(); - continue; - } - - // remove any deadlocks (don't prompt - probably should) - StateList states = model.getDeadlockStates(); - if (states != null) { - if (states.size() > 0) { - guiProp.logWarning(states.size() + " deadlock states detected; adding self-loops in these states..."); - model.fixDeadlocks(); - } - } - - // print some model info - guiProp.log("\n"); - model.printTransInfo(guiProp.getGUI().getLog()); - } - // collect information for simulation if required if (useSimulation && !reuseInfo) { try { info = null; - info = GUISimulationPicker.defineSimulationWithDialog(guiProp.getGUI(), propertyToCheck, modulesFile, "(" + definedMFConstants - + ")"); + info = GUISimulationPicker.defineSimulationWithDialog(guiProp.getGUI(), propertyToCheck, prism.getPRISMModel(), "(" + + definedMFConstants + ")"); } catch (PrismException e) { // in case of error, report it (in log only), store as result, and go on to the next model errorLog(e.getMessage()); @@ -308,8 +256,6 @@ public class GUIExperiment } catch (PrismException e2) { error("Problem storing results"); } - if (!clear) - model.clear(); undefinedConstants.iterateModel(); continue; } @@ -328,31 +274,11 @@ public class GUIExperiment } } - // for distributed simulation, pass control to the GUISimulatorDistributionDialog - if (useSimulation && info.isDistributed()) { - try { - GUISimulatorDistributionDialog dist = new GUISimulatorDistributionDialog(guiProp.getGUI(), prism.getSimulator(), true); - dist.show(exp, this, modulesFile, propertiesFile, undefinedConstants, propertyToCheck, info); - //new GUISimulatorDistributionDialog(guiProp.getGUI(), prism.getSimulator(), true).show(modulesFile, undefinedConstants, propertyToCheck, info); - } catch (PrismException e) { - // in case of error, report it (in log only), store as result, and go on to the next model - errorLog(e.getMessage()); - try { - setMultipleErrors(definedMFConstants, null, e); - } catch (PrismException e2) { - error("Problem storing results"); - } - if (!clear) - model.clear(); - undefinedConstants.iterateModel(); - continue; - } - } - // for simulation where "simultaneous property checking" is enabled... else if (useSimulation && prism.getSettings().getBoolean(PrismSettings.SIMULATOR_SIMULTANEOUS) && undefinedConstants.getNumPropertyIterations() > 1) { try { + // TODO logSeparator(); logln("\nSimulating: " + propertyToCheck); if (definedMFConstants != null) @@ -365,11 +291,11 @@ public class GUIExperiment if (info.getInitialState() == null) { initialState = null; } else { - initialState = new parser.State(info.getInitialState(), modulesFile); + initialState = new parser.State(info.getInitialState(), prism.getPRISMModel()); } // do simulation - prism.modelCheckSimulatorExperiment(modulesFile, propertiesFile, undefinedConstants, results, propertyToCheck, initialState, info - .getMaxPathLength(), info.createSimulationMethod()); + prism.modelCheckSimulatorExperiment(propertiesFile, undefinedConstants, results, propertyToCheck, initialState, + info.getMaxPathLength(), info.createSimulationMethod()); // update progress meter // (all properties simulated simultaneously so can't get more accurate feedback at the moment anyway) table.progressChanged(); @@ -392,57 +318,16 @@ public class GUIExperiment throw new InterruptedException(); try { - // set values for PropertiesFile constants + // Set values for PropertiesFile constants if (propertiesFile != null) { definedPFConstants = undefinedConstants.getPFConstantValues(); propertiesFile.setSomeUndefinedConstants(definedPFConstants); } - - // log output - logSeparator(); - logln("\n" + (useSimulation ? "Simulating" : "Model checking") + ": " + propertyToCheck); - if (definedMFConstants != null) - if (definedMFConstants.getNumValues() > 0) - logln("Model constants: " + definedMFConstants); - if (definedPFConstants != null) - if (definedPFConstants.getNumValues() > 0) - logln("Property constants: " + definedPFConstants); - - // for PTAs via digital clocks, do model translation and build - if (modulesFile.getModelType() == ModelType.PTA - && prism.getSettings().getString(PrismSettings.PRISM_PTA_METHOD).equals("Digital clocks")) { - DigitalClocks dc = new DigitalClocks(prism); - dc.translate(modulesFile, propertiesFile, propertyToCheck); - modulesFileToCheck = dc.getNewModulesFile(); - modulesFileToCheck.setUndefinedConstants(modulesFile.getConstantValues()); - // build model - logSeparator(); - model = prism.buildModel(modulesFileToCheck); - clear = false; - // by construction, deadlocks can only occur from timelocks - StateList states = model.getDeadlockStates(); - if (states != null && states.size() > 0) { - throw new PrismException("Timelock in PTA, e.g. in state (" + states.getFirstAsValues() + ")"); - } - // print some model info - guiProp.log("\n"); - model.printTransInfo(guiProp.getGUI().getLog()); - } else { - modulesFileToCheck = modulesFile; - } - - // exact (non-approximate) model checking + // Normal model checking if (!useSimulation) { - // PTA model checking - if (modulesFileToCheck.getModelType() == ModelType.PTA) { - res = prism.modelCheckPTA(modulesFileToCheck, propertiesFile, propertyToCheck); - } - // Non-PTA model checking - else { - res = prism.modelCheck(model, propertiesFile, propertyToCheck); - } + res = prism.modelCheck(propertiesFile, propertyToCheck, definedPFConstants); } - // approximate (simulation-based) model checking + // Approximate (simulation-based) model checking else { // convert initial Values -> State // (remember: null means use default or pick randomly) @@ -450,10 +335,10 @@ public class GUIExperiment if (info.getInitialState() == null) { initialState = null; } else { - initialState = new parser.State(info.getInitialState(), modulesFileToCheck); + initialState = new parser.State(info.getInitialState(), prism.getPRISMModel()); } // do simulation - res = prism.modelCheckSimulator(modulesFileToCheck, propertiesFile, propertyToCheck, initialState, info.getMaxPathLength(), + res = prism.modelCheckSimulator(propertiesFile, propertyToCheck, definedPFConstants, initialState, info.getMaxPathLength(), info.createSimulationMethod()); } } catch (PrismException e) { @@ -481,8 +366,6 @@ public class GUIExperiment yield(); } } - if (!clear) - model.clear(); // iterate to next model undefinedConstants.iterateModel(); yield(); @@ -521,8 +404,6 @@ public class GUIExperiment catch (InterruptedException e2) { } catch (java.lang.reflect.InvocationTargetException e2) { } - if (!clear) - model.clear(); experimentInterrupted(); } // catch and ignore possible exception from invokeAndWait calls diff --git a/prism/src/userinterface/properties/GUIExperimentTable.java b/prism/src/userinterface/properties/GUIExperimentTable.java index 4e081625..eec25e5f 100644 --- a/prism/src/userinterface/properties/GUIExperimentTable.java +++ b/prism/src/userinterface/properties/GUIExperimentTable.java @@ -70,9 +70,9 @@ public class GUIExperimentTable extends JTable } } - public int newExperiment(PropertiesFile propFile, UndefinedConstants cons, ModulesFile mf, boolean useSimulation)//propFile only contains 1 con + public int newExperiment(PropertiesFile propFile, UndefinedConstants cons, boolean useSimulation)//propFile only contains 1 con { - GUIExperiment ge = new GUIExperiment(this, guiProps, propFile, cons, mf, useSimulation); + GUIExperiment ge = new GUIExperiment(this, guiProps, propFile, cons, useSimulation); return expModel.addExperiment(ge); } diff --git a/prism/src/userinterface/properties/GUIMultiProperties.java b/prism/src/userinterface/properties/GUIMultiProperties.java index 80d2a5c4..c2271d07 100644 --- a/prism/src/userinterface/properties/GUIMultiProperties.java +++ b/prism/src/userinterface/properties/GUIMultiProperties.java @@ -83,8 +83,6 @@ import parser.type.Type; import parser.type.TypeDouble; import parser.type.TypeInt; import parser.type.TypeInterval; -import prism.Model; -import prism.ModelType; import prism.PrismException; import prism.PrismSettings; import prism.PrismSettingsListener; @@ -102,7 +100,6 @@ import userinterface.properties.computation.LoadPropertiesThread; import userinterface.properties.computation.ModelCheckThread; import userinterface.properties.computation.SimulateModelCheckThread; import userinterface.simulator.GUISimulator; -import userinterface.simulator.networking.GUISimulatorDistributionDialog; import userinterface.util.GUIComputationEvent; import userinterface.util.GUIEvent; import userinterface.util.GUIExitEvent; @@ -111,6 +108,7 @@ import userinterface.util.GUIPrismFileFilter; /** * Properties tab of the PRISM GUI. */ +@SuppressWarnings("serial") public class GUIMultiProperties extends GUIPlugin implements MouseListener, ListSelectionListener, PrismSettingsListener, ContainerListener { //CONSTANTS @@ -124,15 +122,13 @@ public class GUIMultiProperties extends GUIPlugin implements MouseListener, List // Current model (gets updated only by event listening to GUIModel) private ModulesFile parsedModel; - private Model builtModel; // Constants for model (updated by events or locally) private Values mfConstants; // State private boolean modified; - private boolean modifiedSinceBuild; private boolean computing; - private boolean verifyAfterReceiveParseNotification, verifyAfterReceiveBuildNotification, experimentAfterReceiveParseNotification, + private boolean verifyAfterReceiveParseNotification, experimentAfterReceiveParseNotification, simulateAfterReceiveParseNotification; private PropertiesFile parsedProperties; private ArrayList propertiesToBeVerified; @@ -171,8 +167,8 @@ public class GUIMultiProperties extends GUIPlugin implements MouseListener, List simulator.setGUIProb(this); // link required initComponents(); a_newList(); - setBuiltModel(null); setParsedModel(null); + doEnables(); //options = new GUIPropertiesOptions(this); } @@ -240,18 +236,6 @@ public class GUIMultiProperties extends GUIPlugin implements MouseListener, List propList.repaint(); } - protected void verifyAfterBuild() - { - verifyAfterReceiveBuildNotification = false; - - // Start model check process - if (builtModel != null && parsedProperties != null && propertiesToBeVerified != null) { - Thread t = new ModelCheckThread(this, builtModel, parsedProperties, propertiesToBeVerified, mfConstants, pfConstants); - t.setPriority(Thread.NORM_PRIORITY); - t.start(); - } - } - protected void verifyAfterParse() { ArrayList validGUIProperties; @@ -278,30 +262,19 @@ public class GUIMultiProperties extends GUIPlugin implements MouseListener, List if (result != GUIConstantsPicker.VALUES_DONE) return; } - // Store model constants (even though will be stored again after build) - // Don't set in model: this will be done during build process + // Store model/property constants mfConstants = uCon.getMFConstantValues(); - // Store property constants and set in file pfConstants = uCon.getPFConstantValues(); + getPrism().setPRISMModelConstants(mfConstants); parsedProperties.setSomeUndefinedConstants(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(); - } - } + for (GUIProperty gp : propertiesToBeVerified) + gp.setConstants(mfConstants, pfConstants); + // Start model checking + Thread t = new ModelCheckThread(this, parsedProperties, propertiesToBeVerified, pfConstants); + t.setPriority(Thread.NORM_PRIORITY); + t.start(); } catch (PrismException e) { error(e.getMessage()); return; @@ -363,12 +336,19 @@ public class GUIMultiProperties extends GUIPlugin implements MouseListener, List return; } - // Store model/property constants and set in files + // Store model/property constants mfConstants = uCon.getMFConstantValues(); pfConstants = uCon.getPFConstantValues(); - parsedModel.setUndefinedConstants(mfConstants); + getPrism().setPRISMModelConstants(mfConstants); parsedProperties.setSomeUndefinedConstants(pfConstants); + for (GUIProperty gp : simulatableGUIProperties) + gp.setConstants(mfConstants, pfConstants); + // Store properties to be verified + propertiesToBeVerified = validGUIProperties; + for (GUIProperty gp : propertiesToBeVerified) + gp.setConstants(mfConstants, pfConstants); + // Get simulation info with dialog SimulationInformation info = GUISimulationPicker.defineSimulationWithDialog(this.getGUI(), simulatableExprs, parsedModel, null); @@ -377,14 +357,9 @@ public class GUIMultiProperties extends GUIPlugin implements MouseListener, List return; if (parsedModel != null && parsedProperties != null) { - if (info.isDistributed()) { - new GUISimulatorDistributionDialog(getGUI(), getPrism().getSimulator(), true).show(this, parsedModel, parsedProperties, simulatableGUIProperties, - info); - } else { - Thread t = new SimulateModelCheckThread(this, parsedModel, parsedProperties, simulatableGUIProperties, mfConstants, pfConstants, info); - t.setPriority(Thread.NORM_PRIORITY); - t.start(); - } + Thread t = new SimulateModelCheckThread(this, parsedProperties, simulatableGUIProperties, pfConstants, info); + t.setPriority(Thread.NORM_PRIORITY); + t.start(); } } catch (PrismException e) { error(e.getMessage()); @@ -470,12 +445,11 @@ public class GUIMultiProperties extends GUIPlugin implements MouseListener, List } // Use these values to create a new experiment - int i = experiments.newExperiment(parsedProperties, uCon, parsedModel, useSimulation); + int i = experiments.newExperiment(parsedProperties, uCon, useSimulation); boolean notCancelled = true; // start the experiment, via the graph dialog if appropriate if (showGraphDialog) { GUIGraphPicker ggp = new GUIGraphPicker(getGUI(), this, experiments.getExperiment(i), graphHandler, false); - if (ggp.isGraphCancelled()) { if (questionYesNo("Do you want to cancel the experiment completely?", 0) == 0) notCancelled = false; @@ -616,12 +590,6 @@ public class GUIMultiProperties extends GUIPlugin implements MouseListener, List doEnables(); } - protected void setBuiltModel(Model m) - { - builtModel = m; - doEnables(); - } - protected void doEnables() { // properties panel @@ -730,7 +698,6 @@ public class GUIMultiProperties extends GUIPlugin implements MouseListener, List consTable.newList(); labTable.newList(); setModified(false); - modifiedSinceBuild = true; setActiveFile(null); doEnables(); notifyEventListeners(new GUIPropertiesEvent(GUIPropertiesEvent.PROPERTIES_LIST_CHANGED)); @@ -1138,16 +1105,13 @@ public class GUIMultiProperties extends GUIPlugin implements MouseListener, List GUIModelEvent me = (GUIModelEvent) e; if (me.getID() == me.NEW_MODEL) { //New Model - setBuiltModel(null); setParsedModel(null); + doEnables(); //newList(); } else if (me.getID() == GUIModelEvent.MODEL_BUILT) { - setBuiltModel(me.getModel()); if (me.getBuildValues() != null) mfConstants = me.getBuildValues(); - modifiedSinceBuild = false; - if (verifyAfterReceiveBuildNotification) - verifyAfterBuild(); + doEnables(); } else if (me.getID() == GUIModelEvent.MODEL_PARSED) { setParsedModel(me.getModulesFile()); if (verifyAfterReceiveParseNotification) @@ -1160,11 +1124,6 @@ public class GUIMultiProperties extends GUIPlugin implements MouseListener, List verifyAfterReceiveParseNotification = false; experimentAfterReceiveParseNotification = false; simulateAfterReceiveParseNotification = false; - } else if (me.getID() == GUIModelEvent.MODEL_BUILD_FAILED) { - verifyAfterReceiveBuildNotification = false; - } else if (me.getID() == GUIModelEvent.MODIFIED_SINCE_SAVE) { - //setBuiltModel(null); - modifiedSinceBuild = true; } else if (me.getID() == GUIModelEvent.NEW_LOAD_NOT_RELOAD_MODEL) { if (getPrism().getSettings().getBoolean(PrismSettings.PROPERTIES_CLEAR_LIST_ON_LOAD)) { a_newList(); diff --git a/prism/src/userinterface/properties/computation/ModelCheckThread.java b/prism/src/userinterface/properties/computation/ModelCheckThread.java index 5ee102a0..bffe834c 100644 --- a/prism/src/userinterface/properties/computation/ModelCheckThread.java +++ b/prism/src/userinterface/properties/computation/ModelCheckThread.java @@ -33,7 +33,6 @@ import javax.swing.*; import parser.*; import parser.ast.*; import prism.*; -import pta.DigitalClocks; import userinterface.*; import userinterface.util.*; import userinterface.properties.*; @@ -45,53 +44,27 @@ 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 model/modulesFile is non-null - private Model model; - private ModulesFile modulesFile; // Properties file and GUI properties (these are assumed to match) // (Also need properties file for access to constants/labels/etc.) private PropertiesFile propertiesFile; private ArrayList guiProps; // Values give to constants - private Values definedMFConstants; private Values definedPFConstants; /** * Create a new instance of ModelCheckThread (where a Model has been built) */ - public ModelCheckThread(GUIMultiProperties parent, Model model, PropertiesFile propertiesFile, ArrayList guiProps, Values definedMFConstants, - Values definedPFConstants) + public ModelCheckThread(GUIMultiProperties parent, PropertiesFile propertiesFile, ArrayList guiProps, Values definedPFConstants) { super(parent); this.parent = parent; - this.model = model; - this.modulesFile = null; this.propertiesFile = propertiesFile; 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 modulesFile, PropertiesFile propertiesFile, ArrayList guiProps, Values definedMFConstants, - Values definedPFConstants) - { - this(parent, (Model) null, propertiesFile, guiProps, definedMFConstants, definedPFConstants); - this.modulesFile = modulesFile; - } - public void run() { - ModulesFile modulesFileToCheck; - boolean clear = true; - - if (model == null && modulesFile == null) - return; - // Notify user interface of the start of computation SwingUtilities.invokeLater(new Runnable() { @@ -128,52 +101,7 @@ public class ModelCheckThread extends GUIComputationThread // Do model checking try { - // Print info to log - logSeparator(); - logln("\nModel checking: " + propertiesFile.getProperty(i)); - if (definedMFConstants != null) - if (definedMFConstants.getNumValues() > 0) - logln("Model constants: " + definedMFConstants); - if (definedPFConstants != null) - if (definedPFConstants.getNumValues() > 0) - logln("Property constants: " + definedPFConstants); - // for PTAs via digital clocks, do model translation and build - if (model == null && modulesFile.getModelType() == ModelType.PTA - && prism.getSettings().getString(PrismSettings.PRISM_PTA_METHOD).equals("Digital clocks")) { - DigitalClocks dc = new DigitalClocks(prism); - dc.translate(modulesFile, propertiesFile, propertiesFile.getProperty(i)); - modulesFileToCheck = dc.getNewModulesFile(); - modulesFileToCheck.setUndefinedConstants(modulesFile.getConstantValues()); - // build model - logSeparator(); - model = prism.buildModel(modulesFileToCheck); - clear = false; - // by construction, deadlocks can only occur from timelocks - StateList states = model.getDeadlockStates(); - if (states != null && states.size() > 0) { - throw new PrismException("Timelock in PTA, e.g. in state (" + states.getFirstAsValues() + ")"); - } - // print some model info - log("\n"); - model.printTransInfo(parent.getGUI().getLog()); - } else { - modulesFileToCheck = modulesFile; - } - // No model (PTA, non-digital-clocks) case - if (model == null) { - if (modulesFile.getModelType() != ModelType.PTA) - throw new PrismException("No model to verify"); - result = prism.modelCheckPTA(modulesFileToCheck, propertiesFile, propertiesFile.getProperty(i)); - } - // Normal model checking - else { - result = prism.modelCheck(model, propertiesFile, propertiesFile.getProperty(i)); - } - // Clear model, if required - if (!clear) { - model.clear(); - clear = true; - } + result = prism.modelCheck(propertiesFile, propertiesFile.getProperty(i), definedPFConstants); } catch (PrismException e) { result = new Result(e); error(e.getMessage()); @@ -186,7 +114,6 @@ public class ModelCheckThread extends GUIComputationThread //while(!ic.canContinue){} gp.setResult(result); gp.setMethodString("Verification"); - gp.setConstants(definedMFConstants, definedPFConstants); gp.setNumberOfWarnings(prism.getMainLog().getNumberOfWarnings()); parent.repaintList(); diff --git a/prism/src/userinterface/properties/computation/SimulateModelCheckThread.java b/prism/src/userinterface/properties/computation/SimulateModelCheckThread.java index 5e2948c3..c4136ff4 100644 --- a/prism/src/userinterface/properties/computation/SimulateModelCheckThread.java +++ b/prism/src/userinterface/properties/computation/SimulateModelCheckThread.java @@ -40,32 +40,28 @@ import userinterface.util.*; import userinterface.properties.*; /** - * This thread handles the calling of simulation-based - * model checking (sampling) with the given modules file (constants - * defined), properties file (constants defined), list of properties to - * be (approximately) verified and initial state (default/random if null). + * Thread that executes approximate (simulation-based) model checking of a property via PRISM. + * Model should have been loaded into PRISM already. Supplied are: + * properties file (constants defined), list of properties to + * be (approximately) verified and initial state (default/random if null). */ public class SimulateModelCheckThread extends GUIComputationThread { private GUIMultiProperties parent; - private ModulesFile mf; private PropertiesFile pf; private ArrayList guiProps; - private Values definedMFConstants; private Values definedPFConstants; private int maxPathLength; private SimulationInformation info; /** Creates a new instance of SimulateModelCheckThread */ - public SimulateModelCheckThread(GUIMultiProperties parent, ModulesFile m, PropertiesFile prFi, ArrayList guiProps, Values definedMFConstants, + public SimulateModelCheckThread(GUIMultiProperties parent, PropertiesFile prFi, ArrayList guiProps, Values definedPFConstants, SimulationInformation info) { super(parent); this.parent = parent; - this.mf = m; this.pf = prFi; this.guiProps = guiProps; - this.definedMFConstants = definedMFConstants; this.definedPFConstants = definedPFConstants; this.info = info; this.maxPathLength = info.getMaxPathLength(); @@ -74,11 +70,8 @@ public class SimulateModelCheckThread extends GUIComputationThread public void run() { boolean allAtOnce = prism.getSettings().getBoolean(PrismSettings.SIMULATOR_SIMULTANEOUS); - + SimulationMethod method = info.createSimulationMethod(); - - if (mf == null) - return; //Notify user interface of the start of computation SwingUtilities.invokeLater(new Runnable() @@ -113,33 +106,16 @@ public class SimulateModelCheckThread extends GUIComputationThread } try { - // display info - logSeparator(); - log("\nSimulating"); - if (pf.getNumProperties() == 1) { - logln(": " + properties.get(0)); - } else { - logln(" " + pf.getNumProperties() + " properties:"); - for (int i = 0; i < properties.size(); i++) { - logln(" " + properties.get(i)); - } - } - if (definedMFConstants != null) - if (definedMFConstants.getNumValues() > 0) - logln("Model constants: " + definedMFConstants); - if (definedPFConstants != null) - if (definedPFConstants.getNumValues() > 0) - logln("Property constants: " + definedPFConstants); // convert initial Values -> State // (remember: null means use default or pick randomly) parser.State initialState; if (info.getInitialState() == null) { initialState = null; } else { - initialState = new parser.State(info.getInitialState(), mf); + initialState = new parser.State(info.getInitialState(), prism.getPRISMModel()); } // do simulation - results = prism.modelCheckSimulatorSimultaneously(mf, pf, properties, initialState, maxPathLength, method); + results = prism.modelCheckSimulatorSimultaneously(pf, properties, definedPFConstants, initialState, maxPathLength, method); method.reset(); } catch (PrismException e) { // in the case of an error which affects all props, store/report it @@ -163,7 +139,6 @@ public class SimulateModelCheckThread extends GUIComputationThread GUIProperty gp = guiProps.get(i); gp.setResult((results == null) ? new Result(resultError) : results[i]); gp.setMethodString("Simulation"); - gp.setConstants(definedMFConstants, definedPFConstants); gp.setNumberOfWarnings(prism.getMainLog().getNumberOfWarnings()); } } @@ -178,28 +153,18 @@ public class SimulateModelCheckThread extends GUIComputationThread ict.start(); // do model checking try { - logSeparator(); - logln("\nSimulating" + ": " + 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); // convert initial Values -> State // (remember: null means use default or pick randomly) parser.State initialState; if (info.getInitialState() == null) { initialState = null; } else { - initialState = new parser.State(info.getInitialState(), mf); + initialState = new parser.State(info.getInitialState(), prism.getPRISMModel()); } // do simulation - result = prism.modelCheckSimulator(mf, pf, pf.getProperty(i), initialState, maxPathLength, method); + result = prism.modelCheckSimulator(pf, pf.getProperty(i), definedPFConstants, initialState, maxPathLength, method); method.reset(); - } - catch(PrismException e) - { + } catch (PrismException e) { result = new Result(e); error(e.getMessage()); } @@ -213,7 +178,6 @@ public class SimulateModelCheckThread extends GUIComputationThread } gp.setResult(result); gp.setMethodString("Simulation"); - gp.setConstants(definedMFConstants, definedPFConstants); parent.repaintList(); }