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

renamed variable partition to local expression information 

Former-commit-id: 59934b401f
main
dehnert 9 years ago
parent
08d0eb6001
commit
cf93d75450
8 changed files with 90 additions and 63 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. 30
      src/storage/prism/menu_games/AbstractCommand.cpp
  2. 10
      src/storage/prism/menu_games/AbstractCommand.h
  3. 8
      src/storage/prism/menu_games/AbstractionExpressionInformation.cpp
  4. 14
      src/storage/prism/menu_games/AbstractionExpressionInformation.h
  5. 39
      src/storage/prism/menu_games/LocalExpressionInformation.cpp
  6. 22
      src/storage/prism/menu_games/LocalExpressionInformation.h
  7. 20
      src/storage/prism/menu_games/StateSetAbstractor.cpp
  8. 10
      src/storage/prism/menu_games/StateSetAbstractor.h

30
src/storage/prism/menu_games/AbstractCommand.cpp
View File

@ -18,13 +18,13 @@ namespace storm {
namespace prism { namespace prism {
namespace menu_games { namespace menu_games {
template <storm::dd::DdType DdType, typename ValueType> template <storm::dd::DdType DdType, typename ValueType>
AbstractCommand<DdType, ValueType>::AbstractCommand(storm::prism::Command const& command, AbstractionExpressionInformation& expressionInformation, AbstractionDdInformation<DdType, ValueType> const& ddInformation, storm::utility::solver::SmtSolverFactory const& smtSolverFactory) : smtSolver(smtSolverFactory.create(expressionInformation.getManager())), expressionInformation(expressionInformation), ddInformation(ddInformation), command(command), variablePartition(expressionInformation.getVariables()), relevantPredicatesAndVariables(), cachedDd(std::make_pair(ddInformation.manager->getBddZero(), 0)), decisionVariables() {
AbstractCommand<DdType, ValueType>::AbstractCommand(storm::prism::Command const& command, AbstractionExpressionInformation& globalExpressionInformation, AbstractionDdInformation<DdType, ValueType> const& ddInformation, storm::utility::solver::SmtSolverFactory const& smtSolverFactory) : smtSolver(smtSolverFactory.create(globalExpressionInformation.getManager())), globalExpressionInformation(globalExpressionInformation), ddInformation(ddInformation), command(command), localExpressionInformation(globalExpressionInformation.getVariables()), relevantPredicatesAndVariables(), cachedDd(std::make_pair(ddInformation.manager->getBddZero(), 0)), decisionVariables() {
// Make the second component of relevant predicates have the right size. // Make the second component of relevant predicates have the right size.
relevantPredicatesAndVariables.second.resize(command.getNumberOfUpdates()); relevantPredicatesAndVariables.second.resize(command.getNumberOfUpdates());
// Assert all range expressions to enforce legal variable values. // Assert all range expressions to enforce legal variable values.
for (auto const& rangeExpression : expressionInformation.getRangeExpressions()) {
for (auto const& rangeExpression : globalExpressionInformation.getRangeExpressions()) {
smtSolver->add(rangeExpression); smtSolver->add(rangeExpression);
} }
@ -32,8 +32,8 @@ namespace storm {
smtSolver->add(command.getGuardExpression()); smtSolver->add(command.getGuardExpression());
// Refine the command based on all initial predicates. // Refine the command based on all initial predicates.
std::vector<uint_fast64_t> allPredicateIndices(expressionInformation.getPredicates().size());
for (auto index = 0; index < expressionInformation.getPredicates().size(); ++index) {
std::vector<uint_fast64_t> allPredicateIndices(globalExpressionInformation.getNumberOfPredicates());
for (auto index = 0; index < globalExpressionInformation.getNumberOfPredicates(); ++index) {
allPredicateIndices[index] = index; allPredicateIndices[index] = index;
} }
this->refine(allPredicateIndices); this->refine(allPredicateIndices);
@ -43,10 +43,10 @@ namespace storm {
void AbstractCommand<DdType, ValueType>::refine(std::vector<uint_fast64_t> const& predicates) { void AbstractCommand<DdType, ValueType>::refine(std::vector<uint_fast64_t> const& predicates) {
// Add all predicates to the variable partition. // Add all predicates to the variable partition.
for (auto predicateIndex : predicates) { for (auto predicateIndex : predicates) {
variablePartition.addExpression(expressionInformation.getPredicates()[predicateIndex]);
localExpressionInformation.addExpression(globalExpressionInformation.getPredicateByIndex(predicateIndex), predicateIndex);
} }
STORM_LOG_TRACE("Current variable partition is: " << variablePartition);
STORM_LOG_TRACE("Current variable partition is: " << localExpressionInformation);
// Next, we check whether there is work to be done by recomputing the relevant predicates and checking // Next, we check whether there is work to be done by recomputing the relevant predicates and checking
// whether they changed. // whether they changed.
@ -119,19 +119,19 @@ namespace storm {
std::set<storm::expressions::Variable> assignedVariables; std::set<storm::expressions::Variable> assignedVariables;
for (auto const& assignment : assignments) { for (auto const& assignment : assignments) {
// Also, variables appearing on the right-hand side of an assignment are relevant for source state. // Also, variables appearing on the right-hand side of an assignment are relevant for source state.
auto const& rightHandSidePredicates = variablePartition.getExpressionsUsingVariables(assignment.getExpression().getVariables());
auto const& rightHandSidePredicates = localExpressionInformation.getExpressionsUsingVariables(assignment.getExpression().getVariables());
result.first.insert(rightHandSidePredicates.begin(), rightHandSidePredicates.end()); result.first.insert(rightHandSidePredicates.begin(), rightHandSidePredicates.end());
// Variables that are being assigned are relevant for the successor state. // Variables that are being assigned are relevant for the successor state.
storm::expressions::Variable const& assignedVariable = assignment.getVariable(); storm::expressions::Variable const& assignedVariable = assignment.getVariable();
auto const& leftHandSidePredicates = variablePartition.getExpressionsUsingVariable(assignedVariable);
auto const& leftHandSidePredicates = localExpressionInformation.getExpressionsUsingVariable(assignedVariable);
result.second.insert(leftHandSidePredicates.begin(), leftHandSidePredicates.end()); result.second.insert(leftHandSidePredicates.begin(), leftHandSidePredicates.end());
// Keep track of all assigned variables, so we can find the related predicates later. // Keep track of all assigned variables, so we can find the related predicates later.
assignedVariables.insert(assignedVariable); assignedVariables.insert(assignedVariable);
} }
auto const& predicatesRelatedToAssignedVariable = variablePartition.getRelatedExpressions(assignedVariables);
auto const& predicatesRelatedToAssignedVariable = localExpressionInformation.getRelatedExpressions(assignedVariables);
result.first.insert(predicatesRelatedToAssignedVariable.begin(), predicatesRelatedToAssignedVariable.end()); result.first.insert(predicatesRelatedToAssignedVariable.begin(), predicatesRelatedToAssignedVariable.end());
@ -143,7 +143,7 @@ namespace storm {
std::pair<std::set<uint_fast64_t>, std::vector<std::set<uint_fast64_t>>> result; std::pair<std::set<uint_fast64_t>, std::vector<std::set<uint_fast64_t>>> result;
// To start with, all predicates related to the guard are relevant source predicates. // To start with, all predicates related to the guard are relevant source predicates.
result.first = variablePartition.getExpressionsUsingVariables(command.get().getGuardExpression().getVariables());
result.first = localExpressionInformation.getExpressionsUsingVariables(command.get().getGuardExpression().getVariables());
// Then, we add the predicates that become relevant, because of some update. // Then, we add the predicates that become relevant, because of some update.
for (auto const& update : command.get().getUpdates()) { for (auto const& update : command.get().getUpdates()) {
@ -173,9 +173,9 @@ namespace storm {
template <storm::dd::DdType DdType, typename ValueType> template <storm::dd::DdType DdType, typename ValueType>
void AbstractCommand<DdType, ValueType>::addMissingPredicates(std::pair<std::set<uint_fast64_t>, std::vector<std::set<uint_fast64_t>>> const& newRelevantPredicates) { void AbstractCommand<DdType, ValueType>::addMissingPredicates(std::pair<std::set<uint_fast64_t>, std::vector<std::set<uint_fast64_t>>> const& newRelevantPredicates) {
// Determine and add new relevant source predicates. // Determine and add new relevant source predicates.
std::vector<std::pair<storm::expressions::Variable, uint_fast64_t>> newSourceVariables = AbstractionDdInformation<DdType, ValueType>::declareNewVariables(expressionInformation.getManager(), relevantPredicatesAndVariables.first, newRelevantPredicates.first);
std::vector<std::pair<storm::expressions::Variable, uint_fast64_t>> newSourceVariables = AbstractionDdInformation<DdType, ValueType>::declareNewVariables(globalExpressionInformation.getManager(), relevantPredicatesAndVariables.first, newRelevantPredicates.first);
for (auto const& element : newSourceVariables) { for (auto const& element : newSourceVariables) {
smtSolver->add(storm::expressions::iff(element.first, expressionInformation.getPredicates()[element.second]));
smtSolver->add(storm::expressions::iff(element.first, globalExpressionInformation.getPredicateByIndex(element.second)));
decisionVariables.push_back(element.first); decisionVariables.push_back(element.first);
} }
@ -185,9 +185,9 @@ namespace storm {
// Do the same for every update. // Do the same for every update.
for (uint_fast64_t index = 0; index < command.get().getNumberOfUpdates(); ++index) { for (uint_fast64_t index = 0; index < command.get().getNumberOfUpdates(); ++index) {
std::vector<std::pair<storm::expressions::Variable, uint_fast64_t>> newSuccessorVariables = AbstractionDdInformation<DdType, ValueType>::declareNewVariables(expressionInformation.getManager(), relevantPredicatesAndVariables.second[index], newRelevantPredicates.second[index]);
std::vector<std::pair<storm::expressions::Variable, uint_fast64_t>> newSuccessorVariables = AbstractionDdInformation<DdType, ValueType>::declareNewVariables(globalExpressionInformation.getManager(), relevantPredicatesAndVariables.second[index], newRelevantPredicates.second[index]);
for (auto const& element : newSuccessorVariables) { for (auto const& element : newSuccessorVariables) {
smtSolver->add(storm::expressions::iff(element.first, expressionInformation.getPredicates()[element.second].substitute(command.get().getUpdate(index).getAsVariableToExpressionMap())));
smtSolver->add(storm::expressions::iff(element.first, globalExpressionInformation.getPredicateByIndex(element.second).substitute(command.get().getUpdate(index).getAsVariableToExpressionMap())));
decisionVariables.push_back(element.first); decisionVariables.push_back(element.first);
} }
@ -277,7 +277,7 @@ namespace storm {
auto relevantIte = relevantPredicatesAndVariables.first.end(); auto relevantIte = relevantPredicatesAndVariables.first.end();
storm::dd::Bdd<DdType> result = ddInformation.manager->getBddOne(); storm::dd::Bdd<DdType> result = ddInformation.manager->getBddOne();
for (uint_fast64_t predicateIndex = 0; predicateIndex < expressionInformation.getPredicates().size(); ++predicateIndex) {
for (uint_fast64_t predicateIndex = 0; predicateIndex < globalExpressionInformation.getNumberOfPredicates(); ++predicateIndex) {
if (relevantIt == relevantIte || relevantIt->second != predicateIndex) { if (relevantIt == relevantIte || relevantIt->second != predicateIndex) {
result &= ddInformation.predicateIdentities[predicateIndex]; result &= ddInformation.predicateIdentities[predicateIndex];
} else { } else {

10
src/storage/prism/menu_games/AbstractCommand.h
View File

@ -6,7 +6,7 @@
#include <set> #include <set>
#include <map> #include <map>
#include "src/storage/prism/menu_games/VariablePartition.h"
#include "src/storage/prism/menu_games/LocalExpressionInformation.h"
#include "src/storage/dd/DdType.h" #include "src/storage/dd/DdType.h"
#include "src/storage/expressions/Expression.h" #include "src/storage/expressions/Expression.h"
@ -155,8 +155,8 @@ namespace storm {
// An SMT responsible for this abstract command. // An SMT responsible for this abstract command.
std::unique_ptr<storm::solver::SmtSolver> smtSolver; std::unique_ptr<storm::solver::SmtSolver> smtSolver;
// The expression-related information.
AbstractionExpressionInformation& expressionInformation;
// The global expression-related information.
AbstractionExpressionInformation& globalExpressionInformation;
// The DD-related information. // The DD-related information.
AbstractionDdInformation<DdType, ValueType> const& ddInformation; AbstractionDdInformation<DdType, ValueType> const& ddInformation;
@ -164,8 +164,8 @@ namespace storm {
// The concrete command this abstract command refers to. // The concrete command this abstract command refers to.
std::reference_wrapper<Command const> command; std::reference_wrapper<Command const> command;
// The partition of variables and expressions.
VariablePartition variablePartition;
// The local expression-related information.
LocalExpressionInformation localExpressionInformation;
// The currently relevant source/successor predicates and the corresponding variables. // The currently relevant source/successor predicates and the corresponding variables.
std::pair<std::vector<std::pair<storm::expressions::Variable, uint_fast64_t>>, std::vector<std::vector<std::pair<storm::expressions::Variable, uint_fast64_t>>>> relevantPredicatesAndVariables; std::pair<std::vector<std::pair<storm::expressions::Variable, uint_fast64_t>>, std::vector<std::vector<std::pair<storm::expressions::Variable, uint_fast64_t>>>> relevantPredicatesAndVariables;

8
src/storage/prism/menu_games/AbstractionExpressionInformation.cpp
View File

@ -37,6 +37,14 @@ namespace storm {
return predicates; 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() { std::set<storm::expressions::Variable>& AbstractionExpressionInformation::getVariables() {
return variables; return variables;
} }

14
src/storage/prism/menu_games/AbstractionExpressionInformation.h
View File

@ -68,6 +68,20 @@ namespace storm {
*/ */
std::vector<storm::expressions::Expression> const& getPredicates() const; 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. * Retrieves all currently known variables.
* *

39
src/storage/prism/menu_games/VariablePartition.cpp → src/storage/prism/menu_games/LocalExpressionInformation.cpp
View File

@ -1,4 +1,4 @@
#include "src/storage/prism/menu_games/VariablePartition.h"
#include "src/storage/prism/menu_games/LocalExpressionInformation.h"
#include <boost/algorithm/string/join.hpp> #include <boost/algorithm/string/join.hpp>
@ -7,7 +7,7 @@
namespace storm { namespace storm {
namespace prism { namespace prism {
namespace menu_games { namespace menu_games {
VariablePartition::VariablePartition(std::set<storm::expressions::Variable> const& relevantVariables, std::vector<storm::expressions::Expression> const& expressions) : relevantVariables(relevantVariables), expressionBlocks(relevantVariables.size()) {
LocalExpressionInformation::LocalExpressionInformation(std::set<storm::expressions::Variable> const& relevantVariables, std::vector<std::pair<storm::expressions::Expression, uint_fast64_t>> const& expressionIndexPairs) : relevantVariables(relevantVariables), expressionBlocks(relevantVariables.size()) {
// Assign each variable to a new block. // Assign each variable to a new block.
uint_fast64_t currentBlock = 0; uint_fast64_t currentBlock = 0;
variableBlocks.resize(relevantVariables.size()); variableBlocks.resize(relevantVariables.size());
@ -19,12 +19,12 @@ namespace storm {
} }
// Add all expressions, which might relate some variables. // Add all expressions, which might relate some variables.
for (auto const& expression : expressions) {
this->addExpression(expression);
for (auto const& expressionIndexPair : expressionIndexPairs) {
this->addExpression(expressionIndexPair.first, expressionIndexPair.second);
} }
} }
bool VariablePartition::addExpression(storm::expressions::Expression const& expression) {
bool LocalExpressionInformation::addExpression(storm::expressions::Expression const& expression, uint_fast64_t globalExpressionIndex) {
// Register the expression for all variables that appear in it. // Register the expression for all variables that appear in it.
std::set<storm::expressions::Variable> expressionVariables = expression.getVariables(); std::set<storm::expressions::Variable> expressionVariables = expression.getVariables();
for (auto const& variable : expressionVariables) { for (auto const& variable : expressionVariables) {
@ -37,19 +37,20 @@ namespace storm {
expressionBlocks[getBlockIndexOfVariable(*expressionVariables.begin())].insert(this->expressions.size()); expressionBlocks[getBlockIndexOfVariable(*expressionVariables.begin())].insert(this->expressions.size());
// Add expression and relate all the appearing variables. // Add expression and relate all the appearing variables.
this->globalToLocalIndexMapping[globalExpressionIndex] = this->expressions.size();
this->expressions.push_back(expression); this->expressions.push_back(expression);
return this->relate(expressionVariables); return this->relate(expressionVariables);
} }
bool VariablePartition::areRelated(storm::expressions::Variable const& firstVariable, storm::expressions::Variable const& secondVariable) {
bool LocalExpressionInformation::areRelated(storm::expressions::Variable const& firstVariable, storm::expressions::Variable const& secondVariable) {
return getBlockIndexOfVariable(firstVariable) == getBlockIndexOfVariable(secondVariable); return getBlockIndexOfVariable(firstVariable) == getBlockIndexOfVariable(secondVariable);
} }
bool VariablePartition::relate(storm::expressions::Variable const& firstVariable, storm::expressions::Variable const& secondVariable) {
bool LocalExpressionInformation::relate(storm::expressions::Variable const& firstVariable, storm::expressions::Variable const& secondVariable) {
return this->relate({firstVariable, secondVariable}); return this->relate({firstVariable, secondVariable});
} }
bool VariablePartition::relate(std::set<storm::expressions::Variable> const& variables) {
bool LocalExpressionInformation::relate(std::set<storm::expressions::Variable> const& variables) {
// Determine all blocks that need to be merged. // Determine all blocks that need to be merged.
std::set<uint_fast64_t> blocksToMerge; std::set<uint_fast64_t> blocksToMerge;
for (auto const& variable : variables) { for (auto const& variable : variables) {
@ -67,7 +68,7 @@ namespace storm {
return true; return true;
} }
void VariablePartition::mergeBlocks(std::set<uint_fast64_t> const& blocksToMerge) {
void LocalExpressionInformation::mergeBlocks(std::set<uint_fast64_t> const& blocksToMerge) {
// Merge all blocks into the block to keep. // Merge all blocks into the block to keep.
std::vector<std::set<storm::expressions::Variable>> newVariableBlocks; std::vector<std::set<storm::expressions::Variable>> newVariableBlocks;
std::vector<std::set<uint_fast64_t>> newExpressionBlocks; std::vector<std::set<uint_fast64_t>> newExpressionBlocks;
@ -107,28 +108,28 @@ namespace storm {
expressionBlocks = std::move(newExpressionBlocks); expressionBlocks = std::move(newExpressionBlocks);
} }
std::set<storm::expressions::Variable> const& VariablePartition::getBlockOfVariable(storm::expressions::Variable const& variable) const {
std::set<storm::expressions::Variable> const& LocalExpressionInformation::getBlockOfVariable(storm::expressions::Variable const& variable) const {
return variableBlocks[getBlockIndexOfVariable(variable)]; return variableBlocks[getBlockIndexOfVariable(variable)];
} }
uint_fast64_t VariablePartition::getNumberOfBlocks() const {
uint_fast64_t LocalExpressionInformation::getNumberOfBlocks() const {
return this->variableBlocks.size(); return this->variableBlocks.size();
} }
std::set<storm::expressions::Variable> const& VariablePartition::getVariableBlockWithIndex(uint_fast64_t blockIndex) const {
std::set<storm::expressions::Variable> const& LocalExpressionInformation::getVariableBlockWithIndex(uint_fast64_t blockIndex) const {
return this->variableBlocks[blockIndex]; return this->variableBlocks[blockIndex];
} }
uint_fast64_t VariablePartition::getBlockIndexOfVariable(storm::expressions::Variable const& variable) const {
uint_fast64_t LocalExpressionInformation::getBlockIndexOfVariable(storm::expressions::Variable const& variable) const {
STORM_LOG_ASSERT(this->relevantVariables.find(variable) != this->relevantVariables.end(), "Illegal variable '" << variable.getName() << "' for partition."); STORM_LOG_ASSERT(this->relevantVariables.find(variable) != this->relevantVariables.end(), "Illegal variable '" << variable.getName() << "' for partition.");
return this->variableToBlockMapping.find(variable)->second; return this->variableToBlockMapping.find(variable)->second;
} }
std::set<uint_fast64_t> const& VariablePartition::getRelatedExpressions(storm::expressions::Variable const& variable) const {
std::set<uint_fast64_t> const& LocalExpressionInformation::getRelatedExpressions(storm::expressions::Variable const& variable) const {
return this->expressionBlocks[getBlockIndexOfVariable(variable)]; return this->expressionBlocks[getBlockIndexOfVariable(variable)];
} }
std::set<uint_fast64_t> VariablePartition::getRelatedExpressions(std::set<storm::expressions::Variable> const& variables) const {
std::set<uint_fast64_t> LocalExpressionInformation::getRelatedExpressions(std::set<storm::expressions::Variable> const& variables) const {
// Start by determining the indices of all expression blocks that are related to any of the variables. // Start by determining the indices of all expression blocks that are related to any of the variables.
std::set<uint_fast64_t> relatedExpressionBlockIndices; std::set<uint_fast64_t> relatedExpressionBlockIndices;
for (auto const& variable : variables) { for (auto const& variable : variables) {
@ -143,12 +144,12 @@ namespace storm {
return result; return result;
} }
std::set<uint_fast64_t> const& VariablePartition::getExpressionsUsingVariable(storm::expressions::Variable const& variable) const {
std::set<uint_fast64_t> const& LocalExpressionInformation::getExpressionsUsingVariable(storm::expressions::Variable const& variable) const {
STORM_LOG_ASSERT(this->relevantVariables.find(variable) != this->relevantVariables.end(), "Illegal variable '" << variable.getName() << "' for partition."); STORM_LOG_ASSERT(this->relevantVariables.find(variable) != this->relevantVariables.end(), "Illegal variable '" << variable.getName() << "' for partition.");
return this->variableToExpressionsMapping.find(variable)->second; return this->variableToExpressionsMapping.find(variable)->second;
} }
std::set<uint_fast64_t> VariablePartition::getExpressionsUsingVariables(std::set<storm::expressions::Variable> const& variables) const {
std::set<uint_fast64_t> LocalExpressionInformation::getExpressionsUsingVariables(std::set<storm::expressions::Variable> const& variables) const {
std::set<uint_fast64_t> result; std::set<uint_fast64_t> result;
for (auto const& variable : variables) { for (auto const& variable : variables) {
@ -160,11 +161,11 @@ namespace storm {
return result; return result;
} }
storm::expressions::Expression const& VariablePartition::getExpression(uint_fast64_t expressionIndex) const {
storm::expressions::Expression const& LocalExpressionInformation::getExpression(uint_fast64_t expressionIndex) const {
return this->expressions[expressionIndex]; return this->expressions[expressionIndex];
} }
std::ostream& operator<<(std::ostream& out, VariablePartition const& partition) {
std::ostream& operator<<(std::ostream& out, LocalExpressionInformation const& partition) {
std::vector<std::string> blocks; std::vector<std::string> blocks;
for (uint_fast64_t index = 0; index < partition.variableBlocks.size(); ++index) { for (uint_fast64_t index = 0; index < partition.variableBlocks.size(); ++index) {
auto const& variableBlock = partition.variableBlocks[index]; auto const& variableBlock = partition.variableBlocks[index];

22
src/storage/prism/menu_games/VariablePartition.h → src/storage/prism/menu_games/LocalExpressionInformation.h
View File

@ -1,5 +1,5 @@
#ifndef STORM_STORAGE_PRISM_MENU_GAMES_VARIABLEPARTITION_H_
#define STORM_STORAGE_PRISM_MENU_GAMES_VARIABLEPARTITION_H_
#ifndef STORM_STORAGE_PRISM_MENU_GAMES_LOCALEXPRESSIONINFORMATION_H_
#define STORM_STORAGE_PRISM_MENU_GAMES_LOCALEXPRESSIONINFORMATION_H_
#include <unordered_map> #include <unordered_map>
#include <set> #include <set>
@ -13,23 +13,24 @@ namespace storm {
namespace prism { namespace prism {
namespace menu_games { namespace menu_games {
class VariablePartition{
class LocalExpressionInformation {
public: public:
/*! /*!
* Constructs a new variable partition. * Constructs a new variable partition.
* *
* @param relevantVariables The variables of this partition. * @param relevantVariables The variables of this partition.
* @param expressions The (initial) expressions that define the partition.
* @param expressionIndexPairs The (initial) pairs of expressions and their global indices.
*/ */
VariablePartition(std::set<storm::expressions::Variable> const& relevantVariables, std::vector<storm::expressions::Expression> const& expressions = std::vector<storm::expressions::Expression>());
LocalExpressionInformation(std::set<storm::expressions::Variable> const& relevantVariables, std::vector<std::pair<storm::expressions::Expression, uint_fast64_t>> const& expressionIndexPairs = {});
/*! /*!
* Adds the expression and therefore indirectly may cause blocks of variables to be merged. * Adds the expression and therefore indirectly may cause blocks of variables to be merged.
* *
* @param expression The expression to add. * @param expression The expression to add.
* @param globalExpressionIndex The global index of the expression.
* @return True iff the partition changed. * @return True iff the partition changed.
*/ */
bool addExpression(storm::expressions::Expression const& expression);
bool addExpression(storm::expressions::Expression const& expression, uint_fast64_t globalExpressionIndex);
/*! /*!
* Retrieves whether the two given variables are in the same block of the partition. * Retrieves whether the two given variables are in the same block of the partition.
@ -128,7 +129,7 @@ namespace storm {
*/ */
storm::expressions::Expression const& getExpression(uint_fast64_t expressionIndex) const; storm::expressions::Expression const& getExpression(uint_fast64_t expressionIndex) const;
friend std::ostream& operator<<(std::ostream& out, VariablePartition const& partition);
friend std::ostream& operator<<(std::ostream& out, LocalExpressionInformation const& partition);
private: private:
/*! /*!
@ -153,14 +154,17 @@ namespace storm {
// A mapping from variables to the indices of all expressions they appear in. // A mapping from variables to the indices of all expressions they appear in.
std::unordered_map<storm::expressions::Variable, std::set<uint_fast64_t>> variableToExpressionsMapping; std::unordered_map<storm::expressions::Variable, std::set<uint_fast64_t>> variableToExpressionsMapping;
// A mapping from global expression indices to local ones.
std::unordered_map<uint_fast64_t, uint_fast64_t> globalToLocalIndexMapping;
// The vector of all expressions. // The vector of all expressions.
std::vector<storm::expressions::Expression> expressions; std::vector<storm::expressions::Expression> expressions;
}; };
std::ostream& operator<<(std::ostream& out, VariablePartition const& partition);
std::ostream& operator<<(std::ostream& out, LocalExpressionInformation const& partition);
} }
} }
} }
#endif /* STORM_STORAGE_PRISM_MENU_GAMES_VARIABLEPARTITION_H_ */
#endif /* STORM_STORAGE_PRISM_MENU_GAMES_LOCALEXPRESSIONINFORMATION_H_ */

20
src/storage/prism/menu_games/StateSetAbstractor.cpp
View File

@ -13,10 +13,10 @@ namespace storm {
namespace menu_games { namespace menu_games {
template <storm::dd::DdType DdType, typename ValueType> template <storm::dd::DdType DdType, typename ValueType>
StateSetAbstractor<DdType, ValueType>::StateSetAbstractor(AbstractionExpressionInformation& expressionInformation, AbstractionDdInformation<DdType, ValueType> const& ddInformation, std::vector<storm::expressions::Expression> const& statePredicates, storm::utility::solver::SmtSolverFactory const& smtSolverFactory) : smtSolver(smtSolverFactory.create(expressionInformation.getManager())), expressionInformation(expressionInformation), ddInformation(ddInformation), variablePartition(expressionInformation.getVariables()), relevantPredicatesAndVariables(), concretePredicateVariables(), needsRecomputation(false), cachedBdd(ddInformation.manager->getBddZero()), constraint(ddInformation.manager->getBddOne()) {
StateSetAbstractor<DdType, ValueType>::StateSetAbstractor(AbstractionExpressionInformation& globalExpressionInformation, AbstractionDdInformation<DdType, ValueType> const& ddInformation, std::vector<storm::expressions::Expression> const& statePredicates, storm::utility::solver::SmtSolverFactory const& smtSolverFactory) : smtSolver(smtSolverFactory.create(globalExpressionInformation.getManager())), globalExpressionInformation(globalExpressionInformation), ddInformation(ddInformation), localExpressionInformation(globalExpressionInformation.getVariables()), relevantPredicatesAndVariables(), concretePredicateVariables(), needsRecomputation(false), cachedBdd(ddInformation.manager->getBddZero()), constraint(ddInformation.manager->getBddOne()) {
// Assert all range expressions to enforce legal variable values. // Assert all range expressions to enforce legal variable values.
for (auto const& rangeExpression : expressionInformation.getRangeExpressions()) {
for (auto const& rangeExpression : globalExpressionInformation.getRangeExpressions()) {
smtSolver->add(rangeExpression); smtSolver->add(rangeExpression);
} }
@ -27,12 +27,12 @@ namespace storm {
// Extract the variables of the predicate, so we know which variables were used when abstracting. // Extract the variables of the predicate, so we know which variables were used when abstracting.
std::set<storm::expressions::Variable> usedVariables = predicate.getVariables(); std::set<storm::expressions::Variable> usedVariables = predicate.getVariables();
concretePredicateVariables.insert(usedVariables.begin(), usedVariables.end()); concretePredicateVariables.insert(usedVariables.begin(), usedVariables.end());
variablePartition.relate(usedVariables);
localExpressionInformation.relate(usedVariables);
} }
// Refine the command based on all initial predicates. // Refine the command based on all initial predicates.
std::vector<uint_fast64_t> allPredicateIndices(expressionInformation.getPredicates().size());
for (auto index = 0; index < expressionInformation.getPredicates().size(); ++index) {
std::vector<uint_fast64_t> allPredicateIndices(globalExpressionInformation.getPredicates().size());
for (auto index = 0; index < globalExpressionInformation.getPredicates().size(); ++index) {
allPredicateIndices[index] = index; allPredicateIndices[index] = index;
} }
this->refine(allPredicateIndices); this->refine(allPredicateIndices);
@ -40,10 +40,10 @@ namespace storm {
template <storm::dd::DdType DdType, typename ValueType> template <storm::dd::DdType DdType, typename ValueType>
void StateSetAbstractor<DdType, ValueType>::addMissingPredicates(std::set<uint_fast64_t> const& newRelevantPredicateIndices) { 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.getManager(), relevantPredicatesAndVariables, newRelevantPredicateIndices);
std::vector<std::pair<storm::expressions::Variable, uint_fast64_t>> newPredicateVariables = AbstractionDdInformation<DdType, ValueType>::declareNewVariables(globalExpressionInformation.getManager(), relevantPredicatesAndVariables, newRelevantPredicateIndices);
for (auto const& element : newPredicateVariables) { for (auto const& element : newPredicateVariables) {
smtSolver->add(storm::expressions::iff(element.first, expressionInformation.getPredicates()[element.second]));
smtSolver->add(storm::expressions::iff(element.first, globalExpressionInformation.getPredicates()[element.second]));
decisionVariables.push_back(element.first); decisionVariables.push_back(element.first);
} }
@ -55,7 +55,7 @@ namespace storm {
void StateSetAbstractor<DdType, ValueType>::refine(std::vector<uint_fast64_t> const& newPredicates) { 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. // Make the partition aware of the new predicates, which may make more predicates relevant to the abstraction.
for (auto const& predicateIndex : newPredicates) { for (auto const& predicateIndex : newPredicates) {
variablePartition.addExpression(expressionInformation.getPredicates()[predicateIndex]);
localExpressionInformation.addExpression(globalExpressionInformation.getPredicateByIndex(predicateIndex), predicateIndex);
} }
needsRecomputation = true; needsRecomputation = true;
} }
@ -86,7 +86,7 @@ namespace storm {
template <storm::dd::DdType DdType, typename ValueType> template <storm::dd::DdType DdType, typename ValueType>
void StateSetAbstractor<DdType, ValueType>::recomputeCachedBdd() { void StateSetAbstractor<DdType, ValueType>::recomputeCachedBdd() {
// Now check whether we need to recompute the cached BDD. // Now check whether we need to recompute the cached BDD.
std::set<uint_fast64_t> newRelevantPredicateIndices = variablePartition.getRelatedExpressions(concretePredicateVariables);
std::set<uint_fast64_t> newRelevantPredicateIndices = localExpressionInformation.getRelatedExpressions(concretePredicateVariables);
STORM_LOG_TRACE("Found " << newRelevantPredicateIndices.size() << " relevant predicates in abstractor."); 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. // Since the number of relevant predicates is monotonic, we can simply check for the size here.
@ -135,7 +135,7 @@ namespace storm {
smtSolver->push(); smtSolver->push();
// Then add the constraint. // Then add the constraint.
std::pair<std::vector<storm::expressions::Expression>, std::unordered_map<std::pair<uint_fast64_t, uint_fast64_t>, storm::expressions::Variable>> result = constraint.toExpression(expressionInformation.getManager(), ddInformation.bddVariableIndexToPredicateMap);
std::pair<std::vector<storm::expressions::Expression>, std::unordered_map<std::pair<uint_fast64_t, uint_fast64_t>, storm::expressions::Variable>> result = constraint.toExpression(globalExpressionInformation.getManager(), ddInformation.bddVariableIndexToPredicateMap);
for (auto const& expression : result.first) { for (auto const& expression : result.first) {
smtSolver->add(expression); smtSolver->add(expression);

10
src/storage/prism/menu_games/StateSetAbstractor.h
View File

@ -11,7 +11,7 @@
#include "src/solver/SmtSolver.h" #include "src/solver/SmtSolver.h"
#include "src/storage/prism/menu_games/VariablePartition.h"
#include "src/storage/prism/menu_games/LocalExpressionInformation.h"
namespace storm { namespace storm {
namespace utility { namespace utility {
@ -115,14 +115,14 @@ namespace storm {
// The SMT solver used for abstracting the set of states. // The SMT solver used for abstracting the set of states.
std::unique_ptr<storm::solver::SmtSolver> smtSolver; std::unique_ptr<storm::solver::SmtSolver> smtSolver;
// The expression-related information.
AbstractionExpressionInformation& expressionInformation;
// The global expression-related information.
AbstractionExpressionInformation& globalExpressionInformation;
// The DD-related information. // The DD-related information.
AbstractionDdInformation<DdType, ValueType> const& ddInformation; AbstractionDdInformation<DdType, ValueType> const& ddInformation;
// The partition of the variables.
VariablePartition variablePartition;
// The local expression-related information.
LocalExpressionInformation localExpressionInformation;
// The set of relevant predicates and the corresponding decision variables. // The set of relevant predicates and the corresponding decision variables.
std::vector<std::pair<storm::expressions::Variable, uint_fast64_t>> relevantPredicatesAndVariables; std::vector<std::pair<storm::expressions::Variable, uint_fast64_t>> relevantPredicatesAndVariables;

Write Preview
Loading…
Cancel
Save