adding Markov automaton tests to explicit JANI model builder

Former-commit-id: 634fe9c08e [formerly 73bbe89f78]
Former-commit-id: bb9339a947

src/generator/JaniNextStateGenerator.cpp

@@ -355,7 +355,7 @@ namespace storm {
                     }
                     
                     // Determine the exit rate if it's a Markovian edge.
-                    boost::optional<ValueType> exitRate;
+                    boost::optional<ValueType> exitRate = boost::none;
                     if (edge.hasRate()) {
                         exitRate = this->evaluator.asRational(edge.getRate());
                     }

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.

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) << ").");
                     }
                 }
             }

src/storage/prism/ToJaniConverter.cpp

@@ -192,7 +192,7 @@ namespace storm {
                     
                     boost::optional<storm::expressions::Expression> rateExpression;
                     std::vector<storm::jani::EdgeDestination> 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<storm::jani::Assignment> assignments;
                         for (auto const& assignment : update.getAssignments()) {

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<storm::models::sparse::Model<double>> model = storm::builder::ExplicitModelBuilder<double>(program).build();
+    std::shared_ptr<storm::models::sparse::Model<double>> model = storm::builder::ExplicitModelBuilder<double>(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<storm::models::sparse::Model<double>> model = storm::builder::ExplicitModelBuilder<double>(program).build();
+    std::shared_ptr<storm::models::sparse::Model<double>> model = storm::builder::ExplicitModelBuilder<double>(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<storm::models::sparse::Model<double>> model = storm::builder::ExplicitModelBuilder<double>(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<storm::models::sparse::MarkovAutomaton<double>>()->getMarkovianStates().getNumberOfSetBits());
+    
+    program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/hybrid_states.ma");
+    janiModel = program.toJani();
+    model = storm::builder::ExplicitModelBuilder<double>(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<storm::models::sparse::MarkovAutomaton<double>>()->getMarkovianStates().getNumberOfSetBits());
+    
+    program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/stream2.ma");
+    janiModel = program.toJani();
+    model = storm::builder::ExplicitModelBuilder<double>(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<storm::models::sparse::MarkovAutomaton<double>>()->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();

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<storm::models::sparse::MarkovAutomaton<double>>()->getMarkovianStates().getNumberOfSetBits());
-    
 }
 
 TEST(ExplicitPrismModelBuilderTest, FailComposition) {