diff --git a/src/formula/Formulas.h b/src/formula/Formulas.h index 89e3da422..d2b4e98da 100644 --- a/src/formula/Formulas.h +++ b/src/formula/Formulas.h @@ -32,6 +32,7 @@ #include "RewardNoBoundOperator.h" #include "SteadyStateReward.h" +#include "SteadyStateNoBoundOperator.h" #include "SteadyStateBoundOperator.h" #include "AbstractFormula.h" diff --git a/src/formula/PathNoBoundOperator.h b/src/formula/PathNoBoundOperator.h index 9c3668a23..f562ecc91 100644 --- a/src/formula/PathNoBoundOperator.h +++ b/src/formula/PathNoBoundOperator.h @@ -22,7 +22,7 @@ namespace formula { template class PathNoBoundOperator; /*! - * @brief Interface class for model checkers that support NoBoundOperator. + * @brief Interface class for model checkers that support PathNoBoundOperator. * * All model checkers that support the formula class NoBoundOperator must inherit * this pure virtual class. diff --git a/src/formula/StateNoBoundOperator.h b/src/formula/StateNoBoundOperator.h new file mode 100644 index 000000000..853e1e0d3 --- /dev/null +++ b/src/formula/StateNoBoundOperator.h @@ -0,0 +1,148 @@ +/* + * StateNoBoundOperator.h + * + * Created on: 09.04.2013 + * Author: thomas + */ + +#ifndef STATENOBOUNDOPERATOR_H_ +#define STATENOBOUNDOPERATOR_H_ + +#include "src/formula/AbstractFormula.h" +#include "src/formula/AbstractPathFormula.h" +#include "src/formula/AbstractFormulaChecker.h" + +#include "src/modelchecker/ForwardDeclarations.h" + +namespace storm { +namespace formula { + +template class StateNoBoundOperator; + +/*! + * @brief Interface class for model checkers that support PathNoBoundOperator. + * + * All model checkers that support the formula class NoBoundOperator must inherit + * this pure virtual class. + */ +template +class IStateNoBoundOperatorModelChecker { + public: + /*! + * @brief Evaluates NoBoundOperator formula within a model checker. + * + * @param obj Formula object with subformulas. + * @return Result of the formula for every node. + */ + virtual std::vector* checkStateNoBoundOperator(const StateNoBoundOperator& obj) const = 0; +}; + + +/*! + * @brief + * Class for a Abstract formula tree with an operator without declaration of probabilities + * as root. + * + * Checking a formula with this operator as root returns the probabilities that the path formula holds + * (for each state) + * + * Has one Abstract state formula as sub formula/tree. + * + * @note + * This class is a hybrid of a state and path formula, and may only appear as the outermost operator. + * Hence, it is seen as neither a state nor a path formula, but is directly derived from AbstractFormula. + * + * @note + * This class does not contain a check() method like the other formula classes. + * The check method should only be called by the model checker to infer the correct check function for sub + * formulas. As this operator can only appear at the root, the method is not useful here. + * Use the checkProbabilisticNoBoundOperator method from the DtmcPrctlModelChecker class instead. + * + * The subtree is seen as part of the object and deleted with it + * (this behavior can be prevented by setting them to NULL before deletion) + * + * + * @see AbstractStateFormula + * @see AbstractPathFormula + * @see SteadyStateNoBoundOperator + * @see AbstractFormula + */ +template +class StateNoBoundOperator: public storm::formula::AbstractFormula { +public: + /*! + * Empty constructor + */ + StateNoBoundOperator() { + stateFormula = nullptr; + } + + /*! + * Constructor + */ + StateNoBoundOperator(AbstractStateFormula* stateFormula) { + this->stateFormula = stateFormula; + } + + /*! + * Destructor + * + * Deletes the subtree + */ + virtual ~StateNoBoundOperator() { + if (stateFormula != nullptr) { + delete stateFormula; + } + } + + const AbstractStateFormula& getStateFormula() { + return *stateFormula; + } + + void setStateFormula(AbstractStateFormula* stateFormula) { + this->stateFormula = stateFormula; + } + + /*! + * Calls the model checker to check this formula. + * Needed to infer the correct type of formula class. + * + * @note This function should only be called in a generic check function of a model checker class. For other uses, + * the methods of the model checker should be used. + * + * @note This function is not implemented in this class. + * + * @returns A vector indicating all states that satisfy the formula represented by the called object. + */ + virtual std::vector* check(const storm::modelchecker::AbstractModelChecker& modelChecker) const { + return modelChecker.template as()->checkStateNoBoundOperator(*this); + } + + /*! + * @returns a string representation of the formula + */ + virtual std::string toString() const { + std::string result; + result += " = ? ["; + result += this->getStateFormula().toString(); + result += "]"; + return result; + } + + /*! + * @brief Checks if the subtree conforms to some logic. + * + * @param checker Formula checker object. + * @return true iff the subtree conforms to some logic. + */ + virtual bool conforms(const AbstractFormulaChecker& checker) const { + return checker.conforms(this->stateFormula); + } + +private: + AbstractStateFormula* stateFormula; +}; + +} /* namespace formula */ +} /* namespace storm */ +#endif /* STATENOBOUNDOPERATOR_H_ */ diff --git a/src/formula/SteadyStateBoundOperator.h b/src/formula/SteadyStateBoundOperator.h index a341e316e..2f5baaab3 100644 --- a/src/formula/SteadyStateBoundOperator.h +++ b/src/formula/SteadyStateBoundOperator.h @@ -108,7 +108,7 @@ public: * @returns A vector indicating the probability that the formula holds for each state. */ virtual storm::storage::BitVector* check(const storm::modelchecker::AbstractModelChecker& modelChecker) const { - return modelChecker.template as()->checkSteadyStateOperator(*this); + return modelChecker.template as()->checkSteadyStateBoundOperator(*this); } }; diff --git a/src/formula/SteadyStateNoBoundOperator.h b/src/formula/SteadyStateNoBoundOperator.h new file mode 100644 index 000000000..2297ebfcd --- /dev/null +++ b/src/formula/SteadyStateNoBoundOperator.h @@ -0,0 +1,97 @@ +/* + * SteadyStateNoBoundOperator.h + * + * Created on: 09.04.2013 + * Author: thomas + */ + +#ifndef STEADYSTATENOBOUNDOPERATOR_H_ +#define STEADYSTATENOBOUNDOPERATOR_H_ + +#include "StateNoBoundOperator.h" + +namespace storm { +namespace formula { + +template class SteadyStateNoBoundOperator; + +/*! + * @brief Interface class for model checkers that support SteadyStateOperator. + * + * All model checkers that support the formula class SteadyStateOperator must inherit + * this pure virtual class. + */ +template +class ISteadyStateNoBoundOperatorModelChecker { + public: + /*! + * @brief Evaluates SteadyStateOperator formula within a model checker. + * + * @param obj Formula object with subformulas. + * @return Result of the formula for every node. + */ + virtual storm::storage::BitVector* checkSteadyStateNoBoundOperator(const SteadyStateNoBoundOperator& obj) const = 0; +}; + +template +class SteadyStateNoBoundOperator: public storm::formula::StateNoBoundOperator { +public: + /*! + * Empty constructor + */ + SteadyStateNoBoundOperator() : StateNoBoundOperator() { + // Intentionally left empty + + } + + /*! + * Constructor + * + * @param stateFormula The state formula that forms the subtree + */ + SteadyStateNoBoundOperator(AbstractStateFormula* stateFormula) : StateNoBoundOperator(stateFormula) { + // Intentionally left empty + } + + /*! + * @returns a string representation of the formula + */ + virtual std::string toString() const { + std::string result = "("; + result += " S "; + result += StateNoBoundOperator::toString(); + result += ")"; + return result; + } + + /*! + * Clones the called object. + * + * Performs a "deep copy", i.e. the subtrees of the new object are clones of the original ones + * + * @returns a new BoundedUntil-object that is identical the called object. + */ + virtual AbstractStateFormula* clone() const { + SteadyStateNoBoundOperator* result = new SteadyStateNoBoundOperator(); + result->setStateFormula(this->getStateFormula().clone()); + return result; + } + + /*! + * Calls the model checker to check this formula. + * Needed to infer the correct type of formula class. + * + * @note This function should only be called in a generic check function of a model checker class. For other uses, + * the methods of the model checker should be used. + * + * @returns A vector indicating the probability that the formula holds for each state. + */ + virtual storm::storage::BitVector* check(const storm::modelchecker::AbstractModelChecker& modelChecker) const { + return modelChecker.template as()->checkSteadyStateNoBoundOperator(*this); + } + +}; + +} /* namespace formula */ +} /* namespace storm */ +#endif /* STEADYSTATENOBOUNDOPERATOR_H_ */