22namespace transformer {
24template<
class SparseModelType>
27 "The subformula " << propositionalGoalStateFormula <<
" should be propositional.");
33 if (model.getInitialStates().isSubsetOf(goalStates)) {
34 STORM_LOG_INFO(
"One objective is already satisfied for all initial states.");
36 typename SparseModelType::RewardModelType>::buildTrivialMemoryStructure(model);
44 for (
auto initState : model.getInitialStates()) {
47 return builder.
build();
50template<
class SparseModelType>
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()),
57 return getGoalMemory<SparseModelType>(model, *notLeftOrRight);
60template<
class SparseModelType>
62 std::vector<std::shared_ptr<storm::logic::Formula const>>
const& formulas) {
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()) {
74 getUntilFormulaMemory(model, subsubFormula.asUntilFormula().getLeftSubformula(), subsubFormula.asUntilFormula().getRightSubformula()));
75 }
else if (subsubFormula.isBoundedUntilFormula()) {
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>())))) {
82 }
else if (subsubFormula.isGloballyFormula()) {
83 auto notPhi = std::make_shared<storm::logic::UnaryBooleanStateFormula>(storm::logic::UnaryBooleanStateFormula::OperatorType::Not,
84 subsubFormula.asGloballyFormula().getSubformula().asSharedPointer());
87 STORM_LOG_THROW(subFormula->isLongRunAverageOperatorFormula() || subsubFormula.isTotalRewardFormula() ||
88 subsubFormula.isCumulativeRewardFormula() || subsubFormula.isLongRunAverageRewardFormula(),
89 storm::exceptions::NotSupportedException,
"The given Formula " << subsubFormula <<
" is not supported.");
96template<
class SparseModelType>
98 SparseModelType
const& model, std::vector<std::shared_ptr<storm::logic::Formula const>>
const& formulas) {
100 auto product = memory.product(model);
101 return product.build()->template as<SparseModelType>();
104template<
class SparseModelType>
107 std::vector<std::shared_ptr<storm::logic::Formula const>>
const& formulas) {
109 auto product = memory.product(model);
110 auto result = product.build();
111 return std::make_pair(result->template as<SparseModelType>(), product.computeReverseData());
114template<
class SparseModelType>
120template<
class SparseModelType>
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.
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.
std::shared_ptr< SparseModelType > build() const
#define STORM_LOG_INFO(message)
#define STORM_LOG_THROW(cond, exception, message)
FragmentSpecification propositional()
bool isZero(ValueType const &a)