Storm 1.11.1.1
A Modern Probabilistic Model Checker
Loading...
Searching...
No Matches
dd.cpp
Go to the documentation of this file.
1#include "storm/utility/dd.h"
2
3#include "storm/adapters/RationalFunctionAdapter.h"
4#include "storm/storage/dd/Add.h"
5#include "storm/storage/dd/Bdd.h"
6#include "storm/storage/dd/DdManager.h"
7
8namespace storm {
9namespace utility {
10namespace dd {
11
12template<storm::dd::DdType Type>
13std::pair<storm::dd::Bdd<Type>, uint64_t> computeReachableStates(storm::dd::Bdd<Type> const& initialStates, storm::dd::Bdd<Type> const& transitions,
14 std::set<storm::expressions::Variable> const& rowMetaVariables,
15 std::set<storm::expressions::Variable> const& columnMetaVariables) {
16 STORM_LOG_TRACE("Computing reachable states: transition matrix BDD has " << transitions.getNodeCount() << " node(s) and " << transitions.getNonZeroCount()
17 << " non-zero(s), " << initialStates.getNonZeroCount() << " initial states).");
18
19 auto start = std::chrono::high_resolution_clock::now();
20 storm::dd::Bdd<Type> reachableStates = initialStates;
21
22 // Perform the BFS to discover all reachable states.
23 bool changed = true;
24 uint_fast64_t iteration = 0;
25 do {
26 changed = false;
27 storm::dd::Bdd<Type> tmp = reachableStates.relationalProduct(transitions, rowMetaVariables, columnMetaVariables);
28 storm::dd::Bdd<Type> newReachableStates = tmp && (!reachableStates);
29
30 // Check whether new states were indeed discovered.
31 if (!newReachableStates.isZero()) {
32 changed = true;
33 }
34
35 reachableStates |= newReachableStates;
36
37 ++iteration;
38 STORM_LOG_TRACE("Iteration " << iteration << " of reachability computation completed: " << reachableStates.getNonZeroCount()
39 << " reachable states found.");
40 } while (changed);
41
42 auto end = std::chrono::high_resolution_clock::now();
43 STORM_LOG_TRACE("Reachability computation completed in " << iteration << " iterations ("
44 << std::chrono::duration_cast<std::chrono::milliseconds>(end - start).count() << "ms).");
45
46 return {reachableStates, iteration};
47}
48
49template<storm::dd::DdType Type>
50storm::dd::Bdd<Type> computeBackwardsReachableStates(storm::dd::Bdd<Type> const& initialStates, storm::dd::Bdd<Type> const& constraintStates,
51 storm::dd::Bdd<Type> const& transitions, std::set<storm::expressions::Variable> const& rowMetaVariables,
52 std::set<storm::expressions::Variable> const& columnMetaVariables) {
53 STORM_LOG_TRACE("Computing backwards reachable states: transition matrix BDD has "
54 << transitions.getNodeCount() << " node(s) and " << transitions.getNonZeroCount() << " non-zero(s), " << initialStates.getNonZeroCount()
55 << " initial states).");
56
57 auto start = std::chrono::high_resolution_clock::now();
58 storm::dd::Bdd<Type> reachableStates = initialStates;
59
60 // Perform the BFS to discover all reachable states.
61 bool changed = true;
62 uint_fast64_t iteration = 0;
63 do {
64 changed = false;
65 storm::dd::Bdd<Type> tmp = reachableStates.inverseRelationalProduct(transitions, rowMetaVariables, columnMetaVariables);
66 storm::dd::Bdd<Type> newReachableStates = tmp && (!reachableStates) && constraintStates;
67
68 // Check whether new states were indeed discovered.
69 if (!newReachableStates.isZero()) {
70 changed = true;
71 }
72
73 reachableStates |= newReachableStates;
74
75 ++iteration;
76 STORM_LOG_TRACE("Iteration " << iteration << " of (backward) reachability computation completed: " << reachableStates.getNonZeroCount()
77 << " reachable states found.");
78 } while (changed);
79
80 auto end = std::chrono::high_resolution_clock::now();
81 STORM_LOG_TRACE("Backward reachability computation completed in " << iteration << " iterations ("
82 << std::chrono::duration_cast<std::chrono::milliseconds>(end - start).count() << "ms).");
83
84 return reachableStates;
85}
86
87template<storm::dd::DdType Type>
88storm::dd::Bdd<Type> getRowColumnDiagonal(
89 storm::dd::DdManager<Type> const& ddManager,
90 std::vector<std::pair<storm::expressions::Variable, storm::expressions::Variable>> const& rowColumnMetaVariablePairs) {
91 return ddManager.getIdentity(rowColumnMetaVariablePairs, false);
92}
93
94template std::pair<storm::dd::Bdd<storm::dd::DdType::CUDD>, uint64_t> computeReachableStates(storm::dd::Bdd<storm::dd::DdType::CUDD> const& initialStates,
95 storm::dd::Bdd<storm::dd::DdType::CUDD> const& transitions,
96 std::set<storm::expressions::Variable> const& rowMetaVariables,
97 std::set<storm::expressions::Variable> const& columnMetaVariables);
98template std::pair<storm::dd::Bdd<storm::dd::DdType::Sylvan>, uint64_t> computeReachableStates(
99 storm::dd::Bdd<storm::dd::DdType::Sylvan> const& initialStates, storm::dd::Bdd<storm::dd::DdType::Sylvan> const& transitions,
100 std::set<storm::expressions::Variable> const& rowMetaVariables, std::set<storm::expressions::Variable> const& columnMetaVariables);
101
102template storm::dd::Bdd<storm::dd::DdType::CUDD> computeBackwardsReachableStates(storm::dd::Bdd<storm::dd::DdType::CUDD> const& initialStates,
103 storm::dd::Bdd<storm::dd::DdType::CUDD> const& constraintStates,
104 storm::dd::Bdd<storm::dd::DdType::CUDD> const& transitions,
105 std::set<storm::expressions::Variable> const& rowMetaVariables,
106 std::set<storm::expressions::Variable> const& columnMetaVariables);
107template storm::dd::Bdd<storm::dd::DdType::Sylvan> computeBackwardsReachableStates(storm::dd::Bdd<storm::dd::DdType::Sylvan> const& initialStates,
108 storm::dd::Bdd<storm::dd::DdType::Sylvan> const& constraintStates,
109 storm::dd::Bdd<storm::dd::DdType::Sylvan> const& transitions,
110 std::set<storm::expressions::Variable> const& rowMetaVariables,
111 std::set<storm::expressions::Variable> const& columnMetaVariables);
112
113template storm::dd::Bdd<storm::dd::DdType::CUDD> getRowColumnDiagonal(
114 storm::dd::DdManager<storm::dd::DdType::CUDD> const& ddManager,
115 std::vector<std::pair<storm::expressions::Variable, storm::expressions::Variable>> const& rowColumnMetaVariablePairs);
116template storm::dd::Bdd<storm::dd::DdType::Sylvan> getRowColumnDiagonal(
117 storm::dd::DdManager<storm::dd::DdType::Sylvan> const& ddManager,
118 std::vector<std::pair<storm::expressions::Variable, storm::expressions::Variable>> const& rowColumnMetaVariablePairs);
119
120} // namespace dd
121} // namespace utility
122} // namespace storm
storm::dd::Bdd::inverseRelationalProduct
Bdd< LibraryType > inverseRelationalProduct(Bdd< LibraryType > const &relation, std::set< storm::expressions::Variable > const &rowMetaVariables, std::set< storm::expressions::Variable > const &columnMetaVariables) const
Computes the inverse relational product of the current BDD and the given BDD representing a relation.
Definition Bdd.cpp:240
storm::dd::Bdd::isZero
bool isZero() const
Retrieves whether this DD represents the constant zero function.
Definition Bdd.cpp:541
storm::dd::Bdd::getNonZeroCount
virtual uint_fast64_t getNonZeroCount() const override
Retrieves the number of encodings that are mapped to a non-zero value.
Definition Bdd.cpp:507
storm::dd::Bdd::getNodeCount
virtual uint_fast64_t getNodeCount() const override
Retrieves the number of nodes necessary to represent the DD.
Definition Bdd.cpp:521
storm::dd::Bdd::relationalProduct
Bdd< LibraryType > relationalProduct(Bdd< LibraryType > const &relation, std::set< storm::expressions::Variable > const &rowMetaVariables, std::set< storm::expressions::Variable > const &columnMetaVariables) const
Computes the relational product of the current BDD and the given BDD representing a relation.
Definition Bdd.cpp:214
storm::dd::DdManager::getIdentity
Add< LibraryType, ValueType > getIdentity(storm::expressions::Variable const &variable) const
Retrieves the ADD representing the identity of the meta variable, i.e., a function that maps all lega...
Definition DdManager.cpp:136
STORM_LOG_TRACE
#define STORM_LOG_TRACE(message)
Definition logging.h:12
storm::utility::dd::computeBackwardsReachableStates
storm::dd::Bdd< Type > computeBackwardsReachableStates(storm::dd::Bdd< Type > const &initialStates, storm::dd::Bdd< Type > const &constraintStates, storm::dd::Bdd< Type > const &transitions, std::set< storm::expressions::Variable > const &rowMetaVariables, std::set< storm::expressions::Variable > const &columnMetaVariables)
Definition dd.cpp:50
storm::utility::dd::computeReachableStates
std::pair< storm::dd::Bdd< Type >, uint64_t > computeReachableStates(storm::dd::Bdd< Type > const &initialStates, storm::dd::Bdd< Type > const &transitions, std::set< storm::expressions::Variable > const &rowMetaVariables, std::set< storm::expressions::Variable > const &columnMetaVariables)
Definition dd.cpp:13
storm::utility::dd::getRowColumnDiagonal
storm::dd::Bdd< Type > getRowColumnDiagonal(storm::dd::DdManager< Type > const &ddManager, std::vector< std::pair< storm::expressions::Variable, storm::expressions::Variable > > const &rowColumnMetaVariablePairs)
Definition dd.cpp:88