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

more work on boolean transient variables in JANI menu game abstraction (labels)

main
dehnert 9 years ago
parent
ccf8631617
commit
3125ad4c89
11 changed files with 49 additions and 40 deletions
Whitespace
Show all changes Ignore whitespace when comparing lines Ignore changes in amount of whitespace Ignore changes in whitespace at EOL
Split View
Diff Options
Show Stats Download Patch File Download Diff File
  1. 21
      src/storm/abstraction/AbstractionInformation.cpp
  2. 10
      src/storm/abstraction/AbstractionInformation.h
  3. 6
      src/storm/abstraction/ExpressionTranslator.cpp
  4. 2
      src/storm/abstraction/MenuGameAbstractor.h
  5. 2
      src/storm/abstraction/MenuGameRefiner.cpp
  6. 2
      src/storm/abstraction/MenuGameRefiner.h
  7. 9
      src/storm/abstraction/jani/JaniMenuGameAbstractor.cpp
  8. 9
      src/storm/abstraction/jani/JaniMenuGameAbstractor.h
  9. 7
      src/storm/abstraction/prism/PrismMenuGameAbstractor.cpp
  10. 9
      src/storm/abstraction/prism/PrismMenuGameAbstractor.h
  11. 8
      src/storm/modelchecker/abstraction/GameBasedMdpModelChecker.cpp

21
src/storm/abstraction/AbstractionInformation.cpp
View File

