diff --git a/src/builder/DdPrismModelBuilder.cpp b/src/builder/DdPrismModelBuilder.cpp index b45269dc4..5a1a38b98 100644 --- a/src/builder/DdPrismModelBuilder.cpp +++ b/src/builder/DdPrismModelBuilder.cpp @@ -1218,9 +1218,7 @@ namespace storm { transitionRewards.get() /= stateActionDd; } } - - stateActionRewards.get().exportToDot("prismrew.dot"); - + return storm::models::symbolic::StandardRewardModel(stateRewards, stateActionRewards, transitionRewards); } diff --git a/test/functional/builder/DdPrismModelBuilderTest.cpp b/test/functional/builder/DdPrismModelBuilderTest.cpp index a6b73779a..fa05bf3e0 100644 --- a/test/functional/builder/DdPrismModelBuilderTest.cpp +++ b/test/functional/builder/DdPrismModelBuilderTest.cpp @@ -3,6 +3,7 @@ #include "src/settings/SettingMemento.h" #include "src/settings/SettingsManager.h" #include "src/settings/modules/IOSettings.h" +#include "src/storage/SymbolicModelDescription.h" #include "src/models/symbolic/Dtmc.h" #include "src/models/symbolic/Ctmc.h" #include "src/models/symbolic/Mdp.h" @@ -11,56 +12,66 @@ #include "src/builder/DdPrismModelBuilder.h" TEST(DdPrismModelBuilderTest_Sylvan, Dtmc) { - storm::prism::Program program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/die.pm"); + storm::storage::SymbolicModelDescription modelDescription = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/die.pm"); + storm::prism::Program program = modelDescription.preprocess().asPrismProgram(); std::shared_ptr> model = storm::builder::DdPrismModelBuilder().build(program); EXPECT_EQ(13ul, model->getNumberOfStates()); EXPECT_EQ(20ul, model->getNumberOfTransitions()); - program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/brp-16-2.pm"); + modelDescription = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/brp-16-2.pm"); + program = modelDescription.preprocess().asPrismProgram(); model = storm::builder::DdPrismModelBuilder().build(program); EXPECT_EQ(677ul, model->getNumberOfStates()); EXPECT_EQ(867ul, model->getNumberOfTransitions()); - program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/crowds-5-5.pm"); + modelDescription = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/crowds-5-5.pm"); + program = modelDescription.preprocess().asPrismProgram(); model = storm::builder::DdPrismModelBuilder().build(program); EXPECT_EQ(8607ul, model->getNumberOfStates()); EXPECT_EQ(15113ul, model->getNumberOfTransitions()); - program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/leader-3-5.pm"); + modelDescription = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/leader-3-5.pm"); + program = modelDescription.preprocess().asPrismProgram(); model = storm::builder::DdPrismModelBuilder().build(program); EXPECT_EQ(273ul, model->getNumberOfStates()); EXPECT_EQ(397ul, model->getNumberOfTransitions()); - program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/nand-5-2.pm"); + modelDescription = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/nand-5-2.pm"); + program = modelDescription.preprocess().asPrismProgram(); model = storm::builder::DdPrismModelBuilder().build(program); EXPECT_EQ(1728ul, model->getNumberOfStates()); EXPECT_EQ(2505ul, model->getNumberOfTransitions()); } TEST(DdPrismModelBuilderTest_Cudd, Dtmc) { - storm::prism::Program program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/die.pm"); - + storm::storage::SymbolicModelDescription modelDescription = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/die.pm"); + storm::prism::Program program = modelDescription.preprocess().asPrismProgram(); + std::shared_ptr> model = storm::builder::DdPrismModelBuilder().build(program); EXPECT_EQ(13ul, model->getNumberOfStates()); EXPECT_EQ(20ul, model->getNumberOfTransitions()); - program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/brp-16-2.pm"); + modelDescription = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/brp-16-2.pm"); + program = modelDescription.preprocess().asPrismProgram(); model = storm::builder::DdPrismModelBuilder().build(program); EXPECT_EQ(677ul, model->getNumberOfStates()); EXPECT_EQ(867ul, model->getNumberOfTransitions()); - program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/crowds-5-5.pm"); + modelDescription = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/crowds-5-5.pm"); + program = modelDescription.preprocess().asPrismProgram(); model = storm::builder::DdPrismModelBuilder().build(program); EXPECT_EQ(8607ul, model->getNumberOfStates()); EXPECT_EQ(15113ul, model->getNumberOfTransitions()); - program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/leader-3-5.pm"); + modelDescription = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/leader-3-5.pm"); + program = modelDescription.preprocess().asPrismProgram(); model = storm::builder::DdPrismModelBuilder().build(program); EXPECT_EQ(273ul, model->getNumberOfStates()); EXPECT_EQ(397ul, model->getNumberOfTransitions()); - program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/nand-5-2.pm"); + modelDescription = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/nand-5-2.pm"); + program = modelDescription.preprocess().asPrismProgram(); model = storm::builder::DdPrismModelBuilder().build(program); EXPECT_EQ(1728ul, model->getNumberOfStates()); EXPECT_EQ(2505ul, model->getNumberOfTransitions()); @@ -70,28 +81,33 @@ TEST(DdPrismModelBuilderTest_Sylvan, Ctmc) { // Set the PRISM compatibility mode temporarily. It is set to its old value once the returned object is destructed. std::unique_ptr enablePrismCompatibility = storm::settings::mutableIOSettings().overridePrismCompatibilityMode(true); - storm::prism::Program program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/cluster2.sm"); + storm::storage::SymbolicModelDescription modelDescription = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/cluster2.sm"); + storm::prism::Program program = modelDescription.preprocess().asPrismProgram(); std::shared_ptr> model = storm::builder::DdPrismModelBuilder().build(program); EXPECT_EQ(276ul, model->getNumberOfStates()); EXPECT_EQ(1120ul, model->getNumberOfTransitions()); - program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/embedded2.sm"); + modelDescription = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/embedded2.sm"); + program = modelDescription.preprocess().asPrismProgram(); model = storm::builder::DdPrismModelBuilder().build(program); EXPECT_EQ(3478ul, model->getNumberOfStates()); EXPECT_EQ(14639ul, model->getNumberOfTransitions()); - program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/polling2.sm"); + modelDescription = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/polling2.sm"); + program = modelDescription.preprocess().asPrismProgram(); model = storm::builder::DdPrismModelBuilder().build(program); EXPECT_EQ(12ul, model->getNumberOfStates()); EXPECT_EQ(22ul, model->getNumberOfTransitions()); - program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/fms2.sm"); + modelDescription = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/fms2.sm"); + program = modelDescription.preprocess().asPrismProgram(); model = storm::builder::DdPrismModelBuilder().build(program); EXPECT_EQ(810ul, model->getNumberOfStates()); EXPECT_EQ(3699ul, model->getNumberOfTransitions()); - program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/tandem5.sm"); + modelDescription = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/tandem5.sm"); + program = modelDescription.preprocess().asPrismProgram(); model = storm::builder::DdPrismModelBuilder().build(program); EXPECT_EQ(66ul, model->getNumberOfStates()); EXPECT_EQ(189ul, model->getNumberOfTransitions()); @@ -101,35 +117,41 @@ TEST(DdPrismModelBuilderTest_Cudd, Ctmc) { // Set the PRISM compatibility mode temporarily. It is set to its old value once the returned object is destructed. std::unique_ptr enablePrismCompatibility = storm::settings::mutableIOSettings().overridePrismCompatibilityMode(true); - storm::prism::Program program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/cluster2.sm"); + storm::storage::SymbolicModelDescription modelDescription = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/cluster2.sm"); + storm::prism::Program program = modelDescription.preprocess().asPrismProgram(); std::shared_ptr> model = storm::builder::DdPrismModelBuilder().build(program); EXPECT_EQ(276ul, model->getNumberOfStates()); EXPECT_EQ(1120ul, model->getNumberOfTransitions()); - program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/embedded2.sm"); + modelDescription = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/embedded2.sm"); + program = modelDescription.preprocess().asPrismProgram(); model = storm::builder::DdPrismModelBuilder().build(program); EXPECT_EQ(3478ul, model->getNumberOfStates()); EXPECT_EQ(14639ul, model->getNumberOfTransitions()); - program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/polling2.sm"); + modelDescription = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/polling2.sm"); + program = modelDescription.preprocess().asPrismProgram(); model = storm::builder::DdPrismModelBuilder().build(program); EXPECT_EQ(12ul, model->getNumberOfStates()); EXPECT_EQ(22ul, model->getNumberOfTransitions()); - program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/fms2.sm"); + modelDescription = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/fms2.sm"); + program = modelDescription.preprocess().asPrismProgram(); model = storm::builder::DdPrismModelBuilder().build(program); EXPECT_EQ(810ul, model->getNumberOfStates()); EXPECT_EQ(3699ul, model->getNumberOfTransitions()); - program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/tandem5.sm"); + modelDescription = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/tandem5.sm"); + program = modelDescription.preprocess().asPrismProgram(); model = storm::builder::DdPrismModelBuilder().build(program); EXPECT_EQ(66ul, model->getNumberOfStates()); EXPECT_EQ(189ul, model->getNumberOfTransitions()); } TEST(DdPrismModelBuilderTest_Sylvan, Mdp) { - storm::prism::Program program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/two_dice.nm"); + storm::storage::SymbolicModelDescription modelDescription = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/two_dice.nm"); + storm::prism::Program program = modelDescription.preprocess().asPrismProgram(); std::shared_ptr> model = storm::builder::DdPrismModelBuilder().build(program); EXPECT_TRUE(model->getType() == storm::models::ModelType::Mdp); @@ -139,9 +161,9 @@ TEST(DdPrismModelBuilderTest_Sylvan, Mdp) { EXPECT_EQ(436ul, mdp->getNumberOfTransitions()); EXPECT_EQ(254ul, mdp->getNumberOfChoices()); - program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/leader3.nm"); + modelDescription = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/leader3.nm"); + program = modelDescription.preprocess().asPrismProgram(); model = storm::builder::DdPrismModelBuilder().build(program); - EXPECT_TRUE(model->getType() == storm::models::ModelType::Mdp); mdp = model->as>(); @@ -149,9 +171,9 @@ TEST(DdPrismModelBuilderTest_Sylvan, Mdp) { EXPECT_EQ(654ul, mdp->getNumberOfTransitions()); EXPECT_EQ(573ul, mdp->getNumberOfChoices()); - program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/coin2-2.nm"); + modelDescription = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/coin2-2.nm"); + program = modelDescription.preprocess().asPrismProgram(); model = storm::builder::DdPrismModelBuilder().build(program); - EXPECT_TRUE(model->getType() == storm::models::ModelType::Mdp); mdp = model->as>(); @@ -159,9 +181,9 @@ TEST(DdPrismModelBuilderTest_Sylvan, Mdp) { EXPECT_EQ(492ul, mdp->getNumberOfTransitions()); EXPECT_EQ(400ul, mdp->getNumberOfChoices()); - program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/csma2-2.nm"); + modelDescription = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/csma2-2.nm"); + program = modelDescription.preprocess().asPrismProgram(); model = storm::builder::DdPrismModelBuilder().build(program); - EXPECT_TRUE(model->getType() == storm::models::ModelType::Mdp); mdp = model->as>(); @@ -169,9 +191,9 @@ TEST(DdPrismModelBuilderTest_Sylvan, Mdp) { EXPECT_EQ(1282ul, mdp->getNumberOfTransitions()); EXPECT_EQ(1054ul, mdp->getNumberOfChoices()); - program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/firewire3-0.5.nm"); + modelDescription = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/firewire3-0.5.nm"); + program = modelDescription.preprocess().asPrismProgram(); model = storm::builder::DdPrismModelBuilder().build(program); - EXPECT_TRUE(model->getType() == storm::models::ModelType::Mdp); mdp = model->as>(); @@ -179,9 +201,9 @@ TEST(DdPrismModelBuilderTest_Sylvan, Mdp) { EXPECT_EQ(5585ul, mdp->getNumberOfTransitions()); EXPECT_EQ(5519ul, mdp->getNumberOfChoices()); - program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/wlan0-2-2.nm"); + modelDescription = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/wlan0-2-2.nm"); + program = modelDescription.preprocess().asPrismProgram(); model = storm::builder::DdPrismModelBuilder().build(program); - EXPECT_TRUE(model->getType() == storm::models::ModelType::Mdp); mdp = model->as>(); @@ -191,9 +213,10 @@ TEST(DdPrismModelBuilderTest_Sylvan, Mdp) { } TEST(DdPrismModelBuilderTest_Cudd, Mdp) { - storm::prism::Program program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/two_dice.nm"); + storm::storage::SymbolicModelDescription modelDescription = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/two_dice.nm"); + storm::prism::Program program = modelDescription.preprocess().asPrismProgram(); std::shared_ptr> model = storm::builder::DdPrismModelBuilder().build(program); - + EXPECT_TRUE(model->getType() == storm::models::ModelType::Mdp); std::shared_ptr> mdp = model->as>(); @@ -201,9 +224,9 @@ TEST(DdPrismModelBuilderTest_Cudd, Mdp) { EXPECT_EQ(436ul, mdp->getNumberOfTransitions()); EXPECT_EQ(254ul, mdp->getNumberOfChoices()); - program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/leader3.nm"); + modelDescription = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/leader3.nm"); + program = modelDescription.preprocess().asPrismProgram(); model = storm::builder::DdPrismModelBuilder().build(program); - EXPECT_TRUE(model->getType() == storm::models::ModelType::Mdp); mdp = model->as>(); @@ -211,9 +234,9 @@ TEST(DdPrismModelBuilderTest_Cudd, Mdp) { EXPECT_EQ(654ul, mdp->getNumberOfTransitions()); EXPECT_EQ(573ul, mdp->getNumberOfChoices()); - program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/coin2-2.nm"); + modelDescription = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/coin2-2.nm"); + program = modelDescription.preprocess().asPrismProgram(); model = storm::builder::DdPrismModelBuilder().build(program); - EXPECT_TRUE(model->getType() == storm::models::ModelType::Mdp); mdp = model->as>(); @@ -221,9 +244,9 @@ TEST(DdPrismModelBuilderTest_Cudd, Mdp) { EXPECT_EQ(492ul, mdp->getNumberOfTransitions()); EXPECT_EQ(400ul, mdp->getNumberOfChoices()); - program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/csma2-2.nm"); + modelDescription = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/csma2-2.nm"); + program = modelDescription.preprocess().asPrismProgram(); model = storm::builder::DdPrismModelBuilder().build(program); - EXPECT_TRUE(model->getType() == storm::models::ModelType::Mdp); mdp = model->as>(); @@ -231,9 +254,9 @@ TEST(DdPrismModelBuilderTest_Cudd, Mdp) { EXPECT_EQ(1282ul, mdp->getNumberOfTransitions()); EXPECT_EQ(1054ul, mdp->getNumberOfChoices()); - program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/firewire3-0.5.nm"); + modelDescription = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/firewire3-0.5.nm"); + program = modelDescription.preprocess().asPrismProgram(); model = storm::builder::DdPrismModelBuilder().build(program); - EXPECT_TRUE(model->getType() == storm::models::ModelType::Mdp); mdp = model->as>(); @@ -241,9 +264,9 @@ TEST(DdPrismModelBuilderTest_Cudd, Mdp) { EXPECT_EQ(5585ul, mdp->getNumberOfTransitions()); EXPECT_EQ(5519ul, mdp->getNumberOfChoices()); - program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/wlan0-2-2.nm"); + modelDescription = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/wlan0-2-2.nm"); + program = modelDescription.preprocess().asPrismProgram(); model = storm::builder::DdPrismModelBuilder().build(program); - EXPECT_TRUE(model->getType() == storm::models::ModelType::Mdp); mdp = model->as>(); @@ -253,7 +276,8 @@ TEST(DdPrismModelBuilderTest_Cudd, Mdp) { } TEST(DdPrismModelBuilderTest_Sylvan, Composition) { - storm::prism::Program program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/system_composition.nm"); + storm::storage::SymbolicModelDescription modelDescription = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/system_composition.nm"); + storm::prism::Program program = modelDescription.preprocess().asPrismProgram(); std::shared_ptr> model = storm::builder::DdPrismModelBuilder().build(program); @@ -264,10 +288,9 @@ TEST(DdPrismModelBuilderTest_Sylvan, Composition) { EXPECT_EQ(61ul, mdp->getNumberOfTransitions()); EXPECT_EQ(61ul, mdp->getNumberOfChoices()); - program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/system_composition2.nm"); - + modelDescription = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/system_composition2.nm"); + program = modelDescription.preprocess().asPrismProgram(); model = storm::builder::DdPrismModelBuilder().build(program); - EXPECT_TRUE(model->getType() == storm::models::ModelType::Mdp); mdp = model->as>(); @@ -277,7 +300,8 @@ TEST(DdPrismModelBuilderTest_Sylvan, Composition) { } TEST(DdPrismModelBuilderTest_Cudd, Composition) { - storm::prism::Program program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/system_composition.nm"); + storm::storage::SymbolicModelDescription modelDescription = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/system_composition.nm"); + storm::prism::Program program = modelDescription.preprocess().asPrismProgram(); std::shared_ptr> model = storm::builder::DdPrismModelBuilder().build(program); @@ -288,10 +312,9 @@ TEST(DdPrismModelBuilderTest_Cudd, Composition) { EXPECT_EQ(61ul, mdp->getNumberOfTransitions()); EXPECT_EQ(61ul, mdp->getNumberOfChoices()); - program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/system_composition2.nm"); - + modelDescription = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/system_composition2.nm"); + program = modelDescription.preprocess().asPrismProgram(); model = storm::builder::DdPrismModelBuilder().build(program); - EXPECT_TRUE(model->getType() == storm::models::ModelType::Mdp); mdp = model->as>(); diff --git a/test/functional/modelchecker/GmmxxHybridCtmcCslModelCheckerTest.cpp b/test/functional/modelchecker/GmmxxHybridCtmcCslModelCheckerTest.cpp index c8ec4d75c..96450fa35 100644 --- a/test/functional/modelchecker/GmmxxHybridCtmcCslModelCheckerTest.cpp +++ b/test/functional/modelchecker/GmmxxHybridCtmcCslModelCheckerTest.cpp @@ -6,6 +6,7 @@ #include "src/logic/Formulas.h" #include "src/builder/DdPrismModelBuilder.h" #include "src/storage/dd/DdType.h" +#include "src/storage/SymbolicModelDescription.h" #include "src/solver/GmmxxLinearEquationSolver.h" #include "src/models/symbolic/StandardRewardModel.h" @@ -26,7 +27,8 @@ TEST(GmmxxHybridCtmcCslModelCheckerTest, Cluster_Cudd) { std::unique_ptr enablePrismCompatibility = storm::settings::mutableIOSettings().overridePrismCompatibilityMode(true); // Parse the model description. - storm::prism::Program program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/cluster2.sm"); + storm::storage::SymbolicModelDescription modelDescription = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/cluster2.sm"); + storm::prism::Program program = modelDescription.preprocess().asPrismProgram(); storm::parser::FormulaParser formulaParser(program.getManager().getSharedPointer()); std::shared_ptr formula(nullptr); @@ -123,7 +125,8 @@ TEST(GmmxxHybridCtmcCslModelCheckerTest, Cluster_Sylvan) { std::unique_ptr enablePrismCompatibility = storm::settings::mutableIOSettings().overridePrismCompatibilityMode(true); // Parse the model description. - storm::prism::Program program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/cluster2.sm"); + storm::storage::SymbolicModelDescription modelDescription = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/cluster2.sm"); + storm::prism::Program program = modelDescription.preprocess().asPrismProgram(); storm::parser::FormulaParser formulaParser(program.getManager().getSharedPointer()); std::shared_ptr formula(nullptr); @@ -220,7 +223,8 @@ TEST(GmmxxHybridCtmcCslModelCheckerTest, Embedded_Cudd) { std::unique_ptr enablePrismCompatibility = storm::settings::mutableIOSettings().overridePrismCompatibilityMode(true); // Parse the model description. - storm::prism::Program program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/embedded2.sm"); + storm::storage::SymbolicModelDescription modelDescription = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/embedded2.sm"); + storm::prism::Program program = modelDescription.preprocess().asPrismProgram(); storm::parser::FormulaParser formulaParser(program.getManager().getSharedPointer()); std::shared_ptr formula(nullptr); @@ -299,7 +303,8 @@ TEST(GmmxxHybridCtmcCslModelCheckerTest, Embedded_Sylvan) { std::unique_ptr enablePrismCompatibility = storm::settings::mutableIOSettings().overridePrismCompatibilityMode(true); // Parse the model description. - storm::prism::Program program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/embedded2.sm"); + storm::storage::SymbolicModelDescription modelDescription = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/embedded2.sm"); + storm::prism::Program program = modelDescription.preprocess().asPrismProgram(); storm::parser::FormulaParser formulaParser(program.getManager().getSharedPointer()); std::shared_ptr formula(nullptr); @@ -378,7 +383,8 @@ TEST(GmmxxHybridCtmcCslModelCheckerTest, Polling_Cudd) { std::unique_ptr enablePrismCompatibility = storm::settings::mutableIOSettings().overridePrismCompatibilityMode(true); // Parse the model description. - storm::prism::Program program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/polling2.sm"); + storm::storage::SymbolicModelDescription modelDescription = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/polling2.sm"); + storm::prism::Program program = modelDescription.preprocess().asPrismProgram(); storm::parser::FormulaParser formulaParser(program.getManager().getSharedPointer()); std::shared_ptr formula(nullptr); @@ -414,7 +420,8 @@ TEST(GmmxxHybridCtmcCslModelCheckerTest, Polling_Sylvan) { std::unique_ptr enablePrismCompatibility = storm::settings::mutableIOSettings().overridePrismCompatibilityMode(true); // Parse the model description. - storm::prism::Program program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/polling2.sm"); + storm::storage::SymbolicModelDescription modelDescription = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/polling2.sm"); + storm::prism::Program program = modelDescription.preprocess().asPrismProgram(); storm::parser::FormulaParser formulaParser(program.getManager().getSharedPointer()); std::shared_ptr formula(nullptr); @@ -457,7 +464,8 @@ TEST(GmmxxHybridCtmcCslModelCheckerTest, Tandem_Cudd) { std::unique_ptr enablePrismCompatibility = storm::settings::mutableIOSettings().overridePrismCompatibilityMode(true); // Parse the model description. - storm::prism::Program program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/tandem5.sm"); + storm::storage::SymbolicModelDescription modelDescription = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/tandem5.sm"); + storm::prism::Program program = modelDescription.preprocess().asPrismProgram(); storm::parser::FormulaParser formulaParser(program.getManager().getSharedPointer()); std::shared_ptr formula(nullptr); @@ -545,7 +553,8 @@ TEST(GmmxxHybridCtmcCslModelCheckerTest, Tandem_Sylvan) { std::unique_ptr enablePrismCompatibility = storm::settings::mutableIOSettings().overridePrismCompatibilityMode(true); // Parse the model description. - storm::prism::Program program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/tandem5.sm"); + storm::storage::SymbolicModelDescription modelDescription = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/tandem5.sm"); + storm::prism::Program program = modelDescription.preprocess().asPrismProgram(); storm::parser::FormulaParser formulaParser(program.getManager().getSharedPointer()); std::shared_ptr formula(nullptr);