sp
/
tempest
1
0
Fork 0
Code Issues Pull Requests Projects Releases Wiki Activity
Browse Source

initial support for transient boolean variables in formulas of JANI models (game-based engine)

main
dehnert 8 years ago
parent
696a2e7ce1
commit
b9e4d6f334
9 changed files with 243 additions and 265 deletions
Whitespace
Show all changes Ignore whitespace when comparing lines Ignore changes in amount of whitespace Ignore changes in whitespace at EOL
Unified View
Diff Options
Show Stats Download Patch File Download Diff File
  1. 4
      src/storm/abstraction/MenuGameRefiner.h
  2. 2
      src/storm/abstraction/jani/JaniMenuGameAbstractor.cpp
  3. 51
      src/storm/modelchecker/abstraction/GameBasedMdpModelChecker.cpp
  4. 30
      src/storm/storage/expressions/FullPredicateSplitter.cpp
  5. 2
      src/storm/storage/expressions/FullPredicateSplitter.h
  6. 225
      src/storm/storage/expressions/VariableSetAbstractor.cpp
  7. 180
      src/storm/storage/expressions/VariableSetPredicateSplitter.cpp
  8. 10
      src/storm/storage/expressions/VariableSetPredicateSplitter.h
  9. 4
      src/storm/storage/jani/Automaton.cpp

4
src/storm/abstraction/MenuGameRefiner.h
View File

