diff --git a/src/storage/prism/menu_games/AbstractCommand.cpp b/src/storage/prism/menu_games/AbstractCommand.cpp
index 1c050cbc5..821512f95 100644
--- a/src/storage/prism/menu_games/AbstractCommand.cpp
+++ b/src/storage/prism/menu_games/AbstractCommand.cpp
@@ -18,13 +18,13 @@ namespace storm {
namespace prism {
namespace menu_games {
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.
relevantPredicatesAndVariables.second.resize(command.getNumberOfUpdates());
// Assert all range expressions to enforce legal variable values.
- for (auto const& rangeExpression : expressionInformation.getRangeExpressions()) {
+ for (auto const& rangeExpression : globalExpressionInformation.getRangeExpressions()) {
smtSolver->add(rangeExpression);
}
@@ -32,8 +32,8 @@ namespace storm {
smtSolver->add(command.getGuardExpression());
// 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;
}
this->refine(allPredicateIndices);
@@ -43,10 +43,10 @@ namespace storm {
void AbstractCommand<DdType, ValueType>::refine(std::vector<uint_fast64_t> const& predicates) {
// Add all predicates to the variable partition.
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
// whether they changed.
@@ -119,19 +119,19 @@ namespace storm {
std::set<storm::expressions::Variable> assignedVariables;
for (auto const& assignment : assignments) {
// 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());
// Variables that are being assigned are relevant for the successor state.
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());
// Keep track of all assigned variables, so we can find the related predicates later.
assignedVariables.insert(assignedVariable);
}
- auto const& predicatesRelatedToAssignedVariable = variablePartition.getRelatedExpressions(assignedVariables);
+ auto const& predicatesRelatedToAssignedVariable = localExpressionInformation.getRelatedExpressions(assignedVariables);
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;
// 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.
for (auto const& update : command.get().getUpdates()) {
@@ -173,9 +173,9 @@ namespace storm {
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) {
// 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) {
- 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);
}
@@ -185,9 +185,9 @@ namespace storm {
// Do the same for every update.
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) {
- 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);
}
@@ -277,7 +277,7 @@ namespace storm {
auto relevantIte = relevantPredicatesAndVariables.first.end();
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) {
result &= ddInformation.predicateIdentities[predicateIndex];
} else {
diff --git a/src/storage/prism/menu_games/AbstractCommand.h b/src/storage/prism/menu_games/AbstractCommand.h
index 77db969fe..57f7db9ed 100644
--- a/src/storage/prism/menu_games/AbstractCommand.h
+++ b/src/storage/prism/menu_games/AbstractCommand.h
@@ -6,7 +6,7 @@
#include <set>
#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/expressions/Expression.h"
@@ -155,8 +155,8 @@ namespace storm {
// An SMT responsible for this abstract command.
std::unique_ptr<storm::solver::SmtSolver> smtSolver;
- // The expression-related information.
- AbstractionExpressionInformation& expressionInformation;
+ // The global expression-related information.
+ AbstractionExpressionInformation& globalExpressionInformation;
// The DD-related information.
AbstractionDdInformation<DdType, ValueType> const& ddInformation;
@@ -164,8 +164,8 @@ namespace storm {
// The concrete command this abstract command refers to.
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.
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;
diff --git a/src/storage/prism/menu_games/AbstractionExpressionInformation.cpp b/src/storage/prism/menu_games/AbstractionExpressionInformation.cpp
index 621d59c01..54ce74223 100644
--- a/src/storage/prism/menu_games/AbstractionExpressionInformation.cpp
+++ b/src/storage/prism/menu_games/AbstractionExpressionInformation.cpp
@@ -37,6 +37,14 @@ namespace storm {
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;
}
diff --git a/src/storage/prism/menu_games/AbstractionExpressionInformation.h b/src/storage/prism/menu_games/AbstractionExpressionInformation.h
index 25c23cb30..ece6e2075 100644
--- a/src/storage/prism/menu_games/AbstractionExpressionInformation.h
+++ b/src/storage/prism/menu_games/AbstractionExpressionInformation.h
@@ -67,7 +67,21 @@ namespace storm {
* @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.
*
diff --git a/src/storage/prism/menu_games/VariablePartition.cpp b/src/storage/prism/menu_games/LocalExpressionInformation.cpp
similarity index 76%
rename from src/storage/prism/menu_games/VariablePartition.cpp
rename to src/storage/prism/menu_games/LocalExpressionInformation.cpp
index 1f872a83e..2be853712 100644
--- a/src/storage/prism/menu_games/VariablePartition.cpp
+++ b/src/storage/prism/menu_games/LocalExpressionInformation.cpp
@@ -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>
@@ -7,7 +7,7 @@
namespace storm {
namespace prism {
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.
uint_fast64_t currentBlock = 0;
variableBlocks.resize(relevantVariables.size());
@@ -19,12 +19,12 @@ namespace storm {
}
// 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.
std::set<storm::expressions::Variable> expressionVariables = expression.getVariables();
for (auto const& variable : expressionVariables) {
@@ -37,19 +37,20 @@ namespace storm {
expressionBlocks[getBlockIndexOfVariable(*expressionVariables.begin())].insert(this->expressions.size());
// Add expression and relate all the appearing variables.
+ this->globalToLocalIndexMapping[globalExpressionIndex] = this->expressions.size();
this->expressions.push_back(expression);
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);
}
- 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});
}
- 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.
std::set<uint_fast64_t> blocksToMerge;
for (auto const& variable : variables) {
@@ -67,7 +68,7 @@ namespace storm {
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.
std::vector<std::set<storm::expressions::Variable>> newVariableBlocks;
std::vector<std::set<uint_fast64_t>> newExpressionBlocks;
@@ -107,28 +108,28 @@ namespace storm {
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)];
}
- uint_fast64_t VariablePartition::getNumberOfBlocks() const {
+ uint_fast64_t LocalExpressionInformation::getNumberOfBlocks() const {
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];
}
- 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.");
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)];
}
- 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.
std::set<uint_fast64_t> relatedExpressionBlockIndices;
for (auto const& variable : variables) {
@@ -143,12 +144,12 @@ namespace storm {
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.");
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;
for (auto const& variable : variables) {
@@ -160,11 +161,11 @@ namespace storm {
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];
}
- std::ostream& operator<<(std::ostream& out, VariablePartition const& partition) {
+ std::ostream& operator<<(std::ostream& out, LocalExpressionInformation const& partition) {
std::vector<std::string> blocks;
for (uint_fast64_t index = 0; index < partition.variableBlocks.size(); ++index) {
auto const& variableBlock = partition.variableBlocks[index];
diff --git a/src/storage/prism/menu_games/VariablePartition.h b/src/storage/prism/menu_games/LocalExpressionInformation.h
similarity index 87%
rename from src/storage/prism/menu_games/VariablePartition.h
rename to src/storage/prism/menu_games/LocalExpressionInformation.h
index b9d87dad1..908d2f181 100644
--- a/src/storage/prism/menu_games/VariablePartition.h
+++ b/src/storage/prism/menu_games/LocalExpressionInformation.h
@@ -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 <set>
@@ -13,23 +13,24 @@ namespace storm {
namespace prism {
namespace menu_games {
- class VariablePartition{
+ class LocalExpressionInformation {
public:
/*!
* Constructs a new variable 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.
*
* @param expression The expression to add.
+ * @param globalExpressionIndex The global index of the expression.
* @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.
@@ -128,7 +129,7 @@ namespace storm {
*/
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:
/*!
@@ -153,14 +154,17 @@ namespace storm {
// 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;
+ // A mapping from global expression indices to local ones.
+ std::unordered_map<uint_fast64_t, uint_fast64_t> globalToLocalIndexMapping;
+
// The vector of all 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_ */
\ No newline at end of file
+#endif /* STORM_STORAGE_PRISM_MENU_GAMES_LOCALEXPRESSIONINFORMATION_H_ */
\ No newline at end of file
diff --git a/src/storage/prism/menu_games/StateSetAbstractor.cpp b/src/storage/prism/menu_games/StateSetAbstractor.cpp
index db8dab01d..5b228afbb 100644
--- a/src/storage/prism/menu_games/StateSetAbstractor.cpp
+++ b/src/storage/prism/menu_games/StateSetAbstractor.cpp
@@ -13,10 +13,10 @@ namespace storm {
namespace menu_games {
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.
- for (auto const& rangeExpression : expressionInformation.getRangeExpressions()) {
+ for (auto const& rangeExpression : globalExpressionInformation.getRangeExpressions()) {
smtSolver->add(rangeExpression);
}
@@ -27,12 +27,12 @@ namespace storm {
// 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);
+ localExpressionInformation.relate(usedVariables);
}
// 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;
}
this->refine(allPredicateIndices);
@@ -40,10 +40,10 @@ namespace storm {
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.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) {
- 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);
}
@@ -55,7 +55,7 @@ namespace storm {
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.getPredicates()[predicateIndex]);
+ localExpressionInformation.addExpression(globalExpressionInformation.getPredicateByIndex(predicateIndex), predicateIndex);
}
needsRecomputation = true;
}
@@ -86,7 +86,7 @@ namespace storm {
template <storm::dd::DdType DdType, typename ValueType>
void StateSetAbstractor<DdType, ValueType>::recomputeCachedBdd() {
// 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.");
// Since the number of relevant predicates is monotonic, we can simply check for the size here.
@@ -135,7 +135,7 @@ namespace storm {
smtSolver->push();
// 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) {
smtSolver->add(expression);
diff --git a/src/storage/prism/menu_games/StateSetAbstractor.h b/src/storage/prism/menu_games/StateSetAbstractor.h
index fef77eb29..157aa27b7 100644
--- a/src/storage/prism/menu_games/StateSetAbstractor.h
+++ b/src/storage/prism/menu_games/StateSetAbstractor.h
@@ -11,7 +11,7 @@
#include "src/solver/SmtSolver.h"
-#include "src/storage/prism/menu_games/VariablePartition.h"
+#include "src/storage/prism/menu_games/LocalExpressionInformation.h"
namespace storm {
namespace utility {
@@ -115,14 +115,14 @@ namespace storm {
// The SMT solver used for abstracting the set of states.
std::unique_ptr<storm::solver::SmtSolver> smtSolver;
- // The expression-related information.
- AbstractionExpressionInformation& expressionInformation;
+ // The global expression-related information.
+ AbstractionExpressionInformation& globalExpressionInformation;
// The DD-related information.
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.
std::vector<std::pair<storm::expressions::Variable, uint_fast64_t>> relevantPredicatesAndVariables;