Storm 1.13.0.1
A Modern Probabilistic Model Checker
Loading...
Searching...
No Matches
LpSolverTest.cpp
Go to the documentation of this file.
1#include "storm-config.h"
2#include "test/storm_gtest.h"
3
4#include "storm/exceptions/InvalidAccessException.h"
5#include "storm/solver/GlpkLpSolver.h"
6#include "storm/solver/GurobiLpSolver.h"
7#include "storm/solver/LpSolver.h"
8#include "storm/solver/OptimizationDirection.h"
9#include "storm/storage/expressions/Expression.h"
10#include "storm/storage/expressions/Variable.h"
11#include "storm/utility/solver.h"
12#include "storm/utility/vector.h"
13
14namespace {
15
16class DefaultEnvironment {
17 public:
18 typedef double ValueType;
19 static const bool isExact = false;
20 static const storm::solver::LpSolverTypeSelection solverSelection = storm::solver::LpSolverTypeSelection::FROMSETTINGS;
21 static const bool IntegerSupport = true;
22 static const bool IncrementalSupport = true;
23 static const bool strictRelationSupport = true;
24
25 static bool skip() {
26#ifdef STORM_HAVE_LP_SOLVER
27 return false;
28#else
29 return true;
30#endif
31 }
32};
33
34class GlpkEnvironment {
35 public:
36 typedef double ValueType;
37 static const bool isExact = false;
38 static const storm::solver::LpSolverTypeSelection solverSelection = storm::solver::LpSolverTypeSelection::Glpk;
39 static const bool IntegerSupport = true;
40 static const bool IncrementalSupport = true;
41 static const bool strictRelationSupport = true;
42
43 static bool skip() {
44 return false;
45 }
46};
47
48#ifdef STORM_HAVE_GUROBI
49class GurobiEnvironment {
50 public:
51 typedef double ValueType;
52 static const bool isExact = false;
53 static const storm::solver::LpSolverTypeSelection solverSelection = storm::solver::LpSolverTypeSelection::Gurobi;
54 static const bool IntegerSupport = true;
55 static const bool IncrementalSupport = true;
56 static const bool strictRelationSupport = true;
57
58 static bool skip() {
59 return storm::test::noGurobi;
60 }
61};
62#endif
63
64class Z3Environment {
65 public:
66 typedef storm::RationalNumber ValueType;
67 static const bool isExact = true;
68 static const storm::solver::LpSolverTypeSelection solverSelection = storm::solver::LpSolverTypeSelection::Z3;
69 static const bool IntegerSupport = true;
70 static const bool IncrementalSupport = true;
71 static const bool strictRelationSupport = true;
72
73 static bool skip() {
74 return false;
75 }
76};
77
78#ifdef STORM_HAVE_SOPLEX
79class SoplexEnvironment {
80 public:
81 typedef double ValueType;
82 static const bool isExact = false;
83 static const storm::solver::LpSolverTypeSelection solverSelection = storm::solver::LpSolverTypeSelection::Soplex;
84 static const bool IntegerSupport = false;
85 static const bool IncrementalSupport = false;
86 static const bool strictRelationSupport = false;
87
88 static bool skip() {
89 return false;
90 }
91};
92
93class SoplexExactEnvironment {
94 public:
95 typedef storm::RationalNumber ValueType;
96 static const bool isExact = true;
97 static const storm::solver::LpSolverTypeSelection solverSelection = storm::solver::LpSolverTypeSelection::Soplex;
98 static const bool IntegerSupport = false;
99 static const bool IncrementalSupport = false;
100 static const bool strictRelationSupport = false;
101
102 static bool skip() {
103 return false;
104 }
105};
106#endif
107
108template<typename TestType>
109class LpSolverTest : public ::testing::Test {
110 public:
111 typedef typename TestType::ValueType ValueType;
112
113 void SetUp() override {
114 if (skipped()) {
115 GTEST_SKIP();
116 }
117 }
118
119 storm::solver::LpSolverTypeSelection solverSelection() const {
120 return TestType::solverSelection;
121 }
122
123 std::unique_ptr<storm::utility::solver::LpSolverFactory<ValueType>> factory() const {
124 return storm::utility::solver::getLpSolverFactory<ValueType>(solverSelection());
125 }
126
127 ValueType parseNumber(std::string const& input) const {
128 return storm::utility::convertNumber<ValueType>(input);
129 }
130
131 ValueType precision() const {
132 return TestType::isExact ? parseNumber("0") : parseNumber("1e-15");
133 }
134
135 bool supportsInteger() const {
136 return TestType::IntegerSupport;
137 }
138
139 bool supportsIncremental() const {
140 return TestType::IncrementalSupport;
141 }
142
143 bool supportsStrictRelation() const {
144 return TestType::strictRelationSupport;
145 }
146
147 bool skipped() const {
148 return TestType::skip();
149 }
150};
151
152typedef ::testing::Types<DefaultEnvironment
153#ifdef STORM_HAVE_GLPK
154 ,
155 GlpkEnvironment
156#endif
157#ifdef STORM_HAVE_GUROBI
158 ,
159 GurobiEnvironment
160#endif
161#ifdef STORM_HAVE_SOPLEX
162 ,
163 SoplexEnvironment, SoplexExactEnvironment
164#endif
165#ifdef STORM_HAVE_Z3
166 ,
167 Z3Environment
168#endif
169 >
170 TestingTypes;
171
172TYPED_TEST_SUITE(LpSolverTest, TestingTypes, );
173
174TYPED_TEST(LpSolverTest, LPOptimizeMax) {
175 auto solver = this->factory()->create("");
176 solver->setOptimizationDirection(storm::OptimizationDirection::Maximize);
177 storm::expressions::Variable x;
178 storm::expressions::Variable y;
179 storm::expressions::Variable z;
180 ASSERT_NO_THROW(x = solver->addBoundedContinuousVariable("x", 0, 1, -1));
181 ASSERT_NO_THROW(y = solver->addLowerBoundedContinuousVariable("y", 0, 2));
182 ASSERT_NO_THROW(z = solver->addLowerBoundedContinuousVariable("z", 0, 1));
183 ASSERT_NO_THROW(solver->update());
184
185 ASSERT_NO_THROW(solver->addConstraint("", x + y + z <= solver->getConstant(12)));
186 ASSERT_NO_THROW(solver->addConstraint("", solver->getConstant(this->parseNumber("1/2")) * y + z - x == solver->getConstant(5)));
187 ASSERT_NO_THROW(solver->addConstraint("", y - x <= solver->getConstant(this->parseNumber("11/2"))));
188 ASSERT_NO_THROW(solver->update());
189
190 ASSERT_NO_THROW(solver->optimize());
191 ASSERT_TRUE(solver->isOptimal());
192 ASSERT_FALSE(solver->isUnbounded());
193 ASSERT_FALSE(solver->isInfeasible());
194 EXPECT_NEAR(this->parseNumber("1"), solver->getContinuousValue(x), this->precision());
195 EXPECT_NEAR(this->parseNumber("13/2"), solver->getContinuousValue(y), this->precision());
196 EXPECT_NEAR(this->parseNumber("11/4"), solver->getContinuousValue(z), this->precision());
197 EXPECT_NEAR(this->parseNumber("59/4"), solver->getObjectiveValue(), this->precision());
198}
199
200TYPED_TEST(LpSolverTest, LPOptimizeMaxRaw) {
201 typedef typename TestFixture::ValueType ValueType;
202 auto solver = this->factory()->createRaw("");
203 solver->setOptimizationDirection(storm::OptimizationDirection::Maximize);
204 ASSERT_EQ(0u, solver->addBoundedContinuousVariable("x", 0, 1, -1));
205 ASSERT_EQ(1u, solver->addLowerBoundedContinuousVariable("y", 0, 2));
206 ASSERT_EQ(2u, solver->addLowerBoundedContinuousVariable("z", 0, 1));
207 ASSERT_NO_THROW(solver->update());
208
209 // x + y + z <= 12
210 storm::solver::RawLpConstraint<ValueType> constraint1(storm::expressions::RelationType::LessOrEqual, this->parseNumber("12"), 3);
211 constraint1.addToLhs(0, this->parseNumber("1"));
212 constraint1.addToLhs(1, this->parseNumber("1"));
213 constraint1.addToLhs(2, this->parseNumber("1"));
214 ASSERT_NO_THROW(solver->addConstraint("", constraint1));
215 // -x + 1/2 * y + z == 5
216 storm::solver::RawLpConstraint<ValueType> constraint2(storm::expressions::RelationType::Equal, this->parseNumber("5"), 3);
217 constraint2.addToLhs(0, -this->parseNumber("1"));
218 constraint2.addToLhs(1, this->parseNumber("1/2"));
219 constraint2.addToLhs(2, this->parseNumber("1"));
220 ASSERT_NO_THROW(solver->addConstraint("", constraint2));
221 // -x + y <= 11/2
222 storm::solver::RawLpConstraint<ValueType> constraint3(storm::expressions::RelationType::LessOrEqual, this->parseNumber("11/2"), 2);
223 constraint3.addToLhs(0, -this->parseNumber("1"));
224 constraint3.addToLhs(1, this->parseNumber("1"));
225 ASSERT_NO_THROW(solver->addConstraint("", constraint3));
226 ASSERT_NO_THROW(solver->update());
227
228 ASSERT_NO_THROW(solver->optimize());
229 ASSERT_TRUE(solver->isOptimal());
230 ASSERT_FALSE(solver->isUnbounded());
231 ASSERT_FALSE(solver->isInfeasible());
232 EXPECT_NEAR(this->parseNumber("1"), solver->getContinuousValue(0), this->precision());
233 EXPECT_NEAR(this->parseNumber("13/2"), solver->getContinuousValue(1), this->precision());
234 EXPECT_NEAR(this->parseNumber("11/4"), solver->getContinuousValue(2), this->precision());
235 EXPECT_NEAR(this->parseNumber("59/4"), solver->getObjectiveValue(), this->precision());
236}
237
238TYPED_TEST(LpSolverTest, LPOptimizeMin) {
239 auto solver = this->factory()->create("");
240 solver->setOptimizationDirection(storm::OptimizationDirection::Minimize);
241 storm::expressions::Variable x;
242 storm::expressions::Variable y;
243 storm::expressions::Variable z;
244 ASSERT_NO_THROW(x = solver->addBoundedContinuousVariable("x", 0, 1, -1));
245 ASSERT_NO_THROW(y = solver->addLowerBoundedContinuousVariable("y", 0, 2));
246 ASSERT_NO_THROW(z = solver->addBoundedContinuousVariable("z", 1, this->parseNumber("57/10"), -1));
247 ASSERT_NO_THROW(solver->update());
248
249 ASSERT_NO_THROW(solver->addConstraint("", x + y + z <= solver->getConstant(12)));
250 ASSERT_NO_THROW(solver->addConstraint("", solver->getConstant(this->parseNumber("1/2")) * y + z - x <= solver->getConstant(5)));
251 ASSERT_NO_THROW(solver->addConstraint("", y - x <= solver->getConstant(this->parseNumber("11/2"))));
252 ASSERT_NO_THROW(solver->update());
253
254 ASSERT_NO_THROW(solver->optimize());
255 ASSERT_TRUE(solver->isOptimal());
256 ASSERT_FALSE(solver->isUnbounded());
257 ASSERT_FALSE(solver->isInfeasible());
258
259 EXPECT_NEAR(this->parseNumber("1"), solver->getContinuousValue(x), this->precision());
260 EXPECT_NEAR(this->parseNumber("0"), solver->getContinuousValue(y), this->precision());
261 EXPECT_NEAR(this->parseNumber("57/10"), solver->getContinuousValue(z), this->precision());
262 EXPECT_NEAR(this->parseNumber("-67/10"), solver->getObjectiveValue(), this->precision());
263}
264
265TYPED_TEST(LpSolverTest, LPOptimizeMinRaw) {
266 typedef typename TestFixture::ValueType ValueType;
267 auto solver = this->factory()->createRaw("");
268 solver->setOptimizationDirection(storm::OptimizationDirection::Minimize);
269
270 ASSERT_EQ(0u, solver->addBoundedContinuousVariable("x", 0, 1, -1));
271 ASSERT_EQ(1u, solver->addLowerBoundedContinuousVariable("y", 0, 2));
272 ASSERT_EQ(2u, solver->addBoundedContinuousVariable("z", 1, this->parseNumber("57/10"), -1));
273 ASSERT_NO_THROW(solver->update());
274
275 // x + y + z <= 12
276 storm::solver::RawLpConstraint<ValueType> constraint1(storm::expressions::RelationType::LessOrEqual, this->parseNumber("12"), 3);
277 constraint1.addToLhs(0, this->parseNumber("1"));
278 constraint1.addToLhs(1, this->parseNumber("1"));
279 constraint1.addToLhs(2, this->parseNumber("1"));
280 ASSERT_NO_THROW(solver->addConstraint("", constraint1));
281 // -x + 1/2 * y + z <= 5
282 storm::solver::RawLpConstraint<ValueType> constraint2(storm::expressions::RelationType::LessOrEqual, this->parseNumber("5"), 3);
283 constraint2.addToLhs(0, -this->parseNumber("1"));
284 constraint2.addToLhs(1, this->parseNumber("1/2"));
285 constraint2.addToLhs(2, this->parseNumber("1"));
286 ASSERT_NO_THROW(solver->addConstraint("", constraint2));
287 // -x + y <= 11/2
288 storm::solver::RawLpConstraint<ValueType> constraint3(storm::expressions::RelationType::LessOrEqual, this->parseNumber("11/2"), 2);
289 constraint3.addToLhs(0, -this->parseNumber("1"));
290 constraint3.addToLhs(1, this->parseNumber("1"));
291 ASSERT_NO_THROW(solver->addConstraint("", constraint3));
292 ASSERT_NO_THROW(solver->update());
293
294 ASSERT_NO_THROW(solver->optimize());
295 ASSERT_TRUE(solver->isOptimal());
296 ASSERT_FALSE(solver->isUnbounded());
297 ASSERT_FALSE(solver->isInfeasible());
298
299 EXPECT_NEAR(this->parseNumber("1"), solver->getContinuousValue(0), this->precision());
300 EXPECT_NEAR(this->parseNumber("0"), solver->getContinuousValue(1), this->precision());
301 EXPECT_NEAR(this->parseNumber("57/10"), solver->getContinuousValue(2), this->precision());
302 EXPECT_NEAR(this->parseNumber("-67/10"), solver->getObjectiveValue(), this->precision());
303}
304
305TYPED_TEST(LpSolverTest, MILPOptimizeMax) {
306 if (!this->supportsInteger()) {
307 GTEST_SKIP();
308 }
309 auto solver = this->factory()->create("");
310 solver->setOptimizationDirection(storm::OptimizationDirection::Maximize);
311 storm::expressions::Variable x;
312 storm::expressions::Variable y;
313 storm::expressions::Variable z;
314 ASSERT_NO_THROW(x = solver->addBinaryVariable("x", -1));
315 ASSERT_NO_THROW(y = solver->addLowerBoundedIntegerVariable("y", 0, 2));
316 ASSERT_NO_THROW(z = solver->addLowerBoundedContinuousVariable("z", 0, 1));
317 ASSERT_NO_THROW(solver->update());
318
319 ASSERT_NO_THROW(solver->addConstraint("", x + y + z <= solver->getConstant(12)));
320 ASSERT_NO_THROW(solver->addConstraint("", solver->getConstant(this->parseNumber("1/2")) * y + z - x == solver->getConstant(5)));
321 ASSERT_NO_THROW(solver->addConstraint("", y - x <= solver->getConstant(this->parseNumber("11/2"))));
322 ASSERT_NO_THROW(solver->update());
323 ASSERT_NO_THROW(solver->optimize());
324 ASSERT_TRUE(solver->isOptimal());
325 ASSERT_FALSE(solver->isUnbounded());
326 ASSERT_FALSE(solver->isInfeasible());
327
328 EXPECT_TRUE(solver->getBinaryValue(x));
329 EXPECT_EQ(6, solver->getIntegerValue(y));
330 EXPECT_NEAR(this->parseNumber("3"), solver->getContinuousValue(z), this->precision());
331 EXPECT_NEAR(this->parseNumber("14"), solver->getObjectiveValue(), this->precision());
332}
333
334TYPED_TEST(LpSolverTest, MILPOptimizeMaxRaw) {
335 if (!this->supportsInteger()) {
336 GTEST_SKIP();
337 }
338 typedef typename TestFixture::ValueType ValueType;
339 auto solver = this->factory()->createRaw("");
340 solver->setOptimizationDirection(storm::OptimizationDirection::Maximize);
341 storm::expressions::Variable x;
342 storm::expressions::Variable y;
343 storm::expressions::Variable z;
344 ASSERT_EQ(0u, solver->addBinaryVariable("x", -1));
345 ASSERT_EQ(1u, solver->addLowerBoundedIntegerVariable("y", 0, 2));
346 ASSERT_EQ(2u, solver->addLowerBoundedContinuousVariable("z", 0, 1));
347 ASSERT_NO_THROW(solver->update());
348
349 // x + y + z <= 12
350 storm::solver::RawLpConstraint<ValueType> constraint1(storm::expressions::RelationType::LessOrEqual, this->parseNumber("12"), 3);
351 constraint1.addToLhs(0, this->parseNumber("1"));
352 constraint1.addToLhs(1, this->parseNumber("1"));
353 constraint1.addToLhs(2, this->parseNumber("1"));
354 ASSERT_NO_THROW(solver->addConstraint("", constraint1));
355 // -x + 1/2 * y + z == 5
356 storm::solver::RawLpConstraint<ValueType> constraint2(storm::expressions::RelationType::Equal, this->parseNumber("5"), 3);
357 constraint2.addToLhs(0, -this->parseNumber("1"));
358 constraint2.addToLhs(1, this->parseNumber("1/2"));
359 constraint2.addToLhs(2, this->parseNumber("1"));
360 ASSERT_NO_THROW(solver->addConstraint("", constraint2));
361 // -x + y <= 11/2
362 storm::solver::RawLpConstraint<ValueType> constraint3(storm::expressions::RelationType::LessOrEqual, this->parseNumber("11/2"), 2);
363 constraint3.addToLhs(0, -this->parseNumber("1"));
364 constraint3.addToLhs(1, this->parseNumber("1"));
365 ASSERT_NO_THROW(solver->addConstraint("", constraint3));
366 ASSERT_NO_THROW(solver->update());
367
368 ASSERT_NO_THROW(solver->optimize());
369 ASSERT_TRUE(solver->isOptimal());
370 ASSERT_FALSE(solver->isUnbounded());
371 ASSERT_FALSE(solver->isInfeasible());
372 EXPECT_TRUE(solver->getBinaryValue(0));
373 EXPECT_EQ(6, solver->getIntegerValue(1));
374 EXPECT_NEAR(this->parseNumber("3"), solver->getContinuousValue(2), this->precision());
375 EXPECT_NEAR(this->parseNumber("14"), solver->getObjectiveValue(), this->precision());
376}
377
378TYPED_TEST(LpSolverTest, MILPOptimizeMin) {
379 if (!this->supportsInteger()) {
380 GTEST_SKIP();
381 }
382 auto solver = this->factory()->create("");
383 solver->setOptimizationDirection(storm::OptimizationDirection::Minimize);
384 storm::expressions::Variable x;
385 storm::expressions::Variable y;
386 storm::expressions::Variable z;
387 ASSERT_NO_THROW(x = solver->addBinaryVariable("x", -1));
388 ASSERT_NO_THROW(y = solver->addLowerBoundedIntegerVariable("y", 0, 2));
389 ASSERT_NO_THROW(z = solver->addBoundedContinuousVariable("z", 0, 5, -1));
390 ASSERT_NO_THROW(solver->update());
391
392 ASSERT_NO_THROW(solver->addConstraint("", x + y + z <= solver->getConstant(12)));
393 ASSERT_NO_THROW(solver->addConstraint("", solver->getConstant(this->parseNumber("1/2")) * y + z - x <= solver->getConstant(5)));
394 ASSERT_NO_THROW(solver->addConstraint("", y - x <= solver->getConstant(this->parseNumber("11/2"))));
395 ASSERT_NO_THROW(solver->update());
396
397#ifdef STORM_HAVE_Z3
398 if (this->solverSelection() == storm::solver::LpSolverTypeSelection::Z3 && storm::test::z3AtLeastVersion(4, 8, 8) &&
399 !storm::test::z3AtLeastVersion(4, 13, 3)) {
400 // z3 v4.8.8 is known to be broken here. It is working for v4.13.3.
401 GTEST_SKIP() << "Test disabled since it triggers a bug in the installed version of z3.";
402 }
403#endif
404
405 ASSERT_NO_THROW(solver->optimize());
406 ASSERT_TRUE(solver->isOptimal());
407 ASSERT_FALSE(solver->isUnbounded());
408 ASSERT_FALSE(solver->isInfeasible());
409
410 EXPECT_TRUE(solver->getBinaryValue(x));
411 EXPECT_EQ(0, solver->getIntegerValue(y));
412 EXPECT_NEAR(this->parseNumber("5"), solver->getContinuousValue(z), this->precision());
413 EXPECT_NEAR(this->parseNumber("-6"), solver->getObjectiveValue(), this->precision());
414}
415
416TYPED_TEST(LpSolverTest, LPInfeasible) {
417 auto solver = this->factory()->create("");
418 solver->setOptimizationDirection(storm::OptimizationDirection::Maximize);
419 storm::expressions::Variable x;
420 storm::expressions::Variable y;
421 storm::expressions::Variable z;
422 ASSERT_NO_THROW(x = solver->addBoundedContinuousVariable("x", 0, 1, -1));
423 ASSERT_NO_THROW(y = solver->addLowerBoundedContinuousVariable("y", 0, 2));
424 ASSERT_NO_THROW(z = solver->addLowerBoundedContinuousVariable("z", 0, 1));
425 ASSERT_NO_THROW(solver->update());
426
427 ASSERT_NO_THROW(solver->addConstraint("", x + y + z <= solver->getConstant(12)));
428 ASSERT_NO_THROW(solver->addConstraint("", solver->getConstant(this->parseNumber("1/2")) * y + z - x == solver->getConstant(5)));
429 ASSERT_NO_THROW(solver->addConstraint("", y - x <= solver->getConstant(this->parseNumber("11/2"))));
430 if (this->supportsStrictRelation()) {
431 ASSERT_NO_THROW(solver->addConstraint("", y > solver->getConstant((this->parseNumber("7")))));
432 } else {
433 ASSERT_NO_THROW(solver->addConstraint("", y >= solver->getConstant(this->parseNumber("7") + this->precision())));
434 }
435 ASSERT_NO_THROW(solver->update());
436
437 ASSERT_NO_THROW(solver->optimize());
438 ASSERT_FALSE(solver->isOptimal());
439 ASSERT_FALSE(solver->isUnbounded());
440 ASSERT_TRUE(solver->isInfeasible());
441 STORM_SILENT_ASSERT_THROW(solver->getContinuousValue(x), storm::exceptions::InvalidAccessException);
442 STORM_SILENT_ASSERT_THROW(solver->getContinuousValue(y), storm::exceptions::InvalidAccessException);
443 STORM_SILENT_ASSERT_THROW(solver->getContinuousValue(z), storm::exceptions::InvalidAccessException);
444 STORM_SILENT_ASSERT_THROW(solver->getObjectiveValue(), storm::exceptions::InvalidAccessException);
445}
446
447TYPED_TEST(LpSolverTest, MILPInfeasible) {
448 if (!this->supportsInteger()) {
449 GTEST_SKIP();
450 }
451 auto solver = this->factory()->create("");
452 solver->setOptimizationDirection(storm::OptimizationDirection::Maximize);
453 storm::expressions::Variable x;
454 storm::expressions::Variable y;
455 storm::expressions::Variable z;
456 ASSERT_NO_THROW(x = solver->addBinaryVariable("x", -1));
457 ASSERT_NO_THROW(y = solver->addLowerBoundedContinuousVariable("y", 0, 2));
458 ASSERT_NO_THROW(z = solver->addLowerBoundedContinuousVariable("z", 0, 1));
459 ASSERT_NO_THROW(solver->update());
460
461 ASSERT_NO_THROW(solver->addConstraint("", x + y + z <= solver->getConstant(12)));
462 ASSERT_NO_THROW(solver->addConstraint("", solver->getConstant(this->parseNumber("1/2")) * y + z - x == solver->getConstant(5)));
463 ASSERT_NO_THROW(solver->addConstraint("", y - x <= solver->getConstant(this->parseNumber("11/2"))));
464 if (this->supportsStrictRelation()) {
465 ASSERT_NO_THROW(solver->addConstraint("", y > solver->getConstant((this->parseNumber("7")))));
466 } else {
467 ASSERT_NO_THROW(solver->addConstraint("", y >= solver->getConstant(this->parseNumber("7") + this->precision())));
468 }
469 ASSERT_NO_THROW(solver->update());
470
471 ASSERT_NO_THROW(solver->optimize());
472 ASSERT_FALSE(solver->isOptimal());
473 ASSERT_FALSE(solver->isUnbounded());
474 ASSERT_TRUE(solver->isInfeasible());
475 STORM_SILENT_ASSERT_THROW(solver->getBinaryValue(x), storm::exceptions::InvalidAccessException);
476 STORM_SILENT_ASSERT_THROW(solver->getIntegerValue(y), storm::exceptions::InvalidAccessException);
477 STORM_SILENT_ASSERT_THROW(solver->getContinuousValue(z), storm::exceptions::InvalidAccessException);
478 STORM_SILENT_ASSERT_THROW(solver->getObjectiveValue(), storm::exceptions::InvalidAccessException);
479}
480
481TYPED_TEST(LpSolverTest, LPUnbounded) {
482 auto solver = this->factory()->create("");
483 solver->setOptimizationDirection(storm::OptimizationDirection::Maximize);
484 storm::expressions::Variable x;
485 storm::expressions::Variable y;
486 storm::expressions::Variable z;
487 ASSERT_NO_THROW(x = solver->addBoundedContinuousVariable("x", 0, 1, -1));
488 ASSERT_NO_THROW(y = solver->addLowerBoundedContinuousVariable("y", 0, 2));
489 ASSERT_NO_THROW(z = solver->addLowerBoundedContinuousVariable("z", 0, 1));
490 ASSERT_NO_THROW(solver->update());
491
492 ASSERT_NO_THROW(solver->addConstraint("", x + y - z <= solver->getConstant(12)));
493 ASSERT_NO_THROW(solver->addConstraint("", y - x <= solver->getConstant(this->parseNumber("11/2"))));
494 ASSERT_NO_THROW(solver->update());
495
496 ASSERT_NO_THROW(solver->optimize());
497 ASSERT_FALSE(solver->isOptimal());
498 ASSERT_TRUE(solver->isUnbounded());
499 ASSERT_FALSE(solver->isInfeasible());
500 STORM_SILENT_ASSERT_THROW(solver->getContinuousValue(x), storm::exceptions::InvalidAccessException);
501 STORM_SILENT_ASSERT_THROW(solver->getContinuousValue(y), storm::exceptions::InvalidAccessException);
502 STORM_SILENT_ASSERT_THROW(solver->getContinuousValue(z), storm::exceptions::InvalidAccessException);
503 STORM_SILENT_ASSERT_THROW(solver->getObjectiveValue(), storm::exceptions::InvalidAccessException);
504}
505
506TYPED_TEST(LpSolverTest, MILPUnbounded) {
507 if (!this->supportsInteger()) {
508 GTEST_SKIP();
509 }
510 auto solver = this->factory()->create("");
511 solver->setOptimizationDirection(storm::OptimizationDirection::Maximize);
512 storm::expressions::Variable x;
513 storm::expressions::Variable y;
514 storm::expressions::Variable z;
515 ASSERT_NO_THROW(x = solver->addBinaryVariable("x", -1));
516 ASSERT_NO_THROW(y = solver->addLowerBoundedContinuousVariable("y", 0, 2));
517 ASSERT_NO_THROW(z = solver->addLowerBoundedContinuousVariable("z", 0, 1));
518 ASSERT_NO_THROW(solver->update());
519
520 ASSERT_NO_THROW(solver->addConstraint("", x + y - z <= solver->getConstant(12)));
521 ASSERT_NO_THROW(solver->addConstraint("", y - x <= solver->getConstant(this->parseNumber("11/2"))));
522 ASSERT_NO_THROW(solver->update());
523
524 ASSERT_NO_THROW(solver->optimize());
525 ASSERT_FALSE(solver->isOptimal());
526 ASSERT_TRUE(solver->isUnbounded());
527 ASSERT_FALSE(solver->isInfeasible());
528 STORM_SILENT_ASSERT_THROW(solver->getBinaryValue(x), storm::exceptions::InvalidAccessException);
529 STORM_SILENT_ASSERT_THROW(solver->getIntegerValue(y), storm::exceptions::InvalidAccessException);
530 STORM_SILENT_ASSERT_THROW(solver->getContinuousValue(z), storm::exceptions::InvalidAccessException);
531 STORM_SILENT_ASSERT_THROW(solver->getObjectiveValue(), storm::exceptions::InvalidAccessException);
532}
533
534TYPED_TEST(LpSolverTest, Incremental) {
535 if (!this->supportsIncremental()) {
536 GTEST_SKIP();
537 }
538 auto solver = this->factory()->create("");
539 solver->setOptimizationDirection(storm::OptimizationDirection::Maximize);
540 storm::expressions::Variable x, y, z;
541 ASSERT_NO_THROW(x = solver->addUnboundedContinuousVariable("x", 1));
542
543 solver->push();
544 ASSERT_NO_THROW(solver->addConstraint("", x <= solver->getConstant(12)));
545 ASSERT_NO_THROW(solver->optimize());
546 // max x s.t. x<=12
547 ASSERT_TRUE(solver->isOptimal());
548 EXPECT_NEAR(this->parseNumber("12"), solver->getContinuousValue(x), this->precision());
549
550 solver->push();
551 ASSERT_NO_THROW(y = solver->addUnboundedContinuousVariable("y"));
552 ASSERT_NO_THROW(solver->addConstraint("", y <= solver->getConstant(6)));
553 ASSERT_NO_THROW(solver->addConstraint("", x <= y));
554 // max x s.t. x<=12 and y <= 6 and x <= y
555 ASSERT_NO_THROW(solver->optimize());
556 ASSERT_TRUE(solver->isOptimal());
557 EXPECT_NEAR(this->parseNumber("6"), solver->getContinuousValue(x), this->precision());
558 EXPECT_NEAR(this->parseNumber("6"), solver->getContinuousValue(y), this->precision());
559 solver->pop();
560 ASSERT_NO_THROW(solver->optimize());
561 // max x s.t. x<=12
562 ASSERT_TRUE(solver->isOptimal());
563 EXPECT_NEAR(this->parseNumber("12"), solver->getContinuousValue(x), this->precision());
564
565 solver->push();
566 ASSERT_NO_THROW(y = solver->addUnboundedContinuousVariable("y", 10));
567 ASSERT_NO_THROW(solver->addConstraint("", y <= solver->getConstant(20)));
568 ASSERT_NO_THROW(solver->addConstraint("", y <= -x));
569 // max x+10y s.t. x<=12 and y<=20 and y<=-x
570 ASSERT_NO_THROW(solver->optimize());
571 ASSERT_TRUE(solver->isOptimal());
572 EXPECT_NEAR(this->parseNumber("-20"), solver->getContinuousValue(x), this->precision());
573 EXPECT_NEAR(this->parseNumber("20"), solver->getContinuousValue(y), this->precision());
574
575 solver->pop();
576 ASSERT_NO_THROW(solver->optimize());
577 // max x s.t. x<=12
578 ASSERT_TRUE(solver->isOptimal());
579 EXPECT_NEAR(this->parseNumber("12"), solver->getContinuousValue(x), this->precision());
580
581 solver->push();
582 ASSERT_NO_THROW(z = solver->addUnboundedIntegerVariable("z"));
583 ASSERT_NO_THROW(solver->addConstraint("", z <= solver->getConstant(6)));
584 ASSERT_NO_THROW(solver->addConstraint("", x <= z));
585 ASSERT_NO_THROW(solver->optimize());
586 // max x s.t. x<=12 and z <= 6 and x <= z
587 ASSERT_TRUE(solver->isOptimal());
588 EXPECT_NEAR(this->parseNumber("6"), solver->getContinuousValue(x), this->precision());
589 EXPECT_EQ(6, solver->getIntegerValue(z));
590
591 solver->pop();
592 ASSERT_NO_THROW(solver->optimize());
593 // max x s.t. x<=12
594 ASSERT_TRUE(solver->isOptimal());
595 EXPECT_NEAR(this->parseNumber("12"), solver->getContinuousValue(x), this->precision());
596
597 solver->pop();
598 // max x s.t. true
599 ASSERT_NO_THROW(solver->optimize());
600 ASSERT_FALSE(solver->isOptimal());
601 ASSERT_TRUE(solver->isUnbounded());
602 ASSERT_FALSE(solver->isInfeasible());
603}
604
605} // namespace
storm::dft::modelchecker::ValueType
SFTBDDChecker::ValueType ValueType
Definition SFTBDDChecker.cpp:12
storm::parser::parseNumber
NumberType parseNumber(std::string const &value)
Parse number from string.
Definition ValueParser.cpp:55
storm::utility::solver::getLpSolverFactory
std::unique_ptr< LpSolverFactory< ValueType > > getLpSolverFactory(storm::solver::LpSolverTypeSelection solvType)
Definition solver.cpp:86
storm::utility::convertNumber
TargetType convertNumber(SourceType const &number)
Definition constants.cpp:135
TYPED_TEST
TYPED_TEST(GraphTestAR, SymbolicProb01StochasticGameDieSmall)
Definition GraphTest.cpp:62
TYPED_TEST_SUITE
TYPED_TEST_SUITE(GraphTestAR, TestingTypes,)
TestingTypes
::testing::Types< Cudd, Sylvan > TestingTypes
Definition GraphTest.cpp:59
storm_gtest.h
STORM_SILENT_ASSERT_THROW
#define STORM_SILENT_ASSERT_THROW(statement, expected_exception)
Definition storm_gtest.h:26