diff --git a/src/formula/ComparisonType.h b/src/formula/ComparisonType.h index fc41540d1..98ee80373 100644 --- a/src/formula/ComparisonType.h +++ b/src/formula/ComparisonType.h @@ -2,7 +2,7 @@ * ComparisonType.h * * Created on: 17.04.2013 - * Author: thomas + * Author: Thomas Heinemann */ #ifndef STORM_FORMULA_COMPARISONTYPE_H_ diff --git a/src/formula/Csl.h b/src/formula/Csl.h index b9724eab3..a6a6c4e67 100644 --- a/src/formula/Csl.h +++ b/src/formula/Csl.h @@ -2,7 +2,7 @@ * Csl.h * * Created on: 19.04.2013 - * Author: thomas + * Author: Thomas Heinemann */ #ifndef STORM_FORMULA_CSL_H_ @@ -28,5 +28,4 @@ #include "modelchecker/csl/AbstractModelChecker.h" - #endif /* STORM_FORMULA_CSL_H_ */ diff --git a/src/formula/Csl/AbstractCslFormula.h b/src/formula/Csl/AbstractCslFormula.h index 0770c1cd7..1c8503180 100644 --- a/src/formula/Csl/AbstractCslFormula.h +++ b/src/formula/Csl/AbstractCslFormula.h @@ -25,13 +25,6 @@ public: } }; -/*! - * @brief An encapsulation type for the Return Type of the CslParser. As a pure virtual Class can not be an r-value return type, it has to be encapsulated. - * @see CslParser - */ -template -using AbstractCslFormularRef_t = std::reference_wrapper>; - } /* namespace csl */ } /* namespace property */ } /* namespace storm */ diff --git a/src/formula/Csl/And.h b/src/formula/Csl/And.h index ebaf0fe9f..f5bfe4eff 100644 --- a/src/formula/Csl/And.h +++ b/src/formula/Csl/And.h @@ -94,7 +94,7 @@ public: * * @returns a new AND-object that is identical the called object. */ - virtual AbstractStateFormula* clone() const { + virtual AbstractStateFormula* clone() const override { And* result = new And(); if (this->leftIsSet()) { result->setLeft(this->getLeft().clone()); @@ -114,7 +114,7 @@ public: * * @returns A bit vector indicating all states that satisfy the formula represented by the called object. */ - virtual storm::storage::BitVector* check(const storm::modelchecker::csl::AbstractModelChecker& modelChecker) const { + virtual storm::storage::BitVector* check(const storm::modelchecker::csl::AbstractModelChecker& modelChecker) const override { return modelChecker.template as()->checkAnd(*this); } diff --git a/src/formula/Csl/Ap.h b/src/formula/Csl/Ap.h index cc0cad9e3..d04ab56f4 100644 --- a/src/formula/Csl/Ap.h +++ b/src/formula/Csl/Ap.h @@ -78,7 +78,7 @@ public: * * @returns a new AND-object that is identical the called object. */ - virtual AbstractStateFormula* clone() const { + virtual AbstractStateFormula* clone() const override { return new Ap(this->getAp()); } @@ -91,7 +91,7 @@ public: * * @returns A bit vector indicating all states that satisfy the formula represented by the called object. */ - virtual storm::storage::BitVector *check(const storm::modelchecker::csl::AbstractModelChecker& modelChecker) const { + virtual storm::storage::BitVector *check(const storm::modelchecker::csl::AbstractModelChecker& modelChecker) const override { return modelChecker.template as()->checkAp(*this); } diff --git a/src/formula/Csl/Eventually.h b/src/formula/Csl/Eventually.h index d4dd43030..9ef900fca 100644 --- a/src/formula/Csl/Eventually.h +++ b/src/formula/Csl/Eventually.h @@ -91,7 +91,7 @@ public: * * @returns a new Eventually-object that is identical the called object. */ - virtual AbstractPathFormula* clone() const { + virtual AbstractPathFormula* clone() const override { Eventually* result = new Eventually(); if (this->childIsSet()) { result->setChild(this->getChild().clone()); @@ -108,7 +108,7 @@ public: * * @returns A vector indicating the probability that the formula holds for each state. */ - virtual std::vector *check(const storm::modelchecker::csl::AbstractModelChecker& modelChecker, bool qualitative) const { + virtual std::vector *check(const storm::modelchecker::csl::AbstractModelChecker& modelChecker, bool qualitative) const override { return modelChecker.template as()->checkEventually(*this, qualitative); } }; diff --git a/src/formula/Csl/Globally.h b/src/formula/Csl/Globally.h index 7bc209d25..7a17677bf 100644 --- a/src/formula/Csl/Globally.h +++ b/src/formula/Csl/Globally.h @@ -93,7 +93,7 @@ public: * * @returns a new Globally-object that is identical the called object. */ - virtual AbstractPathFormula* clone() const { + virtual AbstractPathFormula* clone() const override { Globally* result = new Globally(); if (this->childIsSet()) { result->setChild(this->getChild().clone()); @@ -110,7 +110,7 @@ public: * * @returns A vector indicating the probability that the formula holds for each state. */ - virtual std::vector *check(const storm::modelchecker::csl::AbstractModelChecker& modelChecker, bool qualitative) const { + virtual std::vector *check(const storm::modelchecker::csl::AbstractModelChecker& modelChecker, bool qualitative) const override { return modelChecker.template as()->checkGlobally(*this, qualitative); } }; diff --git a/src/formula/Csl/Next.h b/src/formula/Csl/Next.h index c37a8165b..48b00b7d8 100644 --- a/src/formula/Csl/Next.h +++ b/src/formula/Csl/Next.h @@ -91,7 +91,7 @@ public: * * @returns a new BoundedUntil-object that is identical the called object. */ - virtual AbstractPathFormula* clone() const { + virtual AbstractPathFormula* clone() const override { Next* result = new Next(); if (this->childIsSet()) { result->setChild(this->getChild().clone()); @@ -108,7 +108,7 @@ public: * * @returns A vector indicating the probability that the formula holds for each state. */ - virtual std::vector *check(const storm::modelchecker::csl::AbstractModelChecker& modelChecker, bool qualitative) const { + virtual std::vector *check(const storm::modelchecker::csl::AbstractModelChecker& modelChecker, bool qualitative) const override { return modelChecker.template as()->checkNext(*this, qualitative); } }; diff --git a/src/formula/Csl/Not.h b/src/formula/Csl/Not.h index 0f77142ae..413ba49ed 100644 --- a/src/formula/Csl/Not.h +++ b/src/formula/Csl/Not.h @@ -87,7 +87,7 @@ public: * * @returns a new AND-object that is identical the called object. */ - virtual AbstractStateFormula* clone() const { + virtual AbstractStateFormula* clone() const override { Not* result = new Not(); if (this->childIsSet()) { result->setChild(this->getChild().clone()); @@ -104,7 +104,7 @@ public: * * @returns A bit vector indicating all states that satisfy the formula represented by the called object. */ - virtual storm::storage::BitVector *check(const storm::modelchecker::csl::AbstractModelChecker& modelChecker) const { + virtual storm::storage::BitVector *check(const storm::modelchecker::csl::AbstractModelChecker& modelChecker) const override { return modelChecker.template as()->checkNot(*this); } }; diff --git a/src/formula/Csl/Or.h b/src/formula/Csl/Or.h index edc1fd697..bf7f48de1 100644 --- a/src/formula/Csl/Or.h +++ b/src/formula/Csl/Or.h @@ -93,7 +93,7 @@ public: * * @returns a new AND-object that is identical the called object. */ - virtual AbstractStateFormula* clone() const { + virtual AbstractStateFormula* clone() const override { Or* result = new Or(); if (this->leftIsSet()) { result->setLeft(this->getLeft().clone()); @@ -113,7 +113,7 @@ public: * * @returns A bit vector indicating all states that satisfy the formula represented by the called object. */ - virtual storm::storage::BitVector *check(const storm::modelchecker::csl::AbstractModelChecker& modelChecker) const { + virtual storm::storage::BitVector *check(const storm::modelchecker::csl::AbstractModelChecker& modelChecker) const override { return modelChecker.template as()->checkOr(*this); } }; diff --git a/src/formula/Csl/ProbabilisticBoundOperator.h b/src/formula/Csl/ProbabilisticBoundOperator.h index 48db99b44..d4e4f7326 100644 --- a/src/formula/Csl/ProbabilisticBoundOperator.h +++ b/src/formula/Csl/ProbabilisticBoundOperator.h @@ -92,7 +92,7 @@ public: * * @returns a new AND-object that is identical the called object. */ - virtual AbstractStateFormula* clone() const { + virtual AbstractStateFormula* clone() const override { ProbabilisticBoundOperator* result = new ProbabilisticBoundOperator(); result->setComparisonOperator(this->getComparisonOperator()); result->setBound(this->getBound()); @@ -109,7 +109,7 @@ public: * * @returns A bit vector indicating all states that satisfy the formula represented by the called object. */ - virtual storm::storage::BitVector* check(const storm::modelchecker::csl::AbstractModelChecker& modelChecker) const { + virtual storm::storage::BitVector* check(const storm::modelchecker::csl::AbstractModelChecker& modelChecker) const override { return modelChecker.template as()->checkProbabilisticBoundOperator(*this); } }; diff --git a/src/formula/Csl/ProbabilisticNoBoundOperator.h b/src/formula/Csl/ProbabilisticNoBoundOperator.h index 4eb1a227e..41e0bcf64 100644 --- a/src/formula/Csl/ProbabilisticNoBoundOperator.h +++ b/src/formula/Csl/ProbabilisticNoBoundOperator.h @@ -84,7 +84,7 @@ public: // Intentionally left empty } - virtual AbstractNoBoundOperator* clone() const { + virtual AbstractNoBoundOperator* clone() const override { ProbabilisticNoBoundOperator* result = new ProbabilisticNoBoundOperator(); if (this->pathFormulaIsSet()) { result->setPathFormula(this->getPathFormula().clone()); @@ -103,7 +103,7 @@ public: * * @returns A vector indicating the probability that the formula holds for each state. */ - virtual std::vector* check(const storm::modelchecker::csl::AbstractModelChecker& modelChecker, bool qualitative=false) const { + virtual std::vector* check(const storm::modelchecker::csl::AbstractModelChecker& modelChecker, bool qualitative=false) const override { return this->getPathFormula().check(modelChecker, qualitative); } }; diff --git a/src/formula/Csl/SteadyStateBoundOperator.h b/src/formula/Csl/SteadyStateBoundOperator.h index e9ac6a3e5..5120b632c 100644 --- a/src/formula/Csl/SteadyStateBoundOperator.h +++ b/src/formula/Csl/SteadyStateBoundOperator.h @@ -90,7 +90,7 @@ public: * * @returns a new BoundedUntil-object that is identical the called object. */ - virtual AbstractStateFormula* clone() const { + virtual AbstractStateFormula* clone() const override { SteadyStateBoundOperator* result = new SteadyStateBoundOperator(); result->setStateFormula(this->getStateFormula().clone()); return result; @@ -105,7 +105,7 @@ public: * * @returns A vector indicating the probability that the formula holds for each state. */ - virtual storm::storage::BitVector* check(const storm::modelchecker::csl::AbstractModelChecker& modelChecker) const { + virtual storm::storage::BitVector* check(const storm::modelchecker::csl::AbstractModelChecker& modelChecker) const override { return modelChecker.template as()->checkSteadyStateBoundOperator(*this); } diff --git a/src/formula/Csl/SteadyStateNoBoundOperator.h b/src/formula/Csl/SteadyStateNoBoundOperator.h index 51c407d02..47485256d 100644 --- a/src/formula/Csl/SteadyStateNoBoundOperator.h +++ b/src/formula/Csl/SteadyStateNoBoundOperator.h @@ -72,7 +72,7 @@ public: * * @returns a new BoundedUntil-object that is identical the called object. */ - virtual AbstractNoBoundOperator * clone() const { + virtual AbstractNoBoundOperator * clone() const override { SteadyStateNoBoundOperator* result = new SteadyStateNoBoundOperator(); result->setStateFormula(this->getStateFormula().clone()); return result; @@ -87,7 +87,7 @@ public: * * @returns A vector indicating the probability that the formula holds for each state. */ - virtual std::vector* check(const storm::modelchecker::csl::AbstractModelChecker& modelChecker, bool qualitative=false) const { + virtual std::vector* check(const storm::modelchecker::csl::AbstractModelChecker& modelChecker, bool qualitative=false) const override { return modelChecker.template as()->checkSteadyStateNoBoundOperator(*this); } diff --git a/src/formula/Csl/TimeBoundedEventually.h b/src/formula/Csl/TimeBoundedEventually.h index 06c03b49c..edce482d9 100644 --- a/src/formula/Csl/TimeBoundedEventually.h +++ b/src/formula/Csl/TimeBoundedEventually.h @@ -68,7 +68,7 @@ public: * * @returns a new BoundedUntil-object that is identical the called object. */ - virtual AbstractPathFormula* clone() const { + virtual AbstractPathFormula* clone() const override { TimeBoundedEventually* result = new TimeBoundedEventually(this->getLowerBound(), this->getUpperBound()); if (this->childIsSet()) { result->setChild(this->getChild().clone()); @@ -85,7 +85,7 @@ public: * * @returns A vector indicating the probability that the formula holds for each state. */ - virtual std::vector* check(const storm::modelchecker::csl::AbstractModelChecker& modelChecker, bool qualitative) const { + virtual std::vector* check(const storm::modelchecker::csl::AbstractModelChecker& modelChecker, bool qualitative) const override { return modelChecker.template as()->checkTimeBoundedEventually(*this, qualitative); } }; diff --git a/src/formula/Csl/TimeBoundedUntil.h b/src/formula/Csl/TimeBoundedUntil.h index 4249888f0..54a660169 100644 --- a/src/formula/Csl/TimeBoundedUntil.h +++ b/src/formula/Csl/TimeBoundedUntil.h @@ -78,7 +78,7 @@ public: * * @returns a new BoundedUntil-object that is identical the called object. */ - virtual AbstractPathFormula* clone() const { + virtual AbstractPathFormula* clone() const override { TimeBoundedUntil* result = new TimeBoundedUntil(this->getLowerBound(), this->getUpperBound()); if (this->leftIsSet()) { result->setLeft(this->getLeft().clone()); @@ -99,7 +99,7 @@ public: * * @returns A vector indicating the probability that the formula holds for each state. */ - virtual std::vector* check(const storm::modelchecker::csl::AbstractModelChecker& modelChecker, bool qualitative) const { + virtual std::vector* check(const storm::modelchecker::csl::AbstractModelChecker& modelChecker, bool qualitative) const override { return modelChecker.template as()->checkTimeBoundedUntil(*this, qualitative); } }; diff --git a/src/formula/Csl/Until.h b/src/formula/Csl/Until.h index defd1e35b..7bcb32b08 100644 --- a/src/formula/Csl/Until.h +++ b/src/formula/Csl/Until.h @@ -93,7 +93,7 @@ public: * * @returns a new BoundedUntil-object that is identical the called object. */ - virtual AbstractPathFormula* clone() const { + virtual AbstractPathFormula* clone() const override { Until* result = new Until(); if (this->leftIsSet()) { result->setLeft(this->getLeft().clone()); @@ -113,7 +113,7 @@ public: * * @returns A vector indicating the probability that the formula holds for each state. */ - virtual std::vector *check(const storm::modelchecker::csl::AbstractModelChecker& modelChecker, bool qualitative) const { + virtual std::vector *check(const storm::modelchecker::csl::AbstractModelChecker& modelChecker, bool qualitative) const override { return modelChecker.template as()->checkUntil(*this, qualitative); } }; diff --git a/src/formula/Ltl.h b/src/formula/Ltl.h index 63569ea79..cac53a8be 100644 --- a/src/formula/Ltl.h +++ b/src/formula/Ltl.h @@ -2,7 +2,7 @@ * Ltl.h * * Created on: 22.04.2013 - * Author: thomas + * Author: Thomas Heinemann */ #ifndef STORM_FORMULA_LTL_H_ diff --git a/src/formula/Ltl/AbstractLtlFormula.h b/src/formula/Ltl/AbstractLtlFormula.h index 1d275a464..8286f75db 100644 --- a/src/formula/Ltl/AbstractLtlFormula.h +++ b/src/formula/Ltl/AbstractLtlFormula.h @@ -82,9 +82,6 @@ public: virtual void visit(visitor::AbstractLtlFormulaVisitor& visitor) const = 0; }; -template -using AbstractLtlFormularSharedPtr_t = std::shared_ptr; - } /* namespace ltl */ } /* namespace property */ } /* namespace storm */ diff --git a/src/formula/Ltl/And.h b/src/formula/Ltl/And.h index c2a43e920..800476e5f 100644 --- a/src/formula/Ltl/And.h +++ b/src/formula/Ltl/And.h @@ -111,7 +111,7 @@ public: * * @returns a new AND-object that is identical the called object. */ - virtual AbstractLtlFormula* clone() const { + virtual AbstractLtlFormula* clone() const override { And* result = new And(); if (this->leftIsSet()) { result->setLeft(this->getLeft().clone()); @@ -131,7 +131,7 @@ public: * * @returns A bit vector indicating all states that satisfy the formula represented by the called object. */ - virtual std::vector* check(const storm::modelchecker::ltl::AbstractModelChecker& modelChecker) const { + virtual std::vector* check(const storm::modelchecker::ltl::AbstractModelChecker& modelChecker) const override { return modelChecker.template as()->checkAnd(*this); } diff --git a/src/formula/Ltl/Ap.h b/src/formula/Ltl/Ap.h index 5dd9004cd..4e81a967c 100644 --- a/src/formula/Ltl/Ap.h +++ b/src/formula/Ltl/Ap.h @@ -103,7 +103,7 @@ public: * * @returns A vector indicating the probability that the formula holds for each state. */ - virtual std::vector* check(const storm::modelchecker::ltl::AbstractModelChecker& modelChecker) const { + virtual std::vector* check(const storm::modelchecker::ltl::AbstractModelChecker& modelChecker) const override { return modelChecker.template as()->checkAp(*this); } @@ -114,7 +114,7 @@ public: * * @returns a new AND-object that is identical the called object. */ - virtual AbstractLtlFormula* clone() const { + virtual AbstractLtlFormula* clone() const override { return new Ap(this->getAp()); } diff --git a/src/formula/Ltl/BoundedEventually.h b/src/formula/Ltl/BoundedEventually.h index 6978bfb45..4f1d269db 100644 --- a/src/formula/Ltl/BoundedEventually.h +++ b/src/formula/Ltl/BoundedEventually.h @@ -111,7 +111,7 @@ public: * * @returns a new BoundedUntil-object that is identical the called object. */ - virtual AbstractLtlFormula* clone() const { + virtual AbstractLtlFormula* clone() const override { BoundedEventually* result = new BoundedEventually(); result->setBound(this->getBound()); if (this->childIsSet()) { @@ -130,7 +130,7 @@ public: * * @returns A vector indicating the probability that the formula holds for each state. */ - virtual std::vector* check(const storm::modelchecker::ltl::AbstractModelChecker& modelChecker) const { + virtual std::vector* check(const storm::modelchecker::ltl::AbstractModelChecker& modelChecker) const override { return modelChecker.template as()->checkBoundedEventually(*this); } diff --git a/src/formula/Ltl/BoundedUntil.h b/src/formula/Ltl/BoundedUntil.h index 334081145..4b0dea92b 100644 --- a/src/formula/Ltl/BoundedUntil.h +++ b/src/formula/Ltl/BoundedUntil.h @@ -125,7 +125,7 @@ public: * * @returns a new BoundedUntil-object that is identical the called object. */ - virtual AbstractLtlFormula* clone() const { + virtual AbstractLtlFormula* clone() const override { BoundedUntil* result = new BoundedUntil(); result->setBound(this->getBound()); if (this->leftIsSet()) { diff --git a/src/formula/Ltl/Eventually.h b/src/formula/Ltl/Eventually.h index 2fe7bfb97..8436b0893 100644 --- a/src/formula/Ltl/Eventually.h +++ b/src/formula/Ltl/Eventually.h @@ -107,7 +107,7 @@ public: * * @returns a new Eventually-object that is identical the called object. */ - virtual AbstractLtlFormula* clone() const { + virtual AbstractLtlFormula* clone() const override { Eventually* result = new Eventually(); if (this->childIsSet()) { result->setChild(this->getChild().clone()); diff --git a/src/formula/Ltl/Globally.h b/src/formula/Ltl/Globally.h index 4d15fe92d..d4e544db6 100644 --- a/src/formula/Ltl/Globally.h +++ b/src/formula/Ltl/Globally.h @@ -109,7 +109,7 @@ public: * * @returns a new Globally-object that is identical the called object. */ - virtual AbstractLtlFormula* clone() const { + virtual AbstractLtlFormula* clone() const override { Globally* result = new Globally(); if (this->childIsSet()) { result->setChild(this->getChild().clone()); diff --git a/src/formula/Ltl/Next.h b/src/formula/Ltl/Next.h index a17af9dbf..38dc10e0d 100644 --- a/src/formula/Ltl/Next.h +++ b/src/formula/Ltl/Next.h @@ -107,7 +107,7 @@ public: * * @returns a new BoundedUntil-object that is identical the called object. */ - virtual AbstractLtlFormula* clone() const { + virtual AbstractLtlFormula* clone() const override { Next* result = new Next(); if (this->childIsSet()) { result->setChild(this->getChild().clone()); diff --git a/src/formula/Ltl/Not.h b/src/formula/Ltl/Not.h index ea0cb737c..d53c2349e 100644 --- a/src/formula/Ltl/Not.h +++ b/src/formula/Ltl/Not.h @@ -103,7 +103,7 @@ public: * * @returns a new AND-object that is identical the called object. */ - virtual AbstractLtlFormula* clone() const { + virtual AbstractLtlFormula* clone() const override { Not* result = new Not(); if (this->childIsSet()) { result->setChild(this->getChild().clone()); @@ -120,7 +120,7 @@ public: * * @returns A bit vector indicating all states that satisfy the formula represented by the called object. */ - virtual std::vector* check(const storm::modelchecker::ltl::AbstractModelChecker& modelChecker) const { + virtual std::vector* check(const storm::modelchecker::ltl::AbstractModelChecker& modelChecker) const override { return modelChecker.template as()->checkNot(*this); } diff --git a/src/formula/Ltl/Or.h b/src/formula/Ltl/Or.h index 33628b388..4196769bb 100644 --- a/src/formula/Ltl/Or.h +++ b/src/formula/Ltl/Or.h @@ -105,7 +105,7 @@ public: * * @returns a new AND-object that is identical the called object. */ - virtual AbstractLtlFormula* clone() const { + virtual AbstractLtlFormula* clone() const override { Or* result = new Or(); if (this->leftIsSet()) { result->setLeft(this->getLeft().clone()); @@ -125,7 +125,7 @@ public: * * @returns A bit vector indicating all states that satisfy the formula represented by the called object. */ - virtual std::vector* check(const storm::modelchecker::ltl::AbstractModelChecker& modelChecker) const { + virtual std::vector* check(const storm::modelchecker::ltl::AbstractModelChecker& modelChecker) const override { return modelChecker.template as()->checkOr(*this); } diff --git a/src/formula/Ltl/Until.h b/src/formula/Ltl/Until.h index 1f37762a3..45fc7de51 100644 --- a/src/formula/Ltl/Until.h +++ b/src/formula/Ltl/Until.h @@ -121,7 +121,7 @@ public: * * @returns a new BoundedUntil-object that is identical the called object. */ - virtual AbstractLtlFormula* clone() const { + virtual AbstractLtlFormula* clone() const override { Until* result = new Until(); if (this->leftIsSet()) { result->setLeft(this->getLeft().clone()); diff --git a/src/formula/Prctl.h b/src/formula/Prctl.h index f3d727fc1..87466f55f 100644 --- a/src/formula/Prctl.h +++ b/src/formula/Prctl.h @@ -2,7 +2,7 @@ * Prctl.h * * Created on: 06.12.2012 - * Author: chris + * Author: Christian Dehnert */ #ifndef STORM_FORMULA_PRCTL_H_ diff --git a/src/formula/Prctl/And.h b/src/formula/Prctl/And.h index b14606b54..8bdfb148a 100644 --- a/src/formula/Prctl/And.h +++ b/src/formula/Prctl/And.h @@ -94,7 +94,7 @@ public: * * @returns a new AND-object that is identical the called object. */ - virtual AbstractStateFormula* clone() const { + virtual AbstractStateFormula* clone() const override { And* result = new And(); if (this->leftIsSet()) { result->setLeft(this->getLeft().clone()); @@ -114,7 +114,7 @@ public: * * @returns A bit vector indicating all states that satisfy the formula represented by the called object. */ - virtual storm::storage::BitVector* check(const storm::modelchecker::prctl::AbstractModelChecker& modelChecker) const { + virtual storm::storage::BitVector* check(const storm::modelchecker::prctl::AbstractModelChecker& modelChecker) const override { return modelChecker.template as()->checkAnd(*this); } diff --git a/src/formula/Prctl/Ap.h b/src/formula/Prctl/Ap.h index d7d878366..898d78f13 100644 --- a/src/formula/Prctl/Ap.h +++ b/src/formula/Prctl/Ap.h @@ -78,7 +78,7 @@ public: * * @returns a new AND-object that is identical the called object. */ - virtual AbstractStateFormula* clone() const { + virtual AbstractStateFormula* clone() const override { return new Ap(this->getAp()); } @@ -91,7 +91,7 @@ public: * * @returns A bit vector indicating all states that satisfy the formula represented by the called object. */ - virtual storm::storage::BitVector *check(const storm::modelchecker::prctl::AbstractModelChecker& modelChecker) const { + virtual storm::storage::BitVector *check(const storm::modelchecker::prctl::AbstractModelChecker& modelChecker) const override { return modelChecker.template as()->checkAp(*this); } diff --git a/src/formula/Prctl/BoundedEventually.h b/src/formula/Prctl/BoundedEventually.h index 5f716006d..1956b5da4 100644 --- a/src/formula/Prctl/BoundedEventually.h +++ b/src/formula/Prctl/BoundedEventually.h @@ -95,7 +95,7 @@ public: * * @returns a new BoundedUntil-object that is identical the called object. */ - virtual AbstractPathFormula* clone() const { + virtual AbstractPathFormula* clone() const override { BoundedEventually* result = new BoundedEventually(); result->setBound(this->getBound()); if (this->childIsSet()) { @@ -114,7 +114,7 @@ public: * * @returns A vector indicating the probability that the formula holds for each state. */ - virtual std::vector* check(const storm::modelchecker::prctl::AbstractModelChecker& modelChecker, bool qualitative) const { + virtual std::vector* check(const storm::modelchecker::prctl::AbstractModelChecker& modelChecker, bool qualitative) const override { return modelChecker.template as()->checkBoundedEventually(*this, qualitative); } }; diff --git a/src/formula/Prctl/BoundedNaryUntil.h b/src/formula/Prctl/BoundedNaryUntil.h index ad0d73ebc..21401ffa8 100644 --- a/src/formula/Prctl/BoundedNaryUntil.h +++ b/src/formula/Prctl/BoundedNaryUntil.h @@ -103,7 +103,7 @@ public: * * @returns a new BoundedNaryUntil-object that is identical the called object. */ - virtual AbstractPathFormula* clone() const { + virtual AbstractPathFormula* clone() const override { BoundedNaryUntil* result = new BoundedNaryUntil(); if (this->leftIsSet()) { result->setLeft(this->getLeft().clone()); @@ -128,7 +128,7 @@ public: * * @returns A vector indicating the probability that the formula holds for each state. */ - virtual std::vector *check(const storm::modelchecker::prctl::AbstractModelChecker& modelChecker, bool qualitative) const { + virtual std::vector *check(const storm::modelchecker::prctl::AbstractModelChecker& modelChecker, bool qualitative) const override { return modelChecker.template as()->checkBoundedNaryUntil(*this, qualitative); } diff --git a/src/formula/Prctl/BoundedUntil.h b/src/formula/Prctl/BoundedUntil.h index cfa951bf5..795ddbc23 100644 --- a/src/formula/Prctl/BoundedUntil.h +++ b/src/formula/Prctl/BoundedUntil.h @@ -97,7 +97,7 @@ public: * * @returns a new BoundedUntil-object that is identical the called object. */ - virtual AbstractPathFormula* clone() const { + virtual AbstractPathFormula* clone() const override { BoundedUntil* result = new BoundedUntil(); result->setBound(this->getBound()); if (this->leftIsSet()) { @@ -119,7 +119,7 @@ public: * * @returns A vector indicating the probability that the formula holds for each state. */ - virtual std::vector *check(const storm::modelchecker::prctl::AbstractModelChecker& modelChecker, bool qualitative) const { + virtual std::vector *check(const storm::modelchecker::prctl::AbstractModelChecker& modelChecker, bool qualitative) const override { return modelChecker.template as()->checkBoundedUntil(*this, qualitative); } }; diff --git a/src/formula/Prctl/CumulativeReward.h b/src/formula/Prctl/CumulativeReward.h index 382d31c80..1ed56d2c1 100644 --- a/src/formula/Prctl/CumulativeReward.h +++ b/src/formula/Prctl/CumulativeReward.h @@ -84,7 +84,7 @@ public: * * @returns a new CumulativeReward-object that is identical the called object. */ - virtual AbstractPathFormula* clone() const { + virtual AbstractPathFormula* clone() const override { return new CumulativeReward(this->getBound()); } @@ -98,7 +98,7 @@ public: * * @returns A vector indicating the probability that the formula holds for each state. */ - virtual std::vector *check(const storm::modelchecker::prctl::AbstractModelChecker& modelChecker, bool qualitative) const { + virtual std::vector *check(const storm::modelchecker::prctl::AbstractModelChecker& modelChecker, bool qualitative) const override { return modelChecker.template as()->checkCumulativeReward(*this, qualitative); } }; diff --git a/src/formula/Prctl/Eventually.h b/src/formula/Prctl/Eventually.h index 083d1bf79..39dd73c88 100644 --- a/src/formula/Prctl/Eventually.h +++ b/src/formula/Prctl/Eventually.h @@ -91,7 +91,7 @@ public: * * @returns a new Eventually-object that is identical the called object. */ - virtual AbstractPathFormula* clone() const { + virtual AbstractPathFormula* clone() const override { Eventually* result = new Eventually(); if (this->childIsSet()) { result->setChild(this->getChild().clone()); @@ -108,7 +108,7 @@ public: * * @returns A vector indicating the probability that the formula holds for each state. */ - virtual std::vector *check(const storm::modelchecker::prctl::AbstractModelChecker& modelChecker, bool qualitative) const { + virtual std::vector *check(const storm::modelchecker::prctl::AbstractModelChecker& modelChecker, bool qualitative) const override { return modelChecker.template as()->checkEventually(*this, qualitative); } }; diff --git a/src/formula/Prctl/Globally.h b/src/formula/Prctl/Globally.h index 38b2fcb4c..c9716d4b0 100644 --- a/src/formula/Prctl/Globally.h +++ b/src/formula/Prctl/Globally.h @@ -93,7 +93,7 @@ public: * * @returns a new Globally-object that is identical the called object. */ - virtual AbstractPathFormula* clone() const { + virtual AbstractPathFormula* clone() const override { Globally* result = new Globally(); if (this->childIsSet()) { result->setChild(this->getChild().clone()); @@ -110,7 +110,7 @@ public: * * @returns A vector indicating the probability that the formula holds for each state. */ - virtual std::vector *check(const storm::modelchecker::prctl::AbstractModelChecker& modelChecker, bool qualitative) const { + virtual std::vector *check(const storm::modelchecker::prctl::AbstractModelChecker& modelChecker, bool qualitative) const override { return modelChecker.template as()->checkGlobally(*this, qualitative); } }; diff --git a/src/formula/Prctl/InstantaneousReward.h b/src/formula/Prctl/InstantaneousReward.h index bd54ef289..62b0bde5d 100644 --- a/src/formula/Prctl/InstantaneousReward.h +++ b/src/formula/Prctl/InstantaneousReward.h @@ -85,7 +85,7 @@ public: * * @returns a new InstantaneousReward-object that is identical the called object. */ - virtual AbstractPathFormula* clone() const { + virtual AbstractPathFormula* clone() const override { return new InstantaneousReward(this->getBound()); } @@ -99,7 +99,7 @@ public: * * @returns A vector indicating the probability that the formula holds for each state. */ - virtual std::vector *check(const storm::modelchecker::prctl::AbstractModelChecker& modelChecker, bool qualitative) const { + virtual std::vector *check(const storm::modelchecker::prctl::AbstractModelChecker& modelChecker, bool qualitative) const override { return modelChecker.template as()->checkInstantaneousReward(*this, qualitative); } }; diff --git a/src/formula/Prctl/Next.h b/src/formula/Prctl/Next.h index 5700f5a42..74f260765 100644 --- a/src/formula/Prctl/Next.h +++ b/src/formula/Prctl/Next.h @@ -91,7 +91,7 @@ public: * * @returns a new BoundedUntil-object that is identical the called object. */ - virtual AbstractPathFormula* clone() const { + virtual AbstractPathFormula* clone() const override { Next* result = new Next(); if (this->childIsSet()) { result->setChild(this->getChild().clone()); @@ -108,7 +108,7 @@ public: * * @returns A vector indicating the probability that the formula holds for each state. */ - virtual std::vector *check(const storm::modelchecker::prctl::AbstractModelChecker& modelChecker, bool qualitative) const { + virtual std::vector *check(const storm::modelchecker::prctl::AbstractModelChecker& modelChecker, bool qualitative) const override { return modelChecker.template as()->checkNext(*this, qualitative); } }; diff --git a/src/formula/Prctl/Not.h b/src/formula/Prctl/Not.h index 8b60807db..18c6c3c03 100644 --- a/src/formula/Prctl/Not.h +++ b/src/formula/Prctl/Not.h @@ -87,7 +87,7 @@ public: * * @returns a new AND-object that is identical the called object. */ - virtual AbstractStateFormula* clone() const { + virtual AbstractStateFormula* clone() const override { Not* result = new Not(); if (this->childIsSet()) { result->setChild(this->getChild().clone()); @@ -104,7 +104,7 @@ public: * * @returns A bit vector indicating all states that satisfy the formula represented by the called object. */ - virtual storm::storage::BitVector *check(const storm::modelchecker::prctl::AbstractModelChecker& modelChecker) const { + virtual storm::storage::BitVector *check(const storm::modelchecker::prctl::AbstractModelChecker& modelChecker) const override { return modelChecker.template as()->checkNot(*this); } }; diff --git a/src/formula/Prctl/Or.h b/src/formula/Prctl/Or.h index 6a9159c7a..799d2000c 100644 --- a/src/formula/Prctl/Or.h +++ b/src/formula/Prctl/Or.h @@ -93,7 +93,7 @@ public: * * @returns a new AND-object that is identical the called object. */ - virtual AbstractStateFormula* clone() const { + virtual AbstractStateFormula* clone() const override { Or* result = new Or(); if (this->leftIsSet()) { result->setLeft(this->getLeft().clone()); @@ -113,7 +113,7 @@ public: * * @returns A bit vector indicating all states that satisfy the formula represented by the called object. */ - virtual storm::storage::BitVector *check(const storm::modelchecker::prctl::AbstractModelChecker& modelChecker) const { + virtual storm::storage::BitVector *check(const storm::modelchecker::prctl::AbstractModelChecker& modelChecker) const override { return modelChecker.template as()->checkOr(*this); } }; diff --git a/src/formula/Prctl/ProbabilisticBoundOperator.h b/src/formula/Prctl/ProbabilisticBoundOperator.h index 08c94398d..d65611b8d 100644 --- a/src/formula/Prctl/ProbabilisticBoundOperator.h +++ b/src/formula/Prctl/ProbabilisticBoundOperator.h @@ -110,7 +110,7 @@ public: * * @returns a new AND-object that is identical the called object. */ - virtual AbstractStateFormula* clone() const { + virtual AbstractStateFormula* clone() const override { ProbabilisticBoundOperator* result = new ProbabilisticBoundOperator(); result->setComparisonOperator(this->getComparisonOperator()); result->setBound(this->getBound()); @@ -127,7 +127,7 @@ public: * * @returns A bit vector indicating all states that satisfy the formula represented by the called object. */ - virtual storm::storage::BitVector* check(const storm::modelchecker::prctl::AbstractModelChecker& modelChecker) const { + virtual storm::storage::BitVector* check(const storm::modelchecker::prctl::AbstractModelChecker& modelChecker) const override { return modelChecker.template as()->checkProbabilisticBoundOperator(*this); } }; diff --git a/src/formula/Prctl/ProbabilisticNoBoundOperator.h b/src/formula/Prctl/ProbabilisticNoBoundOperator.h index b50060ec4..1f3a5f24f 100644 --- a/src/formula/Prctl/ProbabilisticNoBoundOperator.h +++ b/src/formula/Prctl/ProbabilisticNoBoundOperator.h @@ -84,7 +84,7 @@ public: // Intentionally left empty } - virtual AbstractNoBoundOperator* clone() const { + virtual AbstractNoBoundOperator* clone() const override { ProbabilisticNoBoundOperator* result = new ProbabilisticNoBoundOperator(); if (this->pathFormulaIsSet()) { result->setPathFormula(this->getPathFormula().clone()); @@ -103,7 +103,7 @@ public: * * @returns A vector indicating the probability that the formula holds for each state. */ - virtual std::vector* check(const storm::modelchecker::prctl::AbstractModelChecker& modelChecker, bool qualitative=false) const { + virtual std::vector* check(const storm::modelchecker::prctl::AbstractModelChecker& modelChecker, bool qualitative=false) const override { return this->getPathFormula().check(modelChecker, qualitative); } }; diff --git a/src/formula/Prctl/ReachabilityReward.h b/src/formula/Prctl/ReachabilityReward.h index a155c2835..ba3ba319c 100644 --- a/src/formula/Prctl/ReachabilityReward.h +++ b/src/formula/Prctl/ReachabilityReward.h @@ -88,7 +88,7 @@ public: * * @returns a new ReachabilityReward-object that is identical the called object. */ - virtual AbstractPathFormula* clone() const { + virtual AbstractPathFormula* clone() const override { ReachabilityReward* result = new ReachabilityReward(); if (this->childIsSet()) { result->setChild(this->getChild().clone()); @@ -105,7 +105,7 @@ public: * * @returns A vector indicating the probability that the formula holds for each state. */ - virtual std::vector *check(const storm::modelchecker::prctl::AbstractModelChecker& modelChecker, bool qualitative) const { + virtual std::vector *check(const storm::modelchecker::prctl::AbstractModelChecker& modelChecker, bool qualitative) const override { return modelChecker.template as()->checkReachabilityReward(*this, qualitative); } }; diff --git a/src/formula/Prctl/RewardBoundOperator.h b/src/formula/Prctl/RewardBoundOperator.h index 572364b88..412371c10 100644 --- a/src/formula/Prctl/RewardBoundOperator.h +++ b/src/formula/Prctl/RewardBoundOperator.h @@ -103,7 +103,7 @@ public: * * @returns a new AND-object that is identical the called object. */ - virtual AbstractStateFormula* clone() const { + virtual AbstractStateFormula* clone() const override { RewardBoundOperator* result = new RewardBoundOperator(); result->setComparisonOperator(this->getComparisonOperator()); result->setBound(this->getBound()); @@ -120,7 +120,7 @@ public: * * @returns A bit vector indicating all states that satisfy the formula represented by the called object. */ - virtual storm::storage::BitVector* check(const storm::modelchecker::prctl::AbstractModelChecker& modelChecker) const { + virtual storm::storage::BitVector* check(const storm::modelchecker::prctl::AbstractModelChecker& modelChecker) const override { return modelChecker.template as()->checkRewardBoundOperator(*this); } }; diff --git a/src/formula/Prctl/RewardNoBoundOperator.h b/src/formula/Prctl/RewardNoBoundOperator.h index 108c1f14c..676517b0b 100644 --- a/src/formula/Prctl/RewardNoBoundOperator.h +++ b/src/formula/Prctl/RewardNoBoundOperator.h @@ -77,7 +77,7 @@ public: // Intentionally left empty } - virtual AbstractNoBoundOperator* clone() const { + virtual AbstractNoBoundOperator* clone() const override { RewardNoBoundOperator* result = new RewardNoBoundOperator(); if (this->pathFormulaIsSet()) { result->setPathFormula(this->getPathFormula().clone()); @@ -96,7 +96,7 @@ public: * * @returns A vector indicating the probability that the formula holds for each state. */ - virtual std::vector* check(const storm::modelchecker::prctl::AbstractModelChecker& modelChecker, bool qualitative=false) const { + virtual std::vector* check(const storm::modelchecker::prctl::AbstractModelChecker& modelChecker, bool qualitative=false) const override { return this->getPathFormula().check(modelChecker, qualitative); } }; diff --git a/src/formula/Prctl/SteadyStateReward.h b/src/formula/Prctl/SteadyStateReward.h index df9f0a6f1..f963b925b 100644 --- a/src/formula/Prctl/SteadyStateReward.h +++ b/src/formula/Prctl/SteadyStateReward.h @@ -67,7 +67,7 @@ public: * * @returns a new SteadyState-object that is identical the called object. */ - virtual AbstractPathFormula* clone() const { + virtual AbstractPathFormula* clone() const override { return new SteadyStateReward(); } @@ -80,7 +80,7 @@ public: * * @returns A vector indicating the probability that the formula holds for each state. */ - virtual std::vector *check(const storm::modelchecker::prctl::AbstractModelChecker& modelChecker, bool qualitative) const { + virtual std::vector *check(const storm::modelchecker::prctl::AbstractModelChecker& modelChecker, bool qualitative) const override { return modelChecker.template as()->checkSteadyStateReward(*this, qualitative); } }; diff --git a/src/formula/Prctl/Until.h b/src/formula/Prctl/Until.h index 75e27eb33..8f9b7a751 100644 --- a/src/formula/Prctl/Until.h +++ b/src/formula/Prctl/Until.h @@ -93,7 +93,7 @@ public: * * @returns a new BoundedUntil-object that is identical the called object. */ - virtual AbstractPathFormula* clone() const { + virtual AbstractPathFormula* clone() const override { Until* result = new Until(); if (this->leftIsSet()) { result->setLeft(this->getLeft().clone()); @@ -113,7 +113,7 @@ public: * * @returns A vector indicating the probability that the formula holds for each state. */ - virtual std::vector *check(const storm::modelchecker::prctl::AbstractModelChecker& modelChecker, bool qualitative) const { + virtual std::vector *check(const storm::modelchecker::prctl::AbstractModelChecker& modelChecker, bool qualitative) const override { return modelChecker.template as()->checkUntil(*this, qualitative); } }; diff --git a/src/formula/abstract/And.h b/src/formula/abstract/And.h index e8c474c73..c2739a9e4 100644 --- a/src/formula/abstract/And.h +++ b/src/formula/abstract/And.h @@ -130,7 +130,7 @@ public: /*! * @returns a string representation of the formula */ - virtual std::string toString() const { + virtual std::string toString() const override { std::string result = "("; result += left->toString(); result += " & "; @@ -145,7 +145,7 @@ public: * @param checker Formula checker object. * @return true iff all subtrees conform to some logic. */ - virtual bool validate(const AbstractFormulaChecker& checker) const { + virtual bool validate(const AbstractFormulaChecker& checker) const override { return checker.validate(this->left) && checker.validate(this->right); } diff --git a/src/formula/abstract/Ap.h b/src/formula/abstract/Ap.h index 47abc09ea..dd0acce82 100644 --- a/src/formula/abstract/Ap.h +++ b/src/formula/abstract/Ap.h @@ -55,7 +55,7 @@ public: * @returns a string representation of the leaf. * */ - virtual std::string toString() const { + virtual std::string toString() const override { return getAp(); } @@ -67,7 +67,7 @@ public: * @param checker Formula checker object. * @return true */ - virtual bool validate(const AbstractFormulaChecker& checker) const { + virtual bool validate(const AbstractFormulaChecker& checker) const override { return true; } diff --git a/src/formula/abstract/BoundedEventually.h b/src/formula/abstract/BoundedEventually.h index 0b3b44ade..295ae7aa5 100644 --- a/src/formula/abstract/BoundedEventually.h +++ b/src/formula/abstract/BoundedEventually.h @@ -118,7 +118,7 @@ public: /*! * @returns a string representation of the formula */ - virtual std::string toString() const { + virtual std::string toString() const override { std::string result = "F<="; result += std::to_string(bound); result += " "; @@ -132,7 +132,7 @@ public: * @param checker Formula checker object. * @return true iff the subtree conforms to some logic. */ - virtual bool validate(const AbstractFormulaChecker& checker) const { + virtual bool validate(const AbstractFormulaChecker& checker) const override { return checker.validate(this->child); } diff --git a/src/formula/abstract/BoundedNaryUntil.h b/src/formula/abstract/BoundedNaryUntil.h index 5863da04d..893501d4c 100644 --- a/src/formula/abstract/BoundedNaryUntil.h +++ b/src/formula/abstract/BoundedNaryUntil.h @@ -138,7 +138,7 @@ public: /*! * @returns a string representation of the formula */ - virtual std::string toString() const { + virtual std::string toString() const override { std::stringstream result; result << "( " << left->toString(); for (auto it = this->right->begin(); it != this->right->end(); ++it) { @@ -154,7 +154,7 @@ public: * @param checker Formula checker object. * @return true iff all subtrees conform to some logic. */ - virtual bool validate(const AbstractFormulaChecker& checker) const { + virtual bool validate(const AbstractFormulaChecker& checker) const override { bool res = checker.validate(this->left); for (auto it = this->right->begin(); it != this->right->end(); ++it) { res &= checker.validate(std::get<0>(*it)); diff --git a/src/formula/abstract/BoundedUntil.h b/src/formula/abstract/BoundedUntil.h index d31236d7b..d382df073 100644 --- a/src/formula/abstract/BoundedUntil.h +++ b/src/formula/abstract/BoundedUntil.h @@ -148,7 +148,7 @@ public: /*! * @returns a string representation of the formula */ - virtual std::string toString() const { + virtual std::string toString() const override { std::string result = left->toString(); result += " U<="; result += std::to_string(bound); @@ -163,7 +163,7 @@ public: * @param checker Formula checker object. * @return true iff all subtrees conform to some logic. */ - virtual bool validate(const AbstractFormulaChecker& checker) const { + virtual bool validate(const AbstractFormulaChecker& checker) const override { return checker.validate(this->left) && checker.validate(this->right); } diff --git a/src/formula/abstract/CumulativeReward.h b/src/formula/abstract/CumulativeReward.h index b55c2119b..f347ebd77 100644 --- a/src/formula/abstract/CumulativeReward.h +++ b/src/formula/abstract/CumulativeReward.h @@ -72,7 +72,7 @@ public: /*! * @returns a string representation of the formula */ - virtual std::string toString() const { + virtual std::string toString() const override { std::string result = "C <= "; result += std::to_string(bound); return result; @@ -86,7 +86,7 @@ public: * @param checker Formula checker object. * @return true */ - virtual bool validate(const AbstractFormulaChecker& checker) const { + virtual bool validate(const AbstractFormulaChecker& checker) const override { return true; } diff --git a/src/formula/abstract/Eventually.h b/src/formula/abstract/Eventually.h index 5b5f68de3..3171c559a 100644 --- a/src/formula/abstract/Eventually.h +++ b/src/formula/abstract/Eventually.h @@ -96,7 +96,7 @@ public: /*! * @returns a string representation of the formula */ - virtual std::string toString() const { + virtual std::string toString() const override { std::string result = "F "; result += child->toString(); return result; @@ -108,7 +108,7 @@ public: * @param checker Formula checker object. * @return true iff the subtree conforms to some logic. */ - virtual bool validate(const AbstractFormulaChecker& checker) const { + virtual bool validate(const AbstractFormulaChecker& checker) const override { return checker.validate(this->child); } diff --git a/src/formula/abstract/Globally.h b/src/formula/abstract/Globally.h index ca9c553c6..77444c232 100644 --- a/src/formula/abstract/Globally.h +++ b/src/formula/abstract/Globally.h @@ -97,7 +97,7 @@ public: /*! * @returns a string representation of the formula */ - virtual std::string toString() const { + virtual std::string toString() const override { std::string result = "G "; result += child->toString(); return result; @@ -109,7 +109,7 @@ public: * @param checker Formula checker object. * @return true iff the subtree conforms to some logic. */ - virtual bool validate(const AbstractFormulaChecker& checker) const { + virtual bool validate(const AbstractFormulaChecker& checker) const override { return checker.validate(this->child); } diff --git a/src/formula/abstract/InstantaneousReward.h b/src/formula/abstract/InstantaneousReward.h index eacbc1906..424b0b9ce 100644 --- a/src/formula/abstract/InstantaneousReward.h +++ b/src/formula/abstract/InstantaneousReward.h @@ -72,7 +72,7 @@ public: /*! * @returns a string representation of the formula */ - virtual std::string toString() const { + virtual std::string toString() const override { std::string result = "I="; result += std::to_string(bound); return result; @@ -86,7 +86,7 @@ public: * @param checker Formula checker object. * @return true */ - virtual bool validate(const AbstractFormulaChecker& checker) const { + virtual bool validate(const AbstractFormulaChecker& checker) const override { return true; } diff --git a/src/formula/abstract/Next.h b/src/formula/abstract/Next.h index bf049ad1b..d4fc9fe94 100644 --- a/src/formula/abstract/Next.h +++ b/src/formula/abstract/Next.h @@ -97,7 +97,7 @@ public: /*! * @returns a string representation of the formula */ - virtual std::string toString() const { + virtual std::string toString() const override { std::string result = "("; result += " X "; result += child->toString(); @@ -111,7 +111,7 @@ public: * @param checker Formula checker object. * @return true iff the subtree conforms to some logic. */ - virtual bool validate(const AbstractFormulaChecker& checker) const { + virtual bool validate(const AbstractFormulaChecker& checker) const override { return checker.validate(this->child); } diff --git a/src/formula/abstract/Not.h b/src/formula/abstract/Not.h index 9ab3ec237..bfa24059d 100644 --- a/src/formula/abstract/Not.h +++ b/src/formula/abstract/Not.h @@ -93,7 +93,7 @@ public: /*! * @returns a string representation of the formula */ - virtual std::string toString() const { + virtual std::string toString() const override { std::string result = "!"; result += child->toString(); return result; @@ -105,7 +105,7 @@ public: * @param checker Formula checker object. * @return true iff the subtree conforms to some logic. */ - virtual bool validate(const AbstractFormulaChecker& checker) const { + virtual bool validate(const AbstractFormulaChecker& checker) const override { return checker.validate(this->child); } diff --git a/src/formula/abstract/Or.h b/src/formula/abstract/Or.h index 071173c4a..67ed1e72d 100644 --- a/src/formula/abstract/Or.h +++ b/src/formula/abstract/Or.h @@ -128,7 +128,7 @@ public: /*! * @returns a string representation of the formula */ - virtual std::string toString() const { + virtual std::string toString() const override { std::string result = "("; result += left->toString(); result += " | "; @@ -143,7 +143,7 @@ public: * @param checker Formula checker object. * @return true iff all subtrees conform to some logic. */ - virtual bool validate(const AbstractFormulaChecker& checker) const { + virtual bool validate(const AbstractFormulaChecker& checker) const override { return checker.validate(this->left) && checker.validate(this->right); } diff --git a/src/formula/abstract/PathBoundOperator.h b/src/formula/abstract/PathBoundOperator.h index f832232a5..cc841d78d 100644 --- a/src/formula/abstract/PathBoundOperator.h +++ b/src/formula/abstract/PathBoundOperator.h @@ -143,7 +143,7 @@ public: /*! * @returns a string representation of the formula */ - virtual std::string toString() const { + virtual std::string toString() const override { std::string result = ""; switch (comparisonOperator) { case LESS: result += "<"; break; @@ -175,7 +175,7 @@ public: * @param checker Formula checker object. * @return true iff the subtree conforms to some logic. */ - virtual bool validate(const AbstractFormulaChecker& checker) const { + virtual bool validate(const AbstractFormulaChecker& checker) const override { return checker.validate(this->pathFormula); } diff --git a/src/formula/abstract/PathNoBoundOperator.h b/src/formula/abstract/PathNoBoundOperator.h index 02107c9ff..1b0af8d1e 100644 --- a/src/formula/abstract/PathNoBoundOperator.h +++ b/src/formula/abstract/PathNoBoundOperator.h @@ -122,7 +122,7 @@ public: /*! * @returns a string representation of the formula */ - virtual std::string toString() const { + virtual std::string toString() const override { std::string result; if (this->isOptimalityOperator()) { if (this->isMinimumOperator()) { @@ -143,7 +143,7 @@ public: * @param checker Formula checker object. * @return true iff the subtree conforms to some logic. */ - virtual bool validate(const AbstractFormulaChecker& checker) const { + virtual bool validate(const AbstractFormulaChecker& checker) const override { return checker.validate(this->pathFormula); } diff --git a/src/formula/abstract/ProbabilisticBoundOperator.h b/src/formula/abstract/ProbabilisticBoundOperator.h index d9b14b183..d8fc0764d 100644 --- a/src/formula/abstract/ProbabilisticBoundOperator.h +++ b/src/formula/abstract/ProbabilisticBoundOperator.h @@ -100,7 +100,7 @@ public: /*! * @returns a string representation of the formula */ - virtual std::string toString() const { + virtual std::string toString() const override { std::string result = "P "; result += PathBoundOperator::toString(); return result; diff --git a/src/formula/abstract/ProbabilisticNoBoundOperator.h b/src/formula/abstract/ProbabilisticNoBoundOperator.h index 9b276f976..7bf01422e 100644 --- a/src/formula/abstract/ProbabilisticNoBoundOperator.h +++ b/src/formula/abstract/ProbabilisticNoBoundOperator.h @@ -90,7 +90,7 @@ public: /*! * @returns a string representation of the formula */ - virtual std::string toString() const { + virtual std::string toString() const override { std::string result = "P"; result += PathNoBoundOperator::toString(); return result; diff --git a/src/formula/abstract/RewardBoundOperator.h b/src/formula/abstract/RewardBoundOperator.h index 961c11f21..d607133f9 100644 --- a/src/formula/abstract/RewardBoundOperator.h +++ b/src/formula/abstract/RewardBoundOperator.h @@ -92,7 +92,7 @@ public: /*! * @returns a string representation of the formula */ - virtual std::string toString() const { + virtual std::string toString() const override { std::string result = "R "; result += PathBoundOperator::toString(); return result; diff --git a/src/formula/abstract/RewardNoBoundOperator.h b/src/formula/abstract/RewardNoBoundOperator.h index 72fb06f6f..a147502d8 100644 --- a/src/formula/abstract/RewardNoBoundOperator.h +++ b/src/formula/abstract/RewardNoBoundOperator.h @@ -89,7 +89,7 @@ public: /*! * @returns a string representation of the formula */ - virtual std::string toString() const { + virtual std::string toString() const override { std::string result = "R"; result += PathNoBoundOperator::toString(); return result; diff --git a/src/formula/abstract/StateBoundOperator.h b/src/formula/abstract/StateBoundOperator.h index ee3daa880..6258c7044 100644 --- a/src/formula/abstract/StateBoundOperator.h +++ b/src/formula/abstract/StateBoundOperator.h @@ -126,7 +126,7 @@ public: /*! * @returns a string representation of the formula */ - virtual std::string toString() const { + virtual std::string toString() const override { std::string result = " "; switch (comparisonOperator) { case LESS: result += "< "; break; @@ -157,7 +157,7 @@ public: * @param checker Formula checker object. * @return true iff the subtree conforms to some logic. */ - virtual bool validate(const AbstractFormulaChecker& checker) const { + virtual bool validate(const AbstractFormulaChecker& checker) const override { return checker.validate(this->stateFormula); } diff --git a/src/formula/abstract/StateNoBoundOperator.h b/src/formula/abstract/StateNoBoundOperator.h index fd2b02896..2961debea 100644 --- a/src/formula/abstract/StateNoBoundOperator.h +++ b/src/formula/abstract/StateNoBoundOperator.h @@ -98,7 +98,7 @@ public: /*! * @returns a string representation of the formula */ - virtual std::string toString() const { + virtual std::string toString() const override { std::string result; result += " = ? ["; result += this->getStateFormula().toString(); @@ -112,7 +112,7 @@ public: * @param checker Formula checker object. * @return true iff the subtree conforms to some logic. */ - virtual bool validate(const AbstractFormulaChecker& checker) const { + virtual bool validate(const AbstractFormulaChecker& checker) const override { return checker.validate(this->stateFormula); } diff --git a/src/formula/abstract/SteadyStateBoundOperator.h b/src/formula/abstract/SteadyStateBoundOperator.h index 3bbb7f88c..5c24ccff0 100644 --- a/src/formula/abstract/SteadyStateBoundOperator.h +++ b/src/formula/abstract/SteadyStateBoundOperator.h @@ -65,7 +65,7 @@ public: /*! * @returns a string representation of the formula */ - virtual std::string toString() const { + virtual std::string toString() const override { return "S" + StateBoundOperator::toString(); } }; diff --git a/src/formula/abstract/SteadyStateNoBoundOperator.h b/src/formula/abstract/SteadyStateNoBoundOperator.h index 88fe73ead..6e544d207 100644 --- a/src/formula/abstract/SteadyStateNoBoundOperator.h +++ b/src/formula/abstract/SteadyStateNoBoundOperator.h @@ -63,7 +63,7 @@ public: /*! * @returns a string representation of the formula */ - virtual std::string toString() const { + virtual std::string toString() const override { return "S" + StateNoBoundOperator::toString(); } diff --git a/src/formula/abstract/SteadyStateReward.h b/src/formula/abstract/SteadyStateReward.h index a57b61fc6..d5f344752 100644 --- a/src/formula/abstract/SteadyStateReward.h +++ b/src/formula/abstract/SteadyStateReward.h @@ -39,7 +39,7 @@ public: /*! * @returns a string representation of the formula */ - virtual std::string toString() const { + virtual std::string toString() const override { return "S"; } @@ -51,7 +51,7 @@ public: * @param checker Formula checker object. * @return true */ - virtual bool validate(const AbstractFormulaChecker& checker) const { + virtual bool validate(const AbstractFormulaChecker& checker) const override { return true; } }; diff --git a/src/formula/abstract/TimeBoundedEventually.h b/src/formula/abstract/TimeBoundedEventually.h index 23d0fd74f..eaecaa868 100644 --- a/src/formula/abstract/TimeBoundedEventually.h +++ b/src/formula/abstract/TimeBoundedEventually.h @@ -78,7 +78,7 @@ public: /*! * @returns a string representation of the formula */ - virtual std::string toString() const { + virtual std::string toString() const override { std::string result = "F"; result += TimeBoundedOperator::toString(); result += " "; @@ -92,7 +92,7 @@ public: * @param checker Formula checker object. * @return true iff the subtree conforms to some logic. */ - virtual bool validate(const AbstractFormulaChecker& checker) const { + virtual bool validate(const AbstractFormulaChecker& checker) const override { return checker.validate(this->child); } diff --git a/src/formula/abstract/TimeBoundedOperator.h b/src/formula/abstract/TimeBoundedOperator.h index cb35b8520..d26fea552 100644 --- a/src/formula/abstract/TimeBoundedOperator.h +++ b/src/formula/abstract/TimeBoundedOperator.h @@ -87,7 +87,7 @@ public: * @returns a string representation of the Interval of the formula * May be used in subclasses to simplify string output. */ - virtual std::string toString() const { + virtual std::string toString() const override { std::string result = ""; if (upperBound == std::numeric_limits::infinity()) { result = ">=" + std::to_string(lowerBound); diff --git a/src/formula/abstract/TimeBoundedUntil.h b/src/formula/abstract/TimeBoundedUntil.h index 146c82cd1..936baeef4 100644 --- a/src/formula/abstract/TimeBoundedUntil.h +++ b/src/formula/abstract/TimeBoundedUntil.h @@ -118,7 +118,7 @@ public: /*! * @returns a string representation of the formula */ - virtual std::string toString() const { + virtual std::string toString() const override { std::string result = left->toString(); result += " U"; result += TimeBoundedOperator::toString(); @@ -133,7 +133,7 @@ public: * @param checker Formula checker object. * @return true iff the subtree conforms to some logic. */ - virtual bool validate(const AbstractFormulaChecker& checker) const { + virtual bool validate(const AbstractFormulaChecker& checker) const override { return checker.validate(this->left) && checker.validate(this->right); } diff --git a/src/formula/abstract/Until.h b/src/formula/abstract/Until.h index 1df330926..dd093de88 100644 --- a/src/formula/abstract/Until.h +++ b/src/formula/abstract/Until.h @@ -128,7 +128,7 @@ public: /*! * @returns a string representation of the formula */ - virtual std::string toString() const { + virtual std::string toString() const override { std::string result = left->toString(); result += " U "; result += right->toString(); @@ -141,7 +141,7 @@ public: * @param checker Formula checker object. * @return true iff all subtrees conform to some logic. */ - virtual bool validate(const AbstractFormulaChecker& checker) const { + virtual bool validate(const AbstractFormulaChecker& checker) const override { return checker.validate(this->left) && checker.validate(this->right); } diff --git a/src/ir/expressions/BooleanLiteral.h b/src/ir/expressions/BooleanLiteral.h new file mode 100644 index 000000000..3768f68f8 --- /dev/null +++ b/src/ir/expressions/BooleanLiteral.h @@ -0,0 +1,62 @@ +/* + * BooleanLiteral.h + * + * Created on: 03.01.2013 + * Author: chris + */ + +#ifndef STORM_IR_EXPRESSIONS_BOOLEANLITERAL_H_ +#define STORM_IR_EXPRESSIONS_BOOLEANLITERAL_H_ + +#include "src/ir/expressions/BaseExpression.h" + +namespace storm { +namespace ir { +namespace expressions { + +class BooleanLiteral : public BaseExpression { +public: + bool value; + + BooleanLiteral(bool value) : BaseExpression(bool_), value(value) { + + } + + virtual ~BooleanLiteral() { + + } + + virtual std::shared_ptr clone(const std::map& renaming, const std::map& bools, const std::map& ints) override { + return std::shared_ptr(new BooleanLiteral(this->value)); + } + + virtual bool getValueAsBool(std::pair, std::vector> const* variableValues) const override { + return value; + } + + virtual void accept(ExpressionVisitor* visitor) override { + visitor->visit(this); + } + + virtual std::string toString() const override { + if (value) { + return std::string("true"); + } else { + return std::string("false"); + } + } + + virtual std::string dump(std::string prefix) const override { + std::stringstream result; + result << prefix << "BooleanLiteral " << this->toString() << std::endl; + return result.str(); + } +}; + +} + +} + +} + +#endif /* STORM_IR_EXPRESSIONS_BOOLEANLITERAL_H_ */ diff --git a/src/ir/expressions/DoubleLiteral.h b/src/ir/expressions/DoubleLiteral.h new file mode 100644 index 000000000..7c66cc636 --- /dev/null +++ b/src/ir/expressions/DoubleLiteral.h @@ -0,0 +1,62 @@ +/* + * DoubleLiteral.h + * + * Created on: 03.01.2013 + * Author: chris + */ + +#ifndef STORM_IR_EXPRESSIONS_DOUBLELITERAL_H_ +#define STORM_IR_EXPRESSIONS_DOUBLELITERAL_H_ + +#include "src/ir/expressions/BaseExpression.h" + +#include "boost/lexical_cast.hpp" + +namespace storm { + +namespace ir { + +namespace expressions { + +class DoubleLiteral : public BaseExpression { +public: + double value; + + DoubleLiteral(double value) : BaseExpression(double_), value(value) { + + } + + virtual ~DoubleLiteral() { + + } + + virtual std::shared_ptr clone(const std::map& renaming, const std::map& bools, const std::map& ints) override { + return std::shared_ptr(new DoubleLiteral(this->value)); + } + + virtual double getValueAsDouble(std::pair, std::vector> const* variableValues) const override { + return value; + } + + virtual void accept(ExpressionVisitor* visitor) override { + visitor->visit(this); + } + + virtual std::string toString() const override { + return boost::lexical_cast(value); + } + + virtual std::string dump(std::string prefix) const override { + std::stringstream result; + result << prefix << "DoubleLiteral " << this->toString() << std::endl; + return result.str(); + } +}; + +} + +} + +} + +#endif /* STORM_IR_EXPRESSIONS_DOUBLELITERAL_H_ */ diff --git a/src/ir/expressions/IntegerLiteral.h b/src/ir/expressions/IntegerLiteral.h new file mode 100644 index 000000000..453d6f685 --- /dev/null +++ b/src/ir/expressions/IntegerLiteral.h @@ -0,0 +1,58 @@ +/* + * IntegerLiteral.h + * + * Created on: 03.01.2013 + * Author: chris + */ + +#ifndef STORM_IR_EXPRESSIONS_INTEGERLITERAL_H_ +#define STORM_IR_EXPRESSIONS_INTEGERLITERAL_H_ + +#include "src/ir/expressions/BaseExpression.h" + +namespace storm { + +namespace ir { + +namespace expressions { + +class IntegerLiteral : public BaseExpression { +public: + int_fast64_t value; + + IntegerLiteral(int_fast64_t value) : BaseExpression(int_), value(value) { + } + + virtual ~IntegerLiteral() { + } + + virtual std::shared_ptr clone(const std::map& renaming, const std::map& bools, const std::map& ints) override { + return std::shared_ptr(new IntegerLiteral(this->value)); + } + + virtual int_fast64_t getValueAsInt(std::pair, std::vector> const* variableValues) const override { + return value; + } + + virtual void accept(ExpressionVisitor* visitor) override { + visitor->visit(this); + } + + virtual std::string toString() const override { + return boost::lexical_cast(value); + } + + virtual std::string dump(std::string prefix) const override { + std::stringstream result; + result << prefix << "IntegerLiteral " << this->toString() << std::endl; + return result.str(); + } +}; + +} + +} + +} + +#endif /* STORM_IR_EXPRESSIONS_INTEGERLITERAL_H_ */