Storm 1.10.0.1
A Modern Probabilistic Model Checker
Loading...
Searching...
No Matches
StateSetAbstractor.h
Go to the documentation of this file.
1#pragma once
2
3#include <boost/optional.hpp>
4#include <memory>
5#include <set>
6
8
11
13
14namespace storm {
15namespace utility {
16namespace solver {
17class SmtSolverFactory;
18}
19} // namespace utility
20
21namespace dd {
22template<storm::dd::DdType DdType>
23class Bdd;
24
25template<storm::dd::DdType DdType, typename ValueType>
26class Add;
27} // namespace dd
28} // namespace storm
29
30namespace storm::gbar {
31namespace abstraction {
32template<storm::dd::DdType DdType>
33class AbstractionInformation;
34
35template<storm::dd::DdType DdType, typename ValueType>
37 public:
38 StateSetAbstractor(StateSetAbstractor const& other) = default;
40
43
52 StateSetAbstractor(AbstractionInformation<DdType>& abstractionInformation, std::vector<storm::expressions::Expression> const& statePredicates,
53 std::shared_ptr<storm::utility::solver::SmtSolverFactory> const& smtSolverFactory =
54 std::make_shared<storm::utility::solver::MathsatSmtSolverFactory>());
55
61 void refine(std::vector<uint_fast64_t> const& newPredicateIndices);
62
69 void constrain(storm::expressions::Expression const& constraint);
70
76 void constrain(storm::dd::Bdd<DdType> const& newConstraint);
77
84
85 private:
91 void addMissingPredicates(std::set<uint_fast64_t> const& newRelevantPredicateIndices);
92
96 void pushConstraintBdd();
97
101 void popConstraintBdd();
102
106 void recomputeCachedBdd();
107
115
121 AbstractionInformation<DdType>& getAbstractionInformation();
122
128 AbstractionInformation<DdType> const& getAbstractionInformation() const;
129
130 // The SMT solver used for abstracting the set of states.
131 std::unique_ptr<storm::solver::SmtSolver> smtSolver;
132
133 // The abstraction-related information.
134 std::reference_wrapper<AbstractionInformation<DdType>> abstractionInformation;
135
136 // The local expression-related information.
137 LocalExpressionInformation<DdType> localExpressionInformation;
138
139 // The set of relevant predicates and the corresponding decision variables.
140 std::vector<std::pair<storm::expressions::Variable, uint_fast64_t>> relevantPredicatesAndVariables;
141
142 // The set of all variables appearing in the concrete predicates.
143 std::set<storm::expressions::Variable> concretePredicateVariables;
144
145 // The set of all decision variables over which to perform the all-sat enumeration.
146 std::vector<storm::expressions::Variable> decisionVariables;
147
148 // A flag indicating whether the cached BDD needs recomputation.
149 bool forceRecomputation;
150
151 // The cached BDD representing the abstraction. This variable is written to in refinement steps (if work
152 // needed to be done).
153 storm::dd::Bdd<DdType> cachedBdd;
154
155 // This BDD currently constrains the search for solutions.
156 storm::dd::Bdd<DdType> constraint;
157};
158} // namespace abstraction
159} // namespace storm::gbar
void constrain(storm::expressions::Expression const &constraint)
Constrains the abstract states with the given expression.
StateSetAbstractor & operator=(StateSetAbstractor &&other)=default
void refine(std::vector< uint_fast64_t > const &newPredicateIndices)
Refines the abstractor by making the given predicates new abstract predicates.
storm::dd::Bdd< DdType > getAbstractStates()
Retrieves the set of abstract states matching all predicates added to this abstractor.
StateSetAbstractor(StateSetAbstractor &&other)=default
StateSetAbstractor & operator=(StateSetAbstractor const &other)=default
StateSetAbstractor(StateSetAbstractor const &other)=default
The base class for all model references.
Definition SmtSolver.h:31
SFTBDDChecker::Bdd Bdd
LabParser.cpp.