From d48e088cdb5d34e82e9240407334c01f30ea3c39 Mon Sep 17 00:00:00 2001 From: Dave Parker Date: Mon, 17 May 2010 14:12:11 +0000 Subject: [PATCH] PTA bug fixes: model labels, multiple properties. git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@1895 bbc10eb1-c90d-0410-af57-cb519fbb1720 --- prism/src/pta/Modules2PTA.java | 5 ++++- prism/src/pta/PTAModelChecker.java | 15 +++++++++++---- 2 files changed, 15 insertions(+), 5 deletions(-) diff --git a/prism/src/pta/Modules2PTA.java b/prism/src/pta/Modules2PTA.java index 586136d2..d896b40b 100644 --- a/prism/src/pta/Modules2PTA.java +++ b/prism/src/pta/Modules2PTA.java @@ -83,7 +83,10 @@ public class Modules2PTA // Clone the model file, replace any constants with values, // and simplify any expressions as much as possible. - modulesFile = (ModulesFile) modulesFile.replaceConstants(constantValues).simplify(); + modulesFile = (ModulesFile) modulesFile.deepCopy().replaceConstants(constantValues).simplify(); + + // Remove labels from (cloned) model - these are not translated. + modulesFile.setLabelList(new LabelList()); // Go through list of modules numModules = modulesFile.getNumModules(); diff --git a/prism/src/pta/PTAModelChecker.java b/prism/src/pta/PTAModelChecker.java index 3178a3b6..adc98fd3 100644 --- a/prism/src/pta/PTAModelChecker.java +++ b/prism/src/pta/PTAModelChecker.java @@ -72,8 +72,15 @@ public class PTAModelChecker if (propertiesFile != null) constantValues.addValues(propertiesFile.getConstantValues()); - // Get combined label list, expand constants - labelList = propertiesFile.getCombinedLabelList(); + // Build a combined label list and expand any constants + // (note labels in model are ignored (removed) during PTA translation so need to store here) + labelList = new LabelList(); + for (int i = 0; i < modulesFile.getLabelList().size(); i++) { + labelList.addLabel(modulesFile.getLabelList().getLabelNameIdent(i), modulesFile.getLabelList().getLabel(i).deepCopy()); + } + for (int i = 0; i < propertiesFile.getLabelList().size(); i++) { + labelList.addLabel(propertiesFile.getLabelList().getLabelNameIdent(i), propertiesFile.getLabelList().getLabel(i).deepCopy()); + } labelList = (LabelList) labelList.replaceConstants(constantValues); // Build mapping from all (original model) variables to non-clocks only @@ -101,7 +108,7 @@ public class PTAModelChecker // Starting model checking timer = System.currentTimeMillis(); - + // Translate ModulesFile object into a PTA object mainLog.println("\nBuilding PTA..."); m2pta = new Modules2PTA(prism, modulesFile); @@ -117,7 +124,7 @@ public class PTAModelChecker // Model checking complete timer = System.currentTimeMillis() - timer; mainLog.println("\nModel checking completed in " + (timer / 1000.0) + " secs."); - + // Print result to log resultString = "Result"; if (!("Result".equals(expr.getResultName())))