You can not select more than 25 topics Topics must start with a letter or number, can include dashes ('-') and can be up to 35 characters long.

647 lines
50 KiB

  1. #include "gtest/gtest.h"
  2. #include "storm-config.h"
  3. #include "src/parser/PrismParser.h"
  4. #include "src/models/symbolic/Dtmc.h"
  5. #include "src/models/symbolic/Mdp.h"
  6. #include "src/models/symbolic/StandardRewardModel.h"
  7. #include "src/models/sparse/Dtmc.h"
  8. #include "src/models/sparse/Mdp.h"
  9. #include "src/models/sparse/StandardRewardModel.h"
  10. #include "src/builder/DdPrismModelBuilder.h"
  11. #include "src/builder/ExplicitModelBuilder.h"
  12. #include "src/utility/graph.h"
  13. #include "src/storage/dd/Add.h"
  14. #include "src/storage/dd/Bdd.h"
  15. #include "src/storage/dd/DdManager.h"
  16. TEST(GraphTest, SymbolicProb01_Cudd) {
  17. storm::prism::Program program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/crowds-5-5.pm");
  18. std::shared_ptr<storm::models::symbolic::Model<storm::dd::DdType::CUDD>> model = storm::builder::DdPrismModelBuilder<storm::dd::DdType::CUDD>().build(program);
  19. ASSERT_TRUE(model->getType() == storm::models::ModelType::Dtmc);
  20. {
  21. // This block is necessary, so the BDDs get disposed before the manager (contained in the model).
  22. std::pair<storm::dd::Bdd<storm::dd::DdType::CUDD>, storm::dd::Bdd<storm::dd::DdType::CUDD>> statesWithProbability01;
  23. ASSERT_NO_THROW(statesWithProbability01 = storm::utility::graph::performProb01(*model->as<storm::models::symbolic::Dtmc<storm::dd::DdType::CUDD>>(), model->getReachableStates(), model->getStates("observe0Greater1")));
  24. EXPECT_EQ(4409ul, statesWithProbability01.first.getNonZeroCount());
  25. EXPECT_EQ(1316ul, statesWithProbability01.second.getNonZeroCount());
  26. ASSERT_NO_THROW(statesWithProbability01 = storm::utility::graph::performProb01(*model->as<storm::models::symbolic::Dtmc<storm::dd::DdType::CUDD>>(), model->getReachableStates(), model->getStates("observeIGreater1")));
  27. EXPECT_EQ(1091ul, statesWithProbability01.first.getNonZeroCount());
  28. EXPECT_EQ(4802ul, statesWithProbability01.second.getNonZeroCount());
  29. ASSERT_NO_THROW(statesWithProbability01 = storm::utility::graph::performProb01(*model->as<storm::models::symbolic::Dtmc<storm::dd::DdType::CUDD>>(), model->getReachableStates(), model->getStates("observeOnlyTrueSender")));
  30. EXPECT_EQ(5829ul, statesWithProbability01.first.getNonZeroCount());
  31. EXPECT_EQ(1032ul, statesWithProbability01.second.getNonZeroCount());
  32. }
  33. }
  34. TEST(GraphTest, SymbolicProb01_Sylvan) {
  35. storm::prism::Program program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/crowds-5-5.pm");
  36. std::shared_ptr<storm::models::symbolic::Model<storm::dd::DdType::Sylvan>> model = storm::builder::DdPrismModelBuilder<storm::dd::DdType::Sylvan>().build(program);
  37. ASSERT_TRUE(model->getType() == storm::models::ModelType::Dtmc);
  38. {
  39. // This block is necessary, so the BDDs get disposed before the manager (contained in the model).
  40. std::pair<storm::dd::Bdd<storm::dd::DdType::Sylvan>, storm::dd::Bdd<storm::dd::DdType::Sylvan>> statesWithProbability01;
  41. ASSERT_NO_THROW(statesWithProbability01 = storm::utility::graph::performProb01(*model->as<storm::models::symbolic::Dtmc<storm::dd::DdType::Sylvan>>(), model->getReachableStates(), model->getStates("observe0Greater1")));
  42. EXPECT_EQ(4409ul, statesWithProbability01.first.getNonZeroCount());
  43. EXPECT_EQ(1316ul, statesWithProbability01.second.getNonZeroCount());
  44. ASSERT_NO_THROW(statesWithProbability01 = storm::utility::graph::performProb01(*model->as<storm::models::symbolic::Dtmc<storm::dd::DdType::Sylvan>>(), model->getReachableStates(), model->getStates("observeIGreater1")));
  45. EXPECT_EQ(1091ul, statesWithProbability01.first.getNonZeroCount());
  46. EXPECT_EQ(4802ul, statesWithProbability01.second.getNonZeroCount());
  47. ASSERT_NO_THROW(statesWithProbability01 = storm::utility::graph::performProb01(*model->as<storm::models::symbolic::Dtmc<storm::dd::DdType::Sylvan>>(), model->getReachableStates(), model->getStates("observeOnlyTrueSender")));
  48. EXPECT_EQ(5829ul, statesWithProbability01.first.getNonZeroCount());
  49. EXPECT_EQ(1032ul, statesWithProbability01.second.getNonZeroCount());
  50. }
  51. }
  52. TEST(GraphTest, SymbolicProb01MinMax_Cudd) {
  53. storm::prism::Program program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/leader3.nm");
  54. std::shared_ptr<storm::models::symbolic::Model<storm::dd::DdType::CUDD>> model = storm::builder::DdPrismModelBuilder<storm::dd::DdType::CUDD>().build(program);
  55. ASSERT_TRUE(model->getType() == storm::models::ModelType::Mdp);
  56. {
  57. // This block is necessary, so the BDDs get disposed before the manager (contained in the model).
  58. std::pair<storm::dd::Bdd<storm::dd::DdType::CUDD>, storm::dd::Bdd<storm::dd::DdType::CUDD>> statesWithProbability01;
  59. ASSERT_NO_THROW(statesWithProbability01 = storm::utility::graph::performProb01Min(*model->as<storm::models::symbolic::Mdp<storm::dd::DdType::CUDD>>(), model->getReachableStates(), model->getStates("elected")));
  60. EXPECT_EQ(0ul, statesWithProbability01.first.getNonZeroCount());
  61. EXPECT_EQ(364ul, statesWithProbability01.second.getNonZeroCount());
  62. ASSERT_NO_THROW(statesWithProbability01 = storm::utility::graph::performProb01Max(*model->as<storm::models::symbolic::Mdp<storm::dd::DdType::CUDD>>(), model->getReachableStates(), model->getStates("elected")));
  63. EXPECT_EQ(0ul, statesWithProbability01.first.getNonZeroCount());
  64. EXPECT_EQ(364ul, statesWithProbability01.second.getNonZeroCount());
  65. }
  66. program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/coin2-2.nm");
  67. model = storm::builder::DdPrismModelBuilder<storm::dd::DdType::CUDD>().build(program);
  68. ASSERT_TRUE(model->getType() == storm::models::ModelType::Mdp);
  69. {
  70. // This block is necessary, so the BDDs get disposed before the manager (contained in the model).
  71. std::pair<storm::dd::Bdd<storm::dd::DdType::CUDD>, storm::dd::Bdd<storm::dd::DdType::CUDD>> statesWithProbability01;
  72. 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")));
  73. EXPECT_EQ(77ul, statesWithProbability01.first.getNonZeroCount());
  74. EXPECT_EQ(149ul, statesWithProbability01.second.getNonZeroCount());
  75. 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")));
  76. EXPECT_EQ(74ul, statesWithProbability01.first.getNonZeroCount());
  77. EXPECT_EQ(198ul, statesWithProbability01.second.getNonZeroCount());
  78. 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")));
  79. EXPECT_EQ(94ul, statesWithProbability01.first.getNonZeroCount());
  80. EXPECT_EQ(33ul, statesWithProbability01.second.getNonZeroCount());
  81. 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")));
  82. EXPECT_EQ(83ul, statesWithProbability01.first.getNonZeroCount());
  83. EXPECT_EQ(35ul, statesWithProbability01.second.getNonZeroCount());
  84. }
  85. program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/csma2-2.nm");
  86. model = storm::builder::DdPrismModelBuilder<storm::dd::DdType::CUDD>().build(program);
  87. ASSERT_TRUE(model->getType() == storm::models::ModelType::Mdp);
  88. {
  89. // This block is necessary, so the BDDs get disposed before the manager (contained in the model).
  90. std::pair<storm::dd::Bdd<storm::dd::DdType::CUDD>, storm::dd::Bdd<storm::dd::DdType::CUDD>> statesWithProbability01;
  91. 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")));
  92. EXPECT_EQ(993ul, statesWithProbability01.first.getNonZeroCount());
  93. EXPECT_EQ(16ul, statesWithProbability01.second.getNonZeroCount());
  94. 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")));
  95. EXPECT_EQ(993ul, statesWithProbability01.first.getNonZeroCount());
  96. EXPECT_EQ(16ul, statesWithProbability01.second.getNonZeroCount());
  97. }
  98. }
  99. TEST(GraphTest, SymbolicProb01MinMax_Sylvan) {
  100. storm::prism::Program program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/leader3.nm");
  101. std::shared_ptr<storm::models::symbolic::Model<storm::dd::DdType::Sylvan>> model = storm::builder::DdPrismModelBuilder<storm::dd::DdType::Sylvan>().build(program);
  102. ASSERT_TRUE(model->getType() == storm::models::ModelType::Mdp);
  103. {
  104. // This block is necessary, so the BDDs get disposed before the manager (contained in the model).
  105. std::pair<storm::dd::Bdd<storm::dd::DdType::Sylvan>, storm::dd::Bdd<storm::dd::DdType::Sylvan>> statesWithProbability01;
  106. ASSERT_NO_THROW(statesWithProbability01 = storm::utility::graph::performProb01Min(*model->as<storm::models::symbolic::Mdp<storm::dd::DdType::Sylvan>>(), model->getReachableStates(), model->getStates("elected")));
  107. EXPECT_EQ(0ul, statesWithProbability01.first.getNonZeroCount());
  108. EXPECT_EQ(364ul, statesWithProbability01.second.getNonZeroCount());
  109. ASSERT_NO_THROW(statesWithProbability01 = storm::utility::graph::performProb01Max(*model->as<storm::models::symbolic::Mdp<storm::dd::DdType::Sylvan>>(), model->getReachableStates(), model->getStates("elected")));
  110. EXPECT_EQ(0ul, statesWithProbability01.first.getNonZeroCount());
  111. EXPECT_EQ(364ul, statesWithProbability01.second.getNonZeroCount());
  112. }
  113. program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/coin2-2.nm");
  114. model = storm::builder::DdPrismModelBuilder<storm::dd::DdType::Sylvan>().build(program);
  115. ASSERT_TRUE(model->getType() == storm::models::ModelType::Mdp);
  116. {
  117. // This block is necessary, so the BDDs get disposed before the manager (contained in the model).
  118. std::pair<storm::dd::Bdd<storm::dd::DdType::Sylvan>, storm::dd::Bdd<storm::dd::DdType::Sylvan>> statesWithProbability01;
  119. ASSERT_NO_THROW(statesWithProbability01 = storm::utility::graph::performProb01Min(*model->as<storm::models::symbolic::Mdp<storm::dd::DdType::Sylvan>>(), model->getReachableStates(), model->getStates("all_coins_equal_0")));
  120. EXPECT_EQ(77ul, statesWithProbability01.first.getNonZeroCount());
  121. EXPECT_EQ(149ul, statesWithProbability01.second.getNonZeroCount());
  122. ASSERT_NO_THROW(statesWithProbability01 = storm::utility::graph::performProb01Max(*model->as<storm::models::symbolic::Mdp<storm::dd::DdType::Sylvan>>(), model->getReachableStates(), model->getStates("all_coins_equal_0")));
  123. EXPECT_EQ(74ul, statesWithProbability01.first.getNonZeroCount());
  124. EXPECT_EQ(198ul, statesWithProbability01.second.getNonZeroCount());
  125. ASSERT_NO_THROW(statesWithProbability01 = storm::utility::graph::performProb01Min(*model->as<storm::models::symbolic::Mdp<storm::dd::DdType::Sylvan>>(), model->getReachableStates(), model->getStates("all_coins_equal_1")));
  126. EXPECT_EQ(94ul, statesWithProbability01.first.getNonZeroCount());
  127. EXPECT_EQ(33ul, statesWithProbability01.second.getNonZeroCount());
  128. ASSERT_NO_THROW(statesWithProbability01 = storm::utility::graph::performProb01Max(*model->as<storm::models::symbolic::Mdp<storm::dd::DdType::Sylvan>>(), model->getReachableStates(), model->getStates("all_coins_equal_1")));
  129. EXPECT_EQ(83ul, statesWithProbability01.first.getNonZeroCount());
  130. EXPECT_EQ(35ul, statesWithProbability01.second.getNonZeroCount());
  131. }
  132. program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/csma2-2.nm");
  133. model = storm::builder::DdPrismModelBuilder<storm::dd::DdType::Sylvan>().build(program);
  134. ASSERT_TRUE(model->getType() == storm::models::ModelType::Mdp);
  135. {
  136. // This block is necessary, so the BDDs get disposed before the manager (contained in the model).
  137. std::pair<storm::dd::Bdd<storm::dd::DdType::Sylvan>, storm::dd::Bdd<storm::dd::DdType::Sylvan>> statesWithProbability01;
  138. ASSERT_NO_THROW(statesWithProbability01 = storm::utility::graph::performProb01Min(*model->as<storm::models::symbolic::Mdp<storm::dd::DdType::Sylvan>>(), model->getReachableStates(), model->getStates("collision_max_backoff")));
  139. EXPECT_EQ(993ul, statesWithProbability01.first.getNonZeroCount());
  140. EXPECT_EQ(16ul, statesWithProbability01.second.getNonZeroCount());
  141. ASSERT_NO_THROW(statesWithProbability01 = storm::utility::graph::performProb01Max(*model->as<storm::models::symbolic::Mdp<storm::dd::DdType::Sylvan>>(), model->getReachableStates(), model->getStates("collision_max_backoff")));
  142. EXPECT_EQ(993ul, statesWithProbability01.first.getNonZeroCount());
  143. EXPECT_EQ(16ul, statesWithProbability01.second.getNonZeroCount());
  144. }
  145. }
  146. #ifdef STORM_HAVE_MSAT
  147. #include "src/abstraction/prism/AbstractProgram.h"
  148. #include "src/storage/expressions/Expression.h"
  149. #include "src/utility/solver.h"
  150. TEST(GraphTest, SymbolicProb01StochasticGameDieSmall) {
  151. storm::prism::Program program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/die.pm");
  152. std::vector<storm::expressions::Expression> initialPredicates;
  153. storm::expressions::ExpressionManager& manager = program.getManager();
  154. initialPredicates.push_back(manager.getVariableExpression("s") < manager.integer(3));
  155. storm::abstraction::prism::AbstractProgram<storm::dd::DdType::CUDD, double> abstractProgram(program, initialPredicates, std::make_shared<storm::utility::solver::MathsatSmtSolverFactory>(), false);
  156. storm::abstraction::MenuGame<storm::dd::DdType::CUDD, double> game = abstractProgram.getAbstractGame();
  157. // The target states are those states where !(s < 3).
  158. storm::dd::Bdd<storm::dd::DdType::CUDD> targetStates = game.getStates(initialPredicates[0], true);
  159. storm::utility::graph::GameProb01Result<storm::dd::DdType::CUDD> result = storm::utility::graph::performProb0(game, game.getQualitativeTransitionMatrix(), game.getReachableStates(), targetStates, storm::OptimizationDirection::Minimize, storm::OptimizationDirection::Minimize, true, true);
  160. EXPECT_EQ(2, result.getPlayer1States().getNonZeroCount());
  161. EXPECT_TRUE(result.hasPlayer1Strategy());
  162. EXPECT_TRUE(result.hasPlayer2Strategy());
  163. result = storm::utility::graph::performProb1(game, game.getQualitativeTransitionMatrix(), game.getReachableStates(), targetStates, storm::OptimizationDirection::Minimize, storm::OptimizationDirection::Minimize);
  164. EXPECT_EQ(2, result.getPlayer1States().getNonZeroCount());
  165. result = storm::utility::graph::performProb0(game, game.getQualitativeTransitionMatrix(), game.getReachableStates(), targetStates, storm::OptimizationDirection::Minimize, storm::OptimizationDirection::Maximize);
  166. EXPECT_EQ(2, result.getPlayer1States().getNonZeroCount());
  167. result = storm::utility::graph::performProb0(game, game.getQualitativeTransitionMatrix(), game.getReachableStates(), targetStates, storm::OptimizationDirection::Minimize, storm::OptimizationDirection::Maximize);
  168. EXPECT_EQ(2, result.getPlayer1States().getNonZeroCount());
  169. result = storm::utility::graph::performProb0(game, game.getQualitativeTransitionMatrix(), game.getReachableStates(), targetStates, storm::OptimizationDirection::Maximize, storm::OptimizationDirection::Minimize);
  170. EXPECT_EQ(2, result.getPlayer1States().getNonZeroCount());
  171. result = storm::utility::graph::performProb1(game, game.getQualitativeTransitionMatrix(), game.getReachableStates(), targetStates, storm::OptimizationDirection::Maximize, storm::OptimizationDirection::Minimize);
  172. EXPECT_EQ(2, result.getPlayer1States().getNonZeroCount());
  173. result = storm::utility::graph::performProb0(game, game.getQualitativeTransitionMatrix(), game.getReachableStates(), targetStates, storm::OptimizationDirection::Maximize, storm::OptimizationDirection::Maximize);
  174. EXPECT_EQ(1, result.getPlayer1States().getNonZeroCount());
  175. result = storm::utility::graph::performProb1(game, game.getQualitativeTransitionMatrix(), game.getReachableStates(), targetStates, storm::OptimizationDirection::Maximize, storm::OptimizationDirection::Maximize, true, true);
  176. EXPECT_EQ(3, result.getPlayer1States().getNonZeroCount());
  177. EXPECT_TRUE(result.hasPlayer1Strategy());
  178. EXPECT_TRUE(result.hasPlayer2Strategy());
  179. abstractProgram.refine({manager.getVariableExpression("s") < manager.integer(2)});
  180. game = abstractProgram.getAbstractGame();
  181. // We need to create a new BDD for the target states since the reachable states might have changed.
  182. targetStates = game.getStates(initialPredicates[0], true);
  183. result = storm::utility::graph::performProb0(game, game.getQualitativeTransitionMatrix(), game.getReachableStates(), targetStates, storm::OptimizationDirection::Minimize, storm::OptimizationDirection::Minimize, true, true);
  184. EXPECT_EQ(2, result.getPlayer1States().getNonZeroCount());
  185. ASSERT_TRUE(result.hasPlayer1Strategy());
  186. ASSERT_TRUE(result.hasPlayer2Strategy());
  187. // Check the validity of the strategies. Start by checking whether only prob0 states have a strategy.
  188. storm::dd::Bdd<storm::dd::DdType::CUDD> nonProb0StatesWithStrategy = !result.getPlayer1States() && result.player1Strategy.get();
  189. EXPECT_TRUE(nonProb0StatesWithStrategy.isZero());
  190. // Proceed by checking whether they select exactly one action in each state.
  191. storm::dd::Add<storm::dd::DdType::CUDD, double> stateDistributionsUnderStrategies = (game.getTransitionMatrix() * result.player1Strategy.get().template toAdd<double>() * result.player2Strategy.get().template toAdd<double>()).sumAbstract(game.getColumnVariables());
  192. EXPECT_EQ(2, stateDistributionsUnderStrategies.getNonZeroCount());
  193. // Check that the number of distributions per state is one (or zero in the case where there are no prob0 states).
  194. storm::dd::Add<storm::dd::DdType::CUDD> stateDistributionCount = stateDistributionsUnderStrategies.sumAbstract(game.getNondeterminismVariables());
  195. EXPECT_EQ(1, stateDistributionCount.getMax());
  196. result = storm::utility::graph::performProb1(game, game.getQualitativeTransitionMatrix(), game.getReachableStates(), targetStates, storm::OptimizationDirection::Minimize, storm::OptimizationDirection::Minimize);
  197. EXPECT_EQ(3, result.getPlayer1States().getNonZeroCount());
  198. result = storm::utility::graph::performProb0(game, game.getQualitativeTransitionMatrix(), game.getReachableStates(), targetStates, storm::OptimizationDirection::Minimize, storm::OptimizationDirection::Maximize);
  199. EXPECT_EQ(1, result.getPlayer1States().getNonZeroCount());
  200. result = storm::utility::graph::performProb1(game, game.getQualitativeTransitionMatrix(), game.getReachableStates(), targetStates, storm::OptimizationDirection::Minimize, storm::OptimizationDirection::Maximize);
  201. EXPECT_EQ(4, result.getPlayer1States().getNonZeroCount());
  202. result = storm::utility::graph::performProb0(game, game.getQualitativeTransitionMatrix(), game.getReachableStates(), targetStates, storm::OptimizationDirection::Maximize, storm::OptimizationDirection::Minimize);
  203. EXPECT_EQ(2, result.getPlayer1States().getNonZeroCount());
  204. result = storm::utility::graph::performProb1(game, game.getQualitativeTransitionMatrix(), game.getReachableStates(), targetStates, storm::OptimizationDirection::Maximize, storm::OptimizationDirection::Minimize);
  205. EXPECT_EQ(3, result.getPlayer1States().getNonZeroCount());
  206. result = storm::utility::graph::performProb0(game, game.getQualitativeTransitionMatrix(), game.getReachableStates(), targetStates, storm::OptimizationDirection::Maximize, storm::OptimizationDirection::Maximize);
  207. EXPECT_EQ(1, result.getPlayer1States().getNonZeroCount());
  208. result = storm::utility::graph::performProb1(game, game.getQualitativeTransitionMatrix(), game.getReachableStates(), targetStates, storm::OptimizationDirection::Maximize, storm::OptimizationDirection::Maximize, true, true);
  209. EXPECT_EQ(4, result.getPlayer1States().getNonZeroCount());
  210. EXPECT_TRUE(result.hasPlayer1Strategy());
  211. EXPECT_TRUE(result.hasPlayer2Strategy());
  212. // Check the validity of the strategies. Start by checking whether only prob1 states have a strategy.
  213. storm::dd::Bdd<storm::dd::DdType::CUDD> nonProb1StatesWithStrategy = !result.getPlayer1States() && result.player1Strategy.get();
  214. EXPECT_TRUE(nonProb1StatesWithStrategy.isZero());
  215. // Proceed by checking whether they select exactly one action in each state.
  216. stateDistributionsUnderStrategies = (game.getTransitionMatrix() * result.player1Strategy.get().template toAdd<double>() * result.player2Strategy.get().template toAdd<double>()).sumAbstract(game.getColumnVariables());
  217. EXPECT_EQ(4, stateDistributionsUnderStrategies.getNonZeroCount());
  218. // Check that the number of distributions per state is one (or zero in the case where there are no prob1 states).
  219. stateDistributionCount = stateDistributionsUnderStrategies.sumAbstract(game.getNondeterminismVariables());
  220. EXPECT_EQ(1, stateDistributionCount.getMax());
  221. }
  222. TEST(GraphTest, SymbolicProb01StochasticGameTwoDice) {
  223. storm::prism::Program program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/two_dice.nm");
  224. program = program.substituteConstants();
  225. program = program.flattenModules(std::make_unique<storm::utility::solver::MathsatSmtSolverFactory>());
  226. std::vector<storm::expressions::Expression> initialPredicates;
  227. storm::expressions::ExpressionManager& manager = program.getManager();
  228. initialPredicates.push_back(manager.getVariableExpression("s1") == manager.integer(0));
  229. initialPredicates.push_back(manager.getVariableExpression("s1") == manager.integer(1));
  230. initialPredicates.push_back(manager.getVariableExpression("s1") == manager.integer(2));
  231. initialPredicates.push_back(manager.getVariableExpression("s1") == manager.integer(3));
  232. initialPredicates.push_back(manager.getVariableExpression("s1") == manager.integer(4));
  233. initialPredicates.push_back(manager.getVariableExpression("s1") == manager.integer(5));
  234. initialPredicates.push_back(manager.getVariableExpression("s1") == manager.integer(6));
  235. initialPredicates.push_back(manager.getVariableExpression("s1") == manager.integer(7));
  236. initialPredicates.push_back(manager.getVariableExpression("d1") == manager.integer(0));
  237. initialPredicates.push_back(manager.getVariableExpression("d1") == manager.integer(1));
  238. initialPredicates.push_back(manager.getVariableExpression("d1") == manager.integer(2));
  239. initialPredicates.push_back(manager.getVariableExpression("d1") == manager.integer(3));
  240. initialPredicates.push_back(manager.getVariableExpression("d1") == manager.integer(4));
  241. initialPredicates.push_back(manager.getVariableExpression("d1") == manager.integer(5));
  242. initialPredicates.push_back(manager.getVariableExpression("d1") == manager.integer(6));
  243. initialPredicates.push_back(manager.getVariableExpression("s2") == manager.integer(0));
  244. initialPredicates.push_back(manager.getVariableExpression("s2") == manager.integer(1));
  245. initialPredicates.push_back(manager.getVariableExpression("s2") == manager.integer(2));
  246. initialPredicates.push_back(manager.getVariableExpression("s2") == manager.integer(3));
  247. initialPredicates.push_back(manager.getVariableExpression("s2") == manager.integer(4));
  248. initialPredicates.push_back(manager.getVariableExpression("s2") == manager.integer(5));
  249. initialPredicates.push_back(manager.getVariableExpression("s2") == manager.integer(6));
  250. initialPredicates.push_back(manager.getVariableExpression("s2") == manager.integer(7));
  251. initialPredicates.push_back(manager.getVariableExpression("d2") == manager.integer(0));
  252. initialPredicates.push_back(manager.getVariableExpression("d2") == manager.integer(1));
  253. initialPredicates.push_back(manager.getVariableExpression("d2") == manager.integer(2));
  254. initialPredicates.push_back(manager.getVariableExpression("d2") == manager.integer(3));
  255. initialPredicates.push_back(manager.getVariableExpression("d2") == manager.integer(4));
  256. initialPredicates.push_back(manager.getVariableExpression("d2") == manager.integer(5));
  257. initialPredicates.push_back(manager.getVariableExpression("d2") == manager.integer(6));
  258. storm::abstraction::prism::AbstractProgram<storm::dd::DdType::CUDD, double> abstractProgram(program, initialPredicates, std::make_shared<storm::utility::solver::MathsatSmtSolverFactory>(), false);
  259. storm::abstraction::MenuGame<storm::dd::DdType::CUDD, double> game = abstractProgram.getAbstractGame();
  260. // The target states are those states where s1 == 7 & s2 == 7 & d1 + d2 == 1.
  261. storm::dd::Bdd<storm::dd::DdType::CUDD> targetStates = game.getStates(initialPredicates[7], false) && game.getStates(initialPredicates[22], false) && game.getStates(initialPredicates[9], false) && game.getStates(initialPredicates[24], false);
  262. storm::utility::graph::GameProb01Result<storm::dd::DdType::CUDD> result = storm::utility::graph::performProb0(game, game.getQualitativeTransitionMatrix(), game.getReachableStates(), targetStates, storm::OptimizationDirection::Minimize, storm::OptimizationDirection::Minimize, true, true);
  263. EXPECT_EQ(153, result.getPlayer1States().getNonZeroCount());
  264. ASSERT_TRUE(result.hasPlayer1Strategy());
  265. ASSERT_TRUE(result.hasPlayer2Strategy());
  266. // Check the validity of the strategies. Start by checking whether only prob0 states have a strategy.
  267. storm::dd::Bdd<storm::dd::DdType::CUDD> nonProb0StatesWithStrategy = !result.getPlayer1States() && result.player1Strategy.get();
  268. EXPECT_TRUE(nonProb0StatesWithStrategy.isZero());
  269. // Proceed by checking whether they select exactly one exaction in each state.
  270. storm::dd::Add<storm::dd::DdType::CUDD, double> stateDistributionsUnderStrategies = (game.getTransitionMatrix() * result.player1Strategy.get().template toAdd<double>() * result.player2Strategy.get().template toAdd<double>()).sumAbstract(game.getColumnVariables());
  271. EXPECT_EQ(153, stateDistributionsUnderStrategies.getNonZeroCount());
  272. storm::dd::Add<storm::dd::DdType::CUDD> stateDistributionCount = stateDistributionsUnderStrategies.sumAbstract(game.getNondeterminismVariables());
  273. EXPECT_EQ(1, stateDistributionCount.getMax());
  274. result = storm::utility::graph::performProb1(game, game.getQualitativeTransitionMatrix(), game.getReachableStates(), targetStates, storm::OptimizationDirection::Minimize, storm::OptimizationDirection::Minimize);
  275. EXPECT_EQ(1, result.getPlayer1States().getNonZeroCount());
  276. result = storm::utility::graph::performProb0(game, game.getQualitativeTransitionMatrix(), game.getReachableStates(), targetStates, storm::OptimizationDirection::Minimize, storm::OptimizationDirection::Maximize);
  277. EXPECT_EQ(153, result.getPlayer1States().getNonZeroCount());
  278. result = storm::utility::graph::performProb1(game, game.getQualitativeTransitionMatrix(), game.getReachableStates(), targetStates, storm::OptimizationDirection::Minimize, storm::OptimizationDirection::Maximize);
  279. EXPECT_EQ(1, result.getPlayer1States().getNonZeroCount());
  280. result = storm::utility::graph::performProb0(game, game.getQualitativeTransitionMatrix(), game.getReachableStates(), targetStates, storm::OptimizationDirection::Maximize, storm::OptimizationDirection::Minimize);
  281. EXPECT_EQ(153, result.getPlayer1States().getNonZeroCount());
  282. result = storm::utility::graph::performProb1(game, game.getQualitativeTransitionMatrix(), game.getReachableStates(), targetStates, storm::OptimizationDirection::Maximize, storm::OptimizationDirection::Minimize);
  283. EXPECT_EQ(1, result.getPlayer1States().getNonZeroCount());
  284. result = storm::utility::graph::performProb0(game, game.getQualitativeTransitionMatrix(), game.getReachableStates(), targetStates, storm::OptimizationDirection::Maximize, storm::OptimizationDirection::Maximize);
  285. EXPECT_EQ(153, result.getPlayer1States().getNonZeroCount());
  286. result = storm::utility::graph::performProb1(game, game.getQualitativeTransitionMatrix(), game.getReachableStates(), targetStates, storm::OptimizationDirection::Maximize, storm::OptimizationDirection::Maximize, true, true);
  287. EXPECT_EQ(1, result.getPlayer1States().getNonZeroCount());
  288. EXPECT_TRUE(result.hasPlayer1Strategy());
  289. EXPECT_TRUE(result.hasPlayer2Strategy());
  290. // Check the validity of the strategies. Start by checking whether only prob1 states have a strategy.
  291. storm::dd::Bdd<storm::dd::DdType::CUDD> nonProb1StatesWithStrategy = !result.getPlayer1States() && result.player1Strategy.get();
  292. EXPECT_TRUE(nonProb1StatesWithStrategy.isZero());
  293. // Proceed by checking whether they select exactly one action in each state.
  294. stateDistributionsUnderStrategies = (game.getTransitionMatrix() * result.player1Strategy.get().template toAdd<double>() * result.player2Strategy.get().template toAdd<double>()).sumAbstract(game.getColumnVariables());
  295. EXPECT_EQ(1, stateDistributionsUnderStrategies.getNonZeroCount());
  296. // Check that the number of distributions per state is one (or zero in the case where there are no prob1 states).
  297. stateDistributionCount = stateDistributionsUnderStrategies.sumAbstract(game.getNondeterminismVariables());
  298. EXPECT_EQ(1, stateDistributionCount.getMax());
  299. }
  300. TEST(GraphTest, SymbolicProb01StochasticGameWlan) {
  301. storm::prism::Program program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/wlan0-2-4.nm");
  302. program = program.substituteConstants();
  303. program = program.flattenModules(std::make_unique<storm::utility::solver::MathsatSmtSolverFactory>());
  304. std::vector<storm::expressions::Expression> initialPredicates;
  305. storm::expressions::ExpressionManager& manager = program.getManager();
  306. initialPredicates.push_back(manager.getVariableExpression("col") == manager.integer(0));
  307. initialPredicates.push_back(manager.getVariableExpression("col") == manager.integer(1));
  308. initialPredicates.push_back(manager.getVariableExpression("col") == manager.integer(2));
  309. initialPredicates.push_back(manager.getVariableExpression("c1") == manager.integer(0));
  310. initialPredicates.push_back(manager.getVariableExpression("c1") == manager.integer(1));
  311. initialPredicates.push_back(manager.getVariableExpression("c1") == manager.integer(2));
  312. initialPredicates.push_back(manager.getVariableExpression("c2") == manager.integer(0));
  313. initialPredicates.push_back(manager.getVariableExpression("c2") == manager.integer(1));
  314. initialPredicates.push_back(manager.getVariableExpression("c2") == manager.integer(2));
  315. initialPredicates.push_back(manager.getVariableExpression("x1") == manager.integer(0));
  316. initialPredicates.push_back(manager.getVariableExpression("x1") == manager.integer(1));
  317. initialPredicates.push_back(manager.getVariableExpression("x1") == manager.integer(2));
  318. initialPredicates.push_back(manager.getVariableExpression("x1") == manager.integer(3));
  319. initialPredicates.push_back(manager.getVariableExpression("x1") == manager.integer(4));
  320. initialPredicates.push_back(manager.getVariableExpression("x1") == manager.integer(5));
  321. initialPredicates.push_back(manager.getVariableExpression("x1") == manager.integer(6));
  322. initialPredicates.push_back(manager.getVariableExpression("x1") == manager.integer(7));
  323. initialPredicates.push_back(manager.getVariableExpression("s1") == manager.integer(1));
  324. initialPredicates.push_back(manager.getVariableExpression("s1") == manager.integer(2));
  325. initialPredicates.push_back(manager.getVariableExpression("s1") == manager.integer(3));
  326. initialPredicates.push_back(manager.getVariableExpression("s1") == manager.integer(4));
  327. initialPredicates.push_back(manager.getVariableExpression("s1") == manager.integer(5));
  328. initialPredicates.push_back(manager.getVariableExpression("s1") == manager.integer(6));
  329. initialPredicates.push_back(manager.getVariableExpression("s1") == manager.integer(7));
  330. initialPredicates.push_back(manager.getVariableExpression("s1") == manager.integer(8));
  331. initialPredicates.push_back(manager.getVariableExpression("s1") == manager.integer(9));
  332. initialPredicates.push_back(manager.getVariableExpression("s1") == manager.integer(10));
  333. initialPredicates.push_back(manager.getVariableExpression("s1") == manager.integer(11));
  334. initialPredicates.push_back(manager.getVariableExpression("s1") == manager.integer(12));
  335. initialPredicates.push_back(manager.getVariableExpression("slot1") == manager.integer(0));
  336. initialPredicates.push_back(manager.getVariableExpression("slot1") == manager.integer(1));
  337. initialPredicates.push_back(manager.getVariableExpression("backoff1") == manager.integer(0));
  338. initialPredicates.push_back(manager.getVariableExpression("backoff1") == manager.integer(1));
  339. initialPredicates.push_back(manager.getVariableExpression("backoff1") == manager.integer(2));
  340. initialPredicates.push_back(manager.getVariableExpression("backoff1") == manager.integer(3));
  341. initialPredicates.push_back(manager.getVariableExpression("backoff1") == manager.integer(4));
  342. initialPredicates.push_back(manager.getVariableExpression("backoff1") == manager.integer(5));
  343. initialPredicates.push_back(manager.getVariableExpression("backoff1") == manager.integer(6));
  344. initialPredicates.push_back(manager.getVariableExpression("backoff1") == manager.integer(7));
  345. initialPredicates.push_back(manager.getVariableExpression("backoff1") == manager.integer(8));
  346. initialPredicates.push_back(manager.getVariableExpression("backoff1") == manager.integer(9));
  347. initialPredicates.push_back(manager.getVariableExpression("backoff1") == manager.integer(10));
  348. initialPredicates.push_back(manager.getVariableExpression("backoff1") == manager.integer(11));
  349. initialPredicates.push_back(manager.getVariableExpression("backoff1") == manager.integer(12));
  350. initialPredicates.push_back(manager.getVariableExpression("backoff1") == manager.integer(13));
  351. initialPredicates.push_back(manager.getVariableExpression("backoff1") == manager.integer(14));
  352. initialPredicates.push_back(manager.getVariableExpression("backoff1") == manager.integer(15));
  353. initialPredicates.push_back(manager.getVariableExpression("bc1") == manager.integer(0));
  354. initialPredicates.push_back(manager.getVariableExpression("bc1") == manager.integer(1));
  355. initialPredicates.push_back(manager.getVariableExpression("x2") == manager.integer(0));
  356. initialPredicates.push_back(manager.getVariableExpression("x2") == manager.integer(1));
  357. initialPredicates.push_back(manager.getVariableExpression("x2") == manager.integer(2));
  358. initialPredicates.push_back(manager.getVariableExpression("x2") == manager.integer(3));
  359. initialPredicates.push_back(manager.getVariableExpression("x2") == manager.integer(4));
  360. initialPredicates.push_back(manager.getVariableExpression("x2") == manager.integer(5));
  361. initialPredicates.push_back(manager.getVariableExpression("x2") == manager.integer(6));
  362. initialPredicates.push_back(manager.getVariableExpression("x2") == manager.integer(7));
  363. initialPredicates.push_back(manager.getVariableExpression("s2") == manager.integer(1));
  364. initialPredicates.push_back(manager.getVariableExpression("s2") == manager.integer(2));
  365. initialPredicates.push_back(manager.getVariableExpression("s2") == manager.integer(3));
  366. initialPredicates.push_back(manager.getVariableExpression("s2") == manager.integer(4));
  367. initialPredicates.push_back(manager.getVariableExpression("s2") == manager.integer(5));
  368. initialPredicates.push_back(manager.getVariableExpression("s2") == manager.integer(6));
  369. initialPredicates.push_back(manager.getVariableExpression("s2") == manager.integer(7));
  370. initialPredicates.push_back(manager.getVariableExpression("s2") == manager.integer(8));
  371. initialPredicates.push_back(manager.getVariableExpression("s2") == manager.integer(9));
  372. initialPredicates.push_back(manager.getVariableExpression("s2") == manager.integer(10));
  373. initialPredicates.push_back(manager.getVariableExpression("s2") == manager.integer(11));
  374. initialPredicates.push_back(manager.getVariableExpression("s2") == manager.integer(12));
  375. initialPredicates.push_back(manager.getVariableExpression("slot2") == manager.integer(0));
  376. initialPredicates.push_back(manager.getVariableExpression("slot2") == manager.integer(1));
  377. initialPredicates.push_back(manager.getVariableExpression("backoff2") == manager.integer(0));
  378. initialPredicates.push_back(manager.getVariableExpression("backoff2") == manager.integer(1));
  379. initialPredicates.push_back(manager.getVariableExpression("backoff2") == manager.integer(2));
  380. initialPredicates.push_back(manager.getVariableExpression("backoff2") == manager.integer(3));
  381. initialPredicates.push_back(manager.getVariableExpression("backoff2") == manager.integer(4));
  382. initialPredicates.push_back(manager.getVariableExpression("backoff2") == manager.integer(5));
  383. initialPredicates.push_back(manager.getVariableExpression("backoff2") == manager.integer(6));
  384. initialPredicates.push_back(manager.getVariableExpression("backoff2") == manager.integer(7));
  385. initialPredicates.push_back(manager.getVariableExpression("backoff2") == manager.integer(8));
  386. initialPredicates.push_back(manager.getVariableExpression("backoff2") == manager.integer(9));
  387. initialPredicates.push_back(manager.getVariableExpression("backoff2") == manager.integer(10));
  388. initialPredicates.push_back(manager.getVariableExpression("backoff2") == manager.integer(11));
  389. initialPredicates.push_back(manager.getVariableExpression("backoff2") == manager.integer(12));
  390. initialPredicates.push_back(manager.getVariableExpression("backoff2") == manager.integer(13));
  391. initialPredicates.push_back(manager.getVariableExpression("backoff2") == manager.integer(14));
  392. initialPredicates.push_back(manager.getVariableExpression("backoff2") == manager.integer(15));
  393. initialPredicates.push_back(manager.getVariableExpression("bc2") == manager.integer(0));
  394. initialPredicates.push_back(manager.getVariableExpression("bc2") == manager.integer(1));
  395. storm::abstraction::prism::AbstractProgram<storm::dd::DdType::CUDD, double> abstractProgram(program, initialPredicates, std::make_shared<storm::utility::solver::MathsatSmtSolverFactory>(), false);
  396. storm::abstraction::MenuGame<storm::dd::DdType::CUDD, double> game = abstractProgram.getAbstractGame();
  397. // The target states are those states where col == 2.
  398. storm::dd::Bdd<storm::dd::DdType::CUDD> targetStates = game.getStates(initialPredicates[2], false);
  399. storm::utility::graph::GameProb01Result<storm::dd::DdType::CUDD> result = storm::utility::graph::performProb0(game, game.getQualitativeTransitionMatrix(), game.getReachableStates(), targetStates, storm::OptimizationDirection::Minimize, storm::OptimizationDirection::Minimize, true, true);
  400. EXPECT_EQ(2831, result.getPlayer1States().getNonZeroCount());
  401. EXPECT_TRUE(result.hasPlayer1Strategy());
  402. EXPECT_TRUE(result.hasPlayer2Strategy());
  403. // Check the validity of the strategies. Start by checking whether only prob0 states have a strategy.
  404. storm::dd::Bdd<storm::dd::DdType::CUDD> nonProb0StatesWithStrategy = !result.getPlayer1States() && result.player1Strategy.get();
  405. EXPECT_TRUE(nonProb0StatesWithStrategy.isZero());
  406. // Proceed by checking whether they select exactly one action in each state.
  407. storm::dd::Add<storm::dd::DdType::CUDD, double> stateDistributionsUnderStrategies = (game.getTransitionMatrix() * result.player1Strategy.get().template toAdd<double>() * result.player2Strategy.get().template toAdd<double>()).sumAbstract(game.getColumnVariables());;
  408. EXPECT_EQ(2831, stateDistributionsUnderStrategies.getNonZeroCount());
  409. // Check that the number of distributions per state is one (or zero in the case where there are no prob0 states).
  410. storm::dd::Add<storm::dd::DdType::CUDD> stateDistributionCount = stateDistributionsUnderStrategies.sumAbstract(game.getNondeterminismVariables());
  411. EXPECT_EQ(1, stateDistributionCount.getMax());
  412. result = storm::utility::graph::performProb1(game, game.getQualitativeTransitionMatrix(), game.getReachableStates(), targetStates, storm::OptimizationDirection::Minimize, storm::OptimizationDirection::Minimize);
  413. EXPECT_EQ(2692, result.getPlayer1States().getNonZeroCount());
  414. result = storm::utility::graph::performProb0(game, game.getQualitativeTransitionMatrix(), game.getReachableStates(), targetStates, storm::OptimizationDirection::Minimize, storm::OptimizationDirection::Maximize);
  415. EXPECT_EQ(2831, result.getPlayer1States().getNonZeroCount());
  416. result = storm::utility::graph::performProb1(game, game.getQualitativeTransitionMatrix(), game.getReachableStates(), targetStates, storm::OptimizationDirection::Minimize, storm::OptimizationDirection::Maximize);
  417. EXPECT_EQ(2692, result.getPlayer1States().getNonZeroCount());
  418. result = storm::utility::graph::performProb0(game, game.getQualitativeTransitionMatrix(), game.getReachableStates(), targetStates, storm::OptimizationDirection::Maximize, storm::OptimizationDirection::Minimize);
  419. EXPECT_EQ(2064, result.getPlayer1States().getNonZeroCount());
  420. result = storm::utility::graph::performProb1(game, game.getQualitativeTransitionMatrix(), game.getReachableStates(), targetStates, storm::OptimizationDirection::Maximize, storm::OptimizationDirection::Minimize);
  421. EXPECT_EQ(2884, result.getPlayer1States().getNonZeroCount());
  422. result = storm::utility::graph::performProb0(game, game.getQualitativeTransitionMatrix(), game.getReachableStates(), targetStates, storm::OptimizationDirection::Maximize, storm::OptimizationDirection::Maximize);
  423. EXPECT_EQ(2064, result.getPlayer1States().getNonZeroCount());
  424. result = storm::utility::graph::performProb1(game, game.getQualitativeTransitionMatrix(), game.getReachableStates(), targetStates, storm::OptimizationDirection::Maximize, storm::OptimizationDirection::Maximize, true, true);
  425. EXPECT_EQ(2884, result.getPlayer1States().getNonZeroCount());
  426. EXPECT_TRUE(result.hasPlayer1Strategy());
  427. EXPECT_TRUE(result.hasPlayer2Strategy());
  428. // Check the validity of the strategies. Start by checking whether only prob1 states have a strategy.
  429. storm::dd::Bdd<storm::dd::DdType::CUDD> nonProb1StatesWithStrategy = !result.getPlayer1States() && result.player1Strategy.get();
  430. EXPECT_TRUE(nonProb1StatesWithStrategy.isZero());
  431. // Proceed by checking whether they select exactly one action in each state.
  432. stateDistributionsUnderStrategies = (game.getTransitionMatrix() * result.player1Strategy.get().template toAdd<double>() * result.player2Strategy.get().template toAdd<double>()).sumAbstract(game.getColumnVariables());
  433. EXPECT_EQ(2884, stateDistributionsUnderStrategies.getNonZeroCount());
  434. // Check that the number of distributions per state is one (or zero in the case where there are no prob1 states).
  435. stateDistributionCount = stateDistributionsUnderStrategies.sumAbstract(game.getNondeterminismVariables());
  436. EXPECT_EQ(1, stateDistributionCount.getMax());
  437. }
  438. #endif
  439. TEST(GraphTest, ExplicitProb01) {
  440. storm::prism::Program program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/crowds-5-5.pm");
  441. std::shared_ptr<storm::models::sparse::Model<double>> model = storm::builder::ExplicitModelBuilder<double>(program, storm::generator::NextStateGeneratorOptions(false, true)).build();
  442. ASSERT_TRUE(model->getType() == storm::models::ModelType::Dtmc);
  443. std::pair<storm::storage::BitVector, storm::storage::BitVector> statesWithProbability01;
  444. ASSERT_NO_THROW(statesWithProbability01 = storm::utility::graph::performProb01(*model->as<storm::models::sparse::Dtmc<double>>(), storm::storage::BitVector(model->getNumberOfStates(), true), model->getStates("observe0Greater1")));
  445. EXPECT_EQ(4409ul, statesWithProbability01.first.getNumberOfSetBits());
  446. EXPECT_EQ(1316ul, statesWithProbability01.second.getNumberOfSetBits());
  447. ASSERT_NO_THROW(statesWithProbability01 = storm::utility::graph::performProb01(*model->as<storm::models::sparse::Dtmc<double>>(), storm::storage::BitVector(model->getNumberOfStates(), true), model->getStates("observeIGreater1")));
  448. EXPECT_EQ(1091ul, statesWithProbability01.first.getNumberOfSetBits());
  449. EXPECT_EQ(4802ul, statesWithProbability01.second.getNumberOfSetBits());
  450. ASSERT_NO_THROW(statesWithProbability01 = storm::utility::graph::performProb01(*model->as<storm::models::sparse::Dtmc<double>>(), storm::storage::BitVector(model->getNumberOfStates(), true), model->getStates("observeOnlyTrueSender")));
  451. EXPECT_EQ(5829ul, statesWithProbability01.first.getNumberOfSetBits());
  452. EXPECT_EQ(1032ul, statesWithProbability01.second.getNumberOfSetBits());
  453. }
  454. TEST(GraphTest, ExplicitProb01MinMax) {
  455. storm::prism::Program program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/leader3.nm");
  456. std::shared_ptr<storm::models::sparse::Model<double>> model = storm::builder::ExplicitModelBuilder<double>(program, storm::generator::NextStateGeneratorOptions(false, true)).build();
  457. ASSERT_TRUE(model->getType() == storm::models::ModelType::Mdp);
  458. std::pair<storm::storage::BitVector, storm::storage::BitVector> statesWithProbability01;
  459. ASSERT_NO_THROW(statesWithProbability01 = storm::utility::graph::performProb01Min(*model->as<storm::models::sparse::Mdp<double>>(), storm::storage::BitVector(model->getNumberOfStates(), true), model->getStates("elected")));
  460. EXPECT_EQ(0ul, statesWithProbability01.first.getNumberOfSetBits());
  461. EXPECT_EQ(364ul, statesWithProbability01.second.getNumberOfSetBits());
  462. ASSERT_NO_THROW(statesWithProbability01 = storm::utility::graph::performProb01Max(*model->as<storm::models::sparse::Mdp<double>>(), storm::storage::BitVector(model->getNumberOfStates(), true), model->getStates("elected")));
  463. EXPECT_EQ(0ul, statesWithProbability01.first.getNumberOfSetBits());
  464. EXPECT_EQ(364ul, statesWithProbability01.second.getNumberOfSetBits());
  465. program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/coin2-2.nm");
  466. model = storm::builder::ExplicitModelBuilder<double>(program, storm::generator::NextStateGeneratorOptions(false, true)).build();
  467. ASSERT_TRUE(model->getType() == storm::models::ModelType::Mdp);
  468. 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")));
  469. EXPECT_EQ(77ul, statesWithProbability01.first.getNumberOfSetBits());
  470. EXPECT_EQ(149ul, statesWithProbability01.second.getNumberOfSetBits());
  471. 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")));
  472. EXPECT_EQ(74ul, statesWithProbability01.first.getNumberOfSetBits());
  473. EXPECT_EQ(198ul, statesWithProbability01.second.getNumberOfSetBits());
  474. 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")));
  475. EXPECT_EQ(94ul, statesWithProbability01.first.getNumberOfSetBits());
  476. EXPECT_EQ(33ul, statesWithProbability01.second.getNumberOfSetBits());
  477. 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")));
  478. EXPECT_EQ(83ul, statesWithProbability01.first.getNumberOfSetBits());
  479. EXPECT_EQ(35ul, statesWithProbability01.second.getNumberOfSetBits());
  480. program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/csma2-2.nm");
  481. model = storm::builder::ExplicitModelBuilder<double>(program, storm::generator::NextStateGeneratorOptions(false, true)).build();
  482. ASSERT_TRUE(model->getType() == storm::models::ModelType::Mdp);
  483. 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")));
  484. EXPECT_EQ(993ul, statesWithProbability01.first.getNumberOfSetBits());
  485. EXPECT_EQ(16ul, statesWithProbability01.second.getNumberOfSetBits());
  486. 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")));
  487. EXPECT_EQ(993ul, statesWithProbability01.first.getNumberOfSetBits());
  488. EXPECT_EQ(16ul, statesWithProbability01.second.getNumberOfSetBits());
  489. }