diff --git a/src/formula/AbstractFormulaChecker.h b/src/formula/AbstractFormulaChecker.h
index f675a319f..6e74c48a4 100644
--- a/src/formula/AbstractFormulaChecker.h
+++ b/src/formula/AbstractFormulaChecker.h
@@ -19,13 +19,13 @@ namespace formula {
*
* Usually, this will be implemented like this:
* @code
- * if (
+ * if (
* dynamic_cast<const And<T>*>(formula) ||
* dynamic_cast<const Not<T>*>(formula) ||
* dynamic_cast<const Or<T>*>(formula)
* ) {
* return formula->conforms(*this);
- * } else return false;
+ * } else return false;
* @endcode
*
* Every formula class implements a conforms() method itself which calls
diff --git a/src/formula/InstantaneousReward.h b/src/formula/InstantaneousReward.h
index 3ab36c584..8f55b2c7c 100644
--- a/src/formula/InstantaneousReward.h
+++ b/src/formula/InstantaneousReward.h
@@ -20,9 +20,21 @@ namespace formula {
template <class T> class InstantaneousReward;
+/*!
+ * @brief Interface class for model checkers that support InstantaneousReward.
+ *
+ * All model checkers that support the formula class InstantaneousReward must inherit
+ * this pure virtual class.
+ */
template <class T>
class IInstantaneousRewardModelChecker {
public:
+ /*!
+ * @brief Evaluates InstantaneousReward formula within a model checker.
+ *
+ * @param obj Formula object with subformulas.
+ * @return Result of the formula for every node.
+ */
virtual std::vector<T>* checkInstantaneousReward(const InstantaneousReward<T>& obj) const = 0;
};
@@ -113,6 +125,14 @@ public:
return modelChecker.template as<IInstantaneousRewardModelChecker>()->checkInstantaneousReward(*this);
}
+ /*!
+ * @brief Checks if all subtrees conform to some logic.
+ *
+ * As InstantaneousReward formulas have no subformulas, we return true here.
+ *
+ * @param checker Formula checker object.
+ * @return true
+ */
virtual bool conforms(const AbstractFormulaChecker<T>& checker) const {
return true;
}
diff --git a/src/formula/Next.h b/src/formula/Next.h
index 8884ac5b6..a91a39ce1 100644
--- a/src/formula/Next.h
+++ b/src/formula/Next.h
@@ -18,9 +18,21 @@ namespace formula {
template <class T> class Next;
+/*!
+ * @brief Interface class for model checkers that support Next.
+ *
+ * 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.
+ */
virtual std::vector<T>* checkNext(const Next<T>& obj) const = 0;
};
@@ -125,6 +137,12 @@ public:
return modelChecker.template as<INextModelChecker>()->checkNext(*this);
}
+ /*!
+ * @brief Checks if the subtree conforms to some logic.
+ *
+ * @param checker Formula checker object.
+ * @return true iff the subtree conforms to some logic.
+ */
virtual bool conforms(const AbstractFormulaChecker<T>& checker) const {
return checker.conforms(this->child);
}
diff --git a/src/formula/NoBoundOperator.h b/src/formula/NoBoundOperator.h
index c7a14d155..4a459c5e8 100644
--- a/src/formula/NoBoundOperator.h
+++ b/src/formula/NoBoundOperator.h
@@ -18,9 +18,21 @@ namespace formula {
template <class T> class NoBoundOperator;
+/*!
+ * @brief Interface class for model checkers that support NoBoundOperator.
+ *
+ * All model checkers that support the formula class NoBoundOperator must inherit
+ * this pure virtual class.
+ */
template <class T>
class INoBoundOperatorModelChecker {
public:
+ /*!
+ * @brief Evaluates NoBoundOperator formula within a model checker.
+ *
+ * @param obj Formula object with subformulas.
+ * @return Result of the formula for every node.
+ */
virtual std::vector<T>* checkNoBoundOperator(const NoBoundOperator<T>& obj) const = 0;
};
@@ -118,6 +130,12 @@ public:
*/
virtual std::string toString() const = 0;
+ /*!
+ * @brief Checks if the subtree conforms to some logic.
+ *
+ * @param checker Formula checker object.
+ * @return true iff the subtree conforms to some logic.
+ */
virtual bool conforms(const AbstractFormulaChecker<T>& checker) const {
return checker.conforms(this->pathFormula);
}
diff --git a/src/formula/Not.h b/src/formula/Not.h
index 56eaf6c6a..cd7a20399 100644
--- a/src/formula/Not.h
+++ b/src/formula/Not.h
@@ -18,9 +18,21 @@ namespace formula {
template <class T> class Not;
+/*!
+ * @brief Interface class for model checkers that support Not.
+ *
+ * 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.
+ */
virtual storm::storage::BitVector* checkNot(const Not<T>& obj) const = 0;
};
@@ -119,6 +131,12 @@ public:
return modelChecker.template as<INotModelChecker>()->checkNot(*this);
}
+ /*!
+ * @brief Checks if the subtree conforms to some logic.
+ *
+ * @param checker Formula checker object.
+ * @return true iff the subtree conforms to some logic.
+ */
virtual bool conforms(const AbstractFormulaChecker<T>& checker) const {
return checker.conforms(this->child);
}
diff --git a/src/formula/Or.h b/src/formula/Or.h
index 6a071f395..e7dd117e5 100644
--- a/src/formula/Or.h
+++ b/src/formula/Or.h
@@ -16,9 +16,21 @@ namespace formula {
template <class T> class Or;
+/*!
+ * @brief Interface class for model checkers that support Or.
+ *
+ * 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.
+ */
virtual storm::storage::BitVector* checkOr(const Or<T>& obj) const = 0;
};
@@ -152,6 +164,12 @@ public:
return modelChecker.template as<IOrModelChecker>()->checkOr(*this);
}
+ /*!
+ * @brief Checks if all subtrees conform to some logic.
+ *
+ * @param checker Formula checker object.
+ * @return true iff all subtrees conform to some logic.
+ */
virtual bool conforms(const AbstractFormulaChecker<T>& checker) const {
return checker.conforms(this->left) && checker.conforms(this->right);
}
diff --git a/src/formula/PrctlFormulaChecker.h b/src/formula/PrctlFormulaChecker.h
index 2a8d882e7..e99cb0666 100644
--- a/src/formula/PrctlFormulaChecker.h
+++ b/src/formula/PrctlFormulaChecker.h
@@ -9,9 +9,22 @@
namespace storm {
namespace formula {
+/*!
+ * @brief Checks formulas if they are within PRCTL.
+ *
+ * This class implements AbstractFormulaChecker to check if a given formula
+ * is part of PRCTL logic.
+ */
template <class T>
class PrctlFormulaChecker : public AbstractFormulaChecker<T> {
public:
+ /*!
+ * Implementation of AbstractFormulaChecker::conforms() using code
+ * looking exactly like the sample code given there.
+ *
+ * We currently allow And, Ap, Eventually, Not, Or,
+ * ProbabilisticNoBoundOperator.
+ */
virtual bool conforms(const AbstractFormula<T>* formula) const {
if (
dynamic_cast<const And<T>*>(formula) ||
@@ -25,11 +38,9 @@ class PrctlFormulaChecker : public AbstractFormulaChecker<T> {
}
return false;
}
-
- private:
};
-}
-}
+} // namespace formula
+} // namespace storm
#endif
\ No newline at end of file
diff --git a/src/formula/ProbabilisticBoundOperator.h b/src/formula/ProbabilisticBoundOperator.h
index 3e6e7fde6..5ac0ff606 100644
--- a/src/formula/ProbabilisticBoundOperator.h
+++ b/src/formula/ProbabilisticBoundOperator.h
@@ -14,7 +14,6 @@
#include "utility/ConstTemplates.h"
namespace storm {
-
namespace formula {
/*!
@@ -92,7 +91,6 @@ public:
};
} //namespace formula
-
} //namespace storm
#endif /* STORM_FORMULA_PROBABILISTICBOUNDOPERATOR_H_ */
diff --git a/src/formula/ProbabilisticNoBoundOperator.h b/src/formula/ProbabilisticNoBoundOperator.h
index bfe6f92db..07e79659c 100644
--- a/src/formula/ProbabilisticNoBoundOperator.h
+++ b/src/formula/ProbabilisticNoBoundOperator.h
@@ -13,7 +13,6 @@
#include "NoBoundOperator.h"
namespace storm {
-
namespace formula {
/*!
@@ -77,7 +76,6 @@ public:
};
} /* namespace formula */
-
} /* namespace storm */
#endif /* STORM_FORMULA_PROBABILISTICNOBOUNDOPERATOR_H_ */
diff --git a/src/formula/ReachabilityReward.h b/src/formula/ReachabilityReward.h
index cef56ab6d..54e2f447b 100644
--- a/src/formula/ReachabilityReward.h
+++ b/src/formula/ReachabilityReward.h
@@ -14,14 +14,25 @@
#include "src/modelChecker/AbstractModelChecker.h"
namespace storm {
-
namespace formula {
template <class T> class ReachabilityReward;
+/*!
+ * @brief Interface class for model checkers that support ReachabilityReward.
+ *
+ * All model checkers that support the formula class ReachabilityReward must inherit
+ * this pure virtual class.
+ */
template <class T>
class IReachabilityRewardModelChecker {
public:
+ /*!
+ * @brief Evaluates ReachabilityReward formula within a model checker.
+ *
+ * @param obj Formula object with subformulas.
+ * @return Result of the formula for every node.
+ */
virtual std::vector<T>* checkReachabilityReward(const ReachabilityReward<T>& obj) const = 0;
};
@@ -121,6 +132,12 @@ public:
return modelChecker.template as<IReachabilityRewardModelChecker>()->checkReachabilityReward(*this);
}
+ /*!
+ * @brief Checks if the subtree conforms to some logic.
+ *
+ * @param checker Formula checker object.
+ * @return true iff the subtree conforms to some logic.
+ */
virtual bool conforms(const AbstractFormulaChecker<T>& checker) const {
return checker.conforms(this->child);
}
@@ -130,7 +147,6 @@ private:
};
} //namespace formula
-
} //namespace storm
#endif /* STORM_FORMULA_REACHABILITYREWARD_H_ */
diff --git a/src/formula/RewardBoundOperator.h b/src/formula/RewardBoundOperator.h
index b2c6065ff..3f30ec0c7 100644
--- a/src/formula/RewardBoundOperator.h
+++ b/src/formula/RewardBoundOperator.h
@@ -14,7 +14,6 @@
#include "utility/ConstTemplates.h"
namespace storm {
-
namespace formula {
/*!
@@ -90,7 +89,6 @@ public:
};
} //namespace formula
-
} //namespace storm
#endif /* STORM_FORMULA_REWARDBOUNDOPERATOR_H_ */
diff --git a/src/formula/RewardNoBoundOperator.h b/src/formula/RewardNoBoundOperator.h
index 3752b381a..f362a5232 100644
--- a/src/formula/RewardNoBoundOperator.h
+++ b/src/formula/RewardNoBoundOperator.h
@@ -13,7 +13,6 @@
#include "NoBoundOperator.h"
namespace storm {
-
namespace formula {
/*!
@@ -77,7 +76,6 @@ public:
};
} /* namespace formula */
-
} /* namespace storm */
#endif /* STORM_FORMULA_REWARDNOBOUNDOPERATOR_H_ */
diff --git a/src/formula/Until.h b/src/formula/Until.h
index cfc186f56..82ac05c9d 100644
--- a/src/formula/Until.h
+++ b/src/formula/Until.h
@@ -13,14 +13,25 @@
#include "src/formula/AbstractFormulaChecker.h"
namespace storm {
-
namespace formula {
template <class T> class Until;
+/*!
+ * @brief Interface class for model checkers that support Until.
+ *
+ * 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;
};
@@ -153,6 +164,12 @@ public:
return modelChecker.template as<IUntilModelChecker>()->checkUntil(*this);
}
+ /*!
+ * @brief Checks if all subtrees conform to some logic.
+ *
+ * @param checker Formula checker object.
+ * @return true iff all subtrees conform to some logic.
+ */
virtual bool conforms(const AbstractFormulaChecker<T>& checker) const {
return checker.conforms(this->left) && checker.conforms(this->right);
}