diff --git a/prism/src/prism/PrismCL.java b/prism/src/prism/PrismCL.java index d32e777a..426552af 100644 --- a/prism/src/prism/PrismCL.java +++ b/prism/src/prism/PrismCL.java @@ -638,8 +638,24 @@ public class PrismCL tmpFile = "explicitbuildtest.tra"; mainLog.println("\nExporting (explicit) model to \"" + tmpFile + "1\"..."); modelExplicit.exportToPrismExplicitTra(tmpFile + "1"); - mainLog.println("\nExporting (explicit) model to \"" + tmpFile + "2\"..."); + 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 + "\""); }