diff --git a/test/functional/utility/GraphTest.cpp b/test/functional/utility/GraphTest.cpp index 9a17e4207..68c62182a 100644 --- a/test/functional/utility/GraphTest.cpp +++ b/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>(), model->getReachableStates(), model->getStates("collision_max_backoff")); ASSERT_NO_THROW(statesWithProbability01 = storm::utility::graph::performProb01Min(*model->as>(), model->getReachableStates(), model->getStates("collision_max_backoff"))); EXPECT_EQ(993, statesWithProbability01.first.getNonZeroCount()); EXPECT_EQ(16, statesWithProbability01.second.getNonZeroCount()); @@ -102,4 +102,55 @@ TEST(GraphTest, ExplicitProb01) { ASSERT_NO_THROW(statesWithProbability01 = storm::utility::graph::performProb01(*model->as>(), storm::storage::BitVector(model->getNumberOfStates(), true), model->getStates("observeOnlyTrueSender"))); 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> model = storm::builder::ExplicitPrismModelBuilder::translateProgram(program); + + ASSERT_TRUE(model->getType() == storm::models::ModelType::Mdp); + + std::pair statesWithProbability01; + + ASSERT_NO_THROW(statesWithProbability01 = storm::utility::graph::performProb01Min(*model->as>(), 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::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::translateProgram(program); + + ASSERT_TRUE(model->getType() == storm::models::ModelType::Mdp); + + ASSERT_NO_THROW(statesWithProbability01 = storm::utility::graph::performProb01Min(*model->as>(), 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::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::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::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::translateProgram(program); + + ASSERT_TRUE(model->getType() == storm::models::ModelType::Mdp); + + ASSERT_NO_THROW(statesWithProbability01 = storm::utility::graph::performProb01Min(*model->as>(), 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::storage::BitVector(model->getNumberOfStates(), true), model->getStates("collision_max_backoff"))); + EXPECT_EQ(993, statesWithProbability01.first.getNumberOfSetBits()); + EXPECT_EQ(16, statesWithProbability01.second.getNumberOfSetBits()); } \ No newline at end of file