From e7a8357ee69aa67c5a38def811bd3556c9e3137e Mon Sep 17 00:00:00 2001 From: TimQu Date: Fri, 26 May 2017 11:31:32 +0200 Subject: [PATCH] Fixed some tests --- src/storm/models/sparse/Ctmc.cpp | 8 +++- src/storm/models/sparse/Model.cpp | 9 +++-- .../parser/NondeterministicModelParser.cpp | 4 +- .../SparseModelMemoryProduct.cpp | 4 +- src/storm/storage/sparse/ModelComponents.h | 3 -- src/storm/utility/ModelInstantiator.cpp | 9 +++-- .../ExplicitJitJaniModelBuilderTest.cpp | 40 +++++++++---------- .../SparseDtmcParameterLiftingTest.cpp | 24 +++++------ ...seMaPcaaMultiObjectiveModelCheckerTest.cpp | 10 ++--- .../SparseMdpParameterLiftingTest.cpp | 20 +++++----- ...eMdpPcaaMultiObjectiveModelCheckerTest.cpp | 10 ++--- 11 files changed, 75 insertions(+), 66 deletions(-) diff --git a/src/storm/models/sparse/Ctmc.cpp b/src/storm/models/sparse/Ctmc.cpp index d52bc742e..d5e33e5d1 100644 --- a/src/storm/models/sparse/Ctmc.cpp +++ b/src/storm/models/sparse/Ctmc.cpp @@ -27,6 +27,9 @@ namespace storm { if (components.exitRates) { exitRates = components.exitRates.get(); + } else { + STORM_LOG_ASSERT(components.rateTransitions, "No rate information given for CTMC."); + exitRates = createExitRateVector(this->getTransitionMatrix()); } if (!components.rateTransitions) { @@ -40,8 +43,11 @@ namespace storm { if (components.exitRates) { exitRates = std::move(components.exitRates.get()); + } else { + STORM_LOG_ASSERT(components.rateTransitions, "No rate information given for CTMC."); + exitRates = createExitRateVector(this->getTransitionMatrix()); } - + if (!components.rateTransitions) { this->getTransitionMatrix().scaleRowsInPlace(exitRates); } diff --git a/src/storm/models/sparse/Model.cpp b/src/storm/models/sparse/Model.cpp index dde504e97..8e62b4b85 100644 --- a/src/storm/models/sparse/Model.cpp +++ b/src/storm/models/sparse/Model.cpp @@ -31,17 +31,20 @@ namespace storm { template void Model::assertValidityOfComponents(storm::storage::sparse::ModelComponents const& components) const { + + // More costly checks are only asserted to avoid doing them in release mode. + uint_fast64_t stateCount = this->getNumberOfStates(); uint_fast64_t choiceCount = this->getTransitionMatrix().getRowCount(); // general components for all model types. STORM_LOG_THROW(this->getTransitionMatrix().getColumnCount() == stateCount, storm::exceptions::IllegalArgumentException, "Invalid column count of transition matrix."); - STORM_LOG_THROW(components.rateTransitions || this->getTransitionMatrix().isProbabilistic(), storm::exceptions::IllegalArgumentException, "The matrix is not probabilistic."); + STORM_LOG_ASSERT(components.rateTransitions || this->hasParameters() || this->getTransitionMatrix().isProbabilistic(), "The matrix is not probabilistic."); STORM_LOG_THROW(this->getStateLabeling().getNumberOfItems() == stateCount, storm::exceptions::IllegalArgumentException, "Invalid item count of state labeling."); for (auto const& rewardModel : this->getRewardModels()) { STORM_LOG_THROW(!rewardModel.second.hasStateRewards() || rewardModel.second.getStateRewardVector().size() == stateCount, storm::exceptions::IllegalArgumentException, "Invalid size of state reward vector."); STORM_LOG_THROW(!rewardModel.second.hasStateActionRewards() || rewardModel.second.getStateActionRewardVector().size() == choiceCount, storm::exceptions::IllegalArgumentException, "Invalid size of state reward vector."); - STORM_LOG_THROW(!rewardModel.second.hasTransitionRewards() || rewardModel.second.getTransitionRewardMatrix().isSubmatrixOf(this->getTransitionMatrix()), storm::exceptions::IllegalArgumentException, "The transition reward matrix is not a submatrix of the transition matrix, i.e. there are rewards for transitions that do not exist."); + STORM_LOG_ASSERT(!rewardModel.second.hasTransitionRewards() || rewardModel.second.getTransitionRewardMatrix().isSubmatrixOf(this->getTransitionMatrix()), "The transition reward matrix is not a submatrix of the transition matrix, i.e. there are rewards for transitions that do not exist."); } STORM_LOG_THROW(!this->hasChoiceLabeling() || this->getChoiceLabeling().getNumberOfItems() == choiceCount, storm::exceptions::IllegalArgumentException, "Invalid item count of choice labeling."); STORM_LOG_THROW(!this->hasStateValuations() || this->getStateValuations().getNumberOfStates() == stateCount, storm::exceptions::IllegalArgumentException, "Invalid choice count for choice origins."); @@ -60,7 +63,7 @@ namespace storm { } else { STORM_LOG_THROW(this->isOfType(ModelType::S2pg), storm::exceptions::IllegalArgumentException, "Invalid model type."); STORM_LOG_THROW(components.player1Matrix.is_initialized(), storm::exceptions::IllegalArgumentException, "No player 1 matrix given for stochastic game."); - STORM_LOG_THROW(components.player1Matrix->isProbabilistic(), storm::exceptions::IllegalArgumentException, "Can not create stochastic game: There is a row in the p1 matrix with not exactly one entry."); + STORM_LOG_ASSERT(components.player1Matrix->isProbabilistic(), "Can not create stochastic game: There is a row in the p1 matrix with not exactly one entry."); STORM_LOG_THROW(stateCount == components.player1Matrix->getRowGroupCount(), storm::exceptions::IllegalArgumentException, "Can not create stochastic game: Number of row groups of p1 matrix does not match state count."); STORM_LOG_THROW(this->getTransitionMatrix().getRowGroupCount() == components.player1Matrix->getColumnCount(), storm::exceptions::IllegalArgumentException, "Can not create stochastic game: Number of row groups of p2 matrix does not match column count of p1 matrix."); } diff --git a/src/storm/parser/NondeterministicModelParser.cpp b/src/storm/parser/NondeterministicModelParser.cpp index b786a0d73..a02b8d622 100644 --- a/src/storm/parser/NondeterministicModelParser.cpp +++ b/src/storm/parser/NondeterministicModelParser.cpp @@ -38,7 +38,7 @@ namespace storm { // Only parse transition rewards if a file is given. boost::optional> transitionRewards; if (!transitionRewardFilename.empty()) { - transitionRewards = std::move(storm::parser::NondeterministicSparseTransitionParser::parseNondeterministicTransitionRewards(transitionRewardFilename, transitions)); + transitionRewards = std::move(storm::parser::NondeterministicSparseTransitionParser::parseNondeterministicTransitionRewards(transitionRewardFilename, result.transitionMatrix)); } if (stateRewards || transitionRewards) { @@ -48,7 +48,7 @@ namespace storm { // Only parse choice labeling if a file is given. boost::optional choiceLabeling; if (!choiceLabelingFilename.empty()) { - result.choiceLabeling = storm::parser::SparseItemLabelingParser::parseChoiceLabeling(transitions.getRowCount(), choiceLabelingFilename, transitions.getRowGroupIndices()); + result.choiceLabeling = storm::parser::SparseItemLabelingParser::parseChoiceLabeling(result.transitionMatrix.getRowCount(), choiceLabelingFilename, result.transitionMatrix.getRowGroupIndices()); } return result; diff --git a/src/storm/storage/memorystructure/SparseModelMemoryProduct.cpp b/src/storm/storage/memorystructure/SparseModelMemoryProduct.cpp index 330091f9d..bc4e49782 100644 --- a/src/storm/storage/memorystructure/SparseModelMemoryProduct.cpp +++ b/src/storm/storage/memorystructure/SparseModelMemoryProduct.cpp @@ -291,10 +291,10 @@ namespace storm { components.rateTransitions = true; } else if (model.isOfType(storm::models::ModelType::MarkovAutomaton)) { // We also need to translate the exit rates and the Markovian states - uint_fast64_t numResStates = matrix.getRowGroupCount(); + uint_fast64_t numResStates = components.transitionMatrix.getRowGroupCount(); uint_fast64_t memoryStateCount = memory.getNumberOfStates(); std::vector resultExitRates; - resultExitRates.reserve(matrix.getRowGroupCount()); + resultExitRates.reserve(components.transitionMatrix.getRowGroupCount()); storm::storage::BitVector resultMarkovianStates(numResStates, false); auto const& modelExitRates = dynamic_cast const&>(model).getExitRates(); auto const& modelMarkovianStates = dynamic_cast const&>(model).getMarkovianStates(); diff --git a/src/storm/storage/sparse/ModelComponents.h b/src/storm/storage/sparse/ModelComponents.h index cf106b98a..b3e7e4f92 100644 --- a/src/storm/storage/sparse/ModelComponents.h +++ b/src/storm/storage/sparse/ModelComponents.h @@ -33,9 +33,6 @@ namespace storm { boost::optional> const& player1Matrix = boost::none) : transitionMatrix(transitionMatrix), stateLabeling(stateLabeling), rewardModels(rewardModels), rateTransitions(rateTransitions), markovianStates(markovianStates), player1Matrix(player1Matrix) { // Intentionally left empty - - // TODO: remove this output - std::cout << "Called copy constructor for model components (which should be avoided)" << std::endl; } ModelComponents(storm::storage::SparseMatrix&& transitionMatrix = storm::storage::SparseMatrix(), diff --git a/src/storm/utility/ModelInstantiator.cpp b/src/storm/utility/ModelInstantiator.cpp index 5403d6228..e28049862 100644 --- a/src/storm/utility/ModelInstantiator.cpp +++ b/src/storm/utility/ModelInstantiator.cpp @@ -36,10 +36,11 @@ namespace storm { true, !parametricMatrix.hasTrivialRowGrouping(), parametricMatrix.hasTrivialRowGrouping() ? 0 : parametricMatrix.getRowGroupCount()); - ConstantType dummyValue = storm::utility::one(); if (parametricMatrix.hasTrivialRowGrouping()) { for (uint_fast64_t row = 0; row < parametricMatrix.getRowCount(); ++row) { - for (auto const& paramEntry : parametricMatrix.getRow(row)) { + auto parametricRow = parametricMatrix.getRow(row); + ConstantType dummyValue = storm::utility::one() / storm::utility::convertNumber(parametricRow.getNumberOfEntries()); + for (auto const& paramEntry : parametricRow) { matrixBuilder.addNextValue(row, paramEntry.getColumn(), dummyValue); } } @@ -48,7 +49,9 @@ namespace storm { for(uint_fast64_t rowGroup = 0; rowGroup < parametricMatrix.getRowGroupCount(); ++rowGroup){ matrixBuilder.newRowGroup(parametricMatrix.getRowGroupIndices()[rowGroup]); for (uint_fast64_t row = parametricMatrix.getRowGroupIndices()[rowGroup]; row < parametricMatrix.getRowGroupIndices()[rowGroup+1]; ++row) { - for(auto const& paramEntry : parametricMatrix.getRow(row)){ + auto parametricRow = parametricMatrix.getRow(row); + ConstantType dummyValue = storm::utility::one() / storm::utility::convertNumber(parametricRow.getNumberOfEntries()); + for(auto const& paramEntry : parametricRow){ matrixBuilder.addNextValue(row, paramEntry.getColumn(), dummyValue); } } diff --git a/src/test/builder/ExplicitJitJaniModelBuilderTest.cpp b/src/test/builder/ExplicitJitJaniModelBuilderTest.cpp index b4b87e958..efb10e00f 100644 --- a/src/test/builder/ExplicitJitJaniModelBuilderTest.cpp +++ b/src/test/builder/ExplicitJitJaniModelBuilderTest.cpp @@ -14,31 +14,31 @@ TEST(ExplicitJitJaniModelBuilderTest, Dtmc) { storm::prism::Program program = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/dtmc/die.pm"); storm::jani::Model janiModel = program.toJani(); - std::shared_ptr> model = storm::builder::jit::ExplicitJitJaniModelBuilder(janiModel).build().getModel();; + std::shared_ptr> model = storm::builder::jit::ExplicitJitJaniModelBuilder(janiModel).build();; EXPECT_EQ(13ul, model->getNumberOfStates()); EXPECT_EQ(20ul, model->getNumberOfTransitions()); program = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/dtmc/brp-16-2.pm"); janiModel = program.toJani(); - model = storm::builder::jit::ExplicitJitJaniModelBuilder(janiModel).build().getModel();; + model = storm::builder::jit::ExplicitJitJaniModelBuilder(janiModel).build();; EXPECT_EQ(677ul, model->getNumberOfStates()); EXPECT_EQ(867ul, model->getNumberOfTransitions()); program = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/dtmc/crowds-5-5.pm"); janiModel = program.toJani(); - model = storm::builder::jit::ExplicitJitJaniModelBuilder(janiModel).build().getModel();; + model = storm::builder::jit::ExplicitJitJaniModelBuilder(janiModel).build();; EXPECT_EQ(8607ul, model->getNumberOfStates()); EXPECT_EQ(15113ul, model->getNumberOfTransitions()); program = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/dtmc/leader-3-5.pm"); janiModel = program.toJani(); - model = storm::builder::jit::ExplicitJitJaniModelBuilder(janiModel).build().getModel();; + model = storm::builder::jit::ExplicitJitJaniModelBuilder(janiModel).build();; EXPECT_EQ(273ul, model->getNumberOfStates()); EXPECT_EQ(397ul, model->getNumberOfTransitions()); program = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/dtmc/nand-5-2.pm"); janiModel = program.toJani(); - model = storm::builder::jit::ExplicitJitJaniModelBuilder(janiModel).build().getModel();; + model = storm::builder::jit::ExplicitJitJaniModelBuilder(janiModel).build();; EXPECT_EQ(1728ul, model->getNumberOfStates()); EXPECT_EQ(2505ul, model->getNumberOfTransitions()); } @@ -50,31 +50,31 @@ TEST(ExplicitJitJaniModelBuilderTest, Ctmc) { storm::prism::Program program = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/ctmc/cluster2.sm"); storm::jani::Model janiModel = program.toJani(); - std::shared_ptr> model = storm::builder::jit::ExplicitJitJaniModelBuilder(janiModel).build().getModel();; + std::shared_ptr> model = storm::builder::jit::ExplicitJitJaniModelBuilder(janiModel).build();; EXPECT_EQ(276ul, model->getNumberOfStates()); EXPECT_EQ(1120ul, model->getNumberOfTransitions()); program = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/ctmc/embedded2.sm"); janiModel = program.toJani(); - model = storm::builder::jit::ExplicitJitJaniModelBuilder(janiModel).build().getModel();; + model = storm::builder::jit::ExplicitJitJaniModelBuilder(janiModel).build();; EXPECT_EQ(3478ul, model->getNumberOfStates()); EXPECT_EQ(14639ul, model->getNumberOfTransitions()); program = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/ctmc/polling2.sm"); janiModel = program.toJani(); - model = storm::builder::jit::ExplicitJitJaniModelBuilder(janiModel).build().getModel();; + model = storm::builder::jit::ExplicitJitJaniModelBuilder(janiModel).build();; EXPECT_EQ(12ul, model->getNumberOfStates()); EXPECT_EQ(22ul, model->getNumberOfTransitions()); program = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/ctmc/fms2.sm"); janiModel = program.toJani(); - model = storm::builder::jit::ExplicitJitJaniModelBuilder(janiModel).build().getModel();; + model = storm::builder::jit::ExplicitJitJaniModelBuilder(janiModel).build();; EXPECT_EQ(810ul, model->getNumberOfStates()); EXPECT_EQ(3699ul, model->getNumberOfTransitions()); program = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/ctmc/tandem5.sm"); janiModel = program.toJani(); - model = storm::builder::jit::ExplicitJitJaniModelBuilder(janiModel).build().getModel();; + model = storm::builder::jit::ExplicitJitJaniModelBuilder(janiModel).build();; EXPECT_EQ(66ul, model->getNumberOfStates()); EXPECT_EQ(189ul, model->getNumberOfTransitions()); } @@ -83,37 +83,37 @@ TEST(ExplicitJitJaniModelBuilderTest, Mdp) { storm::prism::Program program = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/mdp/two_dice.nm"); storm::jani::Model janiModel = program.toJani(); - std::shared_ptr> model = storm::builder::jit::ExplicitJitJaniModelBuilder(janiModel).build().getModel();; + std::shared_ptr> model = storm::builder::jit::ExplicitJitJaniModelBuilder(janiModel).build();; EXPECT_EQ(169ul, model->getNumberOfStates()); EXPECT_EQ(436ul, model->getNumberOfTransitions()); program = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/mdp/leader3.nm"); janiModel = program.toJani(); - model = storm::builder::jit::ExplicitJitJaniModelBuilder(janiModel).build().getModel();; + model = storm::builder::jit::ExplicitJitJaniModelBuilder(janiModel).build();; EXPECT_EQ(364ul, model->getNumberOfStates()); EXPECT_EQ(654ul, model->getNumberOfTransitions()); program = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/mdp/coin2-2.nm"); janiModel = program.toJani(); - model = storm::builder::jit::ExplicitJitJaniModelBuilder(janiModel).build().getModel();; + model = storm::builder::jit::ExplicitJitJaniModelBuilder(janiModel).build();; EXPECT_EQ(272ul, model->getNumberOfStates()); EXPECT_EQ(492ul, model->getNumberOfTransitions()); program = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/mdp/csma2-2.nm"); janiModel = program.toJani(); - model = storm::builder::jit::ExplicitJitJaniModelBuilder(janiModel).build().getModel();; + model = storm::builder::jit::ExplicitJitJaniModelBuilder(janiModel).build();; EXPECT_EQ(1038ul, model->getNumberOfStates()); EXPECT_EQ(1282ul, model->getNumberOfTransitions()); program = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/mdp/firewire3-0.5.nm"); janiModel = program.toJani(); - model = storm::builder::jit::ExplicitJitJaniModelBuilder(janiModel).build().getModel();; + model = storm::builder::jit::ExplicitJitJaniModelBuilder(janiModel).build();; EXPECT_EQ(4093ul, model->getNumberOfStates()); EXPECT_EQ(5585ul, model->getNumberOfTransitions()); program = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/mdp/wlan0-2-2.nm"); janiModel = program.toJani(); - model = storm::builder::jit::ExplicitJitJaniModelBuilder(janiModel).build().getModel();; + model = storm::builder::jit::ExplicitJitJaniModelBuilder(janiModel).build();; EXPECT_EQ(37ul, model->getNumberOfStates()); EXPECT_EQ(59ul, model->getNumberOfTransitions()); } @@ -122,7 +122,7 @@ TEST(ExplicitJitJaniModelBuilderTest, Ma) { storm::prism::Program program = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/ma/simple.ma"); storm::jani::Model janiModel = program.toJani(); - std::shared_ptr> model = storm::builder::jit::ExplicitJitJaniModelBuilder(janiModel).build().getModel();; + std::shared_ptr> model = storm::builder::jit::ExplicitJitJaniModelBuilder(janiModel).build();; EXPECT_EQ(5ul, model->getNumberOfStates()); EXPECT_EQ(8ul, model->getNumberOfTransitions()); ASSERT_TRUE(model->isOfType(storm::models::ModelType::MarkovAutomaton)); @@ -130,7 +130,7 @@ TEST(ExplicitJitJaniModelBuilderTest, Ma) { program = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/ma/hybrid_states.ma"); janiModel = program.toJani(); - model = storm::builder::jit::ExplicitJitJaniModelBuilder(janiModel).build().getModel();; + model = storm::builder::jit::ExplicitJitJaniModelBuilder(janiModel).build();; EXPECT_EQ(5ul, model->getNumberOfStates()); EXPECT_EQ(13ul, model->getNumberOfTransitions()); ASSERT_TRUE(model->isOfType(storm::models::ModelType::MarkovAutomaton)); @@ -138,7 +138,7 @@ TEST(ExplicitJitJaniModelBuilderTest, Ma) { program = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/ma/stream2.ma"); janiModel = program.toJani(); - model = storm::builder::jit::ExplicitJitJaniModelBuilder(janiModel).build().getModel();; + model = storm::builder::jit::ExplicitJitJaniModelBuilder(janiModel).build();; EXPECT_EQ(12ul, model->getNumberOfStates()); EXPECT_EQ(14ul, model->getNumberOfTransitions()); ASSERT_TRUE(model->isOfType(storm::models::ModelType::MarkovAutomaton)); @@ -149,7 +149,7 @@ TEST(ExplicitJitJaniModelBuilderTest, FailComposition) { storm::prism::Program program = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/mdp/system_composition.nm"); storm::jani::Model janiModel = program.toJani(); - ASSERT_THROW(storm::builder::jit::ExplicitJitJaniModelBuilder(janiModel).build().getModel();, storm::exceptions::WrongFormatException); + ASSERT_THROW(storm::builder::jit::ExplicitJitJaniModelBuilder(janiModel).build();, storm::exceptions::WrongFormatException); } TEST(ExplicitJitJaniModelBuilderTest, IllegalSynchronizingWrites) { diff --git a/src/test/modelchecker/SparseDtmcParameterLiftingTest.cpp b/src/test/modelchecker/SparseDtmcParameterLiftingTest.cpp index c6a13347c..0314c3e56 100644 --- a/src/test/modelchecker/SparseDtmcParameterLiftingTest.cpp +++ b/src/test/modelchecker/SparseDtmcParameterLiftingTest.cpp @@ -17,7 +17,7 @@ TEST(SparseDtmcParameterLiftingTest, Brp_Prob) { storm::prism::Program program = storm::parseProgram(programFile); program = storm::utility::prism::preprocess(program, constantsAsString); std::vector> formulas = storm::extractFormulasFromProperties(storm::parsePropertiesForPrismProgram(formulaAsString, program)); - std::shared_ptr> model = storm::buildSparseModel(program, formulas).getModel()->as>(); + std::shared_ptr> model = storm::buildSparseModel(program, formulas)->as>(); auto modelParameters = storm::models::sparse::getProbabilityParameters(*model); auto rewParameters = storm::models::sparse::getRewardParameters(*model); @@ -47,7 +47,7 @@ TEST(SparseDtmcParameterLiftingTest, Brp_Rew) { storm::prism::Program program = storm::parseProgram(programFile); program = storm::utility::prism::preprocess(program, constantsAsString); std::vector> formulas = storm::extractFormulasFromProperties(storm::parsePropertiesForPrismProgram(formulaAsString, program)); - std::shared_ptr> model = storm::buildSparseModel(program, formulas).getModel()->as>(); + std::shared_ptr> model = storm::buildSparseModel(program, formulas)->as>(); auto modelParameters = storm::models::sparse::getProbabilityParameters(*model); auto rewParameters = storm::models::sparse::getRewardParameters(*model); @@ -77,7 +77,7 @@ TEST(SparseDtmcParameterLiftingTest, Brp_Rew_Bounded) { storm::prism::Program program = storm::parseProgram(programFile); program = storm::utility::prism::preprocess(program, constantsAsString); std::vector> formulas = storm::extractFormulasFromProperties(storm::parsePropertiesForPrismProgram(formulaAsString, program)); - std::shared_ptr> model = storm::buildSparseModel(program, formulas).getModel()->as>(); + std::shared_ptr> model = storm::buildSparseModel(program, formulas)->as>(); auto modelParameters = storm::models::sparse::getProbabilityParameters(*model); auto rewParameters = storm::models::sparse::getRewardParameters(*model); @@ -108,7 +108,7 @@ TEST(SparseDtmcParameterLiftingTest, Brp_Prob_exactValidation) { storm::prism::Program program = storm::parseProgram(programFile); program = storm::utility::prism::preprocess(program, constantsAsString); std::vector> formulas = storm::extractFormulasFromProperties(storm::parsePropertiesForPrismProgram(formulaAsString, program)); - std::shared_ptr> model = storm::buildSparseModel(program, formulas).getModel()->as>(); + std::shared_ptr> model = storm::buildSparseModel(program, formulas)->as>(); auto modelParameters = storm::models::sparse::getProbabilityParameters(*model); auto rewParameters = storm::models::sparse::getRewardParameters(*model); @@ -141,7 +141,7 @@ TEST(SparseDtmcParameterLiftingTest, Brp_Rew_exactValidation) { storm::prism::Program program = storm::parseProgram(programFile); program = storm::utility::prism::preprocess(program, constantsAsString); std::vector> formulas = storm::extractFormulasFromProperties(storm::parsePropertiesForPrismProgram(formulaAsString, program)); - std::shared_ptr> model = storm::buildSparseModel(program, formulas).getModel()->as>(); + std::shared_ptr> model = storm::buildSparseModel(program, formulas)->as>(); auto modelParameters = storm::models::sparse::getProbabilityParameters(*model); auto rewParameters = storm::models::sparse::getRewardParameters(*model); @@ -174,7 +174,7 @@ TEST(SparseDtmcParameterLiftingTest, Brp_Rew_Bounded_exactValidation) { storm::prism::Program program = storm::parseProgram(programFile); program = storm::utility::prism::preprocess(program, constantsAsString); std::vector> formulas = storm::extractFormulasFromProperties(storm::parsePropertiesForPrismProgram(formulaAsString, program)); - std::shared_ptr> model = storm::buildSparseModel(program, formulas).getModel()->as>(); + std::shared_ptr> model = storm::buildSparseModel(program, formulas)->as>(); auto modelParameters = storm::models::sparse::getProbabilityParameters(*model); auto rewParameters = storm::models::sparse::getRewardParameters(*model); @@ -207,7 +207,7 @@ TEST(SparseDtmcParameterLiftingTest, Brp_Rew_Infty) { storm::prism::Program program = storm::parseProgram(programFile); program = storm::utility::prism::preprocess(program, constantsAsString); std::vector> formulas = storm::extractFormulasFromProperties(storm::parsePropertiesForPrismProgram(formulaAsString, program)); - std::shared_ptr> model = storm::buildSparseModel(program, formulas).getModel()->as>(); + std::shared_ptr> model = storm::buildSparseModel(program, formulas)->as>(); auto modelParameters = storm::models::sparse::getProbabilityParameters(*model); auto rewParameters = storm::models::sparse::getRewardParameters(*model); @@ -233,7 +233,7 @@ TEST(SparseDtmcParameterLiftingTest, Brp_Rew_4Par) { storm::prism::Program program = storm::parseProgram(programFile); program = storm::utility::prism::preprocess(program, constantsAsString); std::vector> formulas = storm::extractFormulasFromProperties(storm::parsePropertiesForPrismProgram(formulaAsString, program)); - std::shared_ptr> model = storm::buildSparseModel(program, formulas).getModel()->as>(); + std::shared_ptr> model = storm::buildSparseModel(program, formulas)->as>(); auto modelParameters = storm::models::sparse::getProbabilityParameters(*model); auto rewParameters = storm::models::sparse::getRewardParameters(*model); @@ -264,7 +264,7 @@ TEST(SparseDtmcParameterLiftingTest, Crowds_Prob) { storm::prism::Program program = storm::parseProgram(programFile); program = storm::utility::prism::preprocess(program, constantsAsString); std::vector> formulas = storm::extractFormulasFromProperties(storm::parsePropertiesForPrismProgram(formulaAsString, program)); - std::shared_ptr> model = storm::buildSparseModel(program, formulas).getModel()->as>(); + std::shared_ptr> model = storm::buildSparseModel(program, formulas)->as>(); auto modelParameters = storm::models::sparse::getProbabilityParameters(*model); auto rewParameters = storm::models::sparse::getRewardParameters(*model); @@ -297,7 +297,7 @@ TEST(SparseDtmcParameterLiftingTest, Crowds_Prob_stepBounded) { storm::prism::Program program = storm::parseProgram(programFile); program = storm::utility::prism::preprocess(program, constantsAsString); std::vector> formulas = storm::extractFormulasFromProperties(storm::parsePropertiesForPrismProgram(formulaAsString, program)); - std::shared_ptr> model = storm::buildSparseModel(program, formulas).getModel()->as>(); + std::shared_ptr> model = storm::buildSparseModel(program, formulas)->as>(); auto modelParameters = storm::models::sparse::getProbabilityParameters(*model); auto rewParameters = storm::models::sparse::getRewardParameters(*model); @@ -331,7 +331,7 @@ TEST(SparseDtmcParameterLiftingTest, Crowds_Prob_1Par) { storm::prism::Program program = storm::parseProgram(programFile); program = storm::utility::prism::preprocess(program, constantsAsString); std::vector> formulas = storm::extractFormulasFromProperties(storm::parsePropertiesForPrismProgram(formulaAsString, program)); - std::shared_ptr> model = storm::buildSparseModel(program, formulas).getModel()->as>(); + std::shared_ptr> model = storm::buildSparseModel(program, formulas)->as>(); auto modelParameters = storm::models::sparse::getProbabilityParameters(*model); auto rewParameters = storm::models::sparse::getRewardParameters(*model); @@ -362,7 +362,7 @@ TEST(SparseDtmcParameterLiftingTest, Crowds_Prob_Const) { storm::prism::Program program = storm::parseProgram(programFile); program = storm::utility::prism::preprocess(program, constantsAsString); std::vector> formulas = storm::extractFormulasFromProperties(storm::parsePropertiesForPrismProgram(formulaAsString, program)); - std::shared_ptr> model = storm::buildSparseModel(program, formulas).getModel()->as>(); + std::shared_ptr> model = storm::buildSparseModel(program, formulas)->as>(); auto modelParameters = storm::models::sparse::getProbabilityParameters(*model); auto rewParameters = storm::models::sparse::getRewardParameters(*model); diff --git a/src/test/modelchecker/SparseMaPcaaMultiObjectiveModelCheckerTest.cpp b/src/test/modelchecker/SparseMaPcaaMultiObjectiveModelCheckerTest.cpp index 51c3abd19..72523eb50 100644 --- a/src/test/modelchecker/SparseMaPcaaMultiObjectiveModelCheckerTest.cpp +++ b/src/test/modelchecker/SparseMaPcaaMultiObjectiveModelCheckerTest.cpp @@ -56,7 +56,7 @@ TEST(SparseMaPcaaMultiObjectiveModelCheckerTest, server) { storm::prism::Program program = storm::parseProgram(programFile); program = storm::utility::prism::preprocess(program, ""); std::vector> formulas = storm::extractFormulasFromProperties(storm::parsePropertiesForPrismProgram(formulasAsString, program)); - std::shared_ptr> ma = storm::buildSparseModel(program, formulas).getModel()->as>(); + std::shared_ptr> ma = storm::buildSparseModel(program, formulas)->as>(); std::unique_ptr result = storm::modelchecker::multiobjective::performMultiObjectiveModelChecking(*ma, formulas[0]->asMultiObjectiveFormula(), storm::modelchecker::multiobjective::MultiObjectiveMethodSelection::Pcaa); ASSERT_TRUE(result->isExplicitParetoCurveCheckResult()); @@ -85,7 +85,7 @@ TEST(SparseMaPcaaMultiObjectiveModelCheckerTest, jobscheduler_pareto_3Obj) { storm::prism::Program program = storm::parseProgram(programFile); program = storm::utility::prism::preprocess(program, ""); std::vector> formulas = storm::extractFormulasFromProperties(storm::parsePropertiesForPrismProgram(formulasAsString, program)); - std::shared_ptr> ma = storm::buildSparseModel(program, formulas).getModel()->as>(); + std::shared_ptr> ma = storm::buildSparseModel(program, formulas)->as>(); std::unique_ptr result = storm::modelchecker::multiobjective::performMultiObjectiveModelChecking(*ma, formulas[0]->asMultiObjectiveFormula(), storm::modelchecker::multiobjective::MultiObjectiveMethodSelection::Pcaa); ASSERT_TRUE(result->isExplicitParetoCurveCheckResult()); @@ -116,7 +116,7 @@ TEST(SparseMaPcaaMultiObjectiveModelCheckerTest, jobscheduler_achievability_3Obj storm::prism::Program program = storm::parseProgram(programFile); program = storm::utility::prism::preprocess(program, ""); std::vector> formulas = storm::extractFormulasFromProperties(storm::parsePropertiesForPrismProgram(formulasAsString, program)); - std::shared_ptr> ma = storm::buildSparseModel(program, formulas).getModel()->as>(); + std::shared_ptr> ma = storm::buildSparseModel(program, formulas)->as>(); uint_fast64_t const initState = *ma->getInitialStates().begin(); std::unique_ptr result = storm::modelchecker::multiobjective::performMultiObjectiveModelChecking(*ma, formulas[0]->asMultiObjectiveFormula(), storm::modelchecker::multiobjective::MultiObjectiveMethodSelection::Pcaa); @@ -137,7 +137,7 @@ TEST(SparseMaPcaaMultiObjectiveModelCheckerTest, jobscheduler_quantitative_3Obj) storm::prism::Program program = storm::parseProgram(programFile); program = storm::utility::prism::preprocess(program, ""); std::vector> formulas = storm::extractFormulasFromProperties(storm::parsePropertiesForPrismProgram(formulasAsString, program)); - std::shared_ptr> ma = storm::buildSparseModel(program, formulas).getModel()->as>(); + std::shared_ptr> ma = storm::buildSparseModel(program, formulas)->as>(); uint_fast64_t const initState = *ma->getInitialStates().begin(); @@ -158,7 +158,7 @@ TEST(SparseMaPcaaMultiObjectiveModelCheckerTest, jobscheduler_pareto_2Obj) { storm::prism::Program program = storm::parseProgram(programFile); program = storm::utility::prism::preprocess(program, ""); std::vector> formulas = storm::extractFormulasFromProperties(storm::parsePropertiesForPrismProgram(formulasAsString, program)); - std::shared_ptr> ma = storm::buildSparseModel(program, formulas).getModel()->as>(); + std::shared_ptr> ma = storm::buildSparseModel(program, formulas)->as>(); std::unique_ptr result = storm::modelchecker::multiobjective::performMultiObjectiveModelChecking(*ma, formulas[0]->asMultiObjectiveFormula(), storm::modelchecker::multiobjective::MultiObjectiveMethodSelection::Pcaa); ASSERT_TRUE(result->isExplicitParetoCurveCheckResult()); diff --git a/src/test/modelchecker/SparseMdpParameterLiftingTest.cpp b/src/test/modelchecker/SparseMdpParameterLiftingTest.cpp index 59f1eb9f4..81832d240 100644 --- a/src/test/modelchecker/SparseMdpParameterLiftingTest.cpp +++ b/src/test/modelchecker/SparseMdpParameterLiftingTest.cpp @@ -16,7 +16,7 @@ TEST(SparseMdpParameterLiftingTest, two_dice_Prob) { storm::prism::Program program = storm::parseProgram(programFile); std::vector> formulas = storm::extractFormulasFromProperties(storm::parsePropertiesForPrismProgram(formulaFile, program)); - std::shared_ptr> model = storm::buildSparseModel(program, formulas).getModel()->as>(); + std::shared_ptr> model = storm::buildSparseModel(program, formulas)->as>(); auto modelParameters = storm::models::sparse::getProbabilityParameters(*model); auto rewParameters = storm::models::sparse::getRewardParameters(*model); @@ -46,7 +46,7 @@ TEST(SparseMdpParameterLiftingTest, two_dice_Prob_bounded) { storm::prism::Program program = storm::parseProgram(programFile); std::vector> formulas = storm::extractFormulasFromProperties(storm::parsePropertiesForPrismProgram(formulaFile, program)); - std::shared_ptr> model = storm::buildSparseModel(program, formulas).getModel()->as>(); + std::shared_ptr> model = storm::buildSparseModel(program, formulas)->as>(); auto modelParameters = storm::models::sparse::getProbabilityParameters(*model); auto rewParameters = storm::models::sparse::getRewardParameters(*model); @@ -76,7 +76,7 @@ TEST(SparseMdpParameterLiftingTest, two_dice_Prob_exactValidation) { storm::prism::Program program = storm::parseProgram(programFile); std::vector> formulas = storm::extractFormulasFromProperties(storm::parsePropertiesForPrismProgram(formulaFile, program)); - std::shared_ptr> model = storm::buildSparseModel(program, formulas).getModel()->as>(); + std::shared_ptr> model = storm::buildSparseModel(program, formulas)->as>(); auto modelParameters = storm::models::sparse::getProbabilityParameters(*model); auto rewParameters = storm::models::sparse::getRewardParameters(*model); @@ -106,7 +106,7 @@ TEST(SparseMdpParameterLiftingTest, two_dice_Prob_bounded_exactValidation) { storm::prism::Program program = storm::parseProgram(programFile); std::vector> formulas = storm::extractFormulasFromProperties(storm::parsePropertiesForPrismProgram(formulaFile, program)); - std::shared_ptr> model = storm::buildSparseModel(program, formulas).getModel()->as>(); + std::shared_ptr> model = storm::buildSparseModel(program, formulas)->as>(); auto modelParameters = storm::models::sparse::getProbabilityParameters(*model); auto rewParameters = storm::models::sparse::getRewardParameters(*model); @@ -134,7 +134,7 @@ TEST(SparseMdpParameterLiftingTest, coin_Prob) { storm::prism::Program program = storm::parseProgram(programFile); std::vector> formulas = storm::extractFormulasFromProperties(storm::parsePropertiesForPrismProgram(formulaAsString, program)); - std::shared_ptr> model = storm::buildSparseModel(program, formulas).getModel()->as>(); + std::shared_ptr> model = storm::buildSparseModel(program, formulas)->as>(); auto modelParameters = storm::models::sparse::getProbabilityParameters(*model); auto rewParameters = storm::models::sparse::getRewardParameters(*model); @@ -164,7 +164,7 @@ TEST(SparseMdpParameterLiftingTest, brp_Prop) { storm::prism::Program program = storm::parseProgram(programFile); program = storm::utility::prism::preprocess(program, constantsAsString); std::vector> formulas = storm::extractFormulasFromProperties(storm::parsePropertiesForPrismProgram(formulaAsString, program)); - std::shared_ptr> model = storm::buildSparseModel(program, formulas).getModel()->as>(); + std::shared_ptr> model = storm::buildSparseModel(program, formulas)->as>(); auto modelParameters = storm::models::sparse::getProbabilityParameters(*model); auto rewParameters = storm::models::sparse::getRewardParameters(*model); @@ -195,7 +195,7 @@ TEST(SparseMdpParameterLiftingTest, brp_Rew) { storm::prism::Program program = storm::parseProgram(programFile); program = storm::utility::prism::preprocess(program, constantsAsString); std::vector> formulas = storm::extractFormulasFromProperties(storm::parsePropertiesForPrismProgram(formulaAsString, program)); - std::shared_ptr> model = storm::buildSparseModel(program, formulas).getModel()->as>(); + std::shared_ptr> model = storm::buildSparseModel(program, formulas)->as>(); auto modelParameters = storm::models::sparse::getProbabilityParameters(*model); auto rewParameters = storm::models::sparse::getRewardParameters(*model); @@ -225,7 +225,7 @@ TEST(SparseMdpParameterLiftingTest, brp_Rew_bounded) { storm::prism::Program program = storm::parseProgram(programFile); program = storm::utility::prism::preprocess(program, constantsAsString); std::vector> formulas = storm::extractFormulasFromProperties(storm::parsePropertiesForPrismProgram(formulaAsString, program)); - std::shared_ptr> model = storm::buildSparseModel(program, formulas).getModel()->as>(); + std::shared_ptr> model = storm::buildSparseModel(program, formulas)->as>(); auto modelParameters = storm::models::sparse::getProbabilityParameters(*model); auto rewParameters = storm::models::sparse::getRewardParameters(*model); @@ -256,7 +256,7 @@ TEST(SparseMdpParameterLiftingTest, Brp_Rew_Infty) { storm::prism::Program program = storm::parseProgram(programFile); program = storm::utility::prism::preprocess(program, constantsAsString); std::vector> formulas = storm::extractFormulasFromProperties(storm::parsePropertiesForPrismProgram(formulaAsString, program)); - std::shared_ptr> model = storm::buildSparseModel(program, formulas).getModel()->as>(); + std::shared_ptr> model = storm::buildSparseModel(program, formulas)->as>(); auto modelParameters = storm::models::sparse::getProbabilityParameters(*model); auto rewParameters = storm::models::sparse::getRewardParameters(*model); @@ -282,7 +282,7 @@ TEST(SparseMdpParameterLiftingTest, Brp_Rew_4Par) { storm::prism::Program program = storm::parseProgram(programFile); program = storm::utility::prism::preprocess(program, constantsAsString); std::vector> formulas = storm::extractFormulasFromProperties(storm::parsePropertiesForPrismProgram(formulaAsString, program)); - std::shared_ptr> model = storm::buildSparseModel(program, formulas).getModel()->as>(); + std::shared_ptr> model = storm::buildSparseModel(program, formulas)->as>(); auto modelParameters = storm::models::sparse::getProbabilityParameters(*model); auto rewParameters = storm::models::sparse::getRewardParameters(*model); diff --git a/src/test/modelchecker/SparseMdpPcaaMultiObjectiveModelCheckerTest.cpp b/src/test/modelchecker/SparseMdpPcaaMultiObjectiveModelCheckerTest.cpp index 996220281..0d315e74b 100644 --- a/src/test/modelchecker/SparseMdpPcaaMultiObjectiveModelCheckerTest.cpp +++ b/src/test/modelchecker/SparseMdpPcaaMultiObjectiveModelCheckerTest.cpp @@ -23,7 +23,7 @@ TEST(SparseMdpPcaaMultiObjectiveModelCheckerTest, consensus) { storm::prism::Program program = storm::parseProgram(programFile); program = storm::utility::prism::preprocess(program, ""); std::vector> formulas = storm::extractFormulasFromProperties(storm::parsePropertiesForPrismProgram(formulasAsString, program)); - std::shared_ptr> mdp = storm::buildSparseModel(program, formulas).getModel()->as>(); + std::shared_ptr> mdp = storm::buildSparseModel(program, formulas)->as>(); uint_fast64_t const initState = *mdp->getInitialStates().begin();; std::unique_ptr result = storm::modelchecker::multiobjective::performMultiObjectiveModelChecking(*mdp, formulas[0]->asMultiObjectiveFormula(), storm::modelchecker::multiobjective::MultiObjectiveMethodSelection::Pcaa); @@ -49,7 +49,7 @@ TEST(SparseMdpPcaaMultiObjectiveModelCheckerTest, zeroconf) { storm::prism::Program program = storm::parseProgram(programFile); program = storm::utility::prism::preprocess(program, ""); std::vector> formulas = storm::extractFormulasFromProperties(storm::parsePropertiesForPrismProgram(formulasAsString, program)); - std::shared_ptr> mdp = storm::buildSparseModel(program, formulas).getModel()->as>(); + std::shared_ptr> mdp = storm::buildSparseModel(program, formulas)->as>(); uint_fast64_t const initState = *mdp->getInitialStates().begin(); std::unique_ptr result = storm::modelchecker::multiobjective::performMultiObjectiveModelChecking(*mdp, formulas[0]->asMultiObjectiveFormula(), storm::modelchecker::multiobjective::MultiObjectiveMethodSelection::Pcaa); @@ -66,7 +66,7 @@ TEST(SparseMdpPcaaMultiObjectiveModelCheckerTest, team3with3objectives) { storm::prism::Program program = storm::parseProgram(programFile); program = storm::utility::prism::preprocess(program, ""); std::vector> formulas = storm::extractFormulasFromProperties(storm::parsePropertiesForPrismProgram(formulasAsString, program)); - std::shared_ptr> mdp = storm::buildSparseModel(program, formulas).getModel()->as>(); + std::shared_ptr> mdp = storm::buildSparseModel(program, formulas)->as>(); uint_fast64_t const initState = *mdp->getInitialStates().begin(); std::unique_ptr result = storm::modelchecker::multiobjective::performMultiObjectiveModelChecking(*mdp, formulas[0]->asMultiObjectiveFormula(), storm::modelchecker::multiobjective::MultiObjectiveMethodSelection::Pcaa); @@ -83,7 +83,7 @@ TEST(SparseMdpPcaaMultiObjectiveModelCheckerTest, scheduler) { storm::prism::Program program = storm::parseProgram(programFile); program = storm::utility::prism::preprocess(program, ""); std::vector> formulas = storm::extractFormulasFromProperties(storm::parsePropertiesForPrismProgram(formulasAsString, program)); - std::shared_ptr> mdp = storm::buildSparseModel(program, formulas).getModel()->as>(); + std::shared_ptr> mdp = storm::buildSparseModel(program, formulas)->as>(); uint_fast64_t const initState = *mdp->getInitialStates().begin(); std::unique_ptr result = storm::modelchecker::multiobjective::performMultiObjectiveModelChecking(*mdp, formulas[0]->asMultiObjectiveFormula(), storm::modelchecker::multiobjective::MultiObjectiveMethodSelection::Pcaa); @@ -99,7 +99,7 @@ TEST(SparseMdpPcaaMultiObjectiveModelCheckerTest, dpm) { storm::prism::Program program = storm::parseProgram(programFile); program = storm::utility::prism::preprocess(program, ""); std::vector> formulas = storm::extractFormulasFromProperties(storm::parsePropertiesForPrismProgram(formulasAsString, program)); - std::shared_ptr> mdp = storm::buildSparseModel(program, formulas).getModel()->as>(); + std::shared_ptr> mdp = storm::buildSparseModel(program, formulas)->as>(); uint_fast64_t const initState = *mdp->getInitialStates().begin(); std::unique_ptr result = storm::modelchecker::multiobjective::performMultiObjectiveModelChecking(*mdp, formulas[0]->asMultiObjectiveFormula(), storm::modelchecker::multiobjective::MultiObjectiveMethodSelection::Pcaa);