From be5cdf908a2b19d6c9f0a48e64b3ea5fa9ee7b6a Mon Sep 17 00:00:00 2001 From: Dave Parker Date: Sat, 31 Jan 2015 10:43:20 +0000 Subject: [PATCH] Provide getConstantValues() for model checkers, allowing other classes to access the constants. [Joachim Klein] git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@9596 bbc10eb1-c90d-0410-af57-cb519fbb1720 --- prism/src/explicit/StateModelChecker.java | 6 ++++++ prism/src/prism/ModelChecker.java | 2 ++ prism/src/prism/StateModelChecker.java | 7 +++++++ 3 files changed, 15 insertions(+) diff --git a/prism/src/explicit/StateModelChecker.java b/prism/src/explicit/StateModelChecker.java index b8e5ee4c..f29f5b26 100644 --- a/prism/src/explicit/StateModelChecker.java +++ b/prism/src/explicit/StateModelChecker.java @@ -252,6 +252,12 @@ public class StateModelChecker extends PrismComponent return doBisim; } + /** Get the constant values (both from the modules file and the properties file) */ + public Values getConstantValues() + { + return constantValues; + } + // Other setters/getters /** diff --git a/prism/src/prism/ModelChecker.java b/prism/src/prism/ModelChecker.java index 1239747d..2f00cf41 100644 --- a/prism/src/prism/ModelChecker.java +++ b/prism/src/prism/ModelChecker.java @@ -27,6 +27,7 @@ package prism; import jdd.JDDNode; +import parser.Values; import parser.ast.*; // interface for model checker classes @@ -36,6 +37,7 @@ public interface ModelChecker public Result check(Expression expr) throws PrismException; public StateValues checkExpression(Expression expr) throws PrismException; public JDDNode checkExpressionDD(Expression expr) throws PrismException; + public Values getConstantValues(); } //------------------------------------------------------------------------------ diff --git a/prism/src/prism/StateModelChecker.java b/prism/src/prism/StateModelChecker.java index d9abfef0..cffd05d9 100644 --- a/prism/src/prism/StateModelChecker.java +++ b/prism/src/prism/StateModelChecker.java @@ -1392,6 +1392,13 @@ public class StateModelChecker implements ModelChecker throw new PrismException("Invalid reward structure index \"" + rs + "\""); return transRewards; } + + /** Get the constant values (both from the modules file and the properties file) */ + @Override + public Values getConstantValues() + { + return constantValues; + } } // ------------------------------------------------------------------------------