Storm
A Modern Probabilistic Model Checker
All Classes Namespaces Files Functions Variables Typedefs Enumerations Enumerator Friends Macros Pages
ValidBlockAbstractor.cpp
Go to the documentation of this file.
2
4
6
9
10namespace storm::gbar {
11namespace abstraction {
12
13template<storm::dd::DdType DdType>
15 std::shared_ptr<storm::utility::solver::SmtSolverFactory> const& smtSolverFactory)
16 : abstractionInformation(abstractionInformation),
17 localExpressionInformation(abstractionInformation),
18 validBlocks(abstractionInformation.getDdManager().getBddOne()),
19 checkForRecomputation(false) {
20 uint64_t numberOfBlocks = localExpressionInformation.getNumberOfBlocks();
21 validBlocksForPredicateBlocks.resize(numberOfBlocks, abstractionInformation.getDdManager().getBddOne());
22 relevantVariablesAndPredicates.resize(numberOfBlocks);
23 decisionVariables.resize(numberOfBlocks);
24
25 for (uint64_t i = 0; i < numberOfBlocks; ++i) {
26 smtSolvers.emplace_back(smtSolverFactory->create(abstractionInformation.getExpressionManager()));
27 for (auto const& constraint : abstractionInformation.getConstraints()) {
28 smtSolvers.back()->add(constraint);
29 }
30 }
31}
32
33template<storm::dd::DdType DdType>
35 if (checkForRecomputation) {
36 recomputeValidBlocks();
37 }
38
39 return validBlocks;
40}
41
42template<storm::dd::DdType DdType>
44 for (uint64_t i = 0; i < smtSolvers.size(); ++i) {
45 smtSolvers[i]->add(constraint);
46 }
47}
48
49template<storm::dd::DdType DdType>
50void ValidBlockAbstractor<DdType>::refine(std::vector<uint64_t> const& predicates) {
51 for (auto const& predicate : predicates) {
52 std::map<uint64_t, uint64_t> mergeInformation = localExpressionInformation.addExpression(predicate);
53
54 // Perform the remapping caused by merges.
55 for (auto const& blockRemapping : mergeInformation) {
56 if (blockRemapping.first == blockRemapping.second) {
57 continue;
58 }
59
60 validBlocksForPredicateBlocks[blockRemapping.second] = validBlocksForPredicateBlocks[blockRemapping.first];
61 smtSolvers[blockRemapping.second] = std::move(smtSolvers[blockRemapping.first]);
62 relevantVariablesAndPredicates[blockRemapping.second] = std::move(relevantVariablesAndPredicates[blockRemapping.first]);
63 decisionVariables[blockRemapping.second] = std::move(decisionVariables[blockRemapping.first]);
64 }
65 validBlocksForPredicateBlocks.resize(localExpressionInformation.getNumberOfBlocks());
66 smtSolvers.resize(localExpressionInformation.getNumberOfBlocks());
67 relevantVariablesAndPredicates.resize(localExpressionInformation.getNumberOfBlocks());
68 decisionVariables.resize(localExpressionInformation.getNumberOfBlocks());
69 }
70 checkForRecomputation = true;
71}
72
73template<storm::dd::DdType DdType>
75 storm::dd::Bdd<DdType> newValidBlocks = abstractionInformation.get().getDdManager().getBddOne();
76
77 for (uint64_t blockIndex = 0; blockIndex < localExpressionInformation.getNumberOfBlocks(); ++blockIndex) {
78 std::set<uint64_t> const& predicateBlock = localExpressionInformation.getExpressionBlock(blockIndex);
79
80 // If the size of the block changed, we need to add the appropriate variables and recompute the solution.
81 if (relevantVariablesAndPredicates[blockIndex].size() < predicateBlock.size()) {
82 recomputeValidBlocksForPredicateBlock(blockIndex);
83 }
84
85 newValidBlocks &= validBlocksForPredicateBlocks[blockIndex];
86 }
87
88 validBlocks = newValidBlocks;
89}
90
91template<storm::dd::DdType DdType>
92void ValidBlockAbstractor<DdType>::recomputeValidBlocksForPredicateBlock(uint64_t blockIndex) {
93 std::set<uint64_t> const& predicateBlock = localExpressionInformation.getExpressionBlock(blockIndex);
94 std::vector<std::pair<storm::expressions::Variable, uint_fast64_t>> newVariables =
95 this->getAbstractionInformation().declareNewVariables(relevantVariablesAndPredicates[blockIndex], predicateBlock);
96 for (auto const& element : newVariables) {
97 smtSolvers[blockIndex]->add(storm::expressions::iff(element.first, this->getAbstractionInformation().getPredicateByIndex(element.second)));
98 decisionVariables[blockIndex].push_back(element.first);
99 }
100
101 relevantVariablesAndPredicates[blockIndex].insert(relevantVariablesAndPredicates[blockIndex].end(), newVariables.begin(), newVariables.end());
102 std::sort(relevantVariablesAndPredicates[blockIndex].begin(), relevantVariablesAndPredicates[blockIndex].end(),
103 [](std::pair<storm::expressions::Variable, uint_fast64_t> const& first, std::pair<storm::expressions::Variable, uint_fast64_t> const& second) {
104 return first.second < second.second;
105 });
106
107 // Use all-sat to enumerate all valid blocks for this predicate block.
108 storm::dd::Bdd<DdType> result = this->getAbstractionInformation().getDdManager().getBddZero();
109 uint64_t numberOfSolutions = 0;
110 smtSolvers[blockIndex]->allSat(decisionVariables[blockIndex],
111 [&result, this, &numberOfSolutions, blockIndex](storm::solver::SmtSolver::ModelReference const& model) {
112 result |= getSourceStateBdd(model, blockIndex);
113 ++numberOfSolutions;
114 return true;
115 });
116
117 STORM_LOG_TRACE("Computed valid blocks for predicate block " << blockIndex << " (" << numberOfSolutions << " solutions enumerated).");
118
119 validBlocksForPredicateBlocks[blockIndex] = result;
120}
121
122template<storm::dd::DdType DdType>
123AbstractionInformation<DdType> const& ValidBlockAbstractor<DdType>::getAbstractionInformation() const {
124 return abstractionInformation.get();
125}
126
127template<storm::dd::DdType DdType>
128storm::dd::Bdd<DdType> ValidBlockAbstractor<DdType>::getSourceStateBdd(storm::solver::SmtSolver::ModelReference const& model, uint64_t blockIndex) const {
129 storm::dd::Bdd<DdType> result = this->getAbstractionInformation().getDdManager().getBddOne();
130 for (auto variableIndexPairIt = relevantVariablesAndPredicates[blockIndex].rbegin(),
131 variableIndexPairIte = relevantVariablesAndPredicates[blockIndex].rend();
132 variableIndexPairIt != variableIndexPairIte; ++variableIndexPairIt) {
133 auto const& variableIndexPair = *variableIndexPairIt;
134 if (model.getBooleanValue(variableIndexPair.first)) {
135 result &= this->getAbstractionInformation().encodePredicateAsSource(variableIndexPair.second);
136 } else {
137 result &= !this->getAbstractionInformation().encodePredicateAsSource(variableIndexPair.second);
138 }
139 }
140
141 STORM_LOG_ASSERT(!result.isZero(), "Source must not be empty.");
142 return result;
143}
144
145template class ValidBlockAbstractor<storm::dd::DdType::CUDD>;
146template class ValidBlockAbstractor<storm::dd::DdType::Sylvan>;
147
148} // namespace abstraction
149} // namespace storm::gbar
bool isZero() const
Retrieves whether this DD represents the constant zero function.
Definition Bdd.cpp:547
DdManager< LibraryType > & getDdManager() const
Retrieves the manager that is responsible for this DD.
Definition Dd.cpp:39
Bdd< LibraryType > getBddOne() const
Retrieves a BDD representing the constant one function.
Definition DdManager.cpp:36
std::vector< storm::expressions::Expression > const & getConstraints() const
Retrieves a list of expressions that constrain the valid variable values.
storm::expressions::ExpressionManager & getExpressionManager()
Retrieves the expression manager.
storm::dd::DdManager< DdType > & getDdManager()
Retrieves the DD manager.
storm::dd::Bdd< DdType > const & getValidBlocks()
void refine(std::vector< uint64_t > const &predicates)
void constrain(storm::expressions::Expression const &constraint)
ValidBlockAbstractor(AbstractionInformation< DdType > &abstractionInformation, std::shared_ptr< storm::utility::solver::SmtSolverFactory > const &smtSolverFactory)
The base class for all model references.
Definition SmtSolver.h:31
virtual bool getBooleanValue(storm::expressions::Variable const &variable) const =0
#define STORM_LOG_TRACE(message)
Definition logging.h:17
#define STORM_LOG_ASSERT(cond, message)
Definition macros.h:11
Expression iff(Expression const &first, Expression const &second)