Browse Source
added state-set abstractor as a means to, e.g., derive the initial states BDD
added state-set abstractor as a means to, e.g., derive the initial states BDD
Former-commit-id: 34257c7196
tempestpy_adaptions
dehnert
9 years ago
13 changed files with 357 additions and 47 deletions
-
25src/storage/prism/menu_games/AbstractCommand.cpp
-
27src/storage/prism/menu_games/AbstractCommand.h
-
4src/storage/prism/menu_games/AbstractModule.cpp
-
8src/storage/prism/menu_games/AbstractModule.h
-
50src/storage/prism/menu_games/AbstractProgram.cpp
-
11src/storage/prism/menu_games/AbstractProgram.h
-
17src/storage/prism/menu_games/AbstractionDdInformation.cpp
-
11src/storage/prism/menu_games/AbstractionDdInformation.h
-
2src/storage/prism/menu_games/AbstractionExpressionInformation.cpp
-
9src/storage/prism/menu_games/AbstractionExpressionInformation.h
-
114src/storage/prism/menu_games/StateSetAbstractor.cpp
-
117src/storage/prism/menu_games/StateSetAbstractor.h
-
7src/storage/prism/menu_games/VariablePartition.cpp
@ -0,0 +1,114 @@ |
|||
#include "src/storage/prism/menu_games/StateSetAbstractor.h"
|
|||
|
|||
#include "src/storage/prism/menu_games/AbstractionExpressionInformation.h"
|
|||
#include "src/storage/prism/menu_games/AbstractionDdInformation.h"
|
|||
|
|||
#include "src/storage/dd/CuddDdManager.h"
|
|||
|
|||
#include "src/utility/macros.h"
|
|||
#include "src/utility/solver.h"
|
|||
|
|||
namespace storm { |
|||
namespace prism { |
|||
namespace menu_games { |
|||
|
|||
template <storm::dd::DdType DdType, typename ValueType> |
|||
StateSetAbstractor<DdType, ValueType>::StateSetAbstractor(AbstractionExpressionInformation const& expressionInformation, AbstractionDdInformation<DdType, ValueType> const& ddInformation, storm::utility::solver::SmtSolverFactory const& smtSolverFactory) : smtSolver(smtSolverFactory.create(expressionInformation.manager)), expressionInformation(expressionInformation), ddInformation(ddInformation), variablePartition(expressionInformation.variables), relevantPredicatesAndVariables(), concretePredicateVariables(), cachedBdd(ddInformation.manager->getBddZero()) { |
|||
|
|||
// Assert all range expressions to enforce legal variable values.
|
|||
for (auto const& rangeExpression : expressionInformation.rangeExpressions) { |
|||
smtSolver->add(rangeExpression); |
|||
} |
|||
|
|||
// Refine the command based on all initial predicates.
|
|||
std::vector<uint_fast64_t> allPredicateIndices(expressionInformation.predicates.size()); |
|||
for (auto index = 0; index < expressionInformation.predicates.size(); ++index) { |
|||
allPredicateIndices[index] = index; |
|||
} |
|||
this->refine(allPredicateIndices); |
|||
} |
|||
|
|||
template <storm::dd::DdType DdType, typename ValueType> |
|||
void StateSetAbstractor<DdType, ValueType>::addPredicate(storm::expressions::Expression const& predicate) { |
|||
smtSolver->add(predicate); |
|||
|
|||
// Extract the variables of the predicate, so we know which variables were used when abstracting.
|
|||
std::set<storm::expressions::Variable> usedVariables = predicate.getVariables(); |
|||
concretePredicateVariables.insert(usedVariables.begin(), usedVariables.end()); |
|||
variablePartition.relate(usedVariables); |
|||
|
|||
// Since the new predicate might have changed the abstractions, we need to recompute it.
|
|||
this->refine(); |
|||
} |
|||
|
|||
template <storm::dd::DdType DdType, typename ValueType> |
|||
void StateSetAbstractor<DdType, ValueType>::addMissingPredicates(std::set<uint_fast64_t> const& newRelevantPredicateIndices) { |
|||
std::vector<std::pair<storm::expressions::Variable, uint_fast64_t>> newPredicateVariables = AbstractionDdInformation<DdType, ValueType>::declareNewVariables(expressionInformation.manager, relevantPredicatesAndVariables, newRelevantPredicateIndices); |
|||
|
|||
for (auto const& element : newPredicateVariables) { |
|||
smtSolver->add(storm::expressions::iff(element.first, expressionInformation.predicates[element.second])); |
|||
decisionVariables.push_back(element.first); |
|||
} |
|||
|
|||
relevantPredicatesAndVariables.insert(relevantPredicatesAndVariables.end(), newPredicateVariables.begin(), newPredicateVariables.end()); |
|||
std::sort(relevantPredicatesAndVariables.begin(), relevantPredicatesAndVariables.end(), [] (std::pair<storm::expressions::Variable, uint_fast64_t> const& firstPair, std::pair<storm::expressions::Variable, uint_fast64_t> const& secondPair) { return firstPair.second < secondPair.second; } ); |
|||
} |
|||
|
|||
template <storm::dd::DdType DdType, typename ValueType> |
|||
void StateSetAbstractor<DdType, ValueType>::refine(std::vector<uint_fast64_t> const& newPredicates) { |
|||
// Make the partition aware of the new predicates, which may make more predicates relevant to the abstraction.
|
|||
for (auto const& predicateIndex : newPredicates) { |
|||
variablePartition.addExpression(expressionInformation.predicates[predicateIndex]); |
|||
} |
|||
|
|||
// Now check whether we need to recompute the cached BDD.
|
|||
std::set<uint_fast64_t> newRelevantPredicateIndices = variablePartition.getRelatedExpressions(concretePredicateVariables); |
|||
STORM_LOG_TRACE("Found " << newRelevantPredicateIndices.size() << " relevant predicates in abstractor."); |
|||
|
|||
// Since the number of relevant predicates is monotonic, we can simply check for the size here.
|
|||
STORM_LOG_ASSERT(newRelevantPredicateIndices.size() >= relevantPredicatesAndVariables.size(), "Illegal size of relevant predicates."); |
|||
bool recomputeDd = newRelevantPredicateIndices.size() > relevantPredicatesAndVariables.size(); |
|||
|
|||
if (recomputeDd) { |
|||
// If we need to recompute the BDD, we start by introducing decision variables and the corresponding
|
|||
// constraints in the SMT problem.
|
|||
addMissingPredicates(newRelevantPredicateIndices); |
|||
|
|||
// Finally recompute the cached BDD.
|
|||
this->recomputeCachedBdd(); |
|||
} |
|||
} |
|||
|
|||
template <storm::dd::DdType DdType, typename ValueType> |
|||
storm::dd::Bdd<DdType> StateSetAbstractor<DdType, ValueType>::getStateBdd(storm::solver::SmtSolver::ModelReference const& model) const { |
|||
STORM_LOG_TRACE("Building source state BDD."); |
|||
storm::dd::Bdd<DdType> result = ddInformation.manager->getBddOne(); |
|||
for (auto const& variableIndexPair : relevantPredicatesAndVariables) { |
|||
if (model.getBooleanValue(variableIndexPair.first)) { |
|||
result &= ddInformation.predicateBdds[variableIndexPair.second].first; |
|||
} else { |
|||
result &= !ddInformation.predicateBdds[variableIndexPair.second].first; |
|||
} |
|||
} |
|||
return result; |
|||
} |
|||
|
|||
template <storm::dd::DdType DdType, typename ValueType> |
|||
void StateSetAbstractor<DdType, ValueType>::recomputeCachedBdd() { |
|||
STORM_LOG_TRACE("Recomputing BDD for state set abstraction."); |
|||
|
|||
storm::dd::Bdd<DdType> result = ddInformation.manager->getBddZero(); |
|||
smtSolver->allSat(decisionVariables, [&result,this] (storm::solver::SmtSolver::ModelReference const& model) { result |= getStateBdd(model); return true; } ); |
|||
|
|||
cachedBdd = result; |
|||
} |
|||
|
|||
template <storm::dd::DdType DdType, typename ValueType> |
|||
storm::dd::Bdd<DdType> StateSetAbstractor<DdType, ValueType>::getAbstractStates() const { |
|||
return cachedBdd; |
|||
} |
|||
|
|||
template class StateSetAbstractor<storm::dd::DdType::CUDD, double>; |
|||
} |
|||
} |
|||
} |
|||
@ -0,0 +1,117 @@ |
|||
#ifndef STORM_STORAGE_PRISM_MENU_GAMES_STATESETABSTRACTOR_H_ |
|||
#define STORM_STORAGE_PRISM_MENU_GAMES_STATESETABSTRACTOR_H_ |
|||
|
|||
#include <memory> |
|||
#include <set> |
|||
|
|||
#include "src/storage/dd/DdType.h" |
|||
|
|||
#include "src/solver/SmtSolver.h" |
|||
|
|||
#include "src/storage/prism/menu_games/VariablePartition.h" |
|||
|
|||
namespace storm { |
|||
namespace utility { |
|||
namespace solver { |
|||
class SmtSolverFactory; |
|||
} |
|||
} |
|||
|
|||
namespace dd { |
|||
template <storm::dd::DdType DdType> |
|||
class Bdd; |
|||
|
|||
template <storm::dd::DdType DdType> |
|||
class Add; |
|||
} |
|||
|
|||
namespace prism { |
|||
namespace menu_games { |
|||
template <storm::dd::DdType DdType, typename ValueType> |
|||
class AbstractionDdInformation; |
|||
|
|||
class AbstractionExpressionInformation; |
|||
|
|||
template <storm::dd::DdType DdType, typename ValueType> |
|||
class StateSetAbstractor { |
|||
public: |
|||
/*! |
|||
* Creates a state set abstractor. |
|||
* |
|||
* @param expressionInformation The expression-related information including the manager and the predicates. |
|||
* @param ddInformation The DD-related information including the manager. |
|||
* @param smtSolverFactory A factory that can create new SMT solvers. |
|||
*/ |
|||
StateSetAbstractor(AbstractionExpressionInformation const& expressionInformation, AbstractionDdInformation<DdType, ValueType> const& ddInformation, storm::utility::solver::SmtSolverFactory const& smtSolverFactory); |
|||
|
|||
/*! |
|||
* Adds the given (concrete) predicate to the abstractor and therefore restricts the abstraction to |
|||
* abstract states that contain at least some states satisfying the predicate. |
|||
*/ |
|||
void addPredicate(storm::expressions::Expression const& predicate); |
|||
|
|||
/*! |
|||
* Refines the abstractor by making the given predicates new abstract predicates. |
|||
* |
|||
* @param newPredicateIndices The indices of the new predicates. |
|||
*/ |
|||
void refine(std::vector<uint_fast64_t> const& newPredicateIndices = std::vector<uint_fast64_t>()); |
|||
|
|||
/*! |
|||
* Retrieves the set of abstract states matching all predicates added to this abstractor. |
|||
* |
|||
* @return The set of matching abstract states in the form of a BDD |
|||
*/ |
|||
storm::dd::Bdd<DdType> getAbstractStates() const; |
|||
|
|||
private: |
|||
/*! |
|||
* Creates decision variables and the corresponding constraints for the missing predicates. |
|||
* |
|||
* @param newRelevantPredicateIndices The set of all relevant predicate indices. |
|||
*/ |
|||
void addMissingPredicates(std::set<uint_fast64_t> const& newRelevantPredicateIndices); |
|||
|
|||
/*! |
|||
* Recomputes the cached BDD. This needs to be triggered if any relevant predicates change. |
|||
*/ |
|||
void recomputeCachedBdd(); |
|||
|
|||
/*! |
|||
* Translates the given model to a state DD. |
|||
* |
|||
* @param model The model to translate. |
|||
* @return The state encoded as a DD. |
|||
*/ |
|||
storm::dd::Bdd<DdType> getStateBdd(storm::solver::SmtSolver::ModelReference const& model) const; |
|||
|
|||
// The SMT solver used for abstracting the set of states. |
|||
std::unique_ptr<storm::solver::SmtSolver> smtSolver; |
|||
|
|||
// The expression-related information. |
|||
AbstractionExpressionInformation const& expressionInformation; |
|||
|
|||
// The DD-related information. |
|||
AbstractionDdInformation<DdType, ValueType> const& ddInformation; |
|||
|
|||
// The partition of the variables. |
|||
VariablePartition variablePartition; |
|||
|
|||
// The set of relevant predicates and the corresponding decision variables. |
|||
std::vector<std::pair<storm::expressions::Variable, uint_fast64_t>> relevantPredicatesAndVariables; |
|||
|
|||
// The set of all variables appearing in the concrete predicates. |
|||
std::set<storm::expressions::Variable> concretePredicateVariables; |
|||
|
|||
// The set of all decision variables over which to perform the all-sat enumeration. |
|||
std::vector<storm::expressions::Variable> decisionVariables; |
|||
|
|||
// The cached BDD representing the abstraction. This variable is written to in refinement steps (if work |
|||
// needed to be done). |
|||
storm::dd::Bdd<DdType> cachedBdd; |
|||
}; |
|||
} |
|||
} |
|||
} |
|||
|
|||
#endif /* STORM_STORAGE_PRISM_MENU_GAMES_STATESETABSTRACTOR_H_ */ |
|||
Write
Preview
Loading…
Cancel
Save
Reference in new issue