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.

75 lines
3.9 KiB

  1. #include "gtest/gtest.h"
  2. #include "storm-config.h"
  3. #include "src/parser/AutoParser.h"
  4. #include "src/storage/StronglyConnectedComponentDecomposition.h"
  5. TEST(StronglyConnectedComponentDecomposition, Crowds) {
  6. storm::parser::AutoParser<double> parser(STORM_CPP_BASE_PATH "/examples/dtmc/crowds/crowds20_5.tra", STORM_CPP_BASE_PATH "/examples/dtmc/crowds/crowds20_5.lab", "", "");
  7. std::shared_ptr<storm::models::Dtmc<double>> dtmc = parser.getModel<storm::models::Dtmc<double>>();
  8. storm::storage::StronglyConnectedComponentDecomposition<double> sccDecomposition;
  9. ASSERT_NO_THROW(sccDecomposition = storm::storage::StronglyConnectedComponentDecomposition<double>(*dtmc));
  10. ASSERT_EQ(1290297ull, sccDecomposition.size());
  11. ASSERT_NO_THROW(sccDecomposition = storm::storage::StronglyConnectedComponentDecomposition<double>(*dtmc, true));
  12. ASSERT_EQ(1290297, sccDecomposition.size());
  13. ASSERT_NO_THROW(sccDecomposition = storm::storage::StronglyConnectedComponentDecomposition<double>(*dtmc, true, true));
  14. ASSERT_EQ(425040, sccDecomposition.size());
  15. dtmc = nullptr;
  16. }
  17. TEST(StronglyConnectedComponentDecomposition, SynchronousLeader) {
  18. storm::parser::AutoParser<double> parser(STORM_CPP_BASE_PATH "/examples/dtmc/synchronous_leader/leader6_9.tra", STORM_CPP_BASE_PATH "/examples/dtmc/synchronous_leader/leader6_9.lab", "", "");
  19. std::shared_ptr<storm::models::Dtmc<double>> dtmc = parser.getModel<storm::models::Dtmc<double>>();
  20. storm::storage::StronglyConnectedComponentDecomposition<double> sccDecomposition;
  21. ASSERT_NO_THROW(sccDecomposition = storm::storage::StronglyConnectedComponentDecomposition<double>(*dtmc));
  22. ASSERT_EQ(2611835, sccDecomposition.size());
  23. ASSERT_NO_THROW(sccDecomposition = storm::storage::StronglyConnectedComponentDecomposition<double>(*dtmc, true));
  24. ASSERT_EQ(2611835, sccDecomposition.size());
  25. ASSERT_NO_THROW(sccDecomposition = storm::storage::StronglyConnectedComponentDecomposition<double>(*dtmc, true, true));
  26. ASSERT_EQ(1, sccDecomposition.size());
  27. dtmc = nullptr;
  28. }
  29. TEST(StronglyConnectedComponentDecomposition, AsynchronousLeader) {
  30. storm::parser::AutoParser<double> parser(STORM_CPP_BASE_PATH "/examples/mdp/asynchronous_leader/leader7.tra", STORM_CPP_BASE_PATH "/examples/mdp/asynchronous_leader/leader7.lab", "", "");
  31. std::shared_ptr<storm::models::Mdp<double>> mdp = parser.getModel<storm::models::Mdp<double>>();
  32. storm::storage::StronglyConnectedComponentDecomposition<double> sccDecomposition;
  33. ASSERT_NO_THROW(sccDecomposition = storm::storage::StronglyConnectedComponentDecomposition<double>(*mdp));
  34. ASSERT_EQ(1461930, sccDecomposition.size());
  35. ASSERT_NO_THROW(sccDecomposition = storm::storage::StronglyConnectedComponentDecomposition<double>(*mdp, true));
  36. ASSERT_EQ(127, sccDecomposition.size());
  37. ASSERT_NO_THROW(sccDecomposition = storm::storage::StronglyConnectedComponentDecomposition<double>(*mdp, true));
  38. ASSERT_EQ(127, sccDecomposition.size());
  39. mdp = nullptr;
  40. }
  41. TEST(StronglyConnectedComponentDecomposition, Consensus) {
  42. storm::parser::AutoParser<double> parser(STORM_CPP_BASE_PATH "/examples/mdp/consensus/coin6_4.tra", STORM_CPP_BASE_PATH "/examples/mdp/consensus/coin6_4.lab", "", "");
  43. std::shared_ptr<storm::models::Mdp<double>> mdp = parser.getModel<storm::models::Mdp<double>>();
  44. storm::storage::StronglyConnectedComponentDecomposition<double> sccDecomposition;
  45. ASSERT_NO_THROW(sccDecomposition = storm::storage::StronglyConnectedComponentDecomposition<double>(*mdp));
  46. ASSERT_EQ(121251, sccDecomposition.size());
  47. ASSERT_NO_THROW(sccDecomposition = storm::storage::StronglyConnectedComponentDecomposition<double>(*mdp, true));
  48. ASSERT_EQ(1049, sccDecomposition.size());
  49. ASSERT_NO_THROW(sccDecomposition = storm::storage::StronglyConnectedComponentDecomposition<double>(*mdp, true, true));
  50. ASSERT_EQ(384, sccDecomposition.size());
  51. mdp = nullptr;
  52. }