diff --git a/CMakeLists.txt b/CMakeLists.txt index 24c625754..72fa4adef 100644 --- a/CMakeLists.txt +++ b/CMakeLists.txt @@ -255,7 +255,9 @@ file(GLOB_RECURSE STORM_ADAPTERS_FILES ${PROJECT_SOURCE_DIR}/src/adapters/*.h ${ file(GLOB_RECURSE STORM_BUILDER_FILES ${PROJECT_SOURCE_DIR}/src/builder/*.h ${PROJECT_SOURCE_DIR}/src/builder/*.cpp) file(GLOB_RECURSE STORM_EXCEPTIONS_FILES ${PROJECT_SOURCE_DIR}/src/exceptions/*.h ${PROJECT_SOURCE_DIR}/src/exceptions/*.cpp) file(GLOB_RECURSE STORM_LOGIC_FILES ${PROJECT_SOURCE_DIR}/src/logic/*.h ${PROJECT_SOURCE_DIR}/src/logic/*.cpp) -file(GLOB_RECURSE STORM_MODELCHECKER_FILES ${PROJECT_SOURCE_DIR}/src/modelchecker/*.h ${PROJECT_SOURCE_DIR}/src/modelchecker/*.cpp) +file(GLOB STORM_MODELCHECKER_FILES ${PROJECT_SOURCE_DIR}/src/modelchecker/*.h ${PROJECT_SOURCE_DIR}/src/modelchecker/*.cpp) +file(GLOB_RECURSE STORM_MODELCHECKER_PRCTL_FILES ${PROJECT_SOURCE_DIR}/src/modelchecker/prctl/*.h ${PROJECT_SOURCE_DIR}/src/modelchecker/prctl/*.cpp) +file(GLOB_RECURSE STORM_MODELCHECKER_CSL_FILES ${PROJECT_SOURCE_DIR}/src/modelchecker/csl/*.h ${PROJECT_SOURCE_DIR}/src/modelchecker/csl/*.cpp) file(GLOB_RECURSE STORM_COUNTEREXAMPLES_FILES ${PROJECT_SOURCE_DIR}/src/counterexamples/*.h ${PROJECT_SOURCE_DIR}/src/counterexamples/*.cpp) file(GLOB_RECURSE STORM_MODELS_FILES ${PROJECT_SOURCE_DIR}/src/models/*.h ${PROJECT_SOURCE_DIR}/src/models/*.cpp) file(GLOB STORM_PARSER_FILES ${PROJECT_SOURCE_DIR}/src/parser/*.h ${PROJECT_SOURCE_DIR}/src/parser/*.cpp) @@ -288,6 +290,8 @@ source_group(exceptions FILES ${STORM_EXCEPTIONS_FILES}) source_group(logic FILES ${STORM_LOGIC_FILES}) source_group(generated FILES ${STORM_BUILD_HEADERS} ${STORM_BUILD_SOURCES}) source_group(modelchecker FILES ${STORM_MODELCHECKER_FILES}) +source_group(modelchecker\\prctl FILES ${STORM_MODELCHECKER_PRCTL_FILES}) +source_group(modelchecker\\csl FILES ${STORM_MODELCHECKER_CSL_FILES}) source_group(counterexamples FILES ${STORM_COUNTEREXAMPLES_FILES}) source_group(models FILES ${STORM_MODELS_FILES}) source_group(parser FILES ${STORM_PARSER_FILES}) diff --git a/src/logic/BinaryBooleanStateFormula.cpp b/src/logic/BinaryBooleanStateFormula.cpp index 7bd49f109..a2b3d733a 100644 --- a/src/logic/BinaryBooleanStateFormula.cpp +++ b/src/logic/BinaryBooleanStateFormula.cpp @@ -2,7 +2,7 @@ namespace storm { namespace logic { - BinaryBooleanStateFormula::BinaryBooleanStateFormula(OperatorType operatorType, std::shared_ptr const& leftSubformula, std::shared_ptr const& rightSubformula) : BinaryStateFormula(leftSubformula, rightSubformula), operatorType(operatorType) { + BinaryBooleanStateFormula::BinaryBooleanStateFormula(OperatorType operatorType, std::shared_ptr const& leftSubformula, std::shared_ptr const& rightSubformula) : BinaryStateFormula(leftSubformula, rightSubformula), operatorType(operatorType) { // Intentionally left empty. } diff --git a/src/logic/BinaryBooleanStateFormula.h b/src/logic/BinaryBooleanStateFormula.h index bb4688ccd..c55bb0cbf 100644 --- a/src/logic/BinaryBooleanStateFormula.h +++ b/src/logic/BinaryBooleanStateFormula.h @@ -9,7 +9,7 @@ namespace storm { public: enum class OperatorType {And, Or}; - BinaryBooleanStateFormula(OperatorType operatorType, std::shared_ptr const& leftSubformula, std::shared_ptr const& rightSubformula); + BinaryBooleanStateFormula(OperatorType operatorType, std::shared_ptr const& leftSubformula, std::shared_ptr const& rightSubformula); virtual ~BinaryBooleanStateFormula() { // Intentionally left empty. diff --git a/src/logic/BinaryPathFormula.cpp b/src/logic/BinaryPathFormula.cpp index c2e4f3f2f..c48da9667 100644 --- a/src/logic/BinaryPathFormula.cpp +++ b/src/logic/BinaryPathFormula.cpp @@ -2,7 +2,7 @@ namespace storm { namespace logic { - BinaryPathFormula::BinaryPathFormula(std::shared_ptr const& leftSubformula, std::shared_ptr const& rightSubformula) : leftSubformula(leftSubformula), rightSubformula(rightSubformula) { + BinaryPathFormula::BinaryPathFormula(std::shared_ptr const& leftSubformula, std::shared_ptr const& rightSubformula) : leftSubformula(leftSubformula), rightSubformula(rightSubformula) { // Intentionally left empty. } @@ -10,18 +10,10 @@ namespace storm { return true; } - Formula& BinaryPathFormula::getLeftSubformula() { - return *leftSubformula; - } - Formula const& BinaryPathFormula::getLeftSubformula() const { return *leftSubformula; } - - Formula& BinaryPathFormula::getRightSubformula() { - return *rightSubformula; - } - + Formula const& BinaryPathFormula::getRightSubformula() const { return *rightSubformula; } diff --git a/src/logic/BinaryPathFormula.h b/src/logic/BinaryPathFormula.h index cec4fa622..cddc87859 100644 --- a/src/logic/BinaryPathFormula.h +++ b/src/logic/BinaryPathFormula.h @@ -9,7 +9,7 @@ namespace storm { namespace logic { class BinaryPathFormula : public PathFormula { public: - BinaryPathFormula(std::shared_ptr const& leftSubformula, std::shared_ptr const& rightSubformula); + BinaryPathFormula(std::shared_ptr const& leftSubformula, std::shared_ptr const& rightSubformula); virtual ~BinaryPathFormula() { // Intentionally left empty. @@ -17,15 +17,12 @@ namespace storm { virtual bool isBinaryPathFormula() const override; - Formula& getLeftSubformula(); Formula const& getLeftSubformula() const; - - Formula& getRightSubformula(); Formula const& getRightSubformula() const; private: - std::shared_ptr leftSubformula; - std::shared_ptr rightSubformula; + std::shared_ptr leftSubformula; + std::shared_ptr rightSubformula; }; } } diff --git a/src/logic/BinaryStateFormula.cpp b/src/logic/BinaryStateFormula.cpp index 8cbe4b105..f2f9d4c9c 100644 --- a/src/logic/BinaryStateFormula.cpp +++ b/src/logic/BinaryStateFormula.cpp @@ -2,26 +2,17 @@ namespace storm { namespace logic { - BinaryStateFormula::BinaryStateFormula(std::shared_ptr const& leftSubformula, std::shared_ptr const& rightSubformula) : leftSubformula(leftSubformula), rightSubformula(rightSubformula) { + BinaryStateFormula::BinaryStateFormula(std::shared_ptr const& leftSubformula, std::shared_ptr const& rightSubformula) : leftSubformula(leftSubformula), rightSubformula(rightSubformula) { // Intentionally left empty. } bool BinaryStateFormula::isBinaryStateFormula() const { return true; } - - Formula& BinaryStateFormula::getLeftSubformula() { - return *leftSubformula; - } - Formula const& BinaryStateFormula::getLeftSubformula() const { return *leftSubformula; } - Formula& BinaryStateFormula::getRightSubformula() { - return *rightSubformula; - } - Formula const& BinaryStateFormula::getRightSubformula() const { return *rightSubformula; } diff --git a/src/logic/BinaryStateFormula.h b/src/logic/BinaryStateFormula.h index d7e620bc2..0002cb19b 100644 --- a/src/logic/BinaryStateFormula.h +++ b/src/logic/BinaryStateFormula.h @@ -7,7 +7,7 @@ namespace storm { namespace logic { class BinaryStateFormula : public StateFormula { public: - BinaryStateFormula(std::shared_ptr const& leftSubformula, std::shared_ptr const& rightSubformula); + BinaryStateFormula(std::shared_ptr const& leftSubformula, std::shared_ptr const& rightSubformula); virtual ~BinaryStateFormula() { // Intentionally left empty. @@ -15,15 +15,12 @@ namespace storm { virtual bool isBinaryStateFormula() const override; - Formula& getLeftSubformula(); Formula const& getLeftSubformula() const; - - Formula& getRightSubformula(); Formula const& getRightSubformula() const; private: - std::shared_ptr leftSubformula; - std::shared_ptr rightSubformula; + std::shared_ptr leftSubformula; + std::shared_ptr rightSubformula; }; } } diff --git a/src/logic/BooleanLiteralFormula.cpp b/src/logic/BooleanLiteralFormula.cpp index 06d8cd464..175f9b313 100644 --- a/src/logic/BooleanLiteralFormula.cpp +++ b/src/logic/BooleanLiteralFormula.cpp @@ -6,11 +6,11 @@ namespace storm { // Intenionally left empty. } - bool BooleanLiteralFormula::isTrue() const { + bool BooleanLiteralFormula::isTrueFormula() const { return value; } - bool BooleanLiteralFormula::isFalse() const { + bool BooleanLiteralFormula::isFalseFormula() const { return !value; } @@ -18,6 +18,10 @@ namespace storm { return true; } + bool BooleanLiteralFormula::isBooleanLiteralFormula() const { + return true; + } + std::ostream& BooleanLiteralFormula::writeToStream(std::ostream& out) const { if (value) { out << "true"; diff --git a/src/logic/BooleanLiteralFormula.h b/src/logic/BooleanLiteralFormula.h index 0451aa5a7..01ff1ed08 100644 --- a/src/logic/BooleanLiteralFormula.h +++ b/src/logic/BooleanLiteralFormula.h @@ -13,8 +13,9 @@ namespace storm { // Intentionally left empty. } - virtual bool isTrue() const override; - virtual bool isFalse() const override; + virtual bool isBooleanLiteralFormula() const override; + virtual bool isTrueFormula() const override; + virtual bool isFalseFormula() const override; virtual bool isPropositionalFormula() const override; virtual std::ostream& writeToStream(std::ostream& out) const override; diff --git a/src/logic/BoundedUntilFormula.cpp b/src/logic/BoundedUntilFormula.cpp index e5c93201a..7cfbe7b76 100644 --- a/src/logic/BoundedUntilFormula.cpp +++ b/src/logic/BoundedUntilFormula.cpp @@ -2,11 +2,11 @@ namespace storm { namespace logic { - BoundedUntilFormula::BoundedUntilFormula(std::shared_ptr const& leftSubformula, std::shared_ptr const& rightSubformula, double lowerBound, double upperBound) : BinaryPathFormula(leftSubformula, rightSubformula), bounds(std::make_pair(lowerBound, upperBound)) { + BoundedUntilFormula::BoundedUntilFormula(std::shared_ptr const& leftSubformula, std::shared_ptr const& rightSubformula, double lowerBound, double upperBound) : BinaryPathFormula(leftSubformula, rightSubformula), bounds(std::make_pair(lowerBound, upperBound)) { // Intentionally left empty. } - BoundedUntilFormula::BoundedUntilFormula(std::shared_ptr const& leftSubformula, std::shared_ptr const& rightSubformula, uint_fast64_t upperBound) : BinaryPathFormula(leftSubformula, rightSubformula), bounds(upperBound) { + BoundedUntilFormula::BoundedUntilFormula(std::shared_ptr const& leftSubformula, std::shared_ptr const& rightSubformula, uint_fast64_t upperBound) : BinaryPathFormula(leftSubformula, rightSubformula), bounds(upperBound) { // Intentionally left empty. } diff --git a/src/logic/BoundedUntilFormula.h b/src/logic/BoundedUntilFormula.h index ed7ac132e..8dc915041 100644 --- a/src/logic/BoundedUntilFormula.h +++ b/src/logic/BoundedUntilFormula.h @@ -9,8 +9,8 @@ namespace storm { namespace logic { class BoundedUntilFormula : public BinaryPathFormula { public: - BoundedUntilFormula(std::shared_ptr const& leftSubformula, std::shared_ptr const& rightSubformula, double lowerBound, double upperBound); - BoundedUntilFormula(std::shared_ptr const& leftSubformula, std::shared_ptr const& rightSubformula, uint_fast64_t upperBound); + BoundedUntilFormula(std::shared_ptr const& leftSubformula, std::shared_ptr const& rightSubformula, double lowerBound, double upperBound); + BoundedUntilFormula(std::shared_ptr const& leftSubformula, std::shared_ptr const& rightSubformula, uint_fast64_t upperBound); virtual bool isBoundedUntilFormula() const override; diff --git a/src/logic/ConditionalPathFormula.cpp b/src/logic/ConditionalPathFormula.cpp index 106a8d9a1..c1e7078b2 100644 --- a/src/logic/ConditionalPathFormula.cpp +++ b/src/logic/ConditionalPathFormula.cpp @@ -2,7 +2,7 @@ namespace storm { namespace logic { - ConditionalPathFormula::ConditionalPathFormula(std::shared_ptr const& leftSubformula, std::shared_ptr const& rightSubformula) : BinaryPathFormula(leftSubformula, rightSubformula) { + ConditionalPathFormula::ConditionalPathFormula(std::shared_ptr const& leftSubformula, std::shared_ptr const& rightSubformula) : BinaryPathFormula(leftSubformula, rightSubformula) { // Intentionally left empty. } diff --git a/src/logic/ConditionalPathFormula.h b/src/logic/ConditionalPathFormula.h index a65ee8b02..9cbfa7ccc 100644 --- a/src/logic/ConditionalPathFormula.h +++ b/src/logic/ConditionalPathFormula.h @@ -7,7 +7,7 @@ namespace storm { namespace logic { class ConditionalPathFormula : public BinaryPathFormula { public: - ConditionalPathFormula(std::shared_ptr const& leftSubformula, std::shared_ptr const& rightSubformula); + ConditionalPathFormula(std::shared_ptr const& leftSubformula, std::shared_ptr const& rightSubformula); virtual ~ConditionalPathFormula() { // Intentionally left empty. diff --git a/src/logic/CumulativeRewardFormula.cpp b/src/logic/CumulativeRewardFormula.cpp index dc0310c95..0c74d27f4 100644 --- a/src/logic/CumulativeRewardFormula.cpp +++ b/src/logic/CumulativeRewardFormula.cpp @@ -10,6 +10,10 @@ namespace storm { return true; } + uint_fast64_t CumulativeRewardFormula::getStepBound() const { + return stepBound; + } + std::ostream& CumulativeRewardFormula::writeToStream(std::ostream& out) const { out << "C<=" << stepBound; return out; diff --git a/src/logic/CumulativeRewardFormula.h b/src/logic/CumulativeRewardFormula.h index b3c10aad4..45cb761b4 100644 --- a/src/logic/CumulativeRewardFormula.h +++ b/src/logic/CumulativeRewardFormula.h @@ -1,11 +1,11 @@ #ifndef STORM_LOGIC_CUMULATIVEREWARDFORMULA_H_ #define STORM_LOGIC_CUMULATIVEREWARDFORMULA_H_ -#include "src/logic/PathRewardFormula.h" +#include "src/logic/RewardPathFormula.h" namespace storm { namespace logic { - class CumulativeRewardFormula : public PathRewardFormula { + class CumulativeRewardFormula : public RewardPathFormula { public: CumulativeRewardFormula(uint_fast64_t stepBound); @@ -17,6 +17,8 @@ namespace storm { virtual std::ostream& writeToStream(std::ostream& out) const override; + uint_fast64_t getStepBound() const; + private: uint_fast64_t stepBound; }; diff --git a/src/logic/EventuallyFormula.cpp b/src/logic/EventuallyFormula.cpp index 98fc063b2..30ca7fabe 100644 --- a/src/logic/EventuallyFormula.cpp +++ b/src/logic/EventuallyFormula.cpp @@ -2,7 +2,7 @@ namespace storm { namespace logic { - EventuallyFormula::EventuallyFormula(std::shared_ptr const& subformula) : UnaryPathFormula(subformula) { + EventuallyFormula::EventuallyFormula(std::shared_ptr const& subformula) : UnaryPathFormula(subformula) { // Intentionally left empty. } diff --git a/src/logic/EventuallyFormula.h b/src/logic/EventuallyFormula.h index 4b5ea2a9a..cf8a09e38 100644 --- a/src/logic/EventuallyFormula.h +++ b/src/logic/EventuallyFormula.h @@ -7,7 +7,7 @@ namespace storm { namespace logic { class EventuallyFormula : public UnaryPathFormula { public: - EventuallyFormula(std::shared_ptr const& subformula); + EventuallyFormula(std::shared_ptr const& subformula); virtual ~EventuallyFormula() { // Intentionally left empty. diff --git a/src/logic/Formula.cpp b/src/logic/Formula.cpp index d2f4d2527..cb9dd2a15 100644 --- a/src/logic/Formula.cpp +++ b/src/logic/Formula.cpp @@ -30,11 +30,11 @@ namespace storm { return false; } - bool Formula::isTrue() const { + bool Formula::isTrueFormula() const { return false; } - bool Formula::isFalse() const { + bool Formula::isFalseFormula() const { return false; } @@ -82,7 +82,7 @@ namespace storm { return false; } - bool Formula::isPathRewardFormula() const { + bool Formula::isRewardPathFormula() const { return false; } @@ -98,11 +98,11 @@ namespace storm { return false; } - bool Formula::isProbabilityOperator() const { + bool Formula::isProbabilityOperatorFormula() const { return false; } - bool Formula::isRewardOperator() const { + bool Formula::isRewardOperatorFormula() const { return false; } @@ -122,6 +122,10 @@ namespace storm { return false; } + std::shared_ptr Formula::getTrueFormula() { + return std::shared_ptr(new BooleanLiteralFormula(true)); + } + PathFormula& Formula::asPathFormula() { return dynamic_cast(*this); } @@ -258,20 +262,20 @@ namespace storm { return dynamic_cast(*this); } - SteadyStateOperatorFormula& Formula::asSteadyStateFormula() { + SteadyStateOperatorFormula& Formula::asSteadyStateOperatorFormula() { return dynamic_cast(*this); } - SteadyStateOperatorFormula const& Formula::asSteadyStateFormula() const { + SteadyStateOperatorFormula const& Formula::asSteadyStateOperatorFormula() const { return dynamic_cast(*this); } - PathRewardFormula& Formula::asPathRewardFormula() { - return dynamic_cast(*this); + RewardPathFormula& Formula::asRewardPathFormula() { + return dynamic_cast(*this); } - PathRewardFormula const& Formula::asPathRewardFormula() const { - return dynamic_cast(*this); + RewardPathFormula const& Formula::asRewardPathFormula() const { + return dynamic_cast(*this); } CumulativeRewardFormula& Formula::asCumulativeRewardFormula() { @@ -314,6 +318,14 @@ namespace storm { return dynamic_cast(*this); } + std::shared_ptr Formula::asSharedPointer() { + return this->shared_from_this(); + } + + std::shared_ptr Formula::asSharedPointer() const { + return this->shared_from_this(); + } + std::ostream& operator<<(std::ostream& out, Formula const& formula) { return formula.writeToStream(out); } diff --git a/src/logic/Formula.h b/src/logic/Formula.h index e3ab2063d..1ec49a4fe 100644 --- a/src/logic/Formula.h +++ b/src/logic/Formula.h @@ -27,7 +27,7 @@ namespace storm { class ConditionalPathFormula; class NextFormula; class SteadyStateOperatorFormula; - class PathRewardFormula; + class RewardPathFormula; class CumulativeRewardFormula; class InstantaneousRewardFormula; class ReachabilityRewardFormula; @@ -37,7 +37,7 @@ namespace storm { // Also foward-declare base model checker class. class ModelChecker; - class Formula { + class Formula : public std::enable_shared_from_this { public: // Make the destructor virtual to allow deletion of objects of subclasses via a pointer to this class. virtual ~Formula() { @@ -54,8 +54,8 @@ namespace storm { virtual bool isBinaryBooleanStateFormula() const; virtual bool isUnaryBooleanStateFormula() const; virtual bool isBooleanLiteralFormula() const; - virtual bool isTrue() const; - virtual bool isFalse() const; + virtual bool isTrueFormula() const; + virtual bool isFalseFormula() const; virtual bool isAtomicExpressionFormula() const; virtual bool isAtomicLabelFormula() const; virtual bool isUntilFormula() const; @@ -67,18 +67,20 @@ namespace storm { virtual bool isConditionalPathFormula() const; virtual bool isNextFormula() const; virtual bool isSteadyStateOperatorFormula() const; - virtual bool isPathRewardFormula() const; + virtual bool isRewardPathFormula() const; virtual bool isCumulativeRewardFormula() const; virtual bool isInstantaneousRewardFormula() const; virtual bool isReachabilityRewardFormula() const; - virtual bool isProbabilityOperator() const; - virtual bool isRewardOperator() const; + virtual bool isProbabilityOperatorFormula() const; + virtual bool isRewardOperatorFormula() const; virtual bool isPctlPathFormula() const; virtual bool isPctlStateFormula() const; virtual bool isPltlFormula() const; virtual bool isPropositionalFormula() const; + static std::shared_ptr getTrueFormula(); + PathFormula& asPathFormula(); PathFormula const& asPathFormula() const; @@ -130,11 +132,11 @@ namespace storm { NextFormula& asNextFormula(); NextFormula const& asNextFormula() const; - SteadyStateOperatorFormula& asSteadyStateFormula(); - SteadyStateOperatorFormula const& asSteadyStateFormula() const; + SteadyStateOperatorFormula& asSteadyStateOperatorFormula(); + SteadyStateOperatorFormula const& asSteadyStateOperatorFormula() const; - PathRewardFormula& asPathRewardFormula(); - PathRewardFormula const& asPathRewardFormula() const; + RewardPathFormula& asRewardPathFormula(); + RewardPathFormula const& asRewardPathFormula() const; CumulativeRewardFormula& asCumulativeRewardFormula(); CumulativeRewardFormula const& asCumulativeRewardFormula() const; @@ -151,6 +153,9 @@ namespace storm { RewardOperatorFormula& asRewardOperatorFormula(); RewardOperatorFormula const& asRewardOperatorFormula() const; + std::shared_ptr asSharedPointer(); + std::shared_ptr asSharedPointer() const; + virtual std::ostream& writeToStream(std::ostream& out) const = 0; private: diff --git a/src/logic/Formulas.h b/src/logic/Formulas.h index 99b3742ef..ee6355535 100644 --- a/src/logic/Formulas.h +++ b/src/logic/Formulas.h @@ -12,6 +12,7 @@ #include "src/logic/InstantaneousRewardFormula.h" #include "src/logic/NextFormula.h" #include "src/logic/PathFormula.h" +#include "src/logic/RewardPathFormula.h" #include "src/logic/ProbabilityOperatorFormula.h" #include "src/logic/ReachabilityRewardFormula.h" #include "src/logic/RewardOperatorFormula.h" diff --git a/src/logic/GloballyFormula.cpp b/src/logic/GloballyFormula.cpp index 7874bc3dd..f4f6935dd 100644 --- a/src/logic/GloballyFormula.cpp +++ b/src/logic/GloballyFormula.cpp @@ -2,7 +2,7 @@ namespace storm { namespace logic { - GloballyFormula::GloballyFormula(std::shared_ptr const& subformula) : UnaryPathFormula(subformula) { + GloballyFormula::GloballyFormula(std::shared_ptr const& subformula) : UnaryPathFormula(subformula) { // Intentionally left empty. } diff --git a/src/logic/GloballyFormula.h b/src/logic/GloballyFormula.h index ae09f87bb..043a9849e 100644 --- a/src/logic/GloballyFormula.h +++ b/src/logic/GloballyFormula.h @@ -7,7 +7,7 @@ namespace storm { namespace logic { class GloballyFormula : public UnaryPathFormula { public: - GloballyFormula(std::shared_ptr const& subformula); + GloballyFormula(std::shared_ptr const& subformula); virtual ~GloballyFormula() { // Intentionally left empty. diff --git a/src/logic/InstantaneousRewardFormula.cpp b/src/logic/InstantaneousRewardFormula.cpp index 7573476a0..41234d1ab 100644 --- a/src/logic/InstantaneousRewardFormula.cpp +++ b/src/logic/InstantaneousRewardFormula.cpp @@ -10,6 +10,10 @@ namespace storm { return true; } + uint_fast64_t InstantaneousRewardFormula::getStepCount() const { + return stepCount; + } + std::ostream& InstantaneousRewardFormula::writeToStream(std::ostream& out) const { out << "I=" << stepCount; return out; diff --git a/src/logic/InstantaneousRewardFormula.h b/src/logic/InstantaneousRewardFormula.h index a835e29bd..c83afdc85 100644 --- a/src/logic/InstantaneousRewardFormula.h +++ b/src/logic/InstantaneousRewardFormula.h @@ -1,11 +1,11 @@ #ifndef STORM_LOGIC_INSTANTANEOUSREWARDFORMULA_H_ #define STORM_LOGIC_INSTANTANEOUSREWARDFORMULA_H_ -#include "src/logic/PathRewardFormula.h" +#include "src/logic/RewardPathFormula.h" namespace storm { namespace logic { - class InstantaneousRewardFormula : public PathRewardFormula { + class InstantaneousRewardFormula : public RewardPathFormula { public: InstantaneousRewardFormula(uint_fast64_t stepCount); @@ -17,6 +17,8 @@ namespace storm { virtual std::ostream& writeToStream(std::ostream& out) const override; + uint_fast64_t getStepCount() const; + private: uint_fast64_t stepCount; }; diff --git a/src/logic/NextFormula.cpp b/src/logic/NextFormula.cpp index cc98be661..37f4c4b3f 100644 --- a/src/logic/NextFormula.cpp +++ b/src/logic/NextFormula.cpp @@ -2,7 +2,7 @@ namespace storm { namespace logic { - NextFormula::NextFormula(std::shared_ptr const& subformula) : UnaryPathFormula(subformula) { + NextFormula::NextFormula(std::shared_ptr const& subformula) : UnaryPathFormula(subformula) { // Intentionally left empty. } diff --git a/src/logic/NextFormula.h b/src/logic/NextFormula.h index e9659ddfe..186f81e51 100644 --- a/src/logic/NextFormula.h +++ b/src/logic/NextFormula.h @@ -7,7 +7,7 @@ namespace storm { namespace logic { class NextFormula : public UnaryPathFormula { public: - NextFormula(std::shared_ptr const& subformula); + NextFormula(std::shared_ptr const& subformula); virtual ~NextFormula() { // Intentionally left empty. diff --git a/src/logic/OperatorFormula.cpp b/src/logic/OperatorFormula.cpp index 31e56c042..d9faaf057 100644 --- a/src/logic/OperatorFormula.cpp +++ b/src/logic/OperatorFormula.cpp @@ -2,7 +2,7 @@ namespace storm { namespace logic { - OperatorFormula::OperatorFormula(boost::optional optimalityType, boost::optional comparisonType, boost::optional bound, std::shared_ptr const& subformula) : UnaryStateFormula(subformula), comparisonType(comparisonType), bound(bound), optimalityType(optimalityType) { + OperatorFormula::OperatorFormula(boost::optional optimalityType, boost::optional comparisonType, boost::optional bound, std::shared_ptr const& subformula) : UnaryStateFormula(subformula), comparisonType(comparisonType), bound(bound), optimalityType(optimalityType) { // Intentionally left empty. } diff --git a/src/logic/OperatorFormula.h b/src/logic/OperatorFormula.h index 753c44f4a..d1ce2ee78 100644 --- a/src/logic/OperatorFormula.h +++ b/src/logic/OperatorFormula.h @@ -11,7 +11,7 @@ namespace storm { namespace logic { class OperatorFormula : public UnaryStateFormula { public: - OperatorFormula(boost::optional optimalityType, boost::optional comparisonType, boost::optional bound, std::shared_ptr const& subformula); + OperatorFormula(boost::optional optimalityType, boost::optional comparisonType, boost::optional bound, std::shared_ptr const& subformula); virtual ~OperatorFormula() { // Intentionally left empty. diff --git a/src/logic/PathRewardFormula.cpp b/src/logic/PathRewardFormula.cpp deleted file mode 100644 index db13399a1..000000000 --- a/src/logic/PathRewardFormula.cpp +++ /dev/null @@ -1,9 +0,0 @@ -#include "src/logic/PathRewardFormula.h" - -namespace storm { - namespace logic { - bool PathRewardFormula::isPathRewardFormula() const { - return true; - } - } -} \ No newline at end of file diff --git a/src/logic/ProbabilityOperatorFormula.cpp b/src/logic/ProbabilityOperatorFormula.cpp index 3b96dc81f..3573d8bc4 100644 --- a/src/logic/ProbabilityOperatorFormula.cpp +++ b/src/logic/ProbabilityOperatorFormula.cpp @@ -2,27 +2,27 @@ namespace storm { namespace logic { - ProbabilityOperatorFormula::ProbabilityOperatorFormula(std::shared_ptr const& subformula) : ProbabilityOperatorFormula(boost::optional(), boost::optional(), boost::optional(), subformula) { + ProbabilityOperatorFormula::ProbabilityOperatorFormula(std::shared_ptr const& subformula) : ProbabilityOperatorFormula(boost::optional(), boost::optional(), boost::optional(), subformula) { // Intentionally left empty. } - ProbabilityOperatorFormula::ProbabilityOperatorFormula(ComparisonType comparisonType, double bound, std::shared_ptr const& subformula) : ProbabilityOperatorFormula(boost::optional(), boost::optional(comparisonType), boost::optional(bound), subformula) { + ProbabilityOperatorFormula::ProbabilityOperatorFormula(ComparisonType comparisonType, double bound, std::shared_ptr const& subformula) : ProbabilityOperatorFormula(boost::optional(), boost::optional(comparisonType), boost::optional(bound), subformula) { // Intentionally left empty. } - ProbabilityOperatorFormula::ProbabilityOperatorFormula(OptimalityType optimalityType, ComparisonType comparisonType, double bound, std::shared_ptr const& subformula) : ProbabilityOperatorFormula(boost::optional(optimalityType), boost::optional(comparisonType), boost::optional(bound), subformula) { + ProbabilityOperatorFormula::ProbabilityOperatorFormula(OptimalityType optimalityType, ComparisonType comparisonType, double bound, std::shared_ptr const& subformula) : ProbabilityOperatorFormula(boost::optional(optimalityType), boost::optional(comparisonType), boost::optional(bound), subformula) { // Intentionally left empty. } - ProbabilityOperatorFormula::ProbabilityOperatorFormula(OptimalityType optimalityType, std::shared_ptr const& subformula) : ProbabilityOperatorFormula(boost::optional(optimalityType), boost::optional(), boost::optional(), subformula) { + ProbabilityOperatorFormula::ProbabilityOperatorFormula(OptimalityType optimalityType, std::shared_ptr const& subformula) : ProbabilityOperatorFormula(boost::optional(optimalityType), boost::optional(), boost::optional(), subformula) { // Intentionally left empty. } - bool ProbabilityOperatorFormula::isProbabilityOperator() const { + bool ProbabilityOperatorFormula::isProbabilityOperatorFormula() const { return true; } - ProbabilityOperatorFormula::ProbabilityOperatorFormula(boost::optional optimalityType, boost::optional comparisonType, boost::optional bound, std::shared_ptr const& subformula) : OperatorFormula(optimalityType, comparisonType, bound, subformula) { + ProbabilityOperatorFormula::ProbabilityOperatorFormula(boost::optional optimalityType, boost::optional comparisonType, boost::optional bound, std::shared_ptr const& subformula) : OperatorFormula(optimalityType, comparisonType, bound, subformula) { // Intentionally left empty. } diff --git a/src/logic/ProbabilityOperatorFormula.h b/src/logic/ProbabilityOperatorFormula.h index d22d24dfa..394a50a3c 100644 --- a/src/logic/ProbabilityOperatorFormula.h +++ b/src/logic/ProbabilityOperatorFormula.h @@ -7,17 +7,17 @@ namespace storm { namespace logic { class ProbabilityOperatorFormula : public OperatorFormula { public: - ProbabilityOperatorFormula(std::shared_ptr const& subformula); - ProbabilityOperatorFormula(ComparisonType comparisonType, double bound, std::shared_ptr const& subformula); - ProbabilityOperatorFormula(OptimalityType optimalityType, ComparisonType comparisonType, double bound, std::shared_ptr const& subformula); - ProbabilityOperatorFormula(OptimalityType optimalityType, std::shared_ptr const& subformula); - ProbabilityOperatorFormula(boost::optional optimalityType, boost::optional comparisonType, boost::optional bound, std::shared_ptr const& subformula); + ProbabilityOperatorFormula(std::shared_ptr const& subformula); + ProbabilityOperatorFormula(ComparisonType comparisonType, double bound, std::shared_ptr const& subformula); + ProbabilityOperatorFormula(OptimalityType optimalityType, ComparisonType comparisonType, double bound, std::shared_ptr const& subformula); + ProbabilityOperatorFormula(OptimalityType optimalityType, std::shared_ptr const& subformula); + ProbabilityOperatorFormula(boost::optional optimalityType, boost::optional comparisonType, boost::optional bound, std::shared_ptr const& subformula); virtual ~ProbabilityOperatorFormula() { // Intentionally left empty. } - virtual bool isProbabilityOperator() const override; + virtual bool isProbabilityOperatorFormula() const override; virtual std::ostream& writeToStream(std::ostream& out) const override; }; diff --git a/src/logic/ReachabilityRewardFormula.cpp b/src/logic/ReachabilityRewardFormula.cpp index cc11e074d..a3d85dca8 100644 --- a/src/logic/ReachabilityRewardFormula.cpp +++ b/src/logic/ReachabilityRewardFormula.cpp @@ -2,7 +2,7 @@ namespace storm { namespace logic { - ReachabilityRewardFormula::ReachabilityRewardFormula(std::shared_ptr const& subformula) : subformula(subformula) { + ReachabilityRewardFormula::ReachabilityRewardFormula(std::shared_ptr const& subformula) : subformula(subformula) { // Intentionally left empty. } @@ -10,10 +10,6 @@ namespace storm { return true; } - Formula& ReachabilityRewardFormula::getSubformula() { - return *subformula; - } - Formula const& ReachabilityRewardFormula::getSubformula() const { return *subformula; } diff --git a/src/logic/ReachabilityRewardFormula.h b/src/logic/ReachabilityRewardFormula.h index 28596f567..7bc9564e8 100644 --- a/src/logic/ReachabilityRewardFormula.h +++ b/src/logic/ReachabilityRewardFormula.h @@ -3,14 +3,14 @@ #include -#include "src/logic/PathRewardFormula.h" +#include "src/logic/RewardPathFormula.h" #include "src/logic/StateFormula.h" namespace storm { namespace logic { - class ReachabilityRewardFormula : public PathRewardFormula { + class ReachabilityRewardFormula : public RewardPathFormula { public: - ReachabilityRewardFormula(std::shared_ptr const& subformula); + ReachabilityRewardFormula(std::shared_ptr const& subformula); virtual ~ReachabilityRewardFormula() { // Intentionally left empty. @@ -18,13 +18,12 @@ namespace storm { virtual bool isReachabilityRewardFormula() const override; - Formula& getSubformula(); Formula const& getSubformula() const; virtual std::ostream& writeToStream(std::ostream& out) const override; private: - std::shared_ptr const& subformula; + std::shared_ptr subformula; }; } } diff --git a/src/logic/RewardOperatorFormula.cpp b/src/logic/RewardOperatorFormula.cpp index 4b6f0c288..f8eac5e4c 100644 --- a/src/logic/RewardOperatorFormula.cpp +++ b/src/logic/RewardOperatorFormula.cpp @@ -2,27 +2,27 @@ namespace storm { namespace logic { - RewardOperatorFormula::RewardOperatorFormula(std::shared_ptr const& subformula) : RewardOperatorFormula(boost::optional(), boost::optional(), boost::optional(), subformula) { + RewardOperatorFormula::RewardOperatorFormula(std::shared_ptr const& subformula) : RewardOperatorFormula(boost::optional(), boost::optional(), boost::optional(), subformula) { // Intentionally left empty. } - RewardOperatorFormula::RewardOperatorFormula(ComparisonType comparisonType, double bound, std::shared_ptr const& subformula) : RewardOperatorFormula(boost::optional(), boost::optional(comparisonType), boost::optional(bound), subformula) { + RewardOperatorFormula::RewardOperatorFormula(ComparisonType comparisonType, double bound, std::shared_ptr const& subformula) : RewardOperatorFormula(boost::optional(), boost::optional(comparisonType), boost::optional(bound), subformula) { // Intentionally left empty. } - RewardOperatorFormula::RewardOperatorFormula(OptimalityType optimalityType, ComparisonType comparisonType, double bound, std::shared_ptr const& subformula) : RewardOperatorFormula(boost::optional(optimalityType), boost::optional(comparisonType), boost::optional(bound), subformula) { + RewardOperatorFormula::RewardOperatorFormula(OptimalityType optimalityType, ComparisonType comparisonType, double bound, std::shared_ptr const& subformula) : RewardOperatorFormula(boost::optional(optimalityType), boost::optional(comparisonType), boost::optional(bound), subformula) { // Intentionally left empty. } - RewardOperatorFormula::RewardOperatorFormula(OptimalityType optimalityType, std::shared_ptr const& subformula) : RewardOperatorFormula(boost::optional(optimalityType), boost::optional(), boost::optional(), subformula) { + RewardOperatorFormula::RewardOperatorFormula(OptimalityType optimalityType, std::shared_ptr const& subformula) : RewardOperatorFormula(boost::optional(optimalityType), boost::optional(), boost::optional(), subformula) { // Intentionally left empty. } - bool RewardOperatorFormula::isRewardOperator() const { + bool RewardOperatorFormula::isRewardOperatorFormula() const { return true; } - RewardOperatorFormula::RewardOperatorFormula(boost::optional optimalityType, boost::optional comparisonType, boost::optional bound, std::shared_ptr const& subformula) : OperatorFormula(optimalityType, comparisonType, bound, subformula) { + RewardOperatorFormula::RewardOperatorFormula(boost::optional optimalityType, boost::optional comparisonType, boost::optional bound, std::shared_ptr const& subformula) : OperatorFormula(optimalityType, comparisonType, bound, subformula) { // Intentionally left empty. } diff --git a/src/logic/RewardOperatorFormula.h b/src/logic/RewardOperatorFormula.h index dc198f062..37d84c066 100644 --- a/src/logic/RewardOperatorFormula.h +++ b/src/logic/RewardOperatorFormula.h @@ -7,17 +7,17 @@ namespace storm { namespace logic { class RewardOperatorFormula : public OperatorFormula { public: - RewardOperatorFormula(std::shared_ptr const& subformula); - RewardOperatorFormula(ComparisonType comparisonType, double bound, std::shared_ptr const& subformula); - RewardOperatorFormula(OptimalityType optimalityType, ComparisonType comparisonType, double bound, std::shared_ptr const& subformula); - RewardOperatorFormula(OptimalityType optimalityType, std::shared_ptr const& subformula); - RewardOperatorFormula(boost::optional optimalityType, boost::optional comparisonType, boost::optional bound, std::shared_ptr const& subformula); + RewardOperatorFormula(std::shared_ptr const& subformula); + RewardOperatorFormula(ComparisonType comparisonType, double bound, std::shared_ptr const& subformula); + RewardOperatorFormula(OptimalityType optimalityType, ComparisonType comparisonType, double bound, std::shared_ptr const& subformula); + RewardOperatorFormula(OptimalityType optimalityType, std::shared_ptr const& subformula); + RewardOperatorFormula(boost::optional optimalityType, boost::optional comparisonType, boost::optional bound, std::shared_ptr const& subformula); virtual ~RewardOperatorFormula() { // Intentionally left empty. } - virtual bool isRewardOperator() const override; + virtual bool isRewardOperatorFormula() const override; virtual std::ostream& writeToStream(std::ostream& out) const override; }; diff --git a/src/logic/RewardPathFormula.cpp b/src/logic/RewardPathFormula.cpp new file mode 100644 index 000000000..3c97acf74 --- /dev/null +++ b/src/logic/RewardPathFormula.cpp @@ -0,0 +1,9 @@ +#include "src/logic/RewardPathFormula.h" + +namespace storm { + namespace logic { + bool RewardPathFormula::isRewardPathFormula() const { + return true; + } + } +} \ No newline at end of file diff --git a/src/logic/PathRewardFormula.h b/src/logic/RewardPathFormula.h similarity index 56% rename from src/logic/PathRewardFormula.h rename to src/logic/RewardPathFormula.h index 91e340ebb..023e76e2d 100644 --- a/src/logic/PathRewardFormula.h +++ b/src/logic/RewardPathFormula.h @@ -5,13 +5,13 @@ namespace storm { namespace logic { - class PathRewardFormula : public PathFormula { + class RewardPathFormula : public Formula { public: - virtual ~PathRewardFormula() { + virtual ~RewardPathFormula() { // Intentionally left empty. } - virtual bool isPathRewardFormula() const override; + virtual bool isRewardPathFormula() const override; }; } } diff --git a/src/logic/SteadyStateOperatorFormula.cpp b/src/logic/SteadyStateOperatorFormula.cpp index 945798bcb..7edb04400 100644 --- a/src/logic/SteadyStateOperatorFormula.cpp +++ b/src/logic/SteadyStateOperatorFormula.cpp @@ -2,19 +2,19 @@ namespace storm { namespace logic { - SteadyStateOperatorFormula::SteadyStateOperatorFormula(std::shared_ptr const& subformula) : SteadyStateOperatorFormula(boost::optional(), boost::optional(), boost::optional(), subformula) { + SteadyStateOperatorFormula::SteadyStateOperatorFormula(std::shared_ptr const& subformula) : SteadyStateOperatorFormula(boost::optional(), boost::optional(), boost::optional(), subformula) { // Intentionally left empty. } - SteadyStateOperatorFormula::SteadyStateOperatorFormula(ComparisonType comparisonType, double bound, std::shared_ptr const& subformula) : SteadyStateOperatorFormula(boost::optional(), boost::optional(comparisonType), boost::optional(bound), subformula) { + SteadyStateOperatorFormula::SteadyStateOperatorFormula(ComparisonType comparisonType, double bound, std::shared_ptr const& subformula) : SteadyStateOperatorFormula(boost::optional(), boost::optional(comparisonType), boost::optional(bound), subformula) { // Intentionally left empty. } - SteadyStateOperatorFormula::SteadyStateOperatorFormula(OptimalityType optimalityType, ComparisonType comparisonType, double bound, std::shared_ptr const& subformula) : SteadyStateOperatorFormula(boost::optional(optimalityType), boost::optional(comparisonType), boost::optional(bound), subformula) { + SteadyStateOperatorFormula::SteadyStateOperatorFormula(OptimalityType optimalityType, ComparisonType comparisonType, double bound, std::shared_ptr const& subformula) : SteadyStateOperatorFormula(boost::optional(optimalityType), boost::optional(comparisonType), boost::optional(bound), subformula) { // Intentionally left empty. } - SteadyStateOperatorFormula::SteadyStateOperatorFormula(OptimalityType optimalityType, std::shared_ptr const& subformula) : SteadyStateOperatorFormula(boost::optional(optimalityType), boost::optional(), boost::optional(), subformula) { + SteadyStateOperatorFormula::SteadyStateOperatorFormula(OptimalityType optimalityType, std::shared_ptr const& subformula) : SteadyStateOperatorFormula(boost::optional(optimalityType), boost::optional(), boost::optional(), subformula) { // Intentionally left empty. } @@ -22,7 +22,7 @@ namespace storm { return true; } - SteadyStateOperatorFormula::SteadyStateOperatorFormula(boost::optional optimalityType, boost::optional comparisonType, boost::optional bound, std::shared_ptr const& subformula) : OperatorFormula(optimalityType, comparisonType, bound, subformula) { + SteadyStateOperatorFormula::SteadyStateOperatorFormula(boost::optional optimalityType, boost::optional comparisonType, boost::optional bound, std::shared_ptr const& subformula) : OperatorFormula(optimalityType, comparisonType, bound, subformula) { // Intentionally left empty. } diff --git a/src/logic/SteadyStateOperatorFormula.h b/src/logic/SteadyStateOperatorFormula.h index 6e174801b..68f682c41 100644 --- a/src/logic/SteadyStateOperatorFormula.h +++ b/src/logic/SteadyStateOperatorFormula.h @@ -7,11 +7,11 @@ namespace storm { namespace logic { class SteadyStateOperatorFormula : public OperatorFormula { public: - SteadyStateOperatorFormula(std::shared_ptr const& subformula); - SteadyStateOperatorFormula(ComparisonType comparisonType, double bound, std::shared_ptr const& subformula); - SteadyStateOperatorFormula(OptimalityType optimalityType, ComparisonType comparisonType, double bound, std::shared_ptr const& subformula); - SteadyStateOperatorFormula(OptimalityType optimalityType, std::shared_ptr const& subformula); - SteadyStateOperatorFormula(boost::optional optimalityType, boost::optional comparisonType, boost::optional bound, std::shared_ptr const& subformula); + SteadyStateOperatorFormula(std::shared_ptr const& subformula); + SteadyStateOperatorFormula(ComparisonType comparisonType, double bound, std::shared_ptr const& subformula); + SteadyStateOperatorFormula(OptimalityType optimalityType, ComparisonType comparisonType, double bound, std::shared_ptr const& subformula); + SteadyStateOperatorFormula(OptimalityType optimalityType, std::shared_ptr const& subformula); + SteadyStateOperatorFormula(boost::optional optimalityType, boost::optional comparisonType, boost::optional bound, std::shared_ptr const& subformula); virtual ~SteadyStateOperatorFormula() { // Intentionally left empty. diff --git a/src/logic/UnaryBooleanStateFormula.cpp b/src/logic/UnaryBooleanStateFormula.cpp index a54b3a16c..09ee894e0 100644 --- a/src/logic/UnaryBooleanStateFormula.cpp +++ b/src/logic/UnaryBooleanStateFormula.cpp @@ -2,7 +2,7 @@ namespace storm { namespace logic { - UnaryBooleanStateFormula::UnaryBooleanStateFormula(OperatorType operatorType, std::shared_ptr const& subformula) : UnaryStateFormula(subformula), operatorType(operatorType) { + UnaryBooleanStateFormula::UnaryBooleanStateFormula(OperatorType operatorType, std::shared_ptr const& subformula) : UnaryStateFormula(subformula), operatorType(operatorType) { // Intentionally left empty. } diff --git a/src/logic/UnaryBooleanStateFormula.h b/src/logic/UnaryBooleanStateFormula.h index 2e9fd5793..37d6a82ae 100644 --- a/src/logic/UnaryBooleanStateFormula.h +++ b/src/logic/UnaryBooleanStateFormula.h @@ -9,7 +9,7 @@ namespace storm { public: enum class OperatorType { Not }; - UnaryBooleanStateFormula(OperatorType operatorType, std::shared_ptr const& subformula); + UnaryBooleanStateFormula(OperatorType operatorType, std::shared_ptr const& subformula); virtual ~UnaryBooleanStateFormula() { // Intentionally left empty. diff --git a/src/logic/UnaryPathFormula.cpp b/src/logic/UnaryPathFormula.cpp index 25d20bbab..6d5f0f0c2 100644 --- a/src/logic/UnaryPathFormula.cpp +++ b/src/logic/UnaryPathFormula.cpp @@ -2,18 +2,14 @@ namespace storm { namespace logic { - UnaryPathFormula::UnaryPathFormula(std::shared_ptr const& subformula) : subformula(subformula) { + UnaryPathFormula::UnaryPathFormula(std::shared_ptr const& subformula) : subformula(subformula) { // Intentionally left empty. } bool UnaryPathFormula::isUnaryPathFormula() const { return true; } - - Formula& UnaryPathFormula::getSubformula() { - return *subformula; - } - + Formula const& UnaryPathFormula::getSubformula() const { return *subformula; } diff --git a/src/logic/UnaryPathFormula.h b/src/logic/UnaryPathFormula.h index 2115cf411..e1f425a36 100644 --- a/src/logic/UnaryPathFormula.h +++ b/src/logic/UnaryPathFormula.h @@ -9,7 +9,7 @@ namespace storm { namespace logic { class UnaryPathFormula : public PathFormula { public: - UnaryPathFormula(std::shared_ptr const& subformula); + UnaryPathFormula(std::shared_ptr const& subformula); virtual ~UnaryPathFormula() { // Intentionally left empty. @@ -17,11 +17,10 @@ namespace storm { virtual bool isUnaryPathFormula() const override; - Formula& getSubformula(); Formula const& getSubformula() const; private: - std::shared_ptr subformula; + std::shared_ptr subformula; }; } } diff --git a/src/logic/UnaryStateFormula.cpp b/src/logic/UnaryStateFormula.cpp index ee6a5a8c0..a86832338 100644 --- a/src/logic/UnaryStateFormula.cpp +++ b/src/logic/UnaryStateFormula.cpp @@ -2,7 +2,7 @@ namespace storm { namespace logic { - UnaryStateFormula::UnaryStateFormula(std::shared_ptr subformula) : subformula(subformula) { + UnaryStateFormula::UnaryStateFormula(std::shared_ptr subformula) : subformula(subformula) { // Intentionally left empty. } @@ -14,10 +14,6 @@ namespace storm { return this->getSubformula().isPropositionalFormula(); } - Formula& UnaryStateFormula::getSubformula() { - return *subformula; - } - Formula const& UnaryStateFormula::getSubformula() const { return *subformula; } diff --git a/src/logic/UnaryStateFormula.h b/src/logic/UnaryStateFormula.h index 0f6791a20..db758cf8b 100644 --- a/src/logic/UnaryStateFormula.h +++ b/src/logic/UnaryStateFormula.h @@ -7,7 +7,7 @@ namespace storm { namespace logic { class UnaryStateFormula : public StateFormula { public: - UnaryStateFormula(std::shared_ptr subformula); + UnaryStateFormula(std::shared_ptr subformula); virtual ~UnaryStateFormula() { // Intentionally left empty. @@ -16,11 +16,10 @@ namespace storm { virtual bool isUnaryStateFormula() const override; virtual bool isPropositionalFormula() const override; - Formula& getSubformula(); Formula const& getSubformula() const; private: - std::shared_ptr subformula; + std::shared_ptr subformula; }; } } diff --git a/src/logic/UntilFormula.cpp b/src/logic/UntilFormula.cpp index 450e16f2c..74893fa68 100644 --- a/src/logic/UntilFormula.cpp +++ b/src/logic/UntilFormula.cpp @@ -2,7 +2,7 @@ namespace storm { namespace logic { - UntilFormula::UntilFormula(std::shared_ptr const& leftSubformula, std::shared_ptr const& rightSubformula) : BinaryPathFormula(leftSubformula, rightSubformula) { + UntilFormula::UntilFormula(std::shared_ptr const& leftSubformula, std::shared_ptr const& rightSubformula) : BinaryPathFormula(leftSubformula, rightSubformula) { // Intentionally left empty. } diff --git a/src/logic/UntilFormula.h b/src/logic/UntilFormula.h index 790a9457d..a0c80cecf 100644 --- a/src/logic/UntilFormula.h +++ b/src/logic/UntilFormula.h @@ -7,7 +7,7 @@ namespace storm { namespace logic { class UntilFormula : public BinaryPathFormula { public: - UntilFormula(std::shared_ptr const& leftSubformula, std::shared_ptr const& rightSubformula); + UntilFormula(std::shared_ptr const& leftSubformula, std::shared_ptr const& rightSubformula); virtual ~UntilFormula() { // Intentionally left empty. diff --git a/src/modelchecker/AbstractModelChecker.cpp b/src/modelchecker/AbstractModelChecker.cpp new file mode 100644 index 000000000..ffe29f012 --- /dev/null +++ b/src/modelchecker/AbstractModelChecker.cpp @@ -0,0 +1,171 @@ +#include "src/modelchecker/AbstractModelChecker.h" + +#include "src/utility/ConstantsComparator.h" +#include "src/utility/macros.h" +#include "src/exceptions/NotImplementedException.h" + +namespace storm { + namespace modelchecker { + std::unique_ptr AbstractModelChecker::check(storm::logic::Formula const& formula) { + STORM_LOG_THROW(this->canHandle(formula), storm::exceptions::InvalidArgumentException, "The model checker is not able to check this formula."); + if (formula.isStateFormula()) { + return this->checkStateFormula(formula.asStateFormula()); + } else if (formula.isPathFormula()) { + return this->computeProbabilities(formula.asPathFormula()); + } else if (formula.isRewardPathFormula()) { + return this->computeRewards(formula.asRewardPathFormula()); + } + STORM_LOG_THROW(false, storm::exceptions::InvalidArgumentException, "The given formula is invalid."); + } + + std::unique_ptr AbstractModelChecker::computeProbabilities(storm::logic::PathFormula const& pathFormula, bool qualitative, boost::optional const& optimalityType) { + if (pathFormula.isBoundedUntilFormula()) { + return this->computeBoundedUntilProbabilities(pathFormula.asBoundedUntilFormula()); + } else if (pathFormula.isConditionalPathFormula()) { + return this->computeConditionalProbabilities(pathFormula.asConditionalPathFormula()); + } else if (pathFormula.isEventuallyFormula()) { + return this->computeEventuallyProbabilities(pathFormula.asEventuallyFormula()); + } else if (pathFormula.isGloballyFormula()) { + return this->computeGloballyProbabilities(pathFormula.asGloballyFormula()); + } else if (pathFormula.isUntilFormula()) { + return this->computeUntilProbabilities(pathFormula.asUntilFormula()); + } + STORM_LOG_THROW(false, storm::exceptions::InvalidArgumentException, "The given formula is invalid."); + } + + std::unique_ptr AbstractModelChecker::computeBoundedUntilProbabilities(storm::logic::BoundedUntilFormula const& pathFormula, bool qualitative, boost::optional const& optimalityType) { + STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "This model checker does not support the formula: " << pathFormula << "."); + } + + std::unique_ptr AbstractModelChecker::computeConditionalProbabilities(storm::logic::ConditionalPathFormula const& pathFormula, bool qualitative, boost::optional const& optimalityType) { + STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "This model checker does not support the formula: " << pathFormula << "."); + } + + std::unique_ptr AbstractModelChecker::computeEventuallyProbabilities(storm::logic::EventuallyFormula const& pathFormula, bool qualitative, boost::optional const& optimalityType) { + storm::logic::UntilFormula newFormula(storm::logic::Formula::getTrueFormula(), pathFormula.getSubformula().asSharedPointer()); + return this->check(newFormula); + } + + std::unique_ptr AbstractModelChecker::computeGloballyProbabilities(storm::logic::GloballyFormula const& pathFormula, bool qualitative, boost::optional const& optimalityType) { + STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "This model checker does not support the formula: " << pathFormula << "."); + } + + std::unique_ptr AbstractModelChecker::computeNextProbabilities(storm::logic::NextFormula const& pathFormula, bool qualitative, boost::optional const& optimalityType) { + STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "This model checker does not support the formula: " << pathFormula << "."); + } + + std::unique_ptr AbstractModelChecker::computeUntilProbabilities(storm::logic::UntilFormula const& pathFormula, bool qualitative, boost::optional const& optimalityType) { + STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "This model checker does not support the formula: " << pathFormula << "."); + } + + std::unique_ptr AbstractModelChecker::computeRewards(storm::logic::RewardPathFormula const& rewardPathFormula, bool qualitative, boost::optional const& optimalityType) { + if (rewardPathFormula.isCumulativeRewardFormula()) { + return this->computeCumulativeRewards(rewardPathFormula.asCumulativeRewardFormula()); + } else if (rewardPathFormula.isInstantaneousRewardFormula()) { + return this->computeInstantaneousRewards(rewardPathFormula.asInstantaneousRewardFormula()); + } else if (rewardPathFormula.isReachabilityRewardFormula()) { + return this->computeReachabilityRewards(rewardPathFormula.asReachabilityRewardFormula()); + } + STORM_LOG_THROW(false, storm::exceptions::InvalidArgumentException, "The given formula is invalid."); + } + + std::unique_ptr AbstractModelChecker::computeCumulativeRewards(storm::logic::CumulativeRewardFormula const& rewardPathFormula, bool qualitative, boost::optional const& optimalityType) { + STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "This model checker does not support the formula: " << rewardPathFormula << "."); + } + + std::unique_ptr AbstractModelChecker::computeInstantaneousRewards(storm::logic::InstantaneousRewardFormula const& rewardPathFormula, bool qualitative, boost::optional const& optimalityType) { + STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "This model checker does not support the formula: " << rewardPathFormula << "."); + } + + std::unique_ptr AbstractModelChecker::computeReachabilityRewards(storm::logic::ReachabilityRewardFormula const& rewardPathFormula, bool qualitative, boost::optional const& optimalityType) { + STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "This model checker does not support the formula: " << rewardPathFormula << "."); + } + + std::unique_ptr AbstractModelChecker::checkStateFormula(storm::logic::StateFormula const& stateFormula) { + if (stateFormula.isBinaryBooleanStateFormula()) { + return this->checkBinaryBooleanStateFormula(stateFormula.asBinaryBooleanStateFormula()); + } else if (stateFormula.isBooleanLiteralFormula()) { + return this->checkBooleanLiteralFormula(stateFormula.asBooleanLiteralFormula()); + } else if (stateFormula.isProbabilityOperatorFormula()) { + return this->checkProbabilityOperatorFormula(stateFormula.asProbabilityOperatorFormula()); + } else if (stateFormula.isRewardOperatorFormula()) { + return this->checkRewardOperatorFormula(stateFormula.asRewardOperatorFormula()); + } else if (stateFormula.isSteadyStateOperatorFormula()) { + return this->checkSteadyStateOperatorFormula(stateFormula.asSteadyStateOperatorFormula()); + } else if (stateFormula.isAtomicExpressionFormula()) { + return this->checkAtomicExpressionFormula(stateFormula.asAtomicExpressionFormula()); + } else if (stateFormula.isAtomicLabelFormula()) { + return this->checkAtomicLabelFormula(stateFormula.asAtomicLabelFormula()); + } else if (stateFormula.isBooleanLiteralFormula()) { + return this->checkBooleanLiteralFormula(stateFormula.asBooleanLiteralFormula()); + } + STORM_LOG_THROW(false, storm::exceptions::InvalidArgumentException, "The given formula '" << stateFormula << "' is invalid."); + } + + std::unique_ptr AbstractModelChecker::checkAtomicExpressionFormula(storm::logic::AtomicExpressionFormula const& stateFormula) { + STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "This model checker does not support the formula: " << stateFormula << "."); + } + + std::unique_ptr AbstractModelChecker::checkAtomicLabelFormula(storm::logic::AtomicLabelFormula const& stateFormula) { + STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "This model checker does not support the formula: " << stateFormula << "."); + } + + std::unique_ptr AbstractModelChecker::checkBinaryBooleanStateFormula(storm::logic::BinaryBooleanStateFormula const& stateFormula) { + STORM_LOG_THROW(stateFormula.getLeftSubformula().isStateFormula() && stateFormula.getRightSubformula().isStateFormula(), storm::exceptions::InvalidArgumentException, "The given formula is invalid."); + + std::unique_ptr leftResult = this->check(stateFormula.getLeftSubformula().asStateFormula()); + std::unique_ptr rightResult = this->check(stateFormula.getRightSubformula().asStateFormula()); + + *leftResult &= *rightResult; + return leftResult; + } + + std::unique_ptr AbstractModelChecker::checkBooleanLiteralFormula(storm::logic::BooleanLiteralFormula const& stateFormula) { + STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "This model checker does not support the formula: " << stateFormula << "."); + } + + std::unique_ptr AbstractModelChecker::checkProbabilityOperatorFormula(storm::logic::ProbabilityOperatorFormula const& stateFormula) { + STORM_LOG_THROW(stateFormula.getSubformula().isPathFormula(), storm::exceptions::InvalidArgumentException, "The given formula is invalid."); + + // If the probability bound is 0 or 1, is suffices to do qualitative model checking. + bool qualitative = false; + if (stateFormula.hasBound()) { + if (stateFormula.getBound() == storm::utility::zero() || stateFormula.getBound() == storm::utility::one()) { + qualitative = true; + } + } + if (stateFormula.hasOptimalityType()) { + return this->computeProbabilities(stateFormula.getSubformula().asPathFormula(), qualitative, stateFormula.getOptimalityType()); + } else { + return this->computeProbabilities(stateFormula.getSubformula().asPathFormula(), qualitative); + } + } + + std::unique_ptr AbstractModelChecker::checkRewardOperatorFormula(storm::logic::RewardOperatorFormula const& stateFormula) { + STORM_LOG_THROW(stateFormula.getSubformula().isRewardOperatorFormula(), storm::exceptions::InvalidArgumentException, "The given formula is invalid."); + + // If the probability bound is 0, is suffices to do qualitative model checking. + bool qualitative = false; + if (stateFormula.hasBound()) { + if (stateFormula.getBound() == storm::utility::zero() || stateFormula.getBound() == storm::utility::one()) { + qualitative = true; + } + } + if (stateFormula.hasOptimalityType()) { + return this->computeRewards(stateFormula.getSubformula().asRewardPathFormula(), qualitative, stateFormula.getOptimalityType()); + } else { + return this->computeRewards(stateFormula.getSubformula().asRewardPathFormula(), qualitative); + } + } + + std::unique_ptr AbstractModelChecker::checkSteadyStateOperatorFormula(storm::logic::SteadyStateOperatorFormula const& stateFormula) { + STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "This model checker does not support the formula: " << stateFormula << "."); + } + + std::unique_ptr AbstractModelChecker::checkUnaryBooleanStateFormula(storm::logic::UnaryBooleanStateFormula const& stateFormula) { + std::unique_ptr subResult = this->check(stateFormula.getSubformula()); + subResult->complement(); + return subResult; + } + } +} \ No newline at end of file diff --git a/src/modelchecker/AbstractModelChecker.h b/src/modelchecker/AbstractModelChecker.h new file mode 100644 index 000000000..397995414 --- /dev/null +++ b/src/modelchecker/AbstractModelChecker.h @@ -0,0 +1,62 @@ +#ifndef STORM_MODELCHECKER_ABSTRACTMODELCHECKER_H_ +#define STORM_MODELCHECKER_ABSTRACTMODELCHECKER_H_ + +#include + +#include "src/logic/Formulas.h" + +namespace storm { + namespace modelchecker { + class AbstractModelChecker { + public: + virtual ~AbstractModelChecker() { + // Intentionally left empty. + } + + /*! + * Determines whether the model checker can handle the formula. If this method returns false, the formula + * must not be checked using the model checker. + * + * @param formula The formula for which to check whether the model checker can handle it. + * @return True iff the model checker can check the given formula. + */ + virtual bool canHandle(storm::logic::Formula const& formula) const = 0; + + /*! + * Checks the provided formula. + * + * @param formula The formula to check. + * @return The verification result. + */ + virtual std::unique_ptr check(storm::logic::Formula const& formula); + + // The methods to compute probabilities for path formulas. + virtual std::unique_ptr computeProbabilities(storm::logic::PathFormula const& pathFormula, bool qualitative = false, boost::optional const& optimalityType = boost::optional()); + virtual std::unique_ptr computeBoundedUntilProbabilities(storm::logic::BoundedUntilFormula const& pathFormula, bool qualitative = false, boost::optional const& optimalityType = boost::optional()); + virtual std::unique_ptr computeConditionalProbabilities(storm::logic::ConditionalPathFormula const& pathFormula, bool qualitative = false, boost::optional const& optimalityType = boost::optional()); + virtual std::unique_ptr computeEventuallyProbabilities(storm::logic::EventuallyFormula const& pathFormula, bool qualitative = false, boost::optional const& optimalityType = boost::optional()); + virtual std::unique_ptr computeGloballyProbabilities(storm::logic::GloballyFormula const& pathFormula, bool qualitative = false, boost::optional const& optimalityType = boost::optional()); + virtual std::unique_ptr computeNextProbabilities(storm::logic::NextFormula const& pathFormula, bool qualitative = false, boost::optional const& optimalityType = boost::optional()); + virtual std::unique_ptr computeUntilProbabilities(storm::logic::UntilFormula const& pathFormula, bool qualitative = false, boost::optional const& optimalityType = boost::optional()); + + // The methods to compute the rewards for path formulas. + virtual std::unique_ptr computeRewards(storm::logic::RewardPathFormula const& rewardPathFormula, bool qualitative = false, boost::optional const& optimalityType = boost::optional()); + virtual std::unique_ptr computeCumulativeRewards(storm::logic::CumulativeRewardFormula const& rewardPathFormula, bool qualitative = false, boost::optional const& optimalityType = boost::optional()); + virtual std::unique_ptr computeInstantaneousRewards(storm::logic::InstantaneousRewardFormula const& rewardPathFormula, bool qualitative = false, boost::optional const& optimalityType = boost::optional()); + virtual std::unique_ptr computeReachabilityRewards(storm::logic::ReachabilityRewardFormula const& rewardPathFormula, bool qualitative = false, boost::optional const& optimalityType = boost::optional()); + + // The methods to check state formulas. + virtual std::unique_ptr checkStateFormula(storm::logic::StateFormula const& stateFormula); + virtual std::unique_ptr checkAtomicExpressionFormula(storm::logic::AtomicExpressionFormula const& stateFormula); + virtual std::unique_ptr checkAtomicLabelFormula(storm::logic::AtomicLabelFormula const& stateFormula); + virtual std::unique_ptr checkBinaryBooleanStateFormula(storm::logic::BinaryBooleanStateFormula const& stateFormula); + virtual std::unique_ptr checkBooleanLiteralFormula(storm::logic::BooleanLiteralFormula const& stateFormula); + virtual std::unique_ptr checkProbabilityOperatorFormula(storm::logic::ProbabilityOperatorFormula const& stateFormula); + virtual std::unique_ptr checkRewardOperatorFormula(storm::logic::RewardOperatorFormula const& stateFormula); + virtual std::unique_ptr checkSteadyStateOperatorFormula(storm::logic::SteadyStateOperatorFormula const& stateFormula); + virtual std::unique_ptr checkUnaryBooleanStateFormula(storm::logic::UnaryBooleanStateFormula const& stateFormula); + }; + } +} + +#endif /* STORM_MODELCHECKER_ABSTRACTMODELCHECKER_H_ */ \ No newline at end of file diff --git a/src/modelchecker/CheckResult.cpp b/src/modelchecker/CheckResult.cpp new file mode 100644 index 000000000..346b06c95 --- /dev/null +++ b/src/modelchecker/CheckResult.cpp @@ -0,0 +1,74 @@ +#include "src/modelchecker/CheckResult.h" + +#include "src/modelchecker/ExplicitQualitativeCheckResult.h" +#include "src/modelchecker/ExplicitQuantitativeCheckResult.h" + +#include "src/utility/macros.h" +#include "src/exceptions/InvalidOperationException.h" + +namespace storm { + namespace modelchecker { + CheckResult& CheckResult::operator&=(CheckResult const& other) { + STORM_LOG_THROW(false, storm::exceptions::InvalidOperationException, "Unable to perform logical 'and' on the two check results."); + } + + CheckResult& CheckResult::operator|=(CheckResult const& other) { + STORM_LOG_THROW(false, storm::exceptions::InvalidOperationException, "Unable to perform logical 'or' on the two check results."); + } + + void CheckResult::complement() { + STORM_LOG_THROW(false, storm::exceptions::InvalidOperationException, "Unable to perform logical 'not' on the check result."); + } + + bool CheckResult::isExplicit() const { + return false; + } + + bool CheckResult::isQuantitative() const { + return false; + } + + bool CheckResult::isQualitative() const { + return false; + } + + bool CheckResult::isResultForAllStates() const { + return false; + } + + std::ostream& operator<<(std::ostream& out, CheckResult& checkResult) { + checkResult.writeToStream(out); + return out; + } + + bool CheckResult::isExplicitQualitativeCheckResult() const { + return false; + } + + bool CheckResult::isExplicitQuantitativeCheckResult() const { + return false; + } + + ExplicitQualitativeCheckResult& CheckResult::asExplicitQualitativeCheckResult() { + return dynamic_cast(*this); + } + + ExplicitQualitativeCheckResult const& CheckResult::asExplicitQualitativeCheckResult() const { + return dynamic_cast(*this); + } + + template + ExplicitQuantitativeCheckResult& CheckResult::asExplicitQuantitativeCheckResult() { + return dynamic_cast&>(*this); + } + + template + ExplicitQuantitativeCheckResult const& CheckResult::asExplicitQuantitativeCheckResult() const { + return dynamic_cast const&>(*this); + } + + // Explicitly instantiate the template functions. + template ExplicitQuantitativeCheckResult& CheckResult::asExplicitQuantitativeCheckResult(); + template ExplicitQuantitativeCheckResult const& CheckResult::asExplicitQuantitativeCheckResult() const; + } +} \ No newline at end of file diff --git a/src/modelchecker/CheckResult.h b/src/modelchecker/CheckResult.h index ba7e1d5f8..e77727aab 100644 --- a/src/modelchecker/CheckResult.h +++ b/src/modelchecker/CheckResult.h @@ -1,12 +1,47 @@ #ifndef STORM_MODELCHECKER_CHECKRESULT_H_ #define STORM_MODELCHECKER_CHECKRESULT_H_ +#include + namespace storm { namespace modelchecker { + // Forward-declare the existing subclasses. + class QualitativeCheckResult; + template class QuantitativeCheckResult; + class ExplicitQualitativeCheckResult; + template class ExplicitQuantitativeCheckResult; + // The base class of all check results. class CheckResult { + public: + virtual CheckResult& operator&=(CheckResult const& other); + virtual CheckResult& operator|=(CheckResult const& other); + virtual void complement(); + + friend std::ostream& operator<<(std::ostream& out, CheckResult& checkResult); + + virtual bool isExplicit() const; + virtual bool isQuantitative() const; + virtual bool isQualitative() const; + virtual bool isResultForAllStates() const; + + virtual bool isExplicitQualitativeCheckResult() const; + virtual bool isExplicitQuantitativeCheckResult() const; + + ExplicitQualitativeCheckResult& asExplicitQualitativeCheckResult(); + ExplicitQualitativeCheckResult const& asExplicitQualitativeCheckResult() const; + + template + ExplicitQuantitativeCheckResult& asExplicitQuantitativeCheckResult(); + + template + ExplicitQuantitativeCheckResult const& asExplicitQuantitativeCheckResult() const; + protected: + virtual std::ostream& writeToStream(std::ostream& out) const = 0; }; + + std::ostream& operator<<(std::ostream& out, CheckResult& checkResult); } } diff --git a/src/modelchecker/ExplicitQualitativeCheckResult.cpp b/src/modelchecker/ExplicitQualitativeCheckResult.cpp new file mode 100644 index 000000000..f69744fc4 --- /dev/null +++ b/src/modelchecker/ExplicitQualitativeCheckResult.cpp @@ -0,0 +1,51 @@ +#include "src/modelchecker/ExplicitQualitativeCheckResult.h" + +#include "src/utility/macros.h" +#include "src/exceptions/InvalidOperationException.h" + +namespace storm { + namespace modelchecker { + CheckResult& ExplicitQualitativeCheckResult::operator&=(CheckResult const& other) { + STORM_LOG_THROW(typeid(other) == typeid(ExplicitQualitativeCheckResult), storm::exceptions::InvalidOperationException, "Cannot perform logical 'and' on check results of incompatible type."); + ExplicitQualitativeCheckResult const& otherCheckResult = static_cast(other); + this->truthValues &= otherCheckResult.truthValues; + return *this; + } + + CheckResult& ExplicitQualitativeCheckResult::operator|=(CheckResult const& other) { + STORM_LOG_THROW(typeid(other) == typeid(ExplicitQualitativeCheckResult), storm::exceptions::InvalidOperationException, "Cannot perform logical 'or' on check results of incompatible type."); + ExplicitQualitativeCheckResult const& otherCheckResult = static_cast(other); + this->truthValues |= otherCheckResult.truthValues; + return *this; + } + + bool ExplicitQualitativeCheckResult::operator[](uint_fast64_t index) const { + return truthValues.get(index); + } + + storm::storage::BitVector const& ExplicitQualitativeCheckResult::getTruthValues() const { + return truthValues; + } + + void ExplicitQualitativeCheckResult::complement() { + truthValues.complement(); + } + + bool ExplicitQualitativeCheckResult::isExplicit() const { + return true; + } + + bool ExplicitQualitativeCheckResult::isResultForAllStates() const { + return true; + } + + bool ExplicitQualitativeCheckResult::isExplicitQualitativeCheckResult() const { + return true; + } + + std::ostream& ExplicitQualitativeCheckResult::writeToStream(std::ostream& out) const { + out << truthValues; + return out; + } + } +} \ No newline at end of file diff --git a/src/modelchecker/ExplicitQualitativeCheckResult.h b/src/modelchecker/ExplicitQualitativeCheckResult.h new file mode 100644 index 000000000..c45f29577 --- /dev/null +++ b/src/modelchecker/ExplicitQualitativeCheckResult.h @@ -0,0 +1,60 @@ +#ifndef STORM_MODELCHECKER_EXPLICITQUALITATIVECHECKRESULT_H_ +#define STORM_MODELCHECKER_EXPLICITQUALITATIVECHECKRESULT_H_ + +#include "src/modelchecker/QualitativeCheckResult.h" +#include "src/storage/BitVector.h" + +namespace storm { + namespace modelchecker { + class ExplicitQualitativeCheckResult : public QualitativeCheckResult { + public: + /*! + * Constructs a check result with the provided truth values. + * + * @param truthValues The truth values of the result. + */ + ExplicitQualitativeCheckResult(storm::storage::BitVector const& truthValues) : truthValues(truthValues) { + // Intentionally left empty. + + } + + /*! + * Constructs a check result with the provided truth values. + * + * @param truthValues The truth values of the result. + */ + ExplicitQualitativeCheckResult(storm::storage::BitVector&& truthValues) : truthValues(std::move(truthValues)) { + // Intentionally left empty. + } + + ExplicitQualitativeCheckResult(ExplicitQualitativeCheckResult const& other) = default; + ExplicitQualitativeCheckResult& operator=(ExplicitQualitativeCheckResult const& other) = default; +#ifndef WINDOWS + ExplicitQualitativeCheckResult(ExplicitQualitativeCheckResult&& other) = default; + ExplicitQualitativeCheckResult& operator=(ExplicitQualitativeCheckResult&& other) = default; +#endif + + bool operator[](uint_fast64_t index) const; + + virtual bool isExplicit() const override; + virtual bool isResultForAllStates() const override; + + virtual bool isExplicitQualitativeCheckResult() const override; + + virtual CheckResult& operator&=(CheckResult const& other) override; + virtual CheckResult& operator|=(CheckResult const& other) override; + virtual void complement() override; + + storm::storage::BitVector const& getTruthValues() const; + + protected: + virtual std::ostream& writeToStream(std::ostream& out) const override; + + private: + // The values of the quantitative check result. + storm::storage::BitVector truthValues; + }; + } +} + +#endif /* STORM_MODELCHECKER_EXPLICITQUALITATIVECHECKRESULT_H_ */ \ No newline at end of file diff --git a/src/modelchecker/ExplicitQuantitativeCheckResult.cpp b/src/modelchecker/ExplicitQuantitativeCheckResult.cpp new file mode 100644 index 000000000..3c456fd91 --- /dev/null +++ b/src/modelchecker/ExplicitQuantitativeCheckResult.cpp @@ -0,0 +1,47 @@ +#include "src/modelchecker/ExplicitQuantitativeCheckResult.h" + +#include "src/utility/macros.h" +#include "src/exceptions/InvalidOperationException.h" + +namespace storm { + namespace modelchecker { + template + std::vector const& ExplicitQuantitativeCheckResult::getValues() const { + return values; + } + + template + std::ostream& ExplicitQuantitativeCheckResult::writeToStream(std::ostream& out) const { + out << "["; + if (!values.empty()) { + for (auto element: values) { + out << element << " "; + } + } + out << "]"; + return out; + } + + template + ValueType ExplicitQuantitativeCheckResult::operator[](uint_fast64_t index) const { + return values[index]; + } + + template + bool ExplicitQuantitativeCheckResult::isExplicit() const { + return true; + } + + template + bool ExplicitQuantitativeCheckResult::isResultForAllStates() const { + return true; + } + + template + bool ExplicitQuantitativeCheckResult::isExplicitQuantitativeCheckResult() const { + return true; + } + + template class ExplicitQuantitativeCheckResult; + } +} \ No newline at end of file diff --git a/src/modelchecker/ExplicitQuantitativeCheckResult.h b/src/modelchecker/ExplicitQuantitativeCheckResult.h new file mode 100644 index 000000000..b6a379bad --- /dev/null +++ b/src/modelchecker/ExplicitQuantitativeCheckResult.h @@ -0,0 +1,58 @@ +#ifndef STORM_MODELCHECKER_EXPLICITQUANTITATIVECHECKRESULT_H_ +#define STORM_MODELCHECKER_EXPLICITQUANTITATIVECHECKRESULT_H_ + +#include + +#include "src/modelchecker/QuantitativeCheckResult.h" +#include "src/utility/OsDetection.h" + +namespace storm { + namespace modelchecker { + template + class ExplicitQuantitativeCheckResult : public QuantitativeCheckResult { + public: + /*! + * Constructs a check result with the provided values. + * + * @param values The values of the result. + */ + ExplicitQuantitativeCheckResult(std::vector const& values) : values(values) { + // Intentionally left empty. + } + + /*! + * Constructs a check result with the provided values. + * + * @param values The values of the result. + */ + ExplicitQuantitativeCheckResult(std::vector&& values) : values(std::move(values)) { + // Intentionally left empty. + } + + ExplicitQuantitativeCheckResult(ExplicitQuantitativeCheckResult const& other) = default; + ExplicitQuantitativeCheckResult& operator=(ExplicitQuantitativeCheckResult const& other) = default; +#ifndef WINDOWS + ExplicitQuantitativeCheckResult(ExplicitQuantitativeCheckResult&& other) = default; + ExplicitQuantitativeCheckResult& operator=(ExplicitQuantitativeCheckResult&& other) = default; +#endif + + ValueType operator[](uint_fast64_t index) const; + + virtual bool isExplicit() const override; + virtual bool isResultForAllStates() const override; + + virtual bool isExplicitQuantitativeCheckResult() const override; + + std::vector const& getValues() const; + + protected: + virtual std::ostream& writeToStream(std::ostream& out) const override; + + private: + // The values of the quantitative check result. + std::vector values; + }; + } +} + +#endif /* STORM_MODELCHECKER_EXPLICITQUANTITATIVECHECKRESULT_H_ */ \ No newline at end of file diff --git a/src/modelchecker/QualitativeCheckResult.cpp b/src/modelchecker/QualitativeCheckResult.cpp new file mode 100644 index 000000000..5a0dab196 --- /dev/null +++ b/src/modelchecker/QualitativeCheckResult.cpp @@ -0,0 +1,9 @@ +#include "src/modelchecker/QualitativeCheckResult.h" + +namespace storm { + namespace modelchecker { + bool QualitativeCheckResult::isQualitative() const { + return true; + } + } +} \ No newline at end of file diff --git a/src/modelchecker/QualitativeCheckResult.h b/src/modelchecker/QualitativeCheckResult.h new file mode 100644 index 000000000..88691e1c6 --- /dev/null +++ b/src/modelchecker/QualitativeCheckResult.h @@ -0,0 +1,15 @@ +#ifndef STORM_MODELCHECKER_QUALITATIVECHECKRESULT_H_ +#define STORM_MODELCHECKER_QUALITATIVECHECKRESULT_H_ + +#include "src/modelchecker/CheckResult.h" + +namespace storm { + namespace modelchecker { + class QualitativeCheckResult : public CheckResult { + public: + virtual bool isQualitative() const override; + }; + } +} + +#endif /* STORM_MODELCHECKER_QUALITATIVECHECKRESULT_H_ */ \ No newline at end of file diff --git a/src/modelchecker/QuantitativeCheckResult.cpp b/src/modelchecker/QuantitativeCheckResult.cpp new file mode 100644 index 000000000..7dcb6482e --- /dev/null +++ b/src/modelchecker/QuantitativeCheckResult.cpp @@ -0,0 +1,12 @@ +#include "src/modelchecker/QuantitativeCheckResult.h" + +namespace storm { + namespace modelchecker { + template + bool QuantitativeCheckResult::isQuantitative() const { + return true; + } + + template class QuantitativeCheckResult; + } +} \ No newline at end of file diff --git a/src/modelchecker/QuantitativeCheckResult.h b/src/modelchecker/QuantitativeCheckResult.h new file mode 100644 index 000000000..73eda6c6a --- /dev/null +++ b/src/modelchecker/QuantitativeCheckResult.h @@ -0,0 +1,16 @@ +#ifndef STORM_MODELCHECKER_QUANTITATIVECHECKRESULT_H_ +#define STORM_MODELCHECKER_QUANTITATIVECHECKRESULT_H_ + +#include "src/modelchecker/CheckResult.h" + +namespace storm { + namespace modelchecker { + template + class QuantitativeCheckResult : public CheckResult { + public: + virtual bool isQuantitative() const override; + }; + } +} + +#endif /* STORM_MODELCHECKER_QUANTITATIVECHECKRESULT_H_ */ \ No newline at end of file diff --git a/src/modelchecker/SparseAllStatesQualitativeCheckResult.h b/src/modelchecker/SparseAllStatesQualitativeCheckResult.h deleted file mode 100644 index 0976ffe54..000000000 --- a/src/modelchecker/SparseAllStatesQualitativeCheckResult.h +++ /dev/null @@ -1,35 +0,0 @@ -#ifndef STORM_MODELCHECKER_SPARSEALLSTATESQUALITATIVECHECKRESULT_H_ -#define STORM_MODELCHECKER_SPARSEALLSTATESQUALITATIVECHECKRESULT_H_ - -#include "src/modelchecker/CheckResult.h" -#include "src/storage/BitVector.h" - -namespace storm { - namespace modelchecker { - template - class SparseAllStatesQualitativeCheckResult : public CheckResult { - public: - /*! - * Constructs a check result with the provided truth values. - * - * @param truthValues The truth values of the result. - */ - SparseAllStatesQualitativeCheckResult(storm::storage::BitVector&& truthValues) : truthValues(std::move(truthValues)) { - // Intentionally left empty. - } - - SparseAllStatesQualitativeCheckResult(SparseAllStatesQualitativeCheckResult const& other) = default; - SparseAllStatesQualitativeCheckResult& operator=(SparseAllStatesQualitativeCheckResult const& other) = default; -#ifndef WINDOWS - SparseAllStatesQualitativeCheckResult(SparseAllStatesQualitativeCheckResult&& other) = default; - SparseAllStatesQualitativeCheckResult& operator=(SparseAllStatesQualitativeCheckResult&& other) = default; -#endif - - private: - // The values of the quantitative check result. - storm::storage::BitVector truthValues; - }; - } -} - -#endif /* STORM_MODELCHECKER_SPARSEALLSTATESQUALITATIVECHECKRESULT_H_ */ \ No newline at end of file diff --git a/src/modelchecker/SparseAllStatesQuantitativeCheckResult.h b/src/modelchecker/SparseAllStatesQuantitativeCheckResult.h deleted file mode 100644 index 51410a272..000000000 --- a/src/modelchecker/SparseAllStatesQuantitativeCheckResult.h +++ /dev/null @@ -1,37 +0,0 @@ -#ifndef STORM_MODELCHECKER_SPARSEALLSTATESQUANTITATIVECHECKRESULT_H_ -#define STORM_MODELCHECKER_SPARSEALLSTATESQUANTITATIVECHECKRESULT_H_ - -#include - -#include "src/modelchecker/CheckResult.h" -#include "src/utility/OsDetection.h" - -namespace storm { - namespace modelchecker { - template - class SparseAllStatesQuantitativeCheckResult : public CheckResult { - public: - /*! - * Constructs a check result with the provided values. - * - * @param values The values of the result. - */ - SparseAllStatesQuantitativeCheckResult(std::vector&& values) : values(std::move(values)) { - // Intentionally left empty. - } - - SparseAllStatesQuantitativeCheckResult(SparseAllStatesQuantitativeCheckResult const& other) = default; - SparseAllStatesQuantitativeCheckResult& operator=(SparseAllStatesQuantitativeCheckResult const& other) = default; -#ifndef WINDOWS - SparseAllStatesQuantitativeCheckResult(SparseAllStatesQuantitativeCheckResult&& other) = default; - SparseAllStatesQuantitativeCheckResult& operator=(SparseAllStatesQuantitativeCheckResult&& other) = default; -#endif - - private: - // The values of the quantitative check result. - std::vector values; - }; - } -} - -#endif /* STORM_MODELCHECKER_SPARSEALLSTATESQUANTITATIVECHECKRESULT_H_ */ \ No newline at end of file diff --git a/src/modelchecker/csl/AbstractModelChecker.h b/src/modelchecker/csl/AbstractModelChecker.h deleted file mode 100644 index e2c68e740..000000000 --- a/src/modelchecker/csl/AbstractModelChecker.h +++ /dev/null @@ -1,244 +0,0 @@ -/* - * AbstractModelChecker.h - * - * Created on: 22.10.2012 - * Author: Thomas Heinemann - */ - -#ifndef STORM_MODELCHECKER_CSL_ABSTRACTMODELCHECKER_H_ -#define STORM_MODELCHECKER_CSL_ABSTRACTMODELCHECKER_H_ - -#include -#include "src/exceptions/InvalidPropertyException.h" -#include "src/properties/Csl.h" -#include "src/storage/BitVector.h" -#include "src/models/AbstractModel.h" - -#include "log4cplus/logger.h" -#include "log4cplus/loggingmacros.h" - -#include - -extern log4cplus::Logger logger; - -namespace storm { -namespace modelchecker { -namespace csl { - -/*! - * @brief - * (Abstract) interface for all model checker classes. - * - * This class provides basic functions that are common to all model checkers (i.e. subclasses). It mainly declares - * abstract methods that are implemented in the concrete subclasses, but also covers checking procedures that are common - * to all model checkers for state-based models. - */ -template -class AbstractModelChecker : - // A list of interfaces the model checker supports. Typically, for each of the interfaces, a check method needs to - // be implemented that performs the corresponding check. - public virtual storm::properties::csl::IApModelChecker, - public virtual storm::properties::csl::IAndModelChecker, - public virtual storm::properties::csl::IOrModelChecker, - public virtual storm::properties::csl::INotModelChecker, - public virtual storm::properties::csl::IUntilModelChecker, - public virtual storm::properties::csl::IEventuallyModelChecker, - public virtual storm::properties::csl::IGloballyModelChecker, - public virtual storm::properties::csl::INextModelChecker, - public virtual storm::properties::csl::ITimeBoundedUntilModelChecker, - public virtual storm::properties::csl::ITimeBoundedEventuallyModelChecker, - public virtual storm::properties::csl::IProbabilisticBoundOperatorModelChecker { - -public: - /*! - * Constructs an AbstractModelChecker with the given model. - */ - explicit AbstractModelChecker(storm::models::AbstractModel const& model) : minimumOperatorStack(), model(model) { - // Intentionally left empty. - } - /*! - * Copy constructs an AbstractModelChecker from the given model checker. In particular, this means that the newly - * constructed model checker will have the model of the given model checker as its associated model. - */ - explicit AbstractModelChecker(AbstractModelChecker const& modelchecker) : minimumOperatorStack(), model(modelchecker.model) { - // Intentionally left empty. - } - - /*! - * Virtual destructor. Needs to be virtual, because this class has virtual methods. - */ - virtual ~AbstractModelChecker() { - // Intentionally left empty. - } - - /*! - * Returns a pointer to the model checker object that is of the requested type as given by the template parameters. - * @returns A pointer to the model checker object that is of the requested type as given by the template parameters. - * If the model checker is not of the requested type, type casting will fail and result in an exception. - */ - template