From 5b4db6f00261ef6a1aa543e2b9e610eaa2a597cb Mon Sep 17 00:00:00 2001 From: dehnert Date: Mon, 23 Jan 2017 20:41:03 +0100 Subject: [PATCH] fixed issue in JANI abstraction --- src/storm/abstraction/MenuGameRefiner.cpp | 3 + src/storm/abstraction/jani/EdgeAbstractor.cpp | 6 +- src/storm/cli/entrypoints.h | 2 +- .../abstraction/GameBasedMdpModelChecker.cpp | 3 +- .../expressions/LinearityCheckVisitor.cpp | 79 ++++++++++++++++--- .../expressions/LinearityCheckVisitor.h | 3 +- src/storm/storage/jani/Assignment.cpp | 2 +- src/storm/storage/jani/Model.cpp | 2 +- src/storm/storage/jani/TemplateEdge.cpp | 2 +- 9 files changed, 81 insertions(+), 21 deletions(-) diff --git a/src/storm/abstraction/MenuGameRefiner.cpp b/src/storm/abstraction/MenuGameRefiner.cpp index 8a6161bc6..75555bdcd 100644 --- a/src/storm/abstraction/MenuGameRefiner.cpp +++ b/src/storm/abstraction/MenuGameRefiner.cpp @@ -706,6 +706,9 @@ namespace storm { void MenuGameRefiner::performRefinement(std::vector const& refinementCommands) const { for (auto const& command : refinementCommands) { STORM_LOG_TRACE("Refining with " << command.getPredicates().size() << " predicates."); + for (auto const& predicate : command.getPredicates()) { + STORM_LOG_TRACE(predicate); + } abstractor.get().refine(command); } diff --git a/src/storm/abstraction/jani/EdgeAbstractor.cpp b/src/storm/abstraction/jani/EdgeAbstractor.cpp index e95690d8e..980db0846 100644 --- a/src/storm/abstraction/jani/EdgeAbstractor.cpp +++ b/src/storm/abstraction/jani/EdgeAbstractor.cpp @@ -662,10 +662,11 @@ namespace storm { storm::dd::Add EdgeAbstractor::getEdgeDecoratorAdd(boost::optional> const& locationVariables) const { storm::dd::Add result = this->getAbstractionInformation().getDdManager().template getAddZero(); for (uint_fast64_t destinationIndex = 0; destinationIndex < edge.get().getNumberOfDestinations(); ++destinationIndex) { - result += this->getAbstractionInformation().encodeAux(destinationIndex, 0, this->getAbstractionInformation().getAuxVariableCount()).template toAdd() * this->getAbstractionInformation().getDdManager().getConstant(evaluator.asRational(edge.get().getDestination(destinationIndex).getProbability())); + storm::dd::Add tmp = this->getAbstractionInformation().encodeAux(destinationIndex, 0, this->getAbstractionInformation().getAuxVariableCount()).template toAdd() * this->getAbstractionInformation().getDdManager().getConstant(evaluator.asRational(edge.get().getDestination(destinationIndex).getProbability())); if (locationVariables) { - result *= this->getAbstractionInformation().encodeLocation(locationVariables.get().second, edge.get().getDestination(destinationIndex).getLocationIndex()).template toAdd(); + tmp *= this->getAbstractionInformation().encodeLocation(locationVariables.get().second, edge.get().getDestination(destinationIndex).getLocationIndex()).template toAdd(); } + result += tmp; } storm::dd::Add tmp = this->getAbstractionInformation().getDdManager().template getAddOne(); @@ -675,6 +676,7 @@ namespace storm { tmp *= this->getAbstractionInformation().encodePlayer1Choice(edgeId, this->getAbstractionInformation().getPlayer1VariableCount()).template toAdd(); result *= tmp; + return result; } diff --git a/src/storm/cli/entrypoints.h b/src/storm/cli/entrypoints.h index 1653d76ea..3d1a9397e 100644 --- a/src/storm/cli/entrypoints.h +++ b/src/storm/cli/entrypoints.h @@ -129,7 +129,7 @@ namespace storm { modelCheckingWatch.stop(); if (result) { STORM_PRINT_AND_LOG("Result (initial states): "); - STORM_PRINT_AND_LOG(*result); + STORM_PRINT_AND_LOG(*result << std::endl); STORM_PRINT_AND_LOG("Time for model checking: " << modelCheckingWatch << "." << std::endl); } else { STORM_PRINT_AND_LOG(" skipped, because the modelling formalism is currently unsupported." << std::endl); diff --git a/src/storm/modelchecker/abstraction/GameBasedMdpModelChecker.cpp b/src/storm/modelchecker/abstraction/GameBasedMdpModelChecker.cpp index 644584740..b1468d87a 100644 --- a/src/storm/modelchecker/abstraction/GameBasedMdpModelChecker.cpp +++ b/src/storm/modelchecker/abstraction/GameBasedMdpModelChecker.cpp @@ -342,7 +342,6 @@ namespace storm { storm::dd::Bdd globalConstraintStates = abstractor->getStates(constraintExpression); storm::dd::Bdd globalTargetStates = abstractor->getStates(targetStateExpression); - // globalTargetStates.template toAdd().exportToDot("target.dot"); // Enter the main-loop of abstraction refinement. boost::optional> previousQualitativeResult = boost::none; @@ -368,7 +367,9 @@ namespace storm { } // #ifdef LOCAL_DEBUG + // targetStates.template toAdd().exportToDot("target.dot"); // abstractor->exportToDot("game" + std::to_string(iterations) + ".dot", targetStates, game.getManager().getBddOne()); + // game.getReachableStates().template toAdd().exportToDot("reach.dot"); // #endif // (3) compute all states with probability 0/1 wrt. to the two different player 2 goals (min/max). diff --git a/src/storm/storage/expressions/LinearityCheckVisitor.cpp b/src/storm/storage/expressions/LinearityCheckVisitor.cpp index 44cb70728..18198ca0e 100644 --- a/src/storm/storage/expressions/LinearityCheckVisitor.cpp +++ b/src/storm/storage/expressions/LinearityCheckVisitor.cpp @@ -12,19 +12,44 @@ namespace storm { // Intentionally left empty. } - bool LinearityCheckVisitor::check(Expression const& expression) { - LinearityStatus result = boost::any_cast(expression.getBaseExpression().accept(*this, boost::none)); + bool LinearityCheckVisitor::check(Expression const& expression, bool booleanIsLinear) { + LinearityStatus result = boost::any_cast(expression.getBaseExpression().accept(*this, booleanIsLinear)); return result == LinearityStatus::LinearWithoutVariables || result == LinearityStatus::LinearContainsVariables; } - boost::any LinearityCheckVisitor::visit(IfThenElseExpression const&, boost::any const&) { - // An if-then-else expression is never linear. - return LinearityStatus::NonLinear; + boost::any LinearityCheckVisitor::visit(IfThenElseExpression const& expression, boost::any const& data) { + bool booleanIsLinear = boost::any_cast(data); + + if (booleanIsLinear) { + auto conditionResult = boost::any_cast(expression.getCondition()->accept(*this, booleanIsLinear)); + auto thenResult = boost::any_cast(expression.getThenExpression()->accept(*this, booleanIsLinear)); + auto elseResult = boost::any_cast(expression.getElseExpression()->accept(*this, booleanIsLinear)); + + if (conditionResult != LinearityStatus::NonLinear && thenResult != LinearityStatus::NonLinear && elseResult != LinearityStatus::NonLinear) { + return LinearityStatus::LinearContainsVariables; + } else { + return LinearityStatus::NonLinear; + } + } else { + return LinearityStatus::NonLinear; + } } - boost::any LinearityCheckVisitor::visit(BinaryBooleanFunctionExpression const&, boost::any const&) { - // Boolean function applications are not allowed in linear expressions. - return LinearityStatus::NonLinear; + boost::any LinearityCheckVisitor::visit(BinaryBooleanFunctionExpression const& expression, boost::any const& data) { + bool booleanIsLinear = boost::any_cast(data); + + if (booleanIsLinear) { + auto leftResult = boost::any_cast(expression.getFirstOperand()->accept(*this, booleanIsLinear)); + auto rightResult = boost::any_cast(expression.getSecondOperand()->accept(*this, booleanIsLinear)); + + if (leftResult != LinearityStatus::NonLinear && rightResult != LinearityStatus::NonLinear) { + return LinearityStatus::LinearContainsVariables; + } else { + return LinearityStatus::NonLinear; + } + } else { + return LinearityStatus::NonLinear; + } } boost::any LinearityCheckVisitor::visit(BinaryNumericalFunctionExpression const& expression, boost::any const& data) { @@ -56,15 +81,37 @@ namespace storm { STORM_LOG_THROW(false, storm::exceptions::InvalidOperationException, "Illegal binary numerical expression operator."); } - boost::any LinearityCheckVisitor::visit(BinaryRelationExpression const&, boost::any const&) { - return LinearityStatus::NonLinear; + boost::any LinearityCheckVisitor::visit(BinaryRelationExpression const& expression, boost::any const& data) { + bool booleanIsLinear = boost::any_cast(data); + + if (booleanIsLinear) { + auto leftResult = boost::any_cast(expression.getFirstOperand()->accept(*this, booleanIsLinear)); + auto rightResult = boost::any_cast(expression.getSecondOperand()->accept(*this, booleanIsLinear)); + + if (leftResult != LinearityStatus::NonLinear && rightResult != LinearityStatus::NonLinear) { + return LinearityStatus::LinearContainsVariables; + } else { + return LinearityStatus::NonLinear; + } + } else { + return LinearityStatus::NonLinear; + } } boost::any LinearityCheckVisitor::visit(VariableExpression const&, boost::any const&) { return LinearityStatus::LinearContainsVariables; } - boost::any LinearityCheckVisitor::visit(UnaryBooleanFunctionExpression const&, boost::any const&) { + boost::any LinearityCheckVisitor::visit(UnaryBooleanFunctionExpression const& expression, boost::any const& data) { + bool booleanIsLinear = boost::any_cast(data); + + if (booleanIsLinear) { + return boost::any_cast(expression.getOperand()->accept(*this, booleanIsLinear)); + } else { + return LinearityStatus::NonLinear; + } + + // Boolean function applications are not allowed in linear expressions. return LinearityStatus::NonLinear; } @@ -78,8 +125,14 @@ namespace storm { STORM_LOG_THROW(false, storm::exceptions::InvalidOperationException, "Illegal unary numerical expression operator."); } - boost::any LinearityCheckVisitor::visit(BooleanLiteralExpression const&, boost::any const&) { - return LinearityStatus::NonLinear; + boost::any LinearityCheckVisitor::visit(BooleanLiteralExpression const& expression, boost::any const& data) { + bool booleanIsLinear = boost::any_cast(data); + + if (booleanIsLinear) { + return LinearityStatus::LinearWithoutVariables; + } else { + return LinearityStatus::NonLinear; + } } boost::any LinearityCheckVisitor::visit(IntegerLiteralExpression const&, boost::any const&) { diff --git a/src/storm/storage/expressions/LinearityCheckVisitor.h b/src/storm/storage/expressions/LinearityCheckVisitor.h index 735481038..876869313 100644 --- a/src/storm/storage/expressions/LinearityCheckVisitor.h +++ b/src/storm/storage/expressions/LinearityCheckVisitor.h @@ -17,8 +17,9 @@ namespace storm { * Checks that the given expression is linear. * * @param expression The expression to check for linearity. + * @param booleanIsLinear A flag indicating whether boolean components are considered linear. */ - bool check(Expression const& expression); + bool check(Expression const& expression, bool booleanIsLinear = false); virtual boost::any visit(IfThenElseExpression const& expression, boost::any const& data) override; virtual boost::any visit(BinaryBooleanFunctionExpression const& expression, boost::any const& data) override; diff --git a/src/storm/storage/jani/Assignment.cpp b/src/storm/storage/jani/Assignment.cpp index 3b4f97a63..ba0b41c2a 100644 --- a/src/storm/storage/jani/Assignment.cpp +++ b/src/storm/storage/jani/Assignment.cpp @@ -46,7 +46,7 @@ namespace storm { bool Assignment::isLinear() const { storm::expressions::LinearityCheckVisitor linearityChecker; - return linearityChecker.check(this->getAssignedExpression()); + return linearityChecker.check(this->getAssignedExpression(), true); } std::ostream& operator<<(std::ostream& stream, Assignment const& assignment) { diff --git a/src/storm/storage/jani/Model.cpp b/src/storm/storage/jani/Model.cpp index e02bac355..193e7388d 100644 --- a/src/storm/storage/jani/Model.cpp +++ b/src/storm/storage/jani/Model.cpp @@ -1124,7 +1124,7 @@ namespace storm { bool result = true; storm::expressions::LinearityCheckVisitor linearityChecker; - result &= linearityChecker.check(this->getInitialStatesExpression()); + result &= linearityChecker.check(this->getInitialStatesExpression(), true); for (auto const& automaton : this->getAutomata()) { result &= automaton.isLinear(); diff --git a/src/storm/storage/jani/TemplateEdge.cpp b/src/storm/storage/jani/TemplateEdge.cpp index ef4adadf2..07b305ffc 100644 --- a/src/storm/storage/jani/TemplateEdge.cpp +++ b/src/storm/storage/jani/TemplateEdge.cpp @@ -139,7 +139,7 @@ namespace storm { bool TemplateEdge::isLinear() const { storm::expressions::LinearityCheckVisitor linearityChecker; - bool result = linearityChecker.check(this->getGuard()); + bool result = linearityChecker.check(this->getGuard(), true); for (auto const& destination : destinations) { result &= destination.isLinear(); }