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 - PrismNextStateGenerator::PrismNextStateGenerator(storm::prism::Program const& program, NextStateGeneratorOptions const& options) : PrismNextStateGenerator(program.substituteConstants(), options, false) { + PrismNextStateGenerator::PrismNextStateGenerator(storm::prism::Program const& program, NextStateGeneratorOptions const& options) : PrismNextStateGenerator(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 - SparseExplorationModelChecker::SparseExplorationModelChecker(storm::prism::Program const& program) : program(program.substituteConstants()), randomGenerator(std::chrono::system_clock::now().time_since_epoch().count()), comparator(storm::settings::getModule().getPrecision()) { + SparseExplorationModelChecker::SparseExplorationModelChecker(storm::prism::Program const& program) : program(program.substituteConstantsFormulas()), randomGenerator(std::chrono::system_clock::now().time_since_epoch().count()), comparator(storm::settings::getModule().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 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 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 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 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 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 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 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()); std::vector 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()); std::vector 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()); std::vector 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()); std::vector 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()); std::vector 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()); std::vector 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()); std::vector 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()); std::vector 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()); std::vector 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()); std::vector 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()); std::vector 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()); std::vector 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()); std::vector 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()); std::vector initialPredicates;