Storm 1.10.0.1
A Modern Probabilistic Model Checker
Loading...
Searching...
No Matches
DeterministicModelBisimulationDecompositionTest.cpp
Go to the documentation of this file.
1#include "storm-config.h"
7#include "test/storm_gtest.h"
8
9TEST(DeterministicModelBisimulationDecomposition, Die) {
10 std::shared_ptr<storm::models::sparse::Model<double>> abstractModel =
11 storm::parser::AutoParser<>::parseModel(STORM_TEST_RESOURCES_DIR "/tra/die.tra", STORM_TEST_RESOURCES_DIR "/lab/die.lab", "", "");
12
13 ASSERT_EQ(abstractModel->getType(), storm::models::ModelType::Dtmc);
14 std::shared_ptr<storm::models::sparse::Dtmc<double>> dtmc = abstractModel->as<storm::models::sparse::Dtmc<double>>();
15
17 ASSERT_NO_THROW(bisim.computeBisimulationDecomposition());
18 std::shared_ptr<storm::models::sparse::Model<double>> result;
19 ASSERT_NO_THROW(result = bisim.getQuotient());
20
21 EXPECT_EQ(storm::models::ModelType::Dtmc, result->getType());
22 EXPECT_EQ(13ul, result->getNumberOfStates());
23 EXPECT_EQ(20ul, result->getNumberOfTransitions());
24
26 options.respectedAtomicPropositions = std::set<std::string>({"one"});
27
29 ASSERT_NO_THROW(bisim2.computeBisimulationDecomposition());
30 ASSERT_NO_THROW(result = bisim2.getQuotient());
31
32 EXPECT_EQ(storm::models::ModelType::Dtmc, result->getType());
33 EXPECT_EQ(5ul, result->getNumberOfStates());
34 EXPECT_EQ(8ul, result->getNumberOfTransitions());
35
37
39 ASSERT_NO_THROW(bisim3.computeBisimulationDecomposition());
40 ASSERT_NO_THROW(result = bisim3.getQuotient());
41
42 EXPECT_EQ(storm::models::ModelType::Dtmc, result->getType());
43 EXPECT_EQ(5ul, result->getNumberOfStates());
44 EXPECT_EQ(8ul, result->getNumberOfTransitions());
45
46 storm::parser::FormulaParser formulaParser;
47 std::shared_ptr<storm::logic::Formula const> formula = formulaParser.parseSingleFormulaFromString("P=? [F \"one\"]");
48
50
52 ASSERT_NO_THROW(bisim4.computeBisimulationDecomposition());
53 ASSERT_NO_THROW(result = bisim4.getQuotient());
54 EXPECT_EQ(storm::models::ModelType::Dtmc, result->getType());
55 EXPECT_EQ(5ul, result->getNumberOfStates());
56 EXPECT_EQ(8ul, result->getNumberOfTransitions());
57}
58
59TEST(DeterministicModelBisimulationDecomposition, Crowds) {
60 std::shared_ptr<storm::models::sparse::Model<double>> abstractModel =
61 storm::parser::AutoParser<>::parseModel(STORM_TEST_RESOURCES_DIR "/tra/crowds5_5.tra", STORM_TEST_RESOURCES_DIR "/lab/crowds5_5.lab", "", "");
62
63 ASSERT_EQ(abstractModel->getType(), storm::models::ModelType::Dtmc);
64 std::shared_ptr<storm::models::sparse::Dtmc<double>> dtmc = abstractModel->as<storm::models::sparse::Dtmc<double>>();
65
67 std::shared_ptr<storm::models::sparse::Model<double>> result;
68 ASSERT_NO_THROW(bisim.computeBisimulationDecomposition());
69 ASSERT_NO_THROW(result = bisim.getQuotient());
70
71 EXPECT_EQ(storm::models::ModelType::Dtmc, result->getType());
72 EXPECT_EQ(334ul, result->getNumberOfStates());
73 EXPECT_EQ(546ul, result->getNumberOfTransitions());
74
76 options.respectedAtomicPropositions = std::set<std::string>({"observe0Greater1"});
77
79 ASSERT_NO_THROW(bisim2.computeBisimulationDecomposition());
80 ASSERT_NO_THROW(result = bisim2.getQuotient());
81
82 EXPECT_EQ(storm::models::ModelType::Dtmc, result->getType());
83 EXPECT_EQ(65ul, result->getNumberOfStates());
84 EXPECT_EQ(105ul, result->getNumberOfTransitions());
85
87
89 ASSERT_NO_THROW(bisim3.computeBisimulationDecomposition());
90 ASSERT_NO_THROW(result = bisim3.getQuotient());
91
92 EXPECT_EQ(storm::models::ModelType::Dtmc, result->getType());
93 EXPECT_EQ(43ul, result->getNumberOfStates());
94 EXPECT_EQ(83ul, result->getNumberOfTransitions());
95
96 storm::parser::FormulaParser formulaParser;
97 std::shared_ptr<storm::logic::Formula const> formula = formulaParser.parseSingleFormulaFromString("P=? [F \"observe0Greater1\"]");
98
100
102 ASSERT_NO_THROW(bisim5.computeBisimulationDecomposition());
103 ASSERT_NO_THROW(result = bisim5.getQuotient());
104
105 EXPECT_EQ(storm::models::ModelType::Dtmc, result->getType());
106 EXPECT_EQ(64ul, result->getNumberOfStates());
107 EXPECT_EQ(104ul, result->getNumberOfTransitions());
108
109 formula = formulaParser.parseSingleFormulaFromString("P=? [true U<=50 \"observe0Greater1\"] ");
110
112
114 ASSERT_NO_THROW(bisim6.computeBisimulationDecomposition());
115 ASSERT_NO_THROW(result = bisim6.getQuotient());
116
117 EXPECT_EQ(storm::models::ModelType::Dtmc, result->getType());
118 EXPECT_EQ(65ul, result->getNumberOfStates());
119 EXPECT_EQ(105ul, result->getNumberOfTransitions());
120}
TEST(DeterministicModelBisimulationDecomposition, Die)
This class represents a discrete-time Markov chain.
Definition Dtmc.h:14
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.
std::shared_ptr< storm::logic::Formula const > parseSingleFormulaFromString(std::string const &formulaString) const
Parses the formula given by the provided string.
std::shared_ptr< ModelType > getQuotient() const
Retrieves the quotient of the model under the computed bisimulation.
void computeBisimulationDecomposition()
Computes the decomposition of the model into bisimulation equivalence classes.
This class represents the decomposition of a deterministic model into its bisimulation quotient.