From 31be908c5aedc302a63ac04514f711b8aa35634e Mon Sep 17 00:00:00 2001 From: dehnert Date: Fri, 25 Sep 2015 18:40:52 +0200 Subject: [PATCH] mathsat does not like boolean arguments to ite-expressions, so we encode it ourselves now Former-commit-id: e30e7fcd553b2f8f3b39815af3590be11b43d068 --- src/adapters/MathsatExpressionAdapter.h | 15 ++++++++++++--- src/storage/prism/menu_games/AbstractProgram.cpp | 2 -- .../prism/menu_games/StateSetAbstractor.cpp | 16 ++++++++-------- .../functional/abstraction/PrismMenuGameTest.cpp | 14 ++++++++++++++ 4 files changed, 34 insertions(+), 13 deletions(-) diff --git a/src/adapters/MathsatExpressionAdapter.h b/src/adapters/MathsatExpressionAdapter.h index 854b20542..6df269b58 100644 --- a/src/adapters/MathsatExpressionAdapter.h +++ b/src/adapters/MathsatExpressionAdapter.h @@ -58,12 +58,15 @@ namespace storm { */ msat_term translateExpression(storm::expressions::Expression const& expression) { msat_term result = boost::any_cast(expression.getBaseExpression().accept(*this)); - STORM_LOG_THROW(!MSAT_ERROR_TERM(result), storm::exceptions::ExpressionEvaluationException, "Could not translate expression to MathSAT's format."); + if (MSAT_ERROR_TERM(result)) { + std::string errorMessage(msat_last_error_message(env)); + STORM_LOG_THROW(!MSAT_ERROR_TERM(result), storm::exceptions::ExpressionEvaluationException, "Could not translate expression to MathSAT's format. (Message: " << errorMessage << ")"); + } return result; } /*! - * Translates the given variable to an equivalent expression for Z3. + * Translates the given variable to an equivalent expression for MathSAT. * * @param variable The variable to translate. * @return An equivalent term for MathSAT. @@ -164,7 +167,13 @@ namespace storm { msat_term conditionResult = boost::any_cast(expression.getCondition()->accept(*this)); msat_term thenResult = boost::any_cast(expression.getThenExpression()->accept(*this)); msat_term elseResult = boost::any_cast(expression.getElseExpression()->accept(*this)); - return msat_make_term_ite(env, conditionResult, thenResult, elseResult); + + // MathSAT does not allow ite with boolean arguments, so we have to encode it ourselves. + if (expression.getThenExpression()->hasBooleanType() && expression.getElseExpression()->hasBooleanType()) { + return msat_make_and(env, msat_make_or(env, msat_make_not(env, conditionResult), thenResult), msat_make_or(env, conditionResult, elseResult)); + } else { + return msat_make_term_ite(env, conditionResult, thenResult, elseResult); + } } virtual boost::any visit(expressions::BooleanLiteralExpression const& expression) override { diff --git a/src/storage/prism/menu_games/AbstractProgram.cpp b/src/storage/prism/menu_games/AbstractProgram.cpp index acf5878e2..405f6874f 100644 --- a/src/storage/prism/menu_games/AbstractProgram.cpp +++ b/src/storage/prism/menu_games/AbstractProgram.cpp @@ -144,8 +144,6 @@ namespace storm { bottomStates = bottomStateAbstractor.getAbstractStates(); } - std::cout << "found " << (reachableStates && bottomStates).getNonZeroCount() << " reachable bottom states" << std::endl; - // Find the deadlock states in the model. storm::dd::Bdd deadlockStates = transitionRelation.existsAbstract(ddInformation.successorVariables); deadlockStates = reachableStates && !deadlockStates; diff --git a/src/storage/prism/menu_games/StateSetAbstractor.cpp b/src/storage/prism/menu_games/StateSetAbstractor.cpp index 9208273a8..b022c95d7 100644 --- a/src/storage/prism/menu_games/StateSetAbstractor.cpp +++ b/src/storage/prism/menu_games/StateSetAbstractor.cpp @@ -72,14 +72,11 @@ namespace storm { template storm::dd::Bdd StateSetAbstractor::getStateBdd(storm::solver::SmtSolver::ModelReference const& model) const { STORM_LOG_TRACE("Building source state BDD."); - std::cout << "new model: " << std::endl; storm::dd::Bdd result = ddInformation.manager->getBddOne(); for (auto const& variableIndexPair : relevantPredicatesAndVariables) { if (model.getBooleanValue(variableIndexPair.first)) { - std::cout << expressionInformation.predicates[variableIndexPair.second] << " is true" << std::endl; result &= ddInformation.predicateBdds[variableIndexPair.second].first; } else { - std::cout << expressionInformation.predicates[variableIndexPair.second] << " is false" << std::endl; result &= !ddInformation.predicateBdds[variableIndexPair.second].first; } } @@ -114,7 +111,7 @@ namespace storm { storm::dd::Bdd result = ddInformation.manager->getBddZero(); uint_fast64_t modelCounter = 0; - smtSolver->allSat(decisionVariables, [&result,this,&modelCounter] (storm::solver::SmtSolver::ModelReference const& model) { result |= getStateBdd(model); ++modelCounter; std::cout << "found " << modelCounter << " models" << std::endl; return modelCounter < 10000 ? true : false; } ); + smtSolver->allSat(decisionVariables, [&result,this,&modelCounter] (storm::solver::SmtSolver::ModelReference const& model) { result |= getStateBdd(model); return true; } ); cachedBdd = result; } @@ -122,22 +119,25 @@ namespace storm { template void StateSetAbstractor::popConstraintBdd() { // If the last constraint was not the constant one BDD, we need to pop the constraint from the solver. - if (!this->constraint.isOne()) { - smtSolver->pop(); + if (this->constraint.isOne()) { + return; } + smtSolver->pop(); } template void StateSetAbstractor::pushConstraintBdd() { + if (this->constraint.isOne()) { + return; + } + // Create a new backtracking point before adding the constraint. smtSolver->push(); // Then add the constraint. std::pair, std::unordered_map, storm::expressions::Variable>> result = constraint.toExpression(expressionInformation.manager, ddInformation.bddVariableIndexToPredicateMap); - std::cout << "adding expressions... " << std::endl; for (auto const& expression : result.first) { - std::cout << expression << std::endl; smtSolver->add(expression); } } diff --git a/test/functional/abstraction/PrismMenuGameTest.cpp b/test/functional/abstraction/PrismMenuGameTest.cpp index 4231413a1..26b296976 100644 --- a/test/functional/abstraction/PrismMenuGameTest.cpp +++ b/test/functional/abstraction/PrismMenuGameTest.cpp @@ -31,6 +31,7 @@ TEST(PrismMenuGame, DieAbstractionTest) { EXPECT_EQ(10, game.getNumberOfTransitions()); EXPECT_EQ(2, game.getNumberOfStates()); + EXPECT_EQ(0, game.getBottomStates().getNonZeroCount()); } TEST(PrismMenuGame, DieAbstractionAndRefinementTest) { @@ -49,6 +50,7 @@ TEST(PrismMenuGame, DieAbstractionAndRefinementTest) { EXPECT_EQ(10, game.getNumberOfTransitions()); EXPECT_EQ(3, game.getNumberOfStates()); + EXPECT_EQ(0, game.getBottomStates().getNonZeroCount()); } TEST(PrismMenuGame, DieFullAbstractionTest) { @@ -80,6 +82,7 @@ TEST(PrismMenuGame, DieFullAbstractionTest) { EXPECT_EQ(20, game.getNumberOfTransitions()); EXPECT_EQ(13, game.getNumberOfStates()); + EXPECT_EQ(0, game.getBottomStates().getNonZeroCount()); } TEST(PrismMenuGame, CrowdsAbstractionTest) { @@ -97,6 +100,7 @@ TEST(PrismMenuGame, CrowdsAbstractionTest) { EXPECT_EQ(11, game.getNumberOfTransitions()); EXPECT_EQ(2, game.getNumberOfStates()); + EXPECT_EQ(1, game.getBottomStates().getNonZeroCount()); } TEST(PrismMenuGame, CrowdsAbstractionAndRefinementTest) { @@ -116,6 +120,7 @@ TEST(PrismMenuGame, CrowdsAbstractionAndRefinementTest) { EXPECT_EQ(28, game.getNumberOfTransitions()); EXPECT_EQ(4, game.getNumberOfStates()); + EXPECT_EQ(2, game.getBottomStates().getNonZeroCount()); } TEST(PrismMenuGame, CrowdsFullAbstractionTest) { @@ -187,6 +192,7 @@ TEST(PrismMenuGame, CrowdsFullAbstractionTest) { EXPECT_EQ(15113, game.getNumberOfTransitions()); EXPECT_EQ(8607, game.getNumberOfStates()); + EXPECT_EQ(1260, game.getBottomStates().getNonZeroCount()); } TEST(PrismMenuGame, TwoDiceAbstractionTest) { @@ -206,6 +212,7 @@ TEST(PrismMenuGame, TwoDiceAbstractionTest) { EXPECT_EQ(34, game.getNumberOfTransitions()); EXPECT_EQ(4, game.getNumberOfStates()); + EXPECT_EQ(0, game.getBottomStates().getNonZeroCount()); } TEST(PrismMenuGame, TwoDiceAbstractionAndRefinementTest) { @@ -227,6 +234,7 @@ TEST(PrismMenuGame, TwoDiceAbstractionAndRefinementTest) { EXPECT_EQ(164, game.getNumberOfTransitions()); EXPECT_EQ(8, game.getNumberOfStates()); + EXPECT_EQ(0, game.getBottomStates().getNonZeroCount()); } TEST(PrismMenuGame, TwoDiceFullAbstractionTest) { @@ -277,6 +285,7 @@ TEST(PrismMenuGame, TwoDiceFullAbstractionTest) { EXPECT_EQ(436, game.getNumberOfTransitions()); EXPECT_EQ(169, game.getNumberOfStates()); + EXPECT_EQ(0, game.getBottomStates().getNonZeroCount()); } TEST(PrismMenuGame, WlanAbstractionTest) { @@ -295,8 +304,11 @@ TEST(PrismMenuGame, WlanAbstractionTest) { storm::prism::menu_games::MenuGame game = abstractProgram.getAbstractGame(); + game.getTransitionMatrix().exportToDot("trans.dot"); + game.getReachableStates().toAdd().exportToDot("reach.dot"); EXPECT_EQ(281, game.getNumberOfTransitions()); EXPECT_EQ(4, game.getNumberOfStates()); + EXPECT_EQ(4, game.getBottomStates().getNonZeroCount()); } TEST(PrismMenuGame, WlanAbstractionAndRefinementTest) { @@ -319,6 +331,7 @@ TEST(PrismMenuGame, WlanAbstractionAndRefinementTest) { EXPECT_EQ(564, game.getNumberOfTransitions()); EXPECT_EQ(8, game.getNumberOfStates()); + EXPECT_EQ(8, game.getBottomStates().getNonZeroCount()); } TEST(PrismMenuGame, WlanFullAbstractionTest) { @@ -437,6 +450,7 @@ TEST(PrismMenuGame, WlanFullAbstractionTest) { EXPECT_EQ(9503, game.getNumberOfTransitions()); EXPECT_EQ(5523, game.getNumberOfStates()); + EXPECT_EQ(0, game.getBottomStates().getNonZeroCount()); } #endif \ No newline at end of file