From 535ae933b0eaa4c813a08e35c03dc782c3752afc Mon Sep 17 00:00:00 2001 From: Lanchid Date: Mon, 22 Apr 2013 14:37:41 +0200 Subject: [PATCH] Compiling implementation of LTL parser --- src/formula/Ltl.h | 10 +++++++--- src/formula/Ltl/AbstractLtlFormula.h | 5 +++-- src/formula/Ltl/Ap.h | 4 ++-- src/formula/Ltl/BoundedEventually.h | 6 +++--- src/formula/Ltl/BoundedUntil.h | 6 +++--- src/formula/Ltl/Eventually.h | 6 +++--- src/formula/Ltl/Globally.h | 6 +++--- src/formula/Ltl/Next.h | 6 +++--- src/formula/Ltl/Not.h | 5 ++--- src/formula/Ltl/Or.h | 6 +++--- src/formula/Ltl/Until.h | 6 +++--- 11 files changed, 35 insertions(+), 31 deletions(-) diff --git a/src/formula/Ltl.h b/src/formula/Ltl.h index e37aabeca..17a51d68b 100644 --- a/src/formula/Ltl.h +++ b/src/formula/Ltl.h @@ -5,8 +5,10 @@ * Author: thomas */ -#ifndef LTL_H_ -#define LTL_H_ +#ifndef STORM_FORMULA_LTL_H_ +#define STORM_FORMULA_LTL_H_ + +#include "src/modelchecker/ForwardDeclarations.h" #include "Ltl/And.h" #include "Ltl/Ap.h" @@ -19,4 +21,6 @@ #include "Ltl/Or.h" #include "Ltl/Until.h" -#endif /* LTL_H_ */ +#include "modelchecker/AbstractModelChecker.h" + +#endif /* STORM_FORMULA_LTL_H_ */ diff --git a/src/formula/Ltl/AbstractLtlFormula.h b/src/formula/Ltl/AbstractLtlFormula.h index 053f00d1f..eff27a0b6 100644 --- a/src/formula/Ltl/AbstractLtlFormula.h +++ b/src/formula/Ltl/AbstractLtlFormula.h @@ -10,13 +10,14 @@ #include #include "src/modelchecker/ForwardDeclarations.h" +#include "src/formula/abstract/AbstractFormula.h" namespace storm { namespace formula { namespace ltl { template -class AbstractLtlFormula { +class AbstractLtlFormula : public virtual storm::formula::abstract::AbstractFormula { public: /** * Empty destructor @@ -36,7 +37,7 @@ public: * * @returns A vector indicating the probability that the formula holds for each state. */ - virtual std::vector* check(const storm::modelchecker::AbstractModelChecker& modelChecker, bool qualitative) const = 0; + virtual std::vector* check(const storm::modelchecker::AbstractModelChecker& modelChecker) const = 0; /*! * Clones the called object. diff --git a/src/formula/Ltl/Ap.h b/src/formula/Ltl/Ap.h index 19372d771..508cc2823 100644 --- a/src/formula/Ltl/Ap.h +++ b/src/formula/Ltl/Ap.h @@ -76,8 +76,8 @@ public: * * @returns A vector indicating the probability that the formula holds for each state. */ - virtual std::vector* check(const storm::modelchecker::AbstractModelChecker& modelChecker, bool qualitative) const { - return modelChecker.template as>.check(*this); + virtual std::vector* check(const storm::modelchecker::AbstractModelChecker& modelChecker) const { + return modelChecker.template as()->checkAp(*this); } /*! diff --git a/src/formula/Ltl/BoundedEventually.h b/src/formula/Ltl/BoundedEventually.h index 4cf0ab0b9..48dfe3ecb 100644 --- a/src/formula/Ltl/BoundedEventually.h +++ b/src/formula/Ltl/BoundedEventually.h @@ -36,7 +36,7 @@ class IBoundedEventuallyModelChecker { * @param obj Formula object with subformulas. * @return Result of the formula for every node. */ - virtual std::vector* checkBoundedEventually(const BoundedEventually& obj, bool qualitative) const = 0; + virtual std::vector* checkBoundedEventually(const BoundedEventually& obj) const = 0; }; /*! @@ -113,8 +113,8 @@ public: * * @returns A vector indicating the probability that the formula holds for each state. */ - virtual std::vector* check(const storm::modelchecker::AbstractModelChecker& modelChecker, bool qualitative) const { - return modelChecker.template as()->checkBoundedEventually(*this, qualitative); + virtual std::vector* check(const storm::modelchecker::AbstractModelChecker& modelChecker) const { + return modelChecker.template as()->checkBoundedEventually(*this); } }; diff --git a/src/formula/Ltl/BoundedUntil.h b/src/formula/Ltl/BoundedUntil.h index f7ef572f9..1247fb352 100644 --- a/src/formula/Ltl/BoundedUntil.h +++ b/src/formula/Ltl/BoundedUntil.h @@ -35,7 +35,7 @@ class IBoundedUntilModelChecker { * @param obj Formula object with subformulas. * @return Result of the formula for every node. */ - virtual std::vector* checkBoundedUntil(const BoundedUntil& obj, bool qualitative) const = 0; + virtual std::vector* checkBoundedUntil(const BoundedUntil& obj) const = 0; }; /*! @@ -118,8 +118,8 @@ public: * * @returns A vector indicating the probability that the formula holds for each state. */ - virtual std::vector *check(const storm::modelchecker::AbstractModelChecker& modelChecker, bool qualitative) const { - return modelChecker.template as()->checkBoundedUntil(*this, qualitative); + virtual std::vector *check(const storm::modelchecker::AbstractModelChecker& modelChecker) const { + return modelChecker.template as()->checkBoundedUntil(*this); } }; diff --git a/src/formula/Ltl/Eventually.h b/src/formula/Ltl/Eventually.h index a9ffc21bd..6a29b6f9f 100644 --- a/src/formula/Ltl/Eventually.h +++ b/src/formula/Ltl/Eventually.h @@ -33,7 +33,7 @@ class IEventuallyModelChecker { * @param obj Formula object with subformulas. * @return Result of the formula for every node. */ - virtual std::vector* checkEventually(const Eventually& obj, bool qualitative) const = 0; + virtual std::vector* checkEventually(const Eventually& obj) const = 0; }; /*! @@ -107,8 +107,8 @@ public: * * @returns A vector indicating the probability that the formula holds for each state. */ - virtual std::vector *check(const storm::modelchecker::AbstractModelChecker& modelChecker, bool qualitative) const { - return modelChecker.template as()->checkEventually(*this, qualitative); + virtual std::vector *check(const storm::modelchecker::AbstractModelChecker& modelChecker) const { + return modelChecker.template as()->checkEventually(*this); } }; diff --git a/src/formula/Ltl/Globally.h b/src/formula/Ltl/Globally.h index 00a0f19dd..1982be5a1 100644 --- a/src/formula/Ltl/Globally.h +++ b/src/formula/Ltl/Globally.h @@ -34,7 +34,7 @@ class IGloballyModelChecker { * @param obj Formula object with subformulas. * @return Result of the formula for every node. */ - virtual std::vector* checkGlobally(const Globally& obj, bool qualitative) const = 0; + virtual std::vector* checkGlobally(const Globally& obj) const = 0; }; /*! @@ -109,8 +109,8 @@ public: * * @returns A vector indicating the probability that the formula holds for each state. */ - virtual std::vector *check(const storm::modelchecker::AbstractModelChecker& modelChecker, bool qualitative) const { - return modelChecker.template as()->checkGlobally(*this, qualitative); + virtual std::vector *check(const storm::modelchecker::AbstractModelChecker& modelChecker) const { + return modelChecker.template as()->checkGlobally(*this); } }; diff --git a/src/formula/Ltl/Next.h b/src/formula/Ltl/Next.h index 5bf50c9c2..a6df0c93d 100644 --- a/src/formula/Ltl/Next.h +++ b/src/formula/Ltl/Next.h @@ -33,7 +33,7 @@ class INextModelChecker { * @param obj Formula object with subformulas. * @return Result of the formula for every node. */ - virtual std::vector* checkNext(const Next& obj, bool qualitative) const = 0; + virtual std::vector* checkNext(const Next& obj) const = 0; }; /*! @@ -107,8 +107,8 @@ public: * * @returns A vector indicating the probability that the formula holds for each state. */ - virtual std::vector *check(const storm::modelchecker::AbstractModelChecker& modelChecker, bool qualitative) const { - return modelChecker.template as()->checkNext(*this, qualitative); + virtual std::vector *check(const storm::modelchecker::AbstractModelChecker& modelChecker) const { + return modelChecker.template as()->checkNext(*this); } }; diff --git a/src/formula/Ltl/Not.h b/src/formula/Ltl/Not.h index aee6197a2..42965c907 100644 --- a/src/formula/Ltl/Not.h +++ b/src/formula/Ltl/Not.h @@ -11,7 +11,6 @@ #include "AbstractLtlFormula.h" #include "src/formula/abstract/Not.h" #include "src/formula/AbstractFormulaChecker.h" -#include "src/modelchecker/ForwardDeclarations.h" namespace storm { namespace formula { @@ -104,8 +103,8 @@ public: * * @returns A bit vector indicating all states that satisfy the formula represented by the called object. */ - virtual std::vector *check(const storm::modelchecker::AbstractModelChecker& modelChecker) const { - return modelChecker.template as()->checkNot(*this); + virtual std::vector* check(const storm::modelchecker::AbstractModelChecker& modelChecker) const { + return modelChecker.template as()->checkNot(*this); } }; diff --git a/src/formula/Ltl/Or.h b/src/formula/Ltl/Or.h index 99d687c16..d8f1b965c 100644 --- a/src/formula/Ltl/Or.h +++ b/src/formula/Ltl/Or.h @@ -15,7 +15,7 @@ namespace storm { namespace formula { namespace ltl { -template class And; +template class Or; /*! * @brief Interface class for model checkers that support And. @@ -32,7 +32,7 @@ class IOrModelChecker { * @param obj Formula object with subformulas. * @return Result of the formula for every node. */ - virtual std::vector* checkOr(const And& obj) const = 0; + virtual std::vector* checkOr(const Or& obj) const = 0; }; template @@ -54,7 +54,7 @@ public: * @param left The left subformula * @param right The right subformula */ - Or(AbstractLtlFormula left, AbstractLtlFormula right) + Or(AbstractLtlFormula* left, AbstractLtlFormula* right) : storm::formula::abstract::Or>(left, right) { // Intentionally left empty } diff --git a/src/formula/Ltl/Until.h b/src/formula/Ltl/Until.h index d3a1120d7..502401f25 100644 --- a/src/formula/Ltl/Until.h +++ b/src/formula/Ltl/Until.h @@ -33,7 +33,7 @@ class IUntilModelChecker { * @param obj Formula object with subformulas. * @return Result of the formula for every node. */ - virtual std::vector* checkUntil(const Until& obj, bool qualitative) const = 0; + virtual std::vector* checkUntil(const Until& obj) const = 0; }; /*! @@ -112,8 +112,8 @@ public: * * @returns A vector indicating the probability that the formula holds for each state. */ - virtual std::vector *check(const storm::modelchecker::AbstractModelChecker& modelChecker, bool qualitative) const { - return modelChecker.template as()->checkUntil(*this, qualitative); + virtual std::vector *check(const storm::modelchecker::AbstractModelChecker& modelChecker) const { + return modelChecker.template as()->checkUntil(*this); } };