Browse Source

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
master
Dave Parker 16 years ago
parent
commit
16781169f7
  1. 5
      prism/src/parser/ast/ModulesFile.java
  2. 8
      prism/src/pta/Modules2PTA.java

5
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);

8
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<ArrayList<State>>(numModules);

Loading…
Cancel
Save