Storm
A Modern Probabilistic Model Checker
Loading...
Searching...
No Matches
NonMarkovianChainTransformerTest.cpp
Go to the documentation of this file.
1#include "storm-config.h"
2#include "storm-parsers/api/storm-parsers.h"
3#include "storm-parsers/parser/PrismParser.h"
4#include "storm/api/storm.h"
5#include "storm/modelchecker/results/ExplicitQuantitativeCheckResult.h"
6#include "storm/storage/jani/Property.h"
7#include "test/storm_gtest.h"
8
9TEST(NonMarkovianChainTransformerTest, StreamExampleTest) {
10#ifndef STORM_HAVE_Z3
11 GTEST_SKIP() << "Z3 not available.";
12#endif
13
14 storm::prism::Program program = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/ma/stream2.ma");
15 std::string formulasString = "Pmin=? [ F \"done\"];Pmin=? [ F<=1 \"done\"];Tmin=? [ F \"done\" ]";
16 auto formulas = storm::api::extractFormulasFromProperties(storm::api::parsePropertiesForPrismProgram(formulasString, program));
17 auto model = storm::api::buildSparseModel<double>(program, formulas)->template as<storm::models::sparse::MarkovAutomaton<double>>();
18
19 EXPECT_EQ(12ul, model->getNumberOfStates());
20 EXPECT_EQ(14ul, model->getNumberOfTransitions());
21 ASSERT_TRUE(model->isOfType(storm::models::ModelType::MarkovAutomaton));
22 size_t initState = 0;
23
24 auto labeling = model->getStateLabeling();
25 ASSERT_TRUE(labeling.getStateHasLabel("init", initState));
26 ASSERT_TRUE(labeling.getStateHasLabel("done", 10));
27
28 auto result = storm::api::verifyWithSparseEngine(model, storm::api::createTask<double>(formulas[0], true));
29 EXPECT_EQ(1, result->asExplicitQuantitativeCheckResult<double>()[initState]);
30 result = storm::api::verifyWithSparseEngine(model, storm::api::createTask<double>(formulas[1], true));
31 EXPECT_NEAR(0.6487584849, result->asExplicitQuantitativeCheckResult<double>()[initState], 1e-6);
32 result = storm::api::verifyWithSparseEngine(model, storm::api::createTask<double>(formulas[2], true));
33 EXPECT_NEAR(0.7888888889, result->asExplicitQuantitativeCheckResult<double>()[initState], 1e-6);
34
35 // Keep labels
36 auto transformed = storm::api::eliminateNonMarkovianChains(model, formulas, storm::transformer::EliminationLabelBehavior::KeepLabels);
37 ASSERT_EQ(9ul, transformed.first->getNumberOfStates());
38 ASSERT_EQ(11ul, transformed.first->getNumberOfTransitions());
39 labeling = transformed.first->getStateLabeling();
40 ASSERT_TRUE(labeling.getStateHasLabel("init", initState));
41 ASSERT_TRUE(labeling.getStateHasLabel("done", 8));
42 EXPECT_EQ(2ul, transformed.second.size());
43
44 result = storm::api::verifyWithSparseEngine(transformed.first, storm::api::createTask<double>(transformed.second[0], true));
45 EXPECT_EQ(1, result->asExplicitQuantitativeCheckResult<double>()[initState]);
46 result = storm::api::verifyWithSparseEngine(model, storm::api::createTask<double>(transformed.second[1], true));
47 EXPECT_NEAR(0.6487584849, result->asExplicitQuantitativeCheckResult<double>()[initState], 1e-6);
48 // result = storm::api::verifyWithSparseEngine(model, storm::api::createTask<double>(transformed.second[2], true));
49 // EXPECT_NEAR(0.7888888889, result->asExplicitQuantitativeCheckResult<double>()[initState], 1e-6);
50
51 // Merge labels
52 transformed = storm::api::eliminateNonMarkovianChains(model, formulas, storm::transformer::EliminationLabelBehavior::MergeLabels);
53 ASSERT_EQ(8ul, transformed.first->getNumberOfStates());
54 ASSERT_EQ(10ul, transformed.first->getNumberOfTransitions());
55 labeling = transformed.first->getStateLabeling();
56 ASSERT_TRUE(labeling.getStateHasLabel("init", initState));
57 ASSERT_TRUE(labeling.getStateHasLabel("done", 7));
58 EXPECT_EQ(2ul, transformed.second.size());
59
60 result = storm::api::verifyWithSparseEngine(transformed.first, storm::api::createTask<double>(transformed.second[0], true));
61 EXPECT_EQ(1, result->asExplicitQuantitativeCheckResult<double>()[initState]);
62 result = storm::api::verifyWithSparseEngine(model, storm::api::createTask<double>(transformed.second[1], true));
63 EXPECT_NEAR(0.6487584849, result->asExplicitQuantitativeCheckResult<double>()[initState], 1e-6);
64 // result = storm::api::verifyWithSparseEngine(model, storm::api::createTask<double>(transformed.second[2], true));
65 // EXPECT_NEAR(0.7888888889, result->asExplicitQuantitativeCheckResult<double>()[initState], 1e-6);
66
67 // Delete labels
68 transformed = storm::api::eliminateNonMarkovianChains(model, formulas, storm::transformer::EliminationLabelBehavior::DeleteLabels);
69 ASSERT_EQ(8ul, transformed.first->getNumberOfStates());
70 ASSERT_EQ(10ul, transformed.first->getNumberOfTransitions());
71 labeling = transformed.first->getStateLabeling();
72 ASSERT_TRUE(labeling.getStateHasLabel("init", initState));
73 ASSERT_TRUE(labeling.getStateHasLabel("done", 7));
74 EXPECT_EQ(2ul, transformed.second.size());
75
76 result = storm::api::verifyWithSparseEngine(transformed.first, storm::api::createTask<double>(transformed.second[0], true));
77 EXPECT_EQ(1, result->asExplicitQuantitativeCheckResult<double>()[initState]);
78 result = storm::api::verifyWithSparseEngine(model, storm::api::createTask<double>(transformed.second[1], true));
79 EXPECT_NEAR(0.6487584849, result->asExplicitQuantitativeCheckResult<double>()[initState], 1e-6);
80 // result = storm::api::verifyWithSparseEngine(model, storm::api::createTask<double>(transformed.second[2], true));
81 // EXPECT_NEAR(0.7888888889, result->asExplicitQuantitativeCheckResult<double>()[initState], 1e-6);
82}
83
84TEST(NonMarkovianChainTransformerTest, ChainElimination1ExampleTest) {
85 auto model = storm::parser::DirectEncodingParser<double>::parseModel(STORM_TEST_RESOURCES_DIR "/ma/chain_elimination1.drn")
86 ->template as<storm::models::sparse::MarkovAutomaton<double>>();
87 std::string formulasString = "Pmin=? [ F \"Fail\"];Pmin=? [ F<=300 \"Fail\"];Tmin=? [ F \"Fail\" ]";
88 auto formulas = storm::api::extractFormulasFromProperties(storm::api::parseProperties(formulasString));
89
90 EXPECT_EQ(43ul, model->getNumberOfStates());
91 EXPECT_EQ(59ul, model->getNumberOfTransitions());
92 ASSERT_TRUE(model->isOfType(storm::models::ModelType::MarkovAutomaton));
93 size_t initState = 0;
94
95 auto labeling = model->getStateLabeling();
96 ASSERT_TRUE(labeling.getStateHasLabel("init", initState));
97 for (size_t i = 10; i < 43; ++i) {
98 ASSERT_TRUE(labeling.getStateHasLabel("Fail", i));
99 }
100
101 auto result = storm::api::verifyWithSparseEngine(model, storm::api::createTask<double>(formulas[0], true));
102 EXPECT_EQ(1, result->asExplicitQuantitativeCheckResult<double>()[initState]);
103 result = storm::api::verifyWithSparseEngine(model, storm::api::createTask<double>(formulas[1], true));
104 EXPECT_NEAR(0.08606881472, result->asExplicitQuantitativeCheckResult<double>()[initState], 1e-6);
105 result = storm::api::verifyWithSparseEngine(model, storm::api::createTask<double>(formulas[2], true));
106 EXPECT_NEAR(3333.333333, result->asExplicitQuantitativeCheckResult<double>()[initState], 1e-6);
107
108 // Keep labels
109 auto transformed = storm::api::eliminateNonMarkovianChains(model, formulas, storm::transformer::EliminationLabelBehavior::KeepLabels);
110 ASSERT_EQ(13ul, transformed.first->getNumberOfStates());
111 ASSERT_EQ(29ul, transformed.first->getNumberOfTransitions());
112 labeling = transformed.first->getStateLabeling();
113 ASSERT_TRUE(labeling.getStateHasLabel("init", initState));
114 for (size_t i = 5; i < 13; ++i) {
115 ASSERT_TRUE(labeling.getStateHasLabel("Fail", i));
116 }
117 EXPECT_EQ(2ul, transformed.second.size());
118
119 result = storm::api::verifyWithSparseEngine(transformed.first, storm::api::createTask<double>(transformed.second[0], true));
120 EXPECT_EQ(1, result->asExplicitQuantitativeCheckResult<double>()[initState]);
121 result = storm::api::verifyWithSparseEngine(model, storm::api::createTask<double>(transformed.second[1], true));
122 EXPECT_NEAR(0.08606881472, result->asExplicitQuantitativeCheckResult<double>()[initState], 1e-6);
123 // result = storm::api::verifyWithSparseEngine(model, storm::api::createTask<double>(transformed.second[2], true));
124 // EXPECT_NEAR(3333.333333, result->asExplicitQuantitativeCheckResult<double>()[initState], 1e-6);
125
126 // Merge labels
127 transformed = storm::api::eliminateNonMarkovianChains(model, formulas, storm::transformer::EliminationLabelBehavior::MergeLabels);
128 ASSERT_EQ(8ul, transformed.first->getNumberOfStates());
129 ASSERT_EQ(24ul, transformed.first->getNumberOfTransitions());
130 labeling = transformed.first->getStateLabeling();
131 ASSERT_TRUE(labeling.getStateHasLabel("init", initState));
132 for (size_t i = 0; i < 8; ++i) {
133 ASSERT_TRUE(labeling.getStateHasLabel("Fail", i));
134 }
135 EXPECT_EQ(2ul, transformed.second.size());
136
137 result = storm::api::verifyWithSparseEngine(transformed.first, storm::api::createTask<double>(transformed.second[0], true));
138 EXPECT_EQ(1, result->asExplicitQuantitativeCheckResult<double>()[initState]);
139 result = storm::api::verifyWithSparseEngine(model, storm::api::createTask<double>(transformed.second[1], true));
140 EXPECT_NEAR(0.08606881472, result->asExplicitQuantitativeCheckResult<double>()[initState], 1e-6);
141 // result = storm::api::verifyWithSparseEngine(model, storm::api::createTask<double>(transformed.second[2], true));
142 // EXPECT_NEAR(3333.333333, result->asExplicitQuantitativeCheckResult<double>()[initState], 1e-6);
143
144 // Delete labels
145 transformed = storm::api::eliminateNonMarkovianChains(model, formulas, storm::transformer::EliminationLabelBehavior::DeleteLabels);
146 ASSERT_EQ(8ul, transformed.first->getNumberOfStates());
147 ASSERT_EQ(24ul, transformed.first->getNumberOfTransitions());
148 labeling = transformed.first->getStateLabeling();
149 ASSERT_TRUE(labeling.getStateHasLabel("init", initState));
150 ASSERT_FALSE(labeling.getStateHasLabel("Fail", 0));
151 for (size_t i = 1; i < 8; ++i) {
152 ASSERT_TRUE(labeling.getStateHasLabel("Fail", i));
153 }
154 EXPECT_EQ(2ul, transformed.second.size());
155
156 result = storm::api::verifyWithSparseEngine(transformed.first, storm::api::createTask<double>(transformed.second[0], true));
157 EXPECT_EQ(1, result->asExplicitQuantitativeCheckResult<double>()[initState]);
158 result = storm::api::verifyWithSparseEngine(model, storm::api::createTask<double>(transformed.second[1], true));
159 EXPECT_NEAR(0.08606881472, result->asExplicitQuantitativeCheckResult<double>()[initState], 1e-6);
160 // result = storm::api::verifyWithSparseEngine(model, storm::api::createTask<double>(transformed.second[2], true));
161 // EXPECT_NEAR(3333.333333, result->asExplicitQuantitativeCheckResult<double>()[initState], 1e-6);
162}
163
164TEST(NonMarkovianChainTransformerTest, ChainElimination2ExampleTest) {
165 auto model = storm::parser::DirectEncodingParser<double>::parseModel(STORM_TEST_RESOURCES_DIR "/ma/chain_elimination2.drn")
166 ->template as<storm::models::sparse::MarkovAutomaton<double>>();
167 std::string formulasString = "Pmin=? [ F \"Fail\"];Pmin=? [ F<=300 \"Fail\"];Tmin=? [ F \"Fail\" ]";
168 auto formulas = storm::api::extractFormulasFromProperties(storm::api::parseProperties(formulasString));
169
170 EXPECT_EQ(10ul, model->getNumberOfStates());
171 EXPECT_EQ(14ul, model->getNumberOfTransitions());
172 ASSERT_TRUE(model->isOfType(storm::models::ModelType::MarkovAutomaton));
173 size_t initState = 0;
174
175 auto labeling = model->getStateLabeling();
176 ASSERT_TRUE(labeling.getStateHasLabel("init", initState));
177 ASSERT_TRUE(labeling.getStateHasLabel("Fail", 4));
178 ASSERT_TRUE(labeling.getStateHasLabel("Fail", 7));
179 ASSERT_TRUE(labeling.getStateHasLabel("Fail", 8));
180 ASSERT_TRUE(labeling.getStateHasLabel("Fail", 9));
181
182 auto result = storm::api::verifyWithSparseEngine(model, storm::api::createTask<double>(formulas[0], true));
183 EXPECT_EQ(1, result->asExplicitQuantitativeCheckResult<double>()[initState]);
184 result = storm::api::verifyWithSparseEngine(model, storm::api::createTask<double>(formulas[1], true));
185 EXPECT_NEAR(0.791015319, result->asExplicitQuantitativeCheckResult<double>()[initState], 1e-6);
186 result = storm::api::verifyWithSparseEngine(model, storm::api::createTask<double>(formulas[2], true));
187 EXPECT_NEAR(190, result->asExplicitQuantitativeCheckResult<double>()[initState], 1e-6);
188
189 // Keep labels
190 auto transformed = storm::api::eliminateNonMarkovianChains(model, formulas, storm::transformer::EliminationLabelBehavior::KeepLabels);
191 ASSERT_EQ(7ul, transformed.first->getNumberOfStates());
192 ASSERT_EQ(11ul, transformed.first->getNumberOfTransitions());
193 labeling = transformed.first->getStateLabeling();
194 ASSERT_TRUE(labeling.getStateHasLabel("init", initState));
195 ASSERT_TRUE(labeling.getStateHasLabel("Fail", 2));
196 ASSERT_TRUE(labeling.getStateHasLabel("Fail", 5));
197 ASSERT_TRUE(labeling.getStateHasLabel("Fail", 6));
198 EXPECT_EQ(2ul, transformed.second.size());
199
200 result = storm::api::verifyWithSparseEngine(transformed.first, storm::api::createTask<double>(transformed.second[0], true));
201 EXPECT_EQ(1, result->asExplicitQuantitativeCheckResult<double>()[initState]);
202 result = storm::api::verifyWithSparseEngine(model, storm::api::createTask<double>(transformed.second[1], true));
203 EXPECT_NEAR(0.791015319, result->asExplicitQuantitativeCheckResult<double>()[initState], 1e-6);
204 // result = storm::api::verifyWithSparseEngine(model, storm::api::createTask<double>(transformed.second[2], true));
205 // EXPECT_NEAR(190, result->asExplicitQuantitativeCheckResult<double>()[initState], 1e-6);
206
207 // Merge labels
208 transformed = storm::api::eliminateNonMarkovianChains(model, formulas, storm::transformer::EliminationLabelBehavior::MergeLabels);
209 ASSERT_EQ(5ul, transformed.first->getNumberOfStates());
210 ASSERT_EQ(10ul, transformed.first->getNumberOfTransitions());
211 labeling = transformed.first->getStateLabeling();
212 ASSERT_TRUE(labeling.getStateHasLabel("init", initState));
213 ASSERT_TRUE(labeling.getStateHasLabel("Fail", 1));
214 ASSERT_TRUE(labeling.getStateHasLabel("Fail", 2));
215 ASSERT_FALSE(labeling.getStateHasLabel("Fail", 3));
216 ASSERT_TRUE(labeling.getStateHasLabel("Fail", 4));
217 EXPECT_EQ(2ul, transformed.second.size());
218
219 result = storm::api::verifyWithSparseEngine(transformed.first, storm::api::createTask<double>(transformed.second[0], true));
220 EXPECT_EQ(1, result->asExplicitQuantitativeCheckResult<double>()[initState]);
221 result = storm::api::verifyWithSparseEngine(model, storm::api::createTask<double>(transformed.second[1], true));
222 EXPECT_NEAR(0.791015319, result->asExplicitQuantitativeCheckResult<double>()[initState], 1e-6);
223 // result = storm::api::verifyWithSparseEngine(model, storm::api::createTask<double>(transformed.second[2], true));
224 // EXPECT_NEAR(190, result->asExplicitQuantitativeCheckResult<double>()[initState], 1e-6);
225
226 // Delete labels
227 transformed = storm::api::eliminateNonMarkovianChains(model, formulas, storm::transformer::EliminationLabelBehavior::DeleteLabels);
228 ASSERT_EQ(5ul, transformed.first->getNumberOfStates());
229 ASSERT_EQ(10ul, transformed.first->getNumberOfTransitions());
230 labeling = transformed.first->getStateLabeling();
231 ASSERT_TRUE(labeling.getStateHasLabel("init", initState));
232 ASSERT_TRUE(labeling.getStateHasLabel("Fail", 1));
233 ASSERT_FALSE(labeling.getStateHasLabel("Fail", 2));
234 ASSERT_FALSE(labeling.getStateHasLabel("Fail", 3));
235 ASSERT_TRUE(labeling.getStateHasLabel("Fail", 4));
236 EXPECT_EQ(2ul, transformed.second.size());
237
238 result = storm::api::verifyWithSparseEngine(transformed.first, storm::api::createTask<double>(transformed.second[0], true));
239 EXPECT_EQ(1, result->asExplicitQuantitativeCheckResult<double>()[initState]);
240 result = storm::api::verifyWithSparseEngine(model, storm::api::createTask<double>(transformed.second[1], true));
241 EXPECT_NEAR(0.791015319, result->asExplicitQuantitativeCheckResult<double>()[initState], 1e-6);
242 // result = storm::api::verifyWithSparseEngine(model, storm::api::createTask<double>(transformed.second[2], true));
243 // EXPECT_NEAR(190, result->asExplicitQuantitativeCheckResult<double>()[initState], 1e-6);
244}
TEST
TEST(NonMarkovianChainTransformerTest, StreamExampleTest)
Definition NonMarkovianChainTransformerTest.cpp:9
storm::parser::DirectEncodingParser::parseModel
static std::shared_ptr< storm::models::sparse::Model< ValueType, RewardModelType > > parseModel(std::string const &fil, DirectEncodingParserOptions const &options=DirectEncodingParserOptions())
Load a model in DRN format from a file and create the model.
Definition DirectEncodingParser.cpp:34
storm::parser::PrismParser::parse
static storm::prism::Program parse(std::string const &filename, bool prismCompatability=false)
Parses the given file into the PRISM storage classes assuming it complies with the PRISM syntax.
Definition PrismParser.cpp:5
storm::api::parsePropertiesForPrismProgram
std::vector< storm::jani::Property > parsePropertiesForPrismProgram(std::string const &inputString, storm::prism::Program const &program, boost::optional< std::set< std::string > > const &propertyFilter)
Definition properties.cpp:69
storm::api::eliminateNonMarkovianChains
std::pair< std::shared_ptr< storm::models::sparse::Model< ValueType > >, std::vector< std::shared_ptr< storm::logic::Formula const > > > eliminateNonMarkovianChains(std::shared_ptr< storm::models::sparse::MarkovAutomaton< ValueType > > const &ma, std::vector< std::shared_ptr< storm::logic::Formula const > > const &formulas, storm::transformer::EliminationLabelBehavior labelBehavior)
Eliminates chains of non-Markovian states from a given Markov Automaton.
Definition transformation.h:21
storm::api::parseProperties
std::vector< storm::jani::Property > parseProperties(storm::parser::FormulaParser &formulaParser, std::string const &inputString, boost::optional< std::set< std::string > > const &propertyFilter)
Definition properties.cpp:27
storm::api::extractFormulasFromProperties
std::vector< std::shared_ptr< storm::logic::Formula const > > extractFormulasFromProperties(std::vector< storm::jani::Property > const &properties)
Definition properties.cpp:64
storm::api::verifyWithSparseEngine
std::unique_ptr< storm::modelchecker::CheckResult > verifyWithSparseEngine(storm::Environment const &env, std::shared_ptr< storm::models::sparse::Dtmc< ValueType > > const &dtmc, storm::modelchecker::CheckTask< storm::logic::Formula, ValueType > const &task)
Definition verification.h:95
storm_gtest.h