@ -14,7 +14,7 @@ namespace storm {
namespace abstraction {
template<storm::dd::DdType DdType>
AbstractionInformation<DdType>::AbstractionInformation(storm::expressions::ExpressionManager& expressionManager, std::set<storm::expressions::Variable> const& abstractedVariables, std::unique_ptr<storm::solver::SmtSolver>&& smtSolver, std::shared_ptr<storm::dd::DdManager<DdType>> ddManager) : expressionManager(expressionManager), equivalenceChecker(std::move(smtSolver)), abstractedVariables(abstractedVariables), ddManager(ddManager), allPredicateIdentities(ddManager->getBddOne()), expressionToBddMap() {
AbstractionInformation<DdType>::AbstractionInformation(storm::expressions::ExpressionManager& expressionManager, std::set<storm::expressions::Variable> const& abstractedVariables, std::unique_ptr<storm::solver::SmtSolver>&& smtSolver, std::shared_ptr<storm::dd::DdManager<DdType>> ddManager) : expressionManager(expressionManager), equivalenceChecker(std::move(smtSolver)), abstractedVariables(abstractedVariables), ddManager(ddManager), allPredicateIdentities(ddManager->getBddOne()), allLocationIdentities(ddManager->getBddOne()), expressionToBddMap() {
// Intentionally left empty.
}
@ -292,6 +292,10 @@ namespace storm {
storm::dd::Bdd<DdType> const& AbstractionInformation<DdType>::getAllPredicateIdentities() const {
return allPredicateIdentities;
}
template<storm::dd::DdType DdType>
storm::dd::Bdd<DdType> const& AbstractionInformation<DdType>::getAllLocationIdentities() const {
return allLocationIdentities;
}
template<storm::dd::DdType DdType>
std::size_t AbstractionInformation<DdType>::getPlayer1VariableCount() const {
@ -483,12 +487,15 @@ namespace storm {
template <storm::dd::DdType DdType>
std::pair<std::pair<storm::expressions::Variable, storm::expressions::Variable>, uint64_t> AbstractionInformation<DdType>::addLocationVariables(uint64_t highestLocationIndex) {
locationVariablePairs.emplace_back(ddManager->addMetaVariable("loc_" + std::to_string(locationVariablePairs.size()), 0, highestLocationIndex));
allSourceLocationVariables.insert(locationVariablePairs.back().first);
sourceVariables.insert(locationVariablePairs.back().first);
allSuccessorLocationVariables.insert(locationVariablePairs.back().second);
successorVariables.insert(locationVariablePairs.back().second);
extendedPredicateDdVariables.emplace_back(locationVariablePairs.back());
auto newMetaVariable = ddManager->addMetaVariable("loc_" + std::to_string(locationVariablePairs.size()), 0, highestLocationIndex);
locationVariablePairs.emplace_back(newMetaVariable);
allSourceLocationVariables.insert(newMetaVariable.first);
sourceVariables.insert(newMetaVariable.first);
allSuccessorLocationVariables.insert(newMetaVariable.second);
successorVariables.insert(newMetaVariable.second);
extendedPredicateDdVariables.emplace_back(newMetaVariable);
allLocationIdentities &= ddManager->template getIdentity<uint64_t>(newMetaVariable.first).equals(ddManager->template getIdentity<uint64_t>(newMetaVariable.second)) && ddManager->getRange(newMetaVariable.first) && ddManager->getRange(newMetaVariable.second);
return std::make_pair(locationVariablePairs.back(), locationVariablePairs.size() - 1);
}

10
src/storm/abstraction/AbstractionInformation.h
View File

@ -348,6 +348,13 @@ namespace storm {
*/
storm::dd::Bdd<DdType> const& getAllPredicateIdentities() const;
/*!
* Retrieves a BDD representing the identities of all location variables.
*
* @return All location identities.
*/
storm::dd::Bdd<DdType> const& getAllLocationIdentities() const;
/*!
* Retrieves a mapping of the known predicates to the BDDs that represent the corresponding states.
*
@ -559,6 +566,9 @@ namespace storm {
/// A BDD that represents the identity of all predicate variables.
storm::dd::Bdd<DdType> allPredicateIdentities;
/// A BDD that represents the identity of all location variables.
storm::dd::Bdd<DdType> allLocationIdentities;
/// A meta variable pair that marks bottom states.
std::pair<storm::expressions::Variable, storm::expressions::Variable> bottomStateVariables;

6
src/storm/abstraction/ExpressionTranslator.cpp
View File

@ -58,7 +58,7 @@ namespace storm {
}
storm::dd::Bdd<DdType> left = boost::any_cast<storm::dd::Bdd<DdType>>(expression.getFirstOperand()->accept(*this, boost::none));
storm::dd::Bdd<DdType> right = boost::any_cast<storm::dd::Bdd<DdType>>(expression.getFirstOperand()->accept(*this, boost::none));
storm::dd::Bdd<DdType> right = boost::any_cast<storm::dd::Bdd<DdType>>(expression.getSecondOperand()->accept(*this, boost::none));
switch (expression.getOperatorType()) {
case BinaryBooleanFunctionExpression::OperatorType::And: return left && right;
case BinaryBooleanFunctionExpression::OperatorType::Or: return left || right;
@ -93,7 +93,7 @@ namespace storm {
if (hasLocationVariables) {
storm::dd::Add<DdType, double> left = boost::any_cast<storm::dd::Add<DdType, double>>(expression.getFirstOperand()->accept(*this, boost::none));
storm::dd::Add<DdType, double> right = boost::any_cast<storm::dd::Add<DdType, double>>(expression.getFirstOperand()->accept(*this, boost::none));
storm::dd::Add<DdType, double> right = boost::any_cast<storm::dd::Add<DdType, double>>(expression.getSecondOperand()->accept(*this, boost::none));
switch (expression.getRelationType()) {
case BinaryRelationExpression::RelationType::Equal: return left.equals(right);
@ -180,7 +180,7 @@ namespace storm {
template <storm::dd::DdType DdType>
boost::any ExpressionTranslator<DdType>::visit(IntegerLiteralExpression const& expression, boost::any const& data) {
return abstractionInformation.get().getDdManager().template getConstant(expression.getValue());
return abstractionInformation.get().getDdManager().template getConstant<double>(expression.getValue());
}
template <storm::dd::DdType DdType>

2
src/storm/abstraction/MenuGameAbstractor.h
View File

@ -38,7 +38,7 @@ namespace storm {
* Retrieves a BDD that characterizes the states corresponding to the given expression. For this to work,
* appropriate predicates must have been used to refine the abstraction, otherwise this will fail.
*/
virtual storm::dd::Bdd<DdType> getStates(storm::expressions::Expression const& expression) const = 0;
virtual storm::dd::Bdd<DdType> getStates(storm::expressions::Expression const& expression) = 0;
/// Methods to refine the abstraction.
virtual void refine(RefinementCommand const& command) = 0;

2
src/storm/abstraction/MenuGameRefiner.cpp
View File

@ -74,7 +74,7 @@ namespace storm {
template<storm::dd::DdType Type, typename ValueType>
void MenuGameRefiner<Type, ValueType>::refine(std::vector<storm::expressions::Expression> const& predicates) const {
performRefinement(createGlobalRefinement(predicates));
performRefinement(createGlobalRefinement(preprocessPredicates(predicates, RefinementPredicates::Source::Manual)));
}
template<storm::dd::DdType Type, typename ValueType>

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

@ -32,7 +32,7 @@ namespace storm {
class RefinementPredicates {
public:
enum class Source {
WeakestPrecondition, InitialGuard, Guard, Interpolation
WeakestPrecondition, InitialGuard, Guard, Interpolation, Manual
};
RefinementPredicates() = default;

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

@ -2,6 +2,7 @@
#include "storm/abstraction/BottomStateResult.h"
#include "storm/abstraction/GameBddResult.h"
#include "storm/abstraction/ExpressionTranslator.h"
#include "storm/storage/BitVector.h"
@ -128,9 +129,9 @@ namespace storm {
}
template <storm::dd::DdType DdType, typename ValueType>
storm::dd::Bdd<DdType> JaniMenuGameAbstractor<DdType, ValueType>::getStates(storm::expressions::Expression const& predicate) const {
STORM_LOG_ASSERT(currentGame != nullptr, "Game was not properly created.");
return abstractionInformation.getPredicateSourceVariable(predicate);
storm::dd::Bdd<DdType> JaniMenuGameAbstractor<DdType, ValueType>::getStates(storm::expressions::Expression const& expression) {
storm::abstraction::ExpressionTranslator<DdType> translator(abstractionInformation, smtSolverFactory->create(abstractionInformation.getExpressionManager()));
return translator.translate(expression);
}
template <storm::dd::DdType DdType, typename ValueType>
@ -161,7 +162,7 @@ namespace storm {
// If there are deadlock states, we fix them now.
storm::dd::Add<DdType, ValueType> deadlockTransitions = abstractionInformation.getDdManager().template getAddZero<ValueType>();
if (!deadlockStates.isZero()) {
deadlockTransitions = (deadlockStates && abstractionInformation.getAllPredicateIdentities() && abstractionInformation.encodePlayer1Choice(0, abstractionInformation.getPlayer1VariableCount()) && abstractionInformation.encodePlayer2Choice(0, 0, game.numberOfPlayer2Variables) && abstractionInformation.encodeAux(0, 0, abstractionInformation.getAuxVariableCount())).template toAdd<ValueType>();
deadlockTransitions = (deadlockStates && abstractionInformation.getAllPredicateIdentities() && abstractionInformation.getAllLocationIdentities() && abstractionInformation.encodePlayer1Choice(0, abstractionInformation.getPlayer1VariableCount()) && abstractionInformation.encodePlayer2Choice(0, 0, game.numberOfPlayer2Variables) && abstractionInformation.encodeAux(0, 0, abstractionInformation.getAuxVariableCount())).template toAdd<ValueType>();
}
// Compute bottom states and the appropriate transitions if necessary.

9
src/storm/abstraction/jani/JaniMenuGameAbstractor.h
View File

@ -91,14 +91,7 @@ namespace storm {
*/
storm::expressions::Expression getInitialExpression() const override;
/*!
* Retrieves the set of states (represented by a BDD) satisfying the given predicate, assuming that it
* was either given as an initial predicate or used as a refining predicate later.
*
* @param predicate The predicate for which to retrieve the states.
* @return The BDD representing the set of states.
*/
storm::dd::Bdd<DdType> getStates(storm::expressions::Expression const& predicate) const override;
storm::dd::Bdd<DdType> getStates(storm::expressions::Expression const& expression) override;
/*!
* Performs the given refinement command.

7
src/storm/abstraction/prism/PrismMenuGameAbstractor.cpp
View File

@ -2,6 +2,7 @@
#include "storm/abstraction/BottomStateResult.h"
#include "storm/abstraction/GameBddResult.h"
#include "storm/abstraction/ExpressionTranslator.h"
#include "storm/storage/BitVector.h"
@ -129,9 +130,9 @@ namespace storm {
}
template <storm::dd::DdType DdType, typename ValueType>
storm::dd::Bdd<DdType> PrismMenuGameAbstractor<DdType, ValueType>::getStates(storm::expressions::Expression const& expression) const {
STORM_LOG_ASSERT(currentGame != nullptr, "Game was not properly created.");
return abstractionInformation.getPredicateSourceVariable(expression);
storm::dd::Bdd<DdType> PrismMenuGameAbstractor<DdType, ValueType>::getStates(storm::expressions::Expression const& expression) {
storm::abstraction::ExpressionTranslator<DdType> translator(abstractionInformation, smtSolverFactory->create(abstractionInformation.getExpressionManager()));
return translator.translate(expression);
}
template <storm::dd::DdType DdType, typename ValueType>

9
src/storm/abstraction/prism/PrismMenuGameAbstractor.h
View File

@ -91,14 +91,7 @@ namespace storm {
*/
storm::expressions::Expression getInitialExpression() const override;
/*!
* Retrieves the set of states (represented by a BDD) satisfying the given predicate, assuming that it
* was either given as an initial predicate or used as a refining predicate later.
*
* @param predicate The predicate for which to retrieve the states.
* @return The BDD representing the set of states.
*/
storm::dd::Bdd<DdType> getStates(storm::expressions::Expression const& expression) const;
storm::dd::Bdd<DdType> getStates(storm::expressions::Expression const& expression) override;
/*!
* Performs the given refinement command.

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

@ -311,6 +311,10 @@ namespace storm {
storm::abstraction::MenuGameRefiner<Type, ValueType> refiner(*abstractor, smtSolverFactory->create(preprocessedModel.getManager()));
refiner.refine(initialPredicates);
storm::dd::Bdd<Type> globalConstraintStates = abstractor->getStates(constraintExpression);
storm::dd::Bdd<Type> globalTargetStates = abstractor->getStates(targetStateExpression);
globalTargetStates.template toAdd<ValueType>().exportToDot("target.dot");
// Enter the main-loop of abstraction refinement.
boost::optional<QualitativeResultMinMax<Type>> previousQualitativeResult = boost::none;
boost::optional<QuantitativeResult<Type, ValueType>> previousMinQuantitativeResult = boost::none;
@ -328,8 +332,8 @@ namespace storm {
// (2) Prepare transition matrix BDD and target state BDD for later use.
storm::dd::Bdd<Type> transitionMatrixBdd = game.getTransitionMatrix().toBdd();
storm::dd::Bdd<Type> initialStates = game.getInitialStates();
storm::dd::Bdd<Type> constraintStates = game.getStates(constraintExpression);
storm::dd::Bdd<Type> targetStates = game.getStates(targetStateExpression);
storm::dd::Bdd<Type> constraintStates = globalConstraintStates && game.getReachableStates();
storm::dd::Bdd<Type> targetStates = globalTargetStates && game.getReachableStates();
if (player1Direction == storm::OptimizationDirection::Minimize) {
targetStates |= game.getBottomStates();
}

Write Preview
Loading…
Cancel
Save