24 EXPECT_EQ(13ul, model->getNumberOfStates());
25 EXPECT_EQ(20ul, model->getNumberOfTransitions());
29 EXPECT_EQ(677ul, model->getNumberOfStates());
30 EXPECT_EQ(867ul, model->getNumberOfTransitions());
34 EXPECT_EQ(8607ul, model->getNumberOfStates());
35 EXPECT_EQ(15113ul, model->getNumberOfTransitions());
39 EXPECT_EQ(273ul, model->getNumberOfStates());
40 EXPECT_EQ(397ul, model->getNumberOfTransitions());
44 EXPECT_EQ(1728ul, model->getNumberOfStates());
45 EXPECT_EQ(2505ul, model->getNumberOfTransitions());
52 EXPECT_EQ(276ul, model->getNumberOfStates());
53 EXPECT_EQ(1120ul, model->getNumberOfTransitions());
57 EXPECT_EQ(3478ul, model->getNumberOfStates());
58 EXPECT_EQ(14639ul, model->getNumberOfTransitions());
62 EXPECT_EQ(12ul, model->getNumberOfStates());
63 EXPECT_EQ(22ul, model->getNumberOfTransitions());
67 EXPECT_EQ(810ul, model->getNumberOfStates());
68 EXPECT_EQ(3699ul, model->getNumberOfTransitions());
72 EXPECT_EQ(66ul, model->getNumberOfStates());
73 EXPECT_EQ(189ul, model->getNumberOfTransitions());
79 EXPECT_EQ(169ul, model->getNumberOfStates());
80 EXPECT_EQ(436ul, model->getNumberOfTransitions());
84 EXPECT_EQ(364ul, model->getNumberOfStates());
85 EXPECT_EQ(654ul, model->getNumberOfTransitions());
89 EXPECT_EQ(272ul, model->getNumberOfStates());
90 EXPECT_EQ(492ul, model->getNumberOfTransitions());
94 EXPECT_EQ(1038ul, model->getNumberOfStates());
95 EXPECT_EQ(1282ul, model->getNumberOfTransitions());
99 EXPECT_EQ(4093ul, model->getNumberOfStates());
100 EXPECT_EQ(5585ul, model->getNumberOfTransitions());
104 EXPECT_EQ(37ul, model->getNumberOfStates());
105 EXPECT_EQ(59ul, model->getNumberOfTransitions());
110 EXPECT_EQ(9ul, model->getNumberOfStates());
111 EXPECT_EQ(9ul, model->getNumberOfTransitions());
115 EXPECT_EQ(36ul, model->getNumberOfStates());
116 EXPECT_EQ(66ul, model->getNumberOfTransitions());
117 EXPECT_EQ(36ul, model->getInitialStates().getNumberOfSetBits());
121 EXPECT_EQ(5ul, model->getNumberOfStates());
122 EXPECT_EQ(24ul, model->getNumberOfTransitions());
123 EXPECT_EQ(12ul, model->getNumberOfChoices());
130 EXPECT_EQ(5ul, model->getNumberOfStates());
131 EXPECT_EQ(8ul, model->getNumberOfTransitions());
137 EXPECT_EQ(5ul, model->getNumberOfStates());
138 EXPECT_EQ(13ul, model->getNumberOfTransitions());
144 EXPECT_EQ(12ul, model->getNumberOfStates());
145 EXPECT_EQ(14ul, model->getNumberOfTransitions());
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();
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"));
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);
236 std::shared_ptr<storm::models::sparse::Model<double>> model = builder.build();
237 EXPECT_EQ(13ul, model->getNumberOfStates());
238 EXPECT_EQ(48ul, model->getNumberOfTransitions());
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);
244 model = builder.build();
245 EXPECT_EQ(1ul, model->getNumberOfStates());
246 EXPECT_EQ(1ul, model->getNumberOfTransitions());
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);
252 model = builder.build();
253 EXPECT_EQ(13ul, model->getNumberOfStates());
254 EXPECT_EQ(20ul, model->getNumberOfTransitions());
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)