diff --git a/src/generator/JaniNextStateGenerator.cpp b/src/generator/JaniNextStateGenerator.cpp index 59d0eab9b..50f1c76a4 100644 --- a/src/generator/JaniNextStateGenerator.cpp +++ b/src/generator/JaniNextStateGenerator.cpp @@ -355,7 +355,7 @@ namespace storm { } // Determine the exit rate if it's a Markovian edge. - boost::optional exitRate; + boost::optional exitRate = boost::none; if (edge.hasRate()) { exitRate = this->evaluator.asRational(edge.getRate()); } diff --git a/src/generator/NextStateGenerator.cpp b/src/generator/NextStateGenerator.cpp index a7fa2a044..08fe61ba1 100644 --- a/src/generator/NextStateGenerator.cpp +++ b/src/generator/NextStateGenerator.cpp @@ -326,8 +326,10 @@ namespace storm { // that the previous Markovian choice is the very first one in the choices vector. result.getChoices().front().add(choice); - // Swap the choice to the end to indicate it can be removed. - std::swap(choice, result.getChoices().back()); + // Swap the choice to the end to indicate it can be removed (if it's not already there). + if (index != result.getNumberOfChoices() - 1) { + std::swap(choice, result.getChoices().back()); + } ++numberOfChoicesToDelete; } else { // If there is no previous Markovian choice, just move the Markovian choice to the front. diff --git a/src/models/sparse/MarkovAutomaton.cpp b/src/models/sparse/MarkovAutomaton.cpp index 887d3a13b..e50d10bef 100644 --- a/src/models/sparse/MarkovAutomaton.cpp +++ b/src/models/sparse/MarkovAutomaton.cpp @@ -259,15 +259,15 @@ namespace storm { this->exitRates.resize(this->getNumberOfStates()); for (uint_fast64_t state = 0; state< this->getNumberOfStates(); ++state) { uint_fast64_t row = this->getTransitionMatrix().getRowGroupIndices()[state]; - if(this->markovianStates.get(state)) { + if (this->markovianStates.get(state)) { this->exitRates[state] = this->getTransitionMatrix().getRowSum(row); for (auto& transition : this->getTransitionMatrix().getRow(row)) { transition.setValue(transition.getValue() / this->exitRates[state]); } ++row; } - for(; row < this->getTransitionMatrix().getRowGroupIndices()[state+1]; ++row) { - STORM_LOG_THROW(storm::utility::isOne(this->getTransitionMatrix().getRowSum(row)), storm::exceptions::InvalidArgumentException, "Transitions of rateMatrix do not sum up to one for some non-Markovian choice. Sum is " << this->getTransitionMatrix().getRowSum(row) << ". State is " << state << ". Choice is " << row << "."); + for (; row < this->getTransitionMatrix().getRowGroupIndices()[state+1]; ++row) { + STORM_LOG_THROW(storm::utility::isOne(this->getTransitionMatrix().getRowSum(row)), storm::exceptions::InvalidArgumentException, "Entries of transition matrix do not sum up to one for (non-Markovian) choice " << row << " of state " << state << " (sum is " << this->getTransitionMatrix().getRowSum(row) << ")."); } } } diff --git a/src/storage/prism/ToJaniConverter.cpp b/src/storage/prism/ToJaniConverter.cpp index 0a5594427..65289382a 100644 --- a/src/storage/prism/ToJaniConverter.cpp +++ b/src/storage/prism/ToJaniConverter.cpp @@ -192,7 +192,7 @@ namespace storm { boost::optional rateExpression; std::vector destinations; - if (program.getModelType() == Program::ModelType::CTMC || program.getModelType() == Program::ModelType::CTMDP) { + if (program.getModelType() == Program::ModelType::CTMC || program.getModelType() == Program::ModelType::CTMDP || (program.getModelType() == Program::ModelType::MA && command.isMarkovian())) { for (auto const& update : command.getUpdates()) { if (rateExpression) { rateExpression = rateExpression.get() + update.getLikelihoodExpression(); @@ -201,7 +201,7 @@ namespace storm { } } } - + for (auto const& update : command.getUpdates()) { std::vector assignments; for (auto const& assignment : update.getAssignments()) { diff --git a/test/functional/builder/ExplicitJaniModelBuilderTest.cpp b/test/functional/builder/ExplicitJaniModelBuilderTest.cpp index 17df2ca97..405b6d248 100644 --- a/test/functional/builder/ExplicitJaniModelBuilderTest.cpp +++ b/test/functional/builder/ExplicitJaniModelBuilderTest.cpp @@ -1,6 +1,7 @@ #include "gtest/gtest.h" #include "storm-config.h" #include "src/models/sparse/StandardRewardModel.h" +#include "src/models/sparse/MarkovAutomaton.h" #include "src/settings/SettingMemento.h" #include "src/parser/PrismParser.h" #include "src/builder/ExplicitModelBuilder.h" @@ -48,7 +49,7 @@ TEST(ExplicitJaniModelBuilderTest, Ctmc) { storm::prism::Program program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/cluster2.sm"); storm::jani::Model janiModel = program.toJani(); - std::shared_ptr> model = storm::builder::ExplicitModelBuilder(program).build(); + std::shared_ptr> model = storm::builder::ExplicitModelBuilder(janiModel).build(); EXPECT_EQ(276ul, model->getNumberOfStates()); EXPECT_EQ(1120ul, model->getNumberOfTransitions()); @@ -81,7 +82,7 @@ TEST(ExplicitJaniModelBuilderTest, 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(); - std::shared_ptr> model = storm::builder::ExplicitModelBuilder(program).build(); + std::shared_ptr> model = storm::builder::ExplicitModelBuilder(janiModel).build(); EXPECT_EQ(169ul, model->getNumberOfStates()); EXPECT_EQ(436ul, model->getNumberOfTransitions()); @@ -116,6 +117,33 @@ TEST(ExplicitJaniModelBuilderTest, Mdp) { EXPECT_EQ(59ul, model->getNumberOfTransitions()); } +TEST(ExplicitJaniModelBuilderTest, Ma) { + storm::prism::Program program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/simple.ma"); + storm::jani::Model janiModel = program.toJani(); + + std::shared_ptr> model = storm::builder::ExplicitModelBuilder(janiModel).build(); + EXPECT_EQ(5ul, model->getNumberOfStates()); + EXPECT_EQ(8ul, model->getNumberOfTransitions()); + ASSERT_TRUE(model->isOfType(storm::models::ModelType::MarkovAutomaton)); + EXPECT_EQ(4ul, model->as>()->getMarkovianStates().getNumberOfSetBits()); + + program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/hybrid_states.ma"); + janiModel = program.toJani(); + model = storm::builder::ExplicitModelBuilder(janiModel).build(); + EXPECT_EQ(5ul, model->getNumberOfStates()); + EXPECT_EQ(13ul, model->getNumberOfTransitions()); + ASSERT_TRUE(model->isOfType(storm::models::ModelType::MarkovAutomaton)); + EXPECT_EQ(5ul, model->as>()->getMarkovianStates().getNumberOfSetBits()); + + program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/stream2.ma"); + janiModel = program.toJani(); + model = storm::builder::ExplicitModelBuilder(janiModel).build(); + EXPECT_EQ(12ul, model->getNumberOfStates()); + EXPECT_EQ(14ul, model->getNumberOfTransitions()); + ASSERT_TRUE(model->isOfType(storm::models::ModelType::MarkovAutomaton)); + EXPECT_EQ(7ul, model->as>()->getMarkovianStates().getNumberOfSetBits()); +} + TEST(ExplicitJaniModelBuilderTest, FailComposition) { storm::prism::Program program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/system_composition.nm"); storm::jani::Model janiModel = program.toJani(); diff --git a/test/functional/builder/ExplicitPrismModelBuilderTest.cpp b/test/functional/builder/ExplicitPrismModelBuilderTest.cpp index 66906c2c5..d5e5a1771 100644 --- a/test/functional/builder/ExplicitPrismModelBuilderTest.cpp +++ b/test/functional/builder/ExplicitPrismModelBuilderTest.cpp @@ -122,7 +122,6 @@ TEST(ExplicitPrismModelBuilderTest, Ma) { EXPECT_EQ(14ul, model->getNumberOfTransitions()); ASSERT_TRUE(model->isOfType(storm::models::ModelType::MarkovAutomaton)); EXPECT_EQ(7ul, model->as>()->getMarkovianStates().getNumberOfSetBits()); - } TEST(ExplicitPrismModelBuilderTest, FailComposition) {