47 model->getManager().execute([&]() {
52 EXPECT_EQ(11ul, quotient->getNumberOfStates());
53 EXPECT_EQ(17ul, quotient->getNumberOfTransitions());
55 EXPECT_TRUE(quotient->isSymbolicModel());
60 std::vector<std::shared_ptr<storm::logic::Formula const>> formulas;
61 formulas.push_back(formula);
67 EXPECT_EQ(5ul, quotient->getNumberOfStates());
68 EXPECT_EQ(8ul, quotient->getNumberOfTransitions());
70 EXPECT_TRUE(quotient->isSymbolicModel());
80 model->getManager().execute([&]() {
85 ASSERT_TRUE(quotient->isSymbolicModel());
95 std::pair<double, double> resultBounds;
97 std::unique_ptr<storm::modelchecker::CheckResult> result = checker.check(*minFormula);
99 resultBounds.first = result->asQuantitativeCheckResult<
double>().sum();
100 result = checker.check(*maxFormula);
102 resultBounds.second = result->asQuantitativeCheckResult<
double>().sum();
104 EXPECT_EQ(resultBounds.first, storm::utility::zero<double>());
105 EXPECT_EQ(resultBounds.second, storm::utility::one<double>());
112 ASSERT_TRUE(quotient->isSymbolicModel());
117 result = checker2.check(*minFormula);
119 resultBounds.first = result->asQuantitativeCheckResult<
double>().sum();
120 result = checker2.check(*maxFormula);
122 resultBounds.second = result->asQuantitativeCheckResult<
double>().sum();
124 EXPECT_EQ(resultBounds.first, storm::utility::zero<double>());
125 EXPECT_NEAR(resultBounds.second,
static_cast<double>(1) / 3, 1e-6);
132 ASSERT_TRUE(quotient->isSymbolicModel());
137 result = checker3.check(*minFormula);
139 resultBounds.first = result->asQuantitativeCheckResult<
double>().sum();
140 result = checker3.check(*maxFormula);
142 resultBounds.second = result->asQuantitativeCheckResult<
double>().sum();
144 EXPECT_NEAR(resultBounds.first,
static_cast<double>(1) / 6, 1e-6);
145 EXPECT_NEAR(resultBounds.second,
static_cast<double>(1) / 6, 1e-6);
146 EXPECT_NEAR(resultBounds.first, resultBounds.second, 1e-6);
152 ASSERT_TRUE(quotient->isSymbolicModel());
159 result = checker4.check(*formula);
161 resultBounds.first = resultBounds.second = result->asQuantitativeCheckResult<
double>().sum();
163 EXPECT_NEAR(resultBounds.first,
static_cast<double>(1) / 6, 1e-6);
176 model->getManager().execute([&]() {
181 EXPECT_EQ(2007ul, quotient->getNumberOfStates());
182 EXPECT_EQ(3738ul, quotient->getNumberOfTransitions());
184 EXPECT_TRUE(quotient->isSymbolicModel());
189 std::vector<std::shared_ptr<storm::logic::Formula const>> formulas;
190 formulas.push_back(formula);
196 EXPECT_EQ(65ul, quotient->getNumberOfStates());
197 EXPECT_EQ(105ul, quotient->getNumberOfTransitions());
199 EXPECT_TRUE(quotient->isSymbolicModel());
209 model->getManager().execute([&]() {
214 EXPECT_EQ(77ul, quotient->getNumberOfStates());
215 EXPECT_EQ(210ul, quotient->getNumberOfTransitions());
217 EXPECT_TRUE(quotient->isSymbolicModel());
223 std::vector<std::shared_ptr<storm::logic::Formula const>> formulas;
224 formulas.push_back(formula);
230 EXPECT_EQ(11ul, quotient->getNumberOfStates());
231 EXPECT_EQ(34ul, quotient->getNumberOfTransitions());
233 EXPECT_TRUE(quotient->isSymbolicModel());
248 std::shared_ptr<storm::models::symbolic::Model<DdType, double>> model =
251 model->getManager().execute([&]() {
256 EXPECT_EQ(252ul, quotient->getNumberOfStates());
257 EXPECT_EQ(624ul, quotient->getNumberOfTransitions());
259 EXPECT_TRUE(quotient->isSymbolicModel());
262 std::vector<std::shared_ptr<storm::logic::Formula const>> formulas;
263 formulas.push_back(formula);
269 EXPECT_EQ(1107ul, quotient->getNumberOfStates());
270 EXPECT_EQ(2684ul, quotient->getNumberOfTransitions());
272 EXPECT_TRUE(quotient->isSymbolicModel());