Added tests for sparse Prob0/1 to functional tests

Former-commit-id: ef8f9ffb59

test/functional/utility/GraphTest.cpp

@@ -6,6 +6,7 @@
 #include "src/models/symbolic/Dtmc.h"
 #include "src/models/symbolic/Mdp.h"
 #include "src/models/sparse/Dtmc.h"
+#include "src/models/sparse/Mdp.h"
 #include "src/builder/DdPrismModelBuilder.h"
 #include "src/builder/ExplicitPrismModelBuilder.h"
 #include "src/utility/graph.h"
@@ -73,7 +74,6 @@ TEST(GraphTest, SymbolicProb01MinMax) {
     
     ASSERT_TRUE(model->getType() == storm::models::ModelType::Mdp);
     
-    statesWithProbability01 = storm::utility::graph::performProb01Min(*model->as<storm::models::symbolic::Mdp<storm::dd::DdType::CUDD>>(), model->getReachableStates(), model->getStates("collision_max_backoff"));
     ASSERT_NO_THROW(statesWithProbability01 = storm::utility::graph::performProb01Min(*model->as<storm::models::symbolic::Mdp<storm::dd::DdType::CUDD>>(), model->getReachableStates(), model->getStates("collision_max_backoff")));
     EXPECT_EQ(993, statesWithProbability01.first.getNonZeroCount());
     EXPECT_EQ(16, statesWithProbability01.second.getNonZeroCount());
@@ -103,3 +103,54 @@ TEST(GraphTest, ExplicitProb01) {
     EXPECT_EQ(5829, statesWithProbability01.first.getNumberOfSetBits());
     EXPECT_EQ(1032, statesWithProbability01.second.getNumberOfSetBits());
 }
+
+TEST(GraphTest, ExplicitProb01MinMax) {
+    storm::prism::Program program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/leader3.nm");
+    std::shared_ptr<storm::models::sparse::Model<double>> model = storm::builder::ExplicitPrismModelBuilder<double>::translateProgram(program);
+    
+    ASSERT_TRUE(model->getType() == storm::models::ModelType::Mdp);
+    
+    std::pair<storm::storage::BitVector, storm::storage::BitVector> statesWithProbability01;
+    
+    ASSERT_NO_THROW(statesWithProbability01 = storm::utility::graph::performProb01Min(*model->as<storm::models::sparse::Mdp<double>>(), storm::storage::BitVector(model->getNumberOfStates(), true), model->getStates("elected")));
+    EXPECT_EQ(0, statesWithProbability01.first.getNumberOfSetBits());
+    EXPECT_EQ(364, statesWithProbability01.second.getNumberOfSetBits());
+    
+    ASSERT_NO_THROW(statesWithProbability01 = storm::utility::graph::performProb01Max(*model->as<storm::models::sparse::Mdp<double>>(), storm::storage::BitVector(model->getNumberOfStates(), true), model->getStates("elected")));
+    EXPECT_EQ(0, statesWithProbability01.first.getNumberOfSetBits());
+    EXPECT_EQ(364, statesWithProbability01.second.getNumberOfSetBits());
+    
+    program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/coin2-2.nm");
+    model = storm::builder::ExplicitPrismModelBuilder<double>::translateProgram(program);
+    
+    ASSERT_TRUE(model->getType() == storm::models::ModelType::Mdp);
+    
+    ASSERT_NO_THROW(statesWithProbability01 = storm::utility::graph::performProb01Min(*model->as<storm::models::sparse::Mdp<double>>(), storm::storage::BitVector(model->getNumberOfStates(), true), model->getStates("all_coins_equal_0")));
+    EXPECT_EQ(77, statesWithProbability01.first.getNumberOfSetBits());
+    EXPECT_EQ(149, statesWithProbability01.second.getNumberOfSetBits());
+    
+    ASSERT_NO_THROW(statesWithProbability01 = storm::utility::graph::performProb01Max(*model->as<storm::models::sparse::Mdp<double>>(), storm::storage::BitVector(model->getNumberOfStates(), true), model->getStates("all_coins_equal_0")));
+    EXPECT_EQ(74, statesWithProbability01.first.getNumberOfSetBits());
+    EXPECT_EQ(198, statesWithProbability01.second.getNumberOfSetBits());
+    
+    ASSERT_NO_THROW(statesWithProbability01 = storm::utility::graph::performProb01Min(*model->as<storm::models::sparse::Mdp<double>>(), storm::storage::BitVector(model->getNumberOfStates(), true), model->getStates("all_coins_equal_1")));
+    EXPECT_EQ(94, statesWithProbability01.first.getNumberOfSetBits());
+    EXPECT_EQ(33, statesWithProbability01.second.getNumberOfSetBits());
+    
+    ASSERT_NO_THROW(statesWithProbability01 = storm::utility::graph::performProb01Max(*model->as<storm::models::sparse::Mdp<double>>(), storm::storage::BitVector(model->getNumberOfStates(), true), model->getStates("all_coins_equal_1")));
+    EXPECT_EQ(83, statesWithProbability01.first.getNumberOfSetBits());
+    EXPECT_EQ(35, statesWithProbability01.second.getNumberOfSetBits());
+    
+    program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/csma2-2.nm");
+    model = storm::builder::ExplicitPrismModelBuilder<double>::translateProgram(program);
+    
+    ASSERT_TRUE(model->getType() == storm::models::ModelType::Mdp);
+    
+    ASSERT_NO_THROW(statesWithProbability01 = storm::utility::graph::performProb01Min(*model->as<storm::models::sparse::Mdp<double>>(), storm::storage::BitVector(model->getNumberOfStates(), true), model->getStates("collision_max_backoff")));
+    EXPECT_EQ(993, statesWithProbability01.first.getNumberOfSetBits());
+    EXPECT_EQ(16, statesWithProbability01.second.getNumberOfSetBits());
+    
+    ASSERT_NO_THROW(statesWithProbability01 = storm::utility::graph::performProb01Max(*model->as<storm::models::sparse::Mdp<double>>(), storm::storage::BitVector(model->getNumberOfStates(), true), model->getStates("collision_max_backoff")));
+    EXPECT_EQ(993, statesWithProbability01.first.getNumberOfSetBits());
+    EXPECT_EQ(16, statesWithProbability01.second.getNumberOfSetBits());
+}