@ -11,7 +11,7 @@
#include "storm/abstraction/QuantitativeResultMinMax.h" #include "storm/abstraction/QuantitativeResultMinMax.h"
#include "storm/storage/expressions/Expression.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/expressions/EquivalenceChecker.h"
#include "storm/storage/dd/DdType.h" #include "storm/storage/dd/DdType.h"
@ -143,7 +143,7 @@ namespace storm {
storm::settings::modules::AbstractionSettings::PivotSelectionHeuristic pivotSelectionHeuristic; storm::settings::modules::AbstractionSettings::PivotSelectionHeuristic pivotSelectionHeuristic;
/// An object that can be used for splitting predicates. /// 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. /// An object that can be used to determine whether predicates are equivalent.
mutable storm::expressions::EquivalenceChecker equivalenceChecker; mutable storm::expressions::EquivalenceChecker equivalenceChecker;

2
src/storm/abstraction/jani/JaniMenuGameAbstractor.cpp
View File

@ -32,7 +32,7 @@ namespace storm {
using storm::settings::modules::AbstractionSettings; using storm::settings::modules::AbstractionSettings;
template <storm::dd::DdType DdType, typename ValueType> template <storm::dd::DdType DdType, typename ValueType>
JaniMenuGameAbstractor<DdType, ValueType>::JaniMenuGameAbstractor(storm::jani::Model const& model, std::shared_ptr<storm::utility::solver::SmtSolverFactory> 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<DdType, ValueType>::JaniMenuGameAbstractor(storm::jani::Model const& model, std::shared_ptr<storm::utility::solver::SmtSolverFactory> 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 // 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. // to be flattened before the procedure.

51
src/storm/modelchecker/abstraction/GameBasedMdpModelChecker.cpp
View File

@ -8,7 +8,7 @@
#include "storm/models/symbolic/Mdp.h" #include "storm/models/symbolic/Mdp.h"
#include "storm/storage/expressions/ExpressionManager.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" #include "storm/storage/dd/DdManager.h"
@ -78,8 +78,22 @@ namespace storm {
template<storm::dd::DdType Type, typename ModelType> template<storm::dd::DdType Type, typename ModelType>
std::unique_ptr<CheckResult> GameBasedMdpModelChecker<Type, ModelType>::computeUntilProbabilities(CheckTask<storm::logic::UntilFormula> const& checkTask) { std::unique_ptr<CheckResult> GameBasedMdpModelChecker<Type, ModelType>::computeUntilProbabilities(CheckTask<storm::logic::UntilFormula> const& checkTask) {
storm::logic::UntilFormula const& pathFormula = checkTask.getFormula(); storm::logic::UntilFormula const& pathFormula = checkTask.getFormula();
std::map<std::string, storm::expressions::Expression> labelToExpressionMapping = preprocessedModel.asPrismProgram().getLabelToExpressionMapping();
return performGameBasedAbstractionRefinement(checkTask.substituteFormula<storm::logic::Formula>(pathFormula), pathFormula.getLeftSubformula().toExpression(preprocessedModel.getManager(), labelToExpressionMapping), pathFormula.getRightSubformula().toExpression(preprocessedModel.getManager(), labelToExpressionMapping));
std::map<std::string, storm::expressions::Expression> 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<storm::logic::Formula>(pathFormula), constraintExpression, targetStateExpression);
} }
template<storm::dd::DdType Type, typename ModelType> template<storm::dd::DdType Type, typename ModelType>
@ -88,8 +102,19 @@ namespace storm {
std::map<std::string, storm::expressions::Expression> labelToExpressionMapping; std::map<std::string, storm::expressions::Expression> labelToExpressionMapping;
if (preprocessedModel.isPrismProgram()) { if (preprocessedModel.isPrismProgram()) {
labelToExpressionMapping = preprocessedModel.asPrismProgram().getLabelToExpressionMapping(); 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<storm::logic::Formula>(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<storm::logic::Formula>(pathFormula), constraintExpression, targetStateExpression);
} }
template<storm::dd::DdType Type, typename ValueType> template<storm::dd::DdType Type, typename ValueType>
@ -326,7 +351,7 @@ namespace storm {
auto iterationStart = std::chrono::high_resolution_clock::now(); auto iterationStart = std::chrono::high_resolution_clock::now();
STORM_LOG_TRACE("Starting iteration " << iterations << "."); 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(); auto abstractionStart = std::chrono::high_resolution_clock::now();
storm::abstraction::MenuGame<Type, ValueType> game = abstractor->abstract(); storm::abstraction::MenuGame<Type, ValueType> game = abstractor->abstract();
auto abstractionEnd = std::chrono::high_resolution_clock::now(); auto abstractionEnd = std::chrono::high_resolution_clock::now();
@ -447,17 +472,13 @@ namespace storm {
std::vector<storm::expressions::Expression> GameBasedMdpModelChecker<Type, ModelType>::getInitialPredicates(storm::expressions::Expression const& constraintExpression, storm::expressions::Expression const& targetStateExpression) { std::vector<storm::expressions::Expression> GameBasedMdpModelChecker<Type, ModelType>::getInitialPredicates(storm::expressions::Expression const& constraintExpression, storm::expressions::Expression const& targetStateExpression) {
std::vector<storm::expressions::Expression> initialPredicates; std::vector<storm::expressions::Expression> initialPredicates;
if (preprocessedModel.isJaniModel()) { 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<storm::expressions::Expression> 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 { } else {
if (!targetStateExpression.isTrue() && !targetStateExpression.isFalse()) { if (!targetStateExpression.isTrue() && !targetStateExpression.isFalse()) {
initialPredicates.push_back(targetStateExpression); initialPredicates.push_back(targetStateExpression);

30
src/storm/storage/expressions/PredicateSplitter.cpp → src/storm/storage/expressions/FullPredicateSplitter.cpp
View File

@ -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/Expression.h"
#include "storm/storage/expressions/Expressions.h" #include "storm/storage/expressions/Expressions.h"
@ -9,7 +9,7 @@
namespace storm { namespace storm {
namespace expressions { namespace expressions {
std::vector<storm::expressions::Expression> PredicateSplitter::split(storm::expressions::Expression const& expression) {
std::vector<storm::expressions::Expression> FullPredicateSplitter::split(storm::expressions::Expression const& expression) {
STORM_LOG_THROW(expression.hasBooleanType(), storm::exceptions::InvalidArgumentException, "Expected predicate of boolean type."); STORM_LOG_THROW(expression.hasBooleanType(), storm::exceptions::InvalidArgumentException, "Expected predicate of boolean type.");
// Gather all atoms. // Gather all atoms.
@ -28,51 +28,51 @@ namespace storm {
return atomicExpressions; 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(); 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.getFirstOperand()->accept(*this, data);
expression.getSecondOperand()->accept(*this, data); expression.getSecondOperand()->accept(*this, data);
return boost::any(); return boost::any();
} }
boost::any PredicateSplitter::visit(BinaryNumericalFunctionExpression const&, boost::any const&) {
boost::any FullPredicateSplitter::visit(BinaryNumericalFunctionExpression const&, boost::any const&) {
return boost::any(); 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(); 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()) { if (expression.hasBooleanType()) {
atomicExpressions.push_back(expression.shared_from_this());
atomicExpressions.push_back(expression.toExpression());
} }
return boost::any(); 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); expression.getOperand()->accept(*this, data);
return boost::any(); return boost::any();
} }
boost::any PredicateSplitter::visit(UnaryNumericalFunctionExpression const&, boost::any const&) {
boost::any FullPredicateSplitter::visit(UnaryNumericalFunctionExpression const&, boost::any const&) {
return boost::any(); return boost::any();
} }
boost::any PredicateSplitter::visit(BooleanLiteralExpression const&, boost::any const&) {
boost::any FullPredicateSplitter::visit(BooleanLiteralExpression const&, boost::any const&) {
return boost::any(); return boost::any();
} }
boost::any PredicateSplitter::visit(IntegerLiteralExpression const&, boost::any const&) {
boost::any FullPredicateSplitter::visit(IntegerLiteralExpression const&, boost::any const&) {
return boost::any(); return boost::any();
} }
boost::any PredicateSplitter::visit(RationalLiteralExpression const&, boost::any const&) {
boost::any FullPredicateSplitter::visit(RationalLiteralExpression const&, boost::any const&) {
return boost::any(); return boost::any();
} }

2
src/storm/storage/expressions/PredicateSplitter.h → src/storm/storage/expressions/FullPredicateSplitter.h
View File

@ -8,7 +8,7 @@ namespace storm {
namespace expressions { namespace expressions {
class Expression; class Expression;
class PredicateSplitter : public ExpressionVisitor {
class FullPredicateSplitter : public ExpressionVisitor {
public: public:
std::vector<storm::expressions::Expression> split(storm::expressions::Expression const& expression); std::vector<storm::expressions::Expression> split(storm::expressions::Expression const& expression);

225
src/storm/storage/expressions/VariableSetAbstractor.cpp
View File

@ -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<storm::expressions::Variable> const& variablesToAbstract) : variablesToAbstract(variablesToAbstract) {
// Intentionally left empty.
}
storm::expressions::Expression VariableSetAbstractor::abstract(storm::expressions::Expression const& expression) {
std::set<storm::expressions::Variable> containedVariables = expression.getVariables();
bool onlyAbstractedVariables = std::includes(variablesToAbstract.begin(), variablesToAbstract.end(), containedVariables.begin(), containedVariables.end());
if (onlyAbstractedVariables) {
return storm::expressions::Expression();
}
std::set<storm::expressions::Variable> 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<storm::expressions::Expression>(expression.accept(*this, boost::none));
} else {
return expression;
}
}
boost::any VariableSetAbstractor::visit(IfThenElseExpression const& expression, boost::any const& data) {
std::set<storm::expressions::Variable> conditionVariables;
expression.getCondition()->gatherVariables(conditionVariables);
bool conditionOnlyAbstractedVariables = std::includes(variablesToAbstract.begin(), variablesToAbstract.end(), conditionVariables.begin(), conditionVariables.end());
std::set<storm::expressions::Variable> tmp;
std::set_intersection(conditionVariables.begin(), conditionVariables.end(), variablesToAbstract.begin(), variablesToAbstract.end(), std::inserter(tmp, tmp.begin()));
bool conditionHasAbstractedVariables = !tmp.empty();
std::set<storm::expressions::Variable> 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<storm::expressions::Variable> 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<storm::expressions::Variable> leftContainedVariables;
expression.getFirstOperand()->gatherVariables(leftContainedVariables);
bool leftOnlyAbstractedVariables = std::includes(variablesToAbstract.begin(), variablesToAbstract.end(), leftContainedVariables.begin(), leftContainedVariables.end());
std::set<storm::expressions::Variable> tmp;
std::set_intersection(leftContainedVariables.begin(), leftContainedVariables.end(), variablesToAbstract.begin(), variablesToAbstract.end(), std::inserter(tmp, tmp.begin()));
bool leftHasAbstractedVariables = !tmp.empty();
std::set<storm::expressions::Variable> 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<storm::expressions::Expression>(expression.getFirstOperand()->accept(*this, data));
storm::expressions::Expression rightResult = boost::any_cast<storm::expressions::Expression>(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<storm::expressions::Variable> leftContainedVariables;
expression.getFirstOperand()->gatherVariables(leftContainedVariables);
bool leftOnlyAbstractedVariables = std::includes(variablesToAbstract.begin(), variablesToAbstract.end(), leftContainedVariables.begin(), leftContainedVariables.end());
std::set<storm::expressions::Variable> tmp;
std::set_intersection(leftContainedVariables.begin(), leftContainedVariables.end(), variablesToAbstract.begin(), variablesToAbstract.end(), std::inserter(tmp, tmp.begin()));
bool leftHasAbstractedVariables = !tmp.empty();
std::set<storm::expressions::Variable> 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<storm::expressions::Variable> leftContainedVariables;
expression.getFirstOperand()->gatherVariables(leftContainedVariables);
bool leftOnlyAbstractedVariables = std::includes(variablesToAbstract.begin(), variablesToAbstract.end(), leftContainedVariables.begin(), leftContainedVariables.end());
std::set<storm::expressions::Variable> tmp;
std::set_intersection(leftContainedVariables.begin(), leftContainedVariables.end(), variablesToAbstract.begin(), variablesToAbstract.end(), std::inserter(tmp, tmp.begin()));
bool leftHasAbstractedVariables = !tmp.empty();
std::set<storm::expressions::Variable> 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<storm::expressions::Variable> containedVariables;
expression.gatherVariables(containedVariables);
bool onlyAbstractedVariables = std::includes(variablesToAbstract.begin(), variablesToAbstract.end(), containedVariables.begin(), containedVariables.end());
if (onlyAbstractedVariables) {
return boost::any();
}
std::set<storm::expressions::Variable> 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<storm::expressions::Expression>(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<storm::expressions::Variable> containedVariables;
expression.gatherVariables(containedVariables);
bool onlyAbstractedVariables = std::includes(variablesToAbstract.begin(), variablesToAbstract.end(), containedVariables.begin(), containedVariables.end());
if (onlyAbstractedVariables) {
return boost::any();
}
std::set<storm::expressions::Variable> 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();
}
}
}

180
src/storm/storage/expressions/VariableSetPredicateSplitter.cpp
View File

@ -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<storm::expressions::Variable> const& irrelevantVariables) : irrelevantVariables(irrelevantVariables) {
// Intentionally left empty.
}
std::vector<storm::expressions::Expression> 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<storm::expressions::Expression> 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<storm::expressions::Variable> conditionVariables;
expression.getCondition()->gatherVariables(conditionVariables);
bool conditionOnlyIrrelevantVariables = std::includes(irrelevantVariables.begin(), irrelevantVariables.end(), conditionVariables.begin(), conditionVariables.end());
std::set<storm::expressions::Variable> tmp;
std::set_intersection(conditionVariables.begin(), conditionVariables.end(), irrelevantVariables.begin(), irrelevantVariables.end(), std::inserter(tmp, tmp.begin()));
bool conditionHasIrrelevantVariables = !tmp.empty();
std::set<storm::expressions::Variable> 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<storm::expressions::Variable> 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<storm::expressions::Variable> leftContainedVariables;
expression.getFirstOperand()->gatherVariables(leftContainedVariables);
bool leftOnlyIrrelevantVariables = std::includes(irrelevantVariables.begin(), irrelevantVariables.end(), leftContainedVariables.begin(), leftContainedVariables.end());
std::set<storm::expressions::Variable> tmp;
std::set_intersection(leftContainedVariables.begin(), leftContainedVariables.end(), irrelevantVariables.begin(), irrelevantVariables.end(), std::inserter(tmp, tmp.begin()));
bool leftHasIrrelevantVariables = !tmp.empty();
std::set<storm::expressions::Variable> 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<storm::expressions::Variable> leftContainedVariables;
expression.getFirstOperand()->gatherVariables(leftContainedVariables);
bool leftOnlyIrrelevantVariables = std::includes(irrelevantVariables.begin(), irrelevantVariables.end(), leftContainedVariables.begin(), leftContainedVariables.end());
std::set<storm::expressions::Variable> tmp;
std::set_intersection(leftContainedVariables.begin(), leftContainedVariables.end(), irrelevantVariables.begin(), irrelevantVariables.end(), std::inserter(tmp, tmp.begin()));
bool leftHasIrrelevantVariables = !tmp.empty();
std::set<storm::expressions::Variable> 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<storm::expressions::Variable> containedVariables;
expression.gatherVariables(containedVariables);
bool onlyIrrelevantVariables = std::includes(irrelevantVariables.begin(), irrelevantVariables.end(), containedVariables.begin(), containedVariables.end());
if (onlyIrrelevantVariables) {
return boost::any();
}
std::set<storm::expressions::Variable> 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();
}
}
}

10
src/storm/storage/expressions/VariableSetAbstractor.h → src/storm/storage/expressions/VariableSetPredicateSplitter.h
View File

@ -1,6 +1,7 @@
#pragma once #pragma once
#include <set> #include <set>
#include <vector>
#include "storm/storage/expressions/ExpressionVisitor.h" #include "storm/storage/expressions/ExpressionVisitor.h"
@ -10,11 +11,11 @@ namespace storm {
class Variable; class Variable;
class Expression; class Expression;
class VariableSetAbstractor : public ExpressionVisitor {
class VariableSetPredicateSplitter : public ExpressionVisitor {
public: public:
VariableSetAbstractor(std::set<storm::expressions::Variable> const& variablesToAbstract);
VariableSetPredicateSplitter(std::set<storm::expressions::Variable> const& irrelevantVariables);
storm::expressions::Expression abstract(storm::expressions::Expression const& expression);
std::vector<storm::expressions::Expression> split(storm::expressions::Expression const& expression);
virtual boost::any visit(IfThenElseExpression const& expression, boost::any const& data) override; virtual boost::any visit(IfThenElseExpression const& expression, boost::any const& data) override;
virtual boost::any visit(BinaryBooleanFunctionExpression 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; virtual boost::any visit(RationalLiteralExpression const& expression, boost::any const& data) override;
private: private:
std::set<storm::expressions::Variable> variablesToAbstract;
std::set<storm::expressions::Variable> irrelevantVariables;
std::vector<storm::expressions::Expression> resultPredicates;
}; };
} }

4
src/storm/storage/jani/Automaton.cpp
View File

@ -354,10 +354,10 @@ namespace storm {
if (!hasInitialStatesRestriction()) { if (!hasInitialStatesRestriction()) {
return false; return false;
} }
if (getInitialStatesExpression().containsVariables()) {
if (getInitialStatesRestriction().containsVariables()) {
return true; return true;
} else { } else {
return !getInitialStatesExpression().evaluateAsBool();
return !getInitialStatesRestriction().evaluateAsBool();
} }
} }

Write Preview
Loading…
Cancel
Save