From 16781169f7c35a936a108360bc5117e71a9a0541 Mon Sep 17 00:00:00 2001 From: Dave Parker Date: Thu, 2 Sep 2010 21:32:44 +0000 Subject: [PATCH] PTA fix: labels/rewards in models do not cause crashes. git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@2068 bbc10eb1-c90d-0410-af57-cb519fbb1720 --- prism/src/parser/ast/ModulesFile.java | 5 +++++ prism/src/pta/Modules2PTA.java | 8 ++++++-- 2 files changed, 11 insertions(+), 2 deletions(-) diff --git a/prism/src/parser/ast/ModulesFile.java b/prism/src/parser/ast/ModulesFile.java index 63cc3c2b..db9fea74 100644 --- a/prism/src/parser/ast/ModulesFile.java +++ b/prism/src/parser/ast/ModulesFile.java @@ -143,6 +143,11 @@ public class ModulesFile extends ASTElement systemDefn = s; } + public void clearRewardStructs() + { + rewardStructs.clear(); + } + public void addRewardStruct(RewardStruct r) { rewardStructs.add(r); diff --git a/prism/src/pta/Modules2PTA.java b/prism/src/pta/Modules2PTA.java index d896b40b..f1c1beba 100644 --- a/prism/src/pta/Modules2PTA.java +++ b/prism/src/pta/Modules2PTA.java @@ -85,9 +85,13 @@ public class Modules2PTA // and simplify any expressions as much as possible. modulesFile = (ModulesFile) modulesFile.deepCopy().replaceConstants(constantValues).simplify(); - // Remove labels from (cloned) model - these are not translated. + // Remove formulas/labels from (cloned) model - these are not translated. + modulesFile.setFormulaList(new FormulaList()); modulesFile.setLabelList(new LabelList()); - + + // Also remove reward structures - these are not currently used + modulesFile.clearRewardStructs(); + // Go through list of modules numModules = modulesFile.getNumModules(); pcStates = new ArrayList>(numModules);