From b9e4d6f334f972c55f4d311944a37cea43d4c280 Mon Sep 17 00:00:00 2001 From: dehnert Date: Mon, 19 Dec 2016 21:03:37 +0100 Subject: [PATCH] initial support for transient boolean variables in formulas of JANI models (game-based engine) --- src/storm/abstraction/MenuGameRefiner.h | 4 +- .../jani/JaniMenuGameAbstractor.cpp | 2 +- .../abstraction/GameBasedMdpModelChecker.cpp | 51 ++-- ...Splitter.cpp => FullPredicateSplitter.cpp} | 30 +-- ...cateSplitter.h => FullPredicateSplitter.h} | 2 +- .../expressions/VariableSetAbstractor.cpp | 225 ------------------ .../VariableSetPredicateSplitter.cpp | 180 ++++++++++++++ ...actor.h => VariableSetPredicateSplitter.h} | 10 +- src/storm/storage/jani/Automaton.cpp | 4 +- 9 files changed, 243 insertions(+), 265 deletions(-) rename src/storm/storage/expressions/{PredicateSplitter.cpp => FullPredicateSplitter.cpp} (55%) rename src/storm/storage/expressions/{PredicateSplitter.h => FullPredicateSplitter.h} (96%) delete mode 100644 src/storm/storage/expressions/VariableSetAbstractor.cpp create mode 100644 src/storm/storage/expressions/VariableSetPredicateSplitter.cpp rename src/storm/storage/expressions/{VariableSetAbstractor.h => VariableSetPredicateSplitter.h} (76%) diff --git a/src/storm/abstraction/MenuGameRefiner.h b/src/storm/abstraction/MenuGameRefiner.h index 3250b97ab..1157a8985 100644 --- a/src/storm/abstraction/MenuGameRefiner.h +++ b/src/storm/abstraction/MenuGameRefiner.h @@ -11,7 +11,7 @@ #include "storm/abstraction/QuantitativeResultMinMax.h" #include "storm/storage/expressions/Expression.h" -#include "storm/storage/expressions/PredicateSplitter.h" +#include "storm/storage/expressions/FullPredicateSplitter.h" #include "storm/storage/expressions/EquivalenceChecker.h" #include "storm/storage/dd/DdType.h" @@ -143,7 +143,7 @@ namespace storm { storm::settings::modules::AbstractionSettings::PivotSelectionHeuristic pivotSelectionHeuristic; /// An object that can be used for splitting predicates. - mutable storm::expressions::PredicateSplitter splitter; + mutable storm::expressions::FullPredicateSplitter splitter; /// An object that can be used to determine whether predicates are equivalent. mutable storm::expressions::EquivalenceChecker equivalenceChecker; diff --git a/src/storm/abstraction/jani/JaniMenuGameAbstractor.cpp b/src/storm/abstraction/jani/JaniMenuGameAbstractor.cpp index d2f948d69..b35376b6b 100644 --- a/src/storm/abstraction/jani/JaniMenuGameAbstractor.cpp +++ b/src/storm/abstraction/jani/JaniMenuGameAbstractor.cpp @@ -32,7 +32,7 @@ namespace storm { using storm::settings::modules::AbstractionSettings; template - JaniMenuGameAbstractor::JaniMenuGameAbstractor(storm::jani::Model const& model, std::shared_ptr const& smtSolverFactory) : model(model), smtSolverFactory(smtSolverFactory), abstractionInformation(model.getManager(), model.getAllExpressionVariables(), smtSolverFactory->create(model.getManager())), automata(), initialStateAbstractor(abstractionInformation, {model.getInitialStatesExpression()}, this->smtSolverFactory), validBlockAbstractor(abstractionInformation, smtSolverFactory), currentGame(nullptr), refinementPerformed(false) { + JaniMenuGameAbstractor::JaniMenuGameAbstractor(storm::jani::Model const& model, std::shared_ptr const& smtSolverFactory) : model(model), smtSolverFactory(smtSolverFactory), abstractionInformation(model.getManager(), model.getAllExpressionVariables(), smtSolverFactory->create(model.getManager())), automata(), initialStateAbstractor(abstractionInformation, {model.getInitialStatesExpression()}, this->smtSolverFactory), validBlockAbstractor(abstractionInformation, smtSolverFactory), currentGame(nullptr), refinementPerformed(true) { // For now, we assume that there is a single module. If the program has more than one module, it needs // to be flattened before the procedure. diff --git a/src/storm/modelchecker/abstraction/GameBasedMdpModelChecker.cpp b/src/storm/modelchecker/abstraction/GameBasedMdpModelChecker.cpp index a5ef4c2f5..ae6a17ab4 100644 --- a/src/storm/modelchecker/abstraction/GameBasedMdpModelChecker.cpp +++ b/src/storm/modelchecker/abstraction/GameBasedMdpModelChecker.cpp @@ -8,7 +8,7 @@ #include "storm/models/symbolic/Mdp.h" #include "storm/storage/expressions/ExpressionManager.h" -#include "storm/storage/expressions/VariableSetAbstractor.h" +#include "storm/storage/expressions/VariableSetPredicateSplitter.h" #include "storm/storage/dd/DdManager.h" @@ -78,8 +78,22 @@ namespace storm { template std::unique_ptr GameBasedMdpModelChecker::computeUntilProbabilities(CheckTask const& checkTask) { storm::logic::UntilFormula const& pathFormula = checkTask.getFormula(); - std::map labelToExpressionMapping = preprocessedModel.asPrismProgram().getLabelToExpressionMapping(); - return performGameBasedAbstractionRefinement(checkTask.substituteFormula(pathFormula), pathFormula.getLeftSubformula().toExpression(preprocessedModel.getManager(), labelToExpressionMapping), pathFormula.getRightSubformula().toExpression(preprocessedModel.getManager(), labelToExpressionMapping)); + std::map labelToExpressionMapping; + if (preprocessedModel.isPrismProgram()) { + labelToExpressionMapping = preprocessedModel.asPrismProgram().getLabelToExpressionMapping(); + } else { + storm::jani::Model const& janiModel = preprocessedModel.asJaniModel(); + for (auto const& variable : janiModel.getGlobalVariables().getBooleanVariables()) { + if (variable.isTransient()) { + labelToExpressionMapping[variable.getName()] = janiModel.getLabelExpression(variable.asBooleanVariable()); + } + } + } + + storm::expressions::Expression constraintExpression = pathFormula.getLeftSubformula().toExpression(preprocessedModel.getManager(), labelToExpressionMapping); + storm::expressions::Expression targetStateExpression = pathFormula.getRightSubformula().toExpression(preprocessedModel.getManager(), labelToExpressionMapping); + + return performGameBasedAbstractionRefinement(checkTask.substituteFormula(pathFormula), constraintExpression, targetStateExpression); } template @@ -88,8 +102,19 @@ namespace storm { std::map labelToExpressionMapping; if (preprocessedModel.isPrismProgram()) { labelToExpressionMapping = preprocessedModel.asPrismProgram().getLabelToExpressionMapping(); + } else { + storm::jani::Model const& janiModel = preprocessedModel.asJaniModel(); + for (auto const& variable : janiModel.getGlobalVariables().getBooleanVariables()) { + if (variable.isTransient()) { + labelToExpressionMapping[variable.getName()] = janiModel.getLabelExpression(variable.asBooleanVariable()); + } + } } - return performGameBasedAbstractionRefinement(checkTask.substituteFormula(pathFormula), preprocessedModel.getManager().boolean(true), pathFormula.getSubformula().toExpression(preprocessedModel.getManager(), labelToExpressionMapping)); + + storm::expressions::Expression constraintExpression = preprocessedModel.getManager().boolean(true); + storm::expressions::Expression targetStateExpression = pathFormula.getSubformula().toExpression(preprocessedModel.getManager(), labelToExpressionMapping); + + return performGameBasedAbstractionRefinement(checkTask.substituteFormula(pathFormula), constraintExpression, targetStateExpression); } template @@ -326,7 +351,7 @@ namespace storm { auto iterationStart = std::chrono::high_resolution_clock::now(); STORM_LOG_TRACE("Starting iteration " << iterations << "."); - // (1) build initial abstraction based on the the constraint expression (if not 'true') and the target state expression. + // (1) build the abstraction. auto abstractionStart = std::chrono::high_resolution_clock::now(); storm::abstraction::MenuGame game = abstractor->abstract(); auto abstractionEnd = std::chrono::high_resolution_clock::now(); @@ -447,17 +472,13 @@ namespace storm { std::vector GameBasedMdpModelChecker::getInitialPredicates(storm::expressions::Expression const& constraintExpression, storm::expressions::Expression const& targetStateExpression) { std::vector initialPredicates; if (preprocessedModel.isJaniModel()) { - storm::expressions::VariableSetAbstractor abstractor(preprocessedModel.asJaniModel().getAllLocationExpressionVariables()); + storm::expressions::VariableSetPredicateSplitter splitter(preprocessedModel.asJaniModel().getAllLocationExpressionVariables()); - storm::expressions::Expression abstractedExpression = abstractor.abstract(targetStateExpression); - if (abstractedExpression.isInitialized() && !abstractedExpression.isTrue() && !abstractedExpression.isFalse()) { - initialPredicates.push_back(abstractedExpression); - } - - abstractedExpression = abstractor.abstract(constraintExpression); - if (abstractedExpression.isInitialized() && !abstractedExpression.isTrue() && !abstractedExpression.isFalse()) { - initialPredicates.push_back(abstractedExpression); - } + std::vector splitExpressions = splitter.split(targetStateExpression); + initialPredicates.insert(initialPredicates.end(), splitExpressions.begin(), splitExpressions.end()); + + splitExpressions = splitter.split(constraintExpression); + initialPredicates.insert(initialPredicates.end(), splitExpressions.begin(), splitExpressions.end()); } else { if (!targetStateExpression.isTrue() && !targetStateExpression.isFalse()) { initialPredicates.push_back(targetStateExpression); diff --git a/src/storm/storage/expressions/PredicateSplitter.cpp b/src/storm/storage/expressions/FullPredicateSplitter.cpp similarity index 55% rename from src/storm/storage/expressions/PredicateSplitter.cpp rename to src/storm/storage/expressions/FullPredicateSplitter.cpp index 39ac62a6d..06b289847 100644 --- a/src/storm/storage/expressions/PredicateSplitter.cpp +++ b/src/storm/storage/expressions/FullPredicateSplitter.cpp @@ -1,4 +1,4 @@ -#include "storm/storage/expressions/PredicateSplitter.h" +#include "storm/storage/expressions/FullPredicateSplitter.h" #include "storm/storage/expressions/Expression.h" #include "storm/storage/expressions/Expressions.h" @@ -9,7 +9,7 @@ namespace storm { namespace expressions { - std::vector PredicateSplitter::split(storm::expressions::Expression const& expression) { + std::vector FullPredicateSplitter::split(storm::expressions::Expression const& expression) { STORM_LOG_THROW(expression.hasBooleanType(), storm::exceptions::InvalidArgumentException, "Expected predicate of boolean type."); // Gather all atoms. @@ -28,51 +28,51 @@ namespace storm { return atomicExpressions; } - boost::any PredicateSplitter::visit(IfThenElseExpression const& expression, boost::any const&) { - atomicExpressions.push_back(expression.shared_from_this()); + boost::any FullPredicateSplitter::visit(IfThenElseExpression const& expression, boost::any const&) { + atomicExpressions.push_back(expression.toExpression()); return boost::any(); } - boost::any PredicateSplitter::visit(BinaryBooleanFunctionExpression const& expression, boost::any const& data) { + boost::any FullPredicateSplitter::visit(BinaryBooleanFunctionExpression const& expression, boost::any const& data) { expression.getFirstOperand()->accept(*this, data); expression.getSecondOperand()->accept(*this, data); return boost::any(); } - boost::any PredicateSplitter::visit(BinaryNumericalFunctionExpression const&, boost::any const&) { + boost::any FullPredicateSplitter::visit(BinaryNumericalFunctionExpression const&, boost::any const&) { return boost::any(); } - boost::any PredicateSplitter::visit(BinaryRelationExpression const& expression, boost::any const&) { - atomicExpressions.push_back(expression.shared_from_this()); + boost::any FullPredicateSplitter::visit(BinaryRelationExpression const& expression, boost::any const&) { + atomicExpressions.push_back(expression.toExpression()); return boost::any(); } - boost::any PredicateSplitter::visit(VariableExpression const& expression, boost::any const&) { + boost::any FullPredicateSplitter::visit(VariableExpression const& expression, boost::any const&) { if (expression.hasBooleanType()) { - atomicExpressions.push_back(expression.shared_from_this()); + atomicExpressions.push_back(expression.toExpression()); } return boost::any(); } - boost::any PredicateSplitter::visit(UnaryBooleanFunctionExpression const& expression, boost::any const& data) { + boost::any FullPredicateSplitter::visit(UnaryBooleanFunctionExpression const& expression, boost::any const& data) { expression.getOperand()->accept(*this, data); return boost::any(); } - boost::any PredicateSplitter::visit(UnaryNumericalFunctionExpression const&, boost::any const&) { + boost::any FullPredicateSplitter::visit(UnaryNumericalFunctionExpression const&, boost::any const&) { return boost::any(); } - boost::any PredicateSplitter::visit(BooleanLiteralExpression const&, boost::any const&) { + boost::any FullPredicateSplitter::visit(BooleanLiteralExpression const&, boost::any const&) { return boost::any(); } - boost::any PredicateSplitter::visit(IntegerLiteralExpression const&, boost::any const&) { + boost::any FullPredicateSplitter::visit(IntegerLiteralExpression const&, boost::any const&) { return boost::any(); } - boost::any PredicateSplitter::visit(RationalLiteralExpression const&, boost::any const&) { + boost::any FullPredicateSplitter::visit(RationalLiteralExpression const&, boost::any const&) { return boost::any(); } diff --git a/src/storm/storage/expressions/PredicateSplitter.h b/src/storm/storage/expressions/FullPredicateSplitter.h similarity index 96% rename from src/storm/storage/expressions/PredicateSplitter.h rename to src/storm/storage/expressions/FullPredicateSplitter.h index 5fe784a18..0b8a360f8 100644 --- a/src/storm/storage/expressions/PredicateSplitter.h +++ b/src/storm/storage/expressions/FullPredicateSplitter.h @@ -8,7 +8,7 @@ namespace storm { namespace expressions { class Expression; - class PredicateSplitter : public ExpressionVisitor { + class FullPredicateSplitter : public ExpressionVisitor { public: std::vector split(storm::expressions::Expression const& expression); diff --git a/src/storm/storage/expressions/VariableSetAbstractor.cpp b/src/storm/storage/expressions/VariableSetAbstractor.cpp deleted file mode 100644 index 5820db995..000000000 --- a/src/storm/storage/expressions/VariableSetAbstractor.cpp +++ /dev/null @@ -1,225 +0,0 @@ -#include "storm/storage/expressions/VariableSetAbstractor.h" - -#include "storm/storage/expressions/Expressions.h" - -#include "storm/utility/macros.h" -#include "storm/exceptions/InvalidArgumentException.h" - -namespace storm { - namespace expressions { - - VariableSetAbstractor::VariableSetAbstractor(std::set const& variablesToAbstract) : variablesToAbstract(variablesToAbstract) { - // Intentionally left empty. - } - - storm::expressions::Expression VariableSetAbstractor::abstract(storm::expressions::Expression const& expression) { - std::set containedVariables = expression.getVariables(); - bool onlyAbstractedVariables = std::includes(variablesToAbstract.begin(), variablesToAbstract.end(), containedVariables.begin(), containedVariables.end()); - - if (onlyAbstractedVariables) { - return storm::expressions::Expression(); - } - - std::set tmp; - std::set_intersection(containedVariables.begin(), containedVariables.end(), variablesToAbstract.begin(), variablesToAbstract.end(), std::inserter(tmp, tmp.begin())); - bool hasAbstractedVariables = !tmp.empty(); - - if (hasAbstractedVariables) { - return boost::any_cast(expression.accept(*this, boost::none)); - } else { - return expression; - } - } - - boost::any VariableSetAbstractor::visit(IfThenElseExpression const& expression, boost::any const& data) { - std::set conditionVariables; - expression.getCondition()->gatherVariables(conditionVariables); - bool conditionOnlyAbstractedVariables = std::includes(variablesToAbstract.begin(), variablesToAbstract.end(), conditionVariables.begin(), conditionVariables.end()); - - std::set tmp; - std::set_intersection(conditionVariables.begin(), conditionVariables.end(), variablesToAbstract.begin(), variablesToAbstract.end(), std::inserter(tmp, tmp.begin())); - bool conditionHasAbstractedVariables = !tmp.empty(); - - std::set thenVariables; - expression.getThenExpression()->gatherVariables(thenVariables); - bool thenOnlyAbstractedVariables = std::includes(variablesToAbstract.begin(), variablesToAbstract.end(), thenVariables.begin(), thenVariables.end()); - - tmp.clear(); - std::set_intersection(thenVariables.begin(), thenVariables.end(), variablesToAbstract.begin(), variablesToAbstract.end(), std::inserter(tmp, tmp.begin())); - bool thenHasAbstractedVariables = !tmp.empty(); - - std::set elseVariables; - expression.getElseExpression()->gatherVariables(elseVariables); - bool elseOnlyAbstractedVariables = std::includes(variablesToAbstract.begin(), variablesToAbstract.end(), elseVariables.begin(), elseVariables.end()); - - tmp.clear(); - std::set_intersection(elseVariables.begin(), elseVariables.end(), variablesToAbstract.begin(), variablesToAbstract.end(), std::inserter(tmp, tmp.begin())); - bool elseHasAbstractedVariables = !tmp.empty(); - - if (conditionHasAbstractedVariables || thenHasAbstractedVariables || elseHasAbstractedVariables) { - if (conditionOnlyAbstractedVariables && thenOnlyAbstractedVariables && elseOnlyAbstractedVariables) { - return boost::any(); - } else { - STORM_LOG_THROW(false, storm::exceptions::InvalidArgumentException, "Cannot abstract from variable set in expression as it mixes variables of different types."); - } - } else { - return expression.toExpression(); - } - } - - boost::any VariableSetAbstractor::visit(BinaryBooleanFunctionExpression const& expression, boost::any const& data) { - std::set leftContainedVariables; - expression.getFirstOperand()->gatherVariables(leftContainedVariables); - bool leftOnlyAbstractedVariables = std::includes(variablesToAbstract.begin(), variablesToAbstract.end(), leftContainedVariables.begin(), leftContainedVariables.end()); - - std::set tmp; - std::set_intersection(leftContainedVariables.begin(), leftContainedVariables.end(), variablesToAbstract.begin(), variablesToAbstract.end(), std::inserter(tmp, tmp.begin())); - bool leftHasAbstractedVariables = !tmp.empty(); - - std::set rightContainedVariables; - expression.getSecondOperand()->gatherVariables(rightContainedVariables); - bool rightOnlyAbstractedVariables = std::includes(variablesToAbstract.begin(), variablesToAbstract.end(), rightContainedVariables.begin(), rightContainedVariables.end()); - - tmp.clear(); - std::set_intersection(rightContainedVariables.begin(), rightContainedVariables.end(), variablesToAbstract.begin(), variablesToAbstract.end(), std::inserter(tmp, tmp.begin())); - bool rightHasAbstractedVariables = !tmp.empty(); - - if (leftOnlyAbstractedVariables && rightOnlyAbstractedVariables) { - return boost::any(); - } else if (!leftHasAbstractedVariables && !rightHasAbstractedVariables) { - return expression; - } else { - if (leftHasAbstractedVariables && !rightHasAbstractedVariables) { - return expression.getFirstOperand()->toExpression(); - } else if (rightHasAbstractedVariables && !leftHasAbstractedVariables) { - return expression.getSecondOperand()->toExpression(); - } else { - storm::expressions::Expression leftResult = boost::any_cast(expression.getFirstOperand()->accept(*this, data)); - storm::expressions::Expression rightResult = boost::any_cast(expression.getFirstOperand()->accept(*this, data)); - - switch (expression.getOperatorType()) { - case storm::expressions::BinaryBooleanFunctionExpression::OperatorType::And: return leftResult && rightResult; - case storm::expressions::BinaryBooleanFunctionExpression::OperatorType::Or: return leftResult || rightResult; - case storm::expressions::BinaryBooleanFunctionExpression::OperatorType::Xor: return leftResult ^ rightResult; - case storm::expressions::BinaryBooleanFunctionExpression::OperatorType::Implies: return storm::expressions::implies(leftResult, rightResult); - case storm::expressions::BinaryBooleanFunctionExpression::OperatorType::Iff: return storm::expressions::iff(leftResult, rightResult); - } - } - } - } - - boost::any VariableSetAbstractor::visit(BinaryNumericalFunctionExpression const& expression, boost::any const& data) { - std::set leftContainedVariables; - expression.getFirstOperand()->gatherVariables(leftContainedVariables); - bool leftOnlyAbstractedVariables = std::includes(variablesToAbstract.begin(), variablesToAbstract.end(), leftContainedVariables.begin(), leftContainedVariables.end()); - - std::set tmp; - std::set_intersection(leftContainedVariables.begin(), leftContainedVariables.end(), variablesToAbstract.begin(), variablesToAbstract.end(), std::inserter(tmp, tmp.begin())); - bool leftHasAbstractedVariables = !tmp.empty(); - - std::set rightContainedVariables; - expression.getSecondOperand()->gatherVariables(rightContainedVariables); - bool rightOnlyAbstractedVariables = std::includes(variablesToAbstract.begin(), variablesToAbstract.end(), rightContainedVariables.begin(), rightContainedVariables.end()); - - tmp.clear(); - std::set_intersection(rightContainedVariables.begin(), rightContainedVariables.end(), variablesToAbstract.begin(), variablesToAbstract.end(), std::inserter(tmp, tmp.begin())); - bool rightHasAbstractedVariables = !tmp.empty(); - - if (leftOnlyAbstractedVariables && rightOnlyAbstractedVariables) { - return boost::any(); - } else if (!leftHasAbstractedVariables && !rightHasAbstractedVariables) { - return expression; - } else { - STORM_LOG_THROW(false, storm::exceptions::InvalidArgumentException, "Cannot abstract from variable set in expression as it mixes variables of different types."); - } - } - - boost::any VariableSetAbstractor::visit(BinaryRelationExpression const& expression, boost::any const& data) { - std::set leftContainedVariables; - expression.getFirstOperand()->gatherVariables(leftContainedVariables); - bool leftOnlyAbstractedVariables = std::includes(variablesToAbstract.begin(), variablesToAbstract.end(), leftContainedVariables.begin(), leftContainedVariables.end()); - - std::set tmp; - std::set_intersection(leftContainedVariables.begin(), leftContainedVariables.end(), variablesToAbstract.begin(), variablesToAbstract.end(), std::inserter(tmp, tmp.begin())); - bool leftHasAbstractedVariables = !tmp.empty(); - - std::set rightContainedVariables; - expression.getSecondOperand()->gatherVariables(rightContainedVariables); - bool rightOnlyAbstractedVariables = std::includes(variablesToAbstract.begin(), variablesToAbstract.end(), rightContainedVariables.begin(), rightContainedVariables.end()); - - tmp.clear(); - std::set_intersection(rightContainedVariables.begin(), rightContainedVariables.end(), variablesToAbstract.begin(), variablesToAbstract.end(), std::inserter(tmp, tmp.begin())); - bool rightHasAbstractedVariables = !tmp.empty(); - - if (leftOnlyAbstractedVariables && rightOnlyAbstractedVariables) { - return boost::any(); - } else if (!leftHasAbstractedVariables && !rightHasAbstractedVariables) { - return expression; - } else { - STORM_LOG_THROW(false, storm::exceptions::InvalidArgumentException, "Cannot abstract from variable set in expression as it mixes variables of different types."); - } - } - - boost::any VariableSetAbstractor::visit(VariableExpression const& expression, boost::any const& data) { - if (variablesToAbstract.find(expression.getVariable()) != variablesToAbstract.end()) { - return boost::any(); - } else { - return expression.toExpression(); - } - } - - boost::any VariableSetAbstractor::visit(UnaryBooleanFunctionExpression const& expression, boost::any const& data) { - std::set containedVariables; - expression.gatherVariables(containedVariables); - bool onlyAbstractedVariables = std::includes(variablesToAbstract.begin(), variablesToAbstract.end(), containedVariables.begin(), containedVariables.end()); - - if (onlyAbstractedVariables) { - return boost::any(); - } - - std::set tmp; - std::set_intersection(containedVariables.begin(), containedVariables.end(), variablesToAbstract.begin(), variablesToAbstract.end(), std::inserter(tmp, tmp.begin())); - bool hasAbstractedVariables = !tmp.empty(); - if (hasAbstractedVariables) { - storm::expressions::Expression subexpression = boost::any_cast(expression.getOperand()->accept(*this, data)); - switch (expression.getOperatorType()) { - case storm::expressions::UnaryBooleanFunctionExpression::OperatorType::Not: return !subexpression; - } - } else { - return expression.toExpression(); - } - } - - boost::any VariableSetAbstractor::visit(UnaryNumericalFunctionExpression const& expression, boost::any const& data) { - std::set containedVariables; - expression.gatherVariables(containedVariables); - bool onlyAbstractedVariables = std::includes(variablesToAbstract.begin(), variablesToAbstract.end(), containedVariables.begin(), containedVariables.end()); - - if (onlyAbstractedVariables) { - return boost::any(); - } - - std::set tmp; - std::set_intersection(containedVariables.begin(), containedVariables.end(), variablesToAbstract.begin(), variablesToAbstract.end(), std::inserter(tmp, tmp.begin())); - bool hasAbstractedVariables = !tmp.empty(); - if (hasAbstractedVariables) { - STORM_LOG_THROW(false, storm::exceptions::InvalidArgumentException, "Cannot abstract from variable set in expression as it mixes variables of different types."); - } else { - return expression.toExpression(); - } - } - - boost::any VariableSetAbstractor::visit(BooleanLiteralExpression const& expression, boost::any const& data) { - return expression.toExpression(); - } - - boost::any VariableSetAbstractor::visit(IntegerLiteralExpression const& expression, boost::any const& data) { - return expression.toExpression(); - } - - boost::any VariableSetAbstractor::visit(RationalLiteralExpression const& expression, boost::any const& data) { - return expression.toExpression(); - } - - } -} diff --git a/src/storm/storage/expressions/VariableSetPredicateSplitter.cpp b/src/storm/storage/expressions/VariableSetPredicateSplitter.cpp new file mode 100644 index 000000000..a6906ac8a --- /dev/null +++ b/src/storm/storage/expressions/VariableSetPredicateSplitter.cpp @@ -0,0 +1,180 @@ +#include "storm/storage/expressions/VariableSetPredicateSplitter.h" + +#include "storm/storage/expressions/Expressions.h" + +#include "storm/utility/macros.h" +#include "storm/exceptions/InvalidArgumentException.h" + +namespace storm { + namespace expressions { + + VariableSetPredicateSplitter::VariableSetPredicateSplitter(std::set const& irrelevantVariables) : irrelevantVariables(irrelevantVariables) { + // Intentionally left empty. + } + + std::vector VariableSetPredicateSplitter::split(storm::expressions::Expression const& expression) { + STORM_LOG_THROW(expression.hasBooleanType(), storm::exceptions::InvalidArgumentException, "Expected predicate of boolean type."); + + // Gather all atoms. + resultPredicates.clear(); + expression.accept(*this, boost::none); + + // Remove all boolean literals from the atoms. + std::vector expressionsToKeep; + for (auto const& atom : resultPredicates) { + if (!atom.isTrue() && !atom.isFalse()) { + expressionsToKeep.push_back(atom); + } + } + resultPredicates = std::move(expressionsToKeep); + + return resultPredicates; + } + + boost::any VariableSetPredicateSplitter::visit(IfThenElseExpression const& expression, boost::any const& data) { + std::set conditionVariables; + expression.getCondition()->gatherVariables(conditionVariables); + bool conditionOnlyIrrelevantVariables = std::includes(irrelevantVariables.begin(), irrelevantVariables.end(), conditionVariables.begin(), conditionVariables.end()); + + std::set tmp; + std::set_intersection(conditionVariables.begin(), conditionVariables.end(), irrelevantVariables.begin(), irrelevantVariables.end(), std::inserter(tmp, tmp.begin())); + bool conditionHasIrrelevantVariables = !tmp.empty(); + + std::set thenVariables; + expression.getThenExpression()->gatherVariables(thenVariables); + bool thenOnlyIrrelevantVariables = std::includes(irrelevantVariables.begin(), irrelevantVariables.end(), thenVariables.begin(), thenVariables.end()); + + tmp.clear(); + std::set_intersection(thenVariables.begin(), thenVariables.end(), irrelevantVariables.begin(), irrelevantVariables.end(), std::inserter(tmp, tmp.begin())); + bool thenHasIrrelevantVariables = !tmp.empty(); + + std::set elseVariables; + expression.getElseExpression()->gatherVariables(elseVariables); + bool elseOnlyIrrelevantVariables = std::includes(irrelevantVariables.begin(), irrelevantVariables.end(), elseVariables.begin(), elseVariables.end()); + + tmp.clear(); + std::set_intersection(elseVariables.begin(), elseVariables.end(), irrelevantVariables.begin(), irrelevantVariables.end(), std::inserter(tmp, tmp.begin())); + bool elseHasIrrelevantVariables = !tmp.empty(); + + if (conditionHasIrrelevantVariables || thenHasIrrelevantVariables || elseHasIrrelevantVariables) { + STORM_LOG_THROW(conditionOnlyIrrelevantVariables && thenOnlyIrrelevantVariables && elseOnlyIrrelevantVariables, storm::exceptions::InvalidArgumentException, "Cannot split expression based on variable set as variables of different type are related."); + } else { + resultPredicates.push_back(expression.toExpression()); + } + return boost::any(); + } + + boost::any VariableSetPredicateSplitter::visit(BinaryBooleanFunctionExpression const& expression, boost::any const& data) { + std::set leftContainedVariables; + expression.getFirstOperand()->gatherVariables(leftContainedVariables); + bool leftOnlyIrrelevantVariables = std::includes(irrelevantVariables.begin(), irrelevantVariables.end(), leftContainedVariables.begin(), leftContainedVariables.end()); + + std::set tmp; + std::set_intersection(leftContainedVariables.begin(), leftContainedVariables.end(), irrelevantVariables.begin(), irrelevantVariables.end(), std::inserter(tmp, tmp.begin())); + bool leftHasIrrelevantVariables = !tmp.empty(); + + std::set rightContainedVariables; + expression.getSecondOperand()->gatherVariables(rightContainedVariables); + bool rightOnlyIrrelevantVariables = std::includes(irrelevantVariables.begin(), irrelevantVariables.end(), rightContainedVariables.begin(), rightContainedVariables.end()); + + tmp.clear(); + std::set_intersection(rightContainedVariables.begin(), rightContainedVariables.end(), irrelevantVariables.begin(), irrelevantVariables.end(), std::inserter(tmp, tmp.begin())); + bool rightHasIrrelevantVariables = !tmp.empty(); + + if (leftOnlyIrrelevantVariables && rightOnlyIrrelevantVariables) { + return boost::any(); + } + + if (!leftHasIrrelevantVariables && !rightHasIrrelevantVariables) { + resultPredicates.push_back(expression.toExpression()); + } + + if (!leftHasIrrelevantVariables) { + resultPredicates.push_back(expression.getFirstOperand()->toExpression()); + } else if (!leftOnlyIrrelevantVariables) { + return expression.getFirstOperand()->accept(*this, data); + } + + if (!rightHasIrrelevantVariables) { + resultPredicates.push_back(expression.getSecondOperand()->toExpression()); + } else if (!rightOnlyIrrelevantVariables) { + return expression.getSecondOperand()->accept(*this, data); + } + return boost::any(); + } + + boost::any VariableSetPredicateSplitter::visit(BinaryNumericalFunctionExpression const& expression, boost::any const& data) { + return boost::any(); + } + + boost::any VariableSetPredicateSplitter::visit(BinaryRelationExpression const& expression, boost::any const& data) { + std::set leftContainedVariables; + expression.getFirstOperand()->gatherVariables(leftContainedVariables); + bool leftOnlyIrrelevantVariables = std::includes(irrelevantVariables.begin(), irrelevantVariables.end(), leftContainedVariables.begin(), leftContainedVariables.end()); + + std::set tmp; + std::set_intersection(leftContainedVariables.begin(), leftContainedVariables.end(), irrelevantVariables.begin(), irrelevantVariables.end(), std::inserter(tmp, tmp.begin())); + bool leftHasIrrelevantVariables = !tmp.empty(); + + std::set rightContainedVariables; + expression.getSecondOperand()->gatherVariables(rightContainedVariables); + bool rightOnlyIrrelevantVariables = std::includes(irrelevantVariables.begin(), irrelevantVariables.end(), rightContainedVariables.begin(), rightContainedVariables.end()); + + tmp.clear(); + std::set_intersection(rightContainedVariables.begin(), rightContainedVariables.end(), irrelevantVariables.begin(), irrelevantVariables.end(), std::inserter(tmp, tmp.begin())); + bool rightHasIrrelevantVariables = !tmp.empty(); + + if (!leftHasIrrelevantVariables && !rightHasIrrelevantVariables) { + resultPredicates.push_back(expression.toExpression()); + } else { + STORM_LOG_THROW(leftOnlyIrrelevantVariables && rightOnlyIrrelevantVariables, storm::exceptions::InvalidArgumentException, "Cannot abstract from variable set in expression as it mixes variables of different types."); + } + return boost::any(); + } + + boost::any VariableSetPredicateSplitter::visit(VariableExpression const& expression, boost::any const& data) { + if (expression.hasBooleanType() && irrelevantVariables.find(expression.getVariable()) == irrelevantVariables.end()) { + resultPredicates.push_back(expression.toExpression()); + } + return boost::any(); + } + + boost::any VariableSetPredicateSplitter::visit(UnaryBooleanFunctionExpression const& expression, boost::any const& data) { + std::set containedVariables; + expression.gatherVariables(containedVariables); + bool onlyIrrelevantVariables = std::includes(irrelevantVariables.begin(), irrelevantVariables.end(), containedVariables.begin(), containedVariables.end()); + + if (onlyIrrelevantVariables) { + return boost::any(); + } + + std::set tmp; + std::set_intersection(containedVariables.begin(), containedVariables.end(), irrelevantVariables.begin(), irrelevantVariables.end(), std::inserter(tmp, tmp.begin())); + bool hasIrrelevantVariables = !tmp.empty(); + + if (hasIrrelevantVariables) { + expression.getOperand()->accept(*this, data); + } else { + resultPredicates.push_back(expression.toExpression()); + } + return boost::any(); + } + + boost::any VariableSetPredicateSplitter::visit(UnaryNumericalFunctionExpression const& expression, boost::any const& data) { + return boost::any(); + } + + boost::any VariableSetPredicateSplitter::visit(BooleanLiteralExpression const& expression, boost::any const& data) { + return boost::any(); + } + + boost::any VariableSetPredicateSplitter::visit(IntegerLiteralExpression const& expression, boost::any const& data) { + return boost::any(); + } + + boost::any VariableSetPredicateSplitter::visit(RationalLiteralExpression const& expression, boost::any const& data) { + return boost::any(); + } + + } +} diff --git a/src/storm/storage/expressions/VariableSetAbstractor.h b/src/storm/storage/expressions/VariableSetPredicateSplitter.h similarity index 76% rename from src/storm/storage/expressions/VariableSetAbstractor.h rename to src/storm/storage/expressions/VariableSetPredicateSplitter.h index e5d905598..da1b1db46 100644 --- a/src/storm/storage/expressions/VariableSetAbstractor.h +++ b/src/storm/storage/expressions/VariableSetPredicateSplitter.h @@ -1,6 +1,7 @@ #pragma once #include +#include #include "storm/storage/expressions/ExpressionVisitor.h" @@ -10,11 +11,11 @@ namespace storm { class Variable; class Expression; - class VariableSetAbstractor : public ExpressionVisitor { + class VariableSetPredicateSplitter : public ExpressionVisitor { public: - VariableSetAbstractor(std::set const& variablesToAbstract); + VariableSetPredicateSplitter(std::set const& irrelevantVariables); - storm::expressions::Expression abstract(storm::expressions::Expression const& expression); + std::vector split(storm::expressions::Expression const& expression); virtual boost::any visit(IfThenElseExpression const& expression, boost::any const& data) override; virtual boost::any visit(BinaryBooleanFunctionExpression const& expression, boost::any const& data) override; @@ -28,7 +29,8 @@ namespace storm { virtual boost::any visit(RationalLiteralExpression const& expression, boost::any const& data) override; private: - std::set variablesToAbstract; + std::set irrelevantVariables; + std::vector resultPredicates; }; } diff --git a/src/storm/storage/jani/Automaton.cpp b/src/storm/storage/jani/Automaton.cpp index ad6bf5c57..f3dac4889 100644 --- a/src/storm/storage/jani/Automaton.cpp +++ b/src/storm/storage/jani/Automaton.cpp @@ -354,10 +354,10 @@ namespace storm { if (!hasInitialStatesRestriction()) { return false; } - if (getInitialStatesExpression().containsVariables()) { + if (getInitialStatesRestriction().containsVariables()) { return true; } else { - return !getInitialStatesExpression().evaluateAsBool(); + return !getInitialStatesRestriction().evaluateAsBool(); } }