From 1d2e7b245088e8aa36c9f989af70cdb0fb6854af Mon Sep 17 00:00:00 2001 From: TimQu Date: Fri, 17 Feb 2017 03:17:28 +0100 Subject: [PATCH] compilation fixes --- src/storm/adapters/Z3ExpressionAdapter.cpp | 2 +- src/storm/solver/Z3LpSolver.cpp | 2 +- .../SubsetEnumerator.h | 4 ++-- .../SparseMaPcaaModelCheckerTest.cpp | 22 +++++++++---------- 4 files changed, 15 insertions(+), 15 deletions(-) diff --git a/src/storm/adapters/Z3ExpressionAdapter.cpp b/src/storm/adapters/Z3ExpressionAdapter.cpp index d51da9888..c4fbff3cd 100644 --- a/src/storm/adapters/Z3ExpressionAdapter.cpp +++ b/src/storm/adapters/Z3ExpressionAdapter.cpp @@ -123,7 +123,7 @@ namespace storm { long long num; long long den; if (Z3_get_numeral_rational_int64(expr.ctx(), expr, &num, &den)) { - return manager.rational(storm::utility::convertNumber(num) / storm::utility::convertNumber(den)); + return manager.rational(storm::utility::convertNumber((int_fast64_t) num) / storm::utility::convertNumber((int_fast64_t) den)); } else { return manager.rational(storm::utility::convertNumber(std::string(Z3_get_numeral_string(expr.ctx(), expr)))); } diff --git a/src/storm/solver/Z3LpSolver.cpp b/src/storm/solver/Z3LpSolver.cpp index 552f11424..95b061f70 100644 --- a/src/storm/solver/Z3LpSolver.cpp +++ b/src/storm/solver/Z3LpSolver.cpp @@ -134,7 +134,7 @@ namespace storm { // Solve the optimization problem depending on the optimization direction z3::optimize::handle optFuncHandle = this->getOptimizationDirection() == OptimizationDirection::Minimize ? solver->minimize(expressionAdapter->translateExpression(optimizationFunction)) : solver->maximize(expressionAdapter->translateExpression(optimizationFunction)); z3::check_result chkRes = solver->check(); - STORM_LOG_THROW(chkRes != z3::unknown, storm::exceptions::InvalidStateException, "Unable to solve LP problem with Z3: Check result is unknown. Reason: " << Z3_optimize_get_reason_unknown(*context, *solver)); + STORM_LOG_THROW(chkRes != z3::unknown, storm::exceptions::InvalidStateException, "Unable to solve LP problem with Z3: Check result is unknown."); // We need to store the resulting information at this point. Otherwise, the information would be lost after calling pop() ... diff --git a/src/storm/storage/geometry/nativepolytopeconversion/SubsetEnumerator.h b/src/storm/storage/geometry/nativepolytopeconversion/SubsetEnumerator.h index 2d30d9ce3..eef6a2ecd 100644 --- a/src/storm/storage/geometry/nativepolytopeconversion/SubsetEnumerator.h +++ b/src/storm/storage/geometry/nativepolytopeconversion/SubsetEnumerator.h @@ -2,7 +2,7 @@ #define STORM_STORAGE_GEOMETRY_NATIVEPOLYTOPECONVERSION_SUBSETENUMERATOR_H_ #include - +#include namespace storm { namespace storage { @@ -66,4 +66,4 @@ namespace storm { } } -#endif /* STORM_STORAGE_GEOMETRY_NATIVEPOLYTOPECONVERSION_SUBSETENUMERATOR_H_ */ \ No newline at end of file +#endif /* STORM_STORAGE_GEOMETRY_NATIVEPOLYTOPECONVERSION_SUBSETENUMERATOR_H_ */ diff --git a/src/test/modelchecker/SparseMaPcaaModelCheckerTest.cpp b/src/test/modelchecker/SparseMaPcaaModelCheckerTest.cpp index 5f03c77a1..8ba599bde 100644 --- a/src/test/modelchecker/SparseMaPcaaModelCheckerTest.cpp +++ b/src/test/modelchecker/SparseMaPcaaModelCheckerTest.cpp @@ -6,7 +6,7 @@ #include "storm/modelchecker/multiobjective/pcaa.h" #include "storm/modelchecker/results/ExplicitQuantitativeCheckResult.h" #include "storm/modelchecker/results/ExplicitQualitativeCheckResult.h" -#include "storm/modelchecker/results/ParetoCurveCheckResult.h" +#include "storm/modelchecker/results/ExplicitParetoCurveCheckResult.h" #include "storm/models/sparse/MarkovAutomaton.h" #include "storm/storage/geometry/Polytope.h" #include "storm/storage/geometry/Hyperrectangle.h" @@ -33,7 +33,7 @@ TEST(SparseMaPcaaModelCheckerTest, serverRationalNumbers) { storm::modelchecker::SparseMarkovAutomatonCslModelChecker> checker(*ma); std::unique_ptr result = checker.check(storm::modelchecker::CheckTask(*formulas[0], true)); - ASSERT_TRUE(result->isParetoCurveCheckResult()); + ASSERT_TRUE(result->isExplicitParetoCurveCheckResult()); storm::RationalNumber p1 = storm::utility::convertNumber(11.0); p1 /= storm::utility::convertNumber(6.0); storm::RationalNumber p2 = storm::utility::convertNumber(1.0); p2 /= storm::utility::convertNumber(2.0); @@ -42,8 +42,8 @@ TEST(SparseMaPcaaModelCheckerTest, serverRationalNumbers) { storm::RationalNumber q2 = storm::utility::convertNumber(2.0); q2 /= storm::utility::convertNumber(3.0); std::vector q = {q1, q2}; auto expectedAchievableValues = storm::storage::geometry::Polytope::createDownwardClosure(std::vector>({p,q})); - EXPECT_TRUE(expectedAchievableValues->contains(result->asParetoCurveCheckResult().getUnderApproximation())); - EXPECT_TRUE(result->asParetoCurveCheckResult().getOverApproximation()->contains(expectedAchievableValues)); + EXPECT_TRUE(expectedAchievableValues->contains(result->asExplicitParetoCurveCheckResult().getUnderApproximation())); + EXPECT_TRUE(result->asExplicitParetoCurveCheckResult().getOverApproximation()->contains(expectedAchievableValues)); }*/ @@ -59,7 +59,7 @@ TEST(SparseMaPcaaModelCheckerTest, server) { std::shared_ptr> ma = storm::buildSparseModel(program, formulas)->as>(); std::unique_ptr result = storm::modelchecker::multiobjective::performPcaa(*ma, formulas[0]->asMultiObjectiveFormula()); - ASSERT_TRUE(result->isParetoCurveCheckResult()); + ASSERT_TRUE(result->isExplicitParetoCurveCheckResult()); // we do our checks with rationals to avoid numerical issues when doing polytope computations... std::vector p = {11.0/6.0, 1.0/2.0}; @@ -72,8 +72,8 @@ TEST(SparseMaPcaaModelCheckerTest, server) { std::vector lb(2,-eps), ub(2,eps); auto bloatingBox = storm::storage::geometry::Hyperrectangle(lb,ub).asPolytope(); - EXPECT_TRUE(expectedAchievableValues->minkowskiSum(bloatingBox)->contains(result->asParetoCurveCheckResult().getUnderApproximation()->convertNumberRepresentation())); - EXPECT_TRUE(result->asParetoCurveCheckResult().getOverApproximation()->convertNumberRepresentation()->minkowskiSum(bloatingBox)->contains(expectedAchievableValues)); + EXPECT_TRUE(expectedAchievableValues->minkowskiSum(bloatingBox)->contains(result->asExplicitParetoCurveCheckResult().getUnderApproximation()->convertNumberRepresentation())); + EXPECT_TRUE(result->asExplicitParetoCurveCheckResult().getOverApproximation()->convertNumberRepresentation()->minkowskiSum(bloatingBox)->contains(expectedAchievableValues)); } @@ -88,7 +88,7 @@ TEST(SparseMaPcaaModelCheckerTest, jobscheduler_pareto_3Obj) { std::shared_ptr> ma = storm::buildSparseModel(program, formulas)->as>(); std::unique_ptr result = storm::modelchecker::multiobjective::performPcaa(*ma, formulas[0]->asMultiObjectiveFormula()); - ASSERT_TRUE(result->isParetoCurveCheckResult()); + ASSERT_TRUE(result->isExplicitParetoCurveCheckResult()); std::vector j12 = {1.266666667,0.1617571721,0.5}; std::vector j13 = {1.283333333,0.1707737575,0.25}; @@ -104,7 +104,7 @@ TEST(SparseMaPcaaModelCheckerTest, jobscheduler_pareto_3Obj) { std::vector lb(3,-eps), ub(3,eps); auto bloatingBox = storm::storage::geometry::Hyperrectangle(lb,ub).asPolytope(); - EXPECT_TRUE(result->asParetoCurveCheckResult().getOverApproximation()->convertNumberRepresentation()->minkowskiSum(bloatingBox)->contains(expectedAchievableValues)); + EXPECT_TRUE(result->asExplicitParetoCurveCheckResult().getOverApproximation()->convertNumberRepresentation()->minkowskiSum(bloatingBox)->contains(expectedAchievableValues)); } TEST(SparseMaPcaaModelCheckerTest, jobscheduler_achievability_3Obj) { @@ -161,7 +161,7 @@ TEST(SparseMaPcaaModelCheckerTest, jobscheduler_pareto_2Obj) { std::shared_ptr> ma = storm::buildSparseModel(program, formulas)->as>(); std::unique_ptr result = storm::modelchecker::multiobjective::performPcaa(*ma, formulas[0]->asMultiObjectiveFormula()); - ASSERT_TRUE(result->isParetoCurveCheckResult()); + ASSERT_TRUE(result->isExplicitParetoCurveCheckResult()); std::vector j12 = {0.2591835573, 0.01990529674}; std::vector j13 = {0.329682099, 0.01970194998}; @@ -177,7 +177,7 @@ TEST(SparseMaPcaaModelCheckerTest, jobscheduler_pareto_2Obj) { std::vector lb(2,-eps), ub(2,eps); auto bloatingBox = storm::storage::geometry::Hyperrectangle(lb,ub).asPolytope(); - EXPECT_TRUE(result->asParetoCurveCheckResult().getOverApproximation()->convertNumberRepresentation()->minkowskiSum(bloatingBox)->contains(expectedAchievableValues)); + EXPECT_TRUE(result->asExplicitParetoCurveCheckResult().getOverApproximation()->convertNumberRepresentation()->minkowskiSum(bloatingBox)->contains(expectedAchievableValues)); }