Added BoundedEventually as a convenience operator.

Included check for illegal atomic propositions.
Added exception class to be raised in case a property is invalid for the respective model.

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_ */

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 <string>
+
+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 T>
+class BoundedEventually : public PctlPathFormula<T> {
+
+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<T>* 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<T>& getChild() const {
+		return *child;
+	}
+
+	/*!
+	 * Sets the subtree
+	 * @param child the new child node
+	 */
+	void setChild(PctlStateFormula<T>* 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<T>* clone() const {
+		BoundedEventually<T>* result = new BoundedEventually<T>();
+		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<T> *check(const storm::modelChecker::DtmcPrctlModelChecker<T>& modelChecker) const {
+	  return modelChecker.checkBoundedEventually(*this);
+	}
+
+private:
+	PctlStateFormula<T>* child;
+	uint_fast64_t bound;
+};
+
+} //namespace formula
+
+} //namespace storm
+
+#endif /* STORM_FORMULA_BOUNDEDUNTIL_H_ */

src/formula/BoundedUntil.h

@@ -145,7 +145,7 @@ public:
 	 * @returns a new BoundedUntil-object that is identical the called object.
 	 */
 	virtual PctlPathFormula<T>* clone() const {
-		BoundedUntil<T>* result = new BoundedUntil();
+		BoundedUntil<T>* result = new BoundedUntil<T>();
 		result->setBound(bound);
 		if (left != NULL) {
 			result->setLeft(left->clone());

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"

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 <vector>
 
 #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<Type>* checkNext(const storm::formula::Next<Type>& 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<Type>* checkBoundedEventually(const storm::formula::BoundedEventually<Type>& formula) const {
+		// Create equivalent temporary bounded until formula and check it.
+		storm::formula::BoundedUntil<Type> temporaryBoundedUntilFormula(new storm::formula::Ap<Type>("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<Type>* checkEventually(const storm::formula::Eventually<Type>& formula) const {
 		// Create equivalent temporary until formula and check it.
 		storm::formula::Until<Type> temporaryUntilFormula(new storm::formula::Ap<Type>("true"), formula.getChild().clone());
-		std::vector<Type>* 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;
 	}
 

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.

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.

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);
 }