From 93062b2dbaadaf7e3cd4217636a0029f84bd1899 Mon Sep 17 00:00:00 2001 From: Dave Parker Date: Tue, 4 May 2010 11:51:23 +0000 Subject: [PATCH] Addition to (temporary) test code for explicit build. git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@1876 bbc10eb1-c90d-0410-af57-cb519fbb1720 --- prism/src/prism/PrismCL.java | 18 +++++++++++++++++- 1 file changed, 17 insertions(+), 1 deletion(-) 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 + "\""); }