diff --git a/src/exceptions/InvalidPropertyException.h b/src/exceptions/InvalidPropertyException.h new file mode 100644 index 000000000..6cddb9d91 --- /dev/null +++ b/src/exceptions/InvalidPropertyException.h @@ -0,0 +1,26 @@ +/* + * InvalidPropertyException.h + * + * Created on: 27.12.2012 + * Author: Christian Dehnert + */ + +#ifndef STORM_EXCEPTIONS_INVALIDPROPERTYEXCEPTION_H_ +#define STORM_EXCEPTIONS_INVALIDPROPERTYEXCEPTION_H_ + +#include "src/exceptions/BaseException.h" + +namespace storm { + +namespace exceptions { + +/*! + * @brief This exception is thrown when a parameter is invalid in this context + */ +STORM_EXCEPTION_DEFINE_NEW(InvalidPropertyException) + +} // namespace exceptions + +} // namespace storm + +#endif /* STORM_EXCEPTIONS_INVALIDPROPERTYEXCEPTION_H_ */ diff --git a/src/formula/BoundedEventually.h b/src/formula/BoundedEventually.h new file mode 100644 index 000000000..58973456d --- /dev/null +++ b/src/formula/BoundedEventually.h @@ -0,0 +1,151 @@ +/* + * BoundedUntil.h + * + * Created on: 27.11.2012 + * Author: Christian Dehnert + */ + +#ifndef STORM_FORMULA_BOUNDEDEVENTUALLY_H_ +#define STORM_FORMULA_BOUNDEDEVENTUALLY_H_ + +#include "PctlPathFormula.h" +#include "PctlStateFormula.h" +#include "boost/integer/integer_mask.hpp" +#include + +namespace storm { + +namespace formula { + +/*! + * @brief + * Class for a PCTL (path) formula tree with a BoundedEventually node as root. + * + * Has one PCTL state formulas as sub formula/tree. + * + * @par Semantics + * The formula holds iff in at most \e bound steps, formula \e child holds. + * + * The subtrees are seen as part of the object and deleted with the object + * (this behavior can be prevented by setting them to NULL before deletion) + * + * @see PctlPathFormula + * @see PctlFormula + */ +template +class BoundedEventually : public PctlPathFormula { + +public: + /*! + * Empty constructor + */ + BoundedEventually() { + this->child = nullptr; + bound = 0; + } + + /*! + * Constructor + * + * @param child The child formula subtree + * @param bound The maximal number of steps + */ + BoundedEventually(PctlStateFormula* child, uint_fast64_t bound) { + this->child = child; + this->bound = bound; + } + + /*! + * Destructor. + * + * Also deletes the subtrees. + * (this behaviour can be prevented by setting the subtrees to NULL before deletion) + */ + virtual ~BoundedEventually() { + if (child != nullptr) { + delete child; + } + } + + /*! + * @returns the child node + */ + const PctlStateFormula& getChild() const { + return *child; + } + + /*! + * Sets the subtree + * @param child the new child node + */ + void setChild(PctlStateFormula* child) { + this->child = child; + } + + /*! + * @returns the maximally allowed number of steps for the bounded until operator + */ + uint_fast64_t getBound() const { + return bound; + } + + /*! + * Sets the maximally allowed number of steps for the bounded until operator + * + * @param bound the new bound. + */ + void setBound(uint_fast64_t bound) { + this->bound = bound; + } + + /*! + * @returns a string representation of the formula + */ + virtual std::string toString() const { + std::string result = "F<="; + result += std::to_string(bound); + result += " "; + result += child->toString(); + 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 PctlPathFormula* clone() const { + BoundedEventually* result = new BoundedEventually(); + result->setBound(bound); + if (child != nullptr) { + result->setRight(child->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 std::vector *check(const storm::modelChecker::DtmcPrctlModelChecker& modelChecker) const { + return modelChecker.checkBoundedEventually(*this); + } + +private: + PctlStateFormula* child; + uint_fast64_t bound; +}; + +} //namespace formula + +} //namespace storm + +#endif /* STORM_FORMULA_BOUNDEDUNTIL_H_ */ diff --git a/src/formula/BoundedUntil.h b/src/formula/BoundedUntil.h index 1dd8f255f..675138e27 100644 --- a/src/formula/BoundedUntil.h +++ b/src/formula/BoundedUntil.h @@ -145,7 +145,7 @@ public: * @returns a new BoundedUntil-object that is identical the called object. */ virtual PctlPathFormula* clone() const { - BoundedUntil* result = new BoundedUntil(); + BoundedUntil* result = new BoundedUntil(); result->setBound(bound); if (left != NULL) { result->setLeft(left->clone()); diff --git a/src/formula/Formulas.h b/src/formula/Formulas.h index b93952b9b..2698985cd 100644 --- a/src/formula/Formulas.h +++ b/src/formula/Formulas.h @@ -22,6 +22,7 @@ #include "Until.h" #include "Eventually.h" #include "Globally.h" +#include "BoundedEventually.h" #include "InstantaneousReward.h" #include "CumulativeReward.h" diff --git a/src/modelChecker/DtmcPrctlModelChecker.h b/src/modelChecker/DtmcPrctlModelChecker.h index 57ca784d8..c62cfa991 100644 --- a/src/modelChecker/DtmcPrctlModelChecker.h +++ b/src/modelChecker/DtmcPrctlModelChecker.h @@ -30,6 +30,7 @@ class DtmcPrctlModelChecker; #include "src/models/Dtmc.h" #include "src/storage/BitVector.h" +#include "src/exceptions/InvalidPropertyException.h" #include #include "log4cplus/logger.h" @@ -219,6 +220,11 @@ public: } else if (formula.getAp().compare("false") == 0) { return new storm::storage::BitVector(this->getModel().getNumberOfStates()); } + + if (!this->getModel().hasAtomicProposition(formula.getAp())) { + throw storm::exceptions::InvalidPropertyException() << "Atomic proposition '" << formula.getAp() << "' is invalid."; + } + return new storm::storage::BitVector(*this->getModel().getLabeledStates(formula.getAp())); } @@ -357,6 +363,19 @@ public: */ virtual std::vector* checkNext(const storm::formula::Next& formula) const = 0; + /*! + * The check method for a path formula with a Bounded Eventually operator node as root in its + * formula tree + * + * @param formula The Bounded Eventually path formula to check + * @returns for each state the probability that the path formula holds + */ + virtual std::vector* checkBoundedEventually(const storm::formula::BoundedEventually& formula) const { + // Create equivalent temporary bounded until formula and check it. + storm::formula::BoundedUntil temporaryBoundedUntilFormula(new storm::formula::Ap("true"), formula.getChild().clone(), formula.getBound()); + return this->checkBoundedUntil(temporaryBoundedUntilFormula); + } + /*! * The check method for a path formula with an Eventually operator node as root in its formula tree * @@ -366,8 +385,7 @@ public: virtual std::vector* checkEventually(const storm::formula::Eventually& formula) const { // Create equivalent temporary until formula and check it. storm::formula::Until temporaryUntilFormula(new storm::formula::Ap("true"), formula.getChild().clone()); - std::vector* result = this->checkUntil(temporaryUntilFormula); - return result; + return this->checkUntil(temporaryUntilFormula); } /*! @@ -383,7 +401,6 @@ public: // Now subtract the resulting vector from the constant one vector to obtain final result. storm::utility::subtractFromConstantOneVector(result); - return result; } diff --git a/src/modelChecker/GmmxxDtmcPrctlModelChecker.h b/src/modelChecker/GmmxxDtmcPrctlModelChecker.h index 3225ecc59..2d4d65d49 100644 --- a/src/modelChecker/GmmxxDtmcPrctlModelChecker.h +++ b/src/modelChecker/GmmxxDtmcPrctlModelChecker.h @@ -17,7 +17,7 @@ #include "src/utility/ConstTemplates.h" #include "src/utility/Settings.h" #include "src/adapters/GmmxxAdapter.h" -#include "src/exceptions/InvalidArgumentException.h" +#include "src/exceptions/InvalidPropertyException.h" #include "gmm/gmm_matrix.h" #include "gmm/gmm_iter_solvers.h" @@ -170,7 +170,7 @@ public: // Only compute the result if the model has a state-based reward model. if (!this->getModel().hasStateRewards()) { LOG4CPLUS_ERROR(logger, "Missing (state-based) reward model for formula."); - throw storm::exceptions::InvalidArgumentException() << "Missing (state-based) reward model for formula."; + throw storm::exceptions::InvalidPropertyException() << "Missing (state-based) reward model for formula."; } // Transform the transition probability matrix to the gmm++ format to use its arithmetic. @@ -199,7 +199,7 @@ public: // Only compute the result if the model has at least one reward model. if (!this->getModel().hasStateRewards() && !this->getModel().hasTransitionRewards()) { LOG4CPLUS_ERROR(logger, "Missing reward model for formula."); - throw storm::exceptions::InvalidArgumentException() << "Missing reward model for formula."; + throw storm::exceptions::InvalidPropertyException() << "Missing reward model for formula."; } // Transform the transition probability matrix to the gmm++ format to use its arithmetic. @@ -242,7 +242,7 @@ public: // Only compute the result if the model has at least one reward model. if (!this->getModel().hasStateRewards() && !this->getModel().hasTransitionRewards()) { LOG4CPLUS_ERROR(logger, "Missing reward model for formula. Skipping formula"); - throw storm::exceptions::InvalidArgumentException() << "Missing reward model for formula."; + throw storm::exceptions::InvalidPropertyException() << "Missing reward model for formula."; } // Determine the states for which the target predicate holds. diff --git a/src/models/Dtmc.h b/src/models/Dtmc.h index 8b6c8ed43..cb75afc28 100644 --- a/src/models/Dtmc.h +++ b/src/models/Dtmc.h @@ -165,6 +165,15 @@ public: return this->transitionRewardMatrix != nullptr; } + /*! + * Retrieves whether the given atomic proposition is a valid atomic proposition in this model. + * @param atomicProposition The atomic proposition to be checked for validity. + * @return True if the given atomic proposition is valid in this model. + */ + bool hasAtomicProposition(std::string const& atomicProposition) { + return this->stateLabeling->containsAtomicProposition(atomicProposition); + } + /*! * Prints information about the model to the specified stream. * @param out The stream the information is to be printed to. diff --git a/src/storm.cpp b/src/storm.cpp index 28d414260..5959bd537 100644 --- a/src/storm.cpp +++ b/src/storm.cpp @@ -67,7 +67,7 @@ void setUpFileLogging() { */ void printHeader(const int argc, const char* argv[]) { std::cout << "StoRM" << std::endl; - std::cout << "====" << std::endl << std::endl; + std::cout << "-----" << std::endl << std::endl; std::cout << "Version: 1.0 Alpha" << std::endl; // "Compute" the command line argument string with which STORM was invoked. @@ -221,7 +221,7 @@ void testChecking() { dtmc->printModelInformationToStream(std::cout); - // testCheckingDie(*dtmc); + testCheckingDie(*dtmc); // testCheckingCrowds(*dtmc); // testCheckingSynchronousLeader(*dtmc, 4); }