9TEST(DeterministicModelBisimulationDecomposition, Die) {
10 std::shared_ptr<storm::models::sparse::Model<double>> abstractModel =
17 ASSERT_NO_THROW(bisim.computeBisimulationDecomposition());
18 std::shared_ptr<storm::models::sparse::Model<double>> result;
19 ASSERT_NO_THROW(result = bisim.getQuotient());
22 EXPECT_EQ(13ul, result->getNumberOfStates());
23 EXPECT_EQ(20ul, result->getNumberOfTransitions());
26 options.respectedAtomicPropositions = std::set<std::string>({
"one"});
29 ASSERT_NO_THROW(bisim2.computeBisimulationDecomposition());
30 ASSERT_NO_THROW(result = bisim2.getQuotient());
33 EXPECT_EQ(5ul, result->getNumberOfStates());
34 EXPECT_EQ(8ul, result->getNumberOfTransitions());
43 EXPECT_EQ(5ul, result->getNumberOfStates());
44 EXPECT_EQ(8ul, result->getNumberOfTransitions());
55 EXPECT_EQ(5ul, result->getNumberOfStates());
56 EXPECT_EQ(8ul, result->getNumberOfTransitions());
59TEST(DeterministicModelBisimulationDecomposition, Crowds) {
60 std::shared_ptr<storm::models::sparse::Model<double>> abstractModel =
67 std::shared_ptr<storm::models::sparse::Model<double>> result;
68 ASSERT_NO_THROW(bisim.computeBisimulationDecomposition());
69 ASSERT_NO_THROW(result = bisim.getQuotient());
72 EXPECT_EQ(334ul, result->getNumberOfStates());
73 EXPECT_EQ(546ul, result->getNumberOfTransitions());
76 options.respectedAtomicPropositions = std::set<std::string>({
"observe0Greater1"});
79 ASSERT_NO_THROW(bisim2.computeBisimulationDecomposition());
80 ASSERT_NO_THROW(result = bisim2.getQuotient());
83 EXPECT_EQ(65ul, result->getNumberOfStates());
84 EXPECT_EQ(105ul, result->getNumberOfTransitions());
93 EXPECT_EQ(43ul, result->getNumberOfStates());
94 EXPECT_EQ(83ul, result->getNumberOfTransitions());
106 EXPECT_EQ(64ul, result->getNumberOfStates());
107 EXPECT_EQ(104ul, result->getNumberOfTransitions());
118 EXPECT_EQ(65ul, result->getNumberOfStates());
119 EXPECT_EQ(105ul, result->getNumberOfTransitions());
static std::shared_ptr< storm::models::sparse::Model< ValueType, storm::models::sparse::StandardRewardModel< RewardValueType > > > parseModel(std::string const &transitionsFilename, std::string const &labelingFilename, std::string const &stateRewardFilename="", std::string const &transitionRewardFilename="", std::string const &choiceLabelingFilename="")
Checks the given files and parses the model within these files.