diff --git a/prism/src/explicit/DTMCModelChecker.java b/prism/src/explicit/DTMCModelChecker.java index 1038e10c..bc3176ab 100644 --- a/prism/src/explicit/DTMCModelChecker.java +++ b/prism/src/explicit/DTMCModelChecker.java @@ -31,10 +31,15 @@ import java.util.BitSet; import java.util.List; import java.util.Map; +import parser.VarList; +import parser.ast.Declaration; +import parser.ast.DeclarationIntUnbounded; import parser.ast.Expression; import parser.type.TypeDouble; +import prism.Prism; import prism.PrismComponent; import prism.PrismException; +import prism.PrismFileLog; import prism.PrismNotSupportedException; import prism.PrismUtils; import acceptance.AcceptanceReach; @@ -74,6 +79,24 @@ public class DTMCModelChecker extends ProbModelChecker }; product = mcLtl.constructProductMC(this, (DTMC)model, expr, statesOfInterest, allowedAcceptance); + // Output product, if required + if (getExportProductTrans()) { + mainLog.println("\nExporting product transition matrix to file \"" + getExportProductTransFilename() + "\"..."); + product.getProductModel().exportToPrismExplicitTra(getExportProductTransFilename()); + } + if (getExportProductStates()) { + mainLog.println("\nExporting product state space to file \"" + getExportProductStatesFilename() + "\"..."); + PrismFileLog out = new PrismFileLog(getExportProductStatesFilename()); + VarList newVarList = (VarList) modulesFile.createVarList().clone(); + String daVar = "_da"; + while (newVarList.getIndex(daVar) != -1) { + daVar = "_" + daVar; + } + newVarList.addVar(0, new Declaration(daVar, new DeclarationIntUnbounded()), 1, null); + product.getProductModel().exportStates(Prism.EXPORT_PLAIN, modulesFile.createVarList(), out); + out.close(); + } + // Find accepting states + compute reachability probabilities BitSet acc; if (product.getAcceptance() instanceof AcceptanceReach) { diff --git a/prism/src/explicit/LTLModelChecker.java b/prism/src/explicit/LTLModelChecker.java index 7216ad06..ca15a933 100644 --- a/prism/src/explicit/LTLModelChecker.java +++ b/prism/src/explicit/LTLModelChecker.java @@ -299,7 +299,7 @@ public class LTLModelChecker extends PrismComponent int prodNumStates = modelNumStates * daSize; int s_1, s_2, q_1, q_2; BitSet s_labels = new BitSet(numAPs); - List prodStatesList = null; + List prodStatesList = null, daStatesList = null; // Encoding: // each state s' = = s * daSize + q @@ -312,6 +312,10 @@ public class LTLModelChecker extends PrismComponent if (dtmc.getStatesList() != null) { prodStatesList = new ArrayList(); + daStatesList = new ArrayList(da.size()); + for (int i = 0; i < da.size(); i++) { + daStatesList.add(new State(1).setValue(0, i)); + } } // We need results for all states of the original model in statesOfInterest @@ -334,7 +338,7 @@ public class LTLModelChecker extends PrismComponent map[s_0 * daSize + q_0] = prodModel.getNumStates() - 1; if (prodStatesList != null) { // store DTMC state information for the product state - prodStatesList.add(dtmc.getStatesList().get(s_0)); + prodStatesList.add(new State(daStatesList.get(q_0), dtmc.getStatesList().get(s_0))); } } @@ -365,7 +369,7 @@ public class LTLModelChecker extends PrismComponent map[s_2 * daSize + q_2] = prodModel.getNumStates() - 1; if (prodStatesList != null) { // store DTMC state information for the product state - prodStatesList.add(dtmc.getStatesList().get(s_2)); + prodStatesList.add(new State(daStatesList.get(q_2), dtmc.getStatesList().get(s_2))); } } prodModel.setProbability(map[s_1 * daSize + q_1], map[s_2 * daSize + q_2], prob); @@ -444,7 +448,7 @@ public class LTLModelChecker extends PrismComponent int prodNumStates = modelNumStates * daSize; int s_1, s_2, q_1, q_2; BitSet s_labels = new BitSet(numAPs); - List prodStatesList = null; + List prodStatesList = null, daStatesList = null; // Encoding: @@ -458,6 +462,10 @@ public class LTLModelChecker extends PrismComponent if (mdp.getStatesList() != null) { prodStatesList = new ArrayList(); + daStatesList = new ArrayList(da.size()); + for (int i = 0; i < da.size(); i++) { + daStatesList.add(new State(1).setValue(0, i)); + } } // We need results for all states of the original model in statesOfInterest @@ -480,7 +488,7 @@ public class LTLModelChecker extends PrismComponent map[s_0 * daSize + q_0] = prodModel.getNumStates() - 1; if (prodStatesList != null) { // store MDP state information for the product state - prodStatesList.add(mdp.getStatesList().get(s_0)); + prodStatesList.add(new State(daStatesList.get(q_0), mdp.getStatesList().get(s_0))); } } @@ -514,7 +522,7 @@ public class LTLModelChecker extends PrismComponent map[s_2 * daSize + q_2] = prodModel.getNumStates() - 1; if (prodStatesList != null) { // store MDP state information for the product state - prodStatesList.add(mdp.getStatesList().get(s_2)); + prodStatesList.add(new State(daStatesList.get(q_2), mdp.getStatesList().get(s_2))); } } prodDistr.set(map[s_2 * daSize + q_2], prob); diff --git a/prism/src/explicit/MDPModelChecker.java b/prism/src/explicit/MDPModelChecker.java index ebea9184..73198e23 100644 --- a/prism/src/explicit/MDPModelChecker.java +++ b/prism/src/explicit/MDPModelChecker.java @@ -31,7 +31,12 @@ import java.util.Iterator; import java.util.List; import java.util.Map; +import parser.VarList; +import parser.ast.Declaration; +import parser.ast.DeclarationInt; +import parser.ast.DeclarationIntUnbounded; import parser.ast.Expression; +import prism.Prism; import prism.PrismComponent; import prism.PrismDevNullLog; import prism.PrismException; @@ -83,7 +88,26 @@ public class MDPModelChecker extends ProbModelChecker }; product = mcLtl.constructProductMDP(this, (MDP)model, expr, statesOfInterest, allowedAcceptance); - + mainLog.println(product.getProductModel().getStatesList()); + + // Output product, if required + if (getExportProductTrans()) { + mainLog.println("\nExporting product transition matrix to file \"" + getExportProductTransFilename() + "\"..."); + product.getProductModel().exportToPrismExplicitTra(getExportProductTransFilename()); + } + if (getExportProductStates()) { + mainLog.println("\nExporting product state space to file \"" + getExportProductStatesFilename() + "\"..."); + PrismFileLog out = new PrismFileLog(getExportProductStatesFilename()); + VarList newVarList = (VarList) modulesFile.createVarList().clone(); + String daVar = "_da"; + while (newVarList.getIndex(daVar) != -1) { + daVar = "_" + daVar; + } + newVarList.addVar(0, new Declaration(daVar, new DeclarationIntUnbounded()), 1, null); + product.getProductModel().exportStates(Prism.EXPORT_PLAIN, newVarList, out); + out.close(); + } + // Find accepting states + compute reachability probabilities BitSet acc; if (product.getAcceptance() instanceof AcceptanceReach) { diff --git a/prism/src/explicit/ModelExplicit.java b/prism/src/explicit/ModelExplicit.java index 94844fe8..7915e2e1 100644 --- a/prism/src/explicit/ModelExplicit.java +++ b/prism/src/explicit/ModelExplicit.java @@ -153,6 +153,7 @@ public abstract class ModelExplicit implements Model */ public void setStatesList(List statesList) { + new Exception().printStackTrace(); this.statesList = statesList; } diff --git a/prism/src/explicit/StateModelChecker.java b/prism/src/explicit/StateModelChecker.java index fb381d97..eea26b09 100644 --- a/prism/src/explicit/StateModelChecker.java +++ b/prism/src/explicit/StateModelChecker.java @@ -86,6 +86,12 @@ public class StateModelChecker extends PrismComponent // Additional flags/settings not included in PrismSettings + // Export product model info? + protected boolean exportProductTrans = false; + protected String exportProductTransFilename = null; + protected boolean exportProductStates = false; + protected String exportProductStatesFilename = null; + // Store the final results vector after model checking? protected boolean storeVector = false; @@ -196,6 +202,26 @@ public class StateModelChecker extends PrismComponent this.verbosity = verbosity; } + public void setExportProductTrans(boolean b) throws PrismException + { + exportProductTrans = b; + } + + public void setExportProductTransFilename(String s) throws PrismException + { + exportProductTransFilename = s; + } + + public void setExportProductStates(boolean b) throws PrismException + { + exportProductStates = b; + } + + public void setExportProductStatesFilename(String s) throws PrismException + { + exportProductStatesFilename = s; + } + /** * Specify whether or not to store the final results vector after model checking. */ @@ -227,6 +253,26 @@ public class StateModelChecker extends PrismComponent return verbosity; } + public boolean getExportProductTrans() + { + return exportProductTrans; + } + + public String getExportProductTransFilename() + { + return exportProductTransFilename; + } + + public boolean getExportProductStates() + { + return exportProductStates; + } + + public String getExportProductStatesFilename() + { + return exportProductStatesFilename; + } + /** * Whether or not to store the final results vector after model checking. */ diff --git a/prism/src/prism/Prism.java b/prism/src/prism/Prism.java index 02957a12..3b24169d 100644 --- a/prism/src/prism/Prism.java +++ b/prism/src/prism/Prism.java @@ -3571,6 +3571,10 @@ public class Prism extends PrismComponent implements PrismSettingsListener explicit.StateModelChecker mc = explicit.StateModelChecker.createModelChecker(currentModelType, this); mc.setModulesFileAndPropertiesFile(currentModulesFile, propertiesFile); // Pass any additional local settings + mc.setExportProductTrans(exportProductTrans); + mc.setExportProductTransFilename(exportProductTransFilename); + mc.setExportProductStates(exportProductStates); + mc.setExportProductStatesFilename(exportProductStatesFilename); mc.setStoreVector(storeVector); mc.setGenStrat(genStrat); mc.setDoBisim(doBisim);