|
|
|
@ -553,53 +553,6 @@ public class PrismCL implements PrismModelListener |
|
|
|
} |
|
|
|
} |
|
|
|
|
|
|
|
/** |
|
|
|
* Build a model, usually from the passed in modulesFileToBuild. However, if importtrans=true, |
|
|
|
* then explicit model import is done and modulesFileToBuild can be null. |
|
|
|
* This method also displays model info and checks/fixes deadlocks. |
|
|
|
* If flag 'digital' is true, then this (MDP) model was constructed |
|
|
|
* from digital clocks semantics of a PTA - might need for error reporting. |
|
|
|
*/ |
|
|
|
private void buildModel(ModulesFile modulesFileToBuild, boolean digital) throws PrismException |
|
|
|
{ |
|
|
|
// TODO |
|
|
|
/* |
|
|
|
StateList states; |
|
|
|
// If enabled, also construct model explicitly and compare (for testing purposes) |
|
|
|
if (explicitbuildtest) { |
|
|
|
String tmpFile = "'"; |
|
|
|
try { |
|
|
|
explicit.ConstructModel constructModel = new explicit.ConstructModel(prism.getSimulator(), mainLog); |
|
|
|
mainLog.println("\nConstructing model explicitly..."); |
|
|
|
explicit.Model modelExplicit = constructModel.constructModel(modulesFileToBuild); |
|
|
|
tmpFile = File.createTempFile("explicitbuildtest", ".tra").getAbsolutePath(); |
|
|
|
tmpFile = "explicitbuildtest.tra"; |
|
|
|
mainLog.println("\nExporting (explicit) model to \"" + tmpFile + "1\"..."); |
|
|
|
modelExplicit.exportToPrismExplicitTra(tmpFile + "1"); |
|
|
|
mainLog.println("\nExporting (normal) model to \"" + tmpFile + "2\"..."); |
|
|
|
prism.exportTransToFile(model, true, Prism.EXPORT_PLAIN, new File(tmpFile + "2")); |
|
|
|
explicit.ModelSimple modelExplicit2 = null; |
|
|
|
switch (model.getModelType()) { |
|
|
|
case DTMC: |
|
|
|
modelExplicit2 = new explicit.DTMCSimple(); |
|
|
|
break; |
|
|
|
case CTMC: |
|
|
|
modelExplicit2 = new explicit.CTMCSimple(); |
|
|
|
break; |
|
|
|
case MDP: |
|
|
|
modelExplicit2 = new explicit.MDPSimple(); |
|
|
|
break; |
|
|
|
} |
|
|
|
modelExplicit2.buildFromPrismExplicit(tmpFile + "2"); |
|
|
|
if (!modelExplicit.equals(modelExplicit2)) { |
|
|
|
throw new PrismException("Explicit models differ"); |
|
|
|
} |
|
|
|
} catch (IOException e) { |
|
|
|
throw new PrismException("Could not create temporary file \"" + tmpFile + "\""); |
|
|
|
} |
|
|
|
}*/ |
|
|
|
} |
|
|
|
|
|
|
|
// do any exporting requested |
|
|
|
|
|
|
|
private void doExports() |
|
|
|
|