Storm 1.10.0.1
A Modern Probabilistic Model Checker
Loading...
Searching...
No Matches
MemoryIncorporation.cpp
Go to the documentation of this file.
2
16
18
21namespace storm {
22namespace transformer {
23
24template<class SparseModelType>
25storm::storage::MemoryStructure getGoalMemory(SparseModelType const& model, storm::logic::Formula const& propositionalGoalStateFormula) {
26 STORM_LOG_THROW(propositionalGoalStateFormula.isInFragment(storm::logic::propositional()), storm::exceptions::NotSupportedException,
27 "The subformula " << propositionalGoalStateFormula << " should be propositional.");
28
30 storm::storage::BitVector goalStates = mc.check(propositionalGoalStateFormula)->asExplicitQualitativeCheckResult().getTruthValuesVector();
31
32 // Check if the formula is already satisfied for all initial states. In such a case the trivial memory structure suffices.
33 if (model.getInitialStates().isSubsetOf(goalStates)) {
34 STORM_LOG_INFO("One objective is already satisfied for all initial states.");
35 return storm::storage::MemoryStructureBuilder<typename SparseModelType::ValueType,
36 typename SparseModelType::RewardModelType>::buildTrivialMemoryStructure(model);
37 }
38
39 // Create a memory structure that stores whether a goal state has already been reached
41 builder.setTransition(0, 0, ~goalStates);
42 builder.setTransition(0, 1, goalStates);
43 builder.setTransition(1, 1, storm::storage::BitVector(model.getNumberOfStates(), true));
44 for (auto initState : model.getInitialStates()) {
45 builder.setInitialMemoryState(initState, goalStates.get(initState) ? 1 : 0);
46 }
47 return builder.build();
48}
49
50template<class SparseModelType>
51storm::storage::MemoryStructure getUntilFormulaMemory(SparseModelType const& model, storm::logic::Formula const& leftSubFormula,
52 storm::logic::Formula const& rightSubFormula) {
53 auto notLeftOrRight = std::make_shared<storm::logic::BinaryBooleanStateFormula>(
54 storm::logic::BinaryBooleanStateFormula::OperatorType::Or,
55 std::make_shared<storm::logic::UnaryBooleanStateFormula>(storm::logic::UnaryBooleanStateFormula::OperatorType::Not, leftSubFormula.asSharedPointer()),
56 rightSubFormula.asSharedPointer());
57 return getGoalMemory<SparseModelType>(model, *notLeftOrRight);
58}
59
60template<class SparseModelType>
62 std::vector<std::shared_ptr<storm::logic::Formula const>> const& formulas) {
65 model);
66
67 for (auto const& subFormula : formulas) {
68 STORM_LOG_THROW(subFormula->isOperatorFormula(), storm::exceptions::NotSupportedException, "The given Formula " << *subFormula << " is not supported.");
69 auto const& subsubFormula = subFormula->asOperatorFormula().getSubformula();
70 if (subsubFormula.isEventuallyFormula()) {
71 memory = memory.product(getGoalMemory(model, subsubFormula.asEventuallyFormula().getSubformula()));
72 } else if (subsubFormula.isUntilFormula()) {
73 memory = memory.product(
74 getUntilFormulaMemory(model, subsubFormula.asUntilFormula().getLeftSubformula(), subsubFormula.asUntilFormula().getRightSubformula()));
75 } else if (subsubFormula.isBoundedUntilFormula()) {
76 // For bounded formulas it is only reasonable to add the goal memory if it considers a single upper step/time bound.
77 auto const& buf = subsubFormula.asBoundedUntilFormula();
78 if (!buf.isMultiDimensional() && !buf.getTimeBoundReference().isRewardBound() &&
79 (!buf.hasLowerBound() || (!buf.isLowerBoundStrict() && storm::utility::isZero(buf.template getLowerBound<storm::RationalNumber>())))) {
80 memory = memory.product(getUntilFormulaMemory(model, buf.getLeftSubformula(), buf.getRightSubformula()));
81 }
82 } else if (subsubFormula.isGloballyFormula()) {
83 auto notPhi = std::make_shared<storm::logic::UnaryBooleanStateFormula>(storm::logic::UnaryBooleanStateFormula::OperatorType::Not,
84 subsubFormula.asGloballyFormula().getSubformula().asSharedPointer());
85 memory = memory.product(getGoalMemory(model, *notPhi));
86 } else {
87 STORM_LOG_THROW(subFormula->isLongRunAverageOperatorFormula() || subsubFormula.isTotalRewardFormula() ||
88 subsubFormula.isCumulativeRewardFormula() || subsubFormula.isLongRunAverageRewardFormula(),
89 storm::exceptions::NotSupportedException, "The given Formula " << subsubFormula << " is not supported.");
90 }
91 }
92
93 return memory;
94}
95
96template<class SparseModelType>
98 SparseModelType const& model, std::vector<std::shared_ptr<storm::logic::Formula const>> const& formulas) {
99 auto memory = incorporateGoalMemoryHelper(model, formulas);
100 auto product = memory.product(model);
101 return product.build()->template as<SparseModelType>();
102}
103
104template<class SparseModelType>
105std::pair<std::shared_ptr<SparseModelType>, storm::storage::SparseModelMemoryProductReverseData>
107 std::vector<std::shared_ptr<storm::logic::Formula const>> const& formulas) {
108 auto memory = incorporateGoalMemoryHelper(model, formulas);
109 auto product = memory.product(model);
110 auto result = product.build();
111 return std::make_pair(result->template as<SparseModelType>(), product.computeReverseData());
112}
113
114template<class SparseModelType>
119
120template<class SparseModelType>
126
129
132
133} // namespace transformer
134} // namespace storm
bool isInFragment(FragmentSpecification const &fragment) const
Definition Formula.cpp:196
std::shared_ptr< Formula const > asSharedPointer()
Definition Formula.cpp:548
virtual std::unique_ptr< CheckResult > check(Environment const &env, CheckTask< storm::logic::Formula, SolutionType > const &checkTask)
Checks the provided formula.
A bit vector that is internally represented as a vector of 64-bit values.
Definition BitVector.h:16
bool get(uint64_t index) const
Retrieves the truth value of the bit at the given index and performs a bound check.
void setInitialMemoryState(uint_fast64_t initialModelState, uint_fast64_t initialMemoryState)
Specifies for the given state of the model the corresponding initial memory state.
MemoryStructure build()
Builds the memory structure.
static MemoryStructure buildTrivialMemoryStructure(storm::models::sparse::Model< ValueType, RewardModelType > const &model)
Builds a trivial memory structure for the given model (consisting of a single memory state)
void setTransition(uint_fast64_t const &startState, uint_fast64_t const &goalState, storm::storage::BitVector const &modelStates, boost::optional< storm::storage::BitVector > const &modelChoices=boost::none)
Specifies a transition of the memory structure.
This class represents a (deterministic) memory structure that can be used to encode certain events (s...
MemoryStructure product(MemoryStructure const &rhs) const
Builds the product of this memory structure and the given memory structure.
NondeterministicMemoryStructure build(NondeterministicMemoryStructurePattern pattern, uint64_t numStates) const
Data to restore memory incorporation applied with SparseModelMemoryProduct.
Incorporates Memory into the state space of the given model, that is the resulting model is the cross...
static std::shared_ptr< SparseModelType > incorporateFullMemory(SparseModelType const &model, uint64_t memoryStates)
Incorporates a memory structure where the nondeterminism of the model decides which successor state t...
static std::pair< std::shared_ptr< SparseModelType >, storm::storage::SparseModelMemoryProductReverseData > incorporateGoalMemoryWithReverseData(SparseModelType const &model, std::vector< std::shared_ptr< storm::logic::Formula const > > const &formulas)
Like incorporateGoalMemory, but also returns data necessary to translate results (in particular sched...
static std::shared_ptr< SparseModelType > incorporateGoalMemory(SparseModelType const &model, std::vector< std::shared_ptr< storm::logic::Formula const > > const &formulas)
Incorporates memory that stores whether a 'goal' state has already been reached.
static std::shared_ptr< SparseModelType > incorporateCountingMemory(SparseModelType const &model, uint64_t memoryStates)
Incorporates a memory structure where the nondeterminism of the model can increment a counter.
#define STORM_LOG_INFO(message)
Definition logging.h:24
#define STORM_LOG_THROW(cond, exception, message)
Definition macros.h:30
FragmentSpecification propositional()
storm::storage::MemoryStructure getGoalMemory(SparseModelType const &model, storm::logic::Formula const &propositionalGoalStateFormula)
storm::storage::MemoryStructure getUntilFormulaMemory(SparseModelType const &model, storm::logic::Formula const &leftSubFormula, storm::logic::Formula const &rightSubFormula)
storm::storage::MemoryStructure incorporateGoalMemoryHelper(SparseModelType const &model, std::vector< std::shared_ptr< storm::logic::Formula const > > const &formulas)
bool isZero(ValueType const &a)
Definition constants.cpp:41
LabParser.cpp.