Storm 1.10.0.1
A Modern Probabilistic Model Checker
Loading...
Searching...
No Matches
ExplicitPrismModelBuilderTest.cpp
Go to the documentation of this file.
2#include "storm-config.h"
9#include "test/storm_gtest.h"
10
11class ExplicitPrismModelBuilderTest : public ::testing::Test {
12 protected:
13 void SetUp() override {
14#ifndef STORM_HAVE_Z3
15 GTEST_SKIP() << "Z3 not available.";
16#endif
17 }
18};
19
21 storm::prism::Program program = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/dtmc/die.pm");
22
23 std::shared_ptr<storm::models::sparse::Model<double>> model = storm::builder::ExplicitModelBuilder<double>(program).build();
24 EXPECT_EQ(13ul, model->getNumberOfStates());
25 EXPECT_EQ(20ul, model->getNumberOfTransitions());
26
27 program = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/dtmc/brp-16-2.pm");
29 EXPECT_EQ(677ul, model->getNumberOfStates());
30 EXPECT_EQ(867ul, model->getNumberOfTransitions());
31
32 program = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/dtmc/crowds-5-5.pm");
34 EXPECT_EQ(8607ul, model->getNumberOfStates());
35 EXPECT_EQ(15113ul, model->getNumberOfTransitions());
36
37 program = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/dtmc/leader-3-5.pm");
39 EXPECT_EQ(273ul, model->getNumberOfStates());
40 EXPECT_EQ(397ul, model->getNumberOfTransitions());
41
42 program = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/dtmc/nand-5-2.pm");
44 EXPECT_EQ(1728ul, model->getNumberOfStates());
45 EXPECT_EQ(2505ul, model->getNumberOfTransitions());
46}
47
49 storm::prism::Program program = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/ctmc/cluster2.sm", true);
50
51 std::shared_ptr<storm::models::sparse::Model<double>> model = storm::builder::ExplicitModelBuilder<double>(program).build();
52 EXPECT_EQ(276ul, model->getNumberOfStates());
53 EXPECT_EQ(1120ul, model->getNumberOfTransitions());
54
55 program = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/ctmc/embedded2.sm", true);
57 EXPECT_EQ(3478ul, model->getNumberOfStates());
58 EXPECT_EQ(14639ul, model->getNumberOfTransitions());
59
60 program = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/ctmc/polling2.sm", true);
62 EXPECT_EQ(12ul, model->getNumberOfStates());
63 EXPECT_EQ(22ul, model->getNumberOfTransitions());
64
65 program = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/ctmc/fms2.sm", true);
67 EXPECT_EQ(810ul, model->getNumberOfStates());
68 EXPECT_EQ(3699ul, model->getNumberOfTransitions());
69
70 program = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/ctmc/tandem5.sm", true);
72 EXPECT_EQ(66ul, model->getNumberOfStates());
73 EXPECT_EQ(189ul, model->getNumberOfTransitions());
74}
75
77 storm::prism::Program program = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/mdp/two_dice.nm");
78 std::shared_ptr<storm::models::sparse::Model<double>> model = storm::builder::ExplicitModelBuilder<double>(program).build();
79 EXPECT_EQ(169ul, model->getNumberOfStates());
80 EXPECT_EQ(436ul, model->getNumberOfTransitions());
81
82 program = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/mdp/leader3.nm");
84 EXPECT_EQ(364ul, model->getNumberOfStates());
85 EXPECT_EQ(654ul, model->getNumberOfTransitions());
86
87 program = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/mdp/coin2-2.nm");
89 EXPECT_EQ(272ul, model->getNumberOfStates());
90 EXPECT_EQ(492ul, model->getNumberOfTransitions());
91
92 program = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/mdp/csma2-2.nm");
94 EXPECT_EQ(1038ul, model->getNumberOfStates());
95 EXPECT_EQ(1282ul, model->getNumberOfTransitions());
96
97 program = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/mdp/firewire3-0.5.nm");
99 EXPECT_EQ(4093ul, model->getNumberOfStates());
100 EXPECT_EQ(5585ul, model->getNumberOfTransitions());
101
102 program = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/mdp/wlan0-2-2.nm");
104 EXPECT_EQ(37ul, model->getNumberOfStates());
105 EXPECT_EQ(59ul, model->getNumberOfTransitions());
106
107 storm::storage::SymbolicModelDescription modelDescription = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/mdp/unbounded.nm");
108 program = modelDescription.preprocess("N=-7").asPrismProgram();
110 EXPECT_EQ(9ul, model->getNumberOfStates());
111 EXPECT_EQ(9ul, model->getNumberOfTransitions());
112
113 program = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/mdp/enumerate_init.prism");
115 EXPECT_EQ(36ul, model->getNumberOfStates());
116 EXPECT_EQ(66ul, model->getNumberOfTransitions());
117 EXPECT_EQ(36ul, model->getInitialStates().getNumberOfSetBits());
118
119 program = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/mdp/sync.nm");
121 EXPECT_EQ(5ul, model->getNumberOfStates());
122 EXPECT_EQ(24ul, model->getNumberOfTransitions());
123 EXPECT_EQ(12ul, model->getNumberOfChoices());
124}
125
127 storm::prism::Program program = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/ma/simple.ma");
128
129 std::shared_ptr<storm::models::sparse::Model<double>> model = storm::builder::ExplicitModelBuilder<double>(program).build();
130 EXPECT_EQ(5ul, model->getNumberOfStates());
131 EXPECT_EQ(8ul, model->getNumberOfTransitions());
132 ASSERT_TRUE(model->isOfType(storm::models::ModelType::MarkovAutomaton));
134
135 program = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/ma/hybrid_states.ma");
137 EXPECT_EQ(5ul, model->getNumberOfStates());
138 EXPECT_EQ(13ul, model->getNumberOfTransitions());
139 ASSERT_TRUE(model->isOfType(storm::models::ModelType::MarkovAutomaton));
141
142 program = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/ma/stream2.ma");
144 EXPECT_EQ(12ul, model->getNumberOfStates());
145 EXPECT_EQ(14ul, model->getNumberOfTransitions());
146 ASSERT_TRUE(model->isOfType(storm::models::ModelType::MarkovAutomaton));
148}
149
151 storm::prism::Program program = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/pomdp/simple.prism");
152 program = storm::utility::prism::preprocess(program, "slippery=0.4");
153 std::shared_ptr<storm::models::sparse::Model<double>> model = storm::builder::ExplicitModelBuilder<double>(program).build();
154
155 program = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/pomdp/globalvars.prism");
157
158 program = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/pomdp/maze2.prism");
159 program = storm::utility::prism::preprocess(program, "sl=0.4");
161
162 program = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/pomdp/refuel.prism");
163 program = storm::utility::prism::preprocess(program, "N=5");
165}
166
168 storm::prism::Program program = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/imdp/robot.prism");
169 program = storm::utility::prism::preprocess(program, "delta=0.2");
170 std::shared_ptr<storm::models::sparse::Model<storm::Interval>> model = storm::builder::ExplicitModelBuilder<storm::Interval>(program).build();
171
172 program = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/imdp/coin2.prism");
173 program = storm::utility::prism::preprocess(program, "K=2,bias1=0.1");
175}
176
178 storm::prism::Program program = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/smg/action_labels.prism");
179 program = storm::utility::prism::preprocess(program, "");
180 std::shared_ptr<storm::models::sparse::Model<double>> model = storm::builder::ExplicitModelBuilder<double>(program).build();
181 EXPECT_EQ(3ul, model->getNumberOfStates());
182 EXPECT_EQ(3ul, model->getNumberOfChoices());
183 EXPECT_EQ(6ul, model->getNumberOfTransitions());
184}
185
187 storm::prism::Program program = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/mdp/system_composition.nm");
188
189 STORM_SILENT_ASSERT_THROW(storm::builder::ExplicitModelBuilder<double>(program).build(), storm::exceptions::WrongFormatException);
190}
191
193 storm::storage::SymbolicModelDescription modelDescription = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/mdp/unbounded.nm");
194 storm::prism::Program program = modelDescription.preprocess("N=7").asPrismProgram();
195 STORM_SILENT_ASSERT_THROW(storm::builder::ExplicitModelBuilder<double>(program).build(), storm::exceptions::WrongFormatException);
196}
197
198TEST_F(ExplicitPrismModelBuilderTest, ExportExplicitLookup) {
199 storm::prism::Program program = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/dtmc/die.pm");
201 generatorOptions.setBuildAllLabels();
202 auto builder = storm::builder::ExplicitModelBuilder<double>(program, generatorOptions);
203 std::shared_ptr<storm::models::sparse::Model<double>> model = builder.build();
204 auto lookup = builder.exportExplicitStateLookup();
205 auto svar = program.getModules()[0].getIntegerVariable("s").getExpressionVariable();
206 auto dvar = program.getModules()[0].getIntegerVariable("d").getExpressionVariable();
207 auto& manager = program.getManager();
208 EXPECT_EQ(model->getNumberOfStates(), lookup.lookup({{svar, manager.integer(1)}, {dvar, manager.integer(2)}}));
209 EXPECT_TRUE(model->getNumberOfStates() > lookup.lookup({{svar, manager.integer(7)}, {dvar, manager.integer(2)}}));
210 EXPECT_EQ(1ul, model->getLabelsOfState(lookup.lookup({{svar, manager.integer(7)}, {dvar, manager.integer(2)}})).count("two"));
211}
212
214 return true;
215}
216
218 return false;
219}
220
222 return actionIndex <= 1;
223}
224
226 storm::prism::Program program = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/mdp/die_selection.nm");
228 generatorOptions.setBuildAllLabels();
229 generatorOptions.setBuildChoiceLabels();
230 std::shared_ptr<storm::generator::StateValuationFunctionMask<double>> mask_object =
231 std::make_shared<storm::generator::StateValuationFunctionMask<double>>(trivial_true_mask);
232 std::shared_ptr<storm::generator::PrismNextStateGenerator<double>> generator =
233 std::make_shared<storm::generator::PrismNextStateGenerator<double>>(program, generatorOptions, mask_object);
234 auto builder = storm::builder::ExplicitModelBuilder<double>(generator);
235
236 std::shared_ptr<storm::models::sparse::Model<double>> model = builder.build();
237 EXPECT_EQ(13ul, model->getNumberOfStates());
238 EXPECT_EQ(48ul, model->getNumberOfTransitions());
239
240 mask_object = std::make_shared<storm::generator::StateValuationFunctionMask<double>>(trivial_false_mask);
241 generator = std::make_shared<storm::generator::PrismNextStateGenerator<double>>(program, generatorOptions, mask_object);
243
244 model = builder.build();
245 EXPECT_EQ(1ul, model->getNumberOfStates());
246 EXPECT_EQ(1ul, model->getNumberOfTransitions());
247
248 mask_object = std::make_shared<storm::generator::StateValuationFunctionMask<double>>(only_first_action_mask);
249 generator = std::make_shared<storm::generator::PrismNextStateGenerator<double>>(program, generatorOptions, mask_object);
251
252 model = builder.build();
253 EXPECT_EQ(13ul, model->getNumberOfStates());
254 EXPECT_EQ(20ul, model->getNumberOfTransitions());
255}
TEST_F(ExplicitPrismModelBuilderTest, Dtmc)
bool trivial_false_mask(storm::expressions::SimpleValuation const &, uint64_t)
bool trivial_true_mask(storm::expressions::SimpleValuation const &, uint64_t)
bool only_first_action_mask(storm::expressions::SimpleValuation const &, uint64_t actionIndex)
BuilderOptions & setBuildAllLabels(bool newValue=true)
Should all reward models be built? If not set, only required reward models are build.
BuilderOptions & setBuildChoiceLabels(bool newValue=true)
Should the choice labels be built?
std::shared_ptr< storm::models::sparse::Model< ValueType, RewardModelType > > build()
Convert the program given at construction time to an abstract model.
A simple implementation of the valuation interface.
This class represents a discrete-time Markov chain.
Definition Dtmc.h:14
This class represents a Markov automaton.
storm::storage::BitVector const & getMarkovianStates() const
Retrieves the set of Markovian states of the model.
This class represents a (discrete-time) Markov decision process.
Definition Mdp.h:14
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.
std::vector< Module > const & getModules() const
Retrieves all modules of the program.
Definition Program.cpp:629
storm::expressions::ExpressionManager & getManager() const
Retrieves the manager responsible for the expressions of this program.
Definition Program.cpp:2378
uint64_t getNumberOfSetBits() const
Returns the number of bits that are set to true in this bit vector.
storm::prism::Program const & asPrismProgram() const
SymbolicModelDescription preprocess(std::string const &constantDefinitionString="") const
std::pair< storm::RationalNumber, storm::RationalNumber > count(std::vector< storm::storage::BitVector > const &origSets, std::vector< storm::storage::BitVector > const &intersects, std::vector< storm::storage::BitVector > const &intersectsInfo, storm::RationalNumber val, bool plus, uint64_t remdepth)
storm::prism::Program preprocess(storm::prism::Program const &program, std::map< storm::expressions::Variable, storm::expressions::Expression > const &constantDefinitions)
Definition prism.cpp:19
#define STORM_SILENT_ASSERT_THROW(statement, expected_exception)
Definition storm_gtest.h:99