diff --git a/src/storage/dd/CuddAdd.cpp b/src/storage/dd/CuddAdd.cpp
index 691b500a1..58f17137b 100644
--- a/src/storage/dd/CuddAdd.cpp
+++ b/src/storage/dd/CuddAdd.cpp
@@ -420,6 +420,10 @@ namespace storm {
return static_cast<uint_fast64_t>(this->getCuddAdd().NodeReadIndex());
}
+ uint_fast64_t Add<DdType::CUDD>::getLevel() const {
+ return static_cast<uint_fast64_t>(this->getDdManager()->getCuddManager().ReadPerm(this->getIndex()));
+ }
+
template<typename ValueType>
std::vector<ValueType> Add<DdType::CUDD>::toVector() const {
return this->toVector<ValueType>(Odd<DdType::CUDD>(*this));
diff --git a/src/storage/dd/CuddAdd.h b/src/storage/dd/CuddAdd.h
index b7d9fbfcb..f80422493 100644
--- a/src/storage/dd/CuddAdd.h
+++ b/src/storage/dd/CuddAdd.h
@@ -520,6 +520,13 @@ namespace storm {
*/
virtual uint_fast64_t getIndex() const override;
+ /*!
+ * Retrieves the level of the topmost variable in the DD.
+ *
+ * @return The level of the topmost variable in DD.
+ */
+ virtual uint_fast64_t getLevel() const override;
+
/*!
* Converts the ADD to a vector.
*
diff --git a/src/storage/dd/CuddBdd.cpp b/src/storage/dd/CuddBdd.cpp
index 3c2ff4ad3..09e59f390 100644
--- a/src/storage/dd/CuddBdd.cpp
+++ b/src/storage/dd/CuddBdd.cpp
@@ -35,7 +35,6 @@ namespace storm {
this->cuddBdd = fromVector<double>(ddManager, explicitValues, odd, metaVariables, std::bind(std::less_equal<double>(), value, std::placeholders::_1));
break;
}
-
}
Add<DdType::CUDD> Bdd<DdType::CUDD>::toAdd() const {
@@ -242,6 +241,10 @@ namespace storm {
return static_cast<uint_fast64_t>(this->getCuddBdd().NodeReadIndex());
}
+ uint_fast64_t Bdd<DdType::CUDD>::getLevel() const {
+ return static_cast<uint_fast64_t>(this->getDdManager()->getCuddManager().ReadPerm(this->getIndex()));
+ }
+
void Bdd<DdType::CUDD>::exportToDot(std::string const& filename) const {
if (filename.empty()) {
std::vector<BDD> cuddBddVector = { this->getCuddBdd() };
diff --git a/src/storage/dd/CuddBdd.h b/src/storage/dd/CuddBdd.h
index d9af17483..a21402c86 100644
--- a/src/storage/dd/CuddBdd.h
+++ b/src/storage/dd/CuddBdd.h
@@ -262,6 +262,13 @@ namespace storm {
*/
virtual uint_fast64_t getIndex() const override;
+ /*!
+ * Retrieves the level of the topmost variable in the DD.
+ *
+ * @return The level of the topmost variable in DD.
+ */
+ virtual uint_fast64_t getLevel() const override;
+
/*!
* Exports the BDD to the given file in the dot format.
*
diff --git a/src/storage/dd/CuddDd.h b/src/storage/dd/CuddDd.h
index 0077bcc8a..dbfa5ddae 100644
--- a/src/storage/dd/CuddDd.h
+++ b/src/storage/dd/CuddDd.h
@@ -68,6 +68,13 @@ namespace storm {
*/
virtual uint_fast64_t getIndex() const = 0;
+ /*!
+ * Retrieves the level of the topmost variable in the DD.
+ *
+ * @return The level of the topmost variable in DD.
+ */
+ virtual uint_fast64_t getLevel() const = 0;
+
/*!
* Retrieves whether the given meta variable is contained in the DD.
*
diff --git a/src/storage/dd/CuddDdManager.cpp b/src/storage/dd/CuddDdManager.cpp
index b5f31e442..b01b12470 100644
--- a/src/storage/dd/CuddDdManager.cpp
+++ b/src/storage/dd/CuddDdManager.cpp
@@ -114,7 +114,7 @@ namespace storm {
return result;
}
- std::pair<storm::expressions::Variable, storm::expressions::Variable> DdManager<DdType::CUDD>::addMetaVariable(std::string const& name, int_fast64_t low, int_fast64_t high) {
+ std::pair<storm::expressions::Variable, storm::expressions::Variable> DdManager<DdType::CUDD>::addMetaVariable(std::string const& name, int_fast64_t low, int_fast64_t high, boost::optional<std::pair<MetaVariablePosition, storm::expressions::Variable>> const& position) {
// Check whether the variable name is legal.
STORM_LOG_THROW(name != "" && name.back() != '\'', storm::exceptions::InvalidArgumentException, "Illegal name of meta variable: '" << name << "'.");
@@ -126,14 +126,32 @@ namespace storm {
std::size_t numberOfBits = static_cast<std::size_t>(std::ceil(std::log2(high - low + 1)));
+ // If a specific position was requested, we compute it now.
+ boost::optional<uint_fast64_t> level;
+ if (position) {
+ storm::dd::DdMetaVariable<DdType::CUDD> beforeVariable = this->getMetaVariable(position.get().second);
+ level = position.get().first == MetaVariablePosition::Above ? std::numeric_limits<uint_fast64_t>::max() : std::numeric_limits<uint_fast64_t>::min();
+ for (auto const& ddVariable : beforeVariable.getDdVariables()) {
+ level = position.get().first == MetaVariablePosition::Above ? std::min(level.get(), ddVariable.getLevel()) : std::max(level.get(), ddVariable.getLevel());
+ }
+ if (position.get().first == MetaVariablePosition::Below) {
+ ++level.get();
+ }
+ }
+
storm::expressions::Variable unprimed = manager->declareBitVectorVariable(name, numberOfBits);
storm::expressions::Variable primed = manager->declareBitVectorVariable(name + "'", numberOfBits);
std::vector<Bdd<DdType::CUDD>> variables;
std::vector<Bdd<DdType::CUDD>> variablesPrime;
for (std::size_t i = 0; i < numberOfBits; ++i) {
- variables.emplace_back(Bdd<DdType::CUDD>(this->shared_from_this(), cuddManager.bddVar(), {unprimed}));
- variablesPrime.emplace_back(Bdd<DdType::CUDD>(this->shared_from_this(), cuddManager.bddVar(), {primed}));
+ if (level) {
+ variables.emplace_back(Bdd<DdType::CUDD>(this->shared_from_this(), cuddManager.bddNewVarAtLevel(level.get() + 2 * i), {unprimed}));
+ variablesPrime.emplace_back(Bdd<DdType::CUDD>(this->shared_from_this(), cuddManager.bddNewVarAtLevel(level.get() + 2 * i + 1), {primed}));
+ } else {
+ variables.emplace_back(Bdd<DdType::CUDD>(this->shared_from_this(), cuddManager.bddVar(), {unprimed}));
+ variablesPrime.emplace_back(Bdd<DdType::CUDD>(this->shared_from_this(), cuddManager.bddVar(), {primed}));
+ }
}
// Now group the non-primed and primed variable.
@@ -147,20 +165,38 @@ namespace storm {
return std::make_pair(unprimed, primed);
}
- std::pair<storm::expressions::Variable, storm::expressions::Variable> DdManager<DdType::CUDD>::addMetaVariable(std::string const& name) {
+ std::pair<storm::expressions::Variable, storm::expressions::Variable> DdManager<DdType::CUDD>::addMetaVariable(std::string const& name, boost::optional<std::pair<MetaVariablePosition, storm::expressions::Variable>> const& position) {
// Check whether the variable name is legal.
STORM_LOG_THROW(name != "" && name.back() != '\'', storm::exceptions::InvalidArgumentException, "Illegal name of meta variable: '" << name << "'.");
// Check whether a meta variable already exists.
STORM_LOG_THROW(!this->hasMetaVariable(name), storm::exceptions::InvalidArgumentException, "A meta variable '" << name << "' already exists.");
+ // If a specific position was requested, we compute it now.
+ boost::optional<uint_fast64_t> level;
+ if (position) {
+ storm::dd::DdMetaVariable<DdType::CUDD> beforeVariable = this->getMetaVariable(position.get().second);
+ level = position.get().first == MetaVariablePosition::Above ? std::numeric_limits<uint_fast64_t>::max() : std::numeric_limits<uint_fast64_t>::min();
+ for (auto const& ddVariable : beforeVariable.getDdVariables()) {
+ level = position.get().first == MetaVariablePosition::Above ? std::min(level.get(), ddVariable.getLevel()) : std::max(level.get(), ddVariable.getLevel());
+ }
+ if (position.get().first == MetaVariablePosition::Below) {
+ ++level.get();
+ }
+ }
+
storm::expressions::Variable unprimed = manager->declareBooleanVariable(name);
storm::expressions::Variable primed = manager->declareBooleanVariable(name + "'");
std::vector<Bdd<DdType::CUDD>> variables;
std::vector<Bdd<DdType::CUDD>> variablesPrime;
- variables.emplace_back(Bdd<DdType::CUDD>(this->shared_from_this(), cuddManager.bddVar(), {unprimed}));
- variablesPrime.emplace_back(Bdd<DdType::CUDD>(this->shared_from_this(), cuddManager.bddVar(), {primed}));
+ if (position) {
+ variables.emplace_back(Bdd<DdType::CUDD>(this->shared_from_this(), cuddManager.bddNewVarAtLevel(level.get()), {unprimed}));
+ variablesPrime.emplace_back(Bdd<DdType::CUDD>(this->shared_from_this(), cuddManager.bddNewVarAtLevel(level.get() + 1), {primed}));
+ } else {
+ variables.emplace_back(Bdd<DdType::CUDD>(this->shared_from_this(), cuddManager.bddVar(), {unprimed}));
+ variablesPrime.emplace_back(Bdd<DdType::CUDD>(this->shared_from_this(), cuddManager.bddVar(), {primed}));
+ }
// Now group the non-primed and primed variable.
this->getCuddManager().MakeTreeNode(variables.front().getIndex(), 2, MTR_FIXED);
diff --git a/src/storage/dd/CuddDdManager.h b/src/storage/dd/CuddDdManager.h
index ec6a3b57d..e70ea0144 100644
--- a/src/storage/dd/CuddDdManager.h
+++ b/src/storage/dd/CuddDdManager.h
@@ -3,7 +3,9 @@
#include <unordered_map>
#include <memory>
+#include <boost/optional.hpp>
+#include "src/storage/dd/MetaVariablePosition.h"
#include "src/storage/dd/DdManager.h"
#include "src/storage/dd/CuddDdMetaVariable.h"
#include "src/utility/OsDetection.h"
@@ -26,7 +28,7 @@ namespace storm {
friend class Add<DdType::CUDD>;
friend class Odd<DdType::CUDD>;
friend class DdForwardIterator<DdType::CUDD>;
-
+
/*!
* Creates an empty manager without any meta variables.
*/
@@ -110,15 +112,19 @@ namespace storm {
* @param variableName The name of the new variable.
* @param low The lowest value of the range of the variable.
* @param high The highest value of the range of the variable.
+ * @param position A pair indicating the position of the new meta variable. If not given, the meta variable
+ * will be created below all existing ones.
*/
- std::pair<storm::expressions::Variable, storm::expressions::Variable> addMetaVariable(std::string const& variableName, int_fast64_t low, int_fast64_t high);
+ std::pair<storm::expressions::Variable, storm::expressions::Variable> addMetaVariable(std::string const& variableName, int_fast64_t low, int_fast64_t high, boost::optional<std::pair<MetaVariablePosition, storm::expressions::Variable>> const& position = boost::none);
/*!
* Adds a boolean meta variable.
*
* @param variableName The name of the new variable.
+ * @param position A pair indicating the position of the new meta variable. If not given, the meta variable
+ * will be created below all existing ones.
*/
- std::pair<storm::expressions::Variable, storm::expressions::Variable> addMetaVariable(std::string const& variableName);
+ std::pair<storm::expressions::Variable, storm::expressions::Variable> addMetaVariable(std::string const& variableName, boost::optional<std::pair<MetaVariablePosition, storm::expressions::Variable>> const& position = boost::none);
/*!
* Retrieves the names of all meta variables that have been added to the manager.
diff --git a/src/storage/dd/MetaVariablePosition.h b/src/storage/dd/MetaVariablePosition.h
new file mode 100644
index 000000000..5fb9724f2
--- /dev/null
+++ b/src/storage/dd/MetaVariablePosition.h
@@ -0,0 +1,15 @@
+#ifndef STORM_STORAGE_DD_METAVARIABLEPOSITION_H_
+#define STORM_STORAGE_DD_METAVARIABLEPOSITION_H_
+
+#include "src/storage/dd/DdType.h"
+
+namespace storm {
+ namespace dd {
+
+ // An enum that expresses the relation of two meta variables relative to each other.
+ enum class MetaVariablePosition { Above, Below };
+
+ }
+}
+
+#endif /* STORM_STORAGE_DD_METAVARIABLEPOSITION_H_ */
diff --git a/src/storage/prism/menu_games/AbstractCommand.cpp b/src/storage/prism/menu_games/AbstractCommand.cpp
index 4bd5a3ec4..3b91eb01e 100644
--- a/src/storage/prism/menu_games/AbstractCommand.cpp
+++ b/src/storage/prism/menu_games/AbstractCommand.cpp
@@ -71,11 +71,11 @@ namespace storm {
template <storm::dd::DdType DdType, typename ValueType>
void AbstractCommand<DdType, ValueType>::recomputeCachedBdd() {
STORM_LOG_TRACE("Recomputing BDD for command " << command.get());
- std::cout << "recomputing " << command.get() << std::endl;
// Create a mapping from source state DDs to their distributions.
std::unordered_map<storm::dd::Bdd<DdType>, std::vector<storm::dd::Bdd<DdType>>> sourceToDistributionsMap;
- smtSolver->allSat(decisionVariables, [&sourceToDistributionsMap,this] (storm::solver::SmtSolver::ModelReference const& model) { sourceToDistributionsMap[getSourceStateBdd(model)].push_back(getDistributionBdd(model)); return true; } );
+ uint_fast64_t modelCounter = 0;
+ smtSolver->allSat(decisionVariables, [&sourceToDistributionsMap,this,&modelCounter] (storm::solver::SmtSolver::ModelReference const& model) { sourceToDistributionsMap[getSourceStateBdd(model)].push_back(getDistributionBdd(model)); ++modelCounter; return true; } );
// Now we search for the maximal number of choices of player 2 to determine how many DD variables we
// need to encode the nondeterminism.
@@ -88,17 +88,27 @@ namespace storm {
// Finally, build overall result.
storm::dd::Bdd<DdType> resultBdd = ddInformation.manager->getBddZero();
+ uint_fast64_t sourceStateIndex = 0;
for (auto const& sourceDistributionsPair : sourceToDistributionsMap) {
- uint_fast64_t distributionIndex = 0;
+ STORM_LOG_ASSERT(!sourceDistributionsPair.first.isZero(), "The source BDD must not be empty.");
+ STORM_LOG_ASSERT(!sourceDistributionsPair.second.empty(), "The distributions must not be empty.");
storm::dd::Bdd<DdType> allDistributions = ddInformation.manager->getBddZero();
+ uint_fast64_t distributionIndex = 0;
for (auto const& distribution : sourceDistributionsPair.second) {
allDistributions |= distribution && ddInformation.encodeDistributionIndex(numberOfVariablesNeeded, distributionIndex);
+ ++distributionIndex;
+ STORM_LOG_ASSERT(!allDistributions.isZero(), "The BDD must not be empty.");
}
resultBdd |= sourceDistributionsPair.first && allDistributions;
+ ++sourceStateIndex;
+ STORM_LOG_ASSERT(!resultBdd.isZero(), "The BDD must not be empty.");
}
- resultBdd &= computeMissingSourceStateIdentities();
+ STORM_LOG_ASSERT(sourceToDistributionsMap.empty() || !resultBdd.isZero(), "The BDD must not be empty, if there were distributions.");
+ resultBdd &= computeMissingIdentities();
+ STORM_LOG_ASSERT(sourceToDistributionsMap.empty() || !resultBdd.isZero(), "The BDD must not be empty, if there were distributions.");
resultBdd &= ddInformation.manager->getEncoding(ddInformation.commandDdVariable, command.get().getGlobalIndex());
+ STORM_LOG_ASSERT(sourceToDistributionsMap.empty() || !resultBdd.isZero(), "The BDD must not be empty, if there were distributions.");
// Cache the result.
cachedDd = std::make_pair(resultBdd, numberOfVariablesNeeded);
@@ -172,10 +182,6 @@ namespace storm {
// Insert the new variables into the record of relevant source variables.
relevantPredicatesAndVariables.first.insert(relevantPredicatesAndVariables.first.end(), newSourceVariables.begin(), newSourceVariables.end());
std::sort(relevantPredicatesAndVariables.first.begin(), relevantPredicatesAndVariables.first.end(), [] (std::pair<storm::expressions::Variable, uint_fast64_t> const& first, std::pair<storm::expressions::Variable, uint_fast64_t> const& second) { return first.second < second.second; } );
- std::cout << "sorted!" << std::endl;
- for (auto const& el : relevantPredicatesAndVariables.first) {
- std::cout << el.first.getName() << " // " << el.second << std::endl;
- }
// Do the same for every update.
for (uint_fast64_t index = 0; index < command.get().getNumberOfUpdates(); ++index) {
@@ -195,13 +201,14 @@ namespace storm {
STORM_LOG_TRACE("Building source state BDD.");
storm::dd::Bdd<DdType> result = ddInformation.manager->getBddOne();
for (auto const& variableIndexPair : relevantPredicatesAndVariables.first) {
- std::cout << "size: " << ddInformation.predicateBdds.size() << " and index " << variableIndexPair.second << std::endl;
if (model.getBooleanValue(variableIndexPair.first)) {
result &= ddInformation.predicateBdds[variableIndexPair.second].first;
} else {
result &= !ddInformation.predicateBdds[variableIndexPair.second].first;
}
}
+
+ STORM_LOG_ASSERT(!result.isZero(), "Source must not be empty.");
return result;
}
@@ -223,6 +230,24 @@ namespace storm {
updateBdd &= ddInformation.manager->getEncoding(ddInformation.updateDdVariable, updateIndex);
}
+ result |= updateBdd;
+ }
+
+ STORM_LOG_ASSERT(!result.isZero(), "Distribution must not be empty.");
+ return result;
+ }
+
+ template <storm::dd::DdType DdType, typename ValueType>
+ storm::dd::Bdd<DdType> AbstractCommand<DdType, ValueType>::computeMissingIdentities() const {
+ storm::dd::Bdd<DdType> identities = computeMissingGlobalIdentities();
+ identities &= computeMissingUpdateIdentities();
+ return identities;
+ }
+
+ template <storm::dd::DdType DdType, typename ValueType>
+ storm::dd::Bdd<DdType> AbstractCommand<DdType, ValueType>::computeMissingUpdateIdentities() const {
+ storm::dd::Bdd<DdType> result = ddInformation.manager->getBddZero();
+ for (uint_fast64_t updateIndex = 0; updateIndex < command.get().getNumberOfUpdates(); ++updateIndex) {
// Compute the identities that are missing for this update.
auto firstIt = relevantPredicatesAndVariables.first.begin();
auto firstIte = relevantPredicatesAndVariables.first.end();
@@ -231,33 +256,29 @@ namespace storm {
// Go through all relevant source predicates. This is guaranteed to be a superset of the set of
// relevant successor predicates for any update.
+ storm::dd::Bdd<DdType> updateIdentity = ddInformation.manager->getBddOne();
for (; firstIt != firstIte; ++firstIt) {
// If the predicates do not match, there is a predicate missing, so we need to add its identity.
if (secondIt == secondIte || firstIt->second != secondIt->second) {
- updateBdd &= ddInformation.predicateIdentities[firstIt->second];
+ updateIdentity &= ddInformation.predicateIdentities[firstIt->second];
} else if (secondIt != secondIte) {
++secondIt;
}
}
- result |= updateBdd;
+ result |= updateIdentity && ddInformation.manager->getEncoding(ddInformation.updateDdVariable, updateIndex);
}
-
return result;
}
template <storm::dd::DdType DdType, typename ValueType>
- storm::dd::Bdd<DdType> AbstractCommand<DdType, ValueType>::computeMissingSourceStateIdentities() const {
+ storm::dd::Bdd<DdType> AbstractCommand<DdType, ValueType>::computeMissingGlobalIdentities() const {
auto relevantIt = relevantPredicatesAndVariables.first.begin();
auto relevantIte = relevantPredicatesAndVariables.first.end();
- std::cout << "the size is " << relevantPredicatesAndVariables.first.size() << std::endl;
storm::dd::Bdd<DdType> result = ddInformation.manager->getBddOne();
for (uint_fast64_t predicateIndex = 0; predicateIndex < expressionInformation.predicates.size(); ++predicateIndex) {
if (relevantIt == relevantIte || relevantIt->second != predicateIndex) {
- std::cout << (relevantIt == relevantIte) << std::endl;
- std::cout << relevantIt->second << " vs " << predicateIndex << std::endl;
- std::cout << "multiplying identity " << predicateIndex << std::endl;
result &= ddInformation.predicateIdentities[predicateIndex];
} else {
++relevantIt;
diff --git a/src/storage/prism/menu_games/AbstractCommand.h b/src/storage/prism/menu_games/AbstractCommand.h
index 844231edb..ecd8ff971 100644
--- a/src/storage/prism/menu_games/AbstractCommand.h
+++ b/src/storage/prism/menu_games/AbstractCommand.h
@@ -128,14 +128,29 @@ namespace storm {
* Recomputes the cached BDD. This needs to be triggered if any relevant predicates change.
*/
void recomputeCachedBdd();
+
+ /*!
+ * Computes the missing state identities.
+ *
+ * @return A BDD that represents the all missing state identities.
+ */
+ storm::dd::Bdd<DdType> computeMissingIdentities() const;
+
+ /*!
+ * Computes the missing state identities for the updates.
+ *
+ * @return A BDD that represents the state identities for predicates that are irrelevant for the
+ * successor states.
+ */
+ storm::dd::Bdd<DdType> computeMissingUpdateIdentities() const;
/*!
- * Computes the missing source state identities.
+ * Computes the globally missing state identities.
*
- * @return A BDD that represents the source state identities for predicates that are irrelevant for the
- * source states.
+ * @return A BDD that represents the global state identities for predicates that are irrelevant for the
+ * source and successor states.
*/
- storm::dd::Bdd<DdType> computeMissingSourceStateIdentities() const;
+ storm::dd::Bdd<DdType> computeMissingGlobalIdentities() const;
// An SMT responsible for this abstract command.
std::unique_ptr<storm::solver::SmtSolver> smtSolver;
diff --git a/src/storage/prism/menu_games/AbstractProgram.cpp b/src/storage/prism/menu_games/AbstractProgram.cpp
index 14a364321..792efc323 100644
--- a/src/storage/prism/menu_games/AbstractProgram.cpp
+++ b/src/storage/prism/menu_games/AbstractProgram.cpp
@@ -34,11 +34,6 @@ namespace storm {
totalNumberOfCommands += module.getNumberOfCommands();
}
- // Create DD variables for all predicates.
- for (auto const& predicate : expressionInformation.predicates) {
- ddInformation.addPredicate(predicate);
- }
-
// Create DD variable for the command encoding.
ddInformation.commandDdVariable = ddInformation.manager->addMetaVariable("command", 0, totalNumberOfCommands - 1).first;
@@ -51,7 +46,12 @@ namespace storm {
// that it's impossible to treat such models in any event.
for (uint_fast64_t index = 0; index < 100; ++index) {
storm::expressions::Variable newOptionVar = ddInformation.manager->addMetaVariable("opt" + std::to_string(index)).first;
- ddInformation.optionDdVariables.push_back(std::make_pair(newOptionVar, ddInformation.manager->getRange(newOptionVar)));
+ ddInformation.optionDdVariables.push_back(std::make_pair(newOptionVar, ddInformation.manager->getIdentity(newOptionVar).toBdd()));
+ }
+
+ // Create DD variables for all predicates.
+ for (auto const& predicate : expressionInformation.predicates) {
+ ddInformation.addPredicate(predicate);
}
// For each module of the concrete program, we create an abstract counterpart.
@@ -68,8 +68,6 @@ namespace storm {
template <storm::dd::DdType DdType, typename ValueType>
void AbstractProgram<DdType, ValueType>::refine(std::vector<storm::expressions::Expression> const& predicates) {
- std::cout << "refining!" << std::endl;
-
// Add the predicates to the global list of predicates.
uint_fast64_t firstNewPredicateIndex = expressionInformation.predicates.size();
expressionInformation.predicates.insert(expressionInformation.predicates.end(), predicates.begin(), predicates.end());
@@ -85,17 +83,13 @@ namespace storm {
newPredicateIndices.push_back(index);
}
- std::cout << "refining modules" << std::endl;
// Refine all abstract modules.
for (auto& module : modules) {
module.refine(newPredicateIndices);
}
- std::cout << "refining initial" << std::endl;
// Refine initial state abstractor.
initialStateAbstractor.refine(newPredicateIndices);
-
- std::cout << "done " << std::endl;
}
template <storm::dd::DdType DdType, typename ValueType>
@@ -108,8 +102,6 @@ namespace storm {
return lastAbstractAdd;
}
- std::cout << "abstr DD new " << std::endl;
-
// Otherwise, we remember that the abstract BDD changed and perform a reachability analysis.
lastAbstractBdd = gameBdd.first;
@@ -118,15 +110,11 @@ namespace storm {
for (uint_fast64_t index = 0; index < gameBdd.second; ++index) {
variablesToAbstract.insert(ddInformation.optionDdVariables[index].first);
}
-
- std::cout << "reachability... " << std::endl;
// Do a reachability analysis on the raw transition relation.
storm::dd::Bdd<DdType> transitionRelation = lastAbstractBdd.existsAbstract(variablesToAbstract);
storm::dd::Bdd<DdType> reachableStates = this->getReachableStates(initialStateAbstractor.getAbstractStates(), transitionRelation);
- std::cout << "done " << std::endl;
-
// Find the deadlock states in the model.
storm::dd::Bdd<DdType> deadlockStates = transitionRelation.existsAbstract(ddInformation.successorVariables);
deadlockStates = reachableStates && !deadlockStates;
diff --git a/src/storage/prism/menu_games/AbstractionDdInformation.cpp b/src/storage/prism/menu_games/AbstractionDdInformation.cpp
index 6395fa951..bb98b5a0b 100644
--- a/src/storage/prism/menu_games/AbstractionDdInformation.cpp
+++ b/src/storage/prism/menu_games/AbstractionDdInformation.cpp
@@ -9,6 +9,8 @@
#include "src/storage/dd/CuddBdd.h"
#include "src/storage/dd/CuddAdd.h"
+#include "src/utility/macros.h"
+
namespace storm {
namespace prism {
namespace menu_games {
@@ -22,6 +24,7 @@ namespace storm {
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 {
@@ -29,6 +32,7 @@ namespace storm {
}
distributionIndex >>= 1;
}
+ STORM_LOG_ASSERT(!result.isZero(), "Update BDD encoding must not be zero.");
return result;
}
@@ -36,7 +40,15 @@ namespace storm {
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());
+ std::pair<storm::expressions::Variable, storm::expressions::Variable> newMetaVariable;
+
+ // Create the new predicate variable below all other predicate variables.
+ if (predicateDdVariables.empty()) {
+ newMetaVariable = manager->addMetaVariable(stream.str());
+ } else {
+ newMetaVariable = manager->addMetaVariable(stream.str(), std::make_pair(storm::dd::MetaVariablePosition::Below, predicateDdVariables.back().second));
+ }
+
predicateDdVariables.push_back(newMetaVariable);
predicateBdds.emplace_back(manager->getEncoding(newMetaVariable.first, 1), manager->getEncoding(newMetaVariable.second, 1));
predicateIdentities.push_back(manager->getIdentity(newMetaVariable.first).equals(manager->getIdentity(newMetaVariable.second)).toBdd());
@@ -46,13 +58,15 @@ namespace storm {
}
template <storm::dd::DdType DdType, typename ValueType>
- storm::dd::Bdd<DdType> AbstractionDdInformation<DdType, ValueType>::getMissingOptionVariableCube(uint_fast64_t lastUsed, uint_fast64_t lastToBe) const {
+ 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 = lastUsed + 1; index <= lastToBe; ++index) {
+ 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;
}
@@ -66,6 +80,8 @@ namespace storm {
// 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;
}
}
diff --git a/src/storage/prism/menu_games/AbstractionDdInformation.h b/src/storage/prism/menu_games/AbstractionDdInformation.h
index ac5fa4316..ef8e08267 100644
--- a/src/storage/prism/menu_games/AbstractionDdInformation.h
+++ b/src/storage/prism/menu_games/AbstractionDdInformation.h
@@ -52,13 +52,13 @@ namespace storm {
void addPredicate(storm::expressions::Expression const& predicate);
/*!
- * Retrieves the cube of option variables in the range (lastUsed, lastToBe] the given indices.
+ * Retrieves the cube of option variables in the range [begin, end) the given indices.
*
- * @param lastUsed The last variable before the range to return.
- * @param lastToBe The last variable of the range to return.
+ * @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 lastUsed, uint_fast64_t lastToBe) const;
+ 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
diff --git a/test/functional/abstraction/PrismMenuGameTest.cpp b/test/functional/abstraction/PrismMenuGameTest.cpp
index d3bd2d56a..466f7693a 100644
--- a/test/functional/abstraction/PrismMenuGameTest.cpp
+++ b/test/functional/abstraction/PrismMenuGameTest.cpp
@@ -15,7 +15,7 @@
#include "src/utility/solver.h"
-TEST(PrismMenuGame, CommandAbstractionTest) {
+TEST(PrismMenuGame, DieProgramAbstractionTest) {
storm::prism::Program program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/die.pm");
std::vector<storm::expressions::Expression> initialPredicates;
@@ -25,13 +25,156 @@ TEST(PrismMenuGame, CommandAbstractionTest) {
storm::prism::menu_games::AbstractProgram<storm::dd::DdType::CUDD, double> abstractProgram(program.getManager(), program, initialPredicates, std::make_unique<storm::utility::solver::MathsatSmtSolverFactory>(), false);
- storm::dd::Add<storm::dd::DdType::CUDD> abstraction = abstractProgram.getAbstractAdd();
- abstraction.exportToDot("abstr1.dot");
+ storm::dd::Add<storm::dd::DdType::CUDD> abstraction;
+ ASSERT_NO_THROW(abstraction = abstractProgram.getAbstractAdd());
- abstractProgram.refine({manager.getVariableExpression("s") == manager.integer(7)});
- abstraction = abstractProgram.getAbstractAdd();
- abstraction.exportToDot("abstr2.dot");
+ EXPECT_EQ(19, abstraction.getNodeCount());
+}
+
+TEST(PrismMenuGame, DieProgramAbstractionAndRefinementTest) {
+ storm::prism::Program program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/die.pm");
+
+ std::vector<storm::expressions::Expression> initialPredicates;
+ storm::expressions::ExpressionManager& manager = program.getManager();
+
+ initialPredicates.push_back(manager.getVariableExpression("s") < manager.integer(3));
+
+ storm::prism::menu_games::AbstractProgram<storm::dd::DdType::CUDD, double> abstractProgram(program.getManager(), program, initialPredicates, std::make_unique<storm::utility::solver::MathsatSmtSolverFactory>(), false);
+
+ storm::dd::Add<storm::dd::DdType::CUDD> abstraction;
+ ASSERT_NO_THROW(abstraction = abstractProgram.getAbstractAdd());
+
+ ASSERT_NO_THROW(abstractProgram.refine({manager.getVariableExpression("s") == manager.integer(7)}));
+ ASSERT_NO_THROW(abstraction = abstractProgram.getAbstractAdd());
+
+ EXPECT_EQ(26, abstraction.getNodeCount());
+}
+
+TEST(PrismMenuGame, CrowdsProgramAbstractionTest) {
+ storm::prism::Program program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/crowds-5-5.pm");
+ program = program.substituteConstants();
+
+ std::vector<storm::expressions::Expression> initialPredicates;
+ storm::expressions::ExpressionManager& manager = program.getManager();
+
+ initialPredicates.push_back(manager.getVariableExpression("phase") < manager.integer(3));
+
+ storm::prism::menu_games::AbstractProgram<storm::dd::DdType::CUDD, double> abstractProgram(program.getManager(), program, initialPredicates, std::make_unique<storm::utility::solver::MathsatSmtSolverFactory>(), false);
+
+ storm::dd::Add<storm::dd::DdType::CUDD> abstraction;
+ ASSERT_NO_THROW(abstraction = abstractProgram.getAbstractAdd());
+
+ EXPECT_EQ(46, abstraction.getNodeCount());
+}
+
+TEST(PrismMenuGame, CrowdsProgramAbstractionAndRefinementTest) {
+ storm::prism::Program program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/crowds-5-5.pm");
+ program = program.substituteConstants();
+
+ std::vector<storm::expressions::Expression> initialPredicates;
+ storm::expressions::ExpressionManager& manager = program.getManager();
+
+ initialPredicates.push_back(manager.getVariableExpression("phase") < manager.integer(3));
+
+ storm::prism::menu_games::AbstractProgram<storm::dd::DdType::CUDD, double> abstractProgram(program.getManager(), program, initialPredicates, std::make_unique<storm::utility::solver::MathsatSmtSolverFactory>(), false);
+
+ storm::dd::Add<storm::dd::DdType::CUDD> abstraction;
+ ASSERT_NO_THROW(abstraction = abstractProgram.getAbstractAdd());
+
+ EXPECT_EQ(46, abstraction.getNodeCount());
+
+ ASSERT_NO_THROW(abstractProgram.refine({manager.getVariableExpression("observe0") + manager.getVariableExpression("observe1") + manager.getVariableExpression("observe2") + manager.getVariableExpression("observe3") + manager.getVariableExpression("observe4") <= manager.getVariableExpression("runCount")}));
+ ASSERT_NO_THROW(abstraction = abstractProgram.getAbstractAdd());
+
+ EXPECT_EQ(75, abstraction.getNodeCount());
+}
+
+TEST(PrismMenuGame, TwoDiceProgramAbstractionTest) {
+ storm::prism::Program program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/two_dice.nm");
+ program = program.substituteConstants();
+ program = program.flattenModules(std::make_unique<storm::utility::solver::MathsatSmtSolverFactory>());
+
+ std::vector<storm::expressions::Expression> initialPredicates;
+ storm::expressions::ExpressionManager& manager = program.getManager();
+
+ initialPredicates.push_back(manager.getVariableExpression("s1") < manager.integer(3));
+ initialPredicates.push_back(manager.getVariableExpression("s2") == manager.integer(0));
+
+ storm::prism::menu_games::AbstractProgram<storm::dd::DdType::CUDD, double> abstractProgram(program.getManager(), program, initialPredicates, std::make_unique<storm::utility::solver::MathsatSmtSolverFactory>(), false);
+
+ storm::dd::Add<storm::dd::DdType::CUDD> abstraction;
+ ASSERT_NO_THROW(abstraction = abstractProgram.getAbstractAdd());
+
+ EXPECT_EQ(38, abstraction.getNodeCount());
+}
+
+TEST(PrismMenuGame, TwoDiceProgramAbstractionAndRefinementTest) {
+ storm::prism::Program program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/two_dice.nm");
+ program = program.substituteConstants();
+ program = program.flattenModules(std::make_unique<storm::utility::solver::MathsatSmtSolverFactory>());
+
+ std::vector<storm::expressions::Expression> initialPredicates;
+ storm::expressions::ExpressionManager& manager = program.getManager();
+
+ initialPredicates.push_back(manager.getVariableExpression("s1") < manager.integer(3));
+ initialPredicates.push_back(manager.getVariableExpression("s2") == manager.integer(0));
+
+ storm::prism::menu_games::AbstractProgram<storm::dd::DdType::CUDD, double> abstractProgram(program.getManager(), program, initialPredicates, std::make_unique<storm::utility::solver::MathsatSmtSolverFactory>(), false);
+
+ storm::dd::Add<storm::dd::DdType::CUDD> abstraction;
+ ASSERT_NO_THROW(abstraction = abstractProgram.getAbstractAdd());
+
+ EXPECT_EQ(38, abstraction.getNodeCount());
+
+ ASSERT_NO_THROW(abstractProgram.refine({manager.getVariableExpression("d1") + manager.getVariableExpression("d2") == manager.integer(7)}));
+ ASSERT_NO_THROW(abstraction = abstractProgram.getAbstractAdd());
+
+ EXPECT_EQ(107, abstraction.getNodeCount());
+}
+
+TEST(PrismMenuGame, WlanProgramAbstractionTest) {
+ storm::prism::Program program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/wlan0-2-2.nm");
+ program = program.substituteConstants();
+ program = program.flattenModules(std::make_unique<storm::utility::solver::MathsatSmtSolverFactory>());
+
+ std::vector<storm::expressions::Expression> initialPredicates;
+ storm::expressions::ExpressionManager& manager = program.getManager();
+
+ initialPredicates.push_back(manager.getVariableExpression("s1") < manager.integer(5));
+ initialPredicates.push_back(manager.getVariableExpression("bc1") == manager.integer(0));
+ initialPredicates.push_back(manager.getVariableExpression("c1") == manager.getVariableExpression("c2"));
+
+ storm::prism::menu_games::AbstractProgram<storm::dd::DdType::CUDD, double> abstractProgram(program.getManager(), program, initialPredicates, std::make_unique<storm::utility::solver::MathsatSmtSolverFactory>(), false);
+
+ storm::dd::Add<storm::dd::DdType::CUDD> abstraction;
+ ASSERT_NO_THROW(abstraction = abstractProgram.getAbstractAdd());
+
+ EXPECT_EQ(219, abstraction.getNodeCount());
+}
+
+TEST(PrismMenuGame, WlanProgramAbstractionAndRefinementTest) {
+ storm::prism::Program program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/wlan0-2-2.nm");
+ program = program.substituteConstants();
+ program = program.flattenModules(std::make_unique<storm::utility::solver::MathsatSmtSolverFactory>());
+
+ std::vector<storm::expressions::Expression> initialPredicates;
+ storm::expressions::ExpressionManager& manager = program.getManager();
+
+ initialPredicates.push_back(manager.getVariableExpression("s1") < manager.integer(5));
+ initialPredicates.push_back(manager.getVariableExpression("bc1") == manager.integer(0));
+ initialPredicates.push_back(manager.getVariableExpression("c1") == manager.getVariableExpression("c2"));
+
+ storm::prism::menu_games::AbstractProgram<storm::dd::DdType::CUDD, double> abstractProgram(program.getManager(), program, initialPredicates, std::make_unique<storm::utility::solver::MathsatSmtSolverFactory>(), false);
+
+ storm::dd::Add<storm::dd::DdType::CUDD> abstraction;
+ ASSERT_NO_THROW(abstraction = abstractProgram.getAbstractAdd());
+
+ EXPECT_EQ(219, abstraction.getNodeCount());
+
+ ASSERT_NO_THROW(abstractProgram.refine({manager.getVariableExpression("backoff1") < manager.integer(7)}));
+ ASSERT_NO_THROW(abstraction = abstractProgram.getAbstractAdd());
+ EXPECT_EQ(292, abstraction.getNodeCount());
}
#endif
\ No newline at end of file