From 90a43520c23d3ec75f7f719170bd9c9a3b173035 Mon Sep 17 00:00:00 2001 From: Dave Parker Date: Sat, 25 May 2019 00:30:44 +0100 Subject: [PATCH] Simplify ModelGenerator/ModelInfo interfaces slightly. * Remove some unneeded methods: getExploreState() and getTransitionAction(int i) * Add a default implementation of getNumVars() based on name list Existing code which implements the first two methods and annotates them with @Override needs to be changed. TestModelGenerator, ModulesFileModelGenerator, ModulesFileModelGeneratorSymbolic updated accordingly. --- prism/src/prism/ModelGenerator.java | 15 ------------ prism/src/prism/ModelInfo.java | 10 +++++++- prism/src/prism/TestModelGenerator.java | 24 ------------------- .../simulator/ModulesFileModelGenerator.java | 13 ---------- .../ModulesFileModelGeneratorSymbolic.java | 13 ---------- 5 files changed, 9 insertions(+), 66 deletions(-) diff --git a/prism/src/prism/ModelGenerator.java b/prism/src/prism/ModelGenerator.java index 3829cd25..812d3710 100644 --- a/prism/src/prism/ModelGenerator.java +++ b/prism/src/prism/ModelGenerator.java @@ -73,12 +73,6 @@ public interface ModelGenerator extends ModelInfo */ public void exploreState(State exploreState) throws PrismException; - /** - * Get the state that is currently being explored, i.e. the last one for which - * {@link #exploreState(State)} was called. Can return null if there is no such state. - */ - public State getExploreState(); - /** * Get the number of nondeterministic choices in the current state. */ @@ -104,15 +98,6 @@ public interface ModelGenerator extends ModelInfo */ public int getNumTransitions(int i) throws PrismException; - /** - * Get the action label of a transition, specified by its index. - * The label can be any Object, but will often be treated as a string, so it should at least - * have a meaningful toString() method implemented. Absence of an action label is denoted by null. - * Note: For most types of models, the action label will be the same for all transitions within - * the same nondeterministic choice, so it is better to query the action by choice, not transition. - */ - public Object getTransitionAction(int i) throws PrismException; - /** * Get the action label of a transition within a choice, specified by its index/offset. * The label can be any Object, but will often be treated as a string, so it should at least diff --git a/prism/src/prism/ModelInfo.java b/prism/src/prism/ModelInfo.java index e69b5250..23d5872a 100644 --- a/prism/src/prism/ModelInfo.java +++ b/prism/src/prism/ModelInfo.java @@ -32,6 +32,10 @@ import java.util.List; import parser.Values; import parser.VarList; +import parser.ast.Declaration; +import parser.ast.DeclarationBool; +import parser.ast.DeclarationInt; +import parser.ast.Expression; import parser.ast.RewardStruct; import parser.type.Type; @@ -105,7 +109,11 @@ public interface ModelInfo /** * Get the number of variables in the model. */ - public int getNumVars(); + public default int getNumVars() + { + // Default implementation just extracts from getVarNames() + return getVarNames().size(); + } /** * Get the names of all the variables in the model. diff --git a/prism/src/prism/TestModelGenerator.java b/prism/src/prism/TestModelGenerator.java index 09a039c6..b07a3d4d 100644 --- a/prism/src/prism/TestModelGenerator.java +++ b/prism/src/prism/TestModelGenerator.java @@ -61,12 +61,6 @@ public class TestModelGenerator implements ModelGenerator return ModelType.DTMC; } - @Override - public int getNumVars() - { - return 1; - } - @Override public List getVarNames() { @@ -79,12 +73,6 @@ public class TestModelGenerator implements ModelGenerator return varTypes; } - @Override - public int getNumLabels() - { - return 1; - } - @Override public List getLabelNames() { @@ -106,12 +94,6 @@ public class TestModelGenerator implements ModelGenerator x = ((Integer) exploreState.varValues[0]).intValue(); } - @Override - public State getExploreState() - { - return exploreState; - } - @Override public int getNumChoices() throws PrismException { @@ -124,12 +106,6 @@ public class TestModelGenerator implements ModelGenerator return x > 0 && x < n ? 2 : 1; } - @Override - public Object getTransitionAction(int i) throws PrismException - { - return null; - } - @Override public Object getTransitionAction(int i, int offset) throws PrismException { diff --git a/prism/src/simulator/ModulesFileModelGenerator.java b/prism/src/simulator/ModulesFileModelGenerator.java index e06f37b7..40c8bb1d 100644 --- a/prism/src/simulator/ModulesFileModelGenerator.java +++ b/prism/src/simulator/ModulesFileModelGenerator.java @@ -265,12 +265,6 @@ public class ModulesFileModelGenerator implements ModelGenerator transitionListBuilt = false; } - @Override - public State getExploreState() - { - return exploreState; - } - @Override public int getNumChoices() throws PrismException { @@ -289,13 +283,6 @@ public class ModulesFileModelGenerator implements ModelGenerator return getTransitionList().getChoice(index).size(); } - @Override - public String getTransitionAction(int index) throws PrismException - { - int a = getTransitionList().getTransitionModuleOrActionIndex(index); - return a < 0 ? null : modulesFile.getSynch(a - 1); - } - @Override public String getTransitionAction(int index, int offset) throws PrismException { diff --git a/prism/src/simulator/ModulesFileModelGeneratorSymbolic.java b/prism/src/simulator/ModulesFileModelGeneratorSymbolic.java index 47c1ed94..50f0531c 100644 --- a/prism/src/simulator/ModulesFileModelGeneratorSymbolic.java +++ b/prism/src/simulator/ModulesFileModelGeneratorSymbolic.java @@ -294,12 +294,6 @@ public class ModulesFileModelGeneratorSymbolic implements ModelGeneratorSymbolic transitionListBuilt = false; } - @Override - public State getExploreState() - { - return exploreState; - } - @Override public int getNumChoices() throws PrismException { @@ -318,13 +312,6 @@ public class ModulesFileModelGeneratorSymbolic implements ModelGeneratorSymbolic return getTransitionList().getChoice(index).size(); } - @Override - public String getTransitionAction(int index) throws PrismException - { - int a = getTransitionList().getTransitionModuleOrActionIndex(index); - return a < 0 ? null : modulesFile.getSynch(a - 1); - } - @Override public String getTransitionAction(int index, int offset) throws PrismException {