From b5bb87404c510e5567bb2755d283312e69b86381 Mon Sep 17 00:00:00 2001
From: TimQu <tim.quatmann@cs.rwth-aachen.de>
Date: Fri, 14 Sep 2018 17:03:53 +0200
Subject: [PATCH] replaced occurrences of 'substituteConstants' by
'substituteConstantsFormulas'
---
src/storm-conv-cli/storm-conv.cpp | 2 +-
.../generator/PrismNextStateGenerator.cpp | 2 +-
.../SparseExplorationModelChecker.cpp | 2 +-
.../storage/SymbolicModelDescription.cpp | 2 +-
src/storm/utility/prism.cpp | 2 +-
.../storm/abstraction/PrismMenuGameTest.cpp | 36 +++++++++----------
.../GameBasedDtmcModelCheckerTest.cpp | 4 +--
src/test/storm/utility/GraphTest.cpp | 4 +--
8 files changed, 27 insertions(+), 27 deletions(-)
diff --git a/src/storm-conv-cli/storm-conv.cpp b/src/storm-conv-cli/storm-conv.cpp
index 043b27bb9..09e7d6b24 100644
--- a/src/storm-conv-cli/storm-conv.cpp
+++ b/src/storm-conv-cli/storm-conv.cpp
@@ -114,7 +114,7 @@ namespace storm {
// Substitute constant definitions in program and properties.
std::string constantDefinitionString = input.getConstantDefinitionString();
auto constantDefinitions = prismProg.parseConstantDefinitions(constantDefinitionString);
- prismProg = prismProg.preprocess(constantDefinitions);
+ prismProg = storm::storage::SymbolicModelDescription(prismProg.asPrismProgram().defineUndefinedConstants(constantDefinitions).substituteConstants());
if (!properties.empty()) {
properties = storm::api::substituteConstantsInProperties(properties, constantDefinitions);
}
diff --git a/src/storm/generator/PrismNextStateGenerator.cpp b/src/storm/generator/PrismNextStateGenerator.cpp
index 61fe1e80f..a66b8b5dc 100644
--- a/src/storm/generator/PrismNextStateGenerator.cpp
+++ b/src/storm/generator/PrismNextStateGenerator.cpp
@@ -22,7 +22,7 @@ namespace storm {
namespace generator {
template<typename ValueType, typename StateType>
- PrismNextStateGenerator<ValueType, StateType>::PrismNextStateGenerator(storm::prism::Program const& program, NextStateGeneratorOptions const& options) : PrismNextStateGenerator<ValueType, StateType>(program.substituteConstants(), options, false) {
+ PrismNextStateGenerator<ValueType, StateType>::PrismNextStateGenerator(storm::prism::Program const& program, NextStateGeneratorOptions const& options) : PrismNextStateGenerator<ValueType, StateType>(program.substituteConstantsFormulas(), options, false) {
// Intentionally left empty.
}
diff --git a/src/storm/modelchecker/exploration/SparseExplorationModelChecker.cpp b/src/storm/modelchecker/exploration/SparseExplorationModelChecker.cpp
index 73e880662..f59dafb4c 100644
--- a/src/storm/modelchecker/exploration/SparseExplorationModelChecker.cpp
+++ b/src/storm/modelchecker/exploration/SparseExplorationModelChecker.cpp
@@ -37,7 +37,7 @@ namespace storm {
namespace modelchecker {
template<typename ModelType, typename StateType>
- SparseExplorationModelChecker<ModelType, StateType>::SparseExplorationModelChecker(storm::prism::Program const& program) : program(program.substituteConstants()), randomGenerator(std::chrono::system_clock::now().time_since_epoch().count()), comparator(storm::settings::getModule<storm::settings::modules::ExplorationSettings>().getPrecision()) {
+ SparseExplorationModelChecker<ModelType, StateType>::SparseExplorationModelChecker(storm::prism::Program const& program) : program(program.substituteConstantsFormulas()), randomGenerator(std::chrono::system_clock::now().time_since_epoch().count()), comparator(storm::settings::getModule<storm::settings::modules::ExplorationSettings>().getPrecision()) {
// Intentionally left empty.
}
diff --git a/src/storm/storage/SymbolicModelDescription.cpp b/src/storm/storage/SymbolicModelDescription.cpp
index 60708af6e..31606451b 100644
--- a/src/storm/storage/SymbolicModelDescription.cpp
+++ b/src/storm/storage/SymbolicModelDescription.cpp
@@ -152,7 +152,7 @@ namespace storm {
storm::jani::Model preparedModel = this->asJaniModel().defineUndefinedConstants(constantDefinitions).substituteConstants();
return SymbolicModelDescription(preparedModel);
} else if (this->isPrismProgram()) {
- return SymbolicModelDescription(this->asPrismProgram().defineUndefinedConstants(constantDefinitions).substituteConstants());
+ return SymbolicModelDescription(this->asPrismProgram().defineUndefinedConstants(constantDefinitions).substituteConstantsFormulas());
}
return *this;
}
diff --git a/src/storm/utility/prism.cpp b/src/storm/utility/prism.cpp
index a14e98d45..e3e619a48 100644
--- a/src/storm/utility/prism.cpp
+++ b/src/storm/utility/prism.cpp
@@ -18,7 +18,7 @@ namespace storm {
storm::prism::Program preprocess(storm::prism::Program const& program, std::map<storm::expressions::Variable, storm::expressions::Expression> const& constantDefinitions) {
storm::prism::Program result = program.defineUndefinedConstants(constantDefinitions);
- result = result.substituteConstants();
+ result = result.substituteConstantsFormulas();
return result;
}
diff --git a/src/test/storm/abstraction/PrismMenuGameTest.cpp b/src/test/storm/abstraction/PrismMenuGameTest.cpp
index 96c484d99..2987dea1c 100644
--- a/src/test/storm/abstraction/PrismMenuGameTest.cpp
+++ b/src/test/storm/abstraction/PrismMenuGameTest.cpp
@@ -234,7 +234,7 @@ TEST(PrismMenuGame, CrowdsAbstractionTest_Cudd) {
storm::settings::mutableAbstractionSettings().setAddAllGuards(false);
storm::prism::Program program = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/dtmc/crowds-5-5.pm");
- program = program.substituteConstants();
+ program = program.substituteConstantsFormulas();
std::vector<storm::expressions::Expression> initialPredicates;
storm::expressions::ExpressionManager& manager = program.getManager();
@@ -260,7 +260,7 @@ TEST(PrismMenuGame, CrowdsAbstractionTest_Sylvan) {
storm::settings::mutableAbstractionSettings().setAddAllGuards(false);
storm::prism::Program program = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/dtmc/crowds-5-5.pm");
- program = program.substituteConstants();
+ program = program.substituteConstantsFormulas();
std::vector<storm::expressions::Expression> initialPredicates;
storm::expressions::ExpressionManager& manager = program.getManager();
@@ -286,7 +286,7 @@ TEST(PrismMenuGame, CrowdsAbstractionAndRefinementTest_Cudd) {
storm::settings::mutableAbstractionSettings().setAddAllGuards(false);
storm::prism::Program program = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/dtmc/crowds-5-5.pm");
- program = program.substituteConstants();
+ program = program.substituteConstantsFormulas();
std::vector<storm::expressions::Expression> initialPredicates;
storm::expressions::ExpressionManager& manager = program.getManager();
@@ -314,7 +314,7 @@ TEST(PrismMenuGame, CrowdsAbstractionAndRefinementTest_Sylvan) {
storm::settings::mutableAbstractionSettings().setAddAllGuards(false);
storm::prism::Program program = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/dtmc/crowds-5-5.pm");
- program = program.substituteConstants();
+ program = program.substituteConstantsFormulas();
std::vector<storm::expressions::Expression> initialPredicates;
storm::expressions::ExpressionManager& manager = program.getManager();
@@ -342,7 +342,7 @@ TEST(PrismMenuGame, CrowdsFullAbstractionTest_Cudd) {
storm::settings::mutableAbstractionSettings().setAddAllGuards(false);
storm::prism::Program program = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/dtmc/crowds-5-5.pm");
- program = program.substituteConstants();
+ program = program.substituteConstantsFormulas();
std::vector<storm::expressions::Expression> initialPredicates;
storm::expressions::ExpressionManager& manager = program.getManager();
@@ -422,7 +422,7 @@ TEST(PrismMenuGame, CrowdsFullAbstractionTest_Sylvan) {
storm::settings::mutableAbstractionSettings().setAddAllGuards(false);
storm::prism::Program program = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/dtmc/crowds-5-5.pm");
- program = program.substituteConstants();
+ program = program.substituteConstantsFormulas();
std::vector<storm::expressions::Expression> initialPredicates;
storm::expressions::ExpressionManager& manager = program.getManager();
@@ -502,7 +502,7 @@ TEST(PrismMenuGame, TwoDiceAbstractionTest_Cudd) {
storm::settings::mutableAbstractionSettings().setAddAllGuards(false);
storm::prism::Program program = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/mdp/two_dice.nm");
- program = program.substituteConstants();
+ program = program.substituteConstantsFormulas();
program = program.flattenModules(std::make_shared<storm::utility::solver::MathsatSmtSolverFactory>());
std::vector<storm::expressions::Expression> initialPredicates;
@@ -530,7 +530,7 @@ TEST(PrismMenuGame, TwoDiceAbstractionTest_Sylvan) {
storm::settings::mutableAbstractionSettings().setAddAllGuards(false);
storm::prism::Program program = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/mdp/two_dice.nm");
- program = program.substituteConstants();
+ program = program.substituteConstantsFormulas();
program = program.flattenModules(std::make_shared<storm::utility::solver::MathsatSmtSolverFactory>());
std::vector<storm::expressions::Expression> initialPredicates;
@@ -558,7 +558,7 @@ TEST(PrismMenuGame, TwoDiceAbstractionAndRefinementTest_Cudd) {
storm::settings::mutableAbstractionSettings().setAddAllGuards(false);
storm::prism::Program program = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/mdp/two_dice.nm");
- program = program.substituteConstants();
+ program = program.substituteConstantsFormulas();
program = program.flattenModules(std::make_shared<storm::utility::solver::MathsatSmtSolverFactory>());
std::vector<storm::expressions::Expression> initialPredicates;
@@ -588,7 +588,7 @@ TEST(PrismMenuGame, TwoDiceAbstractionAndRefinementTest_Sylvan) {
storm::settings::mutableAbstractionSettings().setAddAllGuards(false);
storm::prism::Program program = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/mdp/two_dice.nm");
- program = program.substituteConstants();
+ program = program.substituteConstantsFormulas();
program = program.flattenModules(std::make_shared<storm::utility::solver::MathsatSmtSolverFactory>());
std::vector<storm::expressions::Expression> initialPredicates;
@@ -618,7 +618,7 @@ TEST(PrismMenuGame, TwoDiceFullAbstractionTest_Cudd) {
storm::settings::mutableAbstractionSettings().setAddAllGuards(false);
storm::prism::Program program = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/mdp/two_dice.nm");
- program = program.substituteConstants();
+ program = program.substituteConstantsFormulas();
program = program.flattenModules(std::make_shared<storm::utility::solver::MathsatSmtSolverFactory>());
std::vector<storm::expressions::Expression> initialPredicates;
@@ -677,7 +677,7 @@ TEST(PrismMenuGame, TwoDiceFullAbstractionTest_Sylvan) {
storm::settings::mutableAbstractionSettings().setAddAllGuards(false);
storm::prism::Program program = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/mdp/two_dice.nm");
- program = program.substituteConstants();
+ program = program.substituteConstantsFormulas();
program = program.flattenModules(std::make_shared<storm::utility::solver::MathsatSmtSolverFactory>());
std::vector<storm::expressions::Expression> initialPredicates;
@@ -736,7 +736,7 @@ TEST(PrismMenuGame, WlanAbstractionTest_Cudd) {
storm::settings::mutableAbstractionSettings().setAddAllGuards(false);
storm::prism::Program program = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/mdp/wlan0-2-4.nm");
- program = program.substituteConstants();
+ program = program.substituteConstantsFormulas();
program = program.flattenModules(std::make_shared<storm::utility::solver::MathsatSmtSolverFactory>());
std::vector<storm::expressions::Expression> initialPredicates;
@@ -765,7 +765,7 @@ TEST(PrismMenuGame, WlanAbstractionTest_Sylvan) {
storm::settings::mutableAbstractionSettings().setAddAllGuards(false);
storm::prism::Program program = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/mdp/wlan0-2-4.nm");
- program = program.substituteConstants();
+ program = program.substituteConstantsFormulas();
program = program.flattenModules(std::make_shared<storm::utility::solver::MathsatSmtSolverFactory>());
std::vector<storm::expressions::Expression> initialPredicates;
@@ -794,7 +794,7 @@ TEST(PrismMenuGame, WlanAbstractionAndRefinementTest_Cudd) {
storm::settings::mutableAbstractionSettings().setAddAllGuards(false);
storm::prism::Program program = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/mdp/wlan0-2-4.nm");
- program = program.substituteConstants();
+ program = program.substituteConstantsFormulas();
program = program.flattenModules(std::make_shared<storm::utility::solver::MathsatSmtSolverFactory>());
std::vector<storm::expressions::Expression> initialPredicates;
@@ -825,7 +825,7 @@ TEST(PrismMenuGame, WlanAbstractionAndRefinementTest_Sylvan) {
storm::settings::mutableAbstractionSettings().setAddAllGuards(false);
storm::prism::Program program = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/mdp/wlan0-2-4.nm");
- program = program.substituteConstants();
+ program = program.substituteConstantsFormulas();
program = program.flattenModules(std::make_shared<storm::utility::solver::MathsatSmtSolverFactory>());
std::vector<storm::expressions::Expression> initialPredicates;
@@ -856,7 +856,7 @@ TEST(PrismMenuGame, WlanFullAbstractionTest_Cudd) {
storm::settings::mutableAbstractionSettings().setAddAllGuards(false);
storm::prism::Program program = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/mdp/wlan0-2-4.nm");
- program = program.substituteConstants();
+ program = program.substituteConstantsFormulas();
program = program.flattenModules(std::make_shared<storm::utility::solver::MathsatSmtSolverFactory>());
std::vector<storm::expressions::Expression> initialPredicates;
@@ -983,7 +983,7 @@ TEST(PrismMenuGame, WlanFullAbstractionTest_Sylvan) {
storm::settings::mutableAbstractionSettings().setAddAllGuards(false);
storm::prism::Program program = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/mdp/wlan0-2-4.nm");
- program = program.substituteConstants();
+ program = program.substituteConstantsFormulas();
program = program.flattenModules(std::make_shared<storm::utility::solver::MathsatSmtSolverFactory>());
std::vector<storm::expressions::Expression> initialPredicates;
diff --git a/src/test/storm/modelchecker/GameBasedDtmcModelCheckerTest.cpp b/src/test/storm/modelchecker/GameBasedDtmcModelCheckerTest.cpp
index 3511aabec..1ea73c377 100644
--- a/src/test/storm/modelchecker/GameBasedDtmcModelCheckerTest.cpp
+++ b/src/test/storm/modelchecker/GameBasedDtmcModelCheckerTest.cpp
@@ -96,7 +96,7 @@ TEST(GameBasedDtmcModelCheckerTest, SynchronousLeader_Cudd) {
TEST(GameBasedDtmcModelCheckerTest, DISABLED_SynchronousLeader_Cudd) {
#endif
storm::prism::Program program = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/dtmc/leader-3-5.pm");
- program = program.substituteConstants();
+ program = program.substituteConstantsFormulas();
// A parser that we use for conveniently constructing the formulas.
storm::parser::FormulaParser formulaParser;
@@ -118,7 +118,7 @@ TEST(GameBasedDtmcModelCheckerTest, SynchronousLeader_Sylvan) {
TEST(GameBasedDtmcModelCheckerTest, DISABLED_SynchronousLeader_Sylvan) {
#endif
storm::prism::Program program = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/dtmc/leader-3-5.pm");
- program = program.substituteConstants();
+ program = program.substituteConstantsFormulas();
// A parser that we use for conveniently constructing the formulas.
storm::parser::FormulaParser formulaParser;
diff --git a/src/test/storm/utility/GraphTest.cpp b/src/test/storm/utility/GraphTest.cpp
index 3098297c0..26c17a3b8 100644
--- a/src/test/storm/utility/GraphTest.cpp
+++ b/src/test/storm/utility/GraphTest.cpp
@@ -316,7 +316,7 @@ TEST(GraphTest, SymbolicProb01StochasticGameDieSmall) {
TEST(GraphTest, SymbolicProb01StochasticGameTwoDice) {
storm::prism::Program program = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/mdp/two_dice.nm");
- program = program.substituteConstants();
+ program = program.substituteConstantsFormulas();
program = program.flattenModules(std::make_unique<storm::utility::solver::MathsatSmtSolverFactory>());
std::vector<storm::expressions::Expression> initialPredicates;
@@ -420,7 +420,7 @@ TEST(GraphTest, SymbolicProb01StochasticGameTwoDice) {
TEST(GraphTest, SymbolicProb01StochasticGameWlan) {
storm::prism::Program program = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/mdp/wlan0-2-4.nm");
- program = program.substituteConstants();
+ program = program.substituteConstantsFormulas();
program = program.flattenModules(std::make_unique<storm::utility::solver::MathsatSmtSolverFactory>());
std::vector<storm::expressions::Expression> initialPredicates;