diff --git a/src/formula/AbstractFilter.h b/src/formula/AbstractFilter.h
index f1e7017f7..3824817fe 100644
--- a/src/formula/AbstractFilter.h
+++ b/src/formula/AbstractFilter.h
@@ -17,25 +17,72 @@ namespace storm {
namespace property {
/*!
- *
+ * This enum contains value indicating which kind of scheduler is to be used
+ * for path formulas, i.e. probability or reward queries on nondeterministic models.
*/
enum OptimizingOperator {MINIMIZE, MAXIMIZE, UNDEFINED};
+/*!
+ * This is the base class for the logic specific filter classes.
+ * It provides the logic independent functionality concerning the organization of actions and the optimization operator.
+ *
+ * The general role of the filter is to twofold.
+ *
+ * On the one hand it is meant to be the interface between the control and the formulas and modelchecker.
+ * It sits one level above the root of the formula tree which is represented by it.
+ * This gives a distinct class that can be moved through the control functions, thus encapsulating the formula tree and all its classes.
+ *
+ * On the other hand, as all modelchecking is initiated through its interface it opens up the opportunity to manipulate the output generated by the modelchecker.
+ * The manipulation is done by a series of filter actions which are evaluated after the modelchecker has finished.
+ * Each action has a distinct function that ranges from state selection to sorting.
+ * The input for the first filter action consists mainly of the modelckecking result.
+ * Thereafter, the result of each filter action is used as input for the next filter action until all actions have been executed.
+ * The final result is then used to generate the output.
+ */
template <class T>
class AbstractFilter {
public:
+ /*!
+ * Constructs an empty AbstractFilter.
+ * If a value for the optimization operator is given it will be set accordingly.
+ * Otherwise, it will be undefined. The undefined value is intended for deterministic
+ * models, as the do not need a scheduler resolving the nondeterminism.
+ *
+ * @note If a query is executed on a nondeterministic model using an undefined optimization operator
+ * the modelchecker will throw an exception.
+ *
+ * @param opt The value of the optimization operator.
+ */
AbstractFilter(OptimizingOperator opt = UNDEFINED) : opt(opt) {
// Intentionally left empty.
}
+ /*!
+ * Constructs an AbstractFilter containing only the specified action.
+ *
+ * @note If the shared_ptr to the action is empty (contains a nullptr) the Abstract filter will be created empty.
+ *
+ * @param action The action to be executed during evaluation.
+ * @param opt The value of the optimization operator.
+ */
AbstractFilter(std::shared_ptr<action::AbstractAction<T>> const & action, OptimizingOperator opt = UNDEFINED) : opt(opt) {
if(action.get() != nullptr) {
actions.push_back(action);
}
}
+ /*!
+ * Constructs an AbstractFilter containing the given vector of actions as action list.
+ * The actions will be executed in ascending order of index.
+ *
+ * @note Any vector entry containing an empty shared_ptr will be ignored. Thus, giving a
+ * vector of five actions with two empty shared_ptr will result in a AbstractFilter containing three actions.
+ *
+ * @param actions A vector of shared_ptr to the actions to be executed during evaluation.
+ * @param opt The value of the optimization operator.
+ */
AbstractFilter(std::vector<std::shared_ptr<action::AbstractAction<T>>> const & actions, OptimizingOperator opt = UNDEFINED) {
// Filter out all nullptr actions.
// First detect that there is at least one.
@@ -64,10 +111,18 @@ public:
this->opt = opt;
}
+ /*!
+ * The virtual destructor.
+ */
virtual ~AbstractFilter() {
// Intentionally left empty.
}
+ /*!
+ * Returns a string representation of the filter.
+ *
+ * @returns A string representing the filter.
+ */
virtual std::string toString() const {
std::string desc = "filter(";
@@ -87,25 +142,32 @@ public:
return desc;
}
- virtual std::string toPrettyString() const {
- std::string desc = "Filter: ";
- desc += "\nActions:";
- for(auto action : actions) {
- desc += "\n\t" + action->toString();
- }
- return desc;
- }
-
+ /*!
+ * Appends the given action to the list of actions to be executed during evaluation.
+ *
+ * @note If the argument is an empty shared_ptr nothing will happen.
+ *
+ * @param action A shared pointer to the action to be appended.
+ */
void addAction(std::shared_ptr<action::AbstractAction<T>> const & action) {
if(action.get() != nullptr) {
actions.push_back(action);
}
}
+ /*!
+ * Removes the last action.
+ */
void removeAction() {
actions.pop_back();
}
+ /*!
+ * Returns the action at the specified position.
+ *
+ * @param position The position of the action to be returned within the action list.
+ * @returns A shared pointer to the specified action.
+ */
std::shared_ptr<action::AbstractAction<T>> getAction(uint_fast64_t position) {
// Make sure the chosen position is not beyond the end of the vector.
// If it is so return the last element.
@@ -116,22 +178,40 @@ public:
}
}
+ /*!
+ * Returns the number of actions to be executed during evaluation.
+ *
+ * @returns The number of actions in the action list.
+ */
uint_fast64_t getActionCount() const {
return actions.size();
}
+ /*!
+ * Sets whether a minimizing or a maximizing scheduler is to be used for
+ * modelchecking of path formulas, i.e. probability and reward queries.
+ *
+ * @param opt The new operator specifying the scheduler to be used for path formulas.
+ */
void setOptimizingOperator(OptimizingOperator opt) {
this->opt = opt;
}
+ /*!
+ * Returns the current optimization operator.
+ *
+ * @return The optimization operator.
+ */
OptimizingOperator getOptimizingOperator() const {
return opt;
}
protected:
+ //! The vector containing the actions to be executed during evaluation.
std::vector<std::shared_ptr<action::AbstractAction<T>>> actions;
+ //! The optimization operator specifying if and which kind of scheduler is to be used during modelchecking of path formulas on nondeterministic models.
OptimizingOperator opt;
};
diff --git a/src/formula/AbstractFormula.h b/src/formula/AbstractFormula.h
index 8ab2fd130..9b009f208 100644
--- a/src/formula/AbstractFormula.h
+++ b/src/formula/AbstractFormula.h
@@ -20,44 +20,36 @@ template <class T> class AbstractFormula;
namespace storm {
namespace property {
-//abstract
+// do properties
+
/*!
- * @brief Abstract base class for logic Abstract formulas in general.
- *
- * The namespace storm::property::abstract contains versions of the formula classes which are logic abstract, and contain
- * the implementation which is not directly dependent on the logics.
- * The classes for the subtrees are referenced by the template parameter FormulaType, which is typically instantiated in
- * the derived classes of concrete logics.
- *
- * The instantiation of FormulaType should be a subclass of AbstractFormula, as the functions "toString" and "validate"
- * of the subformulas are needed.
+ * This is the abstract base class for every formula class in every logic.
*
- * @note
- * Even though the namespace is called "abstract", its classes may be completely implemented; abstract here denotes
- * the abstraction from a concrete logic.
+ * There are currently three implemented logics Ltl, Csl and Pctl.
+ * The implementation of these logics can be found in the namespaces storm::property::<logic>
+ * where <logic> is one of ltl, pctl and csl.
*
- * @attention This class is abstract.
- * @note Formula classes do not have copy constructors. The parameters of the constructors are usually the subtrees, so
- * the syntax conflicts with copy constructors for unary operators. To produce an identical object, the classes
- * AbstractFormula and AbstractFormula offer the method clone().
- *
- * This is the base class for every formula class in every logic.
+ * @note While formula classes do have copy constructors using a copy constructor
+ * will yield a formula objects whose formula subtree consists of the same objects
+ * as the original formula. The ownership of the formula tree will be shared between
+ * the original and the copy.
*/
template <class T>
class AbstractFormula {
public:
+
/*!
- * Virtual destructor.
+ * The virtual destructor.
*/
virtual ~AbstractFormula() {
// Intentionally left empty.
}
/*!
- * @brief Return string representation of this formula.
+ * Return string representation of this formula.
*
- * @note every subclass must implement this method.
+ * @note Every subclass must implement this method.
*
* @returns a string representation of the formula
*/
diff --git a/src/formula/ComparisonType.h b/src/formula/ComparisonType.h
index 98ee80373..bb6ea82ee 100644
--- a/src/formula/ComparisonType.h
+++ b/src/formula/ComparisonType.h
@@ -11,6 +11,11 @@
namespace storm {
namespace property {
+/*!
+ * An enum representing the greater- and less-than operators in both
+ * the strict (<, >) and the non strict (<=, >=) variant.
+ * It is mainly used to represent upper and lower bounds.
+ */
enum ComparisonType { LESS, LESS_EQUAL, GREATER, GREATER_EQUAL };
}
diff --git a/src/formula/IOptimizingOperator.h b/src/formula/IOptimizingOperator.h
deleted file mode 100644
index f89419d91..000000000
--- a/src/formula/IOptimizingOperator.h
+++ /dev/null
@@ -1,43 +0,0 @@
-/*
- * IOptimizingOperator.h
- *
- * Created on: 17.04.2013
- * Author: thomas
- */
-
-#ifndef STORM_FORMULA_IOPTIMIZINGOPERATOR_H_
-#define STORM_FORMULA_IOPTIMIZINGOPERATOR_H_
-
-namespace storm {
-namespace property {
-
-/*!
- * @brief Interface for optimizing operators
- *
- * Needed to link abstract classes in concrete logics with the logic-abstract implementation.
- */
-class IOptimizingOperator {
-public:
-
- virtual ~IOptimizingOperator() {
- // Intentionally left empty
- }
-
- /*!
- * Retrieves whether the operator is to be interpreted as an optimizing (i.e. min/max) operator.
- * @returns True if the operator is an optimizing operator.
- */
- virtual bool isOptimalityOperator() const = 0;
-
- /*!
- * Retrieves whether the operator is a minimizing operator given that it is an optimality
- * operator.
- * @returns True if the operator is an optimizing operator and it is a minimizing operator and
- * false otherwise, i.e. if it is either not an optimizing operator or not a minimizing operator.
- */
- virtual bool isMinimumOperator() const = 0;
-};
-
-} /* namespace property */
-} /* namespace storm */
-#endif /* STORM_FORMULA_IOPTIMIZINGOPERATOR_H_ */
diff --git a/src/formula/actions/AbstractAction.h b/src/formula/actions/AbstractAction.h
index 77d2089ea..0912751fd 100644
--- a/src/formula/actions/AbstractAction.h
+++ b/src/formula/actions/AbstractAction.h
@@ -19,78 +19,122 @@ namespace storm {
namespace property {
namespace action {
+/*!
+ * This is the abstract base class for all filter actions.
+ *
+ * Each action implements a distinct function which executed each time evaluate() is called.
+ * The input and output for each action is an instance of the Result struct.
+ * Thus the action is able to manipulate both the selection of output states and the order in which they are returned.
+ */
template <class T>
class AbstractAction {
public:
+ /*!
+ * This is the struct used by all actions to pass along information.
+ *
+ * It contains fields for the two possible data structures containing the modelchecking results.
+ * A value vector for path formulas and a bit vector for state formulas.
+ * The two other fields are used to describe a selection as well as an ordering of states within the modelchecking results.
+ *
+ * @note For each formula the modelchecker will return either a BitVector or a std::vector.
+ * Thus, either the state- or the pathResult should be set to be empty.
+ * If both contain a value for at least one state the pathResult will be used.
+ *
+ * @note The four vectors should always have the same number of entries.
+ */
struct Result {
/*!
- *
+ * Constructs an empty Result.
*/
Result() : selection(), stateMap(), pathResult(), stateResult(){
// Intentionally left empty.
}
/*!
+ * Copy constructs a Result.
*
+ * @param other The Result from which the fields are copied.
*/
Result(Result const & other) : selection(other.selection), stateMap(other.stateMap), pathResult(other.pathResult), stateResult(other.stateResult) {
// Intentionally left empty.
}
/*!
+ * Constructs a Result using values for each field.
*
+ * @param selection A BitVector describing which states are currently selected.
+ * @param stateMap A vector representing an ordering on the states within the modelchecking results.
+ * @param pathResult The modelchecking result for a path formula.
+ * @param stateResult The modelchecking result for a state formula.
*/
Result(storm::storage::BitVector const & selection, std::vector<uint_fast64_t> const & stateMap, std::vector<T> const & pathResult, storm::storage::BitVector const & stateResult) : selection(selection), stateMap(stateMap), pathResult(pathResult), stateResult(stateResult) {
// Intentionally left empty.
}
- //!
+ //! A BitVector describing which states are currently selected.
+ //! For state i the i-th bit is true iff state i is selected.
storm::storage::BitVector selection;
- //!
+ //! A vector representing an ordering on the states within the modelchecking results.
+ //! The first value of the vector is the index of the state to be returned first.
+ //! Thus, stateMap[i] is the index of the state that is to be returned at position i.
std::vector<uint_fast64_t> stateMap;
- //!
+ //! The modelchecking result for a path formula.
std::vector<T> pathResult;
- //!
+ //! The modelchecking result for a state formula.
storm::storage::BitVector stateResult;
};
/*!
- * Virtual destructor
- * To ensure that the right destructor is called
+ * The virtual destructor.
+ * To ensure that the right destructor is called.
*/
virtual ~AbstractAction() {
//Intentionally left empty
}
- /*
+ /*!
+ * Evaluate the action for a Prctl formula.
*
+ * @param result The Result struct on which the action is to be evaluated.
+ * @param mc The Prctl modelchecker that computed the path- or stateResult contained in the Result struct.
+ * @returns A Result struct containing the output of the action.
*/
- virtual Result evaluate(Result const & filterResult, storm::modelchecker::prctl::AbstractModelChecker<T> const & mc) const {
+ virtual Result evaluate(Result const & result, storm::modelchecker::prctl::AbstractModelChecker<T> const & mc) const {
return Result();
}
- /*
+ /*!
+ * Evaluate the action for a Csl formula.
*
+ * @param result The Result struct on which the action is to be evaluated.
+ * @param mc The Csl modelchecker that computed the path- or stateResult contained in the Result struct.
+ * @returns A Result struct containing the output of the action.
*/
- virtual Result evaluate(Result const & filterResult, storm::modelchecker::csl::AbstractModelChecker<T> const & mc) const {
+ virtual Result evaluate(Result const & result, storm::modelchecker::csl::AbstractModelChecker<T> const & mc) const {
return Result();
}
- /*
+ /*!
+ * Evaluate the action for an Ltl formula.
*
+ * @param result The Result struct on which the action is to be evaluated.
+ * @param mc The Ltl modelchecker that computed the path- or stateResult contained in the Result struct.
+ * @returns A Result struct containing the output of the action.
*/
- virtual Result evaluate(Result const & filterResult, storm::modelchecker::ltl::AbstractModelChecker<T> const & mc) const {
+ virtual Result evaluate(Result const & result, storm::modelchecker::ltl::AbstractModelChecker<T> const & mc) const {
return Result();
}
/*!
+ * Returns a string representation of the action.
*
+ * @returns A string representing the action.
*/
virtual std::string toString() const = 0;
diff --git a/src/formula/actions/BoundAction.h b/src/formula/actions/BoundAction.h
index f90107742..1603c3308 100644
--- a/src/formula/actions/BoundAction.h
+++ b/src/formula/actions/BoundAction.h
@@ -16,52 +16,83 @@ namespace storm {
namespace property {
namespace action {
+/*!
+ * The bound action deselects all states whose modelchecking values do not satisfy the given bound.
+ *
+ * Strict and non strict upper and lower bounds can be represented.
+ * For modelchecking results of state formulas the value is taken to be 1 iff true and 0 otherwise.
+ */
template <class T>
class BoundAction : public AbstractAction<T> {
+ // Convenience typedef to make the code more readable.
typedef typename AbstractAction<T>::Result Result;
public:
+ /*!
+ * Constructs an empty BoundAction.
+ * The bound is set to >= 0. Thus, all states will be selected by the action.
+ */
BoundAction() : comparisonOperator(storm::property::GREATER_EQUAL), bound(0) {
//Intentionally left empty.
}
+ /*!
+ * Constructs a BoundAction using the given values for the comparison operator and the bound.
+ *
+ * @param comparisonOperator The operator used to make the comparison between the bound and the modelchecking values for each state.
+ * @param bound The bound to compare the modelchecking values against.
+ */
BoundAction(storm::property::ComparisonType comparisonOperator, T bound) : comparisonOperator(comparisonOperator), bound(bound) {
//Intentionally left empty.
}
/*!
- * Virtual destructor
- * To ensure that the right destructor is called
+ * The virtual destructor.
+ * To ensure that the right destructor is called.
*/
virtual ~BoundAction() {
//Intentionally left empty
}
/*!
+ * Evaluate the action for an Prctl formula.
*
+ * @param result The Result struct on which the action is to be evaluated.
+ * @param mc The Prctl modelchecker that computed the path- or stateResult contained in the Result struct.
+ * @returns A Result struct containing the output of the action.
*/
virtual Result evaluate(Result const & result, storm::modelchecker::prctl::AbstractModelChecker<T> const & mc) const override {
return evaluate(result);
}
/*!
+ * Evaluate the action for an Csl formula.
*
+ * @param result The Result struct on which the action is to be evaluated.
+ * @param mc The Csl modelchecker that computed the path- or stateResult contained in the Result struct.
+ * @returns A Result struct containing the output of the action.
*/
virtual Result evaluate(Result const & result, storm::modelchecker::csl::AbstractModelChecker<T> const & mc) const override {
return evaluate(result);
}
/*!
+ * Evaluate the action for an Ltl formula.
*
+ * @param result The Result struct on which the action is to be evaluated.
+ * @param mc The Ltl modelchecker that computed the path- or stateResult contained in the Result struct.
+ * @returns A Result struct containing the output of the action.
*/
virtual Result evaluate(Result const & result, storm::modelchecker::ltl::AbstractModelChecker<T> const & mc) const override {
return evaluate(result);
}
/*!
+ * Returns a string representation of this action.
*
+ * @returns A string representing this action.
*/
virtual std::string toString() const override {
std::string out = "bound(";
@@ -92,7 +123,14 @@ public:
private:
/*!
+ * Evaluate the action.
*
+ * As the BoundAction does not depend on the model or the formula for which the modelchecking result was computed,
+ * it does not depend on the modelchecker at all. This internal version of the evaluate method therefore only needs the
+ * modelchecking result as input.
+ *
+ * @param result The Result struct on which the action is to be evaluated.
+ * @returns A Result struct containing the output of the action.
*/
virtual Result evaluate(Result const & result) const {
@@ -159,7 +197,10 @@ private:
return Result(out, result.stateMap, result.pathResult, result.stateResult);
}
+ // The operator used to make the comparison between the bound and the modelchecking values for each state at time of evaluation.
storm::property::ComparisonType comparisonOperator;
+
+ // The bound to compare the modelchecking values against during evaluation.
T bound;
};
diff --git a/src/formula/actions/FormulaAction.h b/src/formula/actions/FormulaAction.h
index 9ac3ad861..5028253fe 100644
--- a/src/formula/actions/FormulaAction.h
+++ b/src/formula/actions/FormulaAction.h
@@ -19,35 +19,62 @@ namespace storm {
namespace property {
namespace action {
+/*!
+ * The Formula action deselects all states that do not satisfy the given state formula.
+ *
+ * @note Since there is no modelchecker implemented for Ltl formulas (except the abstract base class)
+ * the formula action currently only supports Prctl and Csl state formulas.
+ */
template <class T>
class FormulaAction : public AbstractAction<T> {
+ // Convenience typedef to make the code more readable.
typedef typename AbstractAction<T>::Result Result;
public:
+
+ /*!
+ * Constructs an empty FormulaAction.
+ *
+ * The evaluation will do nothing and return the Result as it was put in.
+ */
FormulaAction() : prctlFormula(nullptr), cslFormula(nullptr) {
//Intentionally left empty.
}
+ /*!
+ * Constructs a FormulaAction using the given Prctl formula.
+ *
+ * @param prctlFormula The Prctl state formula used to filter the selection during evaluation.
+ */
FormulaAction(std::shared_ptr<storm::property::prctl::AbstractStateFormula<T>> const & prctlFormula) : prctlFormula(prctlFormula), cslFormula(nullptr) {
//Intentionally left empty.
}
+ /*!
+ * Constructs a FormulaAction using the given Csl formula.
+ *
+ * @param cslFormula The Csl state formula used to filter the selection during evaluation.
+ */
FormulaAction(std::shared_ptr<storm::property::csl::AbstractStateFormula<T>> const & cslFormula) : prctlFormula(nullptr), cslFormula(cslFormula) {
//Intentionally left empty.
}
/*!
- * Virtual destructor
- * To ensure that the right destructor is called
+ * The virtual destructor.
+ * To ensure that the right destructor is called.
*/
virtual ~FormulaAction() {
// Intentionally left empty.
}
/*!
+ * Evaluate the action for an Prctl formula.
*
+ * @param result The Result struct on which the action is to be evaluated.
+ * @param mc The Prctl modelchecker that computed the path- or stateResult contained in the Result struct.
+ * @returns A Result struct containing the output of the action.
*/
virtual Result evaluate(Result const & result, storm::modelchecker::prctl::AbstractModelChecker<T> const & mc) const override {
@@ -62,7 +89,11 @@ public:
}
/*!
+ * Evaluate the action for an Csl formula.
*
+ * @param result The Result struct on which the action is to be evaluated.
+ * @param mc The Csl modelchecker that computed the path- or stateResult contained in the Result struct.
+ * @returns A Result struct containing the output of the action.
*/
virtual Result evaluate(Result const & result, storm::modelchecker::csl::AbstractModelChecker<T> const & mc) const override {
@@ -77,7 +108,9 @@ public:
}
/*!
+ * Returns a string representation of this action.
*
+ * @returns A string representing this action.
*/
virtual std::string toString() const override {
std::string out = "formula(";
@@ -91,7 +124,11 @@ public:
}
private:
+
+ // The Prctl state formula used during evaluation.
std::shared_ptr<storm::property::prctl::AbstractStateFormula<T>> prctlFormula;
+
+ // The Csl state formula used during evaluation.
std::shared_ptr<storm::property::csl::AbstractStateFormula<T>> cslFormula;
};
diff --git a/src/formula/actions/InvertAction.h b/src/formula/actions/InvertAction.h
index 5492e4644..7084d52e2 100644
--- a/src/formula/actions/InvertAction.h
+++ b/src/formula/actions/InvertAction.h
@@ -14,48 +14,71 @@ namespace storm {
namespace property {
namespace action {
+/*!
+ * The InvertAction inverts the selection, selecting precisely the unselected states.
+ */
template <class T>
class InvertAction : public AbstractAction<T> {
+ // Convenience typedef to make the code more readable.
typedef typename AbstractAction<T>::Result Result;
public:
+ /*!
+ * Constructs an InvertAction.
+ *
+ * As the simple inversion of the selection does not need any parameters, the empty constructor is the only one needed.
+ */
InvertAction() {
//Intentionally left empty.
}
/*!
- * Virtual destructor
- * To ensure that the right destructor is called
+ * The virtual destructor.
+ * To ensure that the right destructor is called.
*/
virtual ~InvertAction() {
//Intentionally left empty
}
/*!
+ * Evaluate the action for a Prctl formula.
*
+ * @param result The Result struct on which the action is to be evaluated.
+ * @param mc The Prctl modelchecker that computed the path- or stateResult contained in the Result struct.
+ * @returns A Result struct containing the output of the action.
*/
virtual Result evaluate(Result const & result, storm::modelchecker::prctl::AbstractModelChecker<T> const & mc) const override {
return evaluate(result);
}
/*!
+ * Evaluate the action for a Csl formula.
*
+ * @param result The Result struct on which the action is to be evaluated.
+ * @param mc The Csl modelchecker that computed the path- or stateResult contained in the Result struct.
+ * @returns A Result struct containing the output of the action.
*/
virtual Result evaluate(Result const & result, storm::modelchecker::csl::AbstractModelChecker<T> const & mc) const override {
return evaluate(result);
}
/*!
+ * Evaluate the action for a Ltl formula.
*
+ * @param result The Result struct on which the action is to be evaluated.
+ * @param mc The Ltl modelchecker that computed the path- or stateResult contained in the Result struct.
+ * @returns A Result struct containing the output of the action.
*/
virtual Result evaluate(Result const & result, storm::modelchecker::ltl::AbstractModelChecker<T> const & mc) const override {
return evaluate(result);
}
/*!
+ * Returns a string representation of this action.
*
+ * @returns A string representing this action.
*/
virtual std::string toString() const override {
return "invert";
@@ -64,7 +87,14 @@ public:
private:
/*!
+ * Evaluate the action.
+ *
+ * As the InvertAction does not depend on the model or the formula for which the modelchecking result was computed,
+ * it does not depend on the modelchecker at all. This internal version of the evaluate method therefore only needs the
+ * modelchecking result as input.
*
+ * @param result The Result struct on which the action is to be evaluated.
+ * @returns A Result struct containing the output of the action.
*/
virtual Result evaluate(Result const & result) const {
storm::storage::BitVector out(result.selection);
diff --git a/src/formula/actions/RangeAction.h b/src/formula/actions/RangeAction.h
index 382492d49..8136715b2 100644
--- a/src/formula/actions/RangeAction.h
+++ b/src/formula/actions/RangeAction.h
@@ -14,57 +14,80 @@ namespace storm {
namespace property {
namespace action {
+/*!
+ * The RangeAction deselects all states that are not within the given range.
+ *
+ * The bounds of the range given are indices in the result ordering.
+ * Thus, if the lower bound is 0 and the upper bound is 5 then all states that are not
+ * at index 0 through 5 (including) in the state ordering will be deselected.
+ * This action is thought to be used in connection with the SortAction.
+ */
template <class T>
class RangeAction : public AbstractAction<T> {
+ // Convenience typedef to make the code more readable.
typedef typename AbstractAction<T>::Result Result;
public:
- RangeAction() : from(0), to(0) {
- //Intentionally left empty.
- }
-
/*!
- * Including the state with position to.
+ * Construct a RangeAction using the given values.
+ *
+ * If no values are given they default to [0,UINT_FAST64_MAX] thus deselecting no state at evaluation.
+ *
+ * @note The interval bounds are included in the interval.
*/
- RangeAction(uint_fast64_t from, uint_fast64_t to) : from(from), to(to) {
+ RangeAction(uint_fast64_t from = 0, uint_fast64_t to = UINT_FAST64_MAX) : from(from), to(to) {
if(from > to) {
throw storm::exceptions::IllegalArgumentValueException() << "The end of the range is lower than its beginning";
}
}
/*!
- * Virtual destructor
- * To ensure that the right destructor is called
+ * The virtual destructor.
+ * To ensure that the right destructor is called.
*/
virtual ~RangeAction() {
//Intentionally left empty
}
/*!
+ * Evaluate the action for a Prctl formula.
*
+ * @param result The Result struct on which the action is to be evaluated.
+ * @param mc The Prctl modelchecker that computed the path- or stateResult contained in the Result struct.
+ * @returns A Result struct containing the output of the action.
*/
virtual Result evaluate(Result const & result, storm::modelchecker::prctl::AbstractModelChecker<T> const & mc) const override {
return evaluate(result);
}
/*!
+ * Evaluate the action for a Csl formula.
*
+ * @param result The Result struct on which the action is to be evaluated.
+ * @param mc The Csl modelchecker that computed the path- or stateResult contained in the Result struct.
+ * @returns A Result struct containing the output of the action.
*/
virtual Result evaluate(Result const & result, storm::modelchecker::csl::AbstractModelChecker<T> const & mc) const override {
return evaluate(result);
}
/*!
+ * Evaluate the action for a Ltl formula.
*
+ * @param result The Result struct on which the action is to be evaluated.
+ * @param mc The Ltl modelchecker that computed the path- or stateResult contained in the Result struct.
+ * @returns A Result struct containing the output of the action.
*/
virtual Result evaluate(Result const & result, storm::modelchecker::ltl::AbstractModelChecker<T> const & mc) const override {
return evaluate(result);
}
/*!
+ * Returns a string representation of this action.
*
+ * @returns A string representing this action.
*/
virtual std::string toString() const override {
std::string out = "range(";
@@ -78,7 +101,14 @@ public:
private:
/*!
+ * Evaluate the action.
*
+ * As the RangeAction does not depend on the model or the formula for which the modelchecking result was computed,
+ * it does not depend on the modelchecker at all. This internal version of the evaluate method therefore only needs the
+ * modelchecking result as input.
+ *
+ * @param result The Result struct on which the action is to be evaluated.
+ * @returns A Result struct containing the output of the action.
*/
virtual Result evaluate(Result const & result) const {
//Initialize the output vector.
@@ -110,7 +140,10 @@ private:
return Result(out, result.stateMap, result.pathResult, result.stateResult);
}
+ // The lower bound of the interval of states not deselected.
uint_fast64_t from;
+
+ // The upper bound of the interval of states not deselected.
uint_fast64_t to;
};
diff --git a/src/formula/actions/SortAction.h b/src/formula/actions/SortAction.h
index ea676dfd4..289426f6f 100644
--- a/src/formula/actions/SortAction.h
+++ b/src/formula/actions/SortAction.h
@@ -15,54 +15,81 @@ namespace storm {
namespace property {
namespace action {
+/*!
+ * This action manipulates the state ordering by sorting the states by some category.
+ *
+ * Currently the states can be sorted either by index or by value; ascending or descending.
+ * This is done using the standard libraries sort function, thus the action evaluates in O(n*log n) where n is the number of states.
+ */
template <class T>
class SortAction : public AbstractAction<T> {
+ // Convenience typedef to make the code more readable.
typedef typename AbstractAction<T>::Result Result;
public:
+ //! Enum defining the categories in relation to which the states can be sorted.
enum SortingCategory {INDEX, VALUE};
- SortAction() : category(INDEX), ascending(true) {
- //Intentionally left empty.
- }
-
- SortAction(SortingCategory category, bool ascending = true) : category(category), ascending(ascending) {
+ /*!
+ * Construct a SortAction using the given values.
+ *
+ * If no values are given the action will sort by ascending state index.
+ *
+ * @param category An enum value identifying the category by which the states are to be ordered.
+ * @param ascending Determines whether the values are to be sorted in ascending or descending order.
+ * The parameter is to be set to true iff the values are to be sorted in ascending order.
+ */
+ SortAction(SortingCategory category = INDEX, bool ascending = true) : category(category), ascending(ascending) {
//Intentionally left empty.
}
/*!
- * Virtual destructor
- * To ensure that the right destructor is called
+ * The virtual destructor.
+ * To ensure that the right destructor is called.
*/
virtual ~SortAction() {
//Intentionally left empty
}
/*!
+ * Evaluate the action for a Prctl formula.
*
+ * @param result The Result struct on which the action is to be evaluated.
+ * @param mc The Prctl modelchecker that computed the path- or stateResult contained in the Result struct.
+ * @returns A Result struct containing the output of the action.
*/
virtual Result evaluate(Result const & result, storm::modelchecker::prctl::AbstractModelChecker<T> const & mc) const override {
return evaluate(result);
}
/*!
+ * Evaluate the action for a Csl formula.
*
+ * @param result The Result struct on which the action is to be evaluated.
+ * @param mc The Csl modelchecker that computed the path- or stateResult contained in the Result struct.
+ * @returns A Result struct containing the output of the action.
*/
virtual Result evaluate(Result const & result, storm::modelchecker::csl::AbstractModelChecker<T> const & mc) const override {
return evaluate(result);
}
/*!
+ * Evaluate the action for a Ltl formula.
*
+ * @param result The Result struct on which the action is to be evaluated.
+ * @param mc The Ltl modelchecker that computed the path- or stateResult contained in the Result struct.
+ * @returns A Result struct containing the output of the action.
*/
virtual Result evaluate(Result const & result, storm::modelchecker::ltl::AbstractModelChecker<T> const & mc) const override {
return evaluate(result);
}
/*!
+ * Returns a string representation of this action.
*
+ * @returns A string representing this action.
*/
virtual std::string toString() const override {
std::string out = "sort(";
@@ -87,7 +114,14 @@ public:
private:
/*!
+ * Evaluate the action.
+ *
+ * As the SortAction does not depend on the model or the formula for which the modelchecking result was computed,
+ * it does not depend on the modelchecker at all. This internal version of the evaluate method therefore only needs the
+ * modelchecking result as input.
*
+ * @param result The Result struct on which the action is to be evaluated.
+ * @returns A Result struct containing the output of the action.
*/
Result evaluate(Result const & result) const {
@@ -106,7 +140,11 @@ private:
}
/*!
+ * This method returns a vector of the given length filled with the numbers 0 to length-1 in ascending or descending order,
+ * depending on the value of the member variable ascending. Thus it sorts by state index.
*
+ * @param length The length of the generated vector.
+ * @returns A vector of unsigned integers from 0 to length-1 in ascending or descending order.
*/
std::vector<uint_fast64_t> sort(uint_fast64_t length) const {
@@ -128,7 +166,15 @@ private:
}
/*!
+ * Sort the stateMap vector representing the current state ordering by the values in the values vector.
*
+ * Here the entries in the values vector are assumed to be the modelchecking results of a path formula.
+ * Hence, the value at index i is associated with state i, i.e the value i in the stateMap.
+ * The ordering direction (ascending/decending) is given by the member variable ascending, set in the constructor.
+ *
+ * @param stateMap A vector representing the current state ordering.
+ * @param values A vector containing the values by which the stateMap is to be ordered.
+ * @returns A vector containing the reordered entries of the stateMap.
*/
std::vector<uint_fast64_t> sort(std::vector<uint_fast64_t> const & stateMap, std::vector<T> const & values) const {
@@ -146,7 +192,15 @@ private:
}
/*!
+ * Sort the stateMap vector representing the current state ordering by the values in the values vector.
+ *
+ * Here the entries in the values vector are assumed to be the modelchecking results of a state formula.
+ * Hence, the value at index i is associated with state i, i.e the value i in the stateMap.
+ * The ordering direction (ascending/decending) is given by the member variable ascending, set in the constructor.
*
+ * @param stateMap A vector representing the current state ordering.
+ * @param values A vector containing the values by which the stateMap is to be ordered.
+ * @returns A vector containing the reordered entries of the stateMap.
*/
std::vector<uint_fast64_t> sort(std::vector<uint_fast64_t> const & stateMap, storm::storage::BitVector const & values) const {
@@ -163,7 +217,10 @@ private:
return outMap;
}
+ // The category by which the states are to be ordered.
SortingCategory category;
+
+ // Determines whether the values are to be sorted in ascending or descending order.
bool ascending;
};
diff --git a/src/formula/csl/AbstractCslFormula.h b/src/formula/csl/AbstractCslFormula.h
index 73d4f3dcd..360b5d411 100644
--- a/src/formula/csl/AbstractCslFormula.h
+++ b/src/formula/csl/AbstractCslFormula.h
@@ -5,8 +5,8 @@
* Author: Thomas Heinemann
*/
-#ifndef ABSTRACTCSLFORMULA_H_
-#define ABSTRACTCSLFORMULA_H_
+#ifndef STORM_FORMULA_CSL_ABSTRACTCSLFORMULA_H_
+#define STORM_FORMULA_CSL_ABSTRACTCSLFORMULA_H_
#include "src/formula/AbstractFormula.h"
@@ -14,6 +14,8 @@ namespace storm {
namespace property {
namespace csl {
+// Forward declarations.
+
template <class T> class ProbabilisticBoundOperator;
template <class T> class Eventually;
template <class T> class Until;
@@ -27,11 +29,20 @@ namespace property {
namespace csl {
/*!
- * Abstract base class for all CSL root formulas.
+ * This is the abstract base class for all Csl formulas.
+ *
+ * @note While formula classes do have copy constructors using a copy constructor
+ * will yield a formula objects whose formula subtree consists of the same objects
+ * as the original formula. The ownership of the formula tree will be shared between
+ * the original and the copy.
*/
template <class T>
class AbstractCslFormula : public virtual storm::property::AbstractFormula<T>{
public:
+
+ /*!
+ * The virtual destructor.
+ */
virtual ~AbstractCslFormula() {
// Intentionally left empty
}
@@ -75,4 +86,4 @@ public:
} /* namespace csl */
} /* namespace property */
} /* namespace storm */
-#endif /* ABSTRACTCSLFORMULA_H_ */
+#endif /* STORM_FORMULA_CSL_ABSTRACTCSLFORMULA_H_ */
diff --git a/src/formula/csl/AbstractPathFormula.h b/src/formula/csl/AbstractPathFormula.h
index 6de58a14d..a8d415616 100644
--- a/src/formula/csl/AbstractPathFormula.h
+++ b/src/formula/csl/AbstractPathFormula.h
@@ -8,14 +8,6 @@
#ifndef STORM_FORMULA_CSL_ABSTRACTPATHFORMULA_H_
#define STORM_FORMULA_CSL_ABSTRACTPATHFORMULA_H_
-namespace storm {
-namespace property {
-namespace csl {
-template<class T> class AbstractPathFormula;
-} //namespace csl
-} //namespace property
-} //namespace storm
-
#include "src/formula/csl/AbstractCslFormula.h"
#include "src/modelchecker/csl/ForwardDeclarations.h"
@@ -28,23 +20,18 @@ namespace property {
namespace csl {
/*!
- * @brief
- * Abstract base class for Abstract path formulas.
- *
- * @attention This class is abstract.
- * @note Formula classes do not have copy constructors. The parameters of the constructors are usually the subtrees, so
- * the syntax conflicts with copy constructors for unary operators. To produce an identical object, use the method
- * clone().
+ * Abstract base class for Csl path formulas.
*
- * @note
- * This class is intentionally not derived from AbstractCslFormula, as a path formula is not a complete CSL formula.
+ * @note Differing from the formal definitions of PRCTL a path formula may be the root of a PRCTL formula.
+ * The result of a modelchecking process on such a formula is a vector representing the satisfaction probabilities for each state of the model.
*/
template <class T>
class AbstractPathFormula : public virtual storm::property::csl::AbstractCslFormula<T> {
public:
+
/*!
- * empty destructor
+ * The virtual destructor.
*/
virtual ~AbstractPathFormula() {
// Intentionally left empty
@@ -53,10 +40,11 @@ public:
/*!
* Clones the called object.
*
- * Performs a "deep copy", i.e. the subtrees of the new object are clones of the original ones
+ * Performs a "deep copy", i.e. the subtrees of the new object are clones of the original ones.
*
* @note This function is not implemented in this class.
- * @returns a new AND-object that is identical the called object.
+ *
+ * @returns A deep copy of the called object.
*/
virtual std::shared_ptr<AbstractPathFormula<T>> clone() const = 0;
diff --git a/src/formula/csl/AbstractStateFormula.h b/src/formula/csl/AbstractStateFormula.h
index 4a50c21b2..dec96eb45 100644
--- a/src/formula/csl/AbstractStateFormula.h
+++ b/src/formula/csl/AbstractStateFormula.h
@@ -17,20 +17,15 @@ namespace property {
namespace csl {
/*!
- * @brief
- * Abstract base class for Abstract state formulas.
- *
- * @attention This class is abstract.
- * @note Formula classes do not have copy constructors. The parameters of the constructors are usually the subtrees, so
- * the syntax conflicts with copy constructors for unary operators. To produce an identical object, use the method
- * clone().
+ * Abstract base class for Csl state formulas.
*/
template <class T>
class AbstractStateFormula : public storm::property::csl::AbstractCslFormula<T> {
public:
+
/*!
- * empty destructor
+ * Empty virtual destructor.
*/
virtual ~AbstractStateFormula() {
// Intentionally left empty
@@ -42,7 +37,8 @@ public:
* Performs a "deep copy", i.e. the subtrees of the new object are clones of the original ones
*
* @note This function is not implemented in this class.
- * @returns a new AND-object that is identical the called object.
+ *
+ * @returns A deep copy of the called object.
*/
virtual std::shared_ptr<AbstractStateFormula<T>> clone() const = 0;
diff --git a/src/formula/csl/And.h b/src/formula/csl/And.h
index afb78ceeb..a5ebaffb2 100644
--- a/src/formula/csl/And.h
+++ b/src/formula/csl/And.h
@@ -16,37 +16,45 @@ namespace storm {
namespace property {
namespace csl {
+// Forward declaration for the interface class.
template <class T> class And;
/*!
- * @brief Interface class for model checkers that support And.
+ * Interface class for model checkers that support And.
*
- * All model checkers that support the formula class And must inherit
- * this pure virtual class.
+ * All model checkers that support the formula class And must inherit
+ * this pure virtual class.
*/
template <class T>
class IAndModelChecker {
public:
+
+ /*!
+ * Empty virtual destructor.
+ */
+ virtual ~IAndModelChecker() {
+ // Intentionally left empty
+ }
+
/*!
- * @brief Evaluates And formula within a model checker.
+ * Evaluates an And formula within a model checker.
*
- * @param obj Formula object with subformulas.
- * @return Result of the formula for every node.
+ * @param obj Formula object with subformulas.
+ * @return The modelchecking result of the formula for every state.
*/
virtual storm::storage::BitVector checkAnd(const And<T>& obj) const = 0;
};
/*!
- * @brief
- * Class for an abstract formula tree with AND node as root.
+ * Class for a Csl formula tree with an And node as root.
*
- * Has two Abstract state formulas as sub formulas/trees.
+ * Has two Csl state formulas as sub formulas/trees.
*
- * As AND is commutative, the order is \e theoretically not important, but will influence the order in which
+ * As And is commutative, the order is \e theoretically not important, but will influence the order in which
* the model checker works.
*
- * 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)
+ * The object has shared ownership of its subtrees. If this object is deleted and no other object has a shared
+ * ownership of the subtrees they will be deleted as well.
*
* @see AbstractStateFormula
* @see AbstractCslFormula
@@ -57,29 +65,25 @@ class And : public AbstractStateFormula<T> {
public:
/*!
- * Empty constructor.
- * Will create an AND-node without subnotes. Will not represent a complete formula!
+ * Creates an And node without subnodes.
+ * The resulting object will not represent a complete formula!
*/
And() : left(nullptr), right(nullptr){
// Intentionally left empty.
}
/*!
- * Constructor.
- * Creates an AND note with the parameters as subtrees.
+ * Creates an And node with the parameters as subtrees.
*
- * @param left The left sub formula
- * @param right The right sub formula
+ * @param left The left sub formula.
+ * @param right The right sub formula.
*/
And(std::shared_ptr<AbstractStateFormula<T>> const & left, std::shared_ptr<AbstractStateFormula<T>> const & right) : left(left), right(right) {
// Intentionally left empty.
}
/*!
- * Destructor.
- *
- * The subtrees are deleted with the object
- * (this behavior can be prevented by setting them to NULL before deletion)
+ * Empty virtual destructor.
*/
virtual ~And() {
// Intentionally left empty.
@@ -88,16 +92,16 @@ public:
/*!
* Clones the called object.
*
- * Performs a "deep copy", i.e. the subtrees of the new object are clones of the original ones
+ * Performs a "deep copy", i.e. the subtrees of the new object are clones of the original ones.
*
- * @returns a new AND-object that is identical the called object.
+ * @returns A new And object that is a deep copy of the called object.
*/
virtual std::shared_ptr<AbstractStateFormula<T>> clone() const override {
std::shared_ptr<And<T>> result(new And());
- if (this->leftIsSet()) {
+ if (this->isLeftSet()) {
result->setLeft(left->clone());
}
- if (this->rightIsSet()) {
+ if (this->isRightSet()) {
result->setRight(right->clone());
}
return result;
@@ -117,7 +121,9 @@ public:
}
/*!
- * @returns a string representation of the formula
+ * Returns a textual representation of the formula tree with this node as root.
+ *
+ * @returns A string representing the formula tree.
*/
virtual std::string toString() const override {
std::string result = "(";
@@ -138,55 +144,65 @@ public:
}
/*!
- * Sets the left child node.
+ * Gets the left child node.
*
- * @param newLeft the new left child.
+ * @returns The left child node.
*/
- void setLeft(std::shared_ptr<AbstractStateFormula<T>> const & newLeft) {
- left = newLeft;
+ std::shared_ptr<AbstractStateFormula<T>> const & getLeft() const {
+ return left;
}
/*!
- * Sets the right child node.
+ * Gets the right child node.
*
- * @param newRight the new right child.
+ * @returns The right child node.
*/
- void setRight(std::shared_ptr<AbstractStateFormula<T>> const & newRight) {
- right = newRight;
+ std::shared_ptr<AbstractStateFormula<T>> const & getRight() const {
+ return right;
}
/*!
- * @returns a pointer to the left child node
+ * Sets the left child node.
+ *
+ * @param newLeft The new left child.
*/
- std::shared_ptr<AbstractStateFormula<T>> const & getLeft() const {
- return left;
+ void setLeft(std::shared_ptr<AbstractStateFormula<T>> const & newLeft) {
+ left = newLeft;
}
/*!
- * @returns a pointer to the right child node
+ * Sets the right child node.
+ *
+ * @param newRight The new right child.
*/
- std::shared_ptr<AbstractStateFormula<T>> const & getRight() const {
- return right;
+ void setRight(std::shared_ptr<AbstractStateFormula<T>> const & newRight) {
+ right = newRight;
}
/*!
+ * Checks if the left child is set, i.e. it does not point to null.
*
- * @return True if the left child is set, i.e. it does not point to nullptr; false otherwise
+ * @return True iff the left child is set.
*/
- bool leftIsSet() const {
+ bool isLeftSet() const {
return left.get() != nullptr;
}
/*!
+ * Checks if the right child is set, i.e. it does not point to null.
*
- * @return True if the right child is set, i.e. it does not point to nullptr; false otherwise
+ * @return True iff the right child is set.
*/
- bool rightIsSet() const {
+ bool isRightSet() const {
return right.get() != nullptr;
}
private:
+
+ // The left child node.
std::shared_ptr<AbstractStateFormula<T>> left;
+
+ // The right child node.
std::shared_ptr<AbstractStateFormula<T>> right;
};
diff --git a/src/formula/csl/Ap.h b/src/formula/csl/Ap.h
index a80f8fdfe..8ab7600fe 100644
--- a/src/formula/csl/Ap.h
+++ b/src/formula/csl/Ap.h
@@ -15,29 +15,37 @@ namespace storm {
namespace property {
namespace csl {
+// Forward declaration for the interface class.
template <class T> class Ap;
/*!
- * @brief Interface class for model checkers that support Ap.
+ * Interface class for model checkers that support Ap.
*
- * All model checkers that support the formula class Ap must inherit
- * this pure virtual class.
+ * All model checkers that support the formula class Ap must inherit
+ * this pure virtual class.
*/
template <class T>
class IApModelChecker {
public:
+
+ /*!
+ * Empty virtual destructor.
+ */
+ virtual ~IApModelChecker() {
+ // Intentionally left empty
+ }
+
/*!
- * @brief Evaluates Ap formula within a model checker.
- *
- * @param obj Formula object with subformulas.
- * @return Result of the formula for every node.
- */
+ * Evaluates an Ap formula within a model checker.
+ *
+ * @param obj Formula object with subformulas.
+ * @return The modelchecking result of the formula for every state.
+ */
virtual storm::storage::BitVector checkAp(const Ap<T>& obj) const = 0;
};
/*!
- * @brief
- * Class for an abstract formula tree with atomic proposition as root.
+ * Class for a Csl formula tree with an atomic proposition as root.
*
* This class represents the leaves in the formula tree.
*
@@ -50,19 +58,16 @@ class Ap : public AbstractStateFormula<T> {
public:
/*!
- * Constructor
+ * Creates a new atomic proposition leaf, with the given label.
*
- * Creates a new atomic proposition leaf, with the label Ap
- *
- * @param ap The string representing the atomic proposition
+ * @param ap A string representing the atomic proposition.
*/
- Ap(std::string ap) {
- this->ap = ap;
+ Ap(std::string ap) : ap(ap) {
+ // Intentionally left empty.
}
/*!
- * Destructor.
- * At this time, empty...
+ * Empty virtual destructor.
*/
virtual ~Ap() {
// Intentionally left empty
@@ -71,9 +76,9 @@ public:
/*!
* Clones the called object.
*
- * Performs a "deep copy", i.e. the subtrees of the new object are clones of the original ones
+ * Performs a "deep copy", i.e. the subtrees of the new object are clones of the original ones.
*
- * @returns a new AND-object that is identical the called object.
+ * @returns A new Ap object that is a deep copy of the called object.
*/
virtual std::shared_ptr<AbstractStateFormula<T>> clone() const override {
std::shared_ptr<AbstractStateFormula<T>> result(new Ap(this->getAp()));
@@ -93,6 +98,15 @@ public:
return modelChecker.template as<IApModelChecker>()->checkAp(*this);
}
+ /*!
+ * A string representing the atomic proposition.
+ *
+ * @returns A string representing the leaf.
+ */
+ virtual std::string toString() const override {
+ return getAp();
+ }
+
/*! Returns whether the formula is a propositional logic formula.
* That is, this formula and all its subformulas consist only of And, Or, Not and AP.
*
@@ -103,21 +117,17 @@ public:
}
/*!
- * @returns the name of the atomic proposition
+ * Gets the name of the atomic proposition.
+ *
+ * @returns The name of the atomic proposition.
*/
std::string const & getAp() const {
return ap;
}
- /*!
- * @returns a string representation of the leaf.
- *
- */
- virtual std::string toString() const override {
- return getAp();
- }
-
private:
+
+ // The atomic proposition referenced by this leaf.
std::string ap;
};
diff --git a/src/formula/csl/CslFilter.h b/src/formula/csl/CslFilter.h
index ef1ec5044..4d92829e5 100644
--- a/src/formula/csl/CslFilter.h
+++ b/src/formula/csl/CslFilter.h
@@ -16,45 +16,88 @@
#include "src/formula/actions/AbstractAction.h"
-namespace storm {
-namespace property {
-namespace action {
- template <typename T> class AbstractAction;
-}
-}
-}
-
namespace storm {
namespace property {
namespace csl {
+/*!
+ * This is the Csl specific filter.
+ *
+ * It maintains a Csl formula which can be checked against a given model by either calling evaluate() or check().
+ * Additionally it maintains a list of filter actions that are used to further manipulate the modelchecking results and prepare them for output.
+ */
template <class T>
class CslFilter : public storm::property::AbstractFilter<T> {
+ // Convenience typedef to make the code more readable.
typedef typename storm::property::action::AbstractAction<T>::Result Result;
public:
+ /*!
+ * Creates an empty CslFilter, maintaining no Csl formula.
+ *
+ * Calling check or evaluate will return an empty result.
+ */
CslFilter() : AbstractFilter<T>(UNDEFINED), child(nullptr), steadyStateQuery(false) {
// Intentionally left empty.
}
+ /*!
+ * Creates a CslFilter maintaining a Csl formula but containing no actions.
+ *
+ * The modelchecking result will be returned or printed as is.
+ *
+ * @param child The Csl formula to be maintained.
+ * @param opt An enum value indicating which kind of scheduler shall be used for path formulas on nondeterministic models.
+ * @param steadyStateQuery A flag indicating whether this is a steady state query.
+ */
CslFilter(std::shared_ptr<AbstractCslFormula<T>> const & child, OptimizingOperator opt = UNDEFINED, bool steadyStateQuery = false) : AbstractFilter<T>(opt), child(child), steadyStateQuery(steadyStateQuery) {
// Intentionally left empty.
}
+ /*!
+ * Creates a CslFilter maintaining a Csl formula and containing a single action.
+ *
+ * The given action will be applied to the modelchecking result during evaluation.
+ * Further actions can be added later.
+ *
+ * @param child The Csl formula to be maintained.
+ * @param action The single action to be executed during evaluation.
+ * @param opt An enum value indicating which kind of scheduler shall be used for path formulas on nondeterministic models.
+ * @param steadyStateQuery A flag indicating whether this is a steady state query.
+ */
CslFilter(std::shared_ptr<AbstractCslFormula<T>> const & child, std::shared_ptr<action::AbstractAction<T>> const & action, OptimizingOperator opt = UNDEFINED, bool steadyStateQuery = false) : AbstractFilter<T>(action, opt), child(child), steadyStateQuery(steadyStateQuery) {
// Intentionally left empty
}
+ /*!
+ * Creates a CslFilter using the given parameters.
+ *
+ * The given actions will be applied to the modelchecking result in ascending index order during evaluation.
+ * Further actions can be added later.
+ *
+ * @param child The Csl formula to be maintained.
+ * @param actions A vector conatining the actions that are to be executed during evaluation.
+ * @param opt An enum value indicating which kind of scheduler shall be used for path formulas on nondeterministic models.
+ * @param steadyStateQuery A flag indicating whether this is a steady state query.
+ */
CslFilter(std::shared_ptr<AbstractCslFormula<T>> const & child, std::vector<std::shared_ptr<action::AbstractAction<T>>> const & actions, OptimizingOperator opt = UNDEFINED, bool steadyStateQuery = false) : AbstractFilter<T>(actions, opt), child(child), steadyStateQuery(steadyStateQuery) {
// Intentionally left empty.
}
+ /*!
+ * Empty virtual destructor.
+ */
virtual ~CslFilter() {
// Intentionally left empty.
}
+ /*!
+ * Calls the modelchecker, retrieves the modelchecking result, applies the filter action one by one and prints out the result.
+ *
+ * @param modelchecker The modelchecker to be called.
+ */
void check(storm::modelchecker::csl::AbstractModelChecker<T> const & modelchecker) const {
// Write out the formula to be checked.
@@ -66,6 +109,12 @@ public:
}
+ /*!
+ * Calls the modelchecker, retrieves the modelchecking result, applies the filter action one by one and returns the result.
+ *
+ * @param modelchecker The modelchecker to be called.
+ * @returns The result of the sequential application of the filter actions to the modelchecking result.
+ */
Result evaluate(storm::modelchecker::csl::AbstractModelChecker<T> const & modelchecker) const {
Result result;
@@ -83,6 +132,13 @@ public:
return result;
}
+ /*!
+ * Returns a textual representation of the filter.
+ *
+ * That includes the actions as well as the maintained formula.
+ *
+ * @returns A string representing the filter.
+ */
virtual std::string toString() const override {
std::string desc = "";
@@ -170,30 +226,50 @@ public:
return desc;
}
- virtual std::string toPrettyString() const override{
- std::string desc = "Filter: ";
- desc += "\nActions:";
- for(auto action : this->actions) {
- desc += "\n\t" + action->toString();
- }
- desc += "\nFormula:\n\t" + child->toString();
- return desc;
+ /*!
+ * Gets the child node.
+ *
+ * @returns The child node.
+ */
+ std::shared_ptr<AbstractCslFormula<T>> const & getChild() const {
+ return child;
}
+ /*!
+ * Sets the subtree.
+ *
+ * @param child The new child.
+ */
void setChild(std::shared_ptr<AbstractCslFormula<T>> const & child) {
this->child = child;
}
- std::shared_ptr<AbstractCslFormula<T>> const & getChild() const {
- return child;
+ /*!
+ * Checks if the child is set, i.e. it does not point to null.
+ *
+ * @return True iff the child is set.
+ */
+ bool isChildSet() const {
+ return child.get() != nullptr;
}
private:
+ /*!
+ * Calls the modelchecker for a state formula, retrieves the modelchecking result, applies the filter action one by one and returns the result.
+ *
+ * This an internal version of the evaluate method overloading it for the different Csl formula types.
+ *
+ * @param modelchecker The modelchecker to be called.
+ * @param formula The state formula for which the modelchecker will be called.
+ * @returns The result of the sequential application of the filter actions to the modelchecking result.
+ */
Result evaluate(storm::modelchecker::csl::AbstractModelChecker<T> const & modelchecker, std::shared_ptr<AbstractStateFormula<T>> const & formula) const {
// First, get the model checking result.
Result result;
+ //TODO: Once a modelchecker supporting steady state formulas is implemented, call it here in case steadyStateQuery is set.
+
if(this->opt != UNDEFINED) {
// If there is an action specifying that min/max probabilities should be computed, call the appropriate method of the model checker.
result.stateResult = modelchecker.checkMinMaxOperator(*formula, this->opt == MINIMIZE ? true : false);
@@ -206,6 +282,15 @@ private:
return evaluateActions(result, modelchecker);
}
+ /*!
+ * Calls the modelchecker for a path formula, retrieves the modelchecking result, applies the filter action one by one and returns the result.
+ *
+ * This an internal version of the evaluate method overloading it for the different Csl formula types.
+ *
+ * @param modelchecker The modelchecker to be called.
+ * @param formula The path formula for which the modelchecker will be called.
+ * @returns The result of the sequential application of the filter actions to the modelchecking result.
+ */
Result evaluate(storm::modelchecker::csl::AbstractModelChecker<T> const & modelchecker, std::shared_ptr<AbstractPathFormula<T>> const & formula) const {
// First, get the model checking result.
Result result;
@@ -221,6 +306,13 @@ private:
return evaluateActions(result, modelchecker);
}
+ /*!
+ * Evaluates the filter actions by calling them one by one using the output of each action as the input for the next one.
+ *
+ * @param input The modelchecking result in form of a Result struct.
+ * @param modelchecker The modelchecker that was called to generate the modelchecking result. Needed by some actions.
+ * @returns The result of the sequential application of the filter actions to the modelchecking result.
+ */
Result evaluateActions(Result result, storm::modelchecker::csl::AbstractModelChecker<T> const & modelchecker) const {
// Init the state selection and state map vectors.
@@ -238,6 +330,12 @@ private:
return result;
}
+ /*!
+ * Writes out the given result.
+ *
+ * @param result The result of the sequential application of the filter actions to a modelchecking result.
+ * @param modelchecker The modelchecker that was called to generate the modelchecking result. Needed for legacy support.
+ */
void writeOut(Result const & result, storm::modelchecker::csl::AbstractModelChecker<T> const & modelchecker) const {
// Test if there is anything to write out.
@@ -302,8 +400,10 @@ private:
std::cout << std::endl << "-------------------------------------------" << std::endl;
}
+ // The Csl formula maintained by this filter.
std::shared_ptr<AbstractCslFormula<T>> child;
+ // A flag indicating whether this is a steady state query.
bool steadyStateQuery;
};
diff --git a/src/formula/csl/Eventually.h b/src/formula/csl/Eventually.h
index 21bdd71b4..6c27dfa75 100644
--- a/src/formula/csl/Eventually.h
+++ b/src/formula/csl/Eventually.h
@@ -1,5 +1,5 @@
/*
- * Next.h
+ * Globally.h
*
* Created on: 26.12.2012
* Author: Christian Dehnert
@@ -16,37 +16,48 @@ namespace storm {
namespace property {
namespace csl {
+// Forward declaration for the interface class.
template <class T> class Eventually;
/*!
- * @brief Interface class for model checkers that support Eventually.
+ * Interface class for model checkers that support Eventually.
*
- * All model checkers that support the formula class Eventually must inherit
- * this pure virtual class.
+ * All model checkers that support the formula class Eventually must inherit
+ * this pure virtual class.
*/
template <class T>
class IEventuallyModelChecker {
public:
+
/*!
- * @brief Evaluates Eventually formula within a model checker.
- *
- * @param obj Formula object with subformulas.
- * @return Result of the formula for every node.
- */
+ * Empty virtual destructor.
+ */
+ virtual ~IEventuallyModelChecker() {
+ // Intentionally left empty.
+ }
+
+ /*!
+ * Evaluates an Eventually formula within a model checker.
+ *
+ * @param obj Formula object with subformulas.
+ * @param qualitative A flag indicating whether the formula only needs to be evaluated qualitatively, i.e. if the
+ * results are only compared against the bounds 0 and 1.
+ * @return The modelchecking result of the formula for every state.
+ */
virtual std::vector<T> checkEventually(const Eventually<T>& obj, bool qualitative) const = 0;
};
/*!
* @brief
- * Class for an abstract (path) formula tree with an Eventually node as root.
+ * Class for a Csl (path) formula tree with an Eventually node as root.
*
- * Has one Abstract state formula as sub formula/tree.
+ * Has one Csl state formula as sub formula/tree.
*
* @par Semantics
- * The formula holds iff eventually \e child holds.
+ * The formula holds iff eventually formula \e child holds.
*
- * The subtree is seen as part of the object and deleted with the object
- * (this behavior can be prevented by setting them to nullptr before deletion)
+ * The object has shared ownership of its subtree. If this object is deleted and no other object has a shared
+ * ownership of the subtree it will be deleted as well.
*
* @see AbstractPathFormula
* @see AbstractCslFormula
@@ -57,26 +68,24 @@ class Eventually : public AbstractPathFormula<T> {
public:
/*!
- * Empty constructor
+ * Creates an Eventually node without a subnode.
+ * The resulting object will not represent a complete formula!
*/
Eventually() : child(nullptr) {
// Intentionally left empty.
}
/*!
- * Constructor
+ * Creates an Eventually node using the given parameter.
*
- * @param child The child node
+ * @param child The child formula subtree.
*/
Eventually(std::shared_ptr<AbstractStateFormula<T>> const & child) : child(child){
// Intentionally left empty.
}
/*!
- * Constructor.
- *
- * Also deletes the subtree.
- * (this behaviour can be prevented by setting the subtrees to nullptr before deletion)
+ * Empty virtual destructor.
*/
virtual ~Eventually() {
// Intentionally left empty.
@@ -85,13 +94,13 @@ public:
/*!
* Clones the called object.
*
- * Performs a "deep copy", i.e. the subtrees of the new object are clones of the original ones
+ * Performs a "deep copy", i.e. the subnodes of the new object are clones of the original ones.
*
- * @returns a new Eventually-object that is identical the called object.
+ * @returns A new Eventually object that is a deep copy of the called object.
*/
virtual std::shared_ptr<AbstractPathFormula<T>> clone() const override {
std::shared_ptr<Eventually<T>> result(new Eventually<T>());
- if (this->childIsSet()) {
+ if (this->isChildSet()) {
result->setChild(child->clone());
}
return result;
@@ -111,7 +120,9 @@ public:
}
/*!
- * @returns a string representation of the formula
+ * Returns a textual representation of the formula tree with this node as root.
+ *
+ * @returns A string representing the formula tree.
*/
virtual std::string toString() const override {
std::string result = "F ";
@@ -120,29 +131,35 @@ public:
}
/*!
- * @returns the child node
+ * Gets the child node.
+ *
+ * @returns The child node.
*/
std::shared_ptr<AbstractStateFormula<T>> const & getChild() const {
return child;
}
/*!
- * Sets the subtree
- * @param child the new child node
+ * Sets the subtree.
+ *
+ * @param child The new child.
*/
void setChild(std::shared_ptr<AbstractStateFormula<T>> const & child) {
this->child = child;
}
/*!
+ * Checks if the child is set, i.e. it does not point to null.
*
- * @return True if the child node is set, i.e. it does not point to nullptr; false otherwise
+ * @return True iff the child is set.
*/
- bool childIsSet() const {
+ bool isChildSet() const {
return child.get() != nullptr;
}
private:
+
+ // The child node.
std::shared_ptr<AbstractStateFormula<T>> child;
};
diff --git a/src/formula/csl/Globally.h b/src/formula/csl/Globally.h
index e93baeca5..421d9e354 100644
--- a/src/formula/csl/Globally.h
+++ b/src/formula/csl/Globally.h
@@ -1,5 +1,5 @@
/*
- * Next.h
+ * Globally.h
*
* Created on: 26.12.2012
* Author: Christian Dehnert
@@ -16,37 +16,47 @@ namespace storm {
namespace property {
namespace csl {
+// Forward declaration for the interface class.
template <class T> class Globally;
/*!
- * @brief Interface class for model checkers that support Globally.
+ * Interface class for model checkers that support Globally.
*
- * All model checkers that support the formula class Globally must inherit
- * this pure virtual class.
+ * All model checkers that support the formula class Globally must inherit
+ * this pure virtual class.
*/
template <class T>
class IGloballyModelChecker {
public:
+
/*!
- * @brief Evaluates Globally formula within a model checker.
- *
- * @param obj Formula object with subformulas.
- * @return Result of the formula for every node.
- */
+ * Empty virtual destructor.
+ */
+ virtual ~IGloballyModelChecker() {
+ // Intentionally left empty
+ }
+
+ /*!
+ * Evaluates a Globally formula within a model checker.
+ *
+ * @param obj Formula object with subformulas.
+ * @param qualitative A flag indicating whether the formula only needs to be evaluated qualitatively, i.e. if the
+ * results are only compared against the bounds 0 and 1.
+ * @return The modelchecking result of the formula for every state.
+ */
virtual std::vector<T> checkGlobally(const Globally<T>& obj, bool qualitative) const = 0;
};
/*!
- * @brief
- * Class for an abstract (path) formula tree with a Globally node as root.
+ * Class for a Csl (path) formula tree with a Globally node as root.
*
- * Has one Abstract state formula as sub formula/tree.
+ * Has one Csl state formula as sub formula/tree.
*
* @par Semantics
* The formula holds iff globally \e child holds.
*
- * The subtree is seen as part of the object and deleted with the object
- * (this behavior can be prevented by setting them to nullptr before deletion)
+ * The object has shared ownership of its subtree. If this object is deleted and no other object has a shared
+ * ownership of the subtree it will be deleted as well.
*
* @see AbstractPathFormula
* @see AbstractCslFormula
@@ -57,26 +67,24 @@ class Globally : public AbstractPathFormula<T> {
public:
/*!
- * Empty constructor
+ * Creates a Globally node without a subnode.
+ * The resulting object will not represent a complete formula!
*/
Globally() : child(nullptr){
// Intentionally left empty.
}
/*!
- * Constructor
+ * Creates a Globally node using the given parameter.
*
- * @param child The child node
+ * @param child The child formula subtree.
*/
Globally(std::shared_ptr<AbstractStateFormula<T>> const & child) : child(child){
// Intentionally left empty.
}
/*!
- * Constructor.
- *
- * Also deletes the subtree.
- * (this behaviour can be prevented by setting the subtrees to nullptr before deletion)
+ * Empty virtual destructor.
*/
virtual ~Globally() {
// Intentionally left empty.
@@ -85,13 +93,13 @@ public:
/*!
* Clones the called object.
*
- * Performs a "deep copy", i.e. the subtrees of the new object are clones of the original ones
+ * Performs a "deep copy", i.e. the subnodes of the new object are clones of the original ones.
*
- * @returns a new Globally-object that is identical the called object.
+ * @returns A new Globally object that is a deep copy of the called object.
*/
virtual std::shared_ptr<AbstractPathFormula<T>> clone() const override {
std::shared_ptr<Globally<T>> result(new Globally<T>());
- if (this->childIsSet()) {
+ if (this->isChildSet()) {
result->setChild(child->clone());
}
return result;
@@ -111,7 +119,9 @@ public:
}
/*!
- * @returns a string representation of the formula
+ * Returns a textual representation of the formula tree with this node as root.
+ *
+ * @returns A string representing the formula tree.
*/
virtual std::string toString() const override {
std::string result = "G ";
@@ -120,29 +130,35 @@ public:
}
/*!
- * @returns the child node
+ * Gets the child node.
+ *
+ * @returns The child node.
*/
AbstractStateFormula<T> const & getChild() const {
return child;
}
/*!
- * Sets the subtree
- * @param child the new child node
+ * Sets the subtree.
+ *
+ * @param child The new child.
*/
void setChild(std::shared_ptr<AbstractStateFormula<T>> const & child) {
this->child = child;
}
/*!
+ * Checks if the child is set, i.e. it does not point to null.
*
- * @return True if the child node is set, i.e. it does not point to nullptr; false otherwise
+ * @return True iff the child is set.
*/
- bool childIsSet() const {
+ bool isChildSet() const {
return child.get() != nullptr;
}
private:
+
+ // The child node.
std::shared_ptr<AbstractStateFormula<T>> child;
};
diff --git a/src/formula/csl/Next.h b/src/formula/csl/Next.h
index 8c86095b8..478247de6 100644
--- a/src/formula/csl/Next.h
+++ b/src/formula/csl/Next.h
@@ -15,37 +15,47 @@ namespace storm {
namespace property {
namespace csl {
+// Forward declaration for the interface class.
template <class T> class Next;
/*!
- * @brief Interface class for model checkers that support Next.
+ * Interface class for model checkers that support Next.
*
- * All model checkers that support the formula class Next must inherit
- * this pure virtual class.
+ * All model checkers that support the formula class Next must inherit
+ * this pure virtual class.
*/
template <class T>
class INextModelChecker {
public:
+
/*!
- * @brief Evaluates Next formula within a model checker.
- *
- * @param obj Formula object with subformulas.
- * @return Result of the formula for every node.
- */
+ * Empty virtual destructor.
+ */
+ virtual ~INextModelChecker() {
+ // Intentionally left empty
+ }
+
+ /*!
+ * Evaluates Next formula within a model checker.
+ *
+ * @param obj Formula object with subformulas.
+ * @param qualitative A flag indicating whether the formula only needs to be evaluated qualitatively, i.e. if the
+ * results are only compared against the bounds 0 and 1.
+ * @return Result of the formula for every node.
+ */
virtual std::vector<T> checkNext(const Next<T>& obj, bool qualitative) const = 0;
};
/*!
- * @brief
- * Class for an abstract (path) formula tree with a Next node as root.
+ * Class for a Csl (path) formula tree with a Next node as root.
*
- * Has two Abstract state formulas as sub formulas/trees.
+ * Has two Csl state formulas as sub formulas/trees.
*
* @par Semantics
* The formula holds iff in the next step, \e child holds
*
- * The subtree is seen as part of the object and deleted with the object
- * (this behavior can be prevented by setting them to NULL before deletion)
+ * The object has shared ownership of its subtree. If this object is deleted and no other object has a shared
+ * ownership of the subtree it will be deleted as well.
*
* @see AbstractPathFormula
* @see AbstractCslFormula
@@ -56,26 +66,24 @@ class Next : public AbstractPathFormula<T> {
public:
/*!
- * Empty constructor
+ * Creates a Next node without a subnode.
+ * The resulting object will not represent a complete formula!
*/
Next() : child(nullptr){
// Intentionally left empty.
}
/*!
- * Constructor
+ * Creates a Next node using the given parameter.
*
- * @param child The child node
+ * @param child The child formula subtree.
*/
Next(std::shared_ptr<AbstractStateFormula<T>> const & child) : child(child) {
// Intentionally left empty.
}
/*!
- * Constructor.
- *
- * Also deletes the subtree.
- * (this behavior can be prevented by setting the subtrees to NULL before deletion)
+ * Empty virtual destructor.
*/
virtual ~Next() {
// Intetionally left empty.
@@ -84,13 +92,13 @@ public:
/*!
* Clones the called object.
*
- * Performs a "deep copy", i.e. the subtrees of the new object are clones of the original ones
+ * Performs a "deep copy", i.e. the subnodes of the new object are clones of the original ones.
*
- * @returns a new BoundedUntil-object that is identical the called object.
+ * @returns A new Next object that is a deep copy of the called object.
*/
virtual std::shared_ptr<AbstractPathFormula<T>> clone() const override {
std::shared_ptr<Next<T>> result(new Next<T>());
- if (this->childIsSet()) {
+ if (this->isChildSet()) {
result->setChild(child->clone());
}
return result;
@@ -110,7 +118,9 @@ public:
}
/*!
- * @returns a string representation of the formula
+ * Returns a textual representation of the formula tree with this node as root.
+ *
+ * @returns A string representing the formula tree.
*/
virtual std::string toString() const override {
std::string result = "X ";
@@ -119,29 +129,35 @@ public:
}
/*!
- * @returns the child node
+ * Gets the child node.
+ *
+ * @returns The child node.
*/
std::shared_ptr<AbstractStateFormula<T>> const & getChild() const {
return child;
}
/*!
- * Sets the subtree
- * @param child the new child node
+ * Sets the subtree.
+ *
+ * @param child The new child.
*/
void setChild(std::shared_ptr<AbstractStateFormula<T>> const & child) {
this->child = child;
}
/*!
+ * Checks if the child is set, i.e. it does not point to null.
*
- * @return True if the child node is set, i.e. it does not point to nullptr; false otherwise
+ * @return True iff the child is set.
*/
- bool childIsSet() const {
+ bool isChildSet() const {
return child.get() != nullptr;
}
private:
+
+ // The child node.
std::shared_ptr<AbstractStateFormula<T>> child;
};
diff --git a/src/formula/csl/Not.h b/src/formula/csl/Not.h
index 9c23323ce..5e382893d 100644
--- a/src/formula/csl/Not.h
+++ b/src/formula/csl/Not.h
@@ -15,34 +15,42 @@ namespace storm {
namespace property {
namespace csl {
+// Forward declaration for the interface class.
template <class T> class Not;
/*!
- * @brief Interface class for model checkers that support Not.
+ * Interface class for model checkers that support Not.
*
- * All model checkers that support the formula class Not must inherit
- * this pure virtual class.
+ * All model checkers that support the formula class Not must inherit
+ * this pure virtual class.
*/
template <class T>
class INotModelChecker {
public:
+
/*!
- * @brief Evaluates Not formula within a model checker.
- *
- * @param obj Formula object with subformulas.
- * @return Result of the formula for every node.
- */
+ * Empty virtual destructor.
+ */
+ virtual ~INotModelChecker() {
+ // Intentionally left empty
+ }
+
+ /*!
+ * Evaluates Not formulas within a model checker.
+ *
+ * @param obj Formula object with subformulas.
+ * @return Result of the formula for every node.
+ */
virtual storm::storage::BitVector checkNot(const Not<T>& obj) const = 0;
};
/*!
- * @brief
- * Class for an abstract formula tree with NOT node as root.
+ * Class for a Csl formula tree with Not node as root.
*
- * Has one Abstract state formula as sub formula/tree.
+ * Has one Csl state formula as sub formula/tree.
*
- * The subtree is seen as part of the object and deleted with the object
- * (this behavior can be prevented by setting them to NULL before deletion)
+ * The object has shared ownership of its subtree. If this object is deleted and no other object has a shared
+ * ownership of the subtree it will be deleted as well.
*
* @see AbstractStateFormula
* @see AbstractCslFormula
@@ -53,25 +61,24 @@ class Not : public AbstractStateFormula<T> {
public:
/*!
- * Empty constructor
+ * Creates a Not node without a subnode.
+ * The resulting object will not represent a complete formula!
*/
Not() : child(nullptr) {
// Intentionally left empty.
}
/*!
- * Constructor
- * @param child The child node
+ * Creates a Not node using the given parameter.
+ *
+ * @param child The child formula subtree.
*/
Not(std::shared_ptr<AbstractStateFormula<T>> const & child) : child(child) {
// Intentionally left empty.
}
/*!
- * Destructor
- *
- * Also deletes the subtree
- * (this behavior can be prevented by setting them to NULL before deletion)
+ * Empty virtual destructor.
*/
virtual ~Not() {
// Intentionally left empty.
@@ -80,13 +87,13 @@ public:
/*!
* Clones the called object.
*
- * Performs a "deep copy", i.e. the subtrees of the new object are clones of the original ones
+ * Performs a "deep copy", i.e. the subnodes of the new object are clones of the original ones.
*
- * @returns a new AND-object that is identical the called object.
+ * @returns A new Not object that is a deep copy of the called object.
*/
virtual std::shared_ptr<AbstractStateFormula<T>> clone() const override {
std::shared_ptr<Not<T>> result(new Not<T>());
- if (this->childIsSet()) {
+ if (this->isChildSet()) {
result->setChild(child->clone());
}
return result;
@@ -106,7 +113,9 @@ public:
}
/*!
- * @returns a string representation of the formula
+ * Returns a textual representation of the formula tree with this node as root.
+ *
+ * @returns A string representing the formula tree.
*/
virtual std::string toString() const override {
std::string result = "!";
@@ -124,29 +133,35 @@ public:
}
/*!
- * @returns The child node
+ * Gets the child node.
+ *
+ * @returns The child node.
*/
std::shared_ptr<AbstractStateFormula<T>> const & getChild() const {
return child;
}
/*!
- * Sets the subtree
- * @param child the new child node
+ * Sets the subtree.
+ *
+ * @param child The new child.
*/
void setChild(std::shared_ptr<AbstractStateFormula<T>> const & child) {
this->child = child;
}
/*!
+ * Checks if the child is set, i.e. it does not point to null.
*
- * @return True if the child node is set, i.e. it does not point to nullptr; false otherwise
+ * @return True iff the child is set.
*/
- bool childIsSet() const {
+ bool isChildSet() const {
return child.get() != nullptr;
}
private:
+
+ // The child node.
std::shared_ptr<AbstractStateFormula<T>> child;
};
diff --git a/src/formula/csl/Or.h b/src/formula/csl/Or.h
index b6017d4be..d1c1a795c 100644
--- a/src/formula/csl/Or.h
+++ b/src/formula/csl/Or.h
@@ -14,37 +14,45 @@ namespace storm {
namespace property {
namespace csl {
+// Forward declaration for the interface class.
template <class T> class Or;
/*!
- * @brief Interface class for model checkers that support Or.
+ * Interface class for model checkers that support Or.
*
- * All model checkers that support the formula class Or must inherit
- * this pure virtual class.
+ * All model checkers that support the formula class Or must inherit
+ * this pure virtual class.
*/
template <class T>
class IOrModelChecker {
public:
+
/*!
- * @brief Evaluates Or formula within a model checker.
- *
- * @param obj Formula object with subformulas.
- * @return Result of the formula for every node.
- */
+ * Empty virtual destructor.
+ */
+ virtual ~IOrModelChecker() {
+ // Intentionally left empty
+ }
+
+ /*!
+ * Evaluates Or formula within a model checker.
+ *
+ * @param obj Formula object with subformulas.
+ * @return Result of the formula for every node.
+ */
virtual storm::storage::BitVector checkOr(const Or<T>& obj) const = 0;
};
/*!
- * @brief
- * Class for an abstract formula tree with OR node as root.
+ * Class for an Csl formula tree with an Or node as root.
*
- * Has two Abstract state formulas as sub formulas/trees.
+ * Has two state formulas as sub formulas/trees.
*
- * As OR is commutative, the order is \e theoretically not important, but will influence the order in which
+ * As Or is commutative, the order is \e theoretically not important, but will influence the order in which
* the model checker works.
*
- * 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)
+ * The object has shared ownership of its subtrees. If this object is deleted and no other object has a shared
+ * ownership of the subtrees they will be deleted as well.
*
* @see AbstractStateFormula
* @see AbstractCslFormula
@@ -55,47 +63,43 @@ class Or : public AbstractStateFormula<T> {
public:
/*!
- * Empty constructor.
- * Will create an OR-node without subnotes. Will not represent a complete formula!
- */
- Or() : left(nullptr), right(nullptr) {
- // Intentionally left empty.
- }
+ * Creates an Or node without subnodes.
+ * The resulting object will not represent a complete formula!
+ */
+ Or() : left(nullptr), right(nullptr) {
+ // Intentionally left empty.
+ }
- /*!
- * Constructor.
- * Creates an OR note with the parameters as subtrees.
- *
- * @param left The left sub formula
- * @param right The right sub formula
- */
- Or(std::shared_ptr<AbstractStateFormula<T>> const & left, std::shared_ptr<AbstractStateFormula<T>> const & right) : left(left), right(right) {
- // Intentionally left empty.
- }
+ /*!
+ * Creates an Or node with the parameters as subtrees.
+ *
+ * @param left The left sub formula.
+ * @param right The right sub formula.
+ */
+ Or(std::shared_ptr<AbstractStateFormula<T>> const & left, std::shared_ptr<AbstractStateFormula<T>> const & right) : left(left), right(right) {
+ // Intentionally left empty.
+ }
- /*!
- * Destructor.
- *
- * The subtrees are deleted with the object
- * (this behavior can be prevented by setting them to NULL before deletion)
- */
- virtual ~Or() {
- // Intentionally left empty.
- }
+ /*!
+ * Empty virtual destructor.
+ */
+ virtual ~Or() {
+ // Intentionally left empty.
+ }
/*!
* Clones the called object.
*
- * Performs a "deep copy", i.e. the subtrees of the new object are clones of the original ones
+ * Performs a "deep copy", i.e. the subtrees of the new object are clones of the original ones.
*
- * @returns a new AND-object that is identical the called object.
+ * @returns A new Or object that is a deep copy of the called object.
*/
virtual std::shared_ptr<AbstractStateFormula<T>> clone() const override {
std::shared_ptr<Or<T>> result(new Or());
- if (this->leftIsSet()) {
+ if (this->isLeftSet()) {
result->setLeft(left->clone());
}
- if (this->rightIsSet()) {
+ if (this->isRightSet()) {
result->setRight(right->clone());
}
return result;
@@ -115,7 +119,9 @@ public:
}
/*!
- * @returns a string representation of the formula
+ * Returns a textual representation of the formula tree with this node as root.
+ *
+ * @returns A string representing the formula tree.
*/
virtual std::string toString() const override {
std::string result = "(";
@@ -136,55 +142,65 @@ public:
}
/*!
- * Sets the left child node.
+ * Gets the left child node.
*
- * @param newLeft the new left child.
+ * @returns The left child node.
*/
- void setLeft(std::shared_ptr<AbstractStateFormula<T>> const & newLeft) {
- left = newLeft;
+ std::shared_ptr<AbstractStateFormula<T>> const & getLeft() const {
+ return left;
}
/*!
- * Sets the right child node.
+ * Gets the right child node.
*
- * @param newRight the new right child.
+ * @returns The right child node.
*/
- void setRight(std::shared_ptr<AbstractStateFormula<T>> const & newRight) {
- right = newRight;
+ std::shared_ptr<AbstractStateFormula<T>> const & getRight() const {
+ return right;
}
/*!
- * @returns a pointer to the left child node
+ * Sets the left child node.
+ *
+ * @param newLeft The new left child.
*/
- std::shared_ptr<AbstractStateFormula<T>> const & getLeft() const {
- return left;
+ void setLeft(std::shared_ptr<AbstractStateFormula<T>> const & newLeft) {
+ left = newLeft;
}
/*!
- * @returns a pointer to the right child node
+ * Sets the right child node.
+ *
+ * @param newRight The new right child.
*/
- std::shared_ptr<AbstractStateFormula<T>> const & getRight() const {
- return right;
+ void setRight(std::shared_ptr<AbstractStateFormula<T>> const & newRight) {
+ right = newRight;
}
/*!
+ * Checks if the left child is set, i.e. it does not point to null.
*
- * @return True if the left child is set, i.e. it does not point to nullptr; false otherwise
+ * @return True iff the left child is set.
*/
- bool leftIsSet() const {
+ bool isLeftSet() const {
return left.get() != nullptr;
}
/*!
+ * Checks if the right child is set, i.e. it does not point to null.
*
- * @return True if the right child is set, i.e. it does not point to nullptr; false otherwise
+ * @return True iff the left right is set.
*/
- bool rightIsSet() const {
+ bool isRightSet() const {
return right.get() != nullptr;
}
private:
+
+ // The left child node.
std::shared_ptr<AbstractStateFormula<T>> left;
+
+ // The right child node.
std::shared_ptr<AbstractStateFormula<T>> right;
};
diff --git a/src/formula/csl/ProbabilisticBoundOperator.h b/src/formula/csl/ProbabilisticBoundOperator.h
index f0c51af72..a9adc4d6b 100644
--- a/src/formula/csl/ProbabilisticBoundOperator.h
+++ b/src/formula/csl/ProbabilisticBoundOperator.h
@@ -17,39 +17,49 @@ namespace storm {
namespace property {
namespace csl {
+// Forward declaration for the interface class.
template <class T> class ProbabilisticBoundOperator;
/*!
- * @brief Interface class for model checkers that support ProbabilisticBoundOperator.
+ * Interface class for model checkers that support ProbabilisticBoundOperator.
*
- * All model checkers that support the formula class PathBoundOperator must inherit
- * this pure virtual class.
+ * All model checkers that support the formula class PathBoundOperator must inherit
+ * this pure virtual class.
*/
template <class T>
class IProbabilisticBoundOperatorModelChecker {
public:
+
+ /*!
+ * Empty virtual destructor.
+ */
+ virtual ~IProbabilisticBoundOperatorModelChecker() {
+ // Intentionally left empty
+ }
+
+ /*!
+ * Evaluates a ProbabilisticBoundOperator within a model checker.
+ *
+ * @param obj Formula object with subformulas.
+ * @return The modelchecking result of the formula for every state.
+ */
virtual storm::storage::BitVector checkProbabilisticBoundOperator(const ProbabilisticBoundOperator<T>& obj) const = 0;
};
/*!
- * @brief
- * Class for an abstract formula tree with a P (probablistic) operator node over a probability interval
- * as root.
+ * Class for a Csl formula tree with a P (probablistic) bound operator node as root.
*
- * Has one Abstract path formula as sub formula/tree.
+ * Has one path formula as sub formula/tree.
*
* @par Semantics
- * The formula holds iff the probability that the path formula holds is inside the bounds
+ * The formula holds iff the probability that the path formula holds meets the bound
* specified in this operator
*
- * 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)
- *
+ * The object has shared ownership of its subtree. If this object is deleted and no other object has a shared
+ * ownership of the subtree it will be deleted as well.
*
* @see AbstractStateFormula
* @see AbstractPathFormula
- * @see ProbabilisticOperator
- * @see ProbabilisticNoBoundsOperator
* @see AbstractCslFormula
*/
template<class T>
@@ -58,18 +68,19 @@ class ProbabilisticBoundOperator : public AbstractStateFormula<T> {
public:
/*!
- * Empty constructor
+ * Creates a ProbabilisticBoundOperator node without a subnode.
+ * The resulting object will not represent a complete formula!
*/
ProbabilisticBoundOperator() : comparisonOperator(LESS), bound(0), child(nullptr) {
// Intentionally left empty.
}
/*!
- * Constructor for non-optimizing operator.
+ * Creates a ProbabilisticBoundOperator node using the given parameters.
*
* @param comparisonOperator The relation for the bound.
- * @param bound The bound for the probability
- * @param child The child node
+ * @param bound The bound for the probability.
+ * @param child The child formula subtree.
*/
ProbabilisticBoundOperator(storm::property::ComparisonType comparisonOperator, T bound, std::shared_ptr<AbstractPathFormula<T>> const & child)
: comparisonOperator(comparisonOperator), bound(bound), child(child) {
@@ -77,10 +88,7 @@ public:
}
/*!
- * Destructor
- *
- * The subtree is deleted with the object
- * (this behavior can be prevented by setting them to NULL before deletion)
+ * Empty virtual destructor.
*/
virtual ~ProbabilisticBoundOperator() {
// Intentionally left empty.
@@ -89,9 +97,9 @@ public:
/*!
* Clones the called object.
*
- * Performs a "deep copy", i.e. the subtrees of the new object are clones of the original ones
+ * Performs a "deep copy", i.e. the subnodes of the new object are clones of the original ones.
*
- * @returns a new AND-object that is identical the called object.
+ * @returns A new ProbabilisticBoundOperator object that is a deep copy of the called object.
*/
virtual std::shared_ptr<AbstractStateFormula<T>> clone() const override {
std::shared_ptr<ProbabilisticBoundOperator<T>> result(new ProbabilisticBoundOperator<T>());
@@ -115,7 +123,9 @@ public:
}
/*!
- * @returns a string representation of the formula
+ * Returns a textual representation of the formula tree with this node as root.
+ *
+ * @returns A string representing the formula tree.
*/
virtual std::string toString() const override {
std::string result = "P ";
@@ -134,56 +144,74 @@ public:
}
/*!
- * @returns the child node (representation of a formula)
+ * Gets the child node.
+ *
+ * @returns The child node.
*/
std::shared_ptr<AbstractPathFormula<T>> const & getChild () const {
return child;
}
/*!
- * Sets the child node
+ * Sets the subtree.
*
- * @param child the path formula that becomes the new child node
+ * @param child The new child.
*/
void setChild(std::shared_ptr<AbstractPathFormula<T>> const & child) {
this->child = child;
}
/*!
+ * Checks if the child is set, i.e. it does not point to null.
*
- * @return True if the path formula is set, i.e. it does not point to nullptr; false otherwise
+ * @return True iff the child is set.
*/
- bool childIsSet() const {
+ bool isChildSet() const {
return child.get() != nullptr;
}
/*!
- * @returns the comparison relation
+ * Gets the comparison operator.
+ *
+ * @returns An enum value representing the comparison relation.
*/
storm::property::ComparisonType const getComparisonOperator() const {
return comparisonOperator;
}
+ /*!
+ * Sets the comparison operator.
+ *
+ * @param comparisonOperator An enum value representing the new comparison relation.
+ */
void setComparisonOperator(storm::property::ComparisonType comparisonOperator) {
this->comparisonOperator = comparisonOperator;
}
/*!
- * @returns the bound for the measure
+ * Gets the bound which the probability that the path formula holds has to obey.
+ *
+ * @returns The probability bound.
*/
T const & getBound() const {
return bound;
}
/*!
- * Sets the interval in which the probability that the path formula holds may lie in.
+ * Sets the bound which the probability that the path formula holds has to obey.
*
- * @param bound The bound for the measure
+ * @param bound The new probability bound.
*/
void setBound(T const & bound) {
this->bound = bound;
}
+ /*!
+ * Checks if the bound is met by the given value.
+ *
+ * @param value The value to test against the bound.
+ * @returns True iff value <comparisonOperator> bound holds.
+ */
bool meetsBound(T const & value) const {
switch (comparisonOperator) {
case LESS: return value < bound; break;
@@ -195,8 +223,14 @@ public:
}
private:
+
+ // The operator used to indicate the kind of bound that is to be met.
storm::property::ComparisonType comparisonOperator;
+
+ // The probability bound.
T bound;
+
+ // The path formula for which the probability to be satisfied has to meet the bound.
std::shared_ptr<AbstractPathFormula<T>> child;
};
diff --git a/src/formula/csl/SteadyStateBoundOperator.h b/src/formula/csl/SteadyStateBoundOperator.h
index 3c664f05a..4ca8a2cba 100644
--- a/src/formula/csl/SteadyStateBoundOperator.h
+++ b/src/formula/csl/SteadyStateBoundOperator.h
@@ -15,37 +15,45 @@ namespace storm {
namespace property {
namespace csl {
+// Forward declaration for the interface class.
template <class T> class SteadyStateBoundOperator;
/*!
- * @brief Interface class for model checkers that support SteadyStateOperator.
+ * Interface class for model checkers that support SteadyStateOperator.
*
- * All model checkers that support the formula class SteadyStateOperator must inherit
- * this pure virtual class.
+ * All model checkers that support the formula class SteadyStateOperator must inherit
+ * this pure virtual class.
*/
template <class T>
class ISteadyStateBoundOperatorModelChecker {
public:
+
/*!
- * @brief Evaluates SteadyStateOperator formula within a model checker.
+ * Empty virtual destructor.
+ */
+ virtual ~ISteadyStateBoundOperatorModelChecker() {
+ // Intentionally left empty
+ }
+
+ /*!
+ * Evaluates a SteadyStateOperator formula within a model checker.
*
- * @param obj Formula object with subformulas.
- * @return Result of the formula for every node.
+ * @param obj Formula object with subformulas.
+ * @return The modelchecking result of the formula for every state.
*/
virtual storm::storage::BitVector checkSteadyStateBoundOperator(const SteadyStateBoundOperator<T>& obj) const = 0;
};
/*!
- * @brief
- * Class for an Abstract (path) formula tree with a SteadyStateOperator node as root.
+ * Class for a Csl formula tree with a SteadyStateOperator node as root.
*
- * Has two Abstract state formulas as sub formulas/trees.
+ * Has two state formulas as sub formulas/trees.
*
* @par Semantics
- * The formula holds iff \e child holds SteadyStateOperator step, \e child holds
+ * The formula holds iff the long-run probability of being in a state satisfying \e child meets the \e bound specified in this operator.
*
- * The subtree is seen as part of the object and deleted with the object
- * (this behavior can be prevented by setting them to NULL before deletion)
+ * The object has shared ownership of its subtree. If this object is deleted and no other object has a shared
+ * ownership of the subtree it will be deleted as well.
*
* @see AbstractPathFormula
* @see AbstractCslFormula
@@ -56,29 +64,27 @@ class SteadyStateBoundOperator : public AbstractStateFormula<T> {
public:
/*!
- * Empty constructor
+ * Creates a SteadyStateBoundOperator node without a subnode.
+ * The resulting object will not represent a complete formula!
*/
- SteadyStateBoundOperator() : comparisonOperator(LESS), bound(storm::utility::constantZero<T>()), stateFormula(nullptr) {
+ SteadyStateBoundOperator() : comparisonOperator(LESS), bound(storm::utility::constantZero<T>()), child(nullptr) {
// Intentionally left empty
}
/*!
- * Constructor
+ * Creates a SteadyStateBoundOperator node using the given parameters.
*
* @param comparisonOperator The relation for the bound.
- * @param bound The bound for the probability
- * @param stateFormula The child node
+ * @param bound The bound for the probability.
+ * @param child The child formula subtree.
*/
- SteadyStateBoundOperator(storm::property::ComparisonType comparisonOperator, T bound, std::shared_ptr<AbstractStateFormula<T>> const & stateFormula)
- : comparisonOperator(comparisonOperator), bound(bound), stateFormula(stateFormula) {
+ SteadyStateBoundOperator(storm::property::ComparisonType comparisonOperator, T bound, std::shared_ptr<AbstractStateFormula<T>> const & child)
+ : comparisonOperator(comparisonOperator), bound(bound), child(child) {
// Intentionally left empty
}
/*!
- * Destructor
- *
- * The subtree is deleted with the object
- * (this behavior can be prevented by setting them to NULL before deletion)
+ * Empty virtual destructor.
*/
virtual ~SteadyStateBoundOperator() {
// Intentionally left empty.
@@ -87,13 +93,13 @@ public:
/*!
* Clones the called object.
*
- * Performs a "deep copy", i.e. the subtrees of the new object are clones of the original ones
+ * Performs a "deep copy", i.e. the subnodes of the new object are clones of the original ones.
*
- * @returns a new BoundedUntil-object that is identical the called object.
+ * @returns A new SteadyStateBoundOperator object that is a deep copy of the called object.
*/
virtual std::shared_ptr<AbstractStateFormula<T>> clone() const override {
std::shared_ptr<SteadyStateBoundOperator<T>> result(new SteadyStateBoundOperator<T>());
- result->setStateFormula(stateFormula->clone());
+ result->setChild(child->clone());
return result;
}
@@ -111,7 +117,9 @@ public:
}
/*!
- * @returns a string representation of the formula
+ * Returns a textual representation of the formula tree with this node as root.
+ *
+ * @returns A string representing the formula tree.
*/
virtual std::string toString() const override {
std::string result = "S ";
@@ -123,62 +131,80 @@ public:
}
result += std::to_string(bound);
result += " (";
- result += stateFormula->toString();
+ result += child->toString();
result += ")";
return result;
}
/*!
- * @returns the child node (representation of a formula)
+ * Gets the child node.
+ *
+ * @returns The child node.
*/
- std::shared_ptr<AbstractStateFormula<T>> const & getStateFormula () const {
- return stateFormula;
+ std::shared_ptr<AbstractStateFormula<T>> const & getChild () const {
+ return child;
}
/*!
- * Sets the child node
+ * Sets the subtree.
*
- * @param stateFormula the state formula that becomes the new child node
+ * @param child The new child.
*/
- void setStateFormula(std::shared_ptr<AbstractStateFormula<T>> const & stateFormula) {
- this->stateFormula = stateFormula;
+ void setChild(std::shared_ptr<AbstractStateFormula<T>> const & child) {
+ this->child = child;
}
/*!
+ * Checks if the child is set, i.e. it does not point to null.
*
- * @return True if the state formula is set, i.e. it does not point to nullptr; false otherwise
+ * @return True iff the child is set.
*/
- bool stateFormulaIsSet() const {
- return stateFormula.get() != nullptr;
+ bool isChildSet() const {
+ return child.get() != nullptr;
}
/*!
- * @returns the comparison relation
+ * Gets the comparison operator.
+ *
+ * @returns An enum value representing the comparison relation.
*/
ComparisonType const getComparisonOperator() const {
return comparisonOperator;
}
+ /*!
+ * Sets the comparison operator.
+ *
+ * @param comparisonOperator An enum value representing the new comparison relation.
+ */
void setComparisonOperator(ComparisonType comparisonOperator) {
this->comparisonOperator = comparisonOperator;
}
/*!
- * @returns the bound for the measure
+ * Gets the bound which the steady state probability has to obey.
+ *
+ * @returns The probability bound.
*/
T const & getBound() const {
return bound;
}
/*!
- * Sets the interval in which the probability that the path formula holds may lie in.
+ * Sets the bound which the steady state probability has to obey.
*
- * @param bound The bound for the measure
+ * @param bound The new probability bound.
*/
void setBound(T const & bound) {
this->bound = bound;
}
+ /*!
+ * Checks if the bound is met by the given value.
+ *
+ * @param value The value to test against the bound.
+ * @returns True iff value <comparisonOperator> bound holds.
+ */
bool meetsBound(T value) const {
switch (comparisonOperator) {
case LESS: return value < bound; break;
@@ -190,9 +216,15 @@ public:
}
private:
+
+ // The operator used to indicate the kind of bound that is to be met.
ComparisonType comparisonOperator;
+
+ // The probability bound.
T bound;
- std::shared_ptr<AbstractStateFormula<T>> stateFormula;
+
+ // The state formula for whose state the long-run probability has to meet the bound.
+ std::shared_ptr<AbstractStateFormula<T>> child;
};
} //namespace csl
diff --git a/src/formula/csl/TimeBoundedEventually.h b/src/formula/csl/TimeBoundedEventually.h
index e4c6aa483..785a1677a 100644
--- a/src/formula/csl/TimeBoundedEventually.h
+++ b/src/formula/csl/TimeBoundedEventually.h
@@ -15,45 +15,77 @@ namespace storm {
namespace property {
namespace csl {
+// Forward declaration for the interface class.
template<class T> class TimeBoundedEventually;
/*!
- * @brief Interface class for model checkers that support TimeBoundedEventually.
+ * Interface class for model checkers that support TimeBoundedEventually.
*
- * All model checkers that support the formula class BoundedEventually must inherit
- * this pure virtual class.
+ * All model checkers that support the formula class TimeBoundedEventually must inherit
+ * this pure virtual class.
*/
template <class T>
class ITimeBoundedEventuallyModelChecker {
public:
+
+ /*!
+ * Empty virtual destructor.
+ */
+ virtual ~ITimeBoundedEventuallyModelChecker() {
+ // Intentionally left empty
+ }
+
/*!
- * @brief Evaluates TimeBoundedUntil formula within a model checker.
- *
- * @param obj Formula object with subformulas.
- * @return Result of the formula for every node.
- */
+ * Evaluates a TimeBoundedEventually formula within a model checker.
+ *
+ * @param obj Formula object with subformulas.
+ * @param qualitative A flag indicating whether the formula only needs to be evaluated qualitatively, i.e. if the
+ * results are only compared against the bounds 0 and 1.
+ * @return The modelchecking result of the formula for every state.
+ */
virtual std::vector<T> checkTimeBoundedEventually(const TimeBoundedEventually<T>& obj, bool qualitative) const = 0;
};
-
+/*!
+ * Class for a Csl (path) formula tree with a TimeBoundedEventually node as root.
+ *
+ * Has one state formula as subformula/tree.
+ *
+ * @par Semantics
+ * The formula holds iff formula \e child holds within the given time interval [lowerBound, upperBound].
+ *
+ * The object has shared ownership of its subtree. If this object is deleted and no other object has a shared
+ * ownership of the subtree it will be deleted as well.
+ *
+ * @see AbstractPathFormula
+ * @see AbstractCslFormula
+ */
template<class T>
class TimeBoundedEventually: public AbstractPathFormula<T> {
public:
- /**
- * Simple constructor: Only sets the bounds
- *
- * @param lowerBound
- * @param upperBound
+ /*!
+ * Creates a TimeBoundedEventually node without a subnode.
+ * The resulting object will not represent a complete formula!
*/
- TimeBoundedEventually(T lowerBound, T upperBound) : child(nullptr) {
- setInterval(lowerBound, upperBound);
+ TimeBoundedEventually() : lowerBound(0), upperBound(0), child(nullptr) {
+ // Intentionally left empty.
}
+ /*!
+ * Creates a TimeBoundedEventually node using the given parameters.
+ *
+ * @param lowerBound The lower bound of the admissable time interval.
+ * @param upperBound The upper bound of the admissable time interval.
+ * @param child The child formula subtree.
+ */
TimeBoundedEventually(T lowerBound, T upperBound, std::shared_ptr<AbstractStateFormula<T>> const & child) : child(child) {
setInterval(lowerBound, upperBound);
}
+ /*!
+ * Empty virtual destructor.
+ */
virtual ~TimeBoundedEventually() {
// Intentionally left empty.
}
@@ -61,13 +93,13 @@ public:
/*!
* Clones the called object.
*
- * Performs a "deep copy", i.e. the subtrees of the new object are clones of the original ones
+ * Performs a "deep copy", i.e. the subnodes of the new object are clones of the original ones.
*
- * @returns a new BoundedUntil-object that is identical the called object.
+ * @returns A new TimeBoundedEventually object that is a deep copy of the called object.
*/
virtual std::shared_ptr<AbstractPathFormula<T>> clone() const override {
std::shared_ptr<TimeBoundedEventually<T>> result(new TimeBoundedEventually<T>(lowerBound, upperBound));
- if (this->childIsSet()) {
+ if (this->isChildSet()) {
result->setChild(child->clone());
}
return result;
@@ -87,7 +119,9 @@ public:
}
/*!
- * @returns a string representation of the formula
+ * Returns a textual representation of the formula tree with this node as root.
+ *
+ * @returns A string representing the formula tree.
*/
virtual std::string toString() const override {
std::string result = "F";
@@ -106,50 +140,55 @@ public:
}
/*!
- * @returns the child node
+ * Gets the child node.
+ *
+ * @returns The child node.
*/
std::shared_ptr<AbstractStateFormula<T>> const & getChild() const {
return child;
}
/*!
- * Sets the subtree
- * @param child the new child node
+ * Sets the subtree.
+ *
+ * @param child The new child.
*/
void setChild(std::shared_ptr<AbstractStateFormula<T>> const & child) {
this->child = child;
}
/*!
+ * Checks if the child is set, i.e. it does not point to null.
*
- * @return True if the child is set, i.e. it does not point to nullptr; false otherwise
+ * @return True iff the child is set.
*/
- bool childIsSet() const {
+ bool isChildSet() const {
return child.get() != nullptr;
}
- /**
- * Getter for lowerBound attribute
+ /*!
+ * Get the lower time bound.
*
- * @return lower bound of the operator.
+ * @return The lower time bound.
*/
T const & getLowerBound() const {
return lowerBound;
}
- /**
- * Getter for upperBound attribute
- * @return upper bound of the operator.
+ /*!
+ * Get the upper time bound.
+ *
+ * @return The upper time bound.
*/
T const & getUpperBound() const {
return upperBound;
}
- /**
- * Set the time interval for the time bounded operator
+ /*!
+ * Set the time interval for the time bounded operator.
*
- * @param lowerBound
- * @param upperBound
+ * @param lowerBound The new lower time bound.
+ * @param upperBound The new upper time bound.
* @throw InvalidArgumentException if the lower bound is larger than the upper bound.
*/
void setInterval(T lowerBound, T upperBound) {
@@ -161,8 +200,15 @@ public:
}
private:
+
+ // The child node.
std::shared_ptr<AbstractStateFormula<T>> child;
- T lowerBound, upperBound;
+
+ // The lower time bound.
+ T lowerBound;
+
+ // The upper time bound.
+ T upperBound;
};
} /* namespace csl */
diff --git a/src/formula/csl/TimeBoundedUntil.h b/src/formula/csl/TimeBoundedUntil.h
index 170ddf54a..5e27edd37 100644
--- a/src/formula/csl/TimeBoundedUntil.h
+++ b/src/formula/csl/TimeBoundedUntil.h
@@ -15,55 +15,78 @@ namespace storm {
namespace property {
namespace csl {
+// Forward declaration for the interface class.
template <class T> class TimeBoundedUntil;
/*!
- * @brief Interface class for model checkers that support TimeBoundedUntil.
+ * Interface class for model checkers that support TimeBoundedUntil.
*
- * All model checkers that support the formula class BoundedEventually must inherit
- * this pure virtual class.
+ * All model checkers that support the formula class TimeBoundedUntil must inherit
+ * this pure virtual class.
*/
template <class T>
class ITimeBoundedUntilModelChecker {
public:
+
+ /*!
+ * Empty virtual destructor.
+ */
+ virtual ~ITimeBoundedUntilModelChecker() {
+ // Intentionally left empty
+ }
+
/*!
- * @brief Evaluates TimeBoundedUntil formula within a model checker.
- *
- * @param obj Formula object with subformulas.
- * @return Result of the formula for every node.
- */
+ * Evaluates a TimeBoundedUntil formula within a model checker.
+ *
+ * @param obj Formula object with subformulas.
+ * @param qualitative A flag indicating whether the formula only needs to be evaluated qualitatively, i.e. if the
+ * results are only compared against the bounds 0 and 1.
+ * @return The modelchecking result of the formula for every state.
+ */
virtual std::vector<T> checkTimeBoundedUntil(const TimeBoundedUntil<T>& obj, bool qualitative) const = 0;
};
+
+/*!
+ * Class for a Csl (path) formula tree with a TimeBoundedUntil node as root.
+ *
+ * Has two state formulas as subformulas/trees.
+ *
+ * @par Semantics
+ * The formula holds iff formula \e right holds within the given time interval [lowerBound, upperBound] and \e left holds
+ * in each point in time before that.
+ *
+ * The object has shared ownership of its subtree. If this object is deleted and no other object has a shared
+ * ownership of the subtree it will be deleted as well.
+ *
+ * @see AbstractPathFormula
+ * @see AbstractCslFormula
+ */
template <class T>
class TimeBoundedUntil: public AbstractPathFormula<T> {
public:
- /**
- * Constructor providing bounds only;
- * Sub formulas are set to null.
- *
- * @param lowerBound
- * @param upperBound
+ /*!
+ * Creates a TimeBoundedUntil node without a subnode.
+ * The resulting object will not represent a complete formula!
*/
- TimeBoundedUntil(T lowerBound, T upperBound) : left(nullptr), right(nullptr) {
+ TimeBoundedUntil() : lowerBound(0), upperBound(0), left(nullptr), right(nullptr) {
setInterval(lowerBound, upperBound);
}
-
- /**
- * Full constructor
- * @param lowerBound
- * @param upperBound
- * @param left
- * @param right
+ /*!
+ * Creates a TimeBoundedUntil node using the given parameters.
+ *
+ * @param lowerBound The lower bound of the admissable time interval.
+ * @param upperBound The upper bound of the admissable time interval.
+ * @param child The child formula subtree.
*/
TimeBoundedUntil(T lowerBound, T upperBound, std::shared_ptr<AbstractStateFormula<T>> const & left, std::shared_ptr<AbstractStateFormula<T>> const & right) : left(left), right(right) {
setInterval(lowerBound, upperBound);
}
/*!
- * Destructor
+ * Empty virtual destructor.
*/
virtual ~TimeBoundedUntil() {
// Intentionally left empty.
@@ -72,16 +95,16 @@ public:
/*!
* Clones the called object.
*
- * Performs a "deep copy", i.e. the subtrees of the new object are clones of the original ones
+ * Performs a "deep copy", i.e. the subnodes of the new object are clones of the original ones.
*
- * @returns a new BoundedUntil-object that is identical the called object.
+ * @returns A new TimeBoundedUntil object that is a deep copy of the called object.
*/
virtual std::shared_ptr<AbstractPathFormula<T>> clone() const override {
std::shared_ptr<TimeBoundedUntil<T>> result(new TimeBoundedUntil<T>(lowerBound, upperBound));
- if (this->leftIsSet()) {
+ if (this->isLeftSet()) {
result->setLeft(left->clone());
}
- if (this->rightIsSet()) {
+ if (this->isRightSet()) {
result->setRight(right->clone());
}
return result;
@@ -102,7 +125,9 @@ public:
}
/*!
- * @returns a string representation of the formula
+ * Returns a textual representation of the formula tree with this node as root.
+ *
+ * @returns A string representing the formula tree.
*/
virtual std::string toString() const override {
std::string result = left->toString();
@@ -122,65 +147,72 @@ public:
}
/*!
- * Sets the left child node.
+ * Gets the left child node.
*
- * @param newLeft the new left child.
+ * @returns The left child node.
*/
- void setLeft(std::shared_ptr<AbstractStateFormula<T>> const & newLeft) {
- left = newLeft;
+ std::shared_ptr<AbstractStateFormula<T>> const & getLeft() const {
+ return left;
}
/*!
- * Sets the right child node.
+ * Gets the right child node.
*
- * @param newRight the new right child.
+ * @returns The right child node.
*/
- void setRight(std::shared_ptr<AbstractStateFormula<T>> const & newRight) {
- right = newRight;
+ std::shared_ptr<AbstractStateFormula<T>> const & getRight() const {
+ return right;
}
/*!
- * @returns a pointer to the left child node
+ * Sets the left child node.
+ *
+ * @param newLeft The new left child.
*/
- std::shared_ptr<AbstractStateFormula<T>> const & getLeft() const {
- return left;
+ void setLeft(std::shared_ptr<AbstractStateFormula<T>> const & newLeft) {
+ left = newLeft;
}
/*!
- * @returns a pointer to the right child node
+ * Sets the right child node.
+ *
+ * @param newRight The new right child.
*/
- std::shared_ptr<AbstractStateFormula<T>> const & getRight() const {
- return right;
+ void setRight(std::shared_ptr<AbstractStateFormula<T>> const & newRight) {
+ right = newRight;
}
/*!
+ * Checks if the left child is set, i.e. it does not point to null.
*
- * @return True if the left child is set, i.e. it does not point to nullptr; false otherwise
+ * @return True iff the left child is set.
*/
- bool leftIsSet() const {
+ bool isLeftSet() const {
return left.get() != nullptr;
}
/*!
+ * Checks if the right child is set, i.e. it does not point to null.
*
- * @return True if the right child is set, i.e. it does not point to nullptr; false otherwise
+ * @return True iff the right child is set.
*/
- bool rightIsSet() const {
+ bool isRightSet() const {
return right.get() != nullptr;
}
- /**
- * Getter for lowerBound attribute
+ /*!
+ * Get the lower time bound.
*
- * @return lower bound of the operator.
+ * @return The lower time bound.
*/
T const & getLowerBound() const {
return lowerBound;
}
- /**
- * Getter for upperBound attribute
- * @return upper bound of the operator.
+ /*!
+ * Get the upper time bound.
+ *
+ * @return The upper time bound.
*/
T const & getUpperBound() const {
return upperBound;
@@ -189,8 +221,8 @@ public:
/**
* Set the time interval for the time bounded operator
*
- * @param lowerBound
- * @param upperBound
+ * @param lowerBound The new lower time bound.
+ * @param upperBound The new upper time bound.
* @throw InvalidArgumentException if the lower bound is larger than the upper bound.
*/
void setInterval(T lowerBound, T upperBound) {
@@ -202,9 +234,18 @@ public:
}
private:
+
+ // The left child node.
std::shared_ptr<AbstractStateFormula<T>> left;
+
+ // The right child node.
std::shared_ptr<AbstractStateFormula<T>> right;
- T lowerBound, upperBound;
+
+ // The lower time bound.
+ T lowerBound;
+
+ // The upper time bound.
+ T upperBound;
};
} /* namespace csl */
diff --git a/src/formula/csl/Until.h b/src/formula/csl/Until.h
index 8d2446489..8db1fa7d6 100644
--- a/src/formula/csl/Until.h
+++ b/src/formula/csl/Until.h
@@ -15,38 +15,49 @@ namespace storm {
namespace property {
namespace csl {
+// Forward declaration for the interface class.
template <class T> class Until;
/*!
- * @brief Interface class for model checkers that support Until.
+ * Interface class for model checkers that support Until.
*
- * All model checkers that support the formula class Until must inherit
- * this pure virtual class.
+ * All model checkers that support the formula class Until must inherit
+ * this pure virtual class.
*/
template <class T>
class IUntilModelChecker {
public:
+
+ /*!
+ * Empty virtual destructor.
+ */
+ virtual ~IUntilModelChecker() {
+ // Intentionally left empty
+ }
+
/*!
- * @brief Evaluates Until formula within a model checker.
- *
- * @param obj Formula object with subformulas.
- * @return Result of the formula for every node.
- */
+ * Evaluates an Until formula within a model checker.
+ *
+ * @param obj Formula object with subformulas.
+ * @param qualitative A flag indicating whether the formula only needs to be evaluated qualitatively, i.e. if the
+ * results are only compared against the bounds 0 and 1.
+ * @return The modelchecking result of the formula for every state.
+ */
virtual std::vector<T> checkUntil(const Until<T>& obj, bool qualitative) const = 0;
};
/*!
* @brief
- * Class for an abstract (path) formula tree with an Until node as root.
+ * Class for a Csl (path) formula tree with an Until node as root.
*
- * Has two Abstract state formulas as sub formulas/trees.
+ * Has two state formulas as sub formulas/trees.
*
* @par Semantics
* The formula holds iff eventually, formula \e right (the right subtree) holds, and before,
* \e left holds always.
*
- * 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)
+ * The object has shared ownership of its subtrees. If this object is deleted and no other object has a shared
+ * ownership of the subtrees they will be deleted as well.
*
* @see AbstractPathFormula
* @see AbstractCslFormula
@@ -55,28 +66,27 @@ template <class T>
class Until : public AbstractPathFormula<T> {
public:
+
/*!
- * Empty constructor
+ * Creates an Until node without subnodes.
+ * The resulting object will not represent a complete formula!
*/
Until() : left(nullptr), right(nullptr){
// Intentionally left empty.
}
/*!
- * Constructor
+ * Creates an Until node using the given parameters.
*
- * @param left The left formula subtree
- * @param right The left formula subtree
+ * @param left The left formula subtree.
+ * @param right The right formula subtree.
*/
Until(std::shared_ptr<AbstractStateFormula<T>> const & left, std::shared_ptr<AbstractStateFormula<T>> const & right) : left(left), right(right){
// Intentionally left empty.
}
/*!
- * Destructor.
- *
- * Also deletes the subtrees.
- * (this behaviour can be prevented by setting the subtrees to NULL before deletion)
+ * Empty virtual destructor.
*/
virtual ~Until() {
// Intentionally left empty.
@@ -85,16 +95,16 @@ public:
/*!
* Clones the called object.
*
- * Performs a "deep copy", i.e. the subtrees of the new object are clones of the original ones
+ * Performs a "deep copy", i.e. the subnodes of the new object are clones of the original ones.
*
- * @returns a new BoundedUntil-object that is identical the called object.
+ * @returns A new Until object that is a deep copy of the called object.
*/
virtual std::shared_ptr<AbstractPathFormula<T>> clone() const override {
std::shared_ptr<Until<T>> result(new Until());
- if (this->leftIsSet()) {
+ if (this->isLeftSet()) {
result->setLeft(left->clone());
}
- if (this->rightIsSet()) {
+ if (this->isRightSet()) {
result->setRight(left->clone());
}
return result;
@@ -114,7 +124,9 @@ public:
}
/*!
- * @returns a string representation of the formula
+ * Returns a textual representation of the formula tree with this node as root.
+ *
+ * @returns A string representing the formula tree.
*/
virtual std::string toString() const override {
std::string result = left->toString();
@@ -124,55 +136,65 @@ public:
}
/*!
- * Sets the left child node.
+ * Gets the left child node.
*
- * @param newLeft the new left child.
+ * @returns The left child node.
*/
- void setLeft(std::shared_ptr<AbstractStateFormula<T>> const & newLeft) {
- left = newLeft;
+ std::shared_ptr<AbstractStateFormula<T>> const & getLeft() const {
+ return left;
}
/*!
- * Sets the right child node.
+ * Gets the right child node.
*
- * @param newRight the new right child.
+ * @returns The right child node.
*/
- void setRight(std::shared_ptr<AbstractStateFormula<T>> const & newRight) {
- right = newRight;
+ std::shared_ptr<AbstractStateFormula<T>> const & getRight() const {
+ return right;
}
/*!
- * @returns a pointer to the left child node
+ * Sets the left child node.
+ *
+ * @param newLeft The new left child.
*/
- std::shared_ptr<AbstractStateFormula<T>> const & getLeft() const {
- return left;
+ void setLeft(std::shared_ptr<AbstractStateFormula<T>> const & newLeft) {
+ left = newLeft;
}
/*!
- * @returns a pointer to the right child node
+ * Sets the right child node.
+ *
+ * @param newRight The new right child.
*/
- std::shared_ptr<AbstractStateFormula<T>> const & getRight() const {
- return right;
+ void setRight(std::shared_ptr<AbstractStateFormula<T>> const & newRight) {
+ right = newRight;
}
/*!
+ * Checks if the left child is set, i.e. it does not point to null.
*
- * @return True if the left child is set, i.e. it does not point to nullptr; false otherwise
+ * @return True iff the left child is set.
*/
- bool leftIsSet() const {
+ bool isLeftSet() const {
return left.get() != nullptr;
}
/*!
+ * Checks if the right child is set, i.e. it does not point to null.
*
- * @return True if the right child is set, i.e. it does not point to nullptr; false otherwise
+ * @return True iff the right child is set.
*/
- bool rightIsSet() const {
+ bool isRightSet() const {
return right.get() != nullptr;
}
private:
+
+ // The left child node.
std::shared_ptr<AbstractStateFormula<T>> left;
+
+ // The right child node.
std::shared_ptr<AbstractStateFormula<T>> right;
};
diff --git a/src/formula/ltl/AbstractLtlFormula.h b/src/formula/ltl/AbstractLtlFormula.h
index 1c4ef1403..3605779be 100644
--- a/src/formula/ltl/AbstractLtlFormula.h
+++ b/src/formula/ltl/AbstractLtlFormula.h
@@ -17,18 +17,33 @@ namespace property {
namespace ltl {
/*!
- * Interface class for all LTL root formulas.
+ * This is the abstract base class for all Ltl formulas.
+ *
+ * @note While formula classes do have copy constructors using a copy constructor
+ * will yield a formula objects whose formula subtree consists of the same objects
+ * as the original formula. The ownership of the formula tree will be shared between
+ * the original and the copy.
*/
template <class T>
class AbstractLtlFormula : public virtual storm::property::AbstractFormula<T> {
public:
- /**
- * Empty destructor
+
+ /*!
+ * The virtual destructor.
*/
virtual ~AbstractLtlFormula() {
// Intentionally left empty
}
+ /*!
+ * Clones the called object.
+ *
+ * Performs a "deep copy", i.e. the subtrees of the new object are clones of the original ones
+ *
+ * @returns A deep copy of the called object.
+ */
+ virtual std::shared_ptr<AbstractLtlFormula<T>> clone() const = 0;
+
/*!
* Calls the model checker to check this formula.
* Needed to infer the correct type of formula class.
@@ -41,15 +56,6 @@ public:
* @returns A vector indicating the probability that the formula holds for each state.
*/
virtual std::vector<T> check(const storm::modelchecker::ltl::AbstractModelChecker<T>& modelChecker) const = 0;
-
- /*!
- * 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 AND-object that is identical the called object.
- */
- virtual std::shared_ptr<AbstractLtlFormula<T>> clone() const = 0;
};
} /* namespace ltl */
diff --git a/src/formula/ltl/And.h b/src/formula/ltl/And.h
index 06fc83cae..67656ef9b 100644
--- a/src/formula/ltl/And.h
+++ b/src/formula/ltl/And.h
@@ -16,17 +16,26 @@ namespace storm {
namespace property {
namespace ltl {
+// Forward declaration for the interface class.
template <class T> class And;
/*!
- * @brief Interface class for model checkers that support And.
+ * Interface class for model checkers that support And.
*
- * All model checkers that support the formula class And must inherit
- * this pure virtual class.
+ * All model checkers that support the formula class And must inherit
+ * this pure virtual class.
*/
template <class T>
class IAndModelChecker {
public:
+
+ /*!
+ * Empty virtual destructor.
+ */
+ virtual ~IAndModelChecker() {
+ // Intentionally left empty
+ }
+
/*!
* @brief Evaluates And formula within a model checker.
*
@@ -37,16 +46,15 @@ class IAndModelChecker {
};
/*!
- * @brief
- * Class for an abstract formula tree with AND node as root.
+ * Class for an Ltl formula tree with And node as root.
*
- * Has two Abstract LTL formulas as sub formulas/trees.
+ * Has two Ltl formulas as sub formulas/trees.
*
- * As AND is commutative, the order is \e theoretically not important, but will influence the order in which
+ * As And is commutative, the order is \e theoretically not important, but will influence the order in which
* the model checker works.
*
- * 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)
+ * The object has shared ownership of its subtrees. If this object is deleted and no other object has a shared
+ * ownership of the subtrees they will be deleted as well.
*
* @see AbstractLtlFormula
*/
@@ -56,29 +64,25 @@ class And : public AbstractLtlFormula<T> {
public:
/*!
- * Empty constructor.
- * Will create an AND-node without subnotes. Will not represent a complete formula!
+ * Creates an And node without subnodes.
+ * The resulting object will not represent a complete formula!
*/
And() : left(nullptr), right(nullptr){
// Intentionally left empty.
}
/*!
- * Constructor.
- * Creates an AND note with the parameters as subtrees.
+ * Creates an And node with the parameters as subtrees.
*
- * @param left The left sub formula
- * @param right The right sub formula
+ * @param left The left sub formula.
+ * @param right The right sub formula.
*/
And(std::shared_ptr<AbstractLtlFormula<T>> left, std::shared_ptr<AbstractLtlFormula<T>> right) : left(left), right(right) {
// Intentionally left empty.
}
/*!
- * Destructor.
- *
- * The subtrees are deleted with the object
- * (this behavior can be prevented by setting them to NULL before deletion)
+ * Empty virtual destructor.
*/
virtual ~And() {
// Intentionally left empty.
@@ -87,16 +91,16 @@ public:
/*!
* Clones the called object.
*
- * Performs a "deep copy", i.e. the subtrees of the new object are clones of the original ones
+ * Performs a "deep copy", i.e. the subtrees of the new object are clones of the original ones.
*
- * @returns a new AND-object that is identical the called object.
+ * @returns A new And object that is a deep copy of the called object.
*/
virtual std::shared_ptr<AbstractLtlFormula<T>> clone() const override {
std::shared_ptr<And<T>> result(new And());
- if (this->leftIsSet()) {
+ if (this->isLeftSet()) {
result->setLeft(left->clone());
}
- if (this->rightIsSet()) {
+ if (this->isRightSet()) {
result->setRight(right->clone());
}
return result;
@@ -116,7 +120,9 @@ public:
}
/*!
- * @returns a string representation of the formula
+ * Returns a textual representation of the formula tree with this node as root.
+ *
+ * @returns A string representing the formula tree.
*/
virtual std::string toString() const override {
std::string result = "(";
@@ -138,55 +144,65 @@ public:
}
/*!
- * Sets the left child node.
+ * Gets the left child node.
*
- * @param newLeft the new left child.
+ * @returns The left child node.
*/
- void setLeft(std::shared_ptr<AbstractLtlFormula<T>> const & newLeft) {
- left = newLeft;
+ std::shared_ptr<AbstractLtlFormula<T>> const & getLeft() const {
+ return left;
}
/*!
- * Sets the right child node.
+ * Gets the right child node.
*
- * @param newRight the new right child.
+ * @returns The right child node.
*/
- void setRight(std::shared_ptr<AbstractLtlFormula<T>> const & newRight) {
- right = newRight;
+ std::shared_ptr<AbstractLtlFormula<T>> const & getRight() const {
+ return right;
}
/*!
- * @returns a pointer to the left child node
+ * Sets the left child node.
+ *
+ * @param newLeft The new left child.
*/
- std::shared_ptr<AbstractLtlFormula<T>> const & getLeft() const {
- return left;
+ void setLeft(std::shared_ptr<AbstractLtlFormula<T>> const & newLeft) {
+ left = newLeft;
}
/*!
- * @returns a pointer to the right child node
+ * Sets the right child node.
+ *
+ * @param newRight The new right child.
*/
- std::shared_ptr<AbstractLtlFormula<T>> const & getRight() const {
- return right;
+ void setRight(std::shared_ptr<AbstractLtlFormula<T>> const & newRight) {
+ right = newRight;
}
/*!
+ * Checks if the left child is set, i.e. it does not point to null.
*
- * @return True if the left child is set, i.e. it does not point to nullptr; false otherwise
+ * @return True iff the left child is set.
*/
- bool leftIsSet() const {
+ bool isLeftSet() const {
return left.get() != nullptr;
}
/*!
+ * Checks if the right child is set, i.e. it does not point to null.
*
- * @return True if the right child is set, i.e. it does not point to nullptr; false otherwise
+ * @return True iff the right child is set.
*/
- bool rightIsSet() const {
+ bool isRightSet() const {
return right.get() != nullptr;
}
private:
+
+ // The left child node.
std::shared_ptr<AbstractLtlFormula<T>> left;
+
+ // The right child node.
std::shared_ptr<AbstractLtlFormula<T>> right;
};
diff --git a/src/formula/ltl/Ap.h b/src/formula/ltl/Ap.h
index 451dadb99..544d84ed5 100644
--- a/src/formula/ltl/Ap.h
+++ b/src/formula/ltl/Ap.h
@@ -14,29 +14,37 @@ namespace storm {
namespace property {
namespace ltl {
+// Forward declaration for the interface class.
template <class T> class Ap;
/*!
- * @brief Interface class for model checkers that support And.
+ * Interface class for model checkers that support Ap.
*
- * All model checkers that support the formula class And must inherit
- * this pure virtual class.
+ * All model checkers that support the formula class Ap must inherit
+ * this pure virtual class.
*/
template <class T>
class IApModelChecker {
public:
+
+ /*!
+ * Empty virtual destructor.
+ */
+ virtual ~IApModelChecker() {
+ // Intentionally left empty
+ }
+
/*!
- * @brief Evaluates And formula within a model checker.
+ * Evaluates an Ap formula within a model checker.
*
- * @param obj Formula object with subformulas.
- * @return Result of the formula for every node.
+ * @param obj Formula object with subformulas.
+ * @return The modelchecking result of the formula for every state.
*/
virtual std::vector<T> checkAp(const Ap<T>& obj) const = 0;
};
/*!
- * @brief
- * Class for an abstract formula tree with atomic proposition as root.
+ * Class for an Ltl formula tree with an atomic proposition as root.
*
* This class represents the leaves in the formula tree.
*
@@ -44,33 +52,37 @@ class IApModelChecker {
*/
template <class T>
class Ap: public storm::property::ltl::AbstractLtlFormula<T> {
+
public:
- /*!
- * Empty constructor
- */
- Ap() {
- // Intentionally left empty
- }
/*!
- * Constructor
- *
- * Creates a new atomic proposition leaf, with the label Ap
+ * Creates a new atomic proposition leaf, with the given label.
*
- * @param ap The string representing the atomic proposition
+ * @param ap A string representing the atomic proposition.
*/
Ap(std::string ap) : ap(ap) {
// Intentionally left empty.
}
/*!
- * Destructor
- * At this time, empty...
+ * Empty virtual destructor.
*/
virtual ~Ap() {
// Intentionally left empty
}
+ /*!
+ * 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 Ap object that is a deep copy of the called object.
+ */
+ virtual std::shared_ptr<AbstractLtlFormula<T>> clone() const override {
+ auto result = std::make_shared<Ap<T>>(this->getAp());
+ return result;
+ }
+
/*!
* Calls the model checker to check this formula.
* Needed to infer the correct type of formula class.
@@ -78,8 +90,6 @@ public:
* @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 the probability that the formula holds for each state.
*/
virtual std::vector<T> check(const storm::modelchecker::ltl::AbstractModelChecker<T>& modelChecker) const override {
@@ -87,20 +97,9 @@ public:
}
/*!
- * 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 AND-object that is identical the called object.
- */
- virtual std::shared_ptr<AbstractLtlFormula<T>> clone() const override {
- std::shared_ptr<AbstractLtlFormula<T>> result(new Ap(this->getAp()));
- return result;
- }
-
- /*!
- * @returns a string representation of the leaf.
+ * A string representing the atomic proposition.
*
+ * @returns A string representing the leaf.
*/
virtual std::string toString() const override {
return getAp();
@@ -117,13 +116,17 @@ public:
}
/*!
- * @returns the name of the atomic proposition
+ * Gets the name of the atomic proposition.
+ *
+ * @returns The name of the atomic proposition.
*/
std::string const & getAp() const {
return ap;
}
private:
+
+ // The atomic proposition referenced by this leaf.
std::string ap;
};
diff --git a/src/formula/ltl/BoundedEventually.h b/src/formula/ltl/BoundedEventually.h
index 630e0bbae..57027cea3 100644
--- a/src/formula/ltl/BoundedEventually.h
+++ b/src/formula/ltl/BoundedEventually.h
@@ -17,37 +17,45 @@ namespace storm {
namespace property {
namespace ltl {
+// Forward declaration for the interface class.
template <class T> class BoundedEventually;
/*!
- * @brief Interface class for model checkers that support BoundedEventually.
+ * Interface class for model checkers that support BoundedEventually.
*
- * All model checkers that support the formula class BoundedEventually must inherit
- * this pure virtual class.
+ * All model checkers that support the formula class BoundedEventually must inherit
+ * this pure virtual class.
*/
template <class T>
class IBoundedEventuallyModelChecker {
public:
+
+ /*!
+ * Empty virtual destructor.
+ */
+ virtual ~IBoundedEventuallyModelChecker() {
+ // Intentionally left empty
+ }
+
/*!
- * @brief Evaluates BoundedEventually formula within a model checker.
- *
- * @param obj Formula object with subformulas.
- * @return Result of the formula for every node.
- */
+ * Evaluates a BoundedEventually formula within a model checker.
+ *
+ * @param obj Formula object with subformulas.
+ * @return The modelchecking result of the formula for every state.
+ */
virtual std::vector<T> checkBoundedEventually(const BoundedEventually<T>& obj) const = 0;
};
/*!
- * @brief
- * Class for an abstract (path) formula tree with a BoundedEventually node as root.
+ * Class for a Ltl formula tree with a BoundedEventually node as root.
*
- * Has one Abstract LTL formulas as sub formula/tree.
+ * Has one Ltl formula as subformula/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)
+ * The object has shared ownership of its subtree. If this object is deleted and no other object has a shared
+ * ownership of the subtree it will be deleted as well.
*
* @see AbstractLtlFormula
*/
@@ -57,27 +65,25 @@ class BoundedEventually : public AbstractLtlFormula<T> {
public:
/*!
- * Empty constructor
+ * Creates a BoundedEventually node without a subnode.
+ * The resulting object will not represent a complete formula!
*/
BoundedEventually() : child(nullptr), bound(0) {
// Intentionally left empty.
}
/*!
- * Constructor
+ * Creates a BoundedEventually node using the given parameters.
*
- * @param child The child formula subtree
- * @param bound The maximal number of steps
+ * @param child The child formula subtree.
+ * @param bound The maximal number of steps within which the subformula must hold.
*/
BoundedEventually(std::shared_ptr<AbstractLtlFormula<T>> child, uint_fast64_t bound) : child(child), bound(bound) {
// Intentionally left empty.
}
/*!
- * Destructor.
- *
- * Also deletes the subtrees.
- * (this behaviour can be prevented by setting the subtrees to NULL before deletion)
+ * Empty virtual destructor.
*/
virtual ~BoundedEventually() {
// Intentionally left empty.
@@ -87,14 +93,14 @@ public:
/*!
* Clones the called object.
*
- * Performs a "deep copy", i.e. the subtrees of the new object are clones of the original ones
+ * Performs a "deep copy", i.e. the subnodes of the new object are clones of the original ones.
*
- * @returns a new BoundedUntil-object that is identical the called object.
+ * @returns A new BoundedEventually object that is a deep copy of the called object.
*/
virtual std::shared_ptr<AbstractLtlFormula<T>> clone() const override {
std::shared_ptr<BoundedEventually<T>> result(new BoundedEventually<T>());
result->setBound(bound);
- if (this->childIsSet()) {
+ if (this->isChildSet()) {
result->setChild(child->clone());
}
return result;
@@ -115,7 +121,9 @@ public:
}
/*!
- * @returns a string representation of the formula
+ * Returns a textual representation of the formula tree with this node as root.
+ *
+ * @returns A string representing the formula tree.
*/
virtual std::string toString() const override {
std::string result = "F<=";
@@ -126,39 +134,45 @@ public:
}
/*!
- * @returns the child node
+ * Gets the child node.
+ *
+ * @returns The child node.
*/
std::shared_ptr<AbstractLtlFormula<T>> const & getChild() const {
return child;
}
/*!
- * Sets the subtree
- * @param child the new child node
+ * Sets the subtree.
+ *
+ * @param child The new child.
*/
void setChild(std::shared_ptr<AbstractLtlFormula<T>> const & child) {
this->child = child;
}
/*!
+ * Checks if the child is set, i.e. it does not point to null.
*
- * @return True if the child is set, i.e. it does not point to nullptr; false otherwise
+ * @return True iff the child is set.
*/
- bool childIsSet() const {
+ bool isChildSet() const {
return child.get() != nullptr;
}
/*!
- * @returns the maximally allowed number of steps for the bounded until operator
+ * Gets the maximally allowed number of steps for the bounded eventually operator.
+ *
+ * @returns The bound.
*/
uint_fast64_t getBound() const {
return bound;
}
/*!
- * Sets the maximally allowed number of steps for the bounded until operator
+ * Sets the maximally allowed number of steps for the bounded eventually operator.
*
- * @param bound the new bound.
+ * @param bound The new bound.
*/
void setBound(uint_fast64_t bound) {
this->bound = bound;
@@ -166,7 +180,11 @@ public:
private:
+
+ // The child node.
std::shared_ptr<AbstractLtlFormula<T>> child;
+
+ // The maximal number of steps within which the subformula must hold.
uint_fast64_t bound;
};
diff --git a/src/formula/ltl/BoundedUntil.h b/src/formula/ltl/BoundedUntil.h
index 87e0a7a2d..748e3ae0e 100644
--- a/src/formula/ltl/BoundedUntil.h
+++ b/src/formula/ltl/BoundedUntil.h
@@ -17,38 +17,46 @@ namespace storm {
namespace property {
namespace ltl {
+// Forward declaration for the interface class.
template <class T> class BoundedUntil;
/*!
- * @brief Interface class for model checkers that support BoundedUntil.
+ * Interface class for model checkers that support BoundedUntil.
*
- * All model checkers that support the formula class BoundedUntil must inherit
- * this pure virtual class.
+ * All model checkers that support the formula class BoundedUntil must inherit
+ * this pure virtual class.
*/
template <class T>
class IBoundedUntilModelChecker {
public:
+
+ /*!
+ * Empty virtual destructor.
+ */
+ virtual ~IBoundedUntilModelChecker() {
+ // Intentionally left empty
+ }
+
/*!
- * @brief Evaluates BoundedUntil formula within a model checker.
- *
- * @param obj Formula object with subformulas.
- * @return Result of the formula for every node.
- */
+ * Evaluates a BoundedUntil formula within a model checker.
+ *
+ * @param obj Formula object with subformulas.
+ * @return The modelchecking result of the formula for every state.
+ */
virtual std::vector<T> checkBoundedUntil(const BoundedUntil<T>& obj) const = 0;
};
/*!
- * @brief
- * Class for an abstract (path) formula tree with a BoundedUntil node as root.
+ * Class for an Ltl formula tree with a BoundedUntil node as root.
*
- * Has two Abstract LTL formulas as sub formulas/trees.
+ * Has two Ltl formulas as sub formulas/trees.
*
* @par Semantics
* The formula holds iff in at most \e bound steps, formula \e right (the right subtree) holds, and before,
* \e left 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)
+ * The object has shared ownership of its subtrees. If this object is deleted and no other object has a shared
+ * ownership of the subtrees they will be deleted as well.
*
* @see AbstractLtlFormula
*/
@@ -58,28 +66,26 @@ class BoundedUntil : public AbstractLtlFormula<T> {
public:
/*!
- * Empty constructor
+ * Creates a BoundedUntil node without subnodes.
+ * The resulting object will not represent a complete formula!
*/
BoundedUntil() : left(nullptr), right(nullptr), bound(0) {
// Intentionally left empty.
}
/*!
- * Constructor
+ * Creates a BoundedUntil node using the given parameters.
*
- * @param left The left formula subtree
- * @param right The left formula subtree
- * @param bound The maximal number of steps
+ * @param left The left formula subtree.
+ * @param right The right formula subtree.
+ * @param bound The maximal number of steps within which the right subformula must hold.
*/
BoundedUntil(std::shared_ptr<AbstractLtlFormula<T>> const & left, std::shared_ptr<AbstractLtlFormula<T>> const & right, uint_fast64_t bound) : left(left), right(right), bound(bound) {
// Intentionally left empty.
}
/*!
- * Destructor.
- *
- * Also deletes the subtrees.
- * (this behaviour can be prevented by setting the subtrees to NULL before deletion)
+ * Empty virtual destructor.
*/
virtual ~BoundedUntil() {
// Intentionally left empty.
@@ -88,17 +94,17 @@ public:
/*!
* Clones the called object.
*
- * Performs a "deep copy", i.e. the subtrees of the new object are clones of the original ones
+ * Performs a "deep copy", i.e. the subnodes of the new object are clones of the original ones.
*
- * @returns a new BoundedUntil-object that is identical the called object.
+ * @returns A new BoundedUntil object that is a deep copy of the called object.
*/
virtual std::shared_ptr<AbstractLtlFormula<T>> clone() const override {
std::shared_ptr<BoundedUntil<T>> result(new BoundedUntil<T>());
result->setBound(bound);
- if (this->leftIsSet()) {
+ if (this->isLeftSet()) {
result->setLeft(left->clone());
}
- if (this->rightIsSet()) {
+ if (this->isRightSet()) {
result->setRight(right->clone());
}
return result;
@@ -119,12 +125,9 @@ public:
}
/*!
- * @brief Return string representation of this formula.
- *
- * In LTL, brackets are needed around the until, as Until may appear nested (in other logics, Until always is the
- * root of a path formula); hence this function is overwritten in this class.
+ * Returns a textual representation of the formula tree with this node as root.
*
- * @return A string representation of the formula.
+ * @returns A string representing the formula tree.
*/
virtual std::string toString() const override {
std::string result = "(" + left->toString();
@@ -136,72 +139,86 @@ public:
}
/*!
- * Sets the left child node.
+ * Gets the left child node.
*
- * @param newLeft the new left child.
+ * @returns The left child node.
*/
- void setLeft(std::shared_ptr<AbstractLtlFormula<T>> const & newLeft) {
- left = newLeft;
+ std::shared_ptr<AbstractLtlFormula<T>> const & getLeft() const {
+ return left;
}
/*!
- * Sets the right child node.
+ * Gets the right child node.
*
- * @param newRight the new right child.
+ * @returns The right child node.
*/
- void setRight(std::shared_ptr<AbstractLtlFormula<T>> const & newRight) {
- right = newRight;
+ std::shared_ptr<AbstractLtlFormula<T>> const & getRight() const {
+ return right;
}
/*!
- * @returns a pointer to the left child node
+ * Sets the left child node.
+ *
+ * @param newLeft The new left child.
*/
- std::shared_ptr<AbstractLtlFormula<T>> const & getLeft() const {
- return left;
+ void setLeft(std::shared_ptr<AbstractLtlFormula<T>> const & newLeft) {
+ left = newLeft;
}
/*!
- * @returns a pointer to the right child node
+ * Sets the right child node.
+ *
+ * @param newRight The new right child.
*/
- std::shared_ptr<AbstractLtlFormula<T>> const & getRight() const {
- return right;
+ void setRight(std::shared_ptr<AbstractLtlFormula<T>> const & newRight) {
+ right = newRight;
}
/*!
+ * Checks if the left child is set, i.e. it does not point to null.
*
- * @return True if the left child is set, i.e. it does not point to nullptr; false otherwise
+ * @return True iff the left child is set.
*/
- bool leftIsSet() const {
+ bool isLeftSet() const {
return left.get() != nullptr;
}
/*!
+ * Checks if the right child is set, i.e. it does not point to null.
*
- * @return True if the right child is set, i.e. it does not point to nullptr; false otherwise
+ * @return True iff the right child is set.
*/
- bool rightIsSet() const {
+ bool isRightSet() const {
return right.get() != nullptr;
}
/*!
- * @returns the maximally allowed number of steps for the bounded until operator
+ * Gets the maximally allowed number of steps for the bounded until operator.
+ *
+ * @returns The bound.
*/
uint_fast64_t getBound() const {
return bound;
}
/*!
- * Sets the maximally allowed number of steps for the bounded until operator
+ * Sets the maximally allowed number of steps for the bounded until operator.
*
- * @param bound the new bound.
+ * @param bound The new bound.
*/
void setBound(uint_fast64_t bound) {
this->bound = bound;
}
private:
+
+ // The left child node.
std::shared_ptr<AbstractLtlFormula<T>> left;
+
+ // The right child node.
std::shared_ptr<AbstractLtlFormula<T>> right;
+
+ // The maximal number of steps within which the subformulas must hold.
uint_fast64_t bound;
};
diff --git a/src/formula/ltl/Eventually.h b/src/formula/ltl/Eventually.h
index 328fd993b..9af8ad9b2 100644
--- a/src/formula/ltl/Eventually.h
+++ b/src/formula/ltl/Eventually.h
@@ -1,5 +1,5 @@
/*
- * Next.h
+ * Eventually.h
*
* Created on: 26.12.2012
* Author: Christian Dehnert
@@ -15,37 +15,45 @@ namespace storm {
namespace property {
namespace ltl {
+// Forward declaration for the interface class.
template <class T> class Eventually;
/*!
- * @brief Interface class for model checkers that support Eventually.
+ * Interface class for model checkers that support Eventually.
*
- * All model checkers that support the formula class Eventually must inherit
- * this pure virtual class.
+ * All model checkers that support the formula class Eventually must inherit
+ * this pure virtual class.
*/
template <class T>
class IEventuallyModelChecker {
public:
+
/*!
- * @brief Evaluates Eventually formula within a model checker.
- *
- * @param obj Formula object with subformulas.
- * @return Result of the formula for every node.
- */
+ * Empty virtual destructor.
+ */
+ virtual ~IEventuallyModelChecker() {
+ // Intentionally left empty.
+ }
+
+ /*!
+ * Evaluates an Eventually formula within a model checker.
+ *
+ * @param obj Formula object with subformulas.
+ * @return The modelchecking result of the formula for every state.
+ */
virtual std::vector<T> checkEventually(const Eventually<T>& obj) const = 0;
};
/*!
- * @brief
- * Class for an abstract (path) formula tree with an Eventually node as root.
+ * Class for an Ltl formula tree with an Eventually node as root.
*
- * Has one Abstract LTL formula as sub formula/tree.
+ * Has one Abstract Ltl formula as sub formula/tree.
*
* @par Semantics
* The formula holds iff eventually \e child holds.
*
- * The subtree is seen as part of the object and deleted with the object
- * (this behavior can be prevented by setting them to nullptr before deletion)
+ * The object has shared ownership of its subtree. If this object is deleted and no other object has a shared
+ * ownership of the subtree it will be deleted as well.
*
* @see AbstractLtlFormula
*/
@@ -55,26 +63,24 @@ class Eventually : public AbstractLtlFormula<T> {
public:
/*!
- * Empty constructor
+ * Creates an Eventually node without a subnode.
+ * The resulting object will not represent a complete formula!
*/
Eventually() : child(nullptr) {
// Intentionally left empty.
}
/*!
- * Constructor
+ * Creates an Eventually node using the given parameter.
*
- * @param child The child node
+ * @param child The child formula subtree.
*/
Eventually(std::shared_ptr<AbstractLtlFormula<T>> const & child) : child(child) {
// Intentionally left empty.
}
/*!
- * Constructor.
- *
- * Also deletes the subtree.
- * (this behaviour can be prevented by setting the subtrees to nullptr before deletion)
+ * Empty virtual destructor.
*/
virtual ~Eventually() {
// Intentionally left empty.
@@ -83,13 +89,13 @@ public:
/*!
* Clones the called object.
*
- * Performs a "deep copy", i.e. the subtrees of the new object are clones of the original ones
+ * Performs a "deep copy", i.e. the subnodes of the new object are clones of the original ones.
*
- * @returns a new Eventually-object that is identical the called object.
+ * @returns A new Eventually object that is a deep copy of the called object.
*/
virtual std::shared_ptr<AbstractLtlFormula<T>> clone() const override {
std::shared_ptr<Eventually<T>> result(new Eventually<T>());
- if (this->childIsSet()) {
+ if (this->isChildSet()) {
result->setChild(child->clone());
}
return result;
@@ -109,7 +115,9 @@ public:
}
/*!
- * @returns a string representation of the formula
+ * Returns a textual representation of the formula tree with this node as root.
+ *
+ * @returns A string representing the formula tree.
*/
virtual std::string toString() const override {
std::string result = "F ";
@@ -118,29 +126,35 @@ public:
}
/*!
- * @returns the child node
+ * Gets the child node.
+ *
+ * @returns The child node.
*/
std::shared_ptr<AbstractLtlFormula<T>> const & getChild() const {
return child;
}
/*!
- * Sets the subtree
- * @param child the new child node
+ * Sets the subtree.
+ *
+ * @param child The new child.
*/
void setChild(std::shared_ptr<AbstractLtlFormula<T>> const & child) {
this->child = child;
}
/*!
+ * Checks if the child is set, i.e. it does not point to null.
*
- * @return True if the child node is set, i.e. it does not point to nullptr; false otherwise
+ * @return True iff the child is set.
*/
- bool childIsSet() const {
+ bool isChildSet() const {
return child.get() != nullptr;
}
private:
+
+ // The child node.
std::shared_ptr<AbstractLtlFormula<T>> child;
};
diff --git a/src/formula/ltl/Globally.h b/src/formula/ltl/Globally.h
index 060b5bba2..0e0af887a 100644
--- a/src/formula/ltl/Globally.h
+++ b/src/formula/ltl/Globally.h
@@ -1,5 +1,5 @@
/*
- * Next.h
+ * Globally.h
*
* Created on: 26.12.2012
* Author: Christian Dehnert
@@ -15,37 +15,45 @@ namespace storm {
namespace property {
namespace ltl {
+// Forward declaration for the interface class.
template <class T> class Globally;
/*!
- * @brief Interface class for model checkers that support Globally.
+ * Interface class for model checkers that support Globally.
*
- * All model checkers that support the formula class Globally must inherit
- * this pure virtual class.
+ * All model checkers that support the formula class Globally must inherit
+ * this pure virtual class.
*/
template <class T>
class IGloballyModelChecker {
public:
+
/*!
- * @brief Evaluates Globally formula within a model checker.
- *
- * @param obj Formula object with subformulas.
- * @return Result of the formula for every node.
- */
+ * Empty virtual destructor.
+ */
+ virtual ~IGloballyModelChecker() {
+ // Intentionally left empty
+ }
+
+ /*!
+ * Evaluates a Globally formula within a model checker.
+ *
+ * @param obj Formula object with subformulas.
+ * @return The modelchecking result of the formula for every state.
+ */
virtual std::vector<T> checkGlobally(const Globally<T>& obj) const = 0;
};
/*!
- * @brief
- * Class for an abstract (path) formula tree with a Globally node as root.
+ * Class for an Ltl formula tree with a Globally node as root.
*
- * Has one Abstract LTL formula as sub formula/tree.
+ * Has one Ltl formula as sub formula/tree.
*
* @par Semantics
- * The formula holds iff globally \e child holds.
+ * The formula holds iff always formula \e child holds.
*
- * The subtree is seen as part of the object and deleted with the object
- * (this behavior can be prevented by setting them to nullptr before deletion)
+ * The object has shared ownership of its subtree. If this object is deleted and no other object has a shared
+ * ownership of the subtree it will be deleted as well.
*
* @see AbstractLtlFormula
*/
@@ -55,26 +63,24 @@ class Globally : public AbstractLtlFormula<T> {
public:
/*!
- * Empty constructor
+ * Creates a Globally node without a subnode.
+ * The resulting object will not represent a complete formula!
*/
Globally() : child(nullptr) {
// Intentionally left empty.
}
/*!
- * Constructor
+ * Creates a Globally node using the given parameter.
*
- * @param child The child node
+ * @param child The child formula subtree.
*/
Globally(std::shared_ptr<AbstractLtlFormula<T>> const & child) : child(child) {
// Intentionally left empty.
}
/*!
- * Constructor.
- *
- * Also deletes the subtree.
- * (this behaviour can be prevented by setting the subtrees to nullptr before deletion)
+ * Empty virtual destructor.
*/
virtual ~Globally() {
// Intentionally left empty.
@@ -83,13 +89,13 @@ public:
/*!
* Clones the called object.
*
- * Performs a "deep copy", i.e. the subtrees of the new object are clones of the original ones
+ * Performs a "deep copy", i.e. the subnodes of the new object are clones of the original ones.
*
- * @returns a new Globally-object that is identical the called object.
+ * @returns A new Globally object that is a deep copy of the called object.
*/
virtual std::shared_ptr<AbstractLtlFormula<T>> clone() const override {
std::shared_ptr<Globally<T>> result(new Globally<T>());
- if (this->childIsSet()) {
+ if (this->isChildSet()) {
result->setChild(child->clone());
}
return result;
@@ -109,7 +115,9 @@ public:
}
/*!
- * @returns a string representation of the formula
+ * Returns a textual representation of the formula tree with this node as root.
+ *
+ * @returns A string representing the formula tree.
*/
virtual std::string toString() const override {
std::string result = "G ";
@@ -118,30 +126,36 @@ public:
}
/*!
- * @returns the child node
+ * Gets the child node.
+ *
+ * @returns The child node.
*/
std::shared_ptr<AbstractLtlFormula<T>> const & getChild() const {
return *child;
}
/*!
- * Sets the subtree
- * @param child the new child node
+ * Sets the subtree.
+ *
+ * @param child The new child.
*/
void setChild(std::shared_ptr<AbstractLtlFormula<T>> const & child) {
this->child = child;
}
/*!
+ * Checks if the child is set, i.e. it does not point to null.
*
- * @return True if the child node is set, i.e. it does not point to nullptr; false otherwise
+ * @return True iff the child is set.
*/
- bool childIsSet() const {
+ bool isChildSet() const {
return child.get() != nullptr;
}
- private:
- std::shared_ptr<AbstractLtlFormula<T>> child;
+private:
+
+ // The child node.
+ std::shared_ptr<AbstractLtlFormula<T>> child;
};
} //namespace ltl
diff --git a/src/formula/ltl/LtlFilter.h b/src/formula/ltl/LtlFilter.h
index 9f876bd8c..4b7704b10 100644
--- a/src/formula/ltl/LtlFilter.h
+++ b/src/formula/ltl/LtlFilter.h
@@ -14,51 +14,85 @@
#include "src/formula/actions/AbstractAction.h"
#include "src/exceptions/NotImplementedException.h"
-namespace storm {
-namespace property {
-namespace action {
- template <typename T> class AbstractAction;
-}
-}
-}
-
namespace storm {
namespace property {
namespace ltl {
+/*!
+ * This is the Ltl specific filter.
+ *
+ * It maintains a Ltl formula which can be checked against a given model by either calling evaluate() or check().
+ * Additionally it maintains a list of filter actions that are used to further manipulate the modelchecking results and prepare them for output.
+ */
template <class T>
class LtlFilter : public storm::property::AbstractFilter<T> {
+ // Convenience typedef to make the code more readable.
typedef typename storm::property::action::AbstractAction<T>::Result Result;
public:
+ /*!
+ * Creates an empty LtlFilter, maintaining no Ltl formula.
+ *
+ * Calling check or evaluate will return an empty result.
+ */
LtlFilter() : AbstractFilter<T>(UNDEFINED), child(nullptr) {
// Intentionally left empty.
}
+ /*!
+ * Creates an LtlFilter maintaining an Ltl formula but containing no actions.
+ *
+ * The modelchecking result will be returned or printed as is.
+ *
+ * @param child The Ltl formula to be maintained.
+ * @param opt An enum value indicating which kind of scheduler shall be used for path formulas on nondeterministic models.
+ */
LtlFilter(std::shared_ptr<AbstractLtlFormula<T>> const & child, OptimizingOperator opt = UNDEFINED) : AbstractFilter<T>(opt), child(child) {
// Intentionally left empty.
}
+ /*!
+ * Creates an LtlFilter maintaining a Ltl formula and containing a single action.
+ *
+ * The given action will be applied to the modelchecking result during evaluation.
+ * Further actions can be added later.
+ *
+ * @param child The Ltl formula to be maintained.
+ * @param action The single action to be executed during evaluation.
+ * @param opt An enum value indicating which kind of scheduler shall be used for path formulas on nondeterministic models.
+ */
LtlFilter(std::shared_ptr<AbstractLtlFormula<T>> const & child, std::shared_ptr<action::AbstractAction<T>> const & action, OptimizingOperator opt = UNDEFINED) : AbstractFilter<T>(action, opt), child(child) {
// Intentionally left empty.
}
+ /*!
+ * Creates an LtlFilter using the given parameters.
+ *
+ * The given actions will be applied to the modelchecking result in ascending index order during evaluation.
+ * Further actions can be added later.
+ *
+ * @param child The Ltl formula to be maintained.
+ * @param actions A vector conatining the actions that are to be executed during evaluation.
+ * @param opt An enum value indicating which kind of scheduler shall be used for path formulas on nondeterministic models.
+ */
LtlFilter(std::shared_ptr<AbstractLtlFormula<T>> const & child, std::vector<std::shared_ptr<action::AbstractAction<T>>> const & actions, OptimizingOperator opt = UNDEFINED) : AbstractFilter<T>(actions, opt), child(child) {
// Intentionally left empty.
}
+ /*!
+ * Empty virtual destructor.
+ */
virtual ~LtlFilter() {
// Intentionally left empty.
}
- /*!Description copied from the MC.
- * Checks the given state formula on the model and prints the result (true/false) for all initial states, i.e.
- * states that carry the atomic proposition "init".
+ /*!
+ * Calls the modelchecker, retrieves the modelchecking result, applies the filter action one by one and prints out the result.
*
- * @param stateFormula The formula to be checked.
+ * @param modelchecker The modelchecker to be called.
*/
void check(storm::modelchecker::ltl::AbstractModelChecker<T> const & modelchecker) const {
@@ -83,6 +117,12 @@ public:
}
+ /*!
+ * Calls the modelchecker, retrieves the modelchecking result, applies the filter action one by one and returns the result.
+ *
+ * @param modelchecker The modelchecker to be called.
+ * @returns The result of the sequential application of the filter actions to the modelchecking result.
+ */
Result evaluate(storm::modelchecker::ltl::AbstractModelChecker<T> const & modelchecker) const {
// First, get the model checking result.
Result result;
@@ -112,6 +152,13 @@ public:
return result;
}
+ /*!
+ * Returns a textual representation of the filter.
+ *
+ * That includes the actions as well as the maintained formula.
+ *
+ * @returns A string representing the filter.
+ */
std::string toString() const override {
std::string desc = "";
@@ -151,26 +198,41 @@ public:
return desc;
}
- virtual std::string toPrettyString() const override {
- std::string desc = "Filter: ";
- desc += "\nActions:";
- for(auto action : this->actions) {
- desc += "\n\t" + action->toString();
- }
- desc += "\nFormula:\n\t" + child->toString();
- return desc;
+ /*!
+ * Gets the child node.
+ *
+ * @returns The child node.
+ */
+ std::shared_ptr<AbstractLtlFormula<T>> const & getChild() const {
+ return child;
}
+ /*!
+ * Sets the subtree.
+ *
+ * @param child The new child.
+ */
void setChild(std::shared_ptr<AbstractLtlFormula<T>> const & child) {
this->child = child;
}
- std::shared_ptr<AbstractLtlFormula<T>> const & getChild() const {
- return child;
+ /*!
+ * Checks if the child is set, i.e. it does not point to null.
+ *
+ * @return True iff the child is set.
+ */
+ bool isChildSet() const {
+ return child.get() != nullptr;
}
private:
+ /*!
+ * Writes out the given result.
+ *
+ * @param result The result of the sequential application of the filter actions to a modelchecking result.
+ * @param modelchecker The modelchecker that was called to generate the modelchecking result. Needed for legacy support.
+ */
void writeOut(Result const & result, storm::modelchecker::ltl::AbstractModelChecker<T> const & modelchecker) const {
// Test for the kind of result. Values or states.
@@ -207,6 +269,7 @@ private:
std::cout << std::endl << "-------------------------------------------" << std::endl;
}
+ // The Ltl formula maintained by this filter.
std::shared_ptr<AbstractLtlFormula<T>> child;
};
diff --git a/src/formula/ltl/Next.h b/src/formula/ltl/Next.h
index a038252c2..0eb64a2ed 100644
--- a/src/formula/ltl/Next.h
+++ b/src/formula/ltl/Next.h
@@ -14,37 +14,45 @@ namespace storm {
namespace property {
namespace ltl {
+// Forward declaration for the interface class.
template <class T> class Next;
/*!
- * @brief Interface class for model checkers that support Next.
+ * Interface class for model checkers that support Next.
*
- * All model checkers that support the formula class Next must inherit
- * this pure virtual class.
+ * All model checkers that support the formula class Next must inherit
+ * this pure virtual class.
*/
template <class T>
class INextModelChecker {
public:
+
/*!
- * @brief Evaluates Next formula within a model checker.
- *
- * @param obj Formula object with subformulas.
- * @return Result of the formula for every node.
- */
+ * Empty virtual destructor.
+ */
+ virtual ~INextModelChecker() {
+ // Intentionally left empty
+ }
+
+ /*!
+ * Evaluates Next formula within a model checker.
+ *
+ * @param obj Formula object with subformulas.
+ * @return Result of the formula for every node.
+ */
virtual std::vector<T> checkNext(const Next<T>& obj) const = 0;
};
/*!
- * @brief
- * Class for an abstract (path) formula tree with a Next node as root.
+ * Class for an Ltl formula tree with a Next node as root.
*
- * Has two Abstract LTL formulas as sub formulas/trees.
+ * Has two LTL formulas as sub formulas/trees.
*
* @par Semantics
- * The formula holds iff in the next step, \e child holds
+ * The formula holds iff in the next step, formula \e child holds
*
- * The subtree is seen as part of the object and deleted with the object
- * (this behavior can be prevented by setting them to NULL before deletion)
+ * The object has shared ownership of its subtree. If this object is deleted and no other object has a shared
+ * ownership of the subtree it will be deleted as well.
*
* @see AbstractLtlFormula
*/
@@ -54,26 +62,24 @@ class Next : public AbstractLtlFormula<T> {
public:
/*!
- * Empty constructor
+ * Creates a Next node without a subnode.
+ * The resulting object will not represent a complete formula!
*/
Next() : child(nullptr) {
// Intentionally left empty.
}
/*!
- * Constructor
+ * Creates a Next node using the given parameter.
*
- * @param child The child node
+ * @param child The child formula subtree.
*/
Next(std::shared_ptr<AbstractLtlFormula<T>> const & child) : child(child) {
// Intentionally left empty.
}
/*!
- * Constructor.
- *
- * Also deletes the subtree.
- * (this behaviour can be prevented by setting the subtrees to NULL before deletion)
+ * Empty virtual destructor.
*/
virtual ~Next() {
// Intentionally left empty.
@@ -82,13 +88,13 @@ public:
/*!
* Clones the called object.
*
- * Performs a "deep copy", i.e. the subtrees of the new object are clones of the original ones
+ * Performs a "deep copy", i.e. the subnodes of the new object are clones of the original ones.
*
- * @returns a new BoundedUntil-object that is identical the called object.
+ * @returns A new Next object that is a deep copy of the called object.
*/
virtual std::shared_ptr<AbstractLtlFormula<T>> clone() const override {
std::shared_ptr<Next<T>> result(new Next<T>());
- if (this->childIsSet()) {
+ if (this->isChildSet()) {
result->setChild(child->clone());
}
return result;
@@ -108,7 +114,9 @@ public:
}
/*!
- * @returns a string representation of the formula
+ * Returns a textual representation of the formula tree with this node as root.
+ *
+ * @returns A string representing the formula tree.
*/
virtual std::string toString() const override {
std::string result = "X ";
@@ -117,29 +125,35 @@ public:
}
/*!
- * @returns the child node
+ * Gets the child node.
+ *
+ * @returns The child node.
*/
std::shared_ptr<AbstractLtlFormula<T>> const & getChild() const {
return child;
}
/*!
- * Sets the subtree
- * @param child the new child node
+ * Sets the subtree.
+ *
+ * @param child The new child.
*/
void setChild(std::shared_ptr<AbstractLtlFormula<T>> const & child) {
this->child = child;
}
/*!
+ * Checks if the child is set, i.e. it does not point to null.
*
- * @return True if the child node is set, i.e. it does not point to nullptr; false otherwise
+ * @return True iff the child is set.
*/
- bool childIsSet() const {
+ bool isChildSet() const {
return child.get() != nullptr;
}
private:
+
+ // The child node.
std::shared_ptr<AbstractLtlFormula<T>> child;
};
diff --git a/src/formula/ltl/Not.h b/src/formula/ltl/Not.h
index 2538298a4..cd1edd251 100644
--- a/src/formula/ltl/Not.h
+++ b/src/formula/ltl/Not.h
@@ -14,34 +14,42 @@ namespace storm {
namespace property {
namespace ltl {
+// Forward declaration for the interface class.
template <class T> class Not;
/*!
- * @brief Interface class for model checkers that support Not.
+ * Interface class for model checkers that support Not.
*
- * All model checkers that support the formula class Not must inherit
- * this pure virtual class.
+ * All model checkers that support the formula class Not must inherit
+ * this pure virtual class.
*/
template <class T>
class INotModelChecker {
public:
+
/*!
- * @brief Evaluates Not formula within a model checker.
- *
- * @param obj Formula object with subformulas.
- * @return Result of the formula for every node.
- */
+ * Empty virtual destructor.
+ */
+ virtual ~INotModelChecker() {
+ // Intentionally left empty
+ }
+
+ /*!
+ * Evaluates Not formula within a model checker.
+ *
+ * @param obj Formula object with subformulas.
+ * @return Result of the formula for every node.
+ */
virtual std::vector<T> checkNot(const Not<T>& obj) const = 0;
};
/*!
- * @brief
- * Class for an abstract formula tree with NOT node as root.
+ * Class for an Ltl formula tree with a Not node as root.
*
- * Has one Abstract LTL formula as sub formula/tree.
+ * Has one Ltl formula as sub formula/tree.
*
- * The subtree is seen as part of the object and deleted with the object
- * (this behavior can be prevented by setting them to NULL before deletion)
+ * The object has shared ownership of its subtree. If this object is deleted and no other object has a shared
+ * ownership of the subtree it will be deleted as well.
*
* @see AbstractLtlFormula
*/
@@ -51,25 +59,24 @@ class Not : public AbstractLtlFormula<T> {
public:
/*!
- * Empty constructor
+ * Creates a Not node without a subnode.
+ * The resulting object will not represent a complete formula!
*/
Not() : child(nullptr) {
// Intentionally left empty.
}
/*!
- * Constructor
- * @param child The child node
+ * Creates a Not node using the given parameter.
+ *
+ * @param child The child formula subtree.
*/
Not(std::shared_ptr<AbstractLtlFormula<T>> const & child) : child(child) {
// Intentionally left empty.
}
/*!
- * Destructor
- *
- * Also deletes the subtree
- * (this behavior can be prevented by setting them to NULL before deletion)
+ * Empty virtual destructor.
*/
virtual ~Not() {
// Intentionally left empty.
@@ -78,13 +85,13 @@ public:
/*!
* Clones the called object.
*
- * Performs a "deep copy", i.e. the subtrees of the new object are clones of the original ones
+ * Performs a "deep copy", i.e. the subnodes of the new object are clones of the original ones.
*
- * @returns a new AND-object that is identical the called object.
+ * @returns A new Not object that is a deep copy of the called object.
*/
virtual std::shared_ptr<AbstractLtlFormula<T>> clone() const override {
std::shared_ptr<Not<T>> result(new Not<T>());
- if (this->childIsSet()) {
+ if (this->isChildSet()) {
result->setChild(child->clone());
}
return result;
@@ -104,7 +111,9 @@ public:
}
/*!
- * @returns a string representation of the formula
+ * Returns a textual representation of the formula tree with this node as root.
+ *
+ * @returns A string representing the formula tree.
*/
virtual std::string toString() const override {
std::string result = "!";
@@ -123,29 +132,35 @@ public:
}
/*!
- * @returns The child node
+ * Gets the child node.
+ *
+ * @returns The child node.
*/
std::shared_ptr<AbstractLtlFormula<T>> const & getChild() const {
return child;
}
/*!
- * Sets the subtree
- * @param child the new child node
+ * Sets the subtree.
+ *
+ * @param child The new child.
*/
void setChild(std::shared_ptr<AbstractLtlFormula<T>> const & child) {
this->child = child;
}
/*!
+ * Checks if the child is set, i.e. it does not point to null.
*
- * @return True if the child node is set, i.e. it does not point to nullptr; false otherwise
+ * @return True iff the child is set.
*/
- bool childIsSet() const {
+ bool isChildSet() const {
return child.get() != nullptr;
}
private:
+
+ // The child node.
std::shared_ptr<AbstractLtlFormula<T>> child;
};
diff --git a/src/formula/ltl/Or.h b/src/formula/ltl/Or.h
index 42296766f..a7c73a1f1 100644
--- a/src/formula/ltl/Or.h
+++ b/src/formula/ltl/Or.h
@@ -14,37 +14,45 @@ namespace storm {
namespace property {
namespace ltl {
+// Forward declaration for the interface class.
template <class T> class Or;
/*!
- * @brief Interface class for model checkers that support And.
+ * Interface class for model checkers that support Or.
*
- * All model checkers that support the formula class And must inherit
- * this pure virtual class.
+ * All model checkers that support the formula class Or must inherit
+ * this pure virtual class.
*/
template <class T>
class IOrModelChecker {
public:
+
+ /*!
+ * Empty virtual destructor.
+ */
+ virtual ~IOrModelChecker() {
+ // Intentionally left empty
+ }
+
/*!
- * @brief Evaluates And formula within a model checker.
+ * Evaluates Or formula within a model checker.
*
- * @param obj Formula object with subformulas.
- * @return Result of the formula for every node.
+ * @param obj Formula object with subformulas.
+ * @return Result of the formula for every node.
*/
virtual std::vector<T> checkOr(const Or<T>& obj) const = 0;
};
/*!
- * @brief
- * Class for an abstract formula tree with OR node as root.
+ * Class for an abstract formula tree with an Or node as root.
*
- * Has two LTL formulas as sub formulas/trees.
+ * Has two Ltl formulas as sub formulas/trees.
*
- * As OR is commutative, the order is \e theoretically not important, but will influence the order in which
+ * As Or is commutative, the order is \e theoretically not important, but will influence the order in which
* the model checker works.
*
- * 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)
+ * The object has shared ownership of its subtrees. If this object is deleted and no other object has a shared
+ * ownership of the subtrees they will be deleted as well.
*
* @see AbstractLtlFormula
*/
@@ -54,29 +62,25 @@ class Or: public storm::property::ltl::AbstractLtlFormula<T> {
public:
/*!
- * Empty constructor.
- * Will create an AND-node without subnotes. Will not represent a complete formula!
+ * Creates an Or node without subnodes.
+ * The resulting object will not represent a complete formula!
*/
Or() : left(nullptr), right(nullptr) {
// Intentionally left empty.
}
/*!
- * Constructor.
- * Creates an AND note with the parameters as subtrees.
+ * Creates an Or node with the parameters as subtrees.
*
- * @param left The left sub formula
- * @param right The right sub formula
+ * @param left The left sub formula.
+ * @param right The right sub formula.
*/
Or(std::shared_ptr<AbstractLtlFormula<T>> const & left, std::shared_ptr<AbstractLtlFormula<T>> const & right) : left(left), right(right) {
// Intentionally left empty.
}
/*!
- * Destructor.
- *
- * The subtrees are deleted with the object
- * (this behavior can be prevented by setting them to NULL before deletion)
+ * Empty virtual destructor.
*/
virtual ~Or() {
// Intentionally left empty.
@@ -85,16 +89,16 @@ public:
/*!
* Clones the called object.
*
- * Performs a "deep copy", i.e. the subtrees of the new object are clones of the original ones
+ * Performs a "deep copy", i.e. the subtrees of the new object are clones of the original ones.
*
- * @returns a new AND-object that is identical the called object.
+ * @returns A new Or object that is a deep copy of the called object.
*/
virtual std::shared_ptr<AbstractLtlFormula<T>> clone() const override {
std::shared_ptr<Or<T>> result(new Or<T>());
- if (this->leftIsSet()) {
+ if (this->isLeftSet()) {
result->setLeft(left->clone());
}
- if (this->rightIsSet()) {
+ if (this->isRightSet()) {
result->setRight(right->clone());
}
return result;
@@ -114,7 +118,9 @@ public:
}
/*!
- * @returns a string representation of the formula
+ * Returns a textual representation of the formula tree with this node as root.
+ *
+ * @returns A string representing the formula tree.
*/
virtual std::string toString() const override {
std::string result = "(";
@@ -136,55 +142,65 @@ public:
}
/*!
- * Sets the left child node.
+ * Gets the left child node.
*
- * @param newLeft the new left child.
+ * @returns The left child node.
*/
- void setLeft(std::shared_ptr<AbstractLtlFormula<T>> const & newLeft) {
- left = newLeft;
+ std::shared_ptr<AbstractLtlFormula<T>> const & getLeft() const {
+ return left;
}
/*!
- * Sets the right child node.
+ * Gets the right child node.
*
- * @param newRight the new right child.
+ * @returns The right child node.
*/
- void setRight(std::shared_ptr<AbstractLtlFormula<T>> const & newRight) {
- right = newRight;
+ std::shared_ptr<AbstractLtlFormula<T>> const & getRight() const {
+ return right;
}
/*!
- * @returns a pointer to the left child node
+ * Sets the left child node.
+ *
+ * @param newLeft The new left child.
*/
- std::shared_ptr<AbstractLtlFormula<T>> const & getLeft() const {
- return left;
+ void setLeft(std::shared_ptr<AbstractLtlFormula<T>> const & newLeft) {
+ left = newLeft;
}
/*!
- * @returns a pointer to the right child node
+ * Sets the right child node.
+ *
+ * @param newRight The new right child.
*/
- std::shared_ptr<AbstractLtlFormula<T>> const & getRight() const {
- return right;
+ void setRight(std::shared_ptr<AbstractLtlFormula<T>> const & newRight) {
+ right = newRight;
}
/*!
+ * Checks if the left child is set, i.e. it does not point to null.
*
- * @return True if the left child is set, i.e. it does not point to nullptr; false otherwise
+ * @return True iff the left child is set.
*/
- bool leftIsSet() const {
+ bool isLeftSet() const {
return left.get() != nullptr;
}
/*!
+ * Checks if the right child is set, i.e. it does not point to null.
*
- * @return True if the right child is set, i.e. it does not point to nullptr; false otherwise
+ * @return True iff the left right is set.
*/
- bool rightIsSet() const {
+ bool isRightSet() const {
return right.get() != nullptr;
}
private:
+
+ // The left child node.
std::shared_ptr<AbstractLtlFormula<T>> left;
+
+ // The right child node.
std::shared_ptr<AbstractLtlFormula<T>> right;
};
diff --git a/src/formula/ltl/Until.h b/src/formula/ltl/Until.h
index 92a6e4ed1..56301c0f4 100644
--- a/src/formula/ltl/Until.h
+++ b/src/formula/ltl/Until.h
@@ -14,56 +14,46 @@ namespace storm {
namespace property {
namespace ltl {
+// Forward declaration for the interface class.
template <class T> class Until;
/*!
- * @brief Interface class for model checkers that support Until.
+ * Interface class for model checkers that support Until.
*
- * All model checkers that support the formula class Until must inherit
- * this pure virtual class.
+ * All model checkers that support the formula class Until must inherit
+ * this pure virtual class.
*/
template <class T>
class IUntilModelChecker {
public:
+
/*!
- * @brief Evaluates Until formula within a model checker.
- *
- * @param obj Formula object with subformulas.
- * @return Result of the formula for every node.
- */
- virtual std::vector<T> checkUntil(const Until<T>& obj) const = 0;
-};
+ * Empty virtual destructor.
+ */
+ virtual ~IUntilModelChecker() {
+ // Intentionally left empty
+ }
-/*!
- * @brief Interface class for visitors that support Until.
- *
- * All visitors that support the formula class Until must inherit
- * this pure virtual class.
- */
-template <class T>
-class IUntilVisitor {
- public:
/*!
- * @brief Visits Until formula.
+ * Evaluates an Until formula within a model checker.
*
- * @param obj Formula object with subformulas.
- * @return Result of the formula for every node.
+ * @param obj Formula object with subformulas.
+ * @return The modelchecking result of the formula for every state.
*/
- virtual void visitUntil(const Until<T>& obj) = 0;
+ virtual std::vector<T> checkUntil(const Until<T>& obj) const = 0;
};
/*!
- * @brief
- * Class for an abstract (path) formula tree with an Until node as root.
+ * Class for an Ltl formula tree with an Until node as root.
*
- * Has two Abstract LTL formulas as sub formulas/trees.
+ * Has two Ltl formulas as sub formulas/trees.
*
* @par Semantics
* The formula holds iff eventually, formula \e right (the right subtree) holds, and before,
* \e left holds always.
*
- * 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)
+ * The object has shared ownership of its subtrees. If this object is deleted and no other object has a shared
+ * ownership of the subtrees they will be deleted as well.
*
* @see AbstractLtlFormula
*/
@@ -73,27 +63,25 @@ class Until : public AbstractLtlFormula<T> {
public:
/*!
- * Empty constructor
+ * Creates an Until node without subnodes.
+ * The resulting object will not represent a complete formula!
*/
- Until() : left(left), right(right) {
+ Until() : left(nullptr), right(nullptr) {
// Intentionally left empty.
}
/*!
- * Constructor
+ * Creates an Until node using the given parameters.
*
- * @param left The left formula subtree
- * @param right The left formula subtree
+ * @param left The left formula subtree.
+ * @param right The right formula subtree.
*/
Until(std::shared_ptr<AbstractLtlFormula<T>> const & left, std::shared_ptr<AbstractLtlFormula<T>> const & right) : left(left), right(right) {
// Intentionally left empty.
}
/*!
- * Destructor.
- *
- * Also deletes the subtrees.
- * (this behaviour can be prevented by setting the subtrees to NULL before deletion)
+ * Empty virtual destructor.
*/
virtual ~Until() {
// Intentionally left empty.
@@ -102,16 +90,16 @@ public:
/*!
* Clones the called object.
*
- * Performs a "deep copy", i.e. the subtrees of the new object are clones of the original ones
+ * Performs a "deep copy", i.e. the subnodes of the new object are clones of the original ones.
*
- * @returns a new BoundedUntil-object that is identical the called object.
+ * @returns A new Until object that is a deep copy of the called object.
*/
virtual std::shared_ptr<AbstractLtlFormula<T>> clone() const override {
std::shared_ptr<Until<T>> result(new Until<T>());
- if (this->leftIsSet()) {
+ if (this->isLeftSet()) {
result->setLeft(left->clone());
}
- if (this->rightIsSet()) {
+ if (this->isRightSet()) {
result->setRight(right->clone());
}
return result;
@@ -131,12 +119,9 @@ public:
}
/*!
- * @brief Return string representation of this formula.
- *
- * In LTL, brackets are needed around the until, as Until may appear nested (in other logics, Until always is the
- * root of a path formula); hence this function is overwritten in this class.
+ * Returns a textual representation of the formula tree with this node as root.
*
- * @return A string representation of the formula.
+ * @returns A string representing the formula tree.
*/
virtual std::string toString() const {
std::string result = "(" + left->toString();
@@ -146,55 +131,65 @@ public:
}
/*!
- * Sets the left child node.
+ * Gets the left child node.
*
- * @param newLeft the new left child.
+ * @returns The left child node.
*/
- void setLeft(std::shared_ptr<AbstractLtlFormula<T>> const & newLeft) {
- left = newLeft;
+ std::shared_ptr<AbstractLtlFormula<T>> const & getLeft() const {
+ return left;
}
/*!
- * Sets the right child node.
+ * Gets the right child node.
*
- * @param newRight the new right child.
+ * @returns The right child node.
*/
- void setRight(std::shared_ptr<AbstractLtlFormula<T>> const & newRight) {
- right = newRight;
+ std::shared_ptr<AbstractLtlFormula<T>> const & getRight() const {
+ return right;
}
/*!
- * @returns a pointer to the left child node
+ * Sets the left child node.
+ *
+ * @param newLeft The new left child.
*/
- std::shared_ptr<AbstractLtlFormula<T>> const & getLeft() const {
- return left;
+ void setLeft(std::shared_ptr<AbstractLtlFormula<T>> const & newLeft) {
+ left = newLeft;
}
/*!
- * @returns a pointer to the right child node
+ * Sets the right child node.
+ *
+ * @param newRight The new right child.
*/
- std::shared_ptr<AbstractLtlFormula<T>> const & getRight() const {
- return right;
+ void setRight(std::shared_ptr<AbstractLtlFormula<T>> const & newRight) {
+ right = newRight;
}
/*!
+ * Checks if the left child is set, i.e. it does not point to null.
*
- * @return True if the left child is set, i.e. it does not point to nullptr; false otherwise
+ * @return True iff the left child is set.
*/
- bool leftIsSet() const {
+ bool isLeftSet() const {
return left.get() != nullptr;
}
/*!
+ * Checks if the right child is set, i.e. it does not point to null.
*
- * @return True if the right child is set, i.e. it does not point to nullptr; false otherwise
+ * @return True iff the right child is set.
*/
- bool rightIsSet() const {
+ bool isRightSet() const {
return right.get() != nullptr;
}
private:
+
+ // The left child node.
std::shared_ptr<AbstractLtlFormula<T>> left;
+
+ // The right child node.
std::shared_ptr<AbstractLtlFormula<T>> right;
};
diff --git a/src/formula/prctl/AbstractPathFormula.h b/src/formula/prctl/AbstractPathFormula.h
index f8cb686b6..1caf60297 100644
--- a/src/formula/prctl/AbstractPathFormula.h
+++ b/src/formula/prctl/AbstractPathFormula.h
@@ -20,13 +20,7 @@ namespace property {
namespace prctl {
/*!
- * @brief
- * Abstract base class for Abstract path formulas.
- *
- * @attention This class is abstract.
- * @note Formula classes do not have copy constructors. The parameters of the constructors are usually the subtrees, so
- * the syntax conflicts with copy constructors for unary operators. To produce an identical object, use the method
- * clone().
+ * Abstract base class for Prctl path formulas.
*
* @note Differing from the formal definitions of PRCTL a path formula may be the root of a PRCTL formula.
* The result of a modelchecking process on such a formula is a vector representing the satisfaction probabilities for each state of the model.
@@ -35,8 +29,9 @@ template <class T>
class AbstractPathFormula : public virtual storm::property::prctl::AbstractPrctlFormula<T> {
public:
+
/*!
- * empty destructor
+ * The virtual destructor.
*/
virtual ~AbstractPathFormula() {
// Intentionally left empty
@@ -45,10 +40,11 @@ public:
/*!
* Clones the called object.
*
- * Performs a "deep copy", i.e. the subtrees of the new object are clones of the original ones
+ * Performs a "deep copy", i.e. the subtrees of the new object are clones of the original ones.
*
* @note This function is not implemented in this class.
- * @returns a new AND-object that is identical the called object.
+ *
+ * @returns A deep copy of the called object.
*/
virtual std::shared_ptr<AbstractPathFormula<T>> clone() const = 0;
diff --git a/src/formula/prctl/AbstractPrctlFormula.h b/src/formula/prctl/AbstractPrctlFormula.h
index f728110fe..e7b165afa 100644
--- a/src/formula/prctl/AbstractPrctlFormula.h
+++ b/src/formula/prctl/AbstractPrctlFormula.h
@@ -14,6 +14,8 @@ namespace storm {
namespace property {
namespace prctl {
+// Forward declarations.
+
template <class T> class ProbabilisticBoundOperator;
template <class T> class Eventually;
template <class T> class Until;
@@ -27,22 +29,32 @@ namespace property {
namespace prctl {
/*!
- * Interface class for all PRCTL root formulas.
+ * This is the abstract base class for all Prctl formulas.
+ *
+ * @note While formula classes do have copy constructors using a copy constructor
+ * will yield a formula objects whose formula subtree consists of the same objects
+ * as the original formula. The ownership of the formula tree will be shared between
+ * the original and the copy.
*/
template<class T>
class AbstractPrctlFormula : public virtual storm::property::AbstractFormula<T> {
public:
+
+ /*!
+ * The virtual destructor.
+ */
virtual ~AbstractPrctlFormula() {
// Intentionally left empty
}
- /*! Returns whether the formula is a probabilistic bound reachability formula.
- * Returns true iff the formula conforms to the following pattern.
- * Pattern: P[<,<=,>,>=]p ([psi U, E] phi) whith psi, phi propositional logic formulas (consisiting only of And, Or, Not and AP).
- * That is, a probabilistic bound operator as root with a single until or eventually formula directly below it, whose subformulas are propositional
- * (denoting some set of atomic propositions).
+ /*!
+ * Checks whether the formula is a probabilistic bound reachability formula.
+ * Returns true iff the formula conforms to the following pattern.
+ * Pattern: P[<,<=,>,>=]p ([psi U, E] phi) whith psi, phi propositional logic formulas (consisiting only of And, Or, Not and AP).
+ * That is, a probabilistic bound operator as root with a single until or eventually formula directly below it, whose subformulas are propositional
+ * (denoting some set of atomic propositions).
*
- * @return True iff this is a probabilistic bound reachability formula.
+ * @return True iff this is a probabilistic bound reachability formula.
*/
bool isProbEventuallyAP() const {
diff --git a/src/formula/prctl/AbstractRewardPathFormula.h b/src/formula/prctl/AbstractRewardPathFormula.h
index 949ecc422..09d0dcbf2 100644
--- a/src/formula/prctl/AbstractRewardPathFormula.h
+++ b/src/formula/prctl/AbstractRewardPathFormula.h
@@ -14,16 +14,21 @@ namespace storm {
namespace property {
namespace prctl {
-/*! Base class for reward path formulas.
+/*!
+ * Abstract base class for Prctl reward path formulas.
*
- * Reward path formulas are subformulas of reward bound operators.
- * They may not be subformulas of a probabilitic bound operator.
+ * Reward path formulas may not be subformulas of a probabilitic bound operator, as they describe rewards along paths not probabilities.
*
+ * @note Differing from the formal definitions of PRCTL a reward path formula may be the root of a PRCTL formula.
+ * The result of a modelchecking process on such a formula is a vector representing the rewards for each state of the model.
+ *
+ * @see AbstractPrctlFormula
*/
template <class T>
class AbstractRewardPathFormula : public virtual storm::property::prctl::AbstractPrctlFormula<T> {
public:
+
/*!
* Empty virtual destructor.
*/
@@ -37,7 +42,8 @@ public:
* Performs a "deep copy", i.e. the subtrees of the new object are clones of the original ones
*
* @note This function is not implemented in this class.
- * @returns a new AND-object that is identical the called object.
+ *
+ * @returns A deep copy of the called object.
*/
virtual std::shared_ptr<AbstractRewardPathFormula<T>> clone() const = 0;
diff --git a/src/formula/prctl/AbstractStateFormula.h b/src/formula/prctl/AbstractStateFormula.h
index d07c169a8..2da8c093b 100644
--- a/src/formula/prctl/AbstractStateFormula.h
+++ b/src/formula/prctl/AbstractStateFormula.h
@@ -17,20 +17,15 @@ namespace property {
namespace prctl {
/*!
- * @brief
- * Abstract base class for Abstract state formulas.
- *
- * @attention This class is abstract.
- * @note Formula classes do not have copy constructors. The parameters of the constructors are usually the subtrees, so
- * the syntax conflicts with copy constructors for unary operators. To produce an identical object, use the method
- * clone().
+ * Abstract base class for Prctl state formulas.
*/
template <class T>
class AbstractStateFormula : public storm::property::prctl::AbstractPrctlFormula<T> {
public:
+
/*!
- * empty destructor
+ * Empty virtual destructor.
*/
virtual ~AbstractStateFormula() {
// Intentionally left empty
@@ -42,7 +37,8 @@ public:
* Performs a "deep copy", i.e. the subtrees of the new object are clones of the original ones
*
* @note This function is not implemented in this class.
- * @returns a new AND-object that is identical the called object.
+ *
+ * @returns A deep copy of the called object.
*/
virtual std::shared_ptr<AbstractStateFormula<T>> clone() const = 0;
diff --git a/src/formula/prctl/And.h b/src/formula/prctl/And.h
index 81b33ad28..c312f30c5 100644
--- a/src/formula/prctl/And.h
+++ b/src/formula/prctl/And.h
@@ -16,37 +16,45 @@ namespace storm {
namespace property {
namespace prctl {
+// Forward declaration for the interface class.
template <class T> class And;
/*!
- * @brief Interface class for model checkers that support And.
+ * Interface class for model checkers that support And.
*
- * All model checkers that support the formula class And must inherit
- * this pure virtual class.
+ * All model checkers that support the formula class And must inherit
+ * this pure virtual class.
*/
template <class T>
class IAndModelChecker {
public:
+
+ /*!
+ * Empty virtual destructor.
+ */
+ virtual ~IAndModelChecker() {
+ // Intentionally left empty
+ }
+
/*!
- * @brief Evaluates And formula within a model checker.
+ * Evaluates an And formula within a model checker.
*
- * @param obj Formula object with subformulas.
- * @return Result of the formula for every node.
+ * @param obj Formula object with subformulas.
+ * @return The modelchecking result of the formula for every state.
*/
virtual storm::storage::BitVector checkAnd(const And<T>& obj) const = 0;
};
/*!
- * @brief
- * Class for an abstract formula tree with AND node as root.
+ * Class for a Prctl formula tree with an And node as root.
*
- * Has two Abstract state formulas as sub formulas/trees.
+ * It has two state formulas as sub formulas/trees.
*
- * As AND is commutative, the order is \e theoretically not important, but will influence the order in which
+ * As And is commutative, the order is \e theoretically not important, but will influence the order in which
* the model checker works.
*
- * 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)
+ * The object has shared ownership of its subtrees. If this object is deleted and no other object has a shared
+ * ownership of the subtrees they will be deleted as well.
*
* @see AbstractStateFormula
* @see AbstractPrctlFormula
@@ -57,29 +65,25 @@ class And : public AbstractStateFormula<T> {
public:
/*!
- * Empty constructor.
- * Will create an AND-node without subnotes. Will not represent a complete formula!
+ * Creates an And node without subnodes.
+ * The resulting object will not represent a complete formula!
*/
- And() {
+ And() : left(nullptr), right(nullptr) {
// Intentionally left empty.
}
/*!
- * Constructor.
- * Creates an AND note with the parameters as subtrees.
+ * Creates an And node with the parameters as subtrees.
*
- * @param left The left sub formula
- * @param right The right sub formula
+ * @param left The left sub formula.
+ * @param right The right sub formula.
*/
And(std::shared_ptr<AbstractStateFormula<T>> const & left, std::shared_ptr<AbstractStateFormula<T>> const & right) : left(left), right(right) {
// Intentionally left empty.
}
/*!
- * Destructor.
- *
- * The subtrees are deleted with the object
- * (this behavior can be prevented by setting them to NULL before deletion)
+ * Empty virtual destructor.
*/
virtual ~And() {
// Intentionally left empty.
@@ -88,16 +92,16 @@ public:
/*!
* Clones the called object.
*
- * Performs a "deep copy", i.e. the subtrees of the new object are clones of the original ones
+ * Performs a "deep copy", i.e. the subtrees of the new object are clones of the original ones.
*
- * @returns a new AND-object that is identical the called object.
+ * @returns A new And object that is a deep copy of the called object.
*/
virtual std::shared_ptr<AbstractStateFormula<T>> clone() const override {
std::shared_ptr<And<T>> result(new And());
- if (this->leftIsSet()) {
+ if (this->isLeftSet()) {
result->setLeft(left->clone());
}
- if (this->rightIsSet()) {
+ if (this->isRightSet()) {
result->setRight(right->clone());
}
return result;
@@ -117,7 +121,9 @@ public:
}
/*!
- * @returns a string representation of the formula
+ * Returns a textual representation of the formula tree with this node as root.
+ *
+ * @returns A string representing the formula tree.
*/
virtual std::string toString() const override {
std::string result = "(";
@@ -139,55 +145,65 @@ public:
}
/*!
- * Sets the left child node.
+ * Gets the left child node.
*
- * @param newLeft the new left child.
+ * @returns The left child node.
*/
- void setLeft(std::shared_ptr<AbstractStateFormula<T>> const & newLeft) {
- left = newLeft;
+ std::shared_ptr<AbstractStateFormula<T>> const & getLeft() const {
+ return left;
}
/*!
- * Sets the right child node.
+ * Gets the right child node.
*
- * @param newRight the new right child.
+ * @returns The right child node.
*/
- void setRight(std::shared_ptr<AbstractStateFormula<T>> const & newRight) {
- right = newRight;
+ std::shared_ptr<AbstractStateFormula<T>> const & getRight() const {
+ return right;
}
/*!
- * @returns a reference to the left child node
+ * Sets the left child node.
+ *
+ * @param newLeft The new left child.
*/
- std::shared_ptr<AbstractStateFormula<T>> const & getLeft() const {
- return left;
+ void setLeft(std::shared_ptr<AbstractStateFormula<T>> const & newLeft) {
+ left = newLeft;
}
/*!
- * @returns a reference to the right child node
+ * Sets the right child node.
+ *
+ * @param newRight The new right child.
*/
- std::shared_ptr<AbstractStateFormula<T>> const & getRight() const {
- return right;
+ void setRight(std::shared_ptr<AbstractStateFormula<T>> const & newRight) {
+ right = newRight;
}
/*!
+ * Checks if the left child is set, i.e. it does not point to null.
*
- * @return True if the left child is set, i.e. it does not point to nullptr; false otherwise
+ * @return True iff the left child is set.
*/
- bool leftIsSet() const {
+ bool isLeftSet() const {
return left.get() != nullptr;
}
/*!
+ * Checks if the right child is set, i.e. it does not point to null.
*
- * @return True if the right child is set, i.e. it does not point to nullptr; false otherwise
+ * @return True iff the right child is set.
*/
- bool rightIsSet() const {
+ bool isRightSet() const {
return right.get() != nullptr;
}
private:
+
+ // The left child node.
std::shared_ptr<AbstractStateFormula<T>> left;
+
+ // The right child node.
std::shared_ptr<AbstractStateFormula<T>> right;
};
diff --git a/src/formula/prctl/Ap.h b/src/formula/prctl/Ap.h
index 7df3cabd8..15bd442ca 100644
--- a/src/formula/prctl/Ap.h
+++ b/src/formula/prctl/Ap.h
@@ -15,31 +15,39 @@ namespace storm {
namespace property {
namespace prctl {
+// Forward declaration for the interface class.
template <class T> class Ap;
/*!
- * @brief Interface class for model checkers that support Ap.
+ * Interface class for model checkers that support Ap.
*
- * All model checkers that support the formula class Ap must inherit
- * this pure virtual class.
+ * All model checkers that support the formula class Ap must inherit
+ * this pure virtual class.
*/
template <class T>
class IApModelChecker {
public:
+
+ /*!
+ * Empty virtual destructor.
+ */
+ virtual ~IApModelChecker() {
+ // Intentionally left empty
+ }
+
/*!
- * @brief Evaluates Ap formula within a model checker.
+ * Evaluates an Ap formula within a model checker.
*
- * @param obj Formula object with subformulas.
- * @return Result of the formula for every node.
+ * @param obj Formula object with subformulas.
+ * @return The modelchecking result of the formula for every state.
*/
virtual storm::storage::BitVector checkAp(const Ap<T>& obj) const = 0;
};
/*!
- * @brief
- * Class for an abstract formula tree with atomic proposition as root.
+ * Class for a Prctl formula tree with an atomic proposition as root.
*
- * This class represents the leaves in the formula tree.
+ * This class represents leaves in the formula tree.
*
* @see AbstractPrctlFormula
* @see AbstractStateFormula
@@ -50,19 +58,16 @@ class Ap : public AbstractStateFormula<T> {
public:
/*!
- * Constructor
+ * Creates a new atomic proposition leaf, with the given label.
*
- * Creates a new atomic proposition leaf, with the label Ap
- *
- * @param ap The string representing the atomic proposition
+ * @param ap A string representing the atomic proposition.
*/
- Ap(std::string ap) {
- this->ap = ap;
+ Ap(std::string ap) : ap(ap) {
+ // Intentionally left empty.
}
/*!
- * Destructor.
- * At this time, empty...
+ * Empty virtual destructor.
*/
virtual ~Ap() {
// Intentionally left empty
@@ -71,12 +76,12 @@ public:
/*!
* Clones the called object.
*
- * Performs a "deep copy", i.e. the subtrees of the new object are clones of the original ones
+ * Performs a "deep copy", i.e. the subtrees of the new object are clones of the original ones.
*
- * @returns a new AND-object that is identical the called object.
+ * @returns A new Ap object that is a deep copy of the called object.
*/
virtual std::shared_ptr<AbstractStateFormula<T>> clone() const override {
- std::shared_ptr<AbstractStateFormula<T>> result(new Ap(this->getAp()));
+ auto result = std::make_shared<Ap<T>>(this->getAp());
return result;
}
@@ -93,6 +98,15 @@ public:
return modelChecker.template as<IApModelChecker>()->checkAp(*this);
}
+ /*!
+ * A string representing the atomic proposition.
+ *
+ * @returns A string representing the leaf.
+ */
+ virtual std::string toString() const override {
+ return getAp();
+ }
+
/*!
* Returns whether the formula is a propositional logic formula.
* That is, this formula and all its subformulas consist only of And, Or, Not and AP.
@@ -104,21 +118,17 @@ public:
}
/*!
- * @returns the name of the atomic proposition
- */
- const std::string& getAp() const {
- return ap;
- }
-
- /*!
- * @returns a string representation of the leaf.
+ * Gets the name of the atomic proposition.
*
+ * @returns The name of the atomic proposition.
*/
- virtual std::string toString() const override {
- return getAp();
+ std::string const & getAp() const {
+ return ap;
}
private:
+
+ // The atomic proposition referenced by this leaf.
std::string ap;
};
diff --git a/src/formula/prctl/BoundedEventually.h b/src/formula/prctl/BoundedEventually.h
index 16b7df1d8..920a6a073 100644
--- a/src/formula/prctl/BoundedEventually.h
+++ b/src/formula/prctl/BoundedEventually.h
@@ -18,37 +18,47 @@ namespace storm {
namespace property {
namespace prctl{
+// Forward declaration for the interface class.
template <class T> class BoundedEventually;
/*!
- * @brief Interface class for model checkers that support BoundedEventually.
+ * Interface class for model checkers that support BoundedEventually.
*
- * All model checkers that support the formula class BoundedEventually must inherit
- * this pure virtual class.
+ * All model checkers that support the formula class BoundedEventually must inherit
+ * this pure virtual class.
*/
template <class T>
class IBoundedEventuallyModelChecker {
public:
+
+ /*!
+ * Empty virtual destructor.
+ */
+ virtual ~IBoundedEventuallyModelChecker() {
+ // Intentionally left empty
+ }
+
/*!
- * @brief Evaluates BoundedEventually formula within a model checker.
+ * Evaluates a BoundedEventually formula within a model checker.
*
- * @param obj Formula object with subformulas.
- * @return Result of the formula for every node.
+ * @param obj Formula object with subformulas.
+ * @param qualitative A flag indicating whether the formula only needs to be evaluated qualitatively, i.e. if the
+ * results are only compared against the bounds 0 and 1.
+ * @return The modelchecking result of the formula for every state.
*/
virtual std::vector<T> checkBoundedEventually(const BoundedEventually<T>& obj, bool qualitative) const = 0;
};
/*!
- * @brief
- * Class for an abstract (path) formula tree with a BoundedEventually node as root.
+ * Class for a Prctl (path) formula tree with a BoundedEventually node as root.
*
- * Has one Abstract state formulas as sub formula/tree.
+ * Has one state formula as subformula/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)
+ * The object has shared ownership of its subtree. If this object is deleted and no other object has a shared
+ * ownership of the subtree it will be deleted as well.
*
* @see AbstractPathFormula
* @see AbstractPrctlFormula
@@ -57,28 +67,27 @@ template <class T>
class BoundedEventually : public AbstractPathFormula<T> {
public:
+
/*!
- * Empty constructor
+ * Creates a BoundedEventually node without a subnode.
+ * The resulting object will not represent a complete formula!
*/
- BoundedEventually() : child(nullptr), bound(0){
+ BoundedEventually() : child(nullptr), bound(0) {
// Intentionally left empty.
}
/*!
- * Constructor
+ * Creates a BoundedEventually node using the given parameters.
*
- * @param child The child formula subtree
- * @param bound The maximal number of steps
+ * @param child The child formula subtree.
+ * @param bound The maximal number of steps within which the subformula must hold.
*/
- BoundedEventually(std::shared_ptr<AbstractStateFormula<T>> child, uint_fast64_t bound) : child(child), bound(bound){
+ BoundedEventually(std::shared_ptr<AbstractStateFormula<T>> child, uint_fast64_t bound) : child(child), bound(bound) {
// Intentionally left empty.
}
/*!
- * Destructor.
- *
- * Also deletes the subtrees.
- * (this behaviour can be prevented by setting the subtrees to NULL before deletion)
+ * Empty virtual destructor.
*/
virtual ~BoundedEventually() {
// Intentionally left empty.
@@ -87,14 +96,14 @@ public:
/*!
* Clones the called object.
*
- * Performs a "deep copy", i.e. the subtrees of the new object are clones of the original ones
+ * Performs a "deep copy", i.e. the subnodes of the new object are clones of the original ones.
*
- * @returns a new BoundedUntil-object that is identical the called object.
+ * @returns A new BoundedEventually object that is a deep copy of the called object.
*/
virtual std::shared_ptr<AbstractPathFormula<T>> clone() const override {
std::shared_ptr<BoundedEventually<T>> result(new BoundedEventually<T>());
result->setBound(bound);
- if (this->childIsSet()) {
+ if (this->isChildSet()) {
result->setChild(child->clone());
}
return result;
@@ -115,7 +124,9 @@ public:
}
/*!
- * @returns a string representation of the formula
+ * Returns a textual representation of the formula tree with this node as root.
+ *
+ * @returns A string representing the formula tree.
*/
virtual std::string toString() const override {
std::string result = "F<=";
@@ -126,46 +137,56 @@ public:
}
/*!
- * @returns the child node
+ * Gets the child node.
+ *
+ * @returns The child node.
*/
std::shared_ptr<AbstractStateFormula<T>> const & getChild() const {
return child;
}
/*!
- * Sets the subtree
- * @param child the new child node
+ * Sets the subtree.
+ *
+ * @param child The new child.
*/
void setChild(std::shared_ptr<AbstractStateFormula<T>> const & child) {
this->child = child;
}
/*!
+ * Checks if the child is set, i.e. it does not point to null.
*
- * @return True if the child is set, i.e. it does not point to nullptr; false otherwise
+ * @return True iff the child is set.
*/
- bool childIsSet() const {
+ bool isChildSet() const {
return child.get() != nullptr;
}
/*!
- * @returns the maximally allowed number of steps for the bounded until operator
+ * Gets the maximally allowed number of steps for the bounded eventually operator.
+ *
+ * @returns The bound.
*/
uint_fast64_t getBound() const {
return bound;
}
/*!
- * Sets the maximally allowed number of steps for the bounded until operator
+ * Sets the maximally allowed number of steps for the bounded eventually operator.
*
- * @param bound the new bound.
+ * @param bound The new bound.
*/
void setBound(uint_fast64_t bound) {
this->bound = bound;
}
private:
+
+ // The child node.
std::shared_ptr<AbstractStateFormula<T>> child;
+
+ // The maximal number of steps within which the subformula must hold.
uint_fast64_t bound;
};
diff --git a/src/formula/prctl/BoundedNaryUntil.h b/src/formula/prctl/BoundedNaryUntil.h
index 1c9863ac7..c6e4092e9 100644
--- a/src/formula/prctl/BoundedNaryUntil.h
+++ b/src/formula/prctl/BoundedNaryUntil.h
@@ -21,33 +21,42 @@ namespace storm {
namespace property {
namespace prctl {
-
+// Forward declaration for the interface class.
template <class T> class BoundedNaryUntil;
/*!
- * @brief Interface class for model checkers that support BoundedNaryUntil.
+ * Interface class for model checkers that support BoundedNaryUntil.
*
- * All model checkers that support the formula class BoundedNaryUntil must inherit
- * this pure virtual class.
+ * All model checkers that support the formula class BoundedNaryUntil must inherit
+ * this pure virtual class.
*/
template <class T>
class IBoundedNaryUntilModelChecker {
public:
+
+ /*!
+ * Empty virtual destructor.
+ */
+ virtual ~IBoundedNaryUntilModelChecker() {
+ // Intentionally left empty
+ }
+
/*!
- * @brief Evaluates BoundedNaryUntil formula within a model checker.
+ * Evaluates BoundedNaryUntil formula within a model checker.
*
- * @param obj Formula object with subformulas.
- * @return Result of the formula for every node.
+ * @param obj Formula object with subformulas.
+ * @param qualitative A flag indicating whether the formula only needs to be evaluated qualitatively, i.e. if the
+ * results are only compared against the bounds 0 and 1.
+ * @return Result of the formula for every state.
*/
virtual std::vector<T> checkBoundedNaryUntil(const BoundedNaryUntil<T>& obj, bool qualitative) const = 0;
};
/*!
- * @brief
- * Class for an abstract (path) formula tree with a BoundedNaryUntil node as root.
+ * Class for a Prctl (path) formula tree with a BoundedNaryUntil node as root.
*
- * Has at least two Abstract state formulas as sub formulas and an interval
- * associated with all but the first sub formula. We'll call the first one
+ * Has at least two state formulas as sub formulas and an interval
+ * associated with all but the first sub formula. We will call the first one
* \e left and all other one \e right.
*
* @par Semantics
@@ -55,8 +64,8 @@ class IBoundedNaryUntilModelChecker {
* formulas holds after a number of steps contained in the interval
* associated with this formula.
*
- * 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)
+ * The object has shared ownership of its subtrees. If this object is deleted and no other object has a shared
+ * ownership of the subtrees they will be deleted as well.
*
* @see AbstractPathFormula
* @see AbstractPrctlFormula
@@ -67,27 +76,25 @@ class BoundedNaryUntil : public AbstractPathFormula<T> {
public:
/*!
- * Empty constructor
+ * Creates a BoundedNaryUntil node without subnodes.
+ * The resulting object will not represent a complete formula!
*/
BoundedNaryUntil() : left(nullptr), right() {
// Intentionally left empty.
}
/*!
- * Constructor
+ * Creates a BoundedNaryUntil node with the parameters as subtrees.
*
- * @param left The left formula subtree
- * @param right The left formula subtree
+ * @param left The left formula subtree.
+ * @param right The right formula subtrees with their associated intervals.
*/
BoundedNaryUntil(std::shared_ptr<AbstractStateFormula<T>> const & left, std::vector<std::tuple<std::shared_ptr<AbstractStateFormula<T>>,T,T>> const & right) : left(left), right(right) {
// Intentionally left empty.
}
/*!
- * Destructor.
- *
- * Also deletes the subtrees.
- * (this behaviour can be prevented by setting the subtrees to NULL before deletion)
+ * Empty virtual destructor.
*/
virtual ~BoundedNaryUntil() {
// Intentionally left empty.
@@ -96,16 +103,16 @@ public:
/*!
* Clones the called object.
*
- * Performs a "deep copy", i.e. the subtrees of the new object are clones of the original ones
+ * Performs a "deep copy", i.e. the subtrees of the new object are clones of the original ones.
*
- * @returns a new BoundedNaryUntil-object that is identical the called object.
+ * @returns A new BoundedNaryUntil object that is a deep copy of the called object.
*/
virtual std::shared_ptr<AbstractPathFormula<T>> clone() const override {
std::shared_ptr<BoundedNaryUntil<T>> result(new BoundedNaryUntil<T>());
- if (this->leftIsSet()) {
+ if (this->isLeftSet()) {
result->setLeft(left->clone());
}
- if (this->rightIsSet()) {
+ if (this->isRightSet()) {
std::vector<std::tuple<std::shared_ptr<AbstractStateFormula<T>>,T,T>> newright;
for (auto it = right->begin(); it != right->end(); ++it) {
newright.push_back(std::tuple<std::shared_ptr<AbstractStateFormula<T>>,T,T>(std::get<0>(*it)->clone(), std::get<1>(*it), std::get<2>(*it)));
@@ -130,7 +137,9 @@ public:
}
/*!
- * @returns a string representation of the formula
+ * Returns a textual representation of the formula tree with this node as root.
+ *
+ * @returns A string representing the formula tree.
*/
virtual std::string toString() const override {
std::stringstream result;
@@ -143,60 +152,76 @@ public:
}
/*!
- * Sets the left child node.
+ * Gets the left child node.
*
- * @param newLeft the new left child.
+ * @returns The left child node.
*/
- void setLeft(std::shared_ptr<AbstractStateFormula<T>> const & newLeft) {
- left = newLeft;
+ std::shared_ptr<AbstractStateFormula<T>> const & getLeft() const {
+ return left;
}
- void setRight(std::vector<std::tuple<std::shared_ptr<AbstractStateFormula<T>>,T,T>> const & newRight) {
- right = newRight;
+ /*!
+ * Gets the right child nodes and their associated intervals.
+ *
+ * @returns A vector containing the right children as well as the associated intervals.
+ */
+ std::vector<std::tuple<std::shared_ptr<AbstractStateFormula<T>>,T,T>> const & getRight() const {
+ return right;
}
/*!
+ * Sets the left child node.
*
- * @return True if the left child is set, i.e. it does not point to nullptr; false otherwise
+ * @param newLeft The new left child.
*/
- bool leftIsSet() const {
- return left != nullptr;
+ void setLeft(std::shared_ptr<AbstractStateFormula<T>> const & newLeft) {
+ left = newLeft;
}
/*!
+ * Sets the right child nodes.
*
- * @return True if the right child is set, i.e. it is not empty; false otherwise
+ * @param newRight A vector containing the new right children as well as the associated intervals.
*/
- bool rightIsSet() const {
- return !(right.empty());
+ void setRight(std::vector<std::tuple<std::shared_ptr<AbstractStateFormula<T>>,T,T>> const & newRight) {
+ right = newRight;
}
/*!
- * Sets the right child node.
+ * Adds a new rightmost child node.
*
- * @param newRight the new right child.
+ * @param newRight The new child.
+ * @param upperBound The upper bound of the associated interval.
+ * @param lowerBound The lower bound of the associated interval.
*/
void addRight(std::shared_ptr<AbstractStateFormula<T>> const & newRight, T upperBound, T lowerBound) {
right.push_back(std::tuple<std::shared_ptr<AbstractStateFormula<T>>,T,T>(newRight, upperBound, lowerBound));
}
/*!
- * @returns a pointer to the left child node
+ * Checks if the left child is set, i.e. it does not point to null.
+ *
+ * @return True iff the left child is set.
*/
- std::shared_ptr<AbstractStateFormula<T>> const & getLeft() const {
- return left;
+ bool isLeftSet() const {
+ return left != nullptr;
}
/*!
- * @returns a pointer to the right child nodes.
+ * Checks if the right child is set, i.e. it contains at least one entry.
+ *
+ * @return True iff the right child is set.
*/
- std::vector<std::tuple<std::shared_ptr<AbstractStateFormula<T>>,T,T>> const & getRight() const {
- return right;
+ bool isRightSet() const {
+ return !(right.empty());
}
-
private:
+
+ // The left formula subtree.
std::shared_ptr<AbstractStateFormula<T>> left;
+
+ // The right formula subtrees with their associated intervals.
std::vector<std::tuple<std::shared_ptr<AbstractStateFormula<T>>,T,T>> right;
};
diff --git a/src/formula/prctl/BoundedUntil.h b/src/formula/prctl/BoundedUntil.h
index 92d119583..ec0b59f51 100644
--- a/src/formula/prctl/BoundedUntil.h
+++ b/src/formula/prctl/BoundedUntil.h
@@ -18,38 +18,48 @@ namespace storm {
namespace property {
namespace prctl {
+// Forward declaration for the interface class.
template <class T> class BoundedUntil;
/*!
- * @brief Interface class for model checkers that support BoundedUntil.
+ * Interface class for model checkers that support BoundedUntil.
*
- * All model checkers that support the formula class BoundedUntil must inherit
- * this pure virtual class.
+ * All model checkers that support the formula class BoundedUntil must inherit
+ * this pure virtual class.
*/
template <class T>
class IBoundedUntilModelChecker {
public:
+
/*!
- * @brief Evaluates BoundedUntil formula within a model checker.
+ * Empty virtual destructor.
+ */
+ virtual ~IBoundedUntilModelChecker() {
+ // Intentionally left empty
+ }
+
+ /*!
+ * Evaluates a BoundedUntil formula within a model checker.
*
- * @param obj Formula object with subformulas.
- * @return Result of the formula for every node.
+ * @param obj Formula object with subformulas.
+ * @param qualitative A flag indicating whether the formula only needs to be evaluated qualitatively, i.e. if the
+ * results are only compared against the bounds 0 and 1.
+ * @return The modelchecking result of the formula for every state.
*/
virtual std::vector<T> checkBoundedUntil(const BoundedUntil<T>& obj, bool qualitative) const = 0;
};
/*!
- * @brief
- * Class for an abstract (path) formula tree with a BoundedUntil node as root.
+ * Class for a Prctl (path) formula tree with a BoundedUntil node as root.
*
- * Has two Abstract state formulas as sub formulas/trees.
+ * Has two Prctl state formulas as sub formulas/trees.
*
* @par Semantics
* The formula holds iff in at most \e bound steps, formula \e right (the right subtree) holds, and before,
* \e left 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)
+ * The object has shared ownership of its subtrees. If this object is deleted and no other object has a shared
+ * ownership of the subtrees they will be deleted as well.
*
* @see AbstractPathFormula
* @see AbstractPrctlFormula
@@ -60,26 +70,26 @@ class BoundedUntil : public AbstractPathFormula<T> {
public:
/*!
- * Empty constructor
+ * Creates a BoundedUntil node without subnodes.
+ * The resulting object will not represent a complete formula!
*/
- BoundedUntil() : left(nullptr), right(nullptr), bound(0){
+ BoundedUntil() : left(nullptr), right(nullptr), bound(0) {
// Intentionally left empty.
}
/*!
- * Constructor
+ * Creates a BoundedUntil node using the given parameters.
*
- * @param left The left formula subtree
- * @param right The left formula subtree
- * @param bound The maximal number of steps
+ * @param left The left formula subtree.
+ * @param right The right formula subtree.
+ * @param bound The maximal number of steps within which the right subformula must hold.
*/
BoundedUntil(std::shared_ptr<AbstractStateFormula<T>> const & left, std::shared_ptr<AbstractStateFormula<T>> const & right, uint_fast64_t bound) : left(left), right(right), bound(bound) {
// Intentionally left empty.
}
+
/*!
- * Destructor.
- *
- * Deletes the subtrees iff this object is the only owner of them.
+ * Empty virtual destructor.
*/
virtual ~BoundedUntil() {
// Intentionally left empty.
@@ -88,17 +98,17 @@ public:
/*!
* Clones the called object.
*
- * Performs a "deep copy", i.e. the subtrees of the new object are clones of the original ones
+ * Performs a "deep copy", i.e. the subnodes of the new object are clones of the original ones.
*
- * @returns a new BoundedUntil-object that is identical the called object.
+ * @returns A new BoundedUntil object that is a deep copy of the called object.
*/
virtual std::shared_ptr<AbstractPathFormula<T>> clone() const override {
std::shared_ptr<BoundedUntil<T>> result(new BoundedUntil<T>());
result->setBound(bound);
- if (this->leftIsSet()) {
+ if (this->isLeftSet()) {
result->setLeft(left->clone());
}
- if (this->rightIsSet()) {
+ if (this->isRightSet()) {
result->setRight(right->clone());
}
return result;
@@ -119,7 +129,9 @@ public:
}
/*!
- * @returns a string representation of the formula
+ * Returns a textual representation of the formula tree with this node as root.
+ *
+ * @returns A string representing the formula tree.
*/
virtual std::string toString() const override {
std::string result = left->toString();
@@ -131,72 +143,86 @@ public:
}
/*!
- * Sets the left child node.
+ * Gets the left child node.
*
- * @param newLeft the new left child.
+ * @returns The left child node.
*/
- void setLeft(std::shared_ptr<AbstractStateFormula<T>> const & newLeft) {
- left = newLeft;
+ std::shared_ptr<AbstractStateFormula<T>> const & getLeft() const {
+ return left;
}
/*!
- * Sets the right child node.
+ * Gets the right child node.
*
- * @param newRight the new right child.
+ * @returns The right child node.
*/
- void setRight(std::shared_ptr<AbstractStateFormula<T>> const & newRight) {
- right = newRight;
+ std::shared_ptr<AbstractStateFormula<T>> const & getRight() const {
+ return right;
}
/*!
- * @returns a pointer to the left child node
+ * Sets the left child node.
+ *
+ * @param newLeft The new left child.
*/
- std::shared_ptr<AbstractStateFormula<T>> const & getLeft() const {
- return left;
+ void setLeft(std::shared_ptr<AbstractStateFormula<T>> const & newLeft) {
+ left = newLeft;
}
/*!
- * @returns a pointer to the right child node
+ * Sets the right child node.
+ *
+ * @param newRight The new right child.
*/
- std::shared_ptr<AbstractStateFormula<T>> const & getRight() const {
- return right;
+ void setRight(std::shared_ptr<AbstractStateFormula<T>> const & newRight) {
+ right = newRight;
}
/*!
+ * Checks if the left child is set, i.e. it does not point to null.
*
- * @return True if the left child is set, i.e. it does not point to nullptr; false otherwise
+ * @return True iff the left child is set.
*/
- bool leftIsSet() const {
+ bool isLeftSet() const {
return left.get() != nullptr;
}
/*!
+ * Checks if the right child is set, i.e. it does not point to null.
*
- * @return True if the right child is set, i.e. it does not point to nullptr; false otherwise
+ * @return True iff the right child is set.
*/
- bool rightIsSet() const {
+ bool isRightSet() const {
return right.get() != nullptr;
}
/*!
- * @returns the maximally allowed number of steps for the bounded until operator
+ * Gets the maximally allowed number of steps for the bounded until operator.
+ *
+ * @returns The bound.
*/
uint_fast64_t getBound() const {
return bound;
}
/*!
- * Sets the maximally allowed number of steps for the bounded until operator
+ * Sets the maximally allowed number of steps for the bounded until operator.
*
- * @param bound the new bound.
+ * @param bound The new bound.
*/
void setBound(uint_fast64_t bound) {
this->bound = bound;
}
private:
+
+ // The left child node.
std::shared_ptr<AbstractStateFormula<T>> left;
+
+ // The right child node.
std::shared_ptr<AbstractStateFormula<T>> right;
+
+ // The maximal number of steps within which the subformulas must hold.
uint_fast64_t bound;
};
diff --git a/src/formula/prctl/CumulativeReward.h b/src/formula/prctl/CumulativeReward.h
index 4a94c021b..fd51db72c 100644
--- a/src/formula/prctl/CumulativeReward.h
+++ b/src/formula/prctl/CumulativeReward.h
@@ -15,32 +15,44 @@ namespace storm {
namespace property {
namespace prctl {
+// Forward declaration for the interface class.
template <class T> class CumulativeReward;
/*!
- * @brief Interface class for model checkers that support CumulativeReward.
+ * Interface class for model checkers that support CumulativeReward.
*
- * All model checkers that support the formula class CumulativeReward must inherit
- * this pure virtual class.
+ * All model checkers that support the formula class CumulativeReward must inherit
+ * this pure virtual class.
*/
template <class T>
class ICumulativeRewardModelChecker {
public:
+
+ /*!
+ * Empty virtual destructor.
+ */
+ virtual ~ICumulativeRewardModelChecker() {
+ // Intentionally left empty
+ }
+
/*!
- * @brief Evaluates CumulativeReward formula within a model checker.
+ * Evaluates CumulativeReward formula within a model checker.
*
- * @param obj Formula object with subformulas.
- * @return Result of the formula for every node.
+ * @param obj Formula object with subformulas.
+ * @param qualitative A flag indicating whether the formula only needs to be evaluated qualitatively, i.e. if the
+ * results are only compared against the bounds 0 and 1.
+ * @return Result of the formula for every node.
*/
virtual std::vector<T> checkCumulativeReward(const CumulativeReward<T>& obj, bool qualitative) const = 0;
};
/*!
- * @brief
- * Class for an abstract (path) formula tree with a Cumulative Reward node as root.
+ * Class for a Prctl (reward path) formula tree with a Cumulative Reward node as root.
*
- * 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)
+ * Given a path of finite length.
+ * The sum of all rewards received upon entering each state of the path is the cumulative reward of the path.
+ * The cumulative reward for a state s at time \e bound is the expected cumulative reward of a path of length \e bound starting in s.
+ * In the continuous case all paths that need at most time \e bound are considered.
*
* @see AbstractPathFormula
* @see AbstractPrctlFormula
@@ -49,19 +61,15 @@ template <class T>
class CumulativeReward : public AbstractRewardPathFormula<T> {
public:
- /*!
- * Empty constructor
- */
- CumulativeReward() : bound(0){
- // Intentionally left empty.
- }
/*!
- * Constructor
+ * Creates a CumulativeReward node with the given bound.
+ *
+ * If no bound is given it defaults to 0, referencing the state reward received upon entering the state s itself.
*
- * @param bound The time bound of the reward formula
+ * @param bound The time instance of the reward formula.
*/
- CumulativeReward(T bound) : bound(bound){
+ CumulativeReward(T bound = 0) : bound(bound){
// Intentionally left empty.
}
@@ -75,9 +83,9 @@ public:
/*!
* Clones the called object.
*
- * Performs a "deep copy", i.e. the subtrees of the new object are clones of the original ones
+ * Performs a "deep copy", i.e. the subnodes of the new object are clones of the original ones.
*
- * @returns a new CumulativeReward-object that is identical the called object.
+ * @returns A new CumulativeReward object that is a deep copy of the called object.
*/
virtual std::shared_ptr<AbstractRewardPathFormula<T>> clone() const override {
std::shared_ptr<CumulativeReward<T>> result(new CumulativeReward(this->getBound()));
@@ -99,7 +107,9 @@ public:
}
/*!
- * @returns a string representation of the formula
+ * Returns a textual representation of the formula tree with this node as root.
+ *
+ * @returns A string representing the formula tree.
*/
virtual std::string toString() const override {
std::string result = "C <= ";
@@ -108,22 +118,26 @@ public:
}
/*!
- * @returns the time instance for the instantaneous reward operator
+ * Gets the time bound for the paths considered.
+ *
+ * @returns The time bound for the paths considered.
*/
T getBound() const {
return bound;
}
/*!
- * Sets the the time instance for the instantaneous reward operator
+ * Sets the time bound for the paths considered.
*
- * @param bound the new bound.
+ * @param bound The new bound.
*/
void setBound(T bound) {
this->bound = bound;
}
private:
+
+ // The time bound for the paths considered.
T bound;
};
diff --git a/src/formula/prctl/Eventually.h b/src/formula/prctl/Eventually.h
index 77dcb3c73..6d22e1dd4 100644
--- a/src/formula/prctl/Eventually.h
+++ b/src/formula/prctl/Eventually.h
@@ -1,5 +1,5 @@
/*
- * Next.h
+ * Eventually.h
*
* Created on: 26.12.2012
* Author: Christian Dehnert
@@ -16,37 +16,47 @@ namespace storm {
namespace property {
namespace prctl {
+// Forward declaration for the interface class.
template <class T> class Eventually;
/*!
- * @brief Interface class for model checkers that support Eventually.
+ * Interface class for model checkers that support Eventually.
*
- * All model checkers that support the formula class Eventually must inherit
- * this pure virtual class.
+ * All model checkers that support the formula class Eventually must inherit
+ * this pure virtual class.
*/
template <class T>
class IEventuallyModelChecker {
public:
+
/*!
- * @brief Evaluates Eventually formula within a model checker.
- *
- * @param obj Formula object with subformulas.
- * @return Result of the formula for every node.
- */
+ * Empty virtual destructor.
+ */
+ virtual ~IEventuallyModelChecker() {
+ // Intentionally left empty.
+ }
+
+ /*!
+ * Evaluates an Eventually formula within a model checker.
+ *
+ * @param obj Formula object with subformulas.
+ * @param qualitative A flag indicating whether the formula only needs to be evaluated qualitatively, i.e. if the
+ * results are only compared against the bounds 0 and 1.
+ * @return The modelchecking result of the formula for every state.
+ */
virtual std::vector<T> checkEventually(const Eventually<T>& obj, bool qualitative) const = 0;
};
/*!
- * @brief
- * Class for an abstract (path) formula tree with an Eventually node as root.
+ * Class for a Prctl (path) formula tree with an Eventually node as root.
*
- * Has one Abstract state formula as sub formula/tree.
+ * Has one state formula as sub formula/tree.
*
* @par Semantics
- * The formula holds iff eventually \e child holds.
+ * The formula holds iff eventually formula \e child holds.
*
- * The subtree is seen as part of the object and deleted with the object
- * (this behavior can be prevented by setting them to nullptr before deletion)
+ * The object has shared ownership of its subtree. If this object is deleted and no other object has a shared
+ * ownership of the subtree it will be deleted as well.
*
* @see AbstractPathFormula
* @see AbstractPrctlFormula
@@ -57,25 +67,24 @@ class Eventually : public AbstractPathFormula<T> {
public:
/*!
- * Empty constructor
+ * Creates an Eventually node without a subnode.
+ * The resulting object will not represent a complete formula!
*/
Eventually() : child(nullptr) {
// Intentionally left empty.
}
/*!
- * Constructor
+ * Creates an Eventually node using the given parameter.
*
- * @param child The child node
+ * @param child The child formula subtree.
*/
Eventually(std::shared_ptr<AbstractStateFormula<T>> const & child) : child(child){
// Intentionally left empty.
}
/*!
- * Constructor.
- *
- * Deletes the subtree iff this object is the last remaining owner of the subtree.
+ * Empty virtual destructor.
*/
virtual ~Eventually() {
// Intentionally left empty.
@@ -84,13 +93,13 @@ public:
/*!
* Clones the called object.
*
- * Performs a "deep copy", i.e. the subtrees of the new object are clones of the original ones
+ * Performs a "deep copy", i.e. the subnodes of the new object are clones of the original ones.
*
- * @returns a new Eventually-object that is identical the called object.
+ * @returns A new Eventually object that is a deep copy of the called object.
*/
virtual std::shared_ptr<AbstractPathFormula<T>> clone() const override {
std::shared_ptr<Eventually<T>> result(new Eventually<T>());
- if (this->childIsSet()) {
+ if (this->isChildSet()) {
result->setChild(child->clone());
}
return result;
@@ -110,7 +119,9 @@ public:
}
/*!
- * @returns a string representation of the formula
+ * Returns a textual representation of the formula tree with this node as root.
+ *
+ * @returns A string representing the formula tree.
*/
virtual std::string toString() const override {
std::string result = "F ";
@@ -119,29 +130,35 @@ public:
}
/*!
- * @returns the child node
+ * Gets the child node.
+ *
+ * @returns The child node.
*/
std::shared_ptr<AbstractStateFormula<T>> const & getChild() const {
return child;
}
/*!
- * Sets the subtree
- * @param child the new child node
+ * Sets the subtree.
+ *
+ * @param child The new child.
*/
void setChild(std::shared_ptr<AbstractStateFormula<T>> const & child) {
this->child = child;
}
/*!
+ * Checks if the child is set, i.e. it does not point to null.
*
- * @return True if the child node is set, i.e. it does not point to nullptr; false otherwise
+ * @return True iff the child is set.
*/
- bool childIsSet() const {
+ bool isChildSet() const {
return child.get() != nullptr;
}
private:
+
+ // The child node.
std::shared_ptr<AbstractStateFormula<T>> child;
};
diff --git a/src/formula/prctl/Globally.h b/src/formula/prctl/Globally.h
index 8f0b9c910..12f29f19d 100644
--- a/src/formula/prctl/Globally.h
+++ b/src/formula/prctl/Globally.h
@@ -1,5 +1,5 @@
/*
- * Next.h
+ * Globally.h
*
* Created on: 26.12.2012
* Author: Christian Dehnert
@@ -16,37 +16,47 @@ namespace storm {
namespace property {
namespace prctl {
+// Forward declaration for the interface class.
template <class T> class Globally;
/*!
- * @brief Interface class for model checkers that support Globally.
+ * Interface class for model checkers that support Globally.
*
- * All model checkers that support the formula class Globally must inherit
- * this pure virtual class.
+ * All model checkers that support the formula class Globally must inherit
+ * this pure virtual class.
*/
template <class T>
class IGloballyModelChecker {
public:
+
/*!
- * @brief Evaluates Globally formula within a model checker.
- *
- * @param obj Formula object with subformulas.
- * @return Result of the formula for every node.
- */
+ * Empty virtual destructor.
+ */
+ virtual ~IGloballyModelChecker() {
+ // Intentionally left empty
+ }
+
+ /*!
+ * Evaluates a Globally formula within a model checker.
+ *
+ * @param obj Formula object with subformulas.
+ * @param qualitative A flag indicating whether the formula only needs to be evaluated qualitatively, i.e. if the
+ * results are only compared against the bounds 0 and 1.
+ * @return The modelchecking result of the formula for every state.
+ */
virtual std::vector<T> checkGlobally(const Globally<T>& obj, bool qualitative) const = 0;
};
/*!
- * @brief
- * Class for an abstract (path) formula tree with a Globally node as root.
+ * Class for an Prctl (path) formula tree with a Globally node as root.
*
- * Has one Abstract state formula as sub formula/tree.
+ * Has one state formula as sub formula/tree.
*
* @par Semantics
- * The formula holds iff globally \e child holds.
+ * The formula holds iff globally formula \e child holds.
*
- * The subtree is seen as part of the object and deleted with the object
- * (this behavior can be prevented by setting them to nullptr before deletion)
+ * The object has shared ownership of its subtree. If this object is deleted and no other object has a shared
+ * ownership of the subtree it will be deleted as well.
*
* @see AbstractPathFormula
* @see AbstractPrctlFormula
@@ -57,25 +67,24 @@ class Globally : public AbstractPathFormula<T> {
public:
/*!
- * Empty constructor
+ * Creates a Globally node without a subnode.
+ * The resulting object will not represent a complete formula!
*/
Globally() : child(nullptr){
// Intentionally left empty.
}
/*!
- * Constructor
+ * Creates a Globally node using the given parameter.
*
- * @param child The child node
+ * @param child The child formula subtree.
*/
Globally(std::shared_ptr<AbstractStateFormula<T>> const & child) : child(child){
// Intentionally left empty.
}
/*!
- * Destructor.
- *
- * Deletes the subtree iff this object is the last remaining owner of the subtree.
+ * Empty virtual destructor.
*/
virtual ~Globally() {
// Intentionally left empty.
@@ -84,13 +93,13 @@ public:
/*!
* Clones the called object.
*
- * Performs a "deep copy", i.e. the subtrees of the new object are clones of the original ones
+ * Performs a "deep copy", i.e. the subnodes of the new object are clones of the original ones.
*
- * @returns a new Globally-object that is identical the called object.
+ * @returns A new Globally object that is a deep copy of the called object.
*/
virtual std::shared_ptr<AbstractPathFormula<T>> clone() const override {
std::shared_ptr<Globally<T>> result(new Globally<T>());
- if (this->childIsSet()) {
+ if (this->isChildSet()) {
result->setChild(child->clone());
}
return result;
@@ -110,7 +119,9 @@ public:
}
/*!
- * @returns a string representation of the formula
+ * Returns a textual representation of the formula tree with this node as root.
+ *
+ * @returns A string representing the formula tree.
*/
virtual std::string toString() const override {
std::string result = "G ";
@@ -119,29 +130,35 @@ public:
}
/*!
- * @returns the child node
+ * Gets the child node.
+ *
+ * @returns The child node.
*/
std::shared_ptr<AbstractStateFormula<T>> const & getChild() const {
return child;
}
/*!
- * Sets the subtree
- * @param child the new child node
+ * Sets the subtree.
+ *
+ * @param child The new child.
*/
void setChild(std::shared_ptr<AbstractStateFormula<T>> const & child) {
this->child = child;
}
/*!
+ * Checks if the child is set, i.e. it does not point to null.
*
- * @return True if the child node is set, i.e. it does not point to nullptr; false otherwise
+ * @return True iff the child is set.
*/
- bool childIsSet() const {
+ bool isChildSet() const {
return child.get() != nullptr;
}
private:
+
+ // The child node.
std::shared_ptr<AbstractStateFormula<T>> child;
};
diff --git a/src/formula/prctl/InstantaneousReward.h b/src/formula/prctl/InstantaneousReward.h
index 18cf7eeae..c8f61b120 100644
--- a/src/formula/prctl/InstantaneousReward.h
+++ b/src/formula/prctl/InstantaneousReward.h
@@ -16,32 +16,44 @@ namespace storm {
namespace property {
namespace prctl {
+// Forward declaration for the interface class.
template <class T> class InstantaneousReward;
/*!
- * @brief Interface class for model checkers that support InstantaneousReward.
+ * Interface class for model checkers that support InstantaneousReward.
*
- * All model checkers that support the formula class InstantaneousReward must inherit
- * this pure virtual class.
+ * All model checkers that support the formula class InstantaneousReward must inherit
+ * this pure virtual class.
*/
template <class T>
class IInstantaneousRewardModelChecker {
public:
+
+ /*!
+ * Empty virtual destructor.
+ */
+ virtual ~IInstantaneousRewardModelChecker() {
+ // Intentionally left empty
+ }
+
/*!
- * @brief Evaluates InstantaneousReward formula within a model checker.
+ * Evaluates an InstantaneousReward formula within a model checker.
*
- * @param obj Formula object with subformulas.
- * @return Result of the formula for every node.
+ * @param obj Formula object with subformulas.
+ * @param qualitative A flag indicating whether the formula only needs to be evaluated qualitatively, i.e. if the
+ * results are only compared against the bounds 0 and 1.
+ * @return The modelchecking result of the formula for every state.
*/
virtual std::vector<T> checkInstantaneousReward(const InstantaneousReward<T>& obj, bool qualitative) const = 0;
};
/*!
- * @brief
- * Class for an abstract (path) formula tree with a Instantaneous Reward node as root.
+ * Class for an Instantaneous Reward formula.
+ * This class represents a possible leaf in a reward formula tree.
*
- * 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)
+ * Given a path of finite length.
+ * The reward received upon entering the last state of the path is the instantaneous reward of the path.
+ * The instantaneous reward for a state s at time \e bound is the expected instantaneous reward of a path of length \e bound starting in s.
*
* @see AbstractPathFormula
* @see AbstractPrctlFormula
@@ -52,23 +64,18 @@ class InstantaneousReward : public AbstractRewardPathFormula<T> {
public:
/*!
- * Empty constructor
- */
- InstantaneousReward() : bound(0) {
- // Intentionally left empty.
- }
-
- /*!
- * Constructor
+ * Creates an InstantaneousReward node with the given bound.
+ *
+ * If no bound is given it defaults to 0, referencing the state reward received upon entering the state s itself.
*
- * @param bound The time instance of the reward formula
+ * @param bound The time instance of the reward formula.
*/
- InstantaneousReward(uint_fast64_t bound) : bound(bound) {
+ InstantaneousReward(uint_fast64_t bound = 0) : bound(bound) {
// Intentionally left empty.
}
/*!
- * Empty destructor.
+ * Empty virtual destructor.
*/
virtual ~InstantaneousReward() {
// Intentionally left empty.
@@ -77,9 +84,9 @@ public:
/*!
* Clones the called object.
*
- * Performs a "deep copy", i.e. the subtrees of the new object are clones of the original ones
+ * Performs a "deep copy", i.e. the subnodes of the new object are clones of the original ones.
*
- * @returns a new InstantaneousReward-object that is identical the called object.
+ * @returns A new InstantaneousReward object that is a deep copy of the called object.
*/
virtual std::shared_ptr<AbstractRewardPathFormula<T>> clone() const override {
std::shared_ptr<InstantaneousReward<T>> result(new InstantaneousReward(bound));
@@ -101,7 +108,9 @@ public:
}
/*!
- * @returns a string representation of the formula
+ * Returns a textual representation of the formula tree with this node as root.
+ *
+ * @returns A string representing the formula tree.
*/
virtual std::string toString() const override {
std::string result = "I=";
@@ -110,22 +119,26 @@ public:
}
/*!
- * @returns the time instance for the instantaneous reward operator
+ * Gets the time instance for the instantaneous reward operator.
+ *
+ * @returns The time instance for the instantaneous reward operator.
*/
uint_fast64_t getBound() const {
return bound;
}
/*!
- * Sets the the time instance for the instantaneous reward operator
+ * Sets the the time instance for the instantaneous reward operator.
*
- * @param bound the new bound.
+ * @param bound The new time instance.
*/
void setBound(uint_fast64_t bound) {
this->bound = bound;
}
private:
+
+ // The time instance of the reward formula.
uint_fast64_t bound;
};
diff --git a/src/formula/prctl/Next.h b/src/formula/prctl/Next.h
index 052adf9ca..a83ff1690 100644
--- a/src/formula/prctl/Next.h
+++ b/src/formula/prctl/Next.h
@@ -15,37 +15,47 @@ namespace storm {
namespace property {
namespace prctl {
+// Forward declaration for the interface class.
template <class T> class Next;
/*!
- * @brief Interface class for model checkers that support Next.
+ * Interface class for model checkers that support Next.
*
- * All model checkers that support the formula class Next must inherit
- * this pure virtual class.
+ * All model checkers that support the formula class Next must inherit
+ * this pure virtual class.
*/
template <class T>
class INextModelChecker {
public:
+
/*!
- * @brief Evaluates Next formula within a model checker.
+ * Empty virtual destructor.
+ */
+ virtual ~INextModelChecker() {
+ // Intentionally left empty
+ }
+
+ /*!
+ * Evaluates Next formula within a model checker.
*
- * @param obj Formula object with subformulas.
- * @return Result of the formula for every node.
+ * @param obj Formula object with subformulas.
+ * @param qualitative A flag indicating whether the formula only needs to be evaluated qualitatively, i.e. if the
+ * results are only compared against the bounds 0 and 1.
+ * @return Result of the formula for every node.
*/
virtual std::vector<T> checkNext(const Next<T>& obj, bool qualitative) const = 0;
};
/*!
- * @brief
- * Class for an abstract (path) formula tree with a Next node as root.
+ * Class for a Prctl (path) formula tree with a Next node as root.
*
- * Has two Abstract state formulas as sub formulas/trees.
+ * Has two Prctl state formulas as sub formulas/trees.
*
* @par Semantics
- * The formula holds iff in the next step, \e child holds
+ * The formula holds iff in the next step, formula \e child holds
*
- * The subtree is seen as part of the object and deleted with the object
- * (this behavior can be prevented by setting them to NULL before deletion)
+ * The object has shared ownership of its subtree. If this object is deleted and no other object has a shared
+ * ownership of the subtree it will be deleted as well.
*
* @see AbstractPathFormula
* @see AbstractPrctlFormula
@@ -56,25 +66,24 @@ class Next : public AbstractPathFormula<T> {
public:
/*!
- * Empty constructor
+ * Creates a Next node without a subnode.
+ * The resulting object will not represent a complete formula!
*/
Next() : child(nullptr){
// Intentionally left empty.
}
/*!
- * Constructor
+ * Creates a Next node using the given parameter.
*
- * @param child The child node
+ * @param child The child formula subtree.
*/
Next(std::shared_ptr<AbstractStateFormula<T>> const & child) : child(child){
// Intentionally left empty.
}
/*!
- * Constructor.
- *
- * Deletes the subtree iff this object is the last remaining owner of the subtree.
+ * Empty virtual destructor.
*/
virtual ~Next() {
// Intentionally left empty.
@@ -83,13 +92,13 @@ public:
/*!
* Clones the called object.
*
- * Performs a "deep copy", i.e. the subtrees of the new object are clones of the original ones
+ * Performs a "deep copy", i.e. the subnodes of the new object are clones of the original ones.
*
- * @returns a new BoundedUntil-object that is identical the called object.
+ * @returns A new Next object that is a deep copy of the called object.
*/
virtual std::shared_ptr<AbstractPathFormula<T>> clone() const override {
std::shared_ptr<Next<T>> result(new Next<T>());
- if (this->childIsSet()) {
+ if (this->isChildSet()) {
result->setChild(child->clone());
}
return result;
@@ -109,7 +118,9 @@ public:
}
/*!
- * @returns a string representation of the formula
+ * Returns a textual representation of the formula tree with this node as root.
+ *
+ * @returns A string representing the formula tree.
*/
virtual std::string toString() const override {
std::string result = "X ";
@@ -118,29 +129,35 @@ public:
}
/*!
- * @returns the child node
+ * Gets the child node.
+ *
+ * @returns The child node.
*/
std::shared_ptr<AbstractStateFormula<T>> const & getChild() const {
return child;
}
/*!
- * Sets the subtree
- * @param child the new child node
+ * Sets the subtree.
+ *
+ * @param child The new child.
*/
void setChild(std::shared_ptr<AbstractStateFormula<T>> const & child) {
this->child = child;
}
/*!
+ * Checks if the child is set, i.e. it does not point to null.
*
- * @return True if the child node is set, i.e. it does not point to nullptr; false otherwise
+ * @return True iff the child is set.
*/
- bool childIsSet() const {
+ bool isChildSet() const {
return child.get() != nullptr;
}
private:
+
+ // The child node.
std::shared_ptr<AbstractStateFormula<T>> child;
};
diff --git a/src/formula/prctl/Not.h b/src/formula/prctl/Not.h
index a58c5d3f4..83af85e53 100644
--- a/src/formula/prctl/Not.h
+++ b/src/formula/prctl/Not.h
@@ -15,34 +15,42 @@ namespace storm {
namespace property {
namespace prctl {
+// Forward declaration for the interface class.
template <class T> class Not;
/*!
- * @brief Interface class for model checkers that support Not.
+ * Interface class for model checkers that support Not.
*
- * All model checkers that support the formula class Not must inherit
- * this pure virtual class.
+ * All model checkers that support the formula class Not must inherit
+ * this pure virtual class.
*/
template <class T>
class INotModelChecker {
public:
+
/*!
- * @brief Evaluates Not formula within a model checker.
+ * Empty virtual destructor.
+ */
+ virtual ~INotModelChecker() {
+ // Intentionally left empty
+ }
+
+ /*!
+ * Evaluates Not formulas within a model checker.
*
- * @param obj Formula object with subformulas.
- * @return Result of the formula for every node.
+ * @param obj Formula object with subformulas.
+ * @return Result of the formula for every node.
*/
virtual storm::storage::BitVector checkNot(const Not<T>& obj) const = 0;
};
/*!
- * @brief
- * Class for an abstract formula tree with NOT node as root.
+ * Class for an Prctl formula tree with Not node as root.
*
- * Has one Abstract state formula as sub formula/tree.
+ * Has one state formula as sub formula/tree.
*
- * The subtree is seen as part of the object and deleted with the object
- * (this behavior can be prevented by setting them to NULL before deletion)
+ * The object has shared ownership of its subtree. If this object is deleted and no other object has a shared
+ * ownership of the subtree it will be deleted as well.
*
* @see AbstractStateFormula
* @see AbstractPrctlFormula
@@ -53,24 +61,24 @@ class Not : public AbstractStateFormula<T> {
public:
/*!
- * Empty constructor
+ * Creates a Not node without a subnode.
+ * The resulting object will not represent a complete formula!
*/
Not() : child(nullptr) {
// Intentionally left empty.
}
/*!
- * Constructor
- * @param child The child node
+ * Creates a Not node using the given parameter.
+ *
+ * @param child The child formula subtree.
*/
Not(std::shared_ptr<AbstractStateFormula<T>> child) : child(child) {
// Intentionally left empty.
}
/*!
- * Destructor
- *
- * Deletes the subtree iff this object is the last remaining owner of the subtree.
+ * Empty virtual destructor.
*/
virtual ~Not() {
// Intentionally left empty.
@@ -79,13 +87,13 @@ public:
/*!
* Clones the called object.
*
- * Performs a "deep copy", i.e. the subtrees of the new object are clones of the original ones
+ * Performs a "deep copy", i.e. the subnodes of the new object are clones of the original ones.
*
- * @returns a new AND-object that is identical the called object.
+ * @returns A new Not object that is a deep copy of the called object.
*/
virtual std::shared_ptr<AbstractStateFormula<T>> clone() const override {
std::shared_ptr<Not<T>> result(new Not<T>());
- if (this->childIsSet()) {
+ if (this->isChildSet()) {
result->setChild(child->clone());
}
return result;
@@ -105,7 +113,9 @@ public:
}
/*!
- * @returns a string representation of the formula
+ * Returns a textual representation of the formula tree with this node as root.
+ *
+ * @returns A string representing the formula tree.
*/
virtual std::string toString() const override {
std::string result = "!";
@@ -124,29 +134,35 @@ public:
}
/*!
- * @returns The child node
+ * Gets the child node.
+ *
+ * @returns The child node.
*/
std::shared_ptr<AbstractStateFormula<T>> const & getChild() const {
return child;
}
/*!
- * Sets the subtree
- * @param child the new child node
+ * Sets the subtree.
+ *
+ * @param child The new child.
*/
void setChild(std::shared_ptr<AbstractStateFormula<T>> const & child) {
this->child = child;
}
/*!
+ * Checks if the child is set, i.e. it does not point to null.
*
- * @return True if the child node is set, i.e. it does not point to nullptr; false otherwise
+ * @return True iff the child is set.
*/
- bool childIsSet() const {
+ bool isChildSet() const {
return child.get() != nullptr;
}
private:
+
+ // The child node.
std::shared_ptr<AbstractStateFormula<T>> child;
};
diff --git a/src/formula/prctl/Or.h b/src/formula/prctl/Or.h
index 646b5735c..3044ce3e7 100644
--- a/src/formula/prctl/Or.h
+++ b/src/formula/prctl/Or.h
@@ -14,37 +14,45 @@ namespace storm {
namespace property {
namespace prctl {
+// Forward declaration for the interface class.
template <class T> class Or;
/*!
- * @brief Interface class for model checkers that support Or.
+ * Interface class for model checkers that support Or.
*
- * All model checkers that support the formula class Or must inherit
- * this pure virtual class.
+ * All model checkers that support the formula class Or must inherit
+ * this pure virtual class.
*/
template <class T>
class IOrModelChecker {
public:
+
+ /*!
+ * Empty virtual destructor.
+ */
+ virtual ~IOrModelChecker() {
+ // Intentionally left empty
+ }
+
/*!
- * @brief Evaluates Or formula within a model checker.
+ * Evaluates Or formula within a model checker.
*
- * @param obj Formula object with subformulas.
- * @return Result of the formula for every node.
+ * @param obj Formula object with subformulas.
+ * @return Result of the formula for every node.
*/
virtual storm::storage::BitVector checkOr(const Or<T>& obj) const = 0;
};
/*!
- * @brief
- * Class for an abstract formula tree with OR node as root.
+ * Class for a Prctl formula tree with an Or node as root.
*
- * Has two Abstract state formulas as sub formulas/trees.
+ * Has two state formulas as sub formulas/trees.
*
- * As OR is commutative, the order is \e theoretically not important, but will influence the order in which
+ * As Or is commutative, the order is \e theoretically not important, but will influence the order in which
* the model checker works.
*
- * 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)
+ * The object has shared ownership of its subtrees. If this object is deleted and no other object has a shared
+ * ownership of the subtrees they will be deleted as well.
*
* @see AbstractStateFormula
* @see AbstractPrctlFormula
@@ -55,28 +63,25 @@ class Or : public AbstractStateFormula<T> {
public:
/*!
- * Empty constructor.
- * Will create an OR-node without subnotes. Will not represent a complete formula!
+ * Creates an Or node without subnodes.
+ * The resulting object will not represent a complete formula!
*/
Or() : left(nullptr), right(nullptr) {
// Intentionally left empty.
}
/*!
- * Constructor.
- * Creates an OR note with the parameters as subtrees.
+ * Creates an Or node with the parameters as subtrees.
*
- * @param left The left sub formula
- * @param right The right sub formula
+ * @param left The left sub formula.
+ * @param right The right sub formula.
*/
Or(std::shared_ptr<AbstractStateFormula<T>> left, std::shared_ptr<AbstractStateFormula<T>> right) : left(left), right(right) {
// Intentionally left empty.
}
/*!
- * Destructor.
- *
- * Deletes the subtree iff this object is the last remaining owner of the subtree.
+ * Empty virtual destructor.
*/
virtual ~Or() {
// Intentionally left empty.
@@ -85,16 +90,16 @@ public:
/*!
* Clones the called object.
*
- * Performs a "deep copy", i.e. the subtrees of the new object are clones of the original ones
+ * Performs a "deep copy", i.e. the subtrees of the new object are clones of the original ones.
*
- * @returns a new AND-object that is identical the called object.
+ * @returns A new Or object that is a deep copy of the called object.
*/
virtual std::shared_ptr<AbstractStateFormula<T>> clone() const override {
std::shared_ptr<Or<T>> result(new Or());
- if (this->leftIsSet()) {
+ if (this->isLeftSet()) {
result->setLeft(left->clone());
}
- if (this->rightIsSet()) {
+ if (this->isRightSet()) {
result->setRight(right->clone());
}
return result;
@@ -114,7 +119,9 @@ public:
}
/*!
- * @returns a string representation of the formula
+ * Returns a textual representation of the formula tree with this node as root.
+ *
+ * @returns A string representing the formula tree.
*/
virtual std::string toString() const override {
std::string result = "(";
@@ -136,55 +143,65 @@ public:
}
/*!
- * Sets the left child node.
+ * Gets the left child node.
*
- * @param newLeft the new left child.
+ * @returns The left child node.
*/
- void setLeft(std::shared_ptr<AbstractStateFormula<T>> const & newLeft) {
- left = newLeft;
+ std::shared_ptr<AbstractStateFormula<T>> const & getLeft() const {
+ return left;
}
/*!
- * Sets the right child node.
+ * Gets the right child node.
*
- * @param newRight the new right child.
+ * @returns The right child node.
*/
- void setRight(std::shared_ptr<AbstractStateFormula<T>> const & newRight) {
- right = newRight;
+ std::shared_ptr<AbstractStateFormula<T>> const & getRight() const {
+ return right;
}
/*!
- * @returns a pointer to the left child node
+ * Sets the left child node.
+ *
+ * @param newLeft The new left child.
*/
- std::shared_ptr<AbstractStateFormula<T>> const & getLeft() const {
- return left;
+ void setLeft(std::shared_ptr<AbstractStateFormula<T>> const & newLeft) {
+ left = newLeft;
}
/*!
- * @returns a pointer to the right child node
+ * Sets the right child node.
+ *
+ * @param newRight The new right child.
*/
- std::shared_ptr<AbstractStateFormula<T>> const & getRight() const {
- return right;
+ void setRight(std::shared_ptr<AbstractStateFormula<T>> const & newRight) {
+ right = newRight;
}
/*!
+ * Checks if the left child is set, i.e. it does not point to null.
*
- * @return True if the left child is set, i.e. it does not point to nullptr; false otherwise
+ * @return True iff the left child is set.
*/
- bool leftIsSet() const {
+ bool isLeftSet() const {
return left.get() != nullptr;
}
/*!
+ * Checks if the right child is set, i.e. it does not point to null.
*
- * @return True if the right child is set, i.e. it does not point to nullptr; false otherwise
+ * @return True iff the left right is set.
*/
- bool rightIsSet() const {
+ bool isRightSet() const {
return right.get() != nullptr;
}
private:
+
+ // The left child node.
std::shared_ptr<AbstractStateFormula<T>> left;
+
+ // The right child node.
std::shared_ptr<AbstractStateFormula<T>> right;
};
diff --git a/src/formula/prctl/PrctlFilter.h b/src/formula/prctl/PrctlFilter.h
index 6341764f9..02ffa5c5a 100644
--- a/src/formula/prctl/PrctlFilter.h
+++ b/src/formula/prctl/PrctlFilter.h
@@ -15,15 +15,6 @@
#include "src/modelchecker/prctl/AbstractModelChecker.h"
#include "src/formula/actions/AbstractAction.h"
-// TODO: Test if this can be can be ommitted.
-namespace storm {
-namespace property {
-namespace action {
- template <typename T> class AbstractAction;
-}
-}
-}
-
#include <algorithm>
#include <memory>
@@ -31,33 +22,81 @@ namespace storm {
namespace property {
namespace prctl {
+/*!
+ * This is the Prctl specific filter.
+ *
+ * It maintains a Prctl formula which can be checked against a given model by either calling evaluate() or check().
+ * Additionally it maintains a list of filter actions that are used to further manipulate the modelchecking results and prepare them for output.
+ */
template <class T>
class PrctlFilter : public storm::property::AbstractFilter<T> {
+ // Convenience typedef to make the code more readable.
typedef typename storm::property::action::AbstractAction<T>::Result Result;
public:
+ /*!
+ * Creates an empty PrctlFilter, maintaining no Prctl formula.
+ *
+ * Calling check or evaluate will return an empty result.
+ */
PrctlFilter() : AbstractFilter<T>(UNDEFINED), child(nullptr) {
// Intentionally left empty.
}
+ /*!
+ * Creates a PrctlFilter maintaining a Prctl formula but containing no actions.
+ *
+ * The modelchecking result will be returned or printed as is.
+ *
+ * @param child The Prctl formula to be maintained.
+ * @param opt An enum value indicating which kind of scheduler shall be used for path formulas on nondeterministic models.
+ */
PrctlFilter(std::shared_ptr<AbstractPrctlFormula<T>> const & child, OptimizingOperator opt = UNDEFINED) : AbstractFilter<T>(opt), child(child) {
// Intentionally left empty.
}
+ /*!
+ * Creates a PrctlFilter maintaining a Prctl formula and containing a single action.
+ *
+ * The given action will be applied to the modelchecking result during evaluation.
+ * Further actions can be added later.
+ *
+ * @param child The Prctl formula to be maintained.
+ * @param action The single action to be executed during evaluation.
+ * @param opt An enum value indicating which kind of scheduler shall be used for path formulas on nondeterministic models.
+ */
PrctlFilter(std::shared_ptr<AbstractPrctlFormula<T>> const & child, std::shared_ptr<action::AbstractAction<T>> const & action, OptimizingOperator opt = UNDEFINED) : AbstractFilter<T>(action, opt), child(child) {
// Intentionally left empty.
}
+ /*!
+ * Creates a PrctlFilter using the given parameters.
+ *
+ * The given actions will be applied to the modelchecking result in ascending index order during evaluation.
+ * Further actions can be added later.
+ *
+ * @param child The Prctl formula to be maintained.
+ * @param actions A vector conatining the actions that are to be executed during evaluation.
+ * @param opt An enum value indicating which kind of scheduler shall be used for path formulas on nondeterministic models.
+ */
PrctlFilter(std::shared_ptr<AbstractPrctlFormula<T>> const & child, std::vector<std::shared_ptr<action::AbstractAction<T>>> const & actions, OptimizingOperator opt = UNDEFINED) : AbstractFilter<T>(actions, opt), child(child) {
// Intentionally left empty.
}
+ /*!
+ * Empty virtual destructor.
+ */
virtual ~PrctlFilter() {
// Intentionally left empty.
}
+ /*!
+ * Calls the modelchecker, retrieves the modelchecking result, applies the filter action one by one and prints out the result.
+ *
+ * @param modelchecker The modelchecker to be called.
+ */
void check(storm::modelchecker::prctl::AbstractModelChecker<T> const & modelchecker) const {
// Write out the formula to be checked.
@@ -68,6 +107,12 @@ public:
writeOut(evaluate(modelchecker), modelchecker);
}
+ /*!
+ * Calls the modelchecker, retrieves the modelchecking result, applies the filter action one by one and returns the result.
+ *
+ * @param modelchecker The modelchecker to be called.
+ * @returns The result of the sequential application of the filter actions to the modelchecking result.
+ */
Result evaluate(storm::modelchecker::prctl::AbstractModelChecker<T> const & modelchecker) const {
Result result;
@@ -88,6 +133,13 @@ public:
return result;
}
+ /*!
+ * Returns a textual representation of the filter.
+ *
+ * That includes the actions as well as the maintained formula.
+ *
+ * @returns A string representing the filter.
+ */
virtual std::string toString() const override {
std::string desc = "";
@@ -175,26 +227,44 @@ public:
return desc;
}
- virtual std::string toPrettyString() const override {
- std::string desc = "Filter: ";
- desc += "\nActions:";
- for(auto action : this->actions) {
- desc += "\n\t" + action->toString();
- }
- desc += "\nFormula:\n\t" + child->toString();
- return desc;
+ /*!
+ * Gets the child node.
+ *
+ * @returns The child node.
+ */
+ std::shared_ptr<AbstractPrctlFormula<T>> const & getChild() const {
+ return child;
}
+ /*!
+ * Sets the subtree.
+ *
+ * @param child The new child.
+ */
void setChild(std::shared_ptr<AbstractPrctlFormula<T>> const & child) {
this->child = child;
}
- std::shared_ptr<AbstractPrctlFormula<T>> const & getChild() const {
- return child;
+ /*!
+ * Checks if the child is set, i.e. it does not point to null.
+ *
+ * @return True iff the child is set.
+ */
+ bool isChildSet() const {
+ return child.get() != nullptr;
}
private:
+ /*!
+ * Calls the modelchecker for a state formula, retrieves the modelchecking result, applies the filter action one by one and returns the result.
+ *
+ * This an internal version of the evaluate method overloading it for the different Prctl formula types.
+ *
+ * @param modelchecker The modelchecker to be called.
+ * @param formula The state formula for which the modelchecker will be called.
+ * @returns The result of the sequential application of the filter actions to the modelchecking result.
+ */
Result evaluate(storm::modelchecker::prctl::AbstractModelChecker<T> const & modelchecker, std::shared_ptr<AbstractStateFormula<T>> const & formula) const {
// First, get the model checking result.
Result result;
@@ -210,6 +280,15 @@ private:
return evaluateActions(result, modelchecker);
}
+ /*!
+ * Calls the modelchecker for a path formula, retrieves the modelchecking result, applies the filter action one by one and returns the result.
+ *
+ * This an internal version of the evaluate method overloading it for the different Prctl formula types.
+ *
+ * @param modelchecker The modelchecker to be called.
+ * @param formula The path formula for which the modelchecker will be called.
+ * @returns The result of the sequential application of the filter actions to the modelchecking result.
+ */
Result evaluate(storm::modelchecker::prctl::AbstractModelChecker<T> const & modelchecker, std::shared_ptr<AbstractPathFormula<T>> const & formula) const {
// First, get the model checking result.
Result result;
@@ -225,6 +304,15 @@ private:
return evaluateActions(result, modelchecker);
}
+ /*!
+ * Calls the modelchecker for a reward formula, retrieves the modelchecking result, applies the filter action one by one and returns the result.
+ *
+ * This an internal version of the evaluate method overloading it for the different Prctl formula types.
+ *
+ * @param modelchecker The modelchecker to be called.
+ * @param formula The reward formula for which the modelchecker will be called.
+ * @returns The result of the sequential application of the filter actions to the modelchecking result.
+ */
Result evaluate(storm::modelchecker::prctl::AbstractModelChecker<T> const & modelchecker, std::shared_ptr<AbstractRewardPathFormula<T>> const & formula) const {
// First, get the model checking result.
Result result;
@@ -240,6 +328,13 @@ private:
return evaluateActions(result, modelchecker);
}
+ /*!
+ * Evaluates the filter actions by calling them one by one using the output of each action as the input for the next one.
+ *
+ * @param input The modelchecking result in form of a Result struct.
+ * @param modelchecker The modelchecker that was called to generate the modelchecking result. Needed by some actions.
+ * @returns The result of the sequential application of the filter actions to the modelchecking result.
+ */
Result evaluateActions(Result const & input, storm::modelchecker::prctl::AbstractModelChecker<T> const & modelchecker) const {
// Init the state selection and state map vectors.
@@ -258,7 +353,12 @@ private:
return result;
}
-
+ /*!
+ * Writes out the given result.
+ *
+ * @param result The result of the sequential application of the filter actions to a modelchecking result.
+ * @param modelchecker The modelchecker that was called to generate the modelchecking result. Needed for legacy support.
+ */
void writeOut(Result const & result, storm::modelchecker::prctl::AbstractModelChecker<T> const & modelchecker) const {
// Test if there is anything to write out.
@@ -323,6 +423,7 @@ private:
std::cout << std::endl << "-------------------------------------------" << std::endl;
}
+ // The Prctl formula maintained by this filter.
std::shared_ptr<AbstractPrctlFormula<T>> child;
};
diff --git a/src/formula/prctl/ProbabilisticBoundOperator.h b/src/formula/prctl/ProbabilisticBoundOperator.h
index 6905d9069..abaf1e1db 100644
--- a/src/formula/prctl/ProbabilisticBoundOperator.h
+++ b/src/formula/prctl/ProbabilisticBoundOperator.h
@@ -17,40 +17,51 @@ namespace storm {
namespace property {
namespace prctl {
+// Forward declaration for the interface class.
template <class T> class ProbabilisticBoundOperator;
/*!
- * @brief Interface class for model checkers that support ProbabilisticBoundOperator.
+ * Interface class for model checkers that support ProbabilisticBoundOperator.
*
- * All model checkers that support the formula class PathBoundOperator must inherit
- * this pure virtual class.
+ * All model checkers that support the formula class PathBoundOperator must inherit
+ * this pure virtual class.
*/
template <class T>
class IProbabilisticBoundOperatorModelChecker {
public:
+
+ /*!
+ * Empty virtual destructor.
+ */
+ virtual ~IProbabilisticBoundOperatorModelChecker() {
+ // Intentionally left empty
+ }
+
+ /*!
+ * Evaluates a ProbabilisticBoundOperator within a model checker.
+ *
+ * @param obj Formula object with subformulas.
+ * @return The modelchecking result of the formula for every state.
+ */
virtual storm::storage::BitVector checkProbabilisticBoundOperator(const ProbabilisticBoundOperator<T>& obj) const = 0;
};
/*!
- * @brief
- * Class for an abstract formula tree with a P (probablistic) operator node over a probability interval
- * as root.
+ * Class for a Prctl formula tree with a P (probablistic) bound operator node as root.
*
- * Has one Abstract path formula as sub formula/tree.
+ * Has one path formula as sub formula/tree.
*
* @par Semantics
- * The formula holds iff the probability that the path formula holds is inside the bounds
- * specified in this operator
- *
- * 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)
+ * The formula holds iff the probability that the path formula holds meets the bound
+ * specified in this operator.
*
+ * The object has shared ownership of its subtree. If this object is deleted and no other object has a shared
+ * ownership of the subtree it will be deleted as well.
*
* @see AbstractStateFormula
* @see AbstractPathFormula
- * @see ProbabilisticOperator
- * @see ProbabilisticNoBoundsOperator
* @see AbstractPrctlFormula
+ * @see RewardBoundOperator
*/
template<class T>
class ProbabilisticBoundOperator : public AbstractStateFormula<T> {
@@ -58,18 +69,19 @@ class ProbabilisticBoundOperator : public AbstractStateFormula<T> {
public:
/*!
- * Empty constructor
+ * Creates a ProbabilisticBoundOperator node without a subnode.
+ * The resulting object will not represent a complete formula!
*/
ProbabilisticBoundOperator() : comparisonOperator(LESS), bound(0), child(nullptr) {
// Intentionally left empty.
}
/*!
- * Constructor for non-optimizing operator.
+ * Creates a ProbabilisticBoundOperator node using the given parameters.
*
* @param comparisonOperator The relation for the bound.
- * @param bound The bound for the probability
- * @param child The child node
+ * @param bound The bound for the probability.
+ * @param child The child formula subtree.
*/
ProbabilisticBoundOperator(storm::property::ComparisonType comparisonOperator, T bound, std::shared_ptr<AbstractPathFormula<T>> const & child)
: comparisonOperator(comparisonOperator), bound(bound), child(child) {
@@ -77,9 +89,7 @@ public:
}
/*!
- * Destructor
- *
- * Deletes the subtree iff this object is the last remaining owner of the subtree.
+ * Empty virtual destructor.
*/
virtual ~ProbabilisticBoundOperator() {
// Intentionally left empty.
@@ -88,9 +98,9 @@ public:
/*!
* Clones the called object.
*
- * Performs a "deep copy", i.e. the subtrees of the new object are clones of the original ones
+ * Performs a "deep copy", i.e. the subnodes of the new object are clones of the original ones.
*
- * @returns a new AND-object that is identical the called object.
+ * @returns A new ProbabilisticBoundOperator object that is a deep copy of the called object.
*/
virtual std::shared_ptr<AbstractStateFormula<T>> clone() const override {
std::shared_ptr<ProbabilisticBoundOperator<T>> result(new ProbabilisticBoundOperator<T>());
@@ -114,7 +124,9 @@ public:
}
/*!
- * @returns a string representation of the formula
+ * Returns a textual representation of the formula tree with this node as root.
+ *
+ * @returns A string representing the formula tree.
*/
virtual std::string toString() const override {
std::string result = "P ";
@@ -133,56 +145,74 @@ public:
}
/*!
- * @returns the child node (representation of a formula)
+ * Gets the child node.
+ *
+ * @returns The child node.
*/
std::shared_ptr<AbstractPathFormula<T>> const & getChild () const {
return child;
}
/*!
- * Sets the child node
+ * Sets the subtree.
*
- * @param child the path formula that becomes the new child node
+ * @param child The new child.
*/
void setChild(std::shared_ptr<AbstractPathFormula<T>> const & child) {
this->child = child;
}
/*!
+ * Checks if the child is set, i.e. it does not point to null.
*
- * @return True if the path formula is set, i.e. it does not point to nullptr; false otherwise
+ * @return True iff the child is set.
*/
- bool childIsSet() const {
+ bool isChildSet() const {
return child.get() != nullptr;
}
/*!
- * @returns the comparison relation
+ * Gets the comparison operator.
+ *
+ * @returns An enum value representing the comparison relation.
*/
storm::property::ComparisonType const getComparisonOperator() const {
return comparisonOperator;
}
+ /*!
+ * Sets the comparison operator.
+ *
+ * @param comparisonOperator An enum value representing the new comparison relation.
+ */
void setComparisonOperator(storm::property::ComparisonType comparisonOperator) {
this->comparisonOperator = comparisonOperator;
}
/*!
- * @returns the bound for the measure
+ * Gets the bound which the probability that the path formula holds has to obey.
+ *
+ * @returns The probability bound.
*/
T const & getBound() const {
return bound;
}
/*!
- * Sets the interval in which the probability that the path formula holds may lie in.
+ * Sets the bound which the probability that the path formula holds has to obey.
*
- * @param bound The bound for the measure
+ * @param bound The new probability bound.
*/
void setBound(T bound) {
this->bound = bound;
}
+ /*!
+ * Checks if the bound is met by the given value.
+ *
+ * @param value The value to test against the bound.
+ * @returns True iff value <comparisonOperator> bound holds.
+ */
bool meetsBound(T value) const {
switch (comparisonOperator) {
case LESS: return value < bound; break;
@@ -194,8 +224,14 @@ public:
}
private:
+
+ // The operator used to indicate the kind of bound that is to be met.
storm::property::ComparisonType comparisonOperator;
+
+ // The probability bound.
T bound;
+
+ // The path formula for which the probability to be satisfied has to meet the bound.
std::shared_ptr<AbstractPathFormula<T>> child;
};
diff --git a/src/formula/prctl/ReachabilityReward.h b/src/formula/prctl/ReachabilityReward.h
index 0fe5f5792..2187b6250 100644
--- a/src/formula/prctl/ReachabilityReward.h
+++ b/src/formula/prctl/ReachabilityReward.h
@@ -15,62 +15,77 @@ namespace storm {
namespace property {
namespace prctl {
+// Forward declaration for the interface class.
template <class T> class ReachabilityReward;
/*!
- * @brief Interface class for model checkers that support ReachabilityReward.
+ * Interface class for model checkers that support ReachabilityReward.
*
- * All model checkers that support the formula class ReachabilityReward must inherit
- * this pure virtual class.
+ * All model checkers that support the formula class ReachabilityReward must inherit
+ * this pure virtual class.
*/
template <class T>
class IReachabilityRewardModelChecker {
public:
+
+ /*!
+ * Empty virtual destructor.
+ */
+ virtual ~IReachabilityRewardModelChecker() {
+ // Intentionally left empty
+ }
+
/*!
- * @brief Evaluates ReachabilityReward formula within a model checker.
- *
- * @param obj Formula object with subformulas.
- * @return Result of the formula for every node.
- */
+ * Evaluates a ReachabilityReward formula within a model checker.
+ *
+ * @param obj Formula object with subformulas.
+ * @param qualitative A flag indicating whether the formula only needs to be evaluated qualitatively, i.e. if the
+ * results are only compared against the bounds 0 and 1.
+ * @return The modelchecking result of the formula for every state.
+ */
virtual std::vector<T> checkReachabilityReward(const ReachabilityReward<T>& obj, bool qualitative) const = 0;
};
/*!
- * @brief
- * Class for an abstract (path) formula tree with an Reachability Reward node as root.
+ * Class for an Prctl (reward path) formula tree with an Reachability Reward node as root.
+ *
+ * Has one state formula as sub formula/tree.
*
- * Has one Abstract state formula as sub formula/tree.
+ * This formula expresses the rewards received or costs needed to reach a state satisfying the formula \e child.
+ * In case the state under consiteration itself satisfies the formula \e child the rewards are zero.
+ * In case that there is a non zero probability of not reaching any of the target states the rewards are infinite.
+ * Also note that for this formula both state and transition rewards are considered and use if available in the model.
*
- * The subtree is seen as part of the object and deleted with the object
- * (this behavior can be prevented by setting them to nullptr before deletion)
+ * The object has shared ownership of its subtree. If this object is deleted and no other object has a shared
+ * ownership of the subtree it will be deleted as well.
*
- * @see AbstractPathFormula
+ * @see AbstractRewardPathFormula
* @see AbstractPrctlFormula
*/
template <class T>
class ReachabilityReward : public AbstractRewardPathFormula<T> {
public:
+
/*!
- * Empty constructor
+ * Creates a ReachabilityReward node without a subnode.
+ * The resulting object will not represent a complete formula!
*/
ReachabilityReward() : child(nullptr){
// Intentionally left empty
}
/*!
- * Constructor
+ * Creates an Eventually node using the given parameter.
*
- * @param child The child node
+ * @param child The child formula subtree.
*/
ReachabilityReward(std::shared_ptr<AbstractStateFormula<T>> child) : child(child){
// Intentionally left empty
}
/*!
- * Destructor.
- *
- * Deletes the subtree iff this object is the last remaining owner of the subtree.
+ * Empty virtual destructor.
*/
virtual ~ReachabilityReward() {
// Intentionally left empty.
@@ -79,13 +94,13 @@ public:
/*!
* Clones the called object.
*
- * Performs a "deep copy", i.e. the subtrees of the new object are clones of the original ones
+ * Performs a "deep copy", i.e. the subnodes of the new object are clones of the original ones.
*
- * @returns a new ReachabilityReward-object that is identical the called object.
+ * @returns A new ReachabilityReward object that is a deep copy of the called object.
*/
virtual std::shared_ptr<AbstractRewardPathFormula<T>> clone() const override {
std::shared_ptr<ReachabilityReward<T>> result(new ReachabilityReward<T>());
- if (this->childIsSet()) {
+ if (this->isChildSet()) {
result->setChild(child->clone());
}
return result;
@@ -105,7 +120,9 @@ public:
}
/*!
- * @returns a string representation of the formula
+ * Returns a textual representation of the formula tree with this node as root.
+ *
+ * @returns A string representing the formula tree.
*/
virtual std::string toString() const override {
std::string result = "F ";
@@ -114,29 +131,35 @@ public:
}
/*!
- * @returns the child node
+ * Gets the child node.
+ *
+ * @returns The child node.
*/
std::shared_ptr<AbstractStateFormula<T>> const & getChild() const {
return child;
}
/*!
- * Sets the subtree
- * @param child the new child node
+ * Sets the subtree.
+ *
+ * @param child The new child.
*/
void setChild(std::shared_ptr<AbstractStateFormula<T>> const & child) {
this->child = child;
}
/*!
+ * Checks if the child is set, i.e. it does not point to null.
*
- * @return True if the child node is set, i.e. it does not point to nullptr; false otherwise
+ * @return True iff the child is set.
*/
- bool childIsSet() const {
+ bool isChildSet() const {
return child.get() != nullptr;
}
private:
+
+ // The child node.
std::shared_ptr<AbstractStateFormula<T>> child;
};
diff --git a/src/formula/prctl/RewardBoundOperator.h b/src/formula/prctl/RewardBoundOperator.h
index 12900c58c..a7a4089a9 100644
--- a/src/formula/prctl/RewardBoundOperator.h
+++ b/src/formula/prctl/RewardBoundOperator.h
@@ -17,57 +17,72 @@ namespace storm {
namespace property {
namespace prctl {
+// Forward declaration for the interface class.
template <class T> class RewardBoundOperator;
/*!
- * @brief Interface class for model checkers that support RewardBoundOperator.
+ * Interface class for model checkers that support RewardBoundOperator.
*
- * All model checkers that support the formula class PathBoundOperator must inherit
- * this pure virtual class.
+ * All model checkers that support the formula class PathBoundOperator must inherit
+ * this pure virtual class.
*/
template <class T>
class IRewardBoundOperatorModelChecker {
public:
+
+ /*!
+ * Empty virtual destructor.
+ */
+ virtual ~IRewardBoundOperatorModelChecker() {
+ // Intentionally left empty
+ }
+
+ /*!
+ * Evaluates a RewardBoundOperator within a model checker.
+ *
+ * @param obj Formula object with subformulas.
+ * @return The modelchecking result of the formula for every state.
+ */
virtual storm::storage::BitVector checkRewardBoundOperator(const RewardBoundOperator<T>& obj) const = 0;
};
/*!
- * @brief
- * Class for an abstract formula tree with a R (reward) operator node over a reward interval as root.
+ * Class for a Prctl formula tree with an R (reward) operator node as root.
*
* Has a reward path formula as sub formula/tree.
*
* @par Semantics
- * The formula holds iff the reward of the reward path formula is inside the bounds
- * specified in this operator
+ * The formula holds iff the reward of the reward path formula meets the bound
+ * specified in this operator.
*
- * 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)
+ * The object has shared ownership of its subtree. If this object is deleted and no other object has a shared
+ * ownership of the subtree it will be deleted as well.
*
*
* @see AbstractStateFormula
- * @see AbstractPathFormula
- * @see ProbabilisticOperator
- * @see ProbabilisticNoBoundsOperator
+ * @see AbstractRewardPathFormula
* @see AbstractPrctlFormula
+ * @see ProbabilisticBoundOperator
*/
template<class T>
class RewardBoundOperator : public AbstractStateFormula<T> {
public:
+
/*!
- * Empty constructor
+ * Creates a RewardBoundOperator node without a subnode.
+ * The resulting object will not represent a complete formula!
*/
RewardBoundOperator() : comparisonOperator(LESS), bound(0), child(nullptr){
// Intentionally left empty
}
/*!
- * Constructor for non-optimizing operator.
+ * Creates a ProbabilisticBoundOperator node using the given parameters.
*
* @param comparisonOperator The relation for the bound.
- * @param bound The bound for the probability
- * @param child The child node
+ * @param bound The bound for the rewards.
+ * @param child The child formula subtree.
*/
RewardBoundOperator(storm::property::ComparisonType comparisonOperator, T bound, std::shared_ptr<AbstractRewardPathFormula<T>> const & child)
: comparisonOperator(comparisonOperator), bound(bound), child(child) {
@@ -75,9 +90,7 @@ public:
}
/*!
- * Destructor
- *
- * Deletes the subtree iff this object is the last remaining owner of the subtree.
+ * Empty virtual destructor.
*/
virtual ~RewardBoundOperator() {
// Intentionally left empty.
@@ -86,9 +99,9 @@ public:
/*!
* Clones the called object.
*
- * Performs a "deep copy", i.e. the subtrees of the new object are clones of the original ones
+ * Performs a "deep copy", i.e. the subnodes of the new object are clones of the original ones.
*
- * @returns a new AND-object that is identical the called object.
+ * @returns A new RewardBoundOperator object that is a deep copy of the called object.
*/
virtual std::shared_ptr<AbstractStateFormula<T>> clone() const override {
std::shared_ptr<RewardBoundOperator<T>> result(new RewardBoundOperator<T>());
@@ -112,7 +125,9 @@ public:
}
/*!
- * @returns a string representation of the formula
+ * Returns a textual representation of the formula tree with this node as root.
+ *
+ * @returns A string representing the formula tree.
*/
virtual std::string toString() const override {
std::string result = "R ";
@@ -131,56 +146,74 @@ public:
}
/*!
- * @returns the child node (representation of a formula)
+ * Gets the child node.
+ *
+ * @returns The child node.
*/
std::shared_ptr<AbstractRewardPathFormula<T>> const & getChild () const {
return child;
}
/*!
- * Sets the child node
+ * Sets the subtree.
*
- * @param child the path formula that becomes the new child node
+ * @param child The new child.
*/
void setChild(std::shared_ptr<AbstractRewardPathFormula<T>> const & child) {
this->child = child;
}
/*!
+ * Checks if the child is set, i.e. it does not point to null.
*
- * @return True if the path formula is set, i.e. it does not point to nullptr; false otherwise
+ * @return True iff the child is set.
*/
- bool childIsSet() const {
+ bool isChildSet() const {
return child.get() != nullptr;
}
/*!
- * @returns the comparison relation
+ * Gets the comparison operator.
+ *
+ * @returns An enum value representing the comparison relation.
*/
storm::property::ComparisonType const getComparisonOperator() const {
return comparisonOperator;
}
+ /*!
+ * Sets the comparison operator.
+ *
+ * @param comparisonOperator An enum value representing the new comparison relation.
+ */
void setComparisonOperator(storm::property::ComparisonType comparisonOperator) {
this->comparisonOperator = comparisonOperator;
}
/*!
- * @returns the bound for the measure
+ * Gets the bound which is to be obeyed by the rewards of the reward path formula.
+ *
+ * @returns The probability bound.
*/
T const & getBound() const {
return bound;
}
/*!
- * Sets the interval in which the probability that the path formula holds may lie in.
+ * Sets the bound which is to be obeyed by the rewards of the reward path formula
*
- * @param bound The bound for the measure
+ * @param bound The new reward bound.
*/
void setBound(T bound) {
this->bound = bound;
}
+ /*!
+ * Checks if the bound is met by the given value.
+ *
+ * @param value The value to test against the bound.
+ * @returns True iff value <comparisonOperator> bound holds.
+ */
bool meetsBound(T value) const {
switch (comparisonOperator) {
case LESS: return value < bound; break;
@@ -192,8 +225,14 @@ public:
}
private:
+
+ // The operator used to indicate the kind of bound that is to be met.
storm::property::ComparisonType comparisonOperator;
+
+ // The reward bound.
T bound;
+
+ // The reward path formula whose rewards have to meet the bound.
std::shared_ptr<AbstractRewardPathFormula<T>> child;
};
diff --git a/src/formula/prctl/SteadyStateReward.h b/src/formula/prctl/SteadyStateReward.h
index 84774998f..c075abba9 100644
--- a/src/formula/prctl/SteadyStateReward.h
+++ b/src/formula/prctl/SteadyStateReward.h
@@ -15,43 +15,60 @@ namespace storm {
namespace property {
namespace prctl {
+// Forward declaration for the interface class.
template <class T> class SteadyStateReward;
/*!
- * @brief Interface class for model checkers that support SteadyStateReward.
+ * Interface class for model checkers that support SteadyStateReward.
*
- * All model checkers that support the formula class SteadyStateReward must inherit
- * this pure virtual class.
+ * All model checkers that support the formula class SteadyStateReward must inherit
+ * this pure virtual class.
*/
template <class T>
class ISteadyStateRewardModelChecker {
public:
+
+ /*!
+ * Empty virtual destructor.
+ */
+ virtual ~ISteadyStateRewardModelChecker() {
+ // Intentionally left empty
+ }
+
/*!
- * @brief Evaluates CumulativeReward formula within a model checker.
- *
- * @param obj Formula object with subformulas.
- * @return Result of the formula for every node.
- */
+ * Evaluates a SteadyStateReward formula within a model checker.
+ *
+ * @param obj Formula object with subformulas.
+ * @param qualitative A flag indicating whether the formula only needs to be evaluated qualitatively, i.e. if the
+ * results are only compared against the bounds 0 and 1.
+ * @return The modelchecking result of the formula for every state.
+ */
virtual std::vector<T> checkSteadyStateReward(const SteadyStateReward<T>& obj, bool qualitative) const = 0;
};
/*!
- * @brief
- * Class for an abstract (path) formula tree with a Steady State Reward node as root.
+ * Class for a Steady State Reward formula.
+ * This class represents a possible leaf in a reward formula tree.
+ *
+ * This formula expresses the expected long-run rewards for each state in the model.
*
- * @see AbstractPathFormula
+ * @see AbstractRewardPathFormula
* @see AbstractPrctlFormula
*/
template <class T>
class SteadyStateReward: public AbstractRewardPathFormula<T> {
public:
+
/*!
- * Empty constructor
+ * Creates a new SteadyStateReward node.
*/
SteadyStateReward() {
// Intentionally left empty.
}
+ /*!
+ * Empty virtual destructor.
+ */
virtual ~SteadyStateReward() {
// Intentionally left empty.
}
@@ -59,12 +76,12 @@ public:
/*!
* Clones the called object.
*
- * Performs a "deep copy", i.e. the subtrees of the new object are clones of the original ones
+ * Performs a "deep copy", i.e. the subnodes of the new object are clones of the original ones.
*
- * @returns a new SteadyState-object that is identical the called object.
+ * @returns A new SteadyStateReward object that is a deep copy of the called object.
*/
virtual std::shared_ptr<AbstractRewardPathFormula<T>> clone() const override {
- std::shared_ptr<SteadyStateReward<T>> result(new SteadyStateReward<T>());
+ auto result = std::make_shared<SteadyStateReward<T>>();
return result;
}
@@ -82,7 +99,9 @@ public:
}
/*!
- * @returns a string representation of the formula
+ * Returns a textual representation of the formula tree with this node as root.
+ *
+ * @returns A string representing the formula tree.
*/
virtual std::string toString() const override {
return "S";
diff --git a/src/formula/prctl/Until.h b/src/formula/prctl/Until.h
index eb939b54f..27eb89167 100644
--- a/src/formula/prctl/Until.h
+++ b/src/formula/prctl/Until.h
@@ -15,41 +15,52 @@ namespace storm {
namespace property {
namespace prctl {
+// Forward declaration for the interface class.
template <class T> class Until;
/*!
- * @brief Interface class for model checkers that support Until.
+ * Interface class for model checkers that support Until.
*
- * All model checkers that support the formula class Until must inherit
- * this pure virtual class.
+ * All model checkers that support the formula class Until must inherit
+ * this pure virtual class.
*/
template <class T>
class IUntilModelChecker {
public:
+
+ /*!
+ * Empty virtual destructor.
+ */
+ virtual ~IUntilModelChecker() {
+ // Intentionally left empty
+ }
+
/*!
- * @brief Evaluates Until formula within a model checker.
- *
- * @param obj Formula object with subformulas.
- * @return Result of the formula for every node.
- */
+ * Evaluates an Until formula within a model checker.
+ *
+ * @param obj Formula object with subformulas.
+ * @param qualitative A flag indicating whether the formula only needs to be evaluated qualitatively, i.e. if the
+ * results are only compared against the bounds 0 and 1.
+ * @return The modelchecking result of the formula for every state.
+ */
virtual std::vector<T> checkUntil(const Until<T>& obj, bool qualitative) const = 0;
};
/*!
- * @brief
- * Class for an abstract (path) formula tree with an Until node as root.
+ * Class for a Prctl (path) formula tree with an Until node as root.
*
- * Has two Abstract state formulas as sub formulas/trees.
+ * Has two state formulas as sub formulas/trees.
*
* @par Semantics
* The formula holds iff eventually, formula \e right (the right subtree) holds, and before,
* \e left holds always.
*
- * 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)
+ * The object has shared ownership of its subtrees. If this object is deleted and no other object has a shared
+ * ownership of the subtrees they will be deleted as well.
*
* @see AbstractPathFormula
* @see AbstractPrctlFormula
+ * @see BoundedUntil
*/
template <class T>
class Until : public AbstractPathFormula<T> {
@@ -57,26 +68,25 @@ class Until : public AbstractPathFormula<T> {
public:
/*!
- * Empty constructor
+ * Creates an Until node without subnodes.
+ * The resulting object will not represent a complete formula!
*/
- Until() : left(nullptr), right(nullptr){
+ Until() : left(nullptr), right(nullptr) {
// Intentionally left empty.
}
/*!
- * Constructor
+ * Creates an Until node using the given parameters.
*
- * @param left The left formula subtree
- * @param right The left formula subtree
+ * @param left The left formula subtree.
+ * @param right The right formula subtree.
*/
- Until(std::shared_ptr<AbstractStateFormula<T>> const & left, std::shared_ptr<AbstractStateFormula<T>> const & right) : left(left), right(right){
+ Until(std::shared_ptr<AbstractStateFormula<T>> const & left, std::shared_ptr<AbstractStateFormula<T>> const & right) : left(left), right(right) {
// Intentionally left empty.
}
/*!
- * Destructor.
- *
- * Deletes the subtrees iff this object is the last remaining owner of the subtree to be deleted.
+ * Empty virtual destructor.
*/
virtual ~Until() {
// Intentionally left empty.
@@ -85,16 +95,16 @@ public:
/*!
* Clones the called object.
*
- * Performs a "deep copy", i.e. the subtrees of the new object are clones of the original ones
+ * Performs a "deep copy", i.e. the subnodes of the new object are clones of the original ones.
*
- * @returns a new BoundedUntil-object that is identical the called object.
+ * @returns A new Until object that is a deep copy of the called object.
*/
virtual std::shared_ptr<AbstractPathFormula<T>> clone() const override {
std::shared_ptr<Until<T>> result(new Until());
- if (this->leftIsSet()) {
+ if (this->isLeftSet()) {
result->setLeft(left->clone());
}
- if (this->rightIsSet()) {
+ if (this->isRightSet()) {
result->setRight(right->clone());
}
return result;
@@ -114,7 +124,9 @@ public:
}
/*!
- * @returns a string representation of the formula
+ * Returns a textual representation of the formula tree with this node as root.
+ *
+ * @returns A string representing the formula tree.
*/
virtual std::string toString() const override {
std::string result = left->toString();
@@ -124,55 +136,65 @@ public:
}
/*!
- * Sets the left child node.
+ * Gets the left child node.
*
- * @param newLeft the new left child.
+ * @returns The left child node.
*/
- void setLeft(std::shared_ptr<AbstractStateFormula<T>> const & newLeft) {
- left = newLeft;
+ std::shared_ptr<AbstractStateFormula<T>> const & getLeft() const {
+ return left;
}
/*!
- * Sets the right child node.
+ * Gets the right child node.
*
- * @param newRight the new right child.
+ * @returns The right child node.
*/
- void setRight(std::shared_ptr<AbstractStateFormula<T>> const & newRight) {
- right = newRight;
+ std::shared_ptr<AbstractStateFormula<T>> const & getRight() const {
+ return right;
}
/*!
- * @returns a pointer to the left child node
+ * Sets the left child node.
+ *
+ * @param newLeft The new left child.
*/
- std::shared_ptr<AbstractStateFormula<T>> const & getLeft() const {
- return left;
+ void setLeft(std::shared_ptr<AbstractStateFormula<T>> const & newLeft) {
+ left = newLeft;
}
/*!
- * @returns a pointer to the right child node
+ * Sets the right child node.
+ *
+ * @param newRight The new right child.
*/
- std::shared_ptr<AbstractStateFormula<T>> const & getRight() const {
- return right;
+ void setRight(std::shared_ptr<AbstractStateFormula<T>> const & newRight) {
+ right = newRight;
}
/*!
+ * Checks if the left child is set, i.e. it does not point to null.
*
- * @return True if the left child is set, i.e. it does not point to nullptr; false otherwise
+ * @return True iff the left child is set.
*/
- bool leftIsSet() const {
+ bool isLeftSet() const {
return left.get() != nullptr;
}
/*!
+ * Checks if the right child is set, i.e. it does not point to null.
*
- * @return True if the right child is set, i.e. it does not point to nullptr; false otherwise
+ * @return True iff the right child is set.
*/
- bool rightIsSet() const {
+ bool isRightSet() const {
return right.get() != nullptr;
}
private:
+
+ // The left child node.
std::shared_ptr<AbstractStateFormula<T>> left;
+
+ // The right child node.
std::shared_ptr<AbstractStateFormula<T>> right;
};
diff --git a/src/parser/CslParser.h b/src/parser/CslParser.h
index 9e9b85da5..ccb5b90c3 100644
--- a/src/parser/CslParser.h
+++ b/src/parser/CslParser.h
@@ -15,6 +15,11 @@
namespace storm {
namespace parser {
+/*!
+ * Reads a Csl formula from a string and returns the formula tree.
+ *
+ * If you want to read the formula from a file, use the LtlFileParser class instead.
+ */
class CslParser {
public:
@@ -24,8 +29,9 @@ public:
*
* If the string could not be parsed successfully, it will throw a wrongFormatException.
*
- * @param formulaString The string representation of the formula
- * @throw wrongFormatException If the input could not be parsed successfully
+ * @param formulaString The string representation of the formula.
+ * @throw wrongFormatException If the input could not be parsed successfully.
+ * @return A CslFilter maintaining the parsed formula.
*/
static std::shared_ptr<storm::property::csl::CslFilter<double>> parseCslFormula(std::string formulaString);
diff --git a/src/parser/LtlFileParser.h b/src/parser/LtlFileParser.h
index 2fd73d10f..f21210b7d 100644
--- a/src/parser/LtlFileParser.h
+++ b/src/parser/LtlFileParser.h
@@ -22,8 +22,8 @@ public:
/*!
* Parses each line of a given file as prctl formula and returns a list containing the results of the parsing.
*
- * @param filename
- * @return The list of parsed formulas
+ * @param filename Name and path to the file in which the formula strings can be found.
+ * @return The list of parsed formulas.
*/
static std::list<std::shared_ptr<storm::property::ltl::LtlFilter<double>>> parseLtlFile(std::string filename);
};
diff --git a/src/parser/LtlParser.h b/src/parser/LtlParser.h
index e5f24dec3..ebbad77c0 100644
--- a/src/parser/LtlParser.h
+++ b/src/parser/LtlParser.h
@@ -28,8 +28,9 @@ public:
*
* If the string could not be parsed successfully, it will throw a wrongFormatException.
*
- * @param formulaString The string representation of the formula
- * @throw wrongFormatException If the input could not be parsed successfully
+ * @param formulaString The string representation of the formula.
+ * @throw wrongFormatException If the input could not be parsed successfully.
+ * @return A LtlFilter maintaining the parsed formula.
*/
static std::shared_ptr<storm::property::ltl::LtlFilter<double>> parseLtlFormula(std::string formulaString);
diff --git a/src/parser/PrctlFileParser.h b/src/parser/PrctlFileParser.h
index c992ddf03..615e219c1 100644
--- a/src/parser/PrctlFileParser.h
+++ b/src/parser/PrctlFileParser.h
@@ -20,9 +20,9 @@ class PrctlFileParser {
public:
/*!
- * Parses each line of a given file as prctl formula and returns a list containing the results of the parsing.
+ * Parses each line of a given file as Prctl formula and returns a list containing the results of the parsing.
*
- * @param filename
+ * @param filename Name and path to the file in which the formula strings can be found.
* @return The list of parsed formulas
*/
static std::list<std::shared_ptr<storm::property::prctl::PrctlFilter<double>>> parsePrctlFile(std::string filename);
diff --git a/src/parser/PrctlParser.h b/src/parser/PrctlParser.h
index f8d5d6e78..75e13c117 100644
--- a/src/parser/PrctlParser.h
+++ b/src/parser/PrctlParser.h
@@ -16,14 +16,14 @@ class PrctlParser {
public:
/*!
- * Reads a PRCTL formula from its string representation and parses it into a formula tree, consisting of
+ * Reads a Prctl formula from its string representation and parses it into a formula tree, consisting of
* classes in the namespace storm::property.
*
* If the string could not be parsed successfully, it will throw a wrongFormatException.
*
* @param formulaString The string representation of the formula
* @throw wrongFormatException If the input could not be parsed successfully
- * @return A pointer to the parsed Prctl formula. If the line just contained a comment a nullptr will be returned instead.
+ * @return A PrctlFilter maintaining the parsed formula. If the line just contained a comment a nullptr will be returned instead.
*/
static std::shared_ptr<storm::property::prctl::PrctlFilter<double>> parsePrctlFormula(std::string formulaString);