From c2cab571f5655148a592184af3ce3fc8d0b0cf4d Mon Sep 17 00:00:00 2001 From: dehnert Date: Mon, 12 Sep 2016 11:57:36 +0200 Subject: [PATCH] made tests work again Former-commit-id: bd3e831b0d5c031fae8e7a356e42d67302fb526a [formerly cef4348674ff65b4b4be0c43dba4d94ec3dc623f] Former-commit-id: 8fd0b70c1e7f2f2277c8ef95c0d95c635c03a783 --- src/cli/cli.cpp | 2 +- src/storage/SymbolicModelDescription.cpp | 23 +- src/storage/SymbolicModelDescription.h | 7 +- src/storage/prism/ToJaniConverter.cpp | 17 ++ .../builder/DdJaniModelBuilderTest.cpp | 239 ++++++++---------- .../SparseDtmcRegionModelCheckerTest.cpp | 14 +- .../SparseMdpRegionModelCheckerTest.cpp | 4 +- .../utility/ModelInstantiatorTest.cpp | 6 +- 8 files changed, 157 insertions(+), 155 deletions(-) diff --git a/src/cli/cli.cpp b/src/cli/cli.cpp index 31a0a8afb..78cbcc042 100644 --- a/src/cli/cli.cpp +++ b/src/cli/cli.cpp @@ -219,7 +219,7 @@ namespace storm { // Get the string that assigns values to the unknown currently undefined constants in the model. std::string constantDefinitionString = ioSettings.getConstantDefinitionString(); - model.preprocess(constantDefinitionString); + model = model.preprocess(constantDefinitionString); // Then proceed to parsing the properties (if given), since the model we are building may depend on the property. std::vector> formulas; diff --git a/src/storage/SymbolicModelDescription.cpp b/src/storage/SymbolicModelDescription.cpp index adb1e2afc..3bccf3b73 100644 --- a/src/storage/SymbolicModelDescription.cpp +++ b/src/storage/SymbolicModelDescription.cpp @@ -17,6 +17,14 @@ namespace storm { // Intentionally left empty. } + SymbolicModelDescription& SymbolicModelDescription::operator=(storm::jani::Model const& model) { + this->modelDescription = model; + } + + SymbolicModelDescription& SymbolicModelDescription::operator=(storm::prism::Program const& program) { + this->modelDescription = program; + } + bool SymbolicModelDescription::hasModel() const { return static_cast(modelDescription); } @@ -47,27 +55,26 @@ namespace storm { return boost::get(modelDescription.get()); } - void SymbolicModelDescription::toJani(bool makeVariablesGlobal) { + SymbolicModelDescription SymbolicModelDescription::toJani(bool makeVariablesGlobal) const { if (this->isJaniModel()) { - return; + return *this; } if (this->isPrismProgram()) { - modelDescription = this->asPrismProgram().toJani(makeVariablesGlobal); + return SymbolicModelDescription(this->asPrismProgram().toJani(makeVariablesGlobal)); } else { STORM_LOG_THROW(false, storm::exceptions::InvalidOperationException, "Cannot transform model description to the JANI format."); } } - void SymbolicModelDescription::preprocess(std::string const& constantDefinitionString) { + SymbolicModelDescription SymbolicModelDescription::preprocess(std::string const& constantDefinitionString) const { if (this->isJaniModel()) { std::map substitution = storm::utility::jani::parseConstantDefinitionString(this->asJaniModel(), constantDefinitionString); - this->modelDescription = this->asJaniModel().defineUndefinedConstants(substitution); - this->modelDescription = this->asJaniModel().substituteConstants(); + return SymbolicModelDescription(this->asJaniModel().defineUndefinedConstants(substitution).substituteConstants()); } else if (this->isPrismProgram()) { std::map substitution = storm::utility::prism::parseConstantDefinitionString(this->asPrismProgram(), constantDefinitionString); - this->modelDescription = this->asPrismProgram().defineUndefinedConstants(substitution); - this->modelDescription = this->asPrismProgram().substituteConstants(); + return SymbolicModelDescription(this->asPrismProgram().defineUndefinedConstants(substitution).substituteConstants()); } + return *this; } } diff --git a/src/storage/SymbolicModelDescription.h b/src/storage/SymbolicModelDescription.h index cd08f9ba0..8b5b85d88 100644 --- a/src/storage/SymbolicModelDescription.h +++ b/src/storage/SymbolicModelDescription.h @@ -14,6 +14,9 @@ namespace storm { SymbolicModelDescription(storm::jani::Model const& model); SymbolicModelDescription(storm::prism::Program const& program); + SymbolicModelDescription& operator=(storm::jani::Model const& model); + SymbolicModelDescription& operator=(storm::prism::Program const& program); + bool hasModel() const; bool isJaniModel() const; bool isPrismProgram() const; @@ -24,9 +27,9 @@ namespace storm { storm::jani::Model const& asJaniModel() const; storm::prism::Program const& asPrismProgram() const; - void toJani(bool makeVariablesGlobal = true); + SymbolicModelDescription toJani(bool makeVariablesGlobal = true) const; - void preprocess(std::string const& constantDefinitionString = ""); + SymbolicModelDescription preprocess(std::string const& constantDefinitionString = "") const; private: boost::optional> modelDescription; diff --git a/src/storage/prism/ToJaniConverter.cpp b/src/storage/prism/ToJaniConverter.cpp index 7c3d859b2..33ad88fef 100644 --- a/src/storage/prism/ToJaniConverter.cpp +++ b/src/storage/prism/ToJaniConverter.cpp @@ -137,11 +137,15 @@ namespace storm { } STORM_LOG_THROW(!rewardModel.hasTransitionRewards(), storm::exceptions::NotImplementedException, "Transition reward translation currently not implemented."); } + STORM_LOG_THROW(transientEdgeAssignments.empty() || transientLocationAssignments.empty() || !program.specifiesSystemComposition(), storm::exceptions::NotImplementedException, "Cannot translate reward models from PRISM to JANI that specify a custom system composition."); // Now create the separate JANI automata from the modules of the PRISM program. While doing so, we use the // previously built mapping to make variables global that are read by more than one module. bool firstModule = true; for (auto const& module : program.getModules()) { + // Keep track of the action indices contained in this module. + std::set actionIndicesOfModule; + storm::jani::Automaton automaton(module.getName()); for (auto const& variable : module.getIntegerVariables()) { storm::jani::BoundedIntegerVariable newIntegerVariable = *storm::jani::makeBoundedIntegerVariable(variable.getName(), variable.getExpressionVariable(), variable.hasInitialValue() ? boost::make_optional(variable.getInitialValueExpression()) : boost::none, false, variable.getLowerBoundExpression(), variable.getUpperBoundExpression()); @@ -184,6 +188,8 @@ namespace storm { } for (auto const& command : module.getCommands()) { + actionIndicesOfModule.insert(command.getActionIndex()); + boost::optional rateExpression; std::vector destinations; if (program.getModelType() == Program::ModelType::CTMC || program.getModelType() == Program::ModelType::CTMDP) { @@ -224,6 +230,17 @@ namespace storm { automaton.addEdge(newEdge); } + // Now remove for all actions of this module the corresponding transient assignments, because we must + // not deal out this reward multiple times. + // NOTE: This only works for the standard composition and not for any custom compositions. This case + // must be checked for earlier. + for (auto actionIndex : actionIndicesOfModule) { + auto it = transientEdgeAssignments.find(actionIndex); + if (it != transientEdgeAssignments.end()) { + transientEdgeAssignments.erase(it); + } + } + janiModel.addAutomaton(automaton); firstModule = false; } diff --git a/test/functional/builder/DdJaniModelBuilderTest.cpp b/test/functional/builder/DdJaniModelBuilderTest.cpp index 1470e196d..3fc00e217 100644 --- a/test/functional/builder/DdJaniModelBuilderTest.cpp +++ b/test/functional/builder/DdJaniModelBuilderTest.cpp @@ -6,6 +6,7 @@ #include "src/storage/dd/Add.h" #include "src/storage/dd/Bdd.h" +#include "src/storage/SymbolicModelDescription.h" #include "src/models/symbolic/StandardRewardModel.h" #include "src/parser/PrismParser.h" @@ -16,78 +17,70 @@ #include "src/settings/modules/IOSettings.h" TEST(DdJaniModelBuilderTest_Sylvan, Dtmc) { - storm::prism::Program program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/die.pm"); - storm::jani::Model janiModel = program.toJani(true); + storm::storage::SymbolicModelDescription modelDescription = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/die.pm"); + storm::jani::Model janiModel = modelDescription.toJani(true).preprocess().asJaniModel(); - storm::builder::DdJaniModelBuilder builder(janiModel); - std::shared_ptr> model = builder.build(); + storm::builder::DdJaniModelBuilder builder; + std::shared_ptr> model = builder.build(janiModel); 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"); - janiModel = program.toJani(true); - builder = storm::builder::DdJaniModelBuilder(janiModel); - model = builder.build(); + modelDescription = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/brp-16-2.pm"); + janiModel = modelDescription.toJani(true).preprocess().asJaniModel(); + model = builder.build(janiModel); 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"); - janiModel = program.toJani(true); - builder = storm::builder::DdJaniModelBuilder(janiModel); - model = builder.build(); + modelDescription = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/crowds-5-5.pm"); + janiModel = modelDescription.toJani(true).preprocess().asJaniModel(); + model = builder.build(janiModel); 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"); - janiModel = program.toJani(true); - builder = storm::builder::DdJaniModelBuilder(janiModel); - model = builder.build(); + modelDescription = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/leader-3-5.pm"); + janiModel = modelDescription.toJani(true).preprocess().asJaniModel(); + model = builder.build(janiModel); 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"); - janiModel = program.toJani(true); + modelDescription = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/nand-5-2.pm"); + janiModel = modelDescription.toJani(true).preprocess().asJaniModel(); - builder = storm::builder::DdJaniModelBuilder(janiModel); - model = builder.build(); + model = builder.build(janiModel); EXPECT_EQ(1728ul, model->getNumberOfStates()); EXPECT_EQ(2505ul, model->getNumberOfTransitions()); } TEST(DdJaniModelBuilderTest_Cudd, Dtmc) { - storm::prism::Program program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/die.pm"); - storm::jani::Model janiModel = program.toJani(true); + storm::storage::SymbolicModelDescription modelDescription = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/die.pm"); + storm::jani::Model janiModel = modelDescription.toJani(true).preprocess().asJaniModel(); - storm::builder::DdJaniModelBuilder builder(janiModel); - std::shared_ptr> model = builder.build(); + storm::builder::DdJaniModelBuilder builder; + std::shared_ptr> model = builder.build(janiModel); 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"); - janiModel = program.toJani(true); - builder = storm::builder::DdJaniModelBuilder(janiModel); - model = builder.build(); + modelDescription = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/brp-16-2.pm"); + janiModel = modelDescription.toJani(true).preprocess().asJaniModel(); + model = builder.build(janiModel); 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"); - janiModel = program.toJani(true); - builder = storm::builder::DdJaniModelBuilder(janiModel); - model = builder.build(); + modelDescription = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/crowds-5-5.pm"); + janiModel = modelDescription.toJani(true).preprocess().asJaniModel(); + model = builder.build(janiModel); 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"); - janiModel = program.toJani(true); - builder = storm::builder::DdJaniModelBuilder(janiModel); - model = builder.build(); + modelDescription = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/leader-3-5.pm"); + janiModel = modelDescription.toJani(true).preprocess().asJaniModel(); + model = builder.build(janiModel); 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"); - janiModel = program.toJani(true); - builder = storm::builder::DdJaniModelBuilder(janiModel); - model = builder.build(); + modelDescription = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/nand-5-2.pm"); + janiModel = modelDescription.toJani(true).preprocess().asJaniModel(); + model = builder.build(janiModel); EXPECT_EQ(1728ul, model->getNumberOfStates()); EXPECT_EQ(2505ul, model->getNumberOfTransitions()); } @@ -96,38 +89,34 @@ TEST(DdJaniModelBuilderTest_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::jani::Model janiModel = program.toJani(true); - storm::builder::DdJaniModelBuilder builder(janiModel); - std::shared_ptr> model = builder.build(); + storm::storage::SymbolicModelDescription modelDescription = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/cluster2.sm"); + storm::jani::Model janiModel = modelDescription.toJani(true).preprocess().asJaniModel(); + storm::builder::DdJaniModelBuilder builder; + std::shared_ptr> model = builder.build(janiModel); EXPECT_EQ(276ul, model->getNumberOfStates()); EXPECT_EQ(1120ul, model->getNumberOfTransitions()); - program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/embedded2.sm"); - janiModel = program.toJani(true); - builder = storm::builder::DdJaniModelBuilder(janiModel); - model = builder.build(); + modelDescription = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/embedded2.sm"); + janiModel = modelDescription.toJani(true).preprocess().asJaniModel(); + model = builder.build(janiModel); EXPECT_EQ(3478ul, model->getNumberOfStates()); EXPECT_EQ(14639ul, model->getNumberOfTransitions()); - program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/polling2.sm"); - janiModel = program.toJani(true); - builder = storm::builder::DdJaniModelBuilder(janiModel); - model = builder.build(); + modelDescription = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/polling2.sm"); + janiModel = modelDescription.toJani(true).preprocess().asJaniModel(); + model = builder.build(janiModel); EXPECT_EQ(12ul, model->getNumberOfStates()); EXPECT_EQ(22ul, model->getNumberOfTransitions()); - program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/fms2.sm"); - janiModel = program.toJani(true); - builder = storm::builder::DdJaniModelBuilder(janiModel); - model = builder.build(); + modelDescription = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/fms2.sm"); + janiModel = modelDescription.toJani(true).preprocess().asJaniModel(); + model = builder.build(janiModel); EXPECT_EQ(810ul, model->getNumberOfStates()); EXPECT_EQ(3699ul, model->getNumberOfTransitions()); - program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/tandem5.sm"); - janiModel = program.toJani(true); - builder = storm::builder::DdJaniModelBuilder(janiModel); - model = builder.build(); + modelDescription = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/tandem5.sm"); + janiModel = modelDescription.toJani(true).preprocess().asJaniModel(); + model = builder.build(janiModel); EXPECT_EQ(66ul, model->getNumberOfStates()); EXPECT_EQ(189ul, model->getNumberOfTransitions()); } @@ -136,47 +125,43 @@ TEST(DdJaniModelBuilderTest_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::jani::Model janiModel = program.toJani(true); - storm::builder::DdJaniModelBuilder builder(janiModel); - std::shared_ptr> model = builder.build(); + storm::storage::SymbolicModelDescription modelDescription = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/cluster2.sm"); + storm::jani::Model janiModel = modelDescription.toJani(true).preprocess().asJaniModel(); + storm::builder::DdJaniModelBuilder builder; + std::shared_ptr> model = builder.build(janiModel); EXPECT_EQ(276ul, model->getNumberOfStates()); EXPECT_EQ(1120ul, model->getNumberOfTransitions()); - program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/embedded2.sm"); - janiModel = program.toJani(true); - builder = storm::builder::DdJaniModelBuilder(janiModel); - model = builder.build(); + modelDescription = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/embedded2.sm"); + janiModel = modelDescription.toJani(true).preprocess().asJaniModel(); + model = builder.build(janiModel); EXPECT_EQ(3478ul, model->getNumberOfStates()); EXPECT_EQ(14639ul, model->getNumberOfTransitions()); - program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/polling2.sm"); - janiModel = program.toJani(true); - builder = storm::builder::DdJaniModelBuilder(janiModel); - model = builder.build(); + modelDescription = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/polling2.sm"); + janiModel = modelDescription.toJani(true).preprocess().asJaniModel(); + model = builder.build(janiModel); EXPECT_EQ(12ul, model->getNumberOfStates()); EXPECT_EQ(22ul, model->getNumberOfTransitions()); - program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/fms2.sm"); - janiModel = program.toJani(true); - builder = storm::builder::DdJaniModelBuilder(janiModel); - model = builder.build(); + modelDescription = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/fms2.sm"); + janiModel = modelDescription.toJani(true).preprocess().asJaniModel(); + model = builder.build(janiModel); EXPECT_EQ(810ul, model->getNumberOfStates()); EXPECT_EQ(3699ul, model->getNumberOfTransitions()); - program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/tandem5.sm"); - janiModel = program.toJani(true); - builder = storm::builder::DdJaniModelBuilder(janiModel); - model = builder.build(); + modelDescription = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/tandem5.sm"); + janiModel = modelDescription.toJani(true).preprocess().asJaniModel(); + model = builder.build(janiModel); EXPECT_EQ(66ul, model->getNumberOfStates()); EXPECT_EQ(189ul, model->getNumberOfTransitions()); } TEST(DdJaniModelBuilderTest_Sylvan, Mdp) { - storm::prism::Program program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/two_dice.nm"); - storm::jani::Model janiModel = program.toJani(true); - storm::builder::DdJaniModelBuilder builder(janiModel); - std::shared_ptr> model = builder.build(); + storm::storage::SymbolicModelDescription modelDescription = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/two_dice.nm"); + storm::jani::Model janiModel = modelDescription.toJani(true).preprocess().asJaniModel(); + storm::builder::DdJaniModelBuilder builder; + std::shared_ptr> model = builder.build(janiModel); EXPECT_TRUE(model->getType() == storm::models::ModelType::Mdp); std::shared_ptr> mdp = model->as>(); @@ -185,10 +170,9 @@ TEST(DdJaniModelBuilderTest_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"); - janiModel = program.toJani(true); - builder = storm::builder::DdJaniModelBuilder(janiModel); - model = builder.build(); + modelDescription = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/leader3.nm"); + janiModel = modelDescription.toJani(true).preprocess().asJaniModel(); + model = builder.build(janiModel); EXPECT_TRUE(model->getType() == storm::models::ModelType::Mdp); mdp = model->as>(); @@ -197,10 +181,9 @@ TEST(DdJaniModelBuilderTest_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"); - janiModel = program.toJani(true); - builder = storm::builder::DdJaniModelBuilder(janiModel); - model = builder.build(); + modelDescription = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/coin2-2.nm"); + janiModel = modelDescription.toJani(true).preprocess().asJaniModel(); + model = builder.build(janiModel); EXPECT_TRUE(model->getType() == storm::models::ModelType::Mdp); mdp = model->as>(); @@ -209,10 +192,9 @@ TEST(DdJaniModelBuilderTest_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"); - janiModel = program.toJani(true); - builder = storm::builder::DdJaniModelBuilder(janiModel); - model = builder.build(); + modelDescription = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/csma2-2.nm"); + janiModel = modelDescription.toJani(true).preprocess().asJaniModel(); + model = builder.build(janiModel); EXPECT_TRUE(model->getType() == storm::models::ModelType::Mdp); mdp = model->as>(); @@ -221,10 +203,9 @@ TEST(DdJaniModelBuilderTest_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"); - janiModel = program.toJani(true); - builder = storm::builder::DdJaniModelBuilder(janiModel); - model = builder.build(); + modelDescription = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/firewire3-0.5.nm"); + janiModel = modelDescription.toJani(true).preprocess().asJaniModel(); + model = builder.build(janiModel); EXPECT_TRUE(model->getType() == storm::models::ModelType::Mdp); mdp = model->as>(); @@ -233,10 +214,9 @@ TEST(DdJaniModelBuilderTest_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"); - janiModel = program.toJani(true); - builder = storm::builder::DdJaniModelBuilder(janiModel); - model = builder.build(); + modelDescription = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/wlan0-2-2.nm"); + janiModel = modelDescription.toJani(true).preprocess().asJaniModel(); + model = builder.build(janiModel); EXPECT_TRUE(model->getType() == storm::models::ModelType::Mdp); mdp = model->as>(); @@ -247,10 +227,10 @@ TEST(DdJaniModelBuilderTest_Sylvan, Mdp) { } TEST(DdJaniModelBuilderTest_Cudd, Mdp) { - storm::prism::Program program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/two_dice.nm"); - storm::jani::Model janiModel = program.toJani(true); - storm::builder::DdJaniModelBuilder builder(janiModel); - std::shared_ptr> model = builder.build(); + storm::storage::SymbolicModelDescription modelDescription = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/two_dice.nm"); + storm::jani::Model janiModel = modelDescription.toJani(true).preprocess().asJaniModel(); + storm::builder::DdJaniModelBuilder builder; + std::shared_ptr> model = builder.build(janiModel); EXPECT_TRUE(model->getType() == storm::models::ModelType::Mdp); std::shared_ptr> mdp = model->as>(); @@ -259,10 +239,9 @@ TEST(DdJaniModelBuilderTest_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"); - janiModel = program.toJani(true); - builder = storm::builder::DdJaniModelBuilder(janiModel); - model = builder.build(); + modelDescription = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/leader3.nm"); + janiModel = modelDescription.toJani(true).preprocess().asJaniModel(); + model = builder.build(janiModel); EXPECT_TRUE(model->getType() == storm::models::ModelType::Mdp); mdp = model->as>(); @@ -271,10 +250,9 @@ TEST(DdJaniModelBuilderTest_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"); - janiModel = program.toJani(true); - builder = storm::builder::DdJaniModelBuilder(janiModel); - model = builder.build(); + modelDescription = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/coin2-2.nm"); + janiModel = modelDescription.toJani(true).preprocess().asJaniModel(); + model = builder.build(janiModel); EXPECT_TRUE(model->getType() == storm::models::ModelType::Mdp); mdp = model->as>(); @@ -283,10 +261,9 @@ TEST(DdJaniModelBuilderTest_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"); - janiModel = program.toJani(true); - builder = storm::builder::DdJaniModelBuilder(janiModel); - model = builder.build(); + modelDescription = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/csma2-2.nm"); + janiModel = modelDescription.toJani(true).preprocess().asJaniModel(); + model = builder.build(janiModel); EXPECT_TRUE(model->getType() == storm::models::ModelType::Mdp); mdp = model->as>(); @@ -295,10 +272,9 @@ TEST(DdJaniModelBuilderTest_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"); - janiModel = program.toJani(true); - builder = storm::builder::DdJaniModelBuilder(janiModel); - model = builder.build(); + modelDescription = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/firewire3-0.5.nm"); + janiModel = modelDescription.toJani(true).preprocess().asJaniModel(); + model = builder.build(janiModel); EXPECT_TRUE(model->getType() == storm::models::ModelType::Mdp); mdp = model->as>(); @@ -307,10 +283,9 @@ TEST(DdJaniModelBuilderTest_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"); - janiModel = program.toJani(true); - builder = storm::builder::DdJaniModelBuilder(janiModel); - model = builder.build(); + modelDescription = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/wlan0-2-2.nm"); + janiModel = modelDescription.toJani(true).preprocess().asJaniModel(); + model = builder.build(janiModel); EXPECT_TRUE(model->getType() == storm::models::ModelType::Mdp); mdp = model->as>(); @@ -321,8 +296,8 @@ TEST(DdJaniModelBuilderTest_Cudd, Mdp) { } TEST(DdJaniModelBuilderTest_Cudd, IllegalSynchronizingWrites) { - storm::prism::Program program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/coin2-2-illegalSynchronizingWrite.nm"); - storm::jani::Model janiModel = program.toJani(true); - storm::builder::DdJaniModelBuilder builder(janiModel); - EXPECT_THROW(std::shared_ptr> model = builder.build(), storm::exceptions::WrongFormatException); + storm::storage::SymbolicModelDescription modelDescription = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/coin2-2-illegalSynchronizingWrite.nm"); + storm::jani::Model janiModel = modelDescription.toJani(true).preprocess().asJaniModel(); + storm::builder::DdJaniModelBuilder builder; + EXPECT_THROW(std::shared_ptr> model = builder.build(janiModel), storm::exceptions::WrongFormatException); } \ No newline at end of file diff --git a/test/functional/modelchecker/SparseDtmcRegionModelCheckerTest.cpp b/test/functional/modelchecker/SparseDtmcRegionModelCheckerTest.cpp index f14808886..aed634c75 100644 --- a/test/functional/modelchecker/SparseDtmcRegionModelCheckerTest.cpp +++ b/test/functional/modelchecker/SparseDtmcRegionModelCheckerTest.cpp @@ -24,7 +24,7 @@ TEST(SparseDtmcRegionModelCheckerTest, Brp_Prob) { // Program and formula storm::prism::Program program = storm::parseProgram(programFile); program = storm::utility::prism::preprocess(program, constantsAsString); - std::vector> formulas = storm::parseFormulasForProgram(formulaAsString, program);; + std::vector> formulas = storm::parseFormulasForPrismProgram(formulaAsString, program);; std::shared_ptr> model = storm::buildSparseModel(program, formulas)->as>(); auto const& regionSettings = storm::settings::getModule(); storm::modelchecker::region::SparseRegionModelCheckerSettings settings(regionSettings.getSampleMode(), regionSettings.getApproxMode(), regionSettings.getSmtMode()); @@ -95,7 +95,7 @@ TEST(SparseDtmcRegionModelCheckerTest, Brp_Rew) { storm::prism::Program program = storm::parseProgram(programFile); program = storm::utility::prism::preprocess(program, constantsAsString); - std::vector> formulas = storm::parseFormulasForProgram(formulaAsString, program);; + std::vector> formulas = storm::parseFormulasForPrismProgram(formulaAsString, program);; std::shared_ptr> model = storm::buildSparseModel(program, formulas)->as>(); auto const& regionSettings = storm::settings::getModule(); storm::modelchecker::region::SparseRegionModelCheckerSettings settings(regionSettings.getSampleMode(), regionSettings.getApproxMode(), regionSettings.getSmtMode()); @@ -189,7 +189,7 @@ TEST(SparseDtmcRegionModelCheckerTest, Brp_Rew_Infty) { carl::VariablePool::getInstance().clear(); storm::prism::Program program = storm::parseProgram(programFile); program = storm::utility::prism::preprocess(program, constantsAsString); - std::vector> formulas = storm::parseFormulasForProgram(formulaAsString, program);; + std::vector> formulas = storm::parseFormulasForPrismProgram(formulaAsString, program);; std::shared_ptr> model = storm::buildSparseModel(program, formulas)->as>(); auto const& regionSettings = storm::settings::getModule(); storm::modelchecker::region::SparseRegionModelCheckerSettings settings(regionSettings.getSampleMode(), regionSettings.getApproxMode(), regionSettings.getSmtMode()); @@ -233,7 +233,7 @@ TEST(SparseDtmcRegionModelCheckerTest, Brp_Rew_4Par) { carl::VariablePool::getInstance().clear(); storm::prism::Program program = storm::parseProgram(programFile); program = storm::utility::prism::preprocess(program, constantsAsString); - std::vector> formulas = storm::parseFormulasForProgram(formulaAsString, program);; + std::vector> formulas = storm::parseFormulasForPrismProgram(formulaAsString, program);; std::shared_ptr> model = storm::buildSparseModel(program, formulas)->as>(); auto const& regionSettings = storm::settings::getModule(); storm::modelchecker::region::SparseRegionModelCheckerSettings settings(regionSettings.getSampleMode(), regionSettings.getApproxMode(), regionSettings.getSmtMode()); @@ -297,7 +297,7 @@ TEST(SparseDtmcRegionModelCheckerTest, Crowds_Prob) { storm::prism::Program program = storm::parseProgram(programFile); program = storm::utility::prism::preprocess(program, constantsAsString); - std::vector> formulas = storm::parseFormulasForProgram(formulaAsString, program);; + std::vector> formulas = storm::parseFormulasForPrismProgram(formulaAsString, program);; std::shared_ptr> model = storm::buildSparseModel(program, formulas)->as>(); auto const& regionSettings = storm::settings::getModule(); storm::modelchecker::region::SparseRegionModelCheckerSettings settings(regionSettings.getSampleMode(), regionSettings.getApproxMode(), regionSettings.getSmtMode()); @@ -389,7 +389,7 @@ TEST(SparseDtmcRegionModelCheckerTest, Crowds_Prob_1Par) { storm::prism::Program program = storm::parseProgram(programFile); program = storm::utility::prism::preprocess(program, constantsAsString); - std::vector> formulas = storm::parseFormulasForProgram(formulaAsString, program);; + std::vector> formulas = storm::parseFormulasForPrismProgram(formulaAsString, program);; std::shared_ptr> model = storm::buildSparseModel(program, formulas)->as>(); auto const& regionSettings = storm::settings::getModule(); storm::modelchecker::region::SparseRegionModelCheckerSettings settings(regionSettings.getSampleMode(), regionSettings.getApproxMode(), regionSettings.getSmtMode()); @@ -455,7 +455,7 @@ TEST(SparseDtmcRegionModelCheckerTest, Crowds_Prob_Const) { storm::prism::Program program = storm::parseProgram(programFile); program = storm::utility::prism::preprocess(program, constantsAsString); - std::vector> formulas = storm::parseFormulasForProgram(formulaAsString, program);; + std::vector> formulas = storm::parseFormulasForPrismProgram(formulaAsString, program);; std::shared_ptr> model = storm::buildSparseModel(program, formulas)->as>(); auto const& regionSettings = storm::settings::getModule(); storm::modelchecker::region::SparseRegionModelCheckerSettings settings(regionSettings.getSampleMode(), regionSettings.getApproxMode(), regionSettings.getSmtMode()); diff --git a/test/functional/modelchecker/SparseMdpRegionModelCheckerTest.cpp b/test/functional/modelchecker/SparseMdpRegionModelCheckerTest.cpp index 1ceb6c4e6..2b2aa9d2c 100644 --- a/test/functional/modelchecker/SparseMdpRegionModelCheckerTest.cpp +++ b/test/functional/modelchecker/SparseMdpRegionModelCheckerTest.cpp @@ -23,7 +23,7 @@ TEST(SparseMdpRegionModelCheckerTest, two_dice_Prob) { carl::VariablePool::getInstance().clear(); storm::prism::Program program = storm::parseProgram(programFile); - std::vector> formulas = storm::parseFormulasForProgram(formulaFile, program); + std::vector> formulas = storm::parseFormulasForPrismProgram(formulaFile, program); std::shared_ptr> model = storm::buildSparseModel(program, formulas)->as>(); auto const& regionSettings = storm::settings::getModule(); storm::modelchecker::region::SparseRegionModelCheckerSettings settings(regionSettings.getSampleMode(), regionSettings.getApproxMode(), regionSettings.getSmtMode()); @@ -91,7 +91,7 @@ TEST(SparseMdpRegionModelCheckerTest, coin_Prob) { carl::VariablePool::getInstance().clear(); storm::prism::Program program = storm::parseProgram(programFile); - std::vector> formulas = storm::parseFormulasForProgram(formulaAsString, program); + std::vector> formulas = storm::parseFormulasForPrismProgram(formulaAsString, program); std::shared_ptr> model = storm::buildSparseModel(program, formulas)->as>(); auto const& regionSettings = storm::settings::getModule(); storm::modelchecker::region::SparseRegionModelCheckerSettings settings(regionSettings.getSampleMode(), regionSettings.getApproxMode(), regionSettings.getSmtMode()); diff --git a/test/functional/utility/ModelInstantiatorTest.cpp b/test/functional/utility/ModelInstantiatorTest.cpp index 2dd74c66a..d1319613c 100644 --- a/test/functional/utility/ModelInstantiatorTest.cpp +++ b/test/functional/utility/ModelInstantiatorTest.cpp @@ -26,7 +26,7 @@ TEST(ModelInstantiatorTest, BrpProb) { // Program and formula storm::prism::Program program = storm::parseProgram(programFile); program.checkValidity(); - std::vector> formulas = storm::parseFormulasForProgram(formulaAsString, program); + std::vector> formulas = storm::parseFormulasForPrismProgram(formulaAsString, program); ASSERT_TRUE(formulas.size()==1); // Parametric model storm::generator::NextStateGeneratorOptions options(*formulas.front()); @@ -144,7 +144,7 @@ TEST(ModelInstantiatorTest, Brp_Rew) { // Program and formula storm::prism::Program program = storm::parseProgram(programFile); program.checkValidity(); - std::vector> formulas = storm::parseFormulasForProgram(formulaAsString, program); + std::vector> formulas = storm::parseFormulasForPrismProgram(formulaAsString, program); ASSERT_TRUE(formulas.size()==1); // Parametric model storm::generator::NextStateGeneratorOptions options(*formulas.front()); @@ -214,7 +214,7 @@ TEST(ModelInstantiatorTest, Consensus) { // Program and formula storm::prism::Program program = storm::parseProgram(programFile); program.checkValidity(); - std::vector> formulas = storm::parseFormulasForProgram(formulaAsString, program); + std::vector> formulas = storm::parseFormulasForPrismProgram(formulaAsString, program); ASSERT_TRUE(formulas.size()==1); // Parametric model storm::generator::NextStateGeneratorOptions options(*formulas.front());