Browse Source
Merge branch 'menu_games' of https://sselab.de/lab9/private/git/storm into sylvanRationalFunctions
Merge branch 'menu_games' of https://sselab.de/lab9/private/git/storm into sylvanRationalFunctions
# Conflicts:
# src/abstraction/AbstractionDdInformation.cpp
# src/abstraction/AbstractionDdInformation.h
# src/abstraction/AbstractionExpressionInformation.cpp
# src/abstraction/AbstractionExpressionInformation.h
# src/abstraction/AbstractionInformation.cpp
Former-commit-id: 9def06e790
tempestpy_adaptions
PBerger
9 years ago
19 changed files with 822 additions and 633 deletions
-
90src/abstraction/AbstractionDdInformation.cpp
-
111src/abstraction/AbstractionDdInformation.h
-
64src/abstraction/AbstractionExpressionInformation.cpp
-
127src/abstraction/AbstractionExpressionInformation.h
-
307src/abstraction/AbstractionInformation.cpp
-
317src/abstraction/AbstractionInformation.h
-
4src/abstraction/MenuGame.cpp
-
8src/abstraction/MenuGame.h
-
54src/abstraction/StateSetAbstractor.cpp
-
44src/abstraction/StateSetAbstractor.h
-
84src/abstraction/prism/AbstractCommand.cpp
-
37src/abstraction/prism/AbstractCommand.h
-
18src/abstraction/prism/AbstractModule.cpp
-
25src/abstraction/prism/AbstractModule.h
-
107src/abstraction/prism/AbstractProgram.cpp
-
21src/abstraction/prism/AbstractProgram.h
-
19src/storage/expressions/Expression.h
-
14src/storage/expressions/ExprtkExpressionEvaluator.cpp
-
4src/storage/expressions/ExprtkExpressionEvaluator.h
@ -1,90 +0,0 @@ |
|||
#include "src/abstraction/AbstractionDdInformation.h"
|
|||
|
|||
#include <sstream>
|
|||
|
|||
#include "src/storage/expressions/ExpressionManager.h"
|
|||
|
|||
#include "src/storage/dd/DdManager.h"
|
|||
#include "src/storage/dd/Bdd.h"
|
|||
#include "src/storage/dd/Add.h"
|
|||
|
|||
#include "src/utility/macros.h"
|
|||
|
|||
namespace storm { |
|||
namespace abstraction { |
|||
|
|||
template <storm::dd::DdType DdType, typename ValueType> |
|||
AbstractionDdInformation<DdType, ValueType>::AbstractionDdInformation(std::shared_ptr<storm::dd::DdManager<DdType>> const& manager, std::vector<storm::expressions::Expression> const& initialPredicates) : manager(manager), allPredicateIdentities(manager->getBddOne()), bddVariableIndexToPredicateMap() { |
|||
for (auto const& predicate : initialPredicates) { |
|||
this->addPredicate(predicate); |
|||
} |
|||
} |
|||
|
|||
template <storm::dd::DdType DdType, typename ValueType> |
|||
storm::dd::Bdd<DdType> AbstractionDdInformation<DdType, ValueType>::encodeDistributionIndex(uint_fast64_t numberOfVariables, uint_fast64_t distributionIndex) const { |
|||
storm::dd::Bdd<DdType> result = manager->getBddOne(); |
|||
for (uint_fast64_t bitIndex = 0; bitIndex < numberOfVariables; ++bitIndex) { |
|||
STORM_LOG_ASSERT(!(optionDdVariables[bitIndex].second.isZero() || optionDdVariables[bitIndex].second.isOne()), "Option variable is corrupted."); |
|||
if ((distributionIndex & 1) != 0) { |
|||
result &= optionDdVariables[bitIndex].second; |
|||
} else { |
|||
result &= !optionDdVariables[bitIndex].second; |
|||
} |
|||
distributionIndex >>= 1; |
|||
} |
|||
STORM_LOG_ASSERT(!result.isZero(), "Update BDD encoding must not be zero."); |
|||
return result; |
|||
} |
|||
|
|||
template <storm::dd::DdType DdType, typename ValueType> |
|||
void AbstractionDdInformation<DdType, ValueType>::addPredicate(storm::expressions::Expression const& predicate) { |
|||
std::stringstream stream; |
|||
stream << predicate; |
|||
std::pair<storm::expressions::Variable, storm::expressions::Variable> newMetaVariable = manager->addMetaVariable(stream.str()); |
|||
|
|||
predicateDdVariables.push_back(newMetaVariable); |
|||
predicateBdds.emplace_back(manager->getEncoding(newMetaVariable.first, 1), manager->getEncoding(newMetaVariable.second, 1)); |
|||
predicateIdentities.push_back(manager->getEncoding(newMetaVariable.first, 1).iff(manager->getEncoding(newMetaVariable.second, 1))); |
|||
allPredicateIdentities &= predicateIdentities.back(); |
|||
sourceVariables.insert(newMetaVariable.first); |
|||
successorVariables.insert(newMetaVariable.second); |
|||
expressionToBddMap[predicate] = predicateBdds.back().first; |
|||
bddVariableIndexToPredicateMap[predicateIdentities.back().getIndex()] = predicate; |
|||
} |
|||
|
|||
template <storm::dd::DdType DdType, typename ValueType> |
|||
storm::dd::Bdd<DdType> AbstractionDdInformation<DdType, ValueType>::getMissingOptionVariableCube(uint_fast64_t begin, uint_fast64_t end) const { |
|||
storm::dd::Bdd<DdType> result = manager->getBddOne(); |
|||
|
|||
for (uint_fast64_t index = begin; index < end; ++index) { |
|||
result &= optionDdVariables[index].second; |
|||
} |
|||
|
|||
STORM_LOG_ASSERT(!result.isZero(), "Update variable cube must not be zero."); |
|||
|
|||
return result; |
|||
} |
|||
|
|||
template <storm::dd::DdType DdType, typename ValueType> |
|||
std::vector<std::pair<storm::expressions::Variable, uint_fast64_t>> AbstractionDdInformation<DdType, ValueType>::declareNewVariables(storm::expressions::ExpressionManager& manager, std::vector<std::pair<storm::expressions::Variable, uint_fast64_t>> const& oldRelevantPredicates, std::set<uint_fast64_t> const& newRelevantPredicates) { |
|||
std::vector<std::pair<storm::expressions::Variable, uint_fast64_t>> result; |
|||
|
|||
auto oldIt = oldRelevantPredicates.begin(); |
|||
auto oldIte = oldRelevantPredicates.end(); |
|||
for (auto newIt = newRelevantPredicates.begin(), newIte = newRelevantPredicates.end(); newIt != newIte; ++newIt) { |
|||
// If the new variable does not yet exist as a source variable, we create it now.
|
|||
if (oldIt == oldIte || oldIt->second != *newIt) { |
|||
result.push_back(std::make_pair(manager.declareFreshBooleanVariable(), *newIt)); |
|||
} else { |
|||
++oldIt; |
|||
} |
|||
} |
|||
|
|||
return result; |
|||
} |
|||
|
|||
template struct AbstractionDdInformation<storm::dd::DdType::CUDD, double>; |
|||
template struct AbstractionDdInformation<storm::dd::DdType::Sylvan, double>; |
|||
|
|||
} |
|||
} |
|||
@ -1,111 +0,0 @@ |
|||
#pragma once |
|||
|
|||
#include <memory> |
|||
#include <vector> |
|||
#include <set> |
|||
#include <map> |
|||
#include <unordered_map> |
|||
#include <cstdint> |
|||
|
|||
#include "src/storage/dd/DdType.h" |
|||
#include "src/storage/expressions/Expression.h" |
|||
#include "src/storage/expressions/Variable.h" |
|||
|
|||
namespace storm { |
|||
namespace dd { |
|||
template <storm::dd::DdType DdType> |
|||
class DdManager; |
|||
|
|||
template <storm::dd::DdType DdType> |
|||
class Bdd; |
|||
} |
|||
|
|||
namespace abstraction { |
|||
|
|||
template <storm::dd::DdType DdType, typename ValueType> |
|||
struct AbstractionDdInformation { |
|||
public: |
|||
/*! |
|||
* Creates a new DdInformation that uses the given manager. |
|||
* |
|||
* @param manager The manager to use. |
|||
* @param initialPredicates The initially considered predicates. |
|||
*/ |
|||
AbstractionDdInformation(std::shared_ptr<storm::dd::DdManager<DdType>> const& manager, std::vector<storm::expressions::Expression> const& initialPredicates = std::vector<storm::expressions::Expression>()); |
|||
|
|||
/*! |
|||
* Encodes the given distribution index by using the given number of variables from the optionDdVariables |
|||
* vector. |
|||
* |
|||
* @param numberOfVariables The number of variables to use. |
|||
* @param distributionIndex The distribution index to encode. |
|||
* @return The encoded distribution index. |
|||
*/ |
|||
storm::dd::Bdd<DdType> encodeDistributionIndex(uint_fast64_t numberOfVariables, uint_fast64_t distributionIndex) const; |
|||
|
|||
/*! |
|||
* Adds the given predicate and creates all associated ressources. |
|||
* |
|||
* @param predicate The predicate to add. |
|||
*/ |
|||
void addPredicate(storm::expressions::Expression const& predicate); |
|||
|
|||
/*! |
|||
* Retrieves the cube of option variables in the range [begin, end) the given indices. |
|||
* |
|||
* @param begin The first variable of the range to return. |
|||
* @param end One past the last variable of the range to return. |
|||
* @return The cube of variables in the given range. |
|||
*/ |
|||
storm::dd::Bdd<DdType> getMissingOptionVariableCube(uint_fast64_t begin, uint_fast64_t end) const; |
|||
|
|||
/*! |
|||
* Examines the old and new relevant predicates and declares decision variables for the missing relevant |
|||
* predicates. |
|||
* |
|||
* @param manager The manager in which to declare the decision variable. |
|||
* @param oldRelevantPredicates The previously relevant predicates. |
|||
* @param newRelevantPredicates The new relevant predicates. |
|||
* @return Pairs of decision variables and their index for the missing predicates. |
|||
*/ |
|||
static std::vector<std::pair<storm::expressions::Variable, uint_fast64_t>> declareNewVariables(storm::expressions::ExpressionManager& manager, std::vector<std::pair<storm::expressions::Variable, uint_fast64_t>> const& oldRelevantPredicates, std::set<uint_fast64_t> const& newRelevantPredicates); |
|||
|
|||
// The manager responsible for the DDs. |
|||
std::shared_ptr<storm::dd::DdManager<DdType>> manager; |
|||
|
|||
// The DD variables corresponding to the predicates. |
|||
std::vector<std::pair<storm::expressions::Variable, storm::expressions::Variable>> predicateDdVariables; |
|||
|
|||
// The set of all source variables. |
|||
std::set<storm::expressions::Variable> sourceVariables; |
|||
|
|||
// The set of all source variables. |
|||
std::set<storm::expressions::Variable> successorVariables; |
|||
|
|||
// The BDDs corresponding to the predicates. |
|||
std::vector<std::pair<storm::dd::Bdd<DdType>, storm::dd::Bdd<DdType>>> predicateBdds; |
|||
|
|||
// The BDDs representing the predicate identities (i.e. source and successor variable have the same truth value). |
|||
std::vector<storm::dd::Bdd<DdType>> predicateIdentities; |
|||
|
|||
// A BDD that represents the identity of all predicate variables. |
|||
storm::dd::Bdd<DdType> allPredicateIdentities; |
|||
|
|||
// The DD variable encoding the command (i.e., the nondeterministic choices of player 1). |
|||
storm::expressions::Variable commandDdVariable; |
|||
|
|||
// The DD variable encoding the update IDs for all actions. |
|||
storm::expressions::Variable updateDdVariable; |
|||
|
|||
// The DD variables encoding the nondeterministic choices of player 2. |
|||
std::vector<std::pair<storm::expressions::Variable, storm::dd::Bdd<DdType>>> optionDdVariables; |
|||
|
|||
// A mapping from the predicates to the BDDs. |
|||
std::map<storm::expressions::Expression, storm::dd::Bdd<DdType>> expressionToBddMap; |
|||
|
|||
// A mapping from the indices of the BDD variables to the predicates. |
|||
std::unordered_map<uint_fast64_t, storm::expressions::Expression> bddVariableIndexToPredicateMap; |
|||
}; |
|||
|
|||
} |
|||
} |
|||
@ -1,64 +0,0 @@ |
|||
#include "src/abstraction/AbstractionExpressionInformation.h"
|
|||
|
|||
#include "src/storage/expressions/ExpressionManager.h"
|
|||
#include "src/storage/expressions/Expression.h"
|
|||
|
|||
namespace storm { |
|||
namespace abstraction { |
|||
|
|||
AbstractionExpressionInformation::AbstractionExpressionInformation(storm::expressions::ExpressionManager& manager, std::vector<storm::expressions::Expression> const& predicates, std::set<storm::expressions::Variable> const& variables, std::vector<storm::expressions::Expression> const& rangeExpressions) : manager(manager), predicates(predicates), variables(variables), rangeExpressions(rangeExpressions) { |
|||
// Intentionally left empty.
|
|||
} |
|||
|
|||
void AbstractionExpressionInformation::addPredicate(storm::expressions::Expression const& predicate) { |
|||
predicates.push_back(predicate); |
|||
} |
|||
|
|||
void AbstractionExpressionInformation::addPredicates(std::vector<storm::expressions::Expression> const& predicates) { |
|||
for (auto const& predicate : predicates) { |
|||
this->addPredicate(predicate); |
|||
} |
|||
} |
|||
|
|||
storm::expressions::ExpressionManager& AbstractionExpressionInformation::getManager() { |
|||
return manager; |
|||
} |
|||
|
|||
storm::expressions::ExpressionManager const& AbstractionExpressionInformation::getManager() const { |
|||
return manager; |
|||
} |
|||
|
|||
std::vector<storm::expressions::Expression>& AbstractionExpressionInformation::getPredicates() { |
|||
return predicates; |
|||
} |
|||
|
|||
std::vector<storm::expressions::Expression> const& AbstractionExpressionInformation::getPredicates() const { |
|||
return predicates; |
|||
} |
|||
|
|||
storm::expressions::Expression const& AbstractionExpressionInformation::getPredicateByIndex(uint_fast64_t index) const { |
|||
return predicates[index]; |
|||
} |
|||
|
|||
std::size_t AbstractionExpressionInformation::getNumberOfPredicates() const { |
|||
return predicates.size(); |
|||
} |
|||
|
|||
std::set<storm::expressions::Variable>& AbstractionExpressionInformation::getVariables() { |
|||
return variables; |
|||
} |
|||
|
|||
std::set<storm::expressions::Variable> const& AbstractionExpressionInformation::getVariables() const { |
|||
return variables; |
|||
} |
|||
|
|||
std::vector<storm::expressions::Expression>& AbstractionExpressionInformation::getRangeExpressions() { |
|||
return rangeExpressions; |
|||
} |
|||
|
|||
std::vector<storm::expressions::Expression> const& AbstractionExpressionInformation::getRangeExpressions() const { |
|||
return rangeExpressions; |
|||
} |
|||
|
|||
} |
|||
} |
|||
@ -1,127 +0,0 @@ |
|||
#pragma once |
|||
|
|||
#include <vector> |
|||
#include <set> |
|||
#include <cstdint> |
|||
|
|||
namespace storm { |
|||
namespace expressions { |
|||
class ExpressionManager; |
|||
class Expression; |
|||
class Variable; |
|||
} |
|||
|
|||
namespace abstraction { |
|||
|
|||
struct AbstractionExpressionInformation { |
|||
public: |
|||
/*! |
|||
* Creates an expression information object with the given expression manager. |
|||
* |
|||
* @param manager The expression manager to use. |
|||
* @param predicates The initial set of predicates. |
|||
* @param variables The variables. |
|||
* @param rangeExpressions A set of expressions that enforce the variable bounds. |
|||
*/ |
|||
AbstractionExpressionInformation(storm::expressions::ExpressionManager& manager, std::vector<storm::expressions::Expression> const& predicates = std::vector<storm::expressions::Expression>(), std::set<storm::expressions::Variable> const& variables = std::set<storm::expressions::Variable>(), std::vector<storm::expressions::Expression> const& rangeExpressions = std::vector<storm::expressions::Expression>()); |
|||
|
|||
/*! |
|||
* Adds the given predicate. |
|||
* |
|||
* @param predicate The predicate to add. |
|||
*/ |
|||
void addPredicate(storm::expressions::Expression const& predicate); |
|||
|
|||
/*! |
|||
* Adds the given predicates. |
|||
* |
|||
* @param predicates The predicates to add. |
|||
*/ |
|||
void addPredicates(std::vector<storm::expressions::Expression> const& predicates); |
|||
|
|||
/*! |
|||
* Retrieves the expression manager. |
|||
* |
|||
* @return The manager. |
|||
*/ |
|||
storm::expressions::ExpressionManager& getManager(); |
|||
|
|||
/*! |
|||
* Retrieves the expression manager. |
|||
* |
|||
* @return The manager. |
|||
*/ |
|||
storm::expressions::ExpressionManager const& getManager() const; |
|||
|
|||
/*! |
|||
* Retrieves all currently known predicates. |
|||
* |
|||
* @return The list of known predicates. |
|||
*/ |
|||
std::vector<storm::expressions::Expression>& getPredicates(); |
|||
|
|||
/*! |
|||
* Retrieves all currently known predicates. |
|||
* |
|||
* @return The list of known predicates. |
|||
*/ |
|||
std::vector<storm::expressions::Expression> const& getPredicates() const; |
|||
|
|||
/*! |
|||
* Retrieves the predicate with the given index. |
|||
* |
|||
* @param index The index of the predicate. |
|||
*/ |
|||
storm::expressions::Expression const& getPredicateByIndex(uint_fast64_t index) const; |
|||
|
|||
/*! |
|||
* Retrieves the number of predicates. |
|||
* |
|||
* @return The number of predicates. |
|||
*/ |
|||
std::size_t getNumberOfPredicates() const; |
|||
|
|||
/*! |
|||
* Retrieves all currently known variables. |
|||
* |
|||
* @return The set of known variables. |
|||
*/ |
|||
std::set<storm::expressions::Variable>& getVariables(); |
|||
|
|||
/*! |
|||
* Retrieves all currently known variables. |
|||
* |
|||
* @return The set of known variables. |
|||
*/ |
|||
std::set<storm::expressions::Variable> const& getVariables() const; |
|||
|
|||
/*! |
|||
* Retrieves a list of expressions that ensure the ranges of the variables. |
|||
* |
|||
* @return The range expressions. |
|||
*/ |
|||
std::vector<storm::expressions::Expression>& getRangeExpressions(); |
|||
|
|||
/*! |
|||
* Retrieves a list of expressions that ensure the ranges of the variables. |
|||
* |
|||
* @return The range expressions. |
|||
*/ |
|||
std::vector<storm::expressions::Expression> const& getRangeExpressions() const; |
|||
|
|||
private: |
|||
// The manager responsible for the expressions of the program and the SMT solvers. |
|||
storm::expressions::ExpressionManager& manager; |
|||
|
|||
// The current set of predicates used in the abstraction. |
|||
std::vector<storm::expressions::Expression> predicates; |
|||
|
|||
// The set of all variables. |
|||
std::set<storm::expressions::Variable> variables; |
|||
|
|||
// The expression characterizing the legal ranges of all variables. |
|||
std::vector<storm::expressions::Expression> rangeExpressions; |
|||
}; |
|||
|
|||
} |
|||
} |
|||
@ -1,80 +1,321 @@ |
|||
#include "src/abstraction/AbstractionInformation.h"
|
|||
|
|||
#include "src/storage/dd/DdManager.h"
|
|||
|
|||
#include "src/utility/macros.h"
|
|||
#include "src/exceptions/InvalidOperationException.h"
|
|||
|
|||
#include "src/storage/expressions/Expression.h"
|
|||
#include "src/storage/expressions/ExpressionManager.h"
|
|||
|
|||
namespace storm { |
|||
namespace abstraction { |
|||
|
|||
template<storm::dd::DdType DdType, typename ValueType> |
|||
AbstractionInformation<DdType, ValueType>::AbstractionInformation(storm::expressions::ExpressionManager& expressionManager) : expressionManager(expressionManager) { |
|||
template<storm::dd::DdType DdType> |
|||
AbstractionInformation<DdType>::AbstractionInformation(storm::expressions::ExpressionManager& expressionManager, std::shared_ptr<storm::dd::DdManager<DdType>> ddManager) : expressionManager(expressionManager), ddManager(ddManager), allPredicateIdentities(ddManager->getBddOne()) { |
|||
// Intentionally left empty.
|
|||
} |
|||
|
|||
template<storm::dd::DdType DdType, typename ValueType> |
|||
void AbstractionInformation<DdType, ValueType>::addVariable(storm::expressions::Variable const& variable) { |
|||
template<storm::dd::DdType DdType> |
|||
void AbstractionInformation<DdType>::addExpressionVariable(storm::expressions::Variable const& variable) { |
|||
variables.insert(variable); |
|||
} |
|||
|
|||
template<storm::dd::DdType DdType, typename ValueType> |
|||
void AbstractionInformation<DdType, ValueType>::addVariable(storm::expressions::Variable const& variable, storm::expressions::Expression const& constraint) { |
|||
addVariable(variable); |
|||
template<storm::dd::DdType DdType> |
|||
void AbstractionInformation<DdType>::addExpressionVariable(storm::expressions::Variable const& variable, storm::expressions::Expression const& constraint) { |
|||
addExpressionVariable(variable); |
|||
addConstraint(constraint); |
|||
} |
|||
|
|||
template<storm::dd::DdType DdType, typename ValueType> |
|||
void AbstractionInformation<DdType, ValueType>::addConstraint(storm::expressions::Expression const& constraint) { |
|||
template<storm::dd::DdType DdType> |
|||
std::set<storm::expressions::Variable> AbstractionInformation<DdType>::getExpressionVariables() const { |
|||
return variables; |
|||
} |
|||
|
|||
template<storm::dd::DdType DdType> |
|||
void AbstractionInformation<DdType>::addConstraint(storm::expressions::Expression const& constraint) { |
|||
constraints.push_back(constraint); |
|||
} |
|||
|
|||
template<storm::dd::DdType DdType, typename ValueType> |
|||
void AbstractionInformation<DdType, ValueType>::addPredicate(storm::expressions::Expression const& predicate) { |
|||
template<storm::dd::DdType DdType> |
|||
uint_fast64_t AbstractionInformation<DdType>::addPredicate(storm::expressions::Expression const& predicate) { |
|||
std::size_t predicateIndex = predicates.size(); |
|||
predicateToIndexMap[predicate] = predicateIndex; |
|||
|
|||
// Add the new predicate to the list of known predicates.
|
|||
predicates.push_back(predicate); |
|||
|
|||
// Add DD variables for the new predicate.
|
|||
std::stringstream stream; |
|||
stream << predicate; |
|||
std::pair<storm::expressions::Variable, storm::expressions::Variable> newMetaVariable = ddManager->addMetaVariable(stream.str()); |
|||
|
|||
predicateDdVariables.push_back(newMetaVariable); |
|||
predicateBdds.emplace_back(ddManager->getEncoding(newMetaVariable.first, 1), ddManager->getEncoding(newMetaVariable.second, 1)); |
|||
predicateIdentities.push_back(ddManager->getEncoding(newMetaVariable.first, 1).iff(ddManager->getEncoding(newMetaVariable.second, 1))); |
|||
allPredicateIdentities &= predicateIdentities.back(); |
|||
sourceVariables.insert(newMetaVariable.first); |
|||
successorVariables.insert(newMetaVariable.second); |
|||
ddVariableIndexToPredicateIndexMap[predicateIdentities.back().getIndex()] = predicateIndex; |
|||
return predicateIndex; |
|||
} |
|||
|
|||
template<storm::dd::DdType DdType, typename ValueType> |
|||
void AbstractionInformation<DdType, ValueType>::addPredicates(std::vector<storm::expressions::Expression> const& predicates) { |
|||
template<storm::dd::DdType DdType> |
|||
std::vector<uint_fast64_t> AbstractionInformation<DdType>::addPredicates(std::vector<storm::expressions::Expression> const& predicates) { |
|||
std::vector<uint_fast64_t> predicateIndices; |
|||
for (auto const& predicate : predicates) { |
|||
this->addPredicate(predicate); |
|||
predicateIndices.push_back(this->addPredicate(predicate)); |
|||
} |
|||
return predicateIndices; |
|||
} |
|||
|
|||
template<storm::dd::DdType DdType> |
|||
std::vector<storm::expressions::Expression> const& AbstractionInformation<DdType>::getConstraints() const { |
|||
return constraints; |
|||
} |
|||
|
|||
template<storm::dd::DdType DdType> |
|||
storm::expressions::ExpressionManager& AbstractionInformation<DdType>::getExpressionManager() { |
|||
return expressionManager.get(); |
|||
} |
|||
|
|||
template<storm::dd::DdType DdType, typename ValueType> |
|||
storm::expressions::ExpressionManager& AbstractionInformation<DdType, ValueType>::getExpressionManager() { |
|||
return expressionManager; |
|||
template<storm::dd::DdType DdType> |
|||
storm::expressions::ExpressionManager const& AbstractionInformation<DdType>::getExpressionManager() const { |
|||
return expressionManager.get(); |
|||
} |
|||
|
|||
template<storm::dd::DdType DdType, typename ValueType> |
|||
storm::expressions::ExpressionManager const& AbstractionInformation<DdType, ValueType>::getExpressionManager() const { |
|||
return expressionManager; |
|||
template<storm::dd::DdType DdType> |
|||
storm::dd::DdManager<DdType>& AbstractionInformation<DdType>::getDdManager() { |
|||
return *ddManager; |
|||
} |
|||
|
|||
template<storm::dd::DdType DdType, typename ValueType> |
|||
std::vector<storm::expressions::Expression> const& AbstractionInformation<DdType, ValueType>::getPredicates() const { |
|||
template<storm::dd::DdType DdType> |
|||
storm::dd::DdManager<DdType> const& AbstractionInformation<DdType>::getDdManager() const { |
|||
return *ddManager; |
|||
} |
|||
|
|||
template<storm::dd::DdType DdType> |
|||
std::shared_ptr<storm::dd::DdManager<DdType>> AbstractionInformation<DdType>::getDdManagerAsSharedPointer() { |
|||
return ddManager; |
|||
} |
|||
|
|||
template<storm::dd::DdType DdType> |
|||
std::shared_ptr<storm::dd::DdManager<DdType> const> AbstractionInformation<DdType>::getDdManagerAsSharedPointer() const { |
|||
return ddManager; |
|||
} |
|||
|
|||
template<storm::dd::DdType DdType> |
|||
std::vector<storm::expressions::Expression> const& AbstractionInformation<DdType>::getPredicates() const { |
|||
return predicates; |
|||
} |
|||
|
|||
template<storm::dd::DdType DdType, typename ValueType> |
|||
storm::expressions::Expression const& AbstractionInformation<DdType, ValueType>::getPredicateByIndex(uint_fast64_t index) const { |
|||
template<storm::dd::DdType DdType> |
|||
storm::expressions::Expression const& AbstractionInformation<DdType>::getPredicateByIndex(uint_fast64_t index) const { |
|||
return predicates[index]; |
|||
} |
|||
|
|||
template<storm::dd::DdType DdType, typename ValueType> |
|||
std::size_t AbstractionInformation<DdType, ValueType>::getNumberOfPredicates() const { |
|||
template<storm::dd::DdType DdType> |
|||
storm::dd::Bdd<DdType> AbstractionInformation<DdType>::getPredicateSourceVariable(storm::expressions::Expression const& predicate) const { |
|||
auto indexIt = predicateToIndexMap.find(predicate); |
|||
STORM_LOG_THROW(indexIt != predicateToIndexMap.end(), storm::exceptions::InvalidOperationException, "Cannot retrieve BDD for unknown predicate."); |
|||
return predicateBdds[indexIt->second].first; |
|||
} |
|||
|
|||
template<storm::dd::DdType DdType> |
|||
std::size_t AbstractionInformation<DdType>::getNumberOfPredicates() const { |
|||
return predicates.size(); |
|||
} |
|||
|
|||
template<storm::dd::DdType DdType, typename ValueType> |
|||
std::set<storm::expressions::Variable> const& AbstractionInformation<DdType, ValueType>::getVariables() const { |
|||
template<storm::dd::DdType DdType> |
|||
std::set<storm::expressions::Variable> const& AbstractionInformation<DdType>::getVariables() const { |
|||
return variables; |
|||
} |
|||
|
|||
template<storm::dd::DdType DdType, typename ValueType> |
|||
std::vector<storm::expressions::Expression> const& AbstractionInformation<DdType, ValueType>::getConstraints() const { |
|||
return constraints; |
|||
template<storm::dd::DdType DdType> |
|||
void AbstractionInformation<DdType>::createEncodingVariables(uint64_t player1VariableCount, uint64_t player2VariableCount, uint64_t probabilisticBranchingVariableCount) { |
|||
STORM_LOG_THROW(player1Variables.empty() && player2Variables.empty() && probabilisticBranchingVariables.empty(), storm::exceptions::InvalidOperationException, "Variables have already been created."); |
|||
|
|||
for (uint64_t index = 0; index < player1VariableCount; ++index) { |
|||
storm::expressions::Variable newVariable = ddManager->addMetaVariable("pl1_" + std::to_string(index)).first; |
|||
player1Variables.push_back(newVariable); |
|||
player1VariableBdds.push_back(ddManager->getEncoding(newVariable, 1)); |
|||
} |
|||
STORM_LOG_DEBUG("Created " << player1VariableCount << " player 1 variables."); |
|||
|
|||
for (uint64_t index = 0; index < player2VariableCount; ++index) { |
|||
storm::expressions::Variable newVariable = ddManager->addMetaVariable("pl2_" + std::to_string(index)).first; |
|||
player2Variables.push_back(newVariable); |
|||
player2VariableBdds.push_back(ddManager->getEncoding(newVariable, 1)); |
|||
} |
|||
STORM_LOG_DEBUG("Created " << player2VariableCount << " player 2 variables."); |
|||
|
|||
for (uint64_t index = 0; index < probabilisticBranchingVariableCount; ++index) { |
|||
storm::expressions::Variable newVariable = ddManager->addMetaVariable("pb_" + std::to_string(index)).first; |
|||
probabilisticBranchingVariables.push_back(newVariable); |
|||
probabilisticBranchingVariableBdds.push_back(ddManager->getEncoding(newVariable, 1)); |
|||
} |
|||
STORM_LOG_DEBUG("Created " << probabilisticBranchingVariableCount << " probabilistic branching variables."); |
|||
} |
|||
|
|||
template<storm::dd::DdType DdType> |
|||
storm::dd::Bdd<DdType> AbstractionInformation<DdType>::encodePlayer1Choice(uint_fast64_t index, uint_fast64_t numberOfVariables) const { |
|||
return encodeChoice(index, numberOfVariables, player1VariableBdds); |
|||
} |
|||
|
|||
template<storm::dd::DdType DdType> |
|||
storm::dd::Bdd<DdType> AbstractionInformation<DdType>::encodePlayer2Choice(uint_fast64_t index, uint_fast64_t numberOfVariables) const { |
|||
return encodeChoice(index, numberOfVariables, player2VariableBdds); |
|||
} |
|||
|
|||
template<storm::dd::DdType DdType> |
|||
storm::dd::Bdd<DdType> AbstractionInformation<DdType>::encodeProbabilisticChoice(uint_fast64_t index, uint_fast64_t numberOfVariables) const { |
|||
return encodeChoice(index, numberOfVariables, probabilisticBranchingVariableBdds); |
|||
} |
|||
|
|||
template<storm::dd::DdType DdType> |
|||
storm::dd::Bdd<DdType> AbstractionInformation<DdType>::getPlayer2ZeroCube(uint_fast64_t numberOfVariables, uint_fast64_t offset) const { |
|||
storm::dd::Bdd<DdType> result = ddManager->getBddOne(); |
|||
for (uint_fast64_t index = offset; index < numberOfVariables; ++index) { |
|||
result &= player2VariableBdds[index]; |
|||
} |
|||
STORM_LOG_ASSERT(!result.isZero(), "Zero cube must not be zero."); |
|||
return result; |
|||
} |
|||
|
|||
template<storm::dd::DdType DdType> |
|||
std::vector<storm::expressions::Variable> const& AbstractionInformation<DdType>::getPlayer1Variables() const { |
|||
return player1Variables; |
|||
} |
|||
|
|||
template<storm::dd::DdType DdType> |
|||
std::set<storm::expressions::Variable> AbstractionInformation<DdType>::getPlayer1VariableSet(uint_fast64_t count) const { |
|||
return std::set<storm::expressions::Variable>(player1Variables.begin(), player1Variables.begin() + count); |
|||
} |
|||
|
|||
template<storm::dd::DdType DdType> |
|||
std::vector<storm::expressions::Variable> const& AbstractionInformation<DdType>::getPlayer2Variables() const { |
|||
return player2Variables; |
|||
} |
|||
|
|||
template<storm::dd::DdType DdType> |
|||
std::set<storm::expressions::Variable> AbstractionInformation<DdType>::getPlayer2VariableSet(uint_fast64_t count) const { |
|||
return std::set<storm::expressions::Variable>(player2Variables.begin(), player2Variables.begin() + count); |
|||
} |
|||
|
|||
template<storm::dd::DdType DdType> |
|||
std::vector<storm::expressions::Variable> const& AbstractionInformation<DdType>::getProbabilisticBranchingVariables() const { |
|||
return probabilisticBranchingVariables; |
|||
} |
|||
|
|||
template<storm::dd::DdType DdType> |
|||
std::set<storm::expressions::Variable> AbstractionInformation<DdType>::getProbabilisticBranchingVariableSet(uint_fast64_t count) const { |
|||
return std::set<storm::expressions::Variable>(probabilisticBranchingVariables.begin(), probabilisticBranchingVariables.begin() + count); |
|||
} |
|||
|
|||
template<storm::dd::DdType DdType> |
|||
std::set<storm::expressions::Variable> const& AbstractionInformation<DdType>::getSourceVariables() const { |
|||
return sourceVariables; |
|||
} |
|||
|
|||
template<storm::dd::DdType DdType> |
|||
std::set<storm::expressions::Variable> const& AbstractionInformation<DdType>::getSuccessorVariables() const { |
|||
return successorVariables; |
|||
} |
|||
|
|||
template<storm::dd::DdType DdType> |
|||
storm::dd::Bdd<DdType> const& AbstractionInformation<DdType>::getAllPredicateIdentities() const { |
|||
return allPredicateIdentities; |
|||
} |
|||
|
|||
template<storm::dd::DdType DdType> |
|||
std::size_t AbstractionInformation<DdType>::getPlayer1VariableCount() const { |
|||
return player1Variables.size(); |
|||
} |
|||
|
|||
template<storm::dd::DdType DdType> |
|||
std::size_t AbstractionInformation<DdType>::getPlayer2VariableCount() const { |
|||
return player2Variables.size(); |
|||
} |
|||
|
|||
template<storm::dd::DdType DdType> |
|||
std::size_t AbstractionInformation<DdType>::getProbabilisticBranchingVariableCount() const { |
|||
return probabilisticBranchingVariables.size(); |
|||
} |
|||
|
|||
template<storm::dd::DdType DdType> |
|||
std::map<storm::expressions::Expression, storm::dd::Bdd<DdType>> AbstractionInformation<DdType>::getPredicateToBddMap() const { |
|||
std::map<storm::expressions::Expression, storm::dd::Bdd<DdType>> result; |
|||
|
|||
for (uint_fast64_t index = 0; index < predicates.size(); ++index) { |
|||
result[predicates[index]] = predicateBdds[index].first; |
|||
} |
|||
|
|||
return result; |
|||
} |
|||
|
|||
template<storm::dd::DdType DdType> |
|||
std::vector<std::pair<storm::expressions::Variable, storm::expressions::Variable>> const& AbstractionInformation<DdType>::getSourceSuccessorVariablePairs() const { |
|||
return predicateDdVariables; |
|||
} |
|||
|
|||
template<storm::dd::DdType DdType> |
|||
storm::dd::Bdd<DdType> const& AbstractionInformation<DdType>::encodePredicateAsSource(uint_fast64_t predicateIndex) const { |
|||
return predicateBdds[predicateIndex].first; |
|||
} |
|||
|
|||
template<storm::dd::DdType DdType> |
|||
storm::dd::Bdd<DdType> const& AbstractionInformation<DdType>::encodePredicateAsSuccessor(uint_fast64_t predicateIndex) const { |
|||
return predicateBdds[predicateIndex].second; |
|||
} |
|||
|
|||
template<storm::dd::DdType DdType> |
|||
storm::dd::Bdd<DdType> const& AbstractionInformation<DdType>::getPredicateIdentity(uint_fast64_t predicateIndex) const { |
|||
return predicateIdentities[predicateIndex]; |
|||
} |
|||
|
|||
template<storm::dd::DdType DdType> |
|||
storm::expressions::Expression const& AbstractionInformation<DdType>::getPredicateForDdVariableIndex(uint_fast64_t ddVariableIndex) const { |
|||
auto indexIt = ddVariableIndexToPredicateIndexMap.find(ddVariableIndex); |
|||
STORM_LOG_THROW(indexIt != ddVariableIndexToPredicateIndexMap.end(), storm::exceptions::InvalidOperationException, "Unknown DD variable index."); |
|||
return predicates[indexIt->second]; |
|||
} |
|||
|
|||
template <storm::dd::DdType DdType> |
|||
std::vector<std::pair<storm::expressions::Variable, uint_fast64_t>> AbstractionInformation<DdType>::declareNewVariables(std::vector<std::pair<storm::expressions::Variable, uint_fast64_t>> const& oldPredicates, std::set<uint_fast64_t> const& newPredicates) const { |
|||
std::vector<std::pair<storm::expressions::Variable, uint_fast64_t>> result; |
|||
|
|||
auto oldIt = oldPredicates.begin(); |
|||
auto oldIte = oldPredicates.end(); |
|||
auto newIt = newPredicates.begin(); |
|||
auto newIte = newPredicates.end(); |
|||
|
|||
for (; newIt != newIte; ++newIt) { |
|||
if (oldIt == oldIte || oldIt->second != *newIt) { |
|||
result.push_back(std::make_pair(expressionManager.get().declareFreshBooleanVariable(), *newIt)); |
|||
} else { |
|||
++oldIt; |
|||
} |
|||
} |
|||
|
|||
return result; |
|||
} |
|||
|
|||
template<storm::dd::DdType DdType> |
|||
storm::dd::Bdd<DdType> AbstractionInformation<DdType>::encodeChoice(uint_fast64_t index, uint_fast64_t numberOfVariables, std::vector<storm::dd::Bdd<DdType>> const& variables) const { |
|||
storm::dd::Bdd<DdType> result = ddManager->getBddOne(); |
|||
for (uint_fast64_t bitIndex = 0; bitIndex < numberOfVariables; ++bitIndex) { |
|||
if ((index & 1) != 0) { |
|||
result &= variables[bitIndex]; |
|||
} else { |
|||
result &= !variables[bitIndex]; |
|||
} |
|||
index >>= 1; |
|||
} |
|||
STORM_LOG_ASSERT(!result.isZero(), "BDD encoding must not be zero."); |
|||
return result; |
|||
} |
|||
|
|||
template class AbstractionInformation<storm::dd::DdType::CUDD, double>; |
|||
template class AbstractionInformation<storm::dd::DdType::Sylvan, double>; |
|||
template class AbstractionInformation<storm::dd::DdType::CUDD>; |
|||
template class AbstractionInformation<storm::dd::DdType::Sylvan>; |
|||
} |
|||
} |
|||
Write
Preview
Loading…
Cancel
Save
Reference in new issue