|
|
@ -20,16 +20,16 @@ TEST(GraphTest, SymbolicProb01) { |
|
|
|
std::pair<storm::dd::Bdd<storm::dd::DdType::CUDD>, storm::dd::Bdd<storm::dd::DdType::CUDD>> statesWithProbability01; |
|
|
|
|
|
|
|
ASSERT_NO_THROW(statesWithProbability01 = storm::utility::graph::performProb01(*model->as<storm::models::symbolic::Dtmc<storm::dd::DdType::CUDD>>(), model->getReachableStates(), model->getStates("observe0Greater1"))); |
|
|
|
EXPECT_EQ(4409, statesWithProbability01.first.getNonZeroCount()); |
|
|
|
EXPECT_EQ(1316, statesWithProbability01.second.getNonZeroCount()); |
|
|
|
EXPECT_EQ(4409ul, statesWithProbability01.first.getNonZeroCount()); |
|
|
|
EXPECT_EQ(1316ul, statesWithProbability01.second.getNonZeroCount()); |
|
|
|
|
|
|
|
ASSERT_NO_THROW(statesWithProbability01 = storm::utility::graph::performProb01(*model->as<storm::models::symbolic::Dtmc<storm::dd::DdType::CUDD>>(), model->getReachableStates(), model->getStates("observeIGreater1"))); |
|
|
|
EXPECT_EQ(1091, statesWithProbability01.first.getNonZeroCount()); |
|
|
|
EXPECT_EQ(4802, statesWithProbability01.second.getNonZeroCount()); |
|
|
|
EXPECT_EQ(1091ul, statesWithProbability01.first.getNonZeroCount()); |
|
|
|
EXPECT_EQ(4802ul, statesWithProbability01.second.getNonZeroCount()); |
|
|
|
|
|
|
|
ASSERT_NO_THROW(statesWithProbability01 = storm::utility::graph::performProb01(*model->as<storm::models::symbolic::Dtmc<storm::dd::DdType::CUDD>>(), model->getReachableStates(), model->getStates("observeOnlyTrueSender"))); |
|
|
|
EXPECT_EQ(5829, statesWithProbability01.first.getNonZeroCount()); |
|
|
|
EXPECT_EQ(1032, statesWithProbability01.second.getNonZeroCount()); |
|
|
|
EXPECT_EQ(5829ul, statesWithProbability01.first.getNonZeroCount()); |
|
|
|
EXPECT_EQ(1032ul, statesWithProbability01.second.getNonZeroCount()); |
|
|
|
} |
|
|
|
|
|
|
|
TEST(GraphTest, SymbolicProb01MinMax) { |
|
|
@ -41,12 +41,12 @@ TEST(GraphTest, SymbolicProb01MinMax) { |
|
|
|
std::pair<storm::dd::Bdd<storm::dd::DdType::CUDD>, storm::dd::Bdd<storm::dd::DdType::CUDD>> statesWithProbability01; |
|
|
|
|
|
|
|
ASSERT_NO_THROW(statesWithProbability01 = storm::utility::graph::performProb01Min(*model->as<storm::models::symbolic::Mdp<storm::dd::DdType::CUDD>>(), model->getReachableStates(), model->getStates("elected"))); |
|
|
|
EXPECT_EQ(0, statesWithProbability01.first.getNonZeroCount()); |
|
|
|
EXPECT_EQ(364, statesWithProbability01.second.getNonZeroCount()); |
|
|
|
EXPECT_EQ(0ul, statesWithProbability01.first.getNonZeroCount()); |
|
|
|
EXPECT_EQ(364ul, statesWithProbability01.second.getNonZeroCount()); |
|
|
|
|
|
|
|
ASSERT_NO_THROW(statesWithProbability01 = storm::utility::graph::performProb01Max(*model->as<storm::models::symbolic::Mdp<storm::dd::DdType::CUDD>>(), model->getReachableStates(), model->getStates("elected"))); |
|
|
|
EXPECT_EQ(0, statesWithProbability01.first.getNonZeroCount()); |
|
|
|
EXPECT_EQ(364, statesWithProbability01.second.getNonZeroCount()); |
|
|
|
EXPECT_EQ(0ul, statesWithProbability01.first.getNonZeroCount()); |
|
|
|
EXPECT_EQ(364ul, statesWithProbability01.second.getNonZeroCount()); |
|
|
|
|
|
|
|
program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/coin2-2.nm"); |
|
|
|
model = storm::builder::DdPrismModelBuilder<storm::dd::DdType::CUDD>::translateProgram(program); |
|
|
@ -54,20 +54,20 @@ TEST(GraphTest, SymbolicProb01MinMax) { |
|
|
|
ASSERT_TRUE(model->getType() == storm::models::ModelType::Mdp); |
|
|
|
|
|
|
|
ASSERT_NO_THROW(statesWithProbability01 = storm::utility::graph::performProb01Min(*model->as<storm::models::symbolic::Mdp<storm::dd::DdType::CUDD>>(), model->getReachableStates(), model->getStates("all_coins_equal_0"))); |
|
|
|
EXPECT_EQ(77, statesWithProbability01.first.getNonZeroCount()); |
|
|
|
EXPECT_EQ(149, statesWithProbability01.second.getNonZeroCount()); |
|
|
|
EXPECT_EQ(77ul, statesWithProbability01.first.getNonZeroCount()); |
|
|
|
EXPECT_EQ(149ul, statesWithProbability01.second.getNonZeroCount()); |
|
|
|
|
|
|
|
ASSERT_NO_THROW(statesWithProbability01 = storm::utility::graph::performProb01Max(*model->as<storm::models::symbolic::Mdp<storm::dd::DdType::CUDD>>(), model->getReachableStates(), model->getStates("all_coins_equal_0"))); |
|
|
|
EXPECT_EQ(74, statesWithProbability01.first.getNonZeroCount()); |
|
|
|
EXPECT_EQ(198, statesWithProbability01.second.getNonZeroCount()); |
|
|
|
EXPECT_EQ(74ul, statesWithProbability01.first.getNonZeroCount()); |
|
|
|
EXPECT_EQ(198ul, statesWithProbability01.second.getNonZeroCount()); |
|
|
|
|
|
|
|
ASSERT_NO_THROW(statesWithProbability01 = storm::utility::graph::performProb01Min(*model->as<storm::models::symbolic::Mdp<storm::dd::DdType::CUDD>>(), model->getReachableStates(), model->getStates("all_coins_equal_1"))); |
|
|
|
EXPECT_EQ(94, statesWithProbability01.first.getNonZeroCount()); |
|
|
|
EXPECT_EQ(33, statesWithProbability01.second.getNonZeroCount()); |
|
|
|
EXPECT_EQ(94ul, statesWithProbability01.first.getNonZeroCount()); |
|
|
|
EXPECT_EQ(33ul, statesWithProbability01.second.getNonZeroCount()); |
|
|
|
|
|
|
|
ASSERT_NO_THROW(statesWithProbability01 = storm::utility::graph::performProb01Max(*model->as<storm::models::symbolic::Mdp<storm::dd::DdType::CUDD>>(), model->getReachableStates(), model->getStates("all_coins_equal_1"))); |
|
|
|
EXPECT_EQ(83, statesWithProbability01.first.getNonZeroCount()); |
|
|
|
EXPECT_EQ(35, statesWithProbability01.second.getNonZeroCount()); |
|
|
|
EXPECT_EQ(83ul, statesWithProbability01.first.getNonZeroCount()); |
|
|
|
EXPECT_EQ(35ul, statesWithProbability01.second.getNonZeroCount()); |
|
|
|
|
|
|
|
program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/csma2-2.nm"); |
|
|
|
model = storm::builder::DdPrismModelBuilder<storm::dd::DdType::CUDD>::translateProgram(program); |
|
|
@ -75,12 +75,12 @@ TEST(GraphTest, SymbolicProb01MinMax) { |
|
|
|
ASSERT_TRUE(model->getType() == storm::models::ModelType::Mdp); |
|
|
|
|
|
|
|
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()); |
|
|
|
EXPECT_EQ(993ul, statesWithProbability01.first.getNonZeroCount()); |
|
|
|
EXPECT_EQ(16ul, statesWithProbability01.second.getNonZeroCount()); |
|
|
|
|
|
|
|
ASSERT_NO_THROW(statesWithProbability01 = storm::utility::graph::performProb01Max(*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()); |
|
|
|
EXPECT_EQ(993ul, statesWithProbability01.first.getNonZeroCount()); |
|
|
|
EXPECT_EQ(16ul, statesWithProbability01.second.getNonZeroCount()); |
|
|
|
} |
|
|
|
|
|
|
|
TEST(GraphTest, ExplicitProb01) { |
|
|
@ -92,16 +92,16 @@ TEST(GraphTest, ExplicitProb01) { |
|
|
|
std::pair<storm::storage::BitVector, storm::storage::BitVector> statesWithProbability01; |
|
|
|
|
|
|
|
ASSERT_NO_THROW(statesWithProbability01 = storm::utility::graph::performProb01(*model->as<storm::models::sparse::Dtmc<double>>(), storm::storage::BitVector(model->getNumberOfStates(), true), model->getStates("observe0Greater1"))); |
|
|
|
EXPECT_EQ(4409, statesWithProbability01.first.getNumberOfSetBits()); |
|
|
|
EXPECT_EQ(1316, statesWithProbability01.second.getNumberOfSetBits()); |
|
|
|
EXPECT_EQ(4409ul, statesWithProbability01.first.getNumberOfSetBits()); |
|
|
|
EXPECT_EQ(1316ul, statesWithProbability01.second.getNumberOfSetBits()); |
|
|
|
|
|
|
|
ASSERT_NO_THROW(statesWithProbability01 = storm::utility::graph::performProb01(*model->as<storm::models::sparse::Dtmc<double>>(), storm::storage::BitVector(model->getNumberOfStates(), true), model->getStates("observeIGreater1"))); |
|
|
|
EXPECT_EQ(1091, statesWithProbability01.first.getNumberOfSetBits()); |
|
|
|
EXPECT_EQ(4802, statesWithProbability01.second.getNumberOfSetBits()); |
|
|
|
EXPECT_EQ(1091ul, statesWithProbability01.first.getNumberOfSetBits()); |
|
|
|
EXPECT_EQ(4802ul, statesWithProbability01.second.getNumberOfSetBits()); |
|
|
|
|
|
|
|
ASSERT_NO_THROW(statesWithProbability01 = storm::utility::graph::performProb01(*model->as<storm::models::sparse::Dtmc<double>>(), storm::storage::BitVector(model->getNumberOfStates(), true), model->getStates("observeOnlyTrueSender"))); |
|
|
|
EXPECT_EQ(5829, statesWithProbability01.first.getNumberOfSetBits()); |
|
|
|
EXPECT_EQ(1032, statesWithProbability01.second.getNumberOfSetBits()); |
|
|
|
EXPECT_EQ(5829ul, statesWithProbability01.first.getNumberOfSetBits()); |
|
|
|
EXPECT_EQ(1032ul, statesWithProbability01.second.getNumberOfSetBits()); |
|
|
|
} |
|
|
|
|
|
|
|
TEST(GraphTest, ExplicitProb01MinMax) { |
|
|
@ -113,12 +113,12 @@ TEST(GraphTest, ExplicitProb01MinMax) { |
|
|
|
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()); |
|
|
|
EXPECT_EQ(0ul, statesWithProbability01.first.getNumberOfSetBits()); |
|
|
|
EXPECT_EQ(364ul, 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()); |
|
|
|
EXPECT_EQ(0ul, statesWithProbability01.first.getNumberOfSetBits()); |
|
|
|
EXPECT_EQ(364ul, 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); |
|
|
@ -126,20 +126,20 @@ TEST(GraphTest, ExplicitProb01MinMax) { |
|
|
|
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()); |
|
|
|
EXPECT_EQ(77ul, statesWithProbability01.first.getNumberOfSetBits()); |
|
|
|
EXPECT_EQ(149ul, 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()); |
|
|
|
EXPECT_EQ(74ul, statesWithProbability01.first.getNumberOfSetBits()); |
|
|
|
EXPECT_EQ(198ul, 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()); |
|
|
|
EXPECT_EQ(94ul, statesWithProbability01.first.getNumberOfSetBits()); |
|
|
|
EXPECT_EQ(33ul, 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()); |
|
|
|
EXPECT_EQ(83ul, statesWithProbability01.first.getNumberOfSetBits()); |
|
|
|
EXPECT_EQ(35ul, 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); |
|
|
@ -147,10 +147,10 @@ TEST(GraphTest, ExplicitProb01MinMax) { |
|
|
|
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()); |
|
|
|
EXPECT_EQ(993ul, statesWithProbability01.first.getNumberOfSetBits()); |
|
|
|
EXPECT_EQ(16ul, 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()); |
|
|
|
EXPECT_EQ(993ul, statesWithProbability01.first.getNumberOfSetBits()); |
|
|
|
EXPECT_EQ(16ul, statesWithProbability01.second.getNumberOfSetBits()); |
|
|
|
} |