diff --git a/CMakeLists.txt b/CMakeLists.txt index bf888e5a7..24c625754 100644 --- a/CMakeLists.txt +++ b/CMakeLists.txt @@ -254,12 +254,7 @@ set(STORM_SOURCES "${STORM_SOURCES_WITHOUT_MAIN};${STORM_MAIN_FILE}") file(GLOB_RECURSE STORM_ADAPTERS_FILES ${PROJECT_SOURCE_DIR}/src/adapters/*.h ${PROJECT_SOURCE_DIR}/src/adapters/*.cpp) 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 STORM_PROPERTIES_FILES ${PROJECT_SOURCE_DIR}/src/properties/*.h ${PROJECT_SOURCE_DIR}/src/properties/*.cpp) -file(GLOB_RECURSE STORM_PROPERTIES_CSL_FILES ${PROJECT_SOURCE_DIR}/src/properties/csl/*.h ${PROJECT_SOURCE_DIR}/src/properties/csl/*.cpp) -file(GLOB_RECURSE STORM_PROPERTIES_LTL_FILES ${PROJECT_SOURCE_DIR}/src/properties/ltl/*.h ${PROJECT_SOURCE_DIR}/src/properties/ltl/*.cpp) -file(GLOB_RECURSE STORM_PROPERTIES_PRCTL_FILES ${PROJECT_SOURCE_DIR}/src/properties/prctl/*.h ${PROJECT_SOURCE_DIR}/src/properties/prctl/*.cpp) -file(GLOB_RECURSE STORM_PROPERTIES_LOGIC_FILES ${PROJECT_SOURCE_DIR}/src/properties/logic/*.h ${PROJECT_SOURCE_DIR}/src/properties/logic/*.cpp) -file(GLOB_RECURSE STORM_PROPERTIES_ACTIONS_FILES ${PROJECT_SOURCE_DIR}/src/properties/actions/*.h ${PROJECT_SOURCE_DIR}/src/properties/actions/*.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_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) @@ -290,12 +285,7 @@ source_group(main FILES ${STORM_MAIN_FILE}) source_group(adapters FILES ${STORM_ADAPTERS_FILES}) source_group(builder FILES ${STORM_BUILDER_FILES}) source_group(exceptions FILES ${STORM_EXCEPTIONS_FILES}) -source_group(properties FILES ${STORM_PROPERTIES_FILES}) -source_group(properties\\logic FILES ${STORM_PROPERTIES_LOGIC_FILES}) -source_group(properties\\csl FILES ${STORM_PROPERTIES_CSL_FILES}) -source_group(properties\\ltl FILES ${STORM_PROPERTIES_LTL_FILES}) -source_group(properties\\prctl FILES ${STORM_PROPERTIES_PRCTL_FILES}) -source_group(properties\\actions FILES ${STORM_PROPERTIES_ACTIONS_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(counterexamples FILES ${STORM_COUNTEREXAMPLES_FILES}) diff --git a/src/properties/logic/AtomicExpressionFormula.cpp b/src/logic/AtomicExpressionFormula.cpp similarity index 65% rename from src/properties/logic/AtomicExpressionFormula.cpp rename to src/logic/AtomicExpressionFormula.cpp index c8617a551..2be59262d 100644 --- a/src/properties/logic/AtomicExpressionFormula.cpp +++ b/src/logic/AtomicExpressionFormula.cpp @@ -1,7 +1,11 @@ -#include "src/properties/logic/AtomicExpressionFormula.h" +#include "src/logic/AtomicExpressionFormula.h" namespace storm { namespace logic { + AtomicExpressionFormula::AtomicExpressionFormula(storm::expressions::Expression const& expression) : expression(expression) { + // Intentionally left empty. + } + bool AtomicExpressionFormula::isAtomicExpressionFormula() const { return true; } diff --git a/src/properties/logic/AtomicExpressionFormula.h b/src/logic/AtomicExpressionFormula.h similarity index 81% rename from src/properties/logic/AtomicExpressionFormula.h rename to src/logic/AtomicExpressionFormula.h index b246b8b89..7ba5bbdcb 100644 --- a/src/properties/logic/AtomicExpressionFormula.h +++ b/src/logic/AtomicExpressionFormula.h @@ -1,13 +1,15 @@ #ifndef STORM_LOGIC_ATOMICEXPRESSIONFORMULA_H_ #define STORM_LOGIC_ATOMICEXPRESSIONFORMULA_H_ -#include "src/properties/logic/StateFormula.h" +#include "src/logic/StateFormula.h" #include "src/storage/expressions/Expression.h" namespace storm { namespace logic { class AtomicExpressionFormula : public StateFormula { public: + AtomicExpressionFormula(storm::expressions::Expression const& expression); + virtual ~AtomicExpressionFormula() { // Intentionally left empty. } diff --git a/src/properties/logic/AtomicLabelFormula.cpp b/src/logic/AtomicLabelFormula.cpp similarity index 68% rename from src/properties/logic/AtomicLabelFormula.cpp rename to src/logic/AtomicLabelFormula.cpp index ac8586f19..44f742f19 100644 --- a/src/properties/logic/AtomicLabelFormula.cpp +++ b/src/logic/AtomicLabelFormula.cpp @@ -1,7 +1,11 @@ -#include "src/properties/logic/AtomicLabelFormula.h" +#include "src/logic/AtomicLabelFormula.h" namespace storm { namespace logic { + AtomicLabelFormula::AtomicLabelFormula(std::string const& label) : label(label) { + // Intentionally left empty. + } + bool AtomicLabelFormula::isAtomicLabelFormula() const { return true; } diff --git a/src/properties/logic/AtomicLabelFormula.h b/src/logic/AtomicLabelFormula.h similarity index 80% rename from src/properties/logic/AtomicLabelFormula.h rename to src/logic/AtomicLabelFormula.h index a93129b41..62a001ab2 100644 --- a/src/properties/logic/AtomicLabelFormula.h +++ b/src/logic/AtomicLabelFormula.h @@ -3,12 +3,14 @@ #include -#include "src/properties/logic/StateFormula.h" +#include "src/logic/StateFormula.h" namespace storm { namespace logic { class AtomicLabelFormula : public StateFormula { public: + AtomicLabelFormula(std::string const& label); + virtual ~AtomicLabelFormula() { // Intentionally left empty. } diff --git a/src/properties/logic/BinaryBooleanStateFormula.cpp b/src/logic/BinaryBooleanStateFormula.cpp similarity index 73% rename from src/properties/logic/BinaryBooleanStateFormula.cpp rename to src/logic/BinaryBooleanStateFormula.cpp index 2f1dede58..199cfda39 100644 --- a/src/properties/logic/BinaryBooleanStateFormula.cpp +++ b/src/logic/BinaryBooleanStateFormula.cpp @@ -1,8 +1,8 @@ -#include "src/properties/logic/BinaryBooleanStateFormula.h" +#include "src/logic/BinaryBooleanStateFormula.h" 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/properties/logic/BinaryBooleanStateFormula.h b/src/logic/BinaryBooleanStateFormula.h similarity index 77% rename from src/properties/logic/BinaryBooleanStateFormula.h rename to src/logic/BinaryBooleanStateFormula.h index 366c97a28..3f7d12b0d 100644 --- a/src/properties/logic/BinaryBooleanStateFormula.h +++ b/src/logic/BinaryBooleanStateFormula.h @@ -1,7 +1,7 @@ #ifndef STORM_LOGIC_BINARYBOOLEANSTATEFORMULA_H_ #define STORM_LOGIC_BINARYBOOLEANSTATEFORMULA_H_ -#include "src/properties/logic/BinaryStateFormula.h" +#include "src/logic/BinaryStateFormula.h" namespace storm { namespace logic { @@ -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/properties/logic/BinaryPathFormula.cpp b/src/logic/BinaryPathFormula.cpp similarity index 94% rename from src/properties/logic/BinaryPathFormula.cpp rename to src/logic/BinaryPathFormula.cpp index d877601f8..c2e4f3f2f 100644 --- a/src/properties/logic/BinaryPathFormula.cpp +++ b/src/logic/BinaryPathFormula.cpp @@ -1,4 +1,4 @@ -#include "src/properties/logic/BinaryPathFormula.h" +#include "src/logic/BinaryPathFormula.h" namespace storm { namespace logic { diff --git a/src/properties/logic/BinaryPathFormula.h b/src/logic/BinaryPathFormula.h similarity index 90% rename from src/properties/logic/BinaryPathFormula.h rename to src/logic/BinaryPathFormula.h index ed32b1a98..cec4fa622 100644 --- a/src/properties/logic/BinaryPathFormula.h +++ b/src/logic/BinaryPathFormula.h @@ -3,7 +3,7 @@ #include -#include "src/properties/logic/PathFormula.h" +#include "src/logic/PathFormula.h" namespace storm { namespace logic { diff --git a/src/properties/logic/BinaryStateFormula.cpp b/src/logic/BinaryStateFormula.cpp similarity index 94% rename from src/properties/logic/BinaryStateFormula.cpp rename to src/logic/BinaryStateFormula.cpp index a1c892ce7..8cbe4b105 100644 --- a/src/properties/logic/BinaryStateFormula.cpp +++ b/src/logic/BinaryStateFormula.cpp @@ -1,4 +1,4 @@ -#include "src/properties/logic/BinaryStateFormula.h" +#include "src/logic/BinaryStateFormula.h" namespace storm { namespace logic { diff --git a/src/properties/logic/BinaryStateFormula.h b/src/logic/BinaryStateFormula.h similarity index 90% rename from src/properties/logic/BinaryStateFormula.h rename to src/logic/BinaryStateFormula.h index 1c26cba61..d7e620bc2 100644 --- a/src/properties/logic/BinaryStateFormula.h +++ b/src/logic/BinaryStateFormula.h @@ -1,7 +1,7 @@ #ifndef STORM_LOGIC_BINARYSTATEFORMULA_H_ #define STORM_LOGIC_BINARYSTATEFORMULA_H_ -#include "src/properties/logic/StateFormula.h" +#include "src/logic/StateFormula.h" namespace storm { namespace logic { diff --git a/src/properties/logic/BooleanLiteralFormula.cpp b/src/logic/BooleanLiteralFormula.cpp similarity index 91% rename from src/properties/logic/BooleanLiteralFormula.cpp rename to src/logic/BooleanLiteralFormula.cpp index 46b752f7c..1c7adf5bd 100644 --- a/src/properties/logic/BooleanLiteralFormula.cpp +++ b/src/logic/BooleanLiteralFormula.cpp @@ -1,4 +1,4 @@ -#include "src/properties/logic/BooleanLiteralFormula.h" +#include "src/logic/BooleanLiteralFormula.h" namespace storm { namespace logic { diff --git a/src/properties/logic/BooleanLiteralFormula.h b/src/logic/BooleanLiteralFormula.h similarity index 86% rename from src/properties/logic/BooleanLiteralFormula.h rename to src/logic/BooleanLiteralFormula.h index 420d069e9..bc2f0d95c 100644 --- a/src/properties/logic/BooleanLiteralFormula.h +++ b/src/logic/BooleanLiteralFormula.h @@ -1,7 +1,7 @@ #ifndef STORM_LOGIC_BOOLEANLITERALFORMULA_H_ #define STORM_LOGIC_BOOLEANLITERALFORMULA_H_ -#include "src/properties/logic/StateFormula.h" +#include "src/logic/StateFormula.h" namespace storm { namespace logic { diff --git a/src/properties/logic/BoundedUntilFormula.cpp b/src/logic/BoundedUntilFormula.cpp similarity index 97% rename from src/properties/logic/BoundedUntilFormula.cpp rename to src/logic/BoundedUntilFormula.cpp index 80fe463e2..e5c93201a 100644 --- a/src/properties/logic/BoundedUntilFormula.cpp +++ b/src/logic/BoundedUntilFormula.cpp @@ -1,4 +1,4 @@ -#include "src/properties/logic/BoundedUntilFormula.h" +#include "src/logic/BoundedUntilFormula.h" namespace storm { namespace logic { diff --git a/src/properties/logic/BoundedUntilFormula.h b/src/logic/BoundedUntilFormula.h similarity index 91% rename from src/properties/logic/BoundedUntilFormula.h rename to src/logic/BoundedUntilFormula.h index cf402f864..ed7ac132e 100644 --- a/src/properties/logic/BoundedUntilFormula.h +++ b/src/logic/BoundedUntilFormula.h @@ -3,7 +3,7 @@ #include -#include "src/properties/logic/BinaryPathFormula.h" +#include "src/logic/BinaryPathFormula.h" namespace storm { namespace logic { diff --git a/src/properties/logic/ComparisonType.cpp b/src/logic/ComparisonType.cpp similarity index 89% rename from src/properties/logic/ComparisonType.cpp rename to src/logic/ComparisonType.cpp index 6999cb150..1eacaf1c2 100644 --- a/src/properties/logic/ComparisonType.cpp +++ b/src/logic/ComparisonType.cpp @@ -1,4 +1,4 @@ -#include "src/properties/logic/ComparisonType.h" +#include "src/logic/ComparisonType.h" namespace storm { namespace logic { diff --git a/src/properties/logic/ComparisonType.h b/src/logic/ComparisonType.h similarity index 100% rename from src/properties/logic/ComparisonType.h rename to src/logic/ComparisonType.h diff --git a/src/properties/logic/ConditionalPathFormula.cpp b/src/logic/ConditionalPathFormula.cpp similarity index 88% rename from src/properties/logic/ConditionalPathFormula.cpp rename to src/logic/ConditionalPathFormula.cpp index fed87ae34..106a8d9a1 100644 --- a/src/properties/logic/ConditionalPathFormula.cpp +++ b/src/logic/ConditionalPathFormula.cpp @@ -1,4 +1,4 @@ -#include "src/properties/logic/ConditionalPathFormula.h" +#include "src/logic/ConditionalPathFormula.h" namespace storm { namespace logic { @@ -12,7 +12,7 @@ namespace storm { std::ostream& ConditionalPathFormula::writeToStream(std::ostream& out) const { this->getLeftSubformula().writeToStream(out); - out << " | "; + out << " || "; this->getRightSubformula().writeToStream(out); return out; } diff --git a/src/properties/logic/ConditionalPathFormula.h b/src/logic/ConditionalPathFormula.h similarity index 86% rename from src/properties/logic/ConditionalPathFormula.h rename to src/logic/ConditionalPathFormula.h index d3427bfff..a65ee8b02 100644 --- a/src/properties/logic/ConditionalPathFormula.h +++ b/src/logic/ConditionalPathFormula.h @@ -1,7 +1,7 @@ #ifndef STORM_LOGIC_CONDITIONALPATHFORMULA_H_ #define STORM_LOGIC_CONDITIONALPATHFORMULA_H_ -#include "src/properties/logic/BinaryPathFormula.h" +#include "src/logic/BinaryPathFormula.h" namespace storm { namespace logic { diff --git a/src/properties/logic/CumulativeRewardFormula.cpp b/src/logic/CumulativeRewardFormula.cpp similarity index 89% rename from src/properties/logic/CumulativeRewardFormula.cpp rename to src/logic/CumulativeRewardFormula.cpp index 69933d1da..dc0310c95 100644 --- a/src/properties/logic/CumulativeRewardFormula.cpp +++ b/src/logic/CumulativeRewardFormula.cpp @@ -1,4 +1,4 @@ -#include "src/properties/logic/CumulativeRewardFormula.h" +#include "src/logic/CumulativeRewardFormula.h" namespace storm { namespace logic { diff --git a/src/properties/logic/CumulativeRewardFormula.h b/src/logic/CumulativeRewardFormula.h similarity index 86% rename from src/properties/logic/CumulativeRewardFormula.h rename to src/logic/CumulativeRewardFormula.h index d39a07a56..b3c10aad4 100644 --- a/src/properties/logic/CumulativeRewardFormula.h +++ b/src/logic/CumulativeRewardFormula.h @@ -1,7 +1,7 @@ #ifndef STORM_LOGIC_CUMULATIVEREWARDFORMULA_H_ #define STORM_LOGIC_CUMULATIVEREWARDFORMULA_H_ -#include "src/properties/logic/PathRewardFormula.h" +#include "src/logic/PathRewardFormula.h" namespace storm { namespace logic { diff --git a/src/properties/logic/EventuallyFormula.cpp b/src/logic/EventuallyFormula.cpp similarity index 90% rename from src/properties/logic/EventuallyFormula.cpp rename to src/logic/EventuallyFormula.cpp index 315e88014..98fc063b2 100644 --- a/src/properties/logic/EventuallyFormula.cpp +++ b/src/logic/EventuallyFormula.cpp @@ -1,4 +1,4 @@ -#include "src/properties/logic/EventuallyFormula.h" +#include "src/logic/EventuallyFormula.h" namespace storm { namespace logic { diff --git a/src/properties/logic/EventuallyFormula.h b/src/logic/EventuallyFormula.h similarity index 85% rename from src/properties/logic/EventuallyFormula.h rename to src/logic/EventuallyFormula.h index cb5bbafa4..4b5ea2a9a 100644 --- a/src/properties/logic/EventuallyFormula.h +++ b/src/logic/EventuallyFormula.h @@ -1,7 +1,7 @@ #ifndef STORM_LOGIC_EVENTUALLYFORMULA_H_ #define STORM_LOGIC_EVENTUALLYFORMULA_H_ -#include "src/properties/logic/UnaryPathFormula.h" +#include "src/logic/UnaryPathFormula.h" namespace storm { namespace logic { diff --git a/src/properties/logic/Formula.cpp b/src/logic/Formula.cpp similarity index 96% rename from src/properties/logic/Formula.cpp rename to src/logic/Formula.cpp index 7f170b8cb..0514dff6b 100644 --- a/src/properties/logic/Formula.cpp +++ b/src/logic/Formula.cpp @@ -1,4 +1,4 @@ -#include "src/properties/logic/Formulas.h" +#include "src/logic/Formulas.h" namespace storm { namespace logic { @@ -78,7 +78,7 @@ namespace storm { return false; } - bool Formula::isSteadyStateFormula() const { + bool Formula::isSteadyStateOperatorFormula() const { return false; } @@ -254,12 +254,12 @@ namespace storm { return dynamic_cast(*this); } - SteadyStateFormula& Formula::asSteadyStateFormula() { - return dynamic_cast(*this); + SteadyStateOperatorFormula& Formula::asSteadyStateFormula() { + return dynamic_cast(*this); } - SteadyStateFormula const& Formula::asSteadyStateFormula() const { - return dynamic_cast(*this); + SteadyStateOperatorFormula const& Formula::asSteadyStateFormula() const { + return dynamic_cast(*this); } PathRewardFormula& Formula::asPathRewardFormula() { diff --git a/src/properties/logic/Formula.h b/src/logic/Formula.h similarity index 95% rename from src/properties/logic/Formula.h rename to src/logic/Formula.h index f36ae7568..ee7be3779 100644 --- a/src/properties/logic/Formula.h +++ b/src/logic/Formula.h @@ -26,7 +26,7 @@ namespace storm { class UnaryPathFormula; class ConditionalPathFormula; class NextFormula; - class SteadyStateFormula; + class SteadyStateOperatorFormula; class PathRewardFormula; class CumulativeRewardFormula; class InstantaneousRewardFormula; @@ -66,7 +66,7 @@ namespace storm { virtual bool isUnaryPathFormula() const; virtual bool isConditionalPathFormula() const; virtual bool isNextFormula() const; - virtual bool isSteadyStateFormula() const; + virtual bool isSteadyStateOperatorFormula() const; virtual bool isPathRewardFormula() const; virtual bool isCumulativeRewardFormula() const; virtual bool isInstantaneousRewardFormula() const; @@ -129,8 +129,8 @@ namespace storm { NextFormula& asNextFormula(); NextFormula const& asNextFormula() const; - SteadyStateFormula& asSteadyStateFormula(); - SteadyStateFormula const& asSteadyStateFormula() const; + SteadyStateOperatorFormula& asSteadyStateFormula(); + SteadyStateOperatorFormula const& asSteadyStateFormula() const; PathRewardFormula& asPathRewardFormula(); PathRewardFormula const& asPathRewardFormula() const; diff --git a/src/logic/Formulas.h b/src/logic/Formulas.h new file mode 100644 index 000000000..99b3742ef --- /dev/null +++ b/src/logic/Formulas.h @@ -0,0 +1,28 @@ +#include "src/logic/Formula.h" +#include "src/logic/AtomicExpressionFormula.h" +#include "src/logic/AtomicLabelFormula.h" +#include "src/logic/BinaryBooleanStateFormula.h" +#include "src/logic/BinaryPathFormula.h" +#include "src/logic/BinaryStateFormula.h" +#include "src/logic/BooleanLiteralFormula.h" +#include "src/logic/BoundedUntilFormula.h" +#include "src/logic/CumulativeRewardFormula.h" +#include "src/logic/EventuallyFormula.h" +#include "src/logic/GloballyFormula.h" +#include "src/logic/InstantaneousRewardFormula.h" +#include "src/logic/NextFormula.h" +#include "src/logic/PathFormula.h" +#include "src/logic/ProbabilityOperatorFormula.h" +#include "src/logic/ReachabilityRewardFormula.h" +#include "src/logic/RewardOperatorFormula.h" +#include "src/logic/StateFormula.h" +#include "src/logic/SteadyStateOperatorFormula.h" +#include "src/logic/UnaryBooleanStateFormula.h" +#include "src/logic/UnaryPathFormula.h" +#include "src/logic/UnaryStateFormula.h" +#include "src/logic/UntilFormula.h" +#include "src/logic/ConditionalPathFormula.h" +#include "src/logic/ProbabilityOperatorFormula.h" +#include "src/logic/RewardOperatorFormula.h" +#include "src/logic/ComparisonType.h" +#include "src/logic/OptimalityType.h" \ No newline at end of file diff --git a/src/properties/logic/GloballyFormula.cpp b/src/logic/GloballyFormula.cpp similarity index 91% rename from src/properties/logic/GloballyFormula.cpp rename to src/logic/GloballyFormula.cpp index a2c9a5198..7874bc3dd 100644 --- a/src/properties/logic/GloballyFormula.cpp +++ b/src/logic/GloballyFormula.cpp @@ -1,4 +1,4 @@ -#include "src/properties/logic/GloballyFormula.h" +#include "src/logic/GloballyFormula.h" namespace storm { namespace logic { diff --git a/src/properties/logic/GloballyFormula.h b/src/logic/GloballyFormula.h similarity index 85% rename from src/properties/logic/GloballyFormula.h rename to src/logic/GloballyFormula.h index 1c6a8754b..ae09f87bb 100644 --- a/src/properties/logic/GloballyFormula.h +++ b/src/logic/GloballyFormula.h @@ -1,7 +1,7 @@ #ifndef STORM_LOGIC_GLOBALLYFORMULA_H_ #define STORM_LOGIC_GLOBALLYFORMULA_H_ -#include "src/properties/logic/UnaryPathFormula.h" +#include "src/logic/UnaryPathFormula.h" namespace storm { namespace logic { diff --git a/src/properties/logic/InstantaneousRewardFormula.cpp b/src/logic/InstantaneousRewardFormula.cpp similarity index 89% rename from src/properties/logic/InstantaneousRewardFormula.cpp rename to src/logic/InstantaneousRewardFormula.cpp index 5cb208f79..7573476a0 100644 --- a/src/properties/logic/InstantaneousRewardFormula.cpp +++ b/src/logic/InstantaneousRewardFormula.cpp @@ -1,4 +1,4 @@ -#include "src/properties/logic/InstantaneousRewardFormula.h" +#include "src/logic/InstantaneousRewardFormula.h" namespace storm { namespace logic { diff --git a/src/properties/logic/InstantaneousRewardFormula.h b/src/logic/InstantaneousRewardFormula.h similarity index 86% rename from src/properties/logic/InstantaneousRewardFormula.h rename to src/logic/InstantaneousRewardFormula.h index 808564589..a835e29bd 100644 --- a/src/properties/logic/InstantaneousRewardFormula.h +++ b/src/logic/InstantaneousRewardFormula.h @@ -1,7 +1,7 @@ #ifndef STORM_LOGIC_INSTANTANEOUSREWARDFORMULA_H_ #define STORM_LOGIC_INSTANTANEOUSREWARDFORMULA_H_ -#include "src/properties/logic/PathRewardFormula.h" +#include "src/logic/PathRewardFormula.h" namespace storm { namespace logic { diff --git a/src/properties/logic/NextFormula.cpp b/src/logic/NextFormula.cpp similarity index 91% rename from src/properties/logic/NextFormula.cpp rename to src/logic/NextFormula.cpp index 0bed9d5b7..cc98be661 100644 --- a/src/properties/logic/NextFormula.cpp +++ b/src/logic/NextFormula.cpp @@ -1,4 +1,4 @@ -#include "src/properties/logic/NextFormula.h" +#include "src/logic/NextFormula.h" namespace storm { namespace logic { diff --git a/src/properties/logic/NextFormula.h b/src/logic/NextFormula.h similarity index 85% rename from src/properties/logic/NextFormula.h rename to src/logic/NextFormula.h index 47a47e221..e9659ddfe 100644 --- a/src/properties/logic/NextFormula.h +++ b/src/logic/NextFormula.h @@ -1,7 +1,7 @@ #ifndef STORM_LOGIC_NEXTFORMULA_H_ #define STORM_LOGIC_NEXTFORMULA_H_ -#include "src/properties/logic/UnaryPathFormula.h" +#include "src/logic/UnaryPathFormula.h" namespace storm { namespace logic { diff --git a/src/properties/logic/OperatorFormula.cpp b/src/logic/OperatorFormula.cpp similarity index 84% rename from src/properties/logic/OperatorFormula.cpp rename to src/logic/OperatorFormula.cpp index 7287e3b74..31e56c042 100644 --- a/src/properties/logic/OperatorFormula.cpp +++ b/src/logic/OperatorFormula.cpp @@ -1,8 +1,8 @@ -#include "src/properties/logic/OperatorFormula.h" +#include "src/logic/OperatorFormula.h" namespace storm { namespace logic { - OperatorFormula::OperatorFormula(boost::optional comparisonType, boost::optional bound, boost::optional optimalityType, 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/properties/logic/OperatorFormula.h b/src/logic/OperatorFormula.h similarity index 71% rename from src/properties/logic/OperatorFormula.h rename to src/logic/OperatorFormula.h index eacfcfcb6..753c44f4a 100644 --- a/src/properties/logic/OperatorFormula.h +++ b/src/logic/OperatorFormula.h @@ -3,15 +3,15 @@ #include -#include "src/properties/logic/UnaryStateFormula.h" -#include "src/properties/logic/OptimalityType.h" -#include "src/properties/logic/ComparisonType.h" +#include "src/logic/UnaryStateFormula.h" +#include "src/logic/OptimalityType.h" +#include "src/logic/ComparisonType.h" namespace storm { namespace logic { class OperatorFormula : public UnaryStateFormula { public: - OperatorFormula(boost::optional comparisonType, boost::optional bound, boost::optional optimalityType, 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/properties/logic/OptimalityType.cpp b/src/logic/OptimalityType.cpp similarity index 86% rename from src/properties/logic/OptimalityType.cpp rename to src/logic/OptimalityType.cpp index 138d7dc2e..1c44ad0c3 100644 --- a/src/properties/logic/OptimalityType.cpp +++ b/src/logic/OptimalityType.cpp @@ -1,4 +1,4 @@ -#include "src/properties/logic/OptimalityType.h" +#include "src/logic/OptimalityType.h" namespace storm { namespace logic { diff --git a/src/properties/logic/OptimalityType.h b/src/logic/OptimalityType.h similarity index 100% rename from src/properties/logic/OptimalityType.h rename to src/logic/OptimalityType.h diff --git a/src/properties/logic/PathFormula.cpp b/src/logic/PathFormula.cpp similarity index 73% rename from src/properties/logic/PathFormula.cpp rename to src/logic/PathFormula.cpp index 86718021d..863a7aa66 100644 --- a/src/properties/logic/PathFormula.cpp +++ b/src/logic/PathFormula.cpp @@ -1,4 +1,4 @@ -#include "src/properties/logic/PathFormula.h" +#include "src/logic/PathFormula.h" namespace storm { namespace logic { diff --git a/src/properties/logic/PathFormula.h b/src/logic/PathFormula.h similarity index 81% rename from src/properties/logic/PathFormula.h rename to src/logic/PathFormula.h index 3dbd516c2..7dcfbc846 100644 --- a/src/properties/logic/PathFormula.h +++ b/src/logic/PathFormula.h @@ -1,7 +1,7 @@ #ifndef STORM_LOGIC_PATHFORMULA_H_ #define STORM_LOGIC_PATHFORMULA_H_ -#include "src/properties/logic/Formula.h" +#include "src/logic/Formula.h" namespace storm { namespace logic { diff --git a/src/properties/logic/PathRewardFormula.cpp b/src/logic/PathRewardFormula.cpp similarity index 73% rename from src/properties/logic/PathRewardFormula.cpp rename to src/logic/PathRewardFormula.cpp index 3cbee5012..db13399a1 100644 --- a/src/properties/logic/PathRewardFormula.cpp +++ b/src/logic/PathRewardFormula.cpp @@ -1,4 +1,4 @@ -#include "src/properties/logic/PathRewardFormula.h" +#include "src/logic/PathRewardFormula.h" namespace storm { namespace logic { diff --git a/src/properties/logic/PathRewardFormula.h b/src/logic/PathRewardFormula.h similarity index 81% rename from src/properties/logic/PathRewardFormula.h rename to src/logic/PathRewardFormula.h index 55e3885fd..91e340ebb 100644 --- a/src/properties/logic/PathRewardFormula.h +++ b/src/logic/PathRewardFormula.h @@ -1,7 +1,7 @@ #ifndef STORM_LOGIC_PATHREWARDFORMULA_H_ #define STORM_LOGIC_PATHREWARDFORMULA_H_ -#include "src/properties/logic/PathFormula.h" +#include "src/logic/PathFormula.h" namespace storm { namespace logic { diff --git a/src/properties/logic/ProbabilityOperatorFormula.cpp b/src/logic/ProbabilityOperatorFormula.cpp similarity index 52% rename from src/properties/logic/ProbabilityOperatorFormula.cpp rename to src/logic/ProbabilityOperatorFormula.cpp index 12527f73e..3b96dc81f 100644 --- a/src/properties/logic/ProbabilityOperatorFormula.cpp +++ b/src/logic/ProbabilityOperatorFormula.cpp @@ -1,20 +1,20 @@ -#include "src/properties/logic/ProbabilityOperatorFormula.h" +#include "src/logic/ProbabilityOperatorFormula.h" 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(comparisonType), boost::optional(bound), boost::optional(), 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(ComparisonType comparisonType, double bound, OptimalityType optimalityType, std::shared_ptr const& subformula) : ProbabilityOperatorFormula(boost::optional(comparisonType), boost::optional(bound), boost::optional(optimalityType), 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(), boost::optional(), boost::optional(optimalityType), subformula) { + ProbabilityOperatorFormula::ProbabilityOperatorFormula(OptimalityType optimalityType, std::shared_ptr const& subformula) : ProbabilityOperatorFormula(boost::optional(optimalityType), boost::optional(), boost::optional(), subformula) { // Intentionally left empty. } @@ -22,7 +22,7 @@ namespace storm { return true; } - ProbabilityOperatorFormula::ProbabilityOperatorFormula(boost::optional comparisonType, boost::optional bound, boost::optional optimalityType, std::shared_ptr const& subformula) : OperatorFormula(comparisonType, bound, optimalityType, 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/properties/logic/ProbabilityOperatorFormula.h b/src/logic/ProbabilityOperatorFormula.h similarity index 66% rename from src/properties/logic/ProbabilityOperatorFormula.h rename to src/logic/ProbabilityOperatorFormula.h index 29296acfa..d22d24dfa 100644 --- a/src/properties/logic/ProbabilityOperatorFormula.h +++ b/src/logic/ProbabilityOperatorFormula.h @@ -1,7 +1,7 @@ #ifndef STORM_LOGIC_PROBABILITYOPERATORFORMULA_H_ #define STORM_LOGIC_PROBABILITYOPERATORFORMULA_H_ -#include "src/properties/logic/OperatorFormula.h" +#include "src/logic/OperatorFormula.h" namespace storm { namespace logic { @@ -9,9 +9,10 @@ namespace storm { public: ProbabilityOperatorFormula(std::shared_ptr const& subformula); ProbabilityOperatorFormula(ComparisonType comparisonType, double bound, std::shared_ptr const& subformula); - ProbabilityOperatorFormula(ComparisonType comparisonType, double bound, OptimalityType optimalityType, 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. } @@ -19,9 +20,6 @@ namespace storm { virtual bool isProbabilityOperator() const override; virtual std::ostream& writeToStream(std::ostream& out) const override; - - private: - ProbabilityOperatorFormula(boost::optional comparisonType, boost::optional bound, boost::optional optimalityType, std::shared_ptr const& subformula); }; } } diff --git a/src/properties/logic/ReachabilityRewardFormula.cpp b/src/logic/ReachabilityRewardFormula.cpp similarity index 68% rename from src/properties/logic/ReachabilityRewardFormula.cpp rename to src/logic/ReachabilityRewardFormula.cpp index 8e77931b7..cc11e074d 100644 --- a/src/properties/logic/ReachabilityRewardFormula.cpp +++ b/src/logic/ReachabilityRewardFormula.cpp @@ -1,8 +1,8 @@ -#include "src/properties/logic/ReachabilityRewardFormula.h" +#include "src/logic/ReachabilityRewardFormula.h" 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,11 +10,11 @@ namespace storm { return true; } - StateFormula& ReachabilityRewardFormula::getSubformula() { + Formula& ReachabilityRewardFormula::getSubformula() { return *subformula; } - StateFormula const& ReachabilityRewardFormula::getSubformula() const { + Formula const& ReachabilityRewardFormula::getSubformula() const { return *subformula; } diff --git a/src/properties/logic/ReachabilityRewardFormula.h b/src/logic/ReachabilityRewardFormula.h similarity index 60% rename from src/properties/logic/ReachabilityRewardFormula.h rename to src/logic/ReachabilityRewardFormula.h index 9cf74f4a2..28596f567 100644 --- a/src/properties/logic/ReachabilityRewardFormula.h +++ b/src/logic/ReachabilityRewardFormula.h @@ -3,14 +3,14 @@ #include -#include "src/properties/logic/PathRewardFormula.h" -#include "src/properties/logic/StateFormula.h" +#include "src/logic/PathRewardFormula.h" +#include "src/logic/StateFormula.h" namespace storm { namespace logic { class ReachabilityRewardFormula : public PathRewardFormula { public: - ReachabilityRewardFormula(std::shared_ptr const& subformula); + ReachabilityRewardFormula(std::shared_ptr const& subformula); virtual ~ReachabilityRewardFormula() { // Intentionally left empty. @@ -18,13 +18,13 @@ namespace storm { virtual bool isReachabilityRewardFormula() const override; - StateFormula& getSubformula(); - StateFormula const& getSubformula() const; + Formula& getSubformula(); + Formula const& getSubformula() const; virtual std::ostream& writeToStream(std::ostream& out) const override; private: - std::shared_ptr const& subformula; + std::shared_ptr const& subformula; }; } } diff --git a/src/properties/logic/RewardOperatorFormula.cpp b/src/logic/RewardOperatorFormula.cpp similarity index 54% rename from src/properties/logic/RewardOperatorFormula.cpp rename to src/logic/RewardOperatorFormula.cpp index 1f4ec1e27..4b6f0c288 100644 --- a/src/properties/logic/RewardOperatorFormula.cpp +++ b/src/logic/RewardOperatorFormula.cpp @@ -1,20 +1,20 @@ -#include "src/properties/logic/RewardOperatorFormula.h" +#include "src/logic/RewardOperatorFormula.h" 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(comparisonType), boost::optional(bound), boost::optional(), 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(ComparisonType comparisonType, double bound, OptimalityType optimalityType, std::shared_ptr const& subformula) : RewardOperatorFormula(boost::optional(comparisonType), boost::optional(bound), boost::optional(optimalityType), 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(), boost::optional(), boost::optional(optimalityType), subformula) { + RewardOperatorFormula::RewardOperatorFormula(OptimalityType optimalityType, std::shared_ptr const& subformula) : RewardOperatorFormula(boost::optional(optimalityType), boost::optional(), boost::optional(), subformula) { // Intentionally left empty. } @@ -22,7 +22,7 @@ namespace storm { return true; } - RewardOperatorFormula::RewardOperatorFormula(boost::optional comparisonType, boost::optional bound, boost::optional optimalityType, std::shared_ptr const& subformula) : OperatorFormula(comparisonType, bound, optimalityType, 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/properties/logic/RewardOperatorFormula.h b/src/logic/RewardOperatorFormula.h similarity index 65% rename from src/properties/logic/RewardOperatorFormula.h rename to src/logic/RewardOperatorFormula.h index 14fe708af..dc198f062 100644 --- a/src/properties/logic/RewardOperatorFormula.h +++ b/src/logic/RewardOperatorFormula.h @@ -1,7 +1,7 @@ #ifndef STORM_LOGIC_REWARDOPERATORFORMULA_H_ #define STORM_LOGIC_REWARDOPERATORFORMULA_H_ -#include "src/properties/logic/OperatorFormula.h" +#include "src/logic/OperatorFormula.h" namespace storm { namespace logic { @@ -9,9 +9,10 @@ namespace storm { public: RewardOperatorFormula(std::shared_ptr const& subformula); RewardOperatorFormula(ComparisonType comparisonType, double bound, std::shared_ptr const& subformula); - RewardOperatorFormula(ComparisonType comparisonType, double bound, OptimalityType optimalityType, 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. } @@ -19,9 +20,6 @@ namespace storm { virtual bool isRewardOperator() const override; virtual std::ostream& writeToStream(std::ostream& out) const override; - - private: - RewardOperatorFormula(boost::optional comparisonType, boost::optional bound, boost::optional optimalityType, std::shared_ptr const& subformula); }; } } diff --git a/src/properties/logic/StateFormula.cpp b/src/logic/StateFormula.cpp similarity index 73% rename from src/properties/logic/StateFormula.cpp rename to src/logic/StateFormula.cpp index 9a34eab5c..86e0a683d 100644 --- a/src/properties/logic/StateFormula.cpp +++ b/src/logic/StateFormula.cpp @@ -1,4 +1,4 @@ -#include "src/properties/logic/StateFormula.h" +#include "src/logic/StateFormula.h" namespace storm { namespace logic { diff --git a/src/properties/logic/StateFormula.h b/src/logic/StateFormula.h similarity index 81% rename from src/properties/logic/StateFormula.h rename to src/logic/StateFormula.h index 3c1def818..f55cf9f48 100644 --- a/src/properties/logic/StateFormula.h +++ b/src/logic/StateFormula.h @@ -1,7 +1,7 @@ #ifndef STORM_LOGIC_STATEFORMULA_H_ #define STORM_LOGIC_STATEFORMULA_H_ -#include "src/properties/logic/Formula.h" +#include "src/logic/Formula.h" namespace storm { namespace logic { diff --git a/src/logic/SteadyStateOperatorFormula.cpp b/src/logic/SteadyStateOperatorFormula.cpp new file mode 100644 index 000000000..945798bcb --- /dev/null +++ b/src/logic/SteadyStateOperatorFormula.cpp @@ -0,0 +1,35 @@ +#include "src/logic/SteadyStateOperatorFormula.h" + +namespace storm { + namespace logic { + 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) { + // 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) { + // Intentionally left empty. + } + + SteadyStateOperatorFormula::SteadyStateOperatorFormula(OptimalityType optimalityType, std::shared_ptr const& subformula) : SteadyStateOperatorFormula(boost::optional(optimalityType), boost::optional(), boost::optional(), subformula) { + // Intentionally left empty. + } + + bool SteadyStateOperatorFormula::isSteadyStateOperatorFormula() const { + return true; + } + + SteadyStateOperatorFormula::SteadyStateOperatorFormula(boost::optional optimalityType, boost::optional comparisonType, boost::optional bound, std::shared_ptr const& subformula) : OperatorFormula(optimalityType, comparisonType, bound, subformula) { + // Intentionally left empty. + } + + std::ostream& SteadyStateOperatorFormula::writeToStream(std::ostream& out) const { + out << "S"; + OperatorFormula::writeToStream(out); + return out; + } + } +} \ No newline at end of file diff --git a/src/logic/SteadyStateOperatorFormula.h b/src/logic/SteadyStateOperatorFormula.h new file mode 100644 index 000000000..6e174801b --- /dev/null +++ b/src/logic/SteadyStateOperatorFormula.h @@ -0,0 +1,27 @@ +#ifndef STORM_LOGIC_STEADYSTATEFORMULA_H_ +#define STORM_LOGIC_STEADYSTATEFORMULA_H_ + +#include "src/logic/OperatorFormula.h" + +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); + + virtual ~SteadyStateOperatorFormula() { + // Intentionally left empty. + } + + virtual bool isSteadyStateOperatorFormula() const override; + + virtual std::ostream& writeToStream(std::ostream& out) const override; + }; + } +} + +#endif /* STORM_LOGIC_STEADYSTATEFORMULA_H_ */ \ No newline at end of file diff --git a/src/properties/logic/UnaryBooleanStateFormula.cpp b/src/logic/UnaryBooleanStateFormula.cpp similarity index 72% rename from src/properties/logic/UnaryBooleanStateFormula.cpp rename to src/logic/UnaryBooleanStateFormula.cpp index 9f6bddd0f..4becf8a43 100644 --- a/src/properties/logic/UnaryBooleanStateFormula.cpp +++ b/src/logic/UnaryBooleanStateFormula.cpp @@ -1,4 +1,4 @@ -#include "src/properties/logic/UnaryBooleanStateFormula.h" +#include "src/logic/UnaryBooleanStateFormula.h" namespace storm { namespace logic { diff --git a/src/properties/logic/UnaryBooleanStateFormula.h b/src/logic/UnaryBooleanStateFormula.h similarity index 80% rename from src/properties/logic/UnaryBooleanStateFormula.h rename to src/logic/UnaryBooleanStateFormula.h index 0a9e193ea..a7ae644ba 100644 --- a/src/properties/logic/UnaryBooleanStateFormula.h +++ b/src/logic/UnaryBooleanStateFormula.h @@ -1,7 +1,7 @@ #ifndef STORM_LOGIC_UNARYBOOLEANSTATEFORMULA_H_ #define STORM_LOGIC_UNARYBOOLEANSTATEFORMULA_H_ -#include "src/properties/logic/UnaryStateFormula.h" +#include "src/logic/UnaryStateFormula.h" namespace storm { namespace logic { diff --git a/src/properties/logic/UnaryPathFormula.cpp b/src/logic/UnaryPathFormula.cpp similarity index 91% rename from src/properties/logic/UnaryPathFormula.cpp rename to src/logic/UnaryPathFormula.cpp index ee9b84234..25d20bbab 100644 --- a/src/properties/logic/UnaryPathFormula.cpp +++ b/src/logic/UnaryPathFormula.cpp @@ -1,4 +1,4 @@ -#include "src/properties/logic/UnaryPathFormula.h" +#include "src/logic/UnaryPathFormula.h" namespace storm { namespace logic { diff --git a/src/properties/logic/UnaryPathFormula.h b/src/logic/UnaryPathFormula.h similarity index 88% rename from src/properties/logic/UnaryPathFormula.h rename to src/logic/UnaryPathFormula.h index 3b10c10de..2115cf411 100644 --- a/src/properties/logic/UnaryPathFormula.h +++ b/src/logic/UnaryPathFormula.h @@ -3,7 +3,7 @@ #include -#include "src/properties/logic/PathFormula.h" +#include "src/logic/PathFormula.h" namespace storm { namespace logic { diff --git a/src/properties/logic/UnaryStateFormula.cpp b/src/logic/UnaryStateFormula.cpp similarity index 90% rename from src/properties/logic/UnaryStateFormula.cpp rename to src/logic/UnaryStateFormula.cpp index 2cb5964e1..90b112ee2 100644 --- a/src/properties/logic/UnaryStateFormula.cpp +++ b/src/logic/UnaryStateFormula.cpp @@ -1,4 +1,4 @@ -#include "src/properties/logic/UnaryStateFormula.h" +#include "src/logic/UnaryStateFormula.h" namespace storm { namespace logic { diff --git a/src/properties/logic/UnaryStateFormula.h b/src/logic/UnaryStateFormula.h similarity index 87% rename from src/properties/logic/UnaryStateFormula.h rename to src/logic/UnaryStateFormula.h index 9beed29ed..381348184 100644 --- a/src/properties/logic/UnaryStateFormula.h +++ b/src/logic/UnaryStateFormula.h @@ -1,7 +1,7 @@ #ifndef STORM_LOGIC_UNARYSTATEFORMULA_H_ #define STORM_LOGIC_UNARYSTATEFORMULA_H_ -#include "src/properties/logic/StateFormula.h" +#include "src/logic/StateFormula.h" namespace storm { namespace logic { diff --git a/src/properties/logic/UntilFormula.cpp b/src/logic/UntilFormula.cpp similarity index 93% rename from src/properties/logic/UntilFormula.cpp rename to src/logic/UntilFormula.cpp index 8486fe94b..450e16f2c 100644 --- a/src/properties/logic/UntilFormula.cpp +++ b/src/logic/UntilFormula.cpp @@ -1,4 +1,4 @@ -#include "src/properties/logic/UntilFormula.h" +#include "src/logic/UntilFormula.h" namespace storm { namespace logic { diff --git a/src/properties/logic/UntilFormula.h b/src/logic/UntilFormula.h similarity index 86% rename from src/properties/logic/UntilFormula.h rename to src/logic/UntilFormula.h index 9a831b6d9..790a9457d 100644 --- a/src/properties/logic/UntilFormula.h +++ b/src/logic/UntilFormula.h @@ -1,7 +1,7 @@ #ifndef STORM_LOGIC_UNTILFORMULA_H_ #define STORM_LOGIC_UNTILFORMULA_H_ -#include "src/properties/logic/BinaryPathFormula.h" +#include "src/logic/BinaryPathFormula.h" namespace storm { namespace logic { diff --git a/src/parser/CslParser.cpp b/src/parser/CslParser.cpp deleted file mode 100644 index b16e441e8..000000000 --- a/src/parser/CslParser.cpp +++ /dev/null @@ -1,295 +0,0 @@ -/* - * CslParser.cpp - * - * Created on: 08.04.2013 - * Author: Thomas Heinemann - */ - -#include "src/parser/CslParser.h" -#include "src/utility/OsDetection.h" -#include "src/utility/constants.h" - -// The action class headers. -#include "src/properties/actions/AbstractAction.h" -#include "src/properties/actions/BoundAction.h" -#include "src/properties/actions/InvertAction.h" -#include "src/properties/actions/FormulaAction.h" -#include "src/properties/actions/RangeAction.h" -#include "src/properties/actions/SortAction.h" - -// If the parser fails due to ill-formed data, this exception is thrown. -#include "src/exceptions/WrongFormatException.h" - -// Used for Boost spirit. -#include -#include -#include - -// Include headers for spirit iterators. Needed for diagnostics and input stream iteration. -#include -#include - -// Needed for file IO. -#include -#include -#include - - -// Some typedefs and namespace definitions to reduce code size. -#define MAKE(Type, ...) phoenix::construct>(phoenix::new_(__VA_ARGS__)) -typedef std::string::const_iterator BaseIteratorType; -typedef boost::spirit::classic::position_iterator2 PositionIteratorType; -namespace qi = boost::spirit::qi; -namespace phoenix = boost::phoenix; -namespace csl = storm::properties::csl; - -namespace storm { -namespace parser { - -template -struct CslParser::CslGrammar : qi::grammar>(), Skipper > { - CslGrammar() : CslGrammar::base_type(start) { - //This block contains helper rules that may be used several times - freeIdentifierName = qi::lexeme[qi::alpha >> *(qi::alnum | qi::char_('_'))]; - comparisonType = ( - (qi::lit(">="))[qi::_val = storm::properties::GREATER_EQUAL] | - (qi::lit(">"))[qi::_val = storm::properties::GREATER] | - (qi::lit("<="))[qi::_val = storm::properties::LESS_EQUAL] | - (qi::lit("<"))[qi::_val = storm::properties::LESS]); - sortingCategory = ( - (qi::lit("index"))[qi::_val = storm::properties::action::SortAction::INDEX] | - (qi::lit("value"))[qi::_val = storm::properties::action::SortAction::VALUE] - ); - //Comment: Empty line or line starting with "//" - comment = (qi::lit("//") >> *(qi::char_))[qi::_val = nullptr]; - - //This block defines rules for parsing state formulas - stateFormula %= orFormula; - stateFormula.name("state formula"); - orFormula = andFormula[qi::_val = qi::_1] > *(qi::lit("|") > andFormula)[qi::_val = - MAKE(csl::Or, qi::_val, qi::_1)]; - orFormula.name("or formula"); - andFormula = notFormula[qi::_val = qi::_1] > *(qi::lit("&") > notFormula)[qi::_val = - MAKE(csl::And, qi::_val, qi::_1)]; - andFormula.name("and formula"); - notFormula = atomicStateFormula[qi::_val = qi::_1] | (qi::lit("!") > atomicStateFormula)[qi::_val = - MAKE(csl::Not, qi::_1)]; - notFormula.name("not formula"); - - //This block defines rules for "atomic" state formulas - //(Propositions, probabilistic/reward formulas, and state formulas in brackets) - atomicStateFormula %= probabilisticBoundOperator | steadyStateBoundOperator | atomicProposition | (qi::lit("(") >> stateFormula >> qi::lit(")")) | (qi::lit("[") >> stateFormula >> qi::lit("]")); - atomicStateFormula.name("atomic state formula"); - atomicProposition = (freeIdentifierName)[qi::_val = MAKE(csl::Ap, qi::_1)] | (qi::lit("\"") > (freeIdentifierName)[qi::_val = MAKE(csl::Ap, qi::_1)] > qi::lit("\"")); - atomicProposition.name("atomic proposition"); - probabilisticBoundOperator = ( - (qi::lit("P") >> comparisonType > qi::double_ > pathFormula )[qi::_val = - MAKE(csl::ProbabilisticBoundOperator , qi::_1, qi::_2, qi::_3)] - ); - probabilisticBoundOperator.name("probabilistic bound operator"); - steadyStateBoundOperator = ( - (qi::lit("S") >> comparisonType > qi::double_ > stateFormula )[qi::_val = - MAKE(csl::SteadyStateBoundOperator , qi::_1, qi::_2, qi::_3)] - ); - steadyStateBoundOperator.name("steady state bound operator"); - - //This block defines rules for parsing probabilistic path formulas - pathFormula = (timeBoundedEventually | eventually | globally | next | timeBoundedUntil | until | (qi::lit("(") >> pathFormula >> qi::lit(")")) | (qi::lit("[") >> pathFormula >> qi::lit("]"))); - pathFormula.name("path formula"); - timeBoundedEventually = ( - ((qi::lit("F") >> qi::lit("[") >> qi::double_ >> qi::lit(",")) > qi::double_ > qi::lit("]") > stateFormula)[qi::_val = - MAKE(csl::TimeBoundedEventually, qi::_1, qi::_2, qi::_3)] | - ((qi::lit("F") >> (qi::lit("<=") | qi::lit("<"))) > qi::double_ > stateFormula)[qi::_val = - MAKE(csl::TimeBoundedEventually, 0, qi::_1, qi::_2)] | - ((qi::lit("F") >> (qi::lit(">=") | qi::lit(">"))) > qi::double_ > stateFormula)[qi::_val = - MAKE(csl::TimeBoundedEventually, qi::_1, std::numeric_limits::infinity(), qi::_2)] - ); - timeBoundedEventually.name("time bounded eventually"); - eventually = (qi::lit("F") > stateFormula)[qi::_val = - MAKE(csl::Eventually , qi::_1)]; - eventually.name("eventually"); - next = (qi::lit("X") > stateFormula)[qi::_val = - MAKE(csl::Next , qi::_1)]; - next.name("next"); - globally = (qi::lit("G") > stateFormula)[qi::_val = - MAKE(csl::Globally , qi::_1)]; - globally.name("globally"); - timeBoundedUntil = ( - (stateFormula[qi::_a = qi::_1] >> qi::lit("U") >> qi::lit("[") >> qi::double_ >> qi::lit(",") >> qi::double_ >> qi::lit("]") >> stateFormula) - [qi::_val = MAKE(csl::TimeBoundedUntil, qi::_2, qi::_3, qi::_a, qi::_4)] | - (stateFormula[qi::_a = qi::_1] >> qi::lit("U") >> (qi::lit("<=") | qi::lit("<")) > qi::double_ > stateFormula) - [qi::_val = MAKE(csl::TimeBoundedUntil, 0, qi::_2, qi::_a, qi::_3)] | - (stateFormula[qi::_a = qi::_1] >> qi::lit("U") >> (qi::lit(">=") | qi::lit(">")) > qi::double_ > stateFormula) - [qi::_val = MAKE(csl::TimeBoundedUntil, qi::_2, std::numeric_limits::infinity(), qi::_a, qi::_3)] - ); - timeBoundedUntil.name("time bounded until"); - until = (stateFormula[qi::_a = qi::_1] >> qi::lit("U") > stateFormula)[qi::_val = - MAKE(csl::Until, qi::_a, qi::_2)]; - until.name("until formula"); - - formula = (pathFormula | stateFormula); - formula.name("CSL formula"); - - //This block defines rules for parsing formulas with noBoundOperators - noBoundOperator = (probabilisticNoBoundOperator | steadyStateNoBoundOperator); - noBoundOperator.name("no bound operator"); - probabilisticNoBoundOperator = - ((qi::lit("P") >> qi::lit("min") >> qi::lit("=")) > qi::lit("?") >> pathFormula)[qi::_val = - MAKE(csl::CslFilter, qi::_1, storm::properties::MINIMIZE)] | - ((qi::lit("P") >> qi::lit("max") >> qi::lit("=")) > qi::lit("?") >> pathFormula)[qi::_val = - MAKE(csl::CslFilter, qi::_1, storm::properties::MAXIMIZE)] | - ((qi::lit("P") >> qi::lit("=")) > qi::lit("?") >> pathFormula)[qi::_val = - MAKE(csl::CslFilter, qi::_1)]; - probabilisticNoBoundOperator.name("probabilistic no bound operator"); - steadyStateNoBoundOperator = ((qi::lit("S") >> qi::lit("=")) > qi::lit("?") >> stateFormula )[qi::_val = - MAKE(csl::CslFilter, qi::_1, storm::properties::UNDEFINED, true)]; - steadyStateNoBoundOperator.name("steady state no bound operator"); - - // This block defines rules for parsing filter actions. - boundAction = (qi::lit("bound") > qi::lit("(") >> comparisonType >> qi::lit(",") >> qi::double_ >> qi::lit(")"))[qi::_val = - MAKE(storm::properties::action::BoundAction ,qi::_1, qi::_2)]; - boundAction.name("bound action"); - - invertAction = qi::lit("invert")[qi::_val = MAKE(storm::properties::action::InvertAction, )]; - invertAction.name("invert action"); - - formulaAction = (qi::lit("formula") > qi::lit("(") >> stateFormula >> qi::lit(")"))[qi::_val = - MAKE(storm::properties::action::FormulaAction, qi::_1)]; - formulaAction.name("formula action"); - - rangeAction = ( - ((qi::lit("range") >> qi::lit("(") >> qi::uint_ >> qi::lit(",")) > qi::uint_ >> qi::lit(")"))[qi::_val = - MAKE(storm::properties::action::RangeAction, qi::_1, qi::_2)] | - (qi::lit("range") >> qi::lit("(") >> qi::uint_ >> qi::lit(")"))[qi::_val = - MAKE(storm::properties::action::RangeAction, qi::_1, qi::_1 + 1)] - ); - rangeAction.name("range action"); - - sortAction = ( - (qi::lit("sort") >> qi::lit("(") >> sortingCategory >> qi::lit(")"))[qi::_val = - MAKE(storm::properties::action::SortAction, qi::_1)] | - (qi::lit("sort") >> qi::lit("(") >> sortingCategory >> qi::lit(", ") >> (qi::lit("ascending") | qi::lit("asc")) > qi::lit(")"))[qi::_val = - MAKE(storm::properties::action::SortAction, qi::_1, true)] | - (qi::lit("sort") >> qi::lit("(") >> sortingCategory >> qi::lit(", ") >> (qi::lit("descending") | qi::lit("desc")) > qi::lit(")"))[qi::_val = - MAKE(storm::properties::action::SortAction, qi::_1, false)] - ); - sortAction.name("sort action"); - - abstractAction = (qi::lit(";") | qi::eps) >> (boundAction | invertAction | formulaAction | rangeAction | sortAction) >> (qi::lit(";") | qi::eps); - abstractAction.name("filter action"); - - filter = (qi::lit("filter") >> qi::lit("[") >> +abstractAction >> qi::lit("]") >> qi::lit("(") >> formula >> qi::lit(")"))[qi::_val = - MAKE(csl::CslFilter, qi::_2, qi::_1)] | - ((qi::lit("filter") >> qi::lit("[") >> qi::lit("max")) > +abstractAction >> qi::lit("]") >> qi::lit("(") >> formula >> qi::lit(")"))[qi::_val = - MAKE(csl::CslFilter, qi::_2, qi::_1, storm::properties::MAXIMIZE)] | - ((qi::lit("filter") >> qi::lit("[") >> qi::lit("min")) > +abstractAction >> qi::lit("]") >> qi::lit("(") >> formula >> qi::lit(")"))[qi::_val = - MAKE(csl::CslFilter, qi::_2, qi::_1, storm::properties::MINIMIZE)] | - (noBoundOperator)[qi::_val = - qi::_1] | - (formula)[qi::_val = - MAKE(csl::CslFilter, qi::_1)]; - - filter.name("CSL formula filter"); - - start = (((filter) > (comment | qi::eps))[qi::_val = qi::_1] | comment[qi::_val = MAKE(csl::CslFilter, nullptr)] ) > qi::eoi; - start.name("CSL formula filter start"); - - } - - qi::rule>(), Skipper> start; - qi::rule>(), Skipper> filter; - - qi::rule>(), Skipper> noBoundOperator; - qi::rule>(), Skipper> probabilisticNoBoundOperator; - qi::rule>(), Skipper> steadyStateNoBoundOperator; - - qi::rule>(), Skipper> abstractAction; - qi::rule>(), Skipper> boundAction; - qi::rule>(), Skipper> invertAction; - qi::rule>(), Skipper> formulaAction; - qi::rule>(), Skipper> rangeAction; - qi::rule>(), Skipper> sortAction; - - qi::rule>(), Skipper> formula; - qi::rule>(), Skipper> comment; - - qi::rule>(), Skipper> stateFormula; - qi::rule>(), Skipper> atomicStateFormula; - - qi::rule>(), Skipper> andFormula; - qi::rule>(), Skipper> atomicProposition; - qi::rule>(), Skipper> orFormula; - qi::rule>(), Skipper> notFormula; - qi::rule>(), Skipper> probabilisticBoundOperator; - qi::rule>(), Skipper> steadyStateBoundOperator; - - qi::rule>(), Skipper> pathFormula; - qi::rule>(), Skipper> timeBoundedEventually; - qi::rule>(), Skipper> eventually; - qi::rule>(), Skipper> next; - qi::rule>(), Skipper> globally; - qi::rule>(), qi::locals< std::shared_ptr>>, Skipper> timeBoundedUntil; - qi::rule>(), qi::locals< std::shared_ptr>>, Skipper> until; - - - qi::rule freeIdentifierName; - qi::rule comparisonType; - qi::rule::SortingCategory(), Skipper> sortingCategory; - -}; - -std::shared_ptr> CslParser::parseCslFormula(std::string formulaString) { - // Prepare iterators to input. - BaseIteratorType stringIteratorBegin = formulaString.begin(); - BaseIteratorType stringIteratorEnd = formulaString.end(); - PositionIteratorType positionIteratorBegin(stringIteratorBegin, stringIteratorEnd, formulaString); - PositionIteratorType positionIteratorEnd; - - - // Prepare resulting intermediate representation of input. - std::shared_ptr> result_pointer(nullptr); - - CslGrammar grammar; - - // Now, parse the formula from the given string - try { - qi::phrase_parse(positionIteratorBegin, positionIteratorEnd, grammar, boost::spirit::ascii::space, result_pointer); - } catch(const qi::expectation_failure& e) { - // If the parser expected content different than the one provided, display information - // about the location of the error. - const boost::spirit::classic::file_position_base& pos = e.first.get_position(); - - // Construct the error message including a caret display of the position in the - // erroneous line. - std::stringstream msg; - msg << pos.file << ", line " << pos.line << ", column " << pos.column - << ": parse error: expected " << e.what_ << std::endl << "\t" - << e.first.get_currentline() << std::endl << "\t"; - int i = 0; - for (i = 0; i < pos.column; ++i) { - msg << "-"; - } - msg << "^"; - for (; i < 80; ++i) { - msg << "-"; - } - msg << std::endl; - - std::cerr << msg.str(); - - // Now propagate exception. - throw storm::exceptions::WrongFormatException() << msg.str(); - } - - // The syntax can be so wrong that no rule can be matched at all - // In that case, no expectation failure is thrown, but the parser just returns nullptr - // Then, of course the result is not usable, hence we throw a WrongFormatException, too. - if (!result_pointer) { - throw storm::exceptions::WrongFormatException() << "Syntax error in formula"; - } - - return result_pointer; -} - -} /* namespace parser */ -} /* namespace storm */ diff --git a/src/parser/CslParser.h b/src/parser/CslParser.h deleted file mode 100644 index 78b42c844..000000000 --- a/src/parser/CslParser.h +++ /dev/null @@ -1,50 +0,0 @@ -/* - * CslParser.h - * - * Created on: 08.04.2013 - * Author: Thomas Heinemann - */ - -#ifndef STORM_PARSER_CSLPARSER_H_ -#define STORM_PARSER_CSLPARSER_H_ - -#include "src/properties/Csl.h" -#include "src/properties/csl/CslFilter.h" -#include - -namespace storm { -namespace parser { - -/*! - * Reads a Csl formula from a string and returns the formula tree. - * - * If you want to read the formula from a file, use the LtlFileParser class instead. - */ -class CslParser { -public: - - /*! - * Reads a CSL formula from its string representation and parses it into a formula tree, consisting of - * classes in the namespace storm::properties. - * - * If the string could not be parsed successfully, it will throw a wrongFormatException. - * - * @param formulaString The string representation of the formula. - * @throw wrongFormatException If the input could not be parsed successfully. - * @return A CslFilter maintaining the parsed formula. - */ - static std::shared_ptr> parseCslFormula(std::string formulaString); - -private: - - /*! - * Struct for the CSL grammar, that Boost::Spirit uses to parse the formulas. - */ - template - struct CslGrammar; - -}; - -} /* namespace parser */ -} /* namespace storm */ -#endif /* STORM_PARSER_CSLPARSER_H_ */ diff --git a/src/parser/ExpressionParser.cpp b/src/parser/ExpressionParser.cpp index 8733a4d83..826722618 100644 --- a/src/parser/ExpressionParser.cpp +++ b/src/parser/ExpressionParser.cpp @@ -5,7 +5,7 @@ namespace storm { namespace parser { - ExpressionParser::ExpressionParser(storm::expressions::ExpressionManager& manager, qi::symbols const& invalidIdentifiers_) : ExpressionParser::base_type(expression), orOperator_(), andOperator_(), equalityOperator_(), relationalOperator_(), plusOperator_(), multiplicationOperator_(), powerOperator_(), unaryOperator_(), floorCeilOperator_(), minMaxOperator_(), trueFalse_(manager), manager(manager), createExpressions(false), acceptDoubleLiterals(true), identifiers_(nullptr), invalidIdentifiers_(invalidIdentifiers_) { + ExpressionParser::ExpressionParser(storm::expressions::ExpressionManager const& manager, qi::symbols const& invalidIdentifiers_) : ExpressionParser::base_type(expression), orOperator_(), andOperator_(), equalityOperator_(), relationalOperator_(), plusOperator_(), multiplicationOperator_(), powerOperator_(), unaryOperator_(), floorCeilOperator_(), minMaxOperator_(), trueFalse_(manager), manager(manager), createExpressions(false), acceptDoubleLiterals(true), identifiers_(nullptr), invalidIdentifiers_(invalidIdentifiers_) { identifier %= qi::as_string[qi::raw[qi::lexeme[((qi::alpha | qi::char_('_')) >> *(qi::alnum | qi::char_('_')))]]][qi::_pass = phoenix::bind(&ExpressionParser::isValidIdentifier, phoenix::ref(*this), qi::_1)]; identifier.name("identifier"); diff --git a/src/parser/ExpressionParser.h b/src/parser/ExpressionParser.h index bff79fc14..30807d6c5 100644 --- a/src/parser/ExpressionParser.h +++ b/src/parser/ExpressionParser.h @@ -22,7 +22,7 @@ namespace storm { * @param manager The manager responsible for the expressions. * @param invalidIdentifiers_ A symbol table of identifiers that are to be rejected. */ - ExpressionParser(storm::expressions::ExpressionManager& manager, qi::symbols const& invalidIdentifiers_); + ExpressionParser(storm::expressions::ExpressionManager const& manager, qi::symbols const& invalidIdentifiers_); /*! * Sets an identifier mapping that is used to determine valid variables in the expression. The mapped-to @@ -158,7 +158,7 @@ namespace storm { minMaxOperatorStruct minMaxOperator_; struct trueFalseOperatorStruct : qi::symbols { - trueFalseOperatorStruct(storm::expressions::ExpressionManager& manager) { + trueFalseOperatorStruct(storm::expressions::ExpressionManager const& manager) { add ("true", manager.boolean(true)) ("false", manager.boolean(false)); @@ -169,7 +169,7 @@ namespace storm { trueFalseOperatorStruct trueFalse_; // The manager responsible for the expressions. - storm::expressions::ExpressionManager& manager; + storm::expressions::ExpressionManager const& manager; // A flag that indicates whether expressions should actually be generated or just a syntax check shall be // performed. diff --git a/src/parser/FormulaParser.cpp b/src/parser/FormulaParser.cpp new file mode 100644 index 000000000..89f869504 --- /dev/null +++ b/src/parser/FormulaParser.cpp @@ -0,0 +1,221 @@ +#include "src/parser/FormulaParser.h" + +// If the parser fails due to ill-formed data, this exception is thrown. +#include "src/exceptions/WrongFormatException.h" + +namespace storm { + namespace parser { + + FormulaParser::FormulaParser(std::shared_ptr const& manager) : FormulaParser::base_type(start), expressionParser(*manager, keywords_) { + instantaneousRewardFormula = (qi::lit("I=") > qi::uint_)[qi::_val = phoenix::bind(&FormulaParser::createInstantaneousRewardFormula, phoenix::ref(*this), qi::_1)]; + instantaneousRewardFormula.name("instantaneous reward formula"); + + cumulativeRewardFormula = (qi::lit("C<=") > qi::uint_)[qi::_val = phoenix::bind(&FormulaParser::createCumulativeRewardFormula, phoenix::ref(*this), qi::_1)]; + cumulativeRewardFormula.name("cumulative reward formula"); + + reachabilityRewardFormula = (qi::lit("F") > stateFormula)[qi::_val = phoenix::bind(&FormulaParser::createReachabilityRewardFormula, phoenix::ref(*this), qi::_1)]; + reachabilityRewardFormula.name("reachability reward formula"); + + rewardPathFormula = reachabilityRewardFormula | cumulativeRewardFormula | instantaneousRewardFormula; + rewardPathFormula.name("reward path formula"); + + expressionFormula = expressionParser[qi::_val = phoenix::bind(&FormulaParser::createAtomicExpressionFormula, phoenix::ref(*this), qi::_1)]; + expressionFormula.name("expression formula"); + + label = qi::as_string[qi::raw[qi::lexeme[((qi::alpha | qi::char_('_')) >> *(qi::alnum | qi::char_('_')))]]]; + label.name("label"); + + labelFormula = (qi::lit("\"") >> label >> qi::lit("\""))[qi::_val = phoenix::bind(&FormulaParser::createAtomicLabelFormula, phoenix::ref(*this), qi::_1)]; + labelFormula.name("label formula"); + + booleanLiteralFormula = (qi::lit("true")[qi::_a = true] | qi::lit("false")[qi::_a = false])[qi::_val = phoenix::bind(&FormulaParser::createBooleanLiteralFormula, phoenix::ref(*this), qi::_a)]; + booleanLiteralFormula.name("boolean literal formula"); + + atomicStateFormula = booleanLiteralFormula | labelFormula | expressionFormula | qi::lit("(") > stateFormula > qi::lit(")"); + atomicStateFormula.name("atomic state formula"); + + eventuallyFormula = (qi::lit("F") > formula)[qi::_val = phoenix::bind(&FormulaParser::createEventuallyFormula, phoenix::ref(*this), qi::_1)]; + eventuallyFormula.name("eventually formula"); + + globallyFormula = (qi::lit("G") > formula)[qi::_val = phoenix::bind(&FormulaParser::createGloballyFormula, phoenix::ref(*this), qi::_1)]; + globallyFormula.name("globally formula"); + + nextFormula = (qi::lit("X") > formula)[qi::_val = phoenix::bind(&FormulaParser::createNextFormula, phoenix::ref(*this), qi::_1)]; + nextFormula.name("next formula"); + + boundedUntilFormula = (formula > (qi::lit("U<=") > qi::uint_ > formula))[qi::_val = phoenix::bind(&FormulaParser::createBoundedUntilFormula, phoenix::ref(*this), qi::_1, qi::_2, qi::_3)]; + boundedUntilFormula.name("bounded until formula"); + + untilFormula = (formula >> (qi::lit("U") > formula))[qi::_val = phoenix::bind(&FormulaParser::createUntilFormula, phoenix::ref(*this), qi::_1, qi::_2)]; + untilFormula.name("until formula"); + + conditionalFormula = (formula >> (qi::lit("||") > formula))[qi::_val = phoenix::bind(&FormulaParser::createConditionalFormula, phoenix::ref(*this), qi::_1, qi::_2)]; + conditionalFormula.name("conditional formula"); + + pathFormula = eventuallyFormula | globallyFormula | nextFormula | conditionalFormula | boundedUntilFormula | untilFormula; + pathFormula.name("path formula"); + + formula = stateFormula | pathFormula; + formula.name("formula"); + + operatorInformation = (-optimalityOperator_[qi::_a = qi::_1] >> ((relationalOperator_[qi::_b = qi::_1] > qi::double_[qi::_c = qi::_1]) | qi::lit("=") > qi::lit("?")))[qi::_val = phoenix::construct, boost::optional, boost::optional>>(qi::_a, qi::_b, qi::_c)]; + operatorInformation.name("operator information"); + + steadyStateOperator = (qi::lit("S") > operatorInformation > qi::lit("[") > stateFormula > qi::lit("]"))[qi::_val = phoenix::bind(&FormulaParser::createSteadyStateOperatorFormula, phoenix::ref(*this), qi::_1, qi::_2)]; + steadyStateOperator.name("steady state operator"); + + rewardOperator = (qi::lit("R") > operatorInformation > qi::lit("[") > rewardPathFormula > qi::lit("]"))[qi::_val = phoenix::bind(&FormulaParser::createRewardOperatorFormula, phoenix::ref(*this), qi::_1, qi::_2)]; + rewardOperator.name("reward operator"); + + probabilityOperator = (qi::lit("P") > operatorInformation > qi::lit("[") > pathFormula > qi::lit("]"))[qi::_val = phoenix::bind(&FormulaParser::createProbabilityOperatorFormula, phoenix::ref(*this), qi::_1, qi::_2)]; + probabilityOperator.name("probability operator"); + + andStateFormula = (stateFormula >> (qi::lit("&") > stateFormula))[qi::_val = phoenix::bind(&FormulaParser::createBinaryBooleanStateFormula, phoenix::ref(*this), qi::_1, qi::_2, storm::logic::BinaryBooleanStateFormula::OperatorType::And)]; + andStateFormula.name("and state formula"); + + orStateFormula = (andStateFormula >> (qi::lit("|") > andStateFormula))[qi::_val = phoenix::bind(&FormulaParser::createBinaryBooleanStateFormula, phoenix::ref(*this), qi::_1, qi::_2, storm::logic::BinaryBooleanStateFormula::OperatorType::Or)]; + orStateFormula.name("or state formula"); + + stateFormula = (atomicStateFormula | probabilityOperator | rewardOperator | steadyStateOperator | orStateFormula); + stateFormula.name("state formula"); + + start = qi::eps > stateFormula > qi::eoi; + start.name("start"); + + debug(start); + debug(stateFormula); + debug(orStateFormula); + debug(andStateFormula); + debug(probabilityOperator); + debug(rewardOperator); + debug(steadyStateOperator); + // debug(operatorInformation); + debug(formula); + debug(pathFormula); + debug(conditionalFormula); + debug(nextFormula); + debug(globallyFormula); + debug(eventuallyFormula); + debug(atomicStateFormula); + debug(booleanLiteralFormula); + debug(labelFormula); + debug(expressionFormula); + debug(rewardPathFormula); + debug(reachabilityRewardFormula); + debug(cumulativeRewardFormula); + debug(instantaneousRewardFormula); + + // Enable error reporting. + qi::on_error(start, handler(qi::_1, qi::_2, qi::_3, qi::_4)); + qi::on_error(stateFormula, handler(qi::_1, qi::_2, qi::_3, qi::_4)); + qi::on_error(orStateFormula, handler(qi::_1, qi::_2, qi::_3, qi::_4)); + qi::on_error(andStateFormula, handler(qi::_1, qi::_2, qi::_3, qi::_4)); + qi::on_error(probabilityOperator, handler(qi::_1, qi::_2, qi::_3, qi::_4)); + qi::on_error(rewardOperator, handler(qi::_1, qi::_2, qi::_3, qi::_4)); + qi::on_error(steadyStateOperator, handler(qi::_1, qi::_2, qi::_3, qi::_4)); + qi::on_error(operatorInformation, handler(qi::_1, qi::_2, qi::_3, qi::_4)); + qi::on_error(formula, handler(qi::_1, qi::_2, qi::_3, qi::_4)); + qi::on_error(pathFormula, handler(qi::_1, qi::_2, qi::_3, qi::_4)); + qi::on_error(conditionalFormula, handler(qi::_1, qi::_2, qi::_3, qi::_4)); + qi::on_error(untilFormula, handler(qi::_1, qi::_2, qi::_3, qi::_4)); + qi::on_error(nextFormula, handler(qi::_1, qi::_2, qi::_3, qi::_4)); + qi::on_error(globallyFormula, handler(qi::_1, qi::_2, qi::_3, qi::_4)); + qi::on_error(eventuallyFormula, handler(qi::_1, qi::_2, qi::_3, qi::_4)); + qi::on_error(atomicStateFormula, handler(qi::_1, qi::_2, qi::_3, qi::_4)); + qi::on_error(booleanLiteralFormula, handler(qi::_1, qi::_2, qi::_3, qi::_4)); + qi::on_error(labelFormula, handler(qi::_1, qi::_2, qi::_3, qi::_4)); + qi::on_error(expressionFormula, handler(qi::_1, qi::_2, qi::_3, qi::_4)); + qi::on_error(rewardPathFormula, handler(qi::_1, qi::_2, qi::_3, qi::_4)); + qi::on_error(reachabilityRewardFormula, handler(qi::_1, qi::_2, qi::_3, qi::_4)); + qi::on_error(cumulativeRewardFormula, handler(qi::_1, qi::_2, qi::_3, qi::_4)); + qi::on_error(instantaneousRewardFormula, handler(qi::_1, qi::_2, qi::_3, qi::_4)); + } + + std::shared_ptr FormulaParser::parseFromString(std::string const& formulaString, std::shared_ptr const& manager) { + PositionIteratorType first(formulaString.begin()); + PositionIteratorType iter = first; + PositionIteratorType last(formulaString.end()); + + // Create empty result; + std::shared_ptr result; + + // Create grammar. + storm::parser::FormulaParser grammar(manager); + try { + // Start parsing. + bool succeeded = qi::phrase_parse(iter, last, grammar, boost::spirit::ascii::space | qi::lit("//") >> *(qi::char_ - qi::eol) >> qi::eol, result); + STORM_LOG_THROW(succeeded, storm::exceptions::WrongFormatException, "Could not parse formula."); + STORM_LOG_DEBUG("Parsed formula successfully."); + } catch (qi::expectation_failure const& e) { + STORM_LOG_THROW(false, storm::exceptions::WrongFormatException, e.what_); + } + + return result; + } + + std::shared_ptr FormulaParser::createInstantaneousRewardFormula(unsigned stepCount) const { + return std::shared_ptr(new storm::logic::InstantaneousRewardFormula(static_cast(stepCount))); + } + + std::shared_ptr FormulaParser::createCumulativeRewardFormula(unsigned stepBound) const { + return std::shared_ptr(new storm::logic::CumulativeRewardFormula(static_cast(stepBound))); + } + + std::shared_ptr FormulaParser::createReachabilityRewardFormula(std::shared_ptr const& stateFormula) const { + return std::shared_ptr(new storm::logic::ReachabilityRewardFormula(stateFormula)); + } + + std::shared_ptr FormulaParser::createAtomicExpressionFormula(storm::expressions::Expression const& expression) const { + return std::shared_ptr(new storm::logic::AtomicExpressionFormula(expression)); + } + + std::shared_ptr FormulaParser::createBooleanLiteralFormula(bool literal) const { + return std::shared_ptr(new storm::logic::BooleanLiteralFormula(literal)); + } + + std::shared_ptr FormulaParser::createAtomicLabelFormula(std::string const& label) const { + std::cout << "creating atomic label formula" << std::endl; + return std::shared_ptr(new storm::logic::AtomicLabelFormula(label)); + } + + std::shared_ptr FormulaParser::createEventuallyFormula(std::shared_ptr const& subformula) const { + return std::shared_ptr(new storm::logic::EventuallyFormula(subformula)); + } + + std::shared_ptr FormulaParser::createGloballyFormula(std::shared_ptr const& subformula) const { + return std::shared_ptr(new storm::logic::GloballyFormula(subformula)); + } + + std::shared_ptr FormulaParser::createNextFormula(std::shared_ptr const& subformula) const { + return std::shared_ptr(new storm::logic::NextFormula(subformula)); + } + + std::shared_ptr FormulaParser::createUntilFormula(std::shared_ptr const& leftSubformula, std::shared_ptr const& rightSubformula) { + return std::shared_ptr(new storm::logic::UntilFormula(leftSubformula, rightSubformula)); + } + + std::shared_ptr FormulaParser::createBoundedUntilFormula(std::shared_ptr const& leftSubformula, unsigned stepBound, std::shared_ptr const& rightSubformula) const { + return std::shared_ptr(new storm::logic::BoundedUntilFormula(leftSubformula, rightSubformula, static_cast(stepBound))); + } + + std::shared_ptr FormulaParser::createConditionalFormula(std::shared_ptr const& leftSubformula, std::shared_ptr const& rightSubformula) const { + return std::shared_ptr(new storm::logic::ConditionalPathFormula(leftSubformula, rightSubformula)); + } + + std::shared_ptr FormulaParser::createSteadyStateOperatorFormula(std::tuple, boost::optional, boost::optional> const& operatorInformation, std::shared_ptr const& subformula) const { + return std::shared_ptr(new storm::logic::SteadyStateOperatorFormula(std::get<0>(operatorInformation), std::get<1>(operatorInformation), std::get<2>(operatorInformation), subformula)); + } + + std::shared_ptr FormulaParser::createRewardOperatorFormula(std::tuple, boost::optional, boost::optional> const& operatorInformation, std::shared_ptr const& subformula) const { + return std::shared_ptr(new storm::logic::RewardOperatorFormula(std::get<0>(operatorInformation), std::get<1>(operatorInformation), std::get<2>(operatorInformation), subformula)); + } + + std::shared_ptr FormulaParser::createProbabilityOperatorFormula(std::tuple, boost::optional, boost::optional> const& operatorInformation, std::shared_ptr const& subformula) { + return std::shared_ptr(new storm::logic::ProbabilityOperatorFormula(std::get<0>(operatorInformation), std::get<1>(operatorInformation), std::get<2>(operatorInformation), subformula)); + } + + std::shared_ptr FormulaParser::createBinaryBooleanStateFormula(std::shared_ptr const& leftSubformula, std::shared_ptr const& rightSubformula, storm::logic::BinaryBooleanStateFormula::OperatorType operatorType) { + return std::shared_ptr(new storm::logic::BinaryBooleanStateFormula(operatorType, leftSubformula, rightSubformula)); + } + } // namespace parser +} // namespace storm diff --git a/src/parser/FormulaParser.h b/src/parser/FormulaParser.h new file mode 100644 index 000000000..3c13f65a7 --- /dev/null +++ b/src/parser/FormulaParser.h @@ -0,0 +1,152 @@ +#ifndef STORM_PARSER_PRCTLPARSER_H_ +#define STORM_PARSER_PRCTLPARSER_H_ + +#include + +#include "src/parser/SpiritParserDefinitions.h" +#include "src/parser/ExpressionParser.h" +#include "src/logic/Formulas.h" +#include "src/storage/expressions/Expression.h" +#include "src/utility/macros.h" + +namespace storm { + namespace parser { + + class FormulaParser : public qi::grammar(), Skipper> { + public: + + /*! + * Parses the formula given by the provided string. + * + * @param formulaString The formula as a string. + * @return The resulting formula representation. + */ + static std::shared_ptr parseFromString(std::string const& formulaString, std::shared_ptr const& manager = std::shared_ptr(new storm::expressions::ExpressionManager())); + + private: + FormulaParser(std::shared_ptr const& manager); + + struct keywordsStruct : qi::symbols { + keywordsStruct() { + add + ("true", 1) + ("false", 2) + ("min", 3) + ("max", 4); + } + }; + + // A parser used for recognizing the keywords. + keywordsStruct keywords_; + + struct relationalOperatorStruct : qi::symbols { + relationalOperatorStruct() { + add + (">=", storm::logic::ComparisonType::GreaterEqual) + (">", storm::logic::ComparisonType::Greater) + ("<=", storm::logic::ComparisonType::LessEqual) + ("<", storm::logic::ComparisonType::Less); + } + }; + + // A parser used for recognizing the operators at the "relational" precedence level. + relationalOperatorStruct relationalOperator_; + + struct booleanOperatorStruct : qi::symbols { + booleanOperatorStruct() { + add + ("&", storm::logic::BinaryBooleanStateFormula::OperatorType::And) + ("|", storm::logic::BinaryBooleanStateFormula::OperatorType::Or); + } + }; + + // A parser used for recognizing the operators at the "boolean" precedence level. + booleanOperatorStruct booleanOperator_; + + struct optimalityOperatorStruct : qi::symbols { + optimalityOperatorStruct() { + add + ("min", storm::logic::OptimalityType::Minimize) + ("max", storm::logic::OptimalityType::Maximize); + } + }; + + // A parser used for recognizing the optimality operators. + optimalityOperatorStruct optimalityOperator_; + + // Parser and manager used for recognizing expressions. + storm::parser::ExpressionParser expressionParser; + + // Functor used for displaying error information. + struct ErrorHandler { + typedef qi::error_handler_result result_type; + + template + qi::error_handler_result operator()(T1 b, T2 e, T3 where, T4 const& what) const { + std::stringstream whatAsString; + whatAsString << what; + STORM_LOG_THROW(false, storm::exceptions::WrongFormatException, "Parsing error in line " << get_line(where) << ": " << " expecting " << whatAsString.str() << "."); + return qi::fail; + } + }; + + // An error handler function. + phoenix::function handler; + + qi::rule(), Skipper> start; + + qi::rule, boost::optional, boost::optional>(), qi::locals, boost::optional, boost::optional>, Skipper> operatorInformation; + qi::rule(), Skipper> probabilityOperator; + qi::rule(), Skipper> rewardOperator; + qi::rule(), Skipper> steadyStateOperator; + + qi::rule(), Skipper> formula; + qi::rule(), Skipper> stateFormula; + qi::rule(), Skipper> pathFormula; + + qi::rule(), Skipper> atomicStateFormula; + qi::rule label; + + qi::rule(), Skipper> andStateFormula; + qi::rule(), Skipper> orStateFormula; + qi::rule(), Skipper> notStateFormula; + qi::rule(), Skipper> labelFormula; + qi::rule(), Skipper> expressionFormula; + qi::rule(), qi::locals, Skipper> booleanLiteralFormula; + + qi::rule(), Skipper> conditionalFormula; + qi::rule(), Skipper> eventuallyFormula; + qi::rule(), Skipper> nextFormula; + qi::rule(), Skipper> globallyFormula; + qi::rule(), Skipper> boundedUntilFormula; + qi::rule(), Skipper> untilFormula; + + qi::rule(), Skipper> rewardPathFormula; + qi::rule(), Skipper> cumulativeRewardFormula; + qi::rule(), Skipper> reachabilityRewardFormula; + qi::rule(), Skipper> instantaneousRewardFormula; + + // Methods that actually create the expression objects. + std::shared_ptr createInstantaneousRewardFormula(unsigned stepCount) const; + std::shared_ptr createCumulativeRewardFormula(unsigned stepBound) const; + std::shared_ptr createReachabilityRewardFormula(std::shared_ptr const& stateFormula) const; + std::shared_ptr createAtomicExpressionFormula(storm::expressions::Expression const& expression) const; + std::shared_ptr createBooleanLiteralFormula(bool literal) const; + std::shared_ptr createAtomicLabelFormula(std::string const& label) const; + std::shared_ptr createEventuallyFormula(std::shared_ptr const& subformula) const; + std::shared_ptr createGloballyFormula(std::shared_ptr const& subformula) const; + std::shared_ptr createNextFormula(std::shared_ptr const& subformula) const; + std::shared_ptr createUntilFormula(std::shared_ptr const& leftSubformula, std::shared_ptr const& rightSubformula); + std::shared_ptr createBoundedUntilFormula(std::shared_ptr const& leftSubformula, unsigned stepBound, std::shared_ptr const& rightSubformula) const; + std::shared_ptr createConditionalFormula(std::shared_ptr const& leftSubformula, std::shared_ptr const& rightSubformula) const; + std::shared_ptr createSteadyStateOperatorFormula(std::tuple, boost::optional, boost::optional> const& operatorInformation, std::shared_ptr const& subformula) const; + std::shared_ptr createRewardOperatorFormula(std::tuple, boost::optional, boost::optional> const& operatorInformation, std::shared_ptr const& subformula) const; + std::shared_ptr createProbabilityOperatorFormula(std::tuple, boost::optional, boost::optional> const& operatorInformation, std::shared_ptr const& subformula); + std::shared_ptr createBinaryBooleanStateFormula(std::shared_ptr const& leftSubformula, std::shared_ptr const& rightSubformula, storm::logic::BinaryBooleanStateFormula::OperatorType operatorType); + + }; + + } // namespace parser +} // namespace storm + +#endif /* STORM_PARSER_PRCTLPARSER_H_ */ diff --git a/src/parser/LtlFileParser.cpp b/src/parser/LtlFileParser.cpp deleted file mode 100644 index c7b056183..000000000 --- a/src/parser/LtlFileParser.cpp +++ /dev/null @@ -1,43 +0,0 @@ -/* - * LtlFileParser.cpp - * - * Created on: 13.05.2013 - * Author: thomas - */ - -#include - -#include "LtlFileParser.h" -#include "LtlParser.h" - -#include "src/exceptions/FileIoException.h" - -namespace storm { -namespace parser { - -std::list>> LtlFileParser::parseLtlFile(std::string filename) { - // Open file - std::ifstream inputFileStream(filename, std::ios::in); - - if (!inputFileStream.is_open()) { - std::string message = "Error while opening file "; - throw storm::exceptions::FileIoException() << message << filename; - } - - std::list>> result; - - while(!inputFileStream.eof()) { - std::string line; - //The while loop reads the input file line by line - while (std::getline(inputFileStream, line)) { - result.push_back(storm::parser::LtlParser::parseLtlFormula(line)); - } - } - - return result; -} - -} //namespace parser -} //namespace storm - - diff --git a/src/parser/LtlFileParser.h b/src/parser/LtlFileParser.h deleted file mode 100644 index 4caa67d8f..000000000 --- a/src/parser/LtlFileParser.h +++ /dev/null @@ -1,34 +0,0 @@ -/* - * LtlFileParser.h - * - * Created on: 13.05.2013 - * Author: Thonas Heinemann - */ - -#ifndef LTLFILEPARSER_H_ -#define LTLFILEPARSER_H_ - -#include "properties/Ltl.h" -#include "src/properties/ltl/LtlFilter.h" - -#include - -namespace storm { -namespace parser { - -class LtlFileParser { -public: - - /*! - * Parses each line of a given file as prctl formula and returns a list containing the results of the parsing. - * - * @param filename Name and path to the file in which the formula strings can be found. - * @return The list of parsed formulas. - */ - static std::list>> parseLtlFile(std::string filename); -}; - -} //namespace parser -} //namespace storm - -#endif /* LTLFILEPARSER_H_ */ diff --git a/src/parser/LtlParser.cpp b/src/parser/LtlParser.cpp deleted file mode 100644 index 79059e994..000000000 --- a/src/parser/LtlParser.cpp +++ /dev/null @@ -1,239 +0,0 @@ -/* - * LtlParser.cpp - * - * Created on: 22.04.2013 - * Author: thomas - */ - -#include "LtlParser.h" - -#include "src/utility/OsDetection.h" -#include "src/utility/constants.h" - -// The action class headers. -#include "src/properties/actions/AbstractAction.h" -#include "src/properties/actions/BoundAction.h" -#include "src/properties/actions/InvertAction.h" -#include "src/properties/actions/RangeAction.h" -#include "src/properties/actions/SortAction.h" - -// If the parser fails due to ill-formed data, this exception is thrown. -#include "src/exceptions/WrongFormatException.h" - -// Used for Boost spirit. -#include -#include -#include - -// Include headers for spirit iterators. Needed for diagnostics and input stream iteration. -#include -#include - -// Needed for file IO. -#include -#include -#include - - -// Some typedefs and namespace definitions to reduce code size. -#define MAKE(Type, ...) phoenix::construct>(phoenix::new_(__VA_ARGS__)) -typedef std::string::const_iterator BaseIteratorType; -typedef boost::spirit::classic::position_iterator2 PositionIteratorType; -namespace qi = boost::spirit::qi; -namespace phoenix = boost::phoenix; -namespace ltl = storm::properties::ltl; - - -namespace storm { - -namespace parser { - -template -struct LtlParser::LtlGrammar : qi::grammar>(), Skipper > { - LtlGrammar() : LtlGrammar::base_type(start) { - //This block contains helper rules that may be used several times - freeIdentifierName = qi::lexeme[qi::alpha >> *(qi::alnum | qi::char_('_'))]; - comparisonType = ( - (qi::lit(">="))[qi::_val = storm::properties::GREATER_EQUAL] | - (qi::lit(">"))[qi::_val = storm::properties::GREATER] | - (qi::lit("<="))[qi::_val = storm::properties::LESS_EQUAL] | - (qi::lit("<"))[qi::_val = storm::properties::LESS]); - sortingCategory = ( - (qi::lit("index"))[qi::_val = storm::properties::action::SortAction::INDEX] | - (qi::lit("value"))[qi::_val = storm::properties::action::SortAction::VALUE] - ); - // Comment: Empty line or line starting with "//" - comment = (qi::lit("//") >> *(qi::char_))[qi::_val = nullptr]; - - freeIdentifierName = qi::lexeme[+(qi::alpha | qi::char_('_'))]; - - // This block defines rules for parsing state formulas - formula %= orFormula; - formula.name("LTL formula"); - orFormula = andFormula[qi::_val = qi::_1] > *(qi::lit("|") > andFormula)[qi::_val = - MAKE(ltl::Or, qi::_val, qi::_1)]; - orFormula.name("Or"); - andFormula = untilFormula[qi::_val = qi::_1] > *(qi::lit("&") > untilFormula)[qi::_val = - MAKE(ltl::And, qi::_val, qi::_1)]; - andFormula.name("And"); - untilFormula = notFormula[qi::_val = qi::_1] > - *(((qi::lit("U") >> qi::lit("<=")) > qi::int_ > notFormula)[qi::_val = MAKE(ltl::BoundedUntil, qi::_val, qi::_2, qi::_1)] | - (qi::lit("U") > notFormula)[qi::_val = MAKE(ltl::Until, qi::_val, qi::_1)]); - until.name("Until"); - notFormula = atomicLtlFormula[qi::_val = qi::_1] | (qi::lit("!") > atomicLtlFormula)[qi::_val = - MAKE(ltl::Not, qi::_1)]; - notFormula.name("Not"); - - //This block defines rules for "atomic" state formulas - //(Propositions, probabilistic/reward formulas, and state formulas in brackets) - atomicLtlFormula %= pathFormula | atomicProposition | qi::lit("(") >> formula >> qi::lit(")")| qi::lit("[") >> formula >> qi::lit("]"); - atomicLtlFormula.name("Atomic LTL formula"); - atomicProposition = (freeIdentifierName)[qi::_val = MAKE(ltl::Ap, qi::_1)] | (qi::lit("\"") > (freeIdentifierName)[qi::_val = MAKE(ltl::Ap, qi::_1)] > qi::lit("\"")); - atomicProposition.name("Atomic Proposition"); - - //This block defines rules for parsing probabilistic path formulas - pathFormula = (boundedEventually | eventually | globally | next); - pathFormula.name("Path Formula"); - boundedEventually = ((qi::lit("F") >> qi::lit("<=")) > qi::int_ > formula)[qi::_val = - MAKE(ltl::BoundedEventually, qi::_2, qi::_1)]; - boundedEventually.name("Bounded Eventually"); - eventually = (qi::lit("F") >> formula)[qi::_val = - MAKE(ltl::Eventually, qi::_1)]; - eventually.name("Eventually"); - globally = (qi::lit("G") >> formula)[qi::_val = - MAKE(ltl::Globally, qi::_1)]; - globally.name("Globally"); - next = (qi::lit("X") >> formula)[qi::_val = - MAKE(ltl::Next, qi::_1)]; - next.name("Next"); - - // This block defines rules for parsing filter actions. - boundAction = (qi::lit("bound") > qi::lit("(") >> comparisonType >> qi::lit(",") >> qi::double_ >> qi::lit(")"))[qi::_val = - MAKE(storm::properties::action::BoundAction ,qi::_1, qi::_2)]; - boundAction.name("bound action"); - - invertAction = qi::lit("invert")[qi::_val = MAKE(storm::properties::action::InvertAction, )]; - invertAction.name("invert action"); - - rangeAction = ( - ((qi::lit("range") >> qi::lit("(") >> qi::uint_ >> qi::lit(",")) > qi::uint_ >> qi::lit(")"))[qi::_val = - MAKE(storm::properties::action::RangeAction, qi::_1, qi::_2)] | - (qi::lit("range") >> qi::lit("(") >> qi::uint_ >> qi::lit(")"))[qi::_val = - MAKE(storm::properties::action::RangeAction, qi::_1, qi::_1 + 1)] - ); - rangeAction.name("range action"); - - sortAction = ( - (qi::lit("sort") >> qi::lit("(") >> sortingCategory >> qi::lit(")"))[qi::_val = - MAKE(storm::properties::action::SortAction, qi::_1)] | - (qi::lit("sort") >> qi::lit("(") >> sortingCategory >> qi::lit(", ") >> (qi::lit("ascending") | qi::lit("asc")) > qi::lit(")"))[qi::_val = - MAKE(storm::properties::action::SortAction, qi::_1, true)] | - (qi::lit("sort") >> qi::lit("(") >> sortingCategory >> qi::lit(", ") >> (qi::lit("descending") | qi::lit("desc")) > qi::lit(")"))[qi::_val = - MAKE(storm::properties::action::SortAction, qi::_1, false)] - ); - sortAction.name("sort action"); - - abstractAction = (qi::lit(";") | qi::eps) >> (boundAction | invertAction | rangeAction | sortAction) >> (qi::lit(";") | qi::eps); - abstractAction.name("filter action"); - - filter = (qi::lit("filter") >> qi::lit("[") >> +abstractAction >> qi::lit("]") > qi::lit("(") >> formula >> qi::lit(")"))[qi::_val = - MAKE(ltl::LtlFilter, qi::_2, qi::_1)] | - ((qi::lit("filter") >> qi::lit("[") >> qi::lit("max")) > +abstractAction >> qi::lit("]") >> qi::lit("(") >> formula >> qi::lit(")"))[qi::_val = - MAKE(ltl::LtlFilter, qi::_2, qi::_1, storm::properties::MAXIMIZE)] | - ((qi::lit("filter") >> qi::lit("[") >> qi::lit("min")) > +abstractAction >> qi::lit("]") >> qi::lit("(") >> formula >> qi::lit(")"))[qi::_val = - MAKE(ltl::LtlFilter, qi::_2, qi::_1, storm::properties::MINIMIZE)] | - (formula)[qi::_val = - MAKE(ltl::LtlFilter, qi::_1)]; - filter.name("LTL formula filter"); - - start = (((filter) > (comment | qi::eps))[qi::_val = qi::_1] | comment[qi::_val = MAKE(ltl::LtlFilter, nullptr)] ) > qi::eoi; - start.name("start"); - } - - qi::rule>(), Skipper> start; - qi::rule>(), Skipper> filter; - - qi::rule>(), Skipper> abstractAction; - qi::rule>(), Skipper> boundAction; - qi::rule>(), Skipper> invertAction; - qi::rule>(), Skipper> rangeAction; - qi::rule>(), Skipper> sortAction; - - qi::rule>(), Skipper> comment; - qi::rule>(), Skipper> formula; - qi::rule>(), Skipper> atomicLtlFormula; - - qi::rule>(), Skipper> andFormula; - qi::rule>(), Skipper> untilFormula; - qi::rule>(), Skipper> atomicProposition; - qi::rule>(), Skipper> orFormula; - qi::rule>(), Skipper> notFormula; - - qi::rule>(), Skipper> pathFormula; - qi::rule>(), Skipper> boundedEventually; - qi::rule>(), Skipper> eventually; - qi::rule>(), Skipper> globally; - qi::rule>(), Skipper> next; - qi::rule>(), qi::locals< std::shared_ptr>>, Skipper> boundedUntil; - qi::rule>(), qi::locals< std::shared_ptr>>, Skipper> until; - - qi::rule freeIdentifierName; - qi::rule comparisonType; - qi::rule::SortingCategory(), Skipper> sortingCategory; -}; - -std::shared_ptr> LtlParser::parseLtlFormula(std::string formulaString) { - // Prepare iterators to input. - BaseIteratorType stringIteratorBegin = formulaString.begin(); - BaseIteratorType stringIteratorEnd = formulaString.end(); - PositionIteratorType positionIteratorBegin(stringIteratorBegin, stringIteratorEnd, formulaString); - PositionIteratorType positionIteratorEnd; - - - // Prepare resulting intermediate representation of input. - std::shared_ptr> result_pointer(nullptr); - - LtlGrammar grammar; - - // Now, parse the formula from the given string - try { - qi::phrase_parse(positionIteratorBegin, positionIteratorEnd, grammar, boost::spirit::ascii::space, result_pointer); - } catch(const qi::expectation_failure& e) { - // If the parser expected content different than the one provided, display information - // about the location of the error. - const boost::spirit::classic::file_position_base& pos = e.first.get_position(); - - // Construct the error message including a caret display of the position in the - // erroneous line. - std::stringstream msg; - msg << pos.file << ", line " << pos.line << ", column " << pos.column - << ": parse error: expected " << e.what_ << std::endl << "\t" - << e.first.get_currentline() << std::endl << "\t"; - int i = 0; - for (i = 0; i < pos.column; ++i) { - msg << "-"; - } - msg << "^"; - for (; i < 80; ++i) { - msg << "-"; - } - msg << std::endl; - - std::cerr << msg.str(); - - // Now propagate exception. - throw storm::exceptions::WrongFormatException() << msg.str(); - } - - // The syntax can be so wrong that no rule can be matched at all - // In that case, no expectation failure is thrown, but the parser just returns nullptr - // Then, of course the result is not usable, hence we throw a WrongFormatException, too. - if (!result_pointer) { - throw storm::exceptions::WrongFormatException() << "Syntax error in formula"; - } - - return result_pointer; -} - -} //namespace parser -} //namespace storm diff --git a/src/parser/LtlParser.h b/src/parser/LtlParser.h deleted file mode 100644 index dac3a63ec..000000000 --- a/src/parser/LtlParser.h +++ /dev/null @@ -1,49 +0,0 @@ -/* - * LtlParser.h - * - * Created on: 22.04.2013 - * Author: thomas - */ - -#ifndef STORM_PARSER_LTLPARSER_H_ -#define STORM_PARSER_LTLPARSER_H_ - -#include "src/properties/Ltl.h" -#include "src/properties/ltl/LtlFilter.h" - -namespace storm { -namespace parser { - -/*! - * Reads a LTL formula from a string and return the formula tree. - * - * If you want to read the formula from a file, use the LtlFileParser class instead. - */ -class LtlParser { -public: - - /*! - * Reads a LTL formula from its string representation and parses it into a formula tree, consisting of - * classes in the namespace storm::properties. - * - * If the string could not be parsed successfully, it will throw a wrongFormatException. - * - * @param formulaString The string representation of the formula. - * @throw wrongFormatException If the input could not be parsed successfully. - * @return A LtlFilter maintaining the parsed formula. - */ - static std::shared_ptr> parseLtlFormula(std::string formulaString); - -private: - - /*! - * Struct for the Ltl grammar, that Boost::Spirit uses to parse the formulas. - */ - template - struct LtlGrammar; - -}; - -} /* namespace parser */ -} /* namespace storm */ -#endif /* STORM_PARSER_LTLPARSER_H_ */ diff --git a/src/parser/PrctlFileParser.cpp b/src/parser/PrctlFileParser.cpp deleted file mode 100644 index 64abd2b15..000000000 --- a/src/parser/PrctlFileParser.cpp +++ /dev/null @@ -1,44 +0,0 @@ -/* - * PrctlFileParser.cpp - * - * Created on: 06.02.2013 - * Author: Thomas Heinemann - */ - -#include - -#include "PrctlFileParser.h" -#include "PrctlParser.h" -#include "src/exceptions/FileIoException.h" - -namespace storm { -namespace parser { - -std::list>> PrctlFileParser::parsePrctlFile(std::string filename) { - // Open file - std::ifstream inputFileStream; - inputFileStream.open(filename, std::ios::in); - - if (!inputFileStream.is_open()) { - std::string message = "Error while opening file "; - throw storm::exceptions::FileIoException() << message << filename; - } - - std::list>> result; - - std::string line; - //The while loop reads the input file line by line - while (std::getline(inputFileStream, line)) { - std::shared_ptr> formula = PrctlParser::parsePrctlFormula(line); - if (formula != nullptr) { - //lines containing comments will be skipped. - LOG4CPLUS_INFO(logger, "Parsed formula \"" + line + "\" into \"" + formula->toString() + "\""); - result.push_back(formula); - } - } - - return result; -} - -} /* namespace parser */ -} /* namespace storm */ diff --git a/src/parser/PrctlFileParser.h b/src/parser/PrctlFileParser.h deleted file mode 100644 index dbf458fbf..000000000 --- a/src/parser/PrctlFileParser.h +++ /dev/null @@ -1,35 +0,0 @@ -/* - * PrctlFileParser.h - * - * Created on: 06.02.2013 - * Author: Thomas Heinemann - */ - -#ifndef STORM_PARSER_PRCTLFILEPARSER_H_ -#define STORM_PARSER_PRCTLFILEPARSER_H_ - -#include "properties/Prctl.h" -#include "src/properties/prctl/PrctlFilter.h" - -#include - -namespace storm { -namespace parser { - -class PrctlFileParser { -public: - - /*! - * Parses each line of a given file as Prctl formula and returns a list containing the results of the parsing. - * - * @param filename Name and path to the file in which the formula strings can be found. - * @return The list of parsed formulas - */ - static std::list>> parsePrctlFile(std::string filename); - -}; - -} /* namespace parser */ -} /* namespace storm */ - -#endif /* STORM_PARSER_PRCTLFILEPARSER_H_ */ diff --git a/src/parser/PrctlParser.cpp b/src/parser/PrctlParser.cpp deleted file mode 100644 index d12fba12b..000000000 --- a/src/parser/PrctlParser.cpp +++ /dev/null @@ -1,306 +0,0 @@ -#include "src/parser/PrctlParser.h" -#include "src/utility/OsDetection.h" -#include "src/utility/constants.h" - -// The action class headers. -#include "src/properties/actions/AbstractAction.h" -#include "src/properties/actions/BoundAction.h" -#include "src/properties/actions/InvertAction.h" -#include "src/properties/actions/FormulaAction.h" -#include "src/properties/actions/RangeAction.h" -#include "src/properties/actions/SortAction.h" - -// If the parser fails due to ill-formed data, this exception is thrown. -#include "src/exceptions/WrongFormatException.h" - -// Used for Boost spirit. -#include -#include -#include -#include - -// Include headers for spirit iterators. Needed for diagnostics and input stream iteration. -#include -#include - -// Needed for file IO. -#include -#include -#include - - -// Some typedefs, namespace definitions and a macro to reduce code size. -#define MAKE(Type, ...) phoenix::construct>(phoenix::new_(__VA_ARGS__)) -typedef std::string::const_iterator BaseIteratorType; -typedef boost::spirit::classic::position_iterator2 PositionIteratorType; -namespace qi = boost::spirit::qi; -namespace phoenix = boost::phoenix; -namespace prctl = storm::properties::prctl; - - -namespace storm { - -namespace parser { - -template -struct PrctlParser::PrctlGrammar : qi::grammar>(), Skipper > { - PrctlGrammar() : PrctlGrammar::base_type(start) { - // This block contains helper rules that may be used several times - freeIdentifierName = qi::lexeme[qi::alpha >> *(qi::alnum | qi::char_('_'))]; - comparisonType = ( - (qi::lit(">="))[qi::_val = storm::properties::GREATER_EQUAL] | - (qi::lit(">"))[qi::_val = storm::properties::GREATER] | - (qi::lit("<="))[qi::_val = storm::properties::LESS_EQUAL] | - (qi::lit("<"))[qi::_val = storm::properties::LESS]); - sortingCategory = ( - (qi::lit("index"))[qi::_val = storm::properties::action::SortAction::INDEX] | - (qi::lit("value"))[qi::_val = storm::properties::action::SortAction::VALUE] - ); - // Comment: Empty line or line starting with "//" - comment = (qi::lit("//") >> *(qi::char_))[qi::_val = nullptr]; - - // This block defines rules for parsing state formulas - stateFormula %= orFormula; - stateFormula.name("state formula"); - orFormula = andFormula[qi::_val = qi::_1] > *(qi::lit("|") > andFormula)[qi::_val = - MAKE(prctl::Or, qi::_val, qi::_1)]; - orFormula.name("or formula"); - andFormula = notFormula[qi::_val = qi::_1] > *(qi::lit("&") > notFormula)[qi::_val = - MAKE(prctl::And, qi::_val, qi::_1)]; - andFormula.name("and formula"); - notFormula = atomicStateFormula[qi::_val = qi::_1] | (qi::lit("!") > atomicStateFormula)[qi::_val = - MAKE(prctl::Not, qi::_1)]; - notFormula.name("not formula"); - - // This block defines rules for "atomic" state formulas - // (Propositions, probabilistic/reward formulas, and state formulas in brackets) - atomicStateFormula %= probabilisticBoundOperator | rewardBoundOperator | atomicProposition | qi::lit("(") >> stateFormula >> qi::lit(")") | qi::lit("[") >> stateFormula >> qi::lit("]"); - atomicStateFormula.name("atomic state formula"); - atomicProposition = (freeIdentifierName)[qi::_val = MAKE(prctl::Ap, qi::_1)] | (qi::lit("\"") > (freeIdentifierName)[qi::_val = MAKE(prctl::Ap, qi::_1)] > qi::lit("\"")); - atomicProposition.name("atomic proposition"); - probabilisticBoundOperator = ((qi::lit("P") >> comparisonType > qi::double_ > pathFormula)[qi::_val = - MAKE(prctl::ProbabilisticBoundOperator, qi::_1, qi::_2, qi::_3)]); - probabilisticBoundOperator.name("probabilistic bound operator"); - rewardBoundOperator = ((qi::lit("R") >> comparisonType > qi::double_ > rewardPathFormula)[qi::_val = - MAKE(prctl::RewardBoundOperator, qi::_1, qi::_2, qi::_3)]); - rewardBoundOperator.name("reward bound operator"); - - // This block defines rules for parsing probabilistic path formulas - pathFormula = (boundedEventually | eventually | next | globally | boundedUntil | until | qi::lit("(") >> pathFormula >> qi::lit(")") | qi::lit("[") >> pathFormula >> qi::lit("]")); - pathFormula.name("path formula"); - boundedEventually = ((qi::lit("F") >> qi::lit("<=")) > qi::int_ > stateFormula)[qi::_val = - MAKE(prctl::BoundedEventually, qi::_2, qi::_1)]; - boundedEventually.name("bounded eventually"); - eventually = (qi::lit("F") > stateFormula)[qi::_val = - MAKE(prctl::Eventually, qi::_1)]; - eventually.name("eventually"); - next = (qi::lit("X") > stateFormula)[qi::_val = - MAKE(prctl::Next, qi::_1)]; - next.name("next"); - globally = (qi::lit("G") > stateFormula)[qi::_val = - MAKE(prctl::Globally, qi::_1)]; - globally.name("globally"); - boundedUntil = (stateFormula[qi::_a = qi::_1] >> qi::lit("U") >> qi::lit("<=") > qi::int_ > stateFormula)[qi::_val = - MAKE(prctl::BoundedUntil, qi::_a, qi::_3, qi::_2)]; - boundedUntil.name("boundedUntil"); - until = (stateFormula[qi::_a = qi::_1] >> qi::lit("U") > stateFormula)[qi::_val = - MAKE(prctl::Until, qi::_a, qi::_2)]; - until.name("until"); - - // This block defines rules for parsing reward path formulas. - rewardPathFormula = (cumulativeReward | reachabilityReward | instantaneousReward | steadyStateReward | qi::lit("(") >> rewardPathFormula >> qi::lit(")") | qi::lit("[") >> rewardPathFormula >> qi::lit("]")); - rewardPathFormula.name("path formula (for reward operator)"); - cumulativeReward = (qi::lit("C") > qi::lit("<=") > qi::double_)[qi::_val = - MAKE(prctl::CumulativeReward, qi::_1)]; - cumulativeReward.name("path formula (for reward operator)"); - reachabilityReward = (qi::lit("F") > stateFormula)[qi::_val = - MAKE(prctl::ReachabilityReward, qi::_1)]; - reachabilityReward.name("path formula (for reward operator)"); - instantaneousReward = (qi::lit("I") > qi::lit("=") > qi::uint_)[qi::_val = - MAKE(prctl::InstantaneousReward, qi::_1)]; - instantaneousReward.name("path formula (for reward operator)"); - steadyStateReward = (qi::lit("S"))[qi::_val = - MAKE(prctl::SteadyStateReward, )]; - - formula = (pathFormula | stateFormula); - formula.name("PRCTL formula"); - - // This block defines rules for parsing formulas with noBoundOperators. - // Note that this is purely for legacy support. - // NoBoundOperators are no longer part of the formula tree and are therefore deprecated. - noBoundOperator = (probabilisticNoBoundOperator | rewardNoBoundOperator); - noBoundOperator.name("no bound operator"); - probabilisticNoBoundOperator = ( - ((qi::lit("P") >> qi::lit("min") >> qi::lit("=")) > qi::lit("?") >> pathFormula )[qi::_val = - MAKE(prctl::PrctlFilter, qi::_1, storm::properties::MINIMIZE)] | - ((qi::lit("P") >> qi::lit("max") >> qi::lit("=")) > qi::lit("?") >> pathFormula )[qi::_val = - MAKE(prctl::PrctlFilter, qi::_1, storm::properties::MAXIMIZE)] | - ((qi::lit("P") >> qi::lit("=")) > qi::lit("?") >> pathFormula )[qi::_val = - MAKE(prctl::PrctlFilter, qi::_1)] - ); - probabilisticNoBoundOperator.name("no bound operator"); - - rewardNoBoundOperator = ( - ((qi::lit("R") >> qi::lit("min") >> qi::lit("=")) > qi::lit("?") >> rewardPathFormula )[qi::_val = - MAKE(prctl::PrctlFilter, qi::_1, storm::properties::MINIMIZE)] | - ((qi::lit("R") >> qi::lit("max") >> qi::lit("=")) > qi::lit("?") >> rewardPathFormula )[qi::_val = - MAKE(prctl::PrctlFilter, qi::_1, storm::properties::MAXIMIZE)] | - ((qi::lit("R") >> qi::lit("=")) > qi::lit("?") >> rewardPathFormula )[qi::_val = - MAKE(prctl::PrctlFilter, qi::_1)] - - ); - rewardNoBoundOperator.name("no bound operator"); - - - // This block defines rules for parsing filter actions. - boundAction = (qi::lit("bound") > qi::lit("(") >> comparisonType >> qi::lit(",") >> qi::double_ >> qi::lit(")"))[qi::_val = - MAKE(storm::properties::action::BoundAction ,qi::_1, qi::_2)]; - boundAction.name("bound action"); - - invertAction = qi::lit("invert")[qi::_val = MAKE(storm::properties::action::InvertAction, )]; - invertAction.name("invert action"); - - formulaAction = (qi::lit("formula") > qi::lit("(") >> stateFormula >> qi::lit(")"))[qi::_val = - MAKE(storm::properties::action::FormulaAction, qi::_1)]; - formulaAction.name("formula action"); - - rangeAction = ( - ((qi::lit("range") >> qi::lit("(") >> qi::uint_ >> qi::lit(",")) > qi::uint_ >> qi::lit(")"))[qi::_val = - MAKE(storm::properties::action::RangeAction, qi::_1, qi::_2)] | - (qi::lit("range") >> qi::lit("(") >> qi::uint_ >> qi::lit(")"))[qi::_val = - MAKE(storm::properties::action::RangeAction, qi::_1, qi::_1 + 1)] - ); - rangeAction.name("range action"); - - sortAction = ( - (qi::lit("sort") >> qi::lit("(") >> sortingCategory >> qi::lit(")"))[qi::_val = - MAKE(storm::properties::action::SortAction, qi::_1)] | - (qi::lit("sort") >> qi::lit("(") >> sortingCategory >> qi::lit(", ") >> (qi::lit("ascending") | qi::lit("asc")) > qi::lit(")"))[qi::_val = - MAKE(storm::properties::action::SortAction, qi::_1, true)] | - (qi::lit("sort") >> qi::lit("(") >> sortingCategory >> qi::lit(", ") >> (qi::lit("descending") | qi::lit("desc")) > qi::lit(")"))[qi::_val = - MAKE(storm::properties::action::SortAction, qi::_1, false)] - ); - sortAction.name("sort action"); - - abstractAction = (qi::lit(";") | qi::eps) >> (boundAction | invertAction | formulaAction | rangeAction | sortAction) >> (qi::lit(";") | qi::eps); - abstractAction.name("filter action"); - - filter = (qi::lit("filter") >> qi::lit("[") >> +abstractAction >> qi::lit("]") > qi::lit("(") >> formula >> qi::lit(")"))[qi::_val = - MAKE(prctl::PrctlFilter, qi::_2, qi::_1)] | - ((qi::lit("filter") >> qi::lit("[") >> qi::lit("max")) > +abstractAction >> qi::lit("]") >> qi::lit("(") >> formula >> qi::lit(")"))[qi::_val = - MAKE(prctl::PrctlFilter, qi::_2, qi::_1, storm::properties::MAXIMIZE)] | - ((qi::lit("filter") >> qi::lit("[") >> qi::lit("min")) > +abstractAction >> qi::lit("]") >> qi::lit("(") >> formula >> qi::lit(")"))[qi::_val = - MAKE(prctl::PrctlFilter, qi::_2, qi::_1, storm::properties::MINIMIZE)] | - (noBoundOperator)[qi::_val = - qi::_1] | - (formula)[qi::_val = - MAKE(prctl::PrctlFilter, qi::_1)]; - filter.name("PRCTL formula filter"); - - start = (((filter) > (comment | qi::eps))[qi::_val = qi::_1] | comment[qi::_val = MAKE(prctl::PrctlFilter, nullptr)]) > qi::eoi; - start.name("start"); - - } - - qi::rule>(), Skipper> start; - qi::rule>(), Skipper> filter; - - qi::rule>(), Skipper> noBoundOperator; - qi::rule>(), Skipper> probabilisticNoBoundOperator; - qi::rule>(), Skipper> rewardNoBoundOperator; - - qi::rule>(), Skipper> abstractAction; - qi::rule>(), Skipper> boundAction; - qi::rule>(), Skipper> invertAction; - qi::rule>(), Skipper> formulaAction; - qi::rule>(), Skipper> rangeAction; - qi::rule>(), Skipper> sortAction; - - qi::rule>(), Skipper> formula; - qi::rule>(), Skipper> comment; - - qi::rule>(), Skipper> stateFormula; - qi::rule>(), Skipper> atomicStateFormula; - - qi::rule>(), Skipper> andFormula; - qi::rule>(), Skipper> atomicProposition; - qi::rule>(), Skipper> orFormula; - qi::rule>(), Skipper> notFormula; - qi::rule>(), Skipper> probabilisticBoundOperator; - qi::rule>(), Skipper> rewardBoundOperator; - - qi::rule>(), Skipper> pathFormula; - qi::rule>(), Skipper> boundedEventually; - qi::rule>(), Skipper> eventually; - qi::rule>(), Skipper> next; - qi::rule>(), Skipper> globally; - qi::rule>(), qi::locals< std::shared_ptr>>, Skipper> boundedUntil; - qi::rule>(), qi::locals< std::shared_ptr>>, Skipper> until; - - qi::rule>(), Skipper> rewardPathFormula; - qi::rule>(), Skipper> cumulativeReward; - qi::rule>(), Skipper> reachabilityReward; - qi::rule>(), Skipper> instantaneousReward; - qi::rule>(), Skipper> steadyStateReward; - - - qi::rule freeIdentifierName; - qi::rule comparisonType; - qi::rule::SortingCategory(), Skipper> sortingCategory; -}; - -std::shared_ptr> PrctlParser::parsePrctlFormula(std::string formulaString) { - // Prepare iterators to input. - BaseIteratorType stringIteratorBegin = formulaString.begin(); - BaseIteratorType stringIteratorEnd = formulaString.end(); - PositionIteratorType positionIteratorBegin(stringIteratorBegin, stringIteratorEnd, formulaString); - PositionIteratorType positionIteratorEnd; - - - // Prepare resulting intermediate representation of input. - std::shared_ptr> result_pointer(nullptr); - - PrctlGrammar grammar; - - // Now, parse the formula from the given string - try { - qi::phrase_parse(positionIteratorBegin, positionIteratorEnd, grammar, boost::spirit::ascii::space, result_pointer); - } catch(const qi::expectation_failure& e) { - // If the parser expected content different than the one provided, display information - // about the location of the error. - const boost::spirit::classic::file_position_base& pos = e.first.get_position(); - - // Construct the error message including a caret display of the position in the - // erroneous line. - std::stringstream msg; - msg << pos.file << ", line " << pos.line << ", column " << pos.column - << ": parse error: expected " << e.what_ << std::endl << "\t" - << e.first.get_currentline() << std::endl << "\t"; - int i = 0; - for (i = 0; i < pos.column; ++i) { - msg << "-"; - } - msg << "^"; - for (; i < 80; ++i) { - msg << "-"; - } - msg << std::endl; - - std::cerr << msg.str(); - - // Now propagate exception. - throw storm::exceptions::WrongFormatException() << msg.str(); - } - - // The syntax can be so wrong that no rule can be matched at all - // In that case, no expectation failure is thrown, but the parser just returns nullptr - // Then, of course the result is not usable, hence we throw a WrongFormatException, too. - if (!result_pointer) { - throw storm::exceptions::WrongFormatException() << "Syntax error in formula"; - } - - return result_pointer; -} - -} //namespace parser -} //namespace storm diff --git a/src/parser/PrctlParser.h b/src/parser/PrctlParser.h deleted file mode 100644 index c1fc798bb..000000000 --- a/src/parser/PrctlParser.h +++ /dev/null @@ -1,43 +0,0 @@ -#ifndef STORM_PARSER_PRCTLPARSER_H_ -#define STORM_PARSER_PRCTLPARSER_H_ - -#include "src/properties/Prctl.h" -#include "src/properties/prctl/PrctlFilter.h" - -namespace storm { -namespace parser { - -/*! - * Reads a PRCTL formula from a string and return the formula tree. - * - * If you want to read the formula from a file, use the PrctlFileParser class instead. - */ -class PrctlParser { -public: - - /*! - * Reads a Prctl formula from its string representation and parses it into a formula tree, consisting of - * classes in the namespace storm::properties. - * - * If the string could not be parsed successfully, it will throw a wrongFormatException. - * - * @param formulaString The string representation of the formula - * @throw wrongFormatException If the input could not be parsed successfully - * @return A PrctlFilter maintaining the parsed formula. If the line just contained a comment a nullptr will be returned instead. - */ - static std::shared_ptr> parsePrctlFormula(std::string formulaString); - -private: - - /*! - * Struct for the Prctl grammar, that Boost::Spirit uses to parse the formulas. - */ - template - struct PrctlGrammar; - -}; - -} // namespace parser -} // namespace storm - -#endif /* STORM_PARSER_PRCTLPARSER_H_ */ diff --git a/src/parser/PrismParser.h b/src/parser/PrismParser.h index 539c9bc48..ab501c43c 100644 --- a/src/parser/PrismParser.h +++ b/src/parser/PrismParser.h @@ -91,12 +91,13 @@ namespace storm { ("rewards", 11) ("endrewards", 12) ("true", 13) - ("min", 14) - ("max", 15) - ("floor", 16) - ("ceil", 17) - ("init", 18) - ("endinit", 19); + ("false", 14) + ("min", 15) + ("max", 16) + ("floor", 17) + ("ceil", 18) + ("init", 19) + ("endinit", 20); } }; diff --git a/src/properties/logic/Formulas.h b/src/properties/logic/Formulas.h deleted file mode 100644 index 141769ecb..000000000 --- a/src/properties/logic/Formulas.h +++ /dev/null @@ -1,33 +0,0 @@ -#include "src/properties/logic/Formula.h" -#include "src/properties/logic/AtomicExpressionFormula.h" -#include "src/properties/logic/AtomicLabelFormula.h" -#include "src/properties/logic/BinaryBooleanStateFormula.h" -#include "src/properties/logic/BinaryPathFormula.h" -#include "src/properties/logic/BinaryStateFormula.h" -#include "src/properties/logic/BooleanLiteralFormula.h" -#include "src/properties/logic/BoundedUntilFormula.h" -#include "src/properties/logic/CumulativeRewardFormula.h" -#include "src/properties/logic/EventuallyFormula.h" -#include "src/properties/logic/GloballyFormula.h" -#include "src/properties/logic/InstantaneousRewardFormula.h" -#include "src/properties/logic/NextFormula.h" -#include "src/properties/logic/PathFormula.h" -#include "src/properties/logic/ProbabilityOperatorFormula.h" -#include "src/properties/logic/ReachabilityRewardFormula.h" -#include "src/properties/logic/RewardOperatorFormula.h" -#include "src/properties/logic/StateFormula.h" -#include "src/properties/logic/SteadyStateFormula.h" -#include "src/properties/logic/UnaryBooleanStateFormula.h" -#include "src/properties/logic/UnaryPathFormula.h" -#include "src/properties/logic/UnaryStateFormula.h" -#include "src/properties/logic/UntilFormula.h" -#include "src/properties/logic/ConditionalPathFormula.h" -#include "src/properties/logic/ProbabilityOperatorFormula.h" -#include "src/properties/logic/RewardOperatorFormula.h" - - - - - - - diff --git a/src/properties/logic/SteadyStateFormula.cpp b/src/properties/logic/SteadyStateFormula.cpp deleted file mode 100644 index 1b7197a10..000000000 --- a/src/properties/logic/SteadyStateFormula.cpp +++ /dev/null @@ -1,35 +0,0 @@ -#include "src/properties/logic/SteadyStateFormula.h" - -namespace storm { - namespace logic { - SteadyStateFormula::SteadyStateFormula(std::shared_ptr const& subformula) : SteadyStateFormula(boost::optional(), boost::optional(), boost::optional(), subformula) { - // Intentionally left empty. - } - - SteadyStateFormula::SteadyStateFormula(ComparisonType comparisonType, double bound, std::shared_ptr const& subformula) : SteadyStateFormula(boost::optional(comparisonType), boost::optional(bound), boost::optional(), subformula) { - // Intentionally left empty. - } - - SteadyStateFormula::SteadyStateFormula(ComparisonType comparisonType, double bound, OptimalityType optimalityType, std::shared_ptr const& subformula) : SteadyStateFormula(boost::optional(comparisonType), boost::optional(bound), boost::optional(optimalityType), subformula) { - // Intentionally left empty. - } - - SteadyStateFormula::SteadyStateFormula(OptimalityType optimalityType, std::shared_ptr const& subformula) : SteadyStateFormula(boost::optional(), boost::optional(), boost::optional(optimalityType), subformula) { - // Intentionally left empty. - } - - bool SteadyStateFormula::isSteadyStateFormula() const { - return true; - } - - SteadyStateFormula::SteadyStateFormula(boost::optional comparisonType, boost::optional bound, boost::optional optimalityType, std::shared_ptr const& subformula) : OperatorFormula(comparisonType, bound, optimalityType, subformula) { - // Intentionally left empty. - } - - std::ostream& SteadyStateFormula::writeToStream(std::ostream& out) const { - out << "S"; - OperatorFormula::writeToStream(out); - return out; - } - } -} \ No newline at end of file diff --git a/src/properties/logic/SteadyStateFormula.h b/src/properties/logic/SteadyStateFormula.h deleted file mode 100644 index 720480a82..000000000 --- a/src/properties/logic/SteadyStateFormula.h +++ /dev/null @@ -1,29 +0,0 @@ -#ifndef STORM_LOGIC_STEADYSTATEFORMULA_H_ -#define STORM_LOGIC_STEADYSTATEFORMULA_H_ - -#include "src/properties/logic/OperatorFormula.h" - -namespace storm { - namespace logic { - class SteadyStateFormula : public OperatorFormula { - public: - SteadyStateFormula(std::shared_ptr const& subformula); - SteadyStateFormula(ComparisonType comparisonType, double bound, std::shared_ptr const& subformula); - SteadyStateFormula(ComparisonType comparisonType, double bound, OptimalityType optimalityType, std::shared_ptr const& subformula); - SteadyStateFormula(OptimalityType optimalityType, std::shared_ptr const& subformula); - - virtual ~SteadyStateFormula() { - // Intentionally left empty. - } - - virtual bool isSteadyStateFormula() const override; - - virtual std::ostream& writeToStream(std::ostream& out) const override; - - private: - SteadyStateFormula(boost::optional comparisonType, boost::optional bound, boost::optional optimalityType, std::shared_ptr const& subformula); - }; - } -} - -#endif /* STORM_LOGIC_STEADYSTATEFORMULA_H_ */ \ No newline at end of file diff --git a/test/functional/modelchecker/ActionTest.cpp b/test/functional/modelchecker/ActionTest.cpp deleted file mode 100644 index 75fa37106..000000000 --- a/test/functional/modelchecker/ActionTest.cpp +++ /dev/null @@ -1,573 +0,0 @@ -/* - * ActionTest.cpp - * - * Created on: Jun 27, 2014 - * Author: Manuel Sascha Weiand - */ - -#include "gtest/gtest.h" -#include "storm-config.h" - -#include "src/properties/actions/BoundAction.h" -#include "src/properties/actions/FormulaAction.h" -#include "src/properties/actions/InvertAction.h" -#include "src/properties/actions/RangeAction.h" -#include "src/properties/actions/SortAction.h" - -#include "src/parser/MarkovAutomatonParser.h" -#include "src/parser/DeterministicModelParser.h" -#include "src/modelchecker/prctl/SparseDtmcPrctlModelChecker.h" -#include "src/modelchecker/csl/SparseMarkovAutomatonCslModelChecker.h" -#include "src/solver/GmmxxLinearEquationSolver.h" -#include "src/exceptions/InvalidArgumentException.h" - -typedef storm::properties::action::AbstractAction::Result Result; - -TEST(ActionTest, BoundActionFunctionality) { - - // Setup the modelchecker. - storm::models::Dtmc model = storm::parser::DeterministicModelParser::parseDtmc(STORM_CPP_TESTS_BASE_PATH "/functional/parser/tra_files/dtmc_actionTest.tra", STORM_CPP_TESTS_BASE_PATH "/functional/parser/lab_files/dtmc_actionTest.lab"); - storm::modelchecker::prctl::SparseDtmcPrctlModelChecker mc(model, std::unique_ptr>(new storm::solver::GmmxxLinearEquationSolver())); - - // Build the filter input. - // Basically the modelchecking result of "F a" on the used DTMC. - std::vector pathResult = mc.checkEventually(storm::properties::prctl::Eventually(std::make_shared>("a")), false); - std::vector stateMap(pathResult.size()); - for(uint_fast64_t i = 0; i < pathResult.size(); i++) { - stateMap[i] = i; - } - Result input(storm::storage::BitVector(pathResult.size(), true), stateMap, pathResult, storm::storage::BitVector()); - - // Test the action. - // First test that the boundAction build by the empty constructor does not change the selection. - storm::properties::action::BoundAction action; - Result result = action.evaluate(input, mc); - - for(auto value : result.selection) { - ASSERT_TRUE(input.selection[value]); - } - - // Test that using a strict bound can give different results than using a non-strict bound. - action = storm::properties::action::BoundAction(storm::properties::GREATER, 0); - result = action.evaluate(input, mc); - - for(uint_fast64_t i = 0; i < result.selection.size()-2; i++) { - ASSERT_TRUE(result.selection[i]); - } - ASSERT_FALSE(result.selection[6]); - ASSERT_FALSE(result.selection[7]); - - // Test whether the filter actually uses the selection given by the input. - action = storm::properties::action::BoundAction(storm::properties::LESS, 0.5); - result = action.evaluate(result, mc); - - ASSERT_FALSE(result.selection[0]); - ASSERT_TRUE(result.selection[1]); - ASSERT_FALSE(result.selection[6]); - ASSERT_FALSE(result.selection[7]); - - // Check whether the state order has any effect on the selected states, which it should not. - for(uint_fast64_t i = 0; i < pathResult.size(); i++) { - stateMap[i] = pathResult.size() - i - 1; - } - - action = storm::properties::action::BoundAction(storm::properties::GREATER, 0); - result = action.evaluate(input, mc); - - for(uint_fast64_t i = 0; i < result.selection.size()-2; i++) { - ASSERT_TRUE(result.selection[i]); - } - ASSERT_FALSE(result.selection[6]); - ASSERT_FALSE(result.selection[7]); - - // Test the functionality for state formulas instead. - input.pathResult = std::vector(); - input.stateResult = mc.checkAp(storm::properties::prctl::Ap("a")); - action = storm::properties::action::BoundAction(storm::properties::GREATER, 0.5); - result = action.evaluate(input, mc); - - for(uint_fast64_t i = 0; i < result.selection.size(); i++) { - if(i == 5) { - ASSERT_TRUE(result.selection[i]); - } else { - ASSERT_FALSE(result.selection[i]); - } - } - - // Make sure that the modelchecker has no influence on the result. - storm::models::MarkovAutomaton ma = storm::parser::MarkovAutomatonParser::parseMarkovAutomaton(STORM_CPP_TESTS_BASE_PATH "/functional/parser/tra_files/ma_general.tra", STORM_CPP_TESTS_BASE_PATH "/functional/parser/lab_files/ma_general.lab"); - storm::modelchecker::csl::SparseMarkovAutomatonCslModelChecker cslMc(ma); - result = action.evaluate(input, cslMc); - - for(uint_fast64_t i = 0; i < result.selection.size(); i++) { - if(i == 5) { - ASSERT_TRUE(result.selection[i]); - } else { - ASSERT_FALSE(result.selection[i]); - } - } -} - -TEST(ActionTest, BoundActionSafety) { - - // Setup the modelchecker. - storm::models::Dtmc model = storm::parser::DeterministicModelParser::parseDtmc(STORM_CPP_TESTS_BASE_PATH "/functional/parser/tra_files/dtmc_actionTest.tra", STORM_CPP_TESTS_BASE_PATH "/functional/parser/lab_files/dtmc_actionTest.lab"); - storm::modelchecker::prctl::SparseDtmcPrctlModelChecker mc(model, std::unique_ptr>(new storm::solver::GmmxxLinearEquationSolver())); - - // Build the filter input. - // Basically the modelchecking result of "F a" on the used DTMC. - std::vector pathResult = mc.checkEventually(storm::properties::prctl::Eventually(std::make_shared>("a")), false); - storm::storage::BitVector stateResult = mc.checkAp(storm::properties::prctl::Ap("a")); - std::vector stateMap(pathResult.size()); - for(uint_fast64_t i = 0; i < pathResult.size(); i++) { - stateMap[i] = i; - } - Result input(storm::storage::BitVector(pathResult.size(), true), stateMap, pathResult, storm::storage::BitVector()); - - // First, test unusual bounds. - storm::properties::action::BoundAction action(storm::properties::LESS, -2044); - Result result; - - ASSERT_NO_THROW(result = action.evaluate(input, mc)); - ASSERT_EQ(0, result.selection.getNumberOfSetBits()); - - action = storm::properties::action::BoundAction(storm::properties::GREATER_EQUAL, 5879); - - ASSERT_NO_THROW(result = action.evaluate(input, mc)); - ASSERT_EQ(0, result.selection.getNumberOfSetBits()); - - action = storm::properties::action::BoundAction(storm::properties::LESS_EQUAL, 5879); - - ASSERT_NO_THROW(result = action.evaluate(input, mc)); - ASSERT_EQ(result.selection.size(), result.selection.getNumberOfSetBits()); - - // Now, check the behavior under a undefined comparison type. - action = storm::properties::action::BoundAction(static_cast(10), 5879); - ASSERT_THROW(action.toString(), storm::exceptions::InvalidArgumentException); - ASSERT_THROW(action.evaluate(input, mc), storm::exceptions::InvalidArgumentException); - - // Test for a result input with both results filled. - // It should put out a warning and use the pathResult. - action = storm::properties::action::BoundAction(storm::properties::GREATER_EQUAL, 0.5); - input.stateResult = stateResult; - - // To capture the warning, redirect cout and test the written buffer content. - std::stringstream buffer; - std::streambuf *sbuf = std::cout.rdbuf(); - std::cout.rdbuf(buffer.rdbuf()); - - ASSERT_NO_THROW(result = action.evaluate(input, mc)); - std::cout.rdbuf(sbuf); - - ASSERT_FALSE(buffer.str().empty()); - ASSERT_TRUE(result.selection[0]); - ASSERT_FALSE(result.selection[1]); - ASSERT_TRUE(result.selection[2]); - ASSERT_TRUE(result.selection[5]); - - // Check for empty input. - ASSERT_NO_THROW(result = action.evaluate(Result(), mc)); -} - -TEST(ActionTest, FormulaActionFunctionality) { - - // Setup the modelchecker. - storm::models::Dtmc model = storm::parser::DeterministicModelParser::parseDtmc(STORM_CPP_TESTS_BASE_PATH "/functional/parser/tra_files/dtmc_actionTest.tra", STORM_CPP_TESTS_BASE_PATH "/functional/parser/lab_files/dtmc_actionTest.lab"); - storm::modelchecker::prctl::SparseDtmcPrctlModelChecker mc(model, std::unique_ptr>(new storm::solver::GmmxxLinearEquationSolver())); - - // Build the filter input. - // Basically the modelchecking result of "F a" on the used DTMC. - std::vector pathResult = mc.checkEventually(storm::properties::prctl::Eventually(std::make_shared>("a")), false); - storm::storage::BitVector stateResult = mc.checkAp(storm::properties::prctl::Ap("c")); - std::vector stateMap(pathResult.size()); - for(uint_fast64_t i = 0; i < pathResult.size(); i++) { - stateMap[i] = i; - } - Result input(storm::storage::BitVector(pathResult.size(), true), stateMap, pathResult, storm::storage::BitVector()); - Result result; - - // Test the action. - // First test that the empty action does no change to the input. - storm::properties::action::FormulaAction action; - input.selection.set(0,false); - ASSERT_NO_THROW(result = action.evaluate(input, mc)); - for(uint_fast64_t i = 0; i < pathResult.size(); i++) { - if(i != 0) { - ASSERT_TRUE(result.selection[i]); - } else { - ASSERT_FALSE(result.selection[i]); - } - ASSERT_EQ(i, result.stateMap[i]); - ASSERT_EQ(input.pathResult[i], result.pathResult[i]); - } - ASSERT_TRUE(result.stateResult.size() == 0); - input.selection.set(0,true); - - // Now test the general functionality. - action = storm::properties::action::FormulaAction(std::make_shared>(storm::properties::LESS, 0.5, std::make_shared>(std::make_shared>("b")))); - ASSERT_NO_THROW(result = action.evaluate(input, mc)); - ASSERT_TRUE(result.selection[0]); - ASSERT_TRUE(result.selection[1]); - ASSERT_TRUE(result.selection[2]); - ASSERT_FALSE(result.selection[3]); - ASSERT_FALSE(result.selection[4]); - ASSERT_TRUE(result.selection[5]); - ASSERT_FALSE(result.selection[6]); - ASSERT_FALSE(result.selection[7]); - - // Check that the actual modelchecking results are not touched. - ASSERT_EQ(input.stateResult.size(), result.stateResult.size()); - ASSERT_EQ(input.pathResult.size(), result.pathResult.size()); - for(uint_fast64_t i = 0; i < input.pathResult.size(); i++) { - ASSERT_EQ(input.pathResult[i], result.pathResult[i]); - } - - // Do the same but this time using a state result instead of a path result. - input.pathResult = std::vector(); - input.stateResult = stateResult; - ASSERT_NO_THROW(result = action.evaluate(input, mc)); - ASSERT_TRUE(result.selection[0]); - ASSERT_TRUE(result.selection[1]); - ASSERT_TRUE(result.selection[2]); - ASSERT_FALSE(result.selection[3]); - ASSERT_FALSE(result.selection[4]); - ASSERT_TRUE(result.selection[5]); - ASSERT_FALSE(result.selection[6]); - ASSERT_FALSE(result.selection[7]); - - ASSERT_EQ(input.stateResult.size(), result.stateResult.size()); - ASSERT_EQ(input.pathResult.size(), result.pathResult.size()); - for(uint_fast64_t i = 0; i < input.stateResult.size(); i++) { - ASSERT_EQ(input.stateResult[i], result.stateResult[i]); - } -} - -TEST(ActionTest, FormulaActionSafety){ - // Setup the modelchecker. - storm::models::Dtmc model = storm::parser::DeterministicModelParser::parseDtmc(STORM_CPP_TESTS_BASE_PATH "/functional/parser/tra_files/dtmc_actionTest.tra", STORM_CPP_TESTS_BASE_PATH "/functional/parser/lab_files/dtmc_actionTest.lab"); - storm::modelchecker::prctl::SparseDtmcPrctlModelChecker mc(model, std::unique_ptr>(new storm::solver::GmmxxLinearEquationSolver())); - - // Build the filter input. - // Basically the modelchecking result of "F a" on the used DTMC. - std::vector pathResult = mc.checkEventually(storm::properties::prctl::Eventually(std::make_shared>("a")), false); - std::vector stateMap(pathResult.size()); - for(uint_fast64_t i = 0; i < pathResult.size(); i++) { - stateMap[i] = i; - } - Result input(storm::storage::BitVector(pathResult.size(), true), stateMap, pathResult, storm::storage::BitVector()); - Result result; - - // Check that constructing the action using a nullptr and using an empty constructor leads to the same behavior. - storm::properties::action::FormulaAction action(std::shared_ptr>(nullptr)); - input.selection.set(0,false); - ASSERT_NO_THROW(result = action.evaluate(input, mc)); - for(uint_fast64_t i = 0; i < pathResult.size(); i++) { - if(i != 0) { - ASSERT_TRUE(result.selection[i]); - } else { - ASSERT_FALSE(result.selection[i]); - } - ASSERT_EQ(i, result.stateMap[i]); - ASSERT_EQ(input.pathResult[i], result.pathResult[i]); - } - ASSERT_TRUE(result.stateResult.size() == 0); - input.selection.set(0,true); - ASSERT_NO_THROW(action.toString()); -} - -TEST(ActionTest, InvertActionFunctionality){ - // Setup the modelchecker. - storm::models::Dtmc model = storm::parser::DeterministicModelParser::parseDtmc(STORM_CPP_TESTS_BASE_PATH "/functional/parser/tra_files/dtmc_actionTest.tra", STORM_CPP_TESTS_BASE_PATH "/functional/parser/lab_files/dtmc_actionTest.lab"); - storm::modelchecker::prctl::SparseDtmcPrctlModelChecker mc(model, std::unique_ptr>(new storm::solver::GmmxxLinearEquationSolver())); - - // Build the filter input. - // Basically the modelchecking result of "F a" on the used DTMC. - std::vector pathResult = mc.checkEventually(storm::properties::prctl::Eventually(std::make_shared>("a")), false); - storm::storage::BitVector stateResult = mc.checkAp(storm::properties::prctl::Ap("c")); - std::vector stateMap(pathResult.size()); - for(uint_fast64_t i = 0; i < pathResult.size(); i++) { - stateMap[i] = pathResult.size()-i-1; - } - Result input(storm::storage::BitVector(pathResult.size(), true), stateMap, pathResult, storm::storage::BitVector()); - Result result; - - // Check whether the selection becomes inverted while the rest stays the same. - storm::properties::action::InvertAction action; - input.selection.set(0,false); - ASSERT_NO_THROW(result = action.evaluate(input, mc)); - for(uint_fast64_t i = 0; i < pathResult.size(); i++) { - if(i != 0) { - ASSERT_FALSE(result.selection[i]); - } else { - ASSERT_TRUE(result.selection[i]); - } - ASSERT_EQ(pathResult.size()-i-1, result.stateMap[i]); - ASSERT_EQ(input.pathResult[i], result.pathResult[i]); - } - ASSERT_TRUE(result.stateResult.size() == 0); - input.selection.set(0,true); - ASSERT_NO_THROW(action.toString()); -} - -TEST(ActionTest, RangeActionFunctionality){ - // Setup the modelchecker. - storm::models::Dtmc model = storm::parser::DeterministicModelParser::parseDtmc(STORM_CPP_TESTS_BASE_PATH "/functional/parser/tra_files/dtmc_actionTest.tra", STORM_CPP_TESTS_BASE_PATH "/functional/parser/lab_files/dtmc_actionTest.lab"); - storm::modelchecker::prctl::SparseDtmcPrctlModelChecker mc(model, std::unique_ptr>(new storm::solver::GmmxxLinearEquationSolver())); - - // Build the filter input. - // Basically the modelchecking result of "F a" on the used DTMC. - std::vector pathResult = mc.checkEventually(storm::properties::prctl::Eventually(std::make_shared>("a")), false); - storm::storage::BitVector stateResult = mc.checkAp(storm::properties::prctl::Ap("c")); - std::vector stateMap(pathResult.size()); - for(uint_fast64_t i = 0; i < pathResult.size(); i++) { - stateMap[i] = i; - } - Result input(storm::storage::BitVector(pathResult.size(), true), stateMap, pathResult, storm::storage::BitVector()); - Result result; - - // Test if the action selects the first 3 states in relation to the order given by the stateMap. - // First in index order. - storm::properties::action::RangeAction action(0,2); - ASSERT_NO_THROW(result = action.evaluate(input, mc)); - for(uint_fast64_t i = 0; i < result.selection.size(); i++) { - ASSERT_EQ(input.stateMap[i], result.stateMap[i]); - } - for(uint_fast64_t i = 0; i < 3; i++) { - ASSERT_TRUE(result.selection[i]); - } - for(uint_fast64_t i = 3; i < result.selection.size(); i++) { - ASSERT_FALSE(result.selection[i]); - } - input.selection.clear(); - input.selection.complement(); - - // Now against index order. - for(uint_fast64_t i = 0; i < input.pathResult.size(); i++) { - input.stateMap[i] = input.pathResult.size()-i-1; - } - ASSERT_NO_THROW(result = action.evaluate(input, mc)); - for(uint_fast64_t i = 0; i < result.selection.size(); i++) { - ASSERT_EQ(input.stateMap[i], result.stateMap[i]); - } - for(uint_fast64_t i = 0; i < 3; i++) { - ASSERT_TRUE(result.selection[result.selection.size()-i-1]); - } - for(uint_fast64_t i = 3; i < result.selection.size(); i++) { - ASSERT_FALSE(result.selection[result.selection.size()-i-1]); - } - input.selection.clear(); - input.selection.complement(); - - // Finally test a random order. - std::srand(time(nullptr)); - uint_fast64_t pos1, pos2, temp; - for(uint_fast64_t i = 0; i < 100; i++) { - // Randomly select two positions. - pos1 = rand() % result.selection.size(); - pos2 = rand() % result.selection.size(); - - // Swap the values there. - temp = input.stateMap[pos1]; - input.stateMap[pos1] = input.stateMap[pos2]; - input.stateMap[pos2] = temp; - } - ASSERT_NO_THROW(result = action.evaluate(input, mc)); - for(uint_fast64_t i = 0; i < 8; i++) { - ASSERT_EQ(input.stateMap[i], result.stateMap[i]); - } - for(uint_fast64_t i = 0; i < 3; i++) { - ASSERT_TRUE(result.selection[result.stateMap[i]]); - } - for(uint_fast64_t i = 3; i < result.selection.size(); i++) { - ASSERT_FALSE(result.selection[result.stateMap[i]]); - } - - // Test that specifying and interval of (i,i) selects only state i. - for(uint_fast64_t i = 0; i < input.selection.size(); i++) { - action = storm::properties::action::RangeAction(i,i); - ASSERT_NO_THROW(result = action.evaluate(input, mc)); - ASSERT_EQ(1, result.selection.getNumberOfSetBits()); - ASSERT_TRUE(result.selection[result.stateMap[i]]); - } -} - -TEST(ActionTest, RangeActionSafety){ - // Setup the modelchecker. - storm::models::Dtmc model = storm::parser::DeterministicModelParser::parseDtmc(STORM_CPP_TESTS_BASE_PATH "/functional/parser/tra_files/dtmc_actionTest.tra", STORM_CPP_TESTS_BASE_PATH "/functional/parser/lab_files/dtmc_actionTest.lab"); - storm::modelchecker::prctl::SparseDtmcPrctlModelChecker mc(model, std::unique_ptr>(new storm::solver::GmmxxLinearEquationSolver())); - - // Build the filter input. - // Basically the modelchecking result of "F a" on the used DTMC. - std::vector pathResult = mc.checkEventually(storm::properties::prctl::Eventually(std::make_shared>("a")), false); - storm::storage::BitVector stateResult = mc.checkAp(storm::properties::prctl::Ap("c")); - std::vector stateMap(pathResult.size()); - for(uint_fast64_t i = 0; i < pathResult.size(); i++) { - stateMap[i] = i; - } - Result input(storm::storage::BitVector(pathResult.size(), true), stateMap, pathResult, storm::storage::BitVector()); - Result result; - - // Test invalid ranges. - - // To capture the warning, redirect cout and test the written buffer content. - std::stringstream buffer; - std::streambuf * sbuf = std::cout.rdbuf(); - std::cout.rdbuf(buffer.rdbuf()); - - storm::properties::action::RangeAction action(0,42); - ASSERT_NO_THROW(result = action.evaluate(input, mc)); - ASSERT_TRUE(result.selection.full()); - - ASSERT_FALSE(buffer.str().empty()); - buffer.str(""); - - action = storm::properties::action::RangeAction(42,98); - ASSERT_NO_THROW(result = action.evaluate(input, mc)); - ASSERT_TRUE(result.selection.empty()); - - ASSERT_FALSE(buffer.str().empty()); - std::cout.rdbuf(sbuf); - - ASSERT_THROW(storm::properties::action::RangeAction(3,1), storm::exceptions::IllegalArgumentValueException); -} - -TEST(ActionTest, SortActionFunctionality){ - // Setup the modelchecker. - storm::models::Dtmc model = storm::parser::DeterministicModelParser::parseDtmc(STORM_CPP_TESTS_BASE_PATH "/functional/parser/tra_files/dtmc_actionTest.tra", STORM_CPP_TESTS_BASE_PATH "/functional/parser/lab_files/dtmc_actionTest.lab"); - storm::modelchecker::prctl::SparseDtmcPrctlModelChecker mc(model, std::unique_ptr>(new storm::solver::GmmxxLinearEquationSolver())); - - // Build the filter input. - // Basically the modelchecking result of "F a" on the used DTMC. - std::vector pathResult = mc.checkEventually(storm::properties::prctl::Eventually(std::make_shared>("a")), false); - storm::storage::BitVector stateResult = mc.checkAp(storm::properties::prctl::Ap("c")); - std::vector stateMap(pathResult.size()); - for(uint_fast64_t i = 0; i < pathResult.size(); i++) { - stateMap[i] = pathResult.size()-i-1; - } - Result input(storm::storage::BitVector(pathResult.size(), true), stateMap, pathResult, storm::storage::BitVector()); - Result result; - - // Test that sorting preserves everything except the state map. - storm::properties::action::SortAction action; - ASSERT_NO_THROW(action.toString()); - input.selection.set(0,false); - ASSERT_NO_THROW(result = action.evaluate(input, mc)); - for(uint_fast64_t i = 0; i < pathResult.size(); i++) { - if(i != 0) { - ASSERT_TRUE(result.selection[i]); - } else { - ASSERT_FALSE(result.selection[i]); - } - ASSERT_EQ(i, result.stateMap[i]); - ASSERT_EQ(input.pathResult[i], result.pathResult[i]); - } - ASSERT_TRUE(result.stateResult.size() == 0); - input.selection.set(0,true); - - // Test sorting cases. Note that the input selection should be irrelevant for the resulting state order. - // 1) index, ascending -> see above - // 2) index descending - input.selection.set(3,false); - action = storm::properties::action::SortAction(storm::properties::action::SortAction::INDEX, false); - ASSERT_NO_THROW(result = action.evaluate(input, mc)); - for(uint_fast64_t i = 0; i < pathResult.size(); i++) { - ASSERT_EQ(pathResult.size()-i-1, result.stateMap[i]); - } - - // 3) value, ascending - action = storm::properties::action::SortAction(storm::properties::action::SortAction::VALUE); - ASSERT_NO_THROW(result = action.evaluate(input, mc)); - ASSERT_EQ(6, result.stateMap[0]); - ASSERT_EQ(7, result.stateMap[1]); - ASSERT_EQ(3, result.stateMap[2]); - ASSERT_EQ(4, result.stateMap[3]); - ASSERT_EQ(1, result.stateMap[4]); - ASSERT_EQ(0, result.stateMap[5]); - ASSERT_EQ(2, result.stateMap[6]); - ASSERT_EQ(5, result.stateMap[7]); - - // 3) value, decending - action = storm::properties::action::SortAction(storm::properties::action::SortAction::VALUE, false); - ASSERT_NO_THROW(result = action.evaluate(input, mc)); - ASSERT_EQ(5, result.stateMap[0]); - ASSERT_EQ(2, result.stateMap[1]); - ASSERT_EQ(0, result.stateMap[2]); - ASSERT_EQ(1, result.stateMap[3]); - ASSERT_EQ(4, result.stateMap[4]); - ASSERT_EQ(3, result.stateMap[5]); - ASSERT_EQ(6, result.stateMap[6]); - ASSERT_EQ(7, result.stateMap[7]); - - // Check that this also works for state results instead. - input.pathResult = std::vector(); - input.stateResult = stateResult; - - action = storm::properties::action::SortAction(storm::properties::action::SortAction::VALUE); - ASSERT_NO_THROW(result = action.evaluate(input, mc)); - ASSERT_EQ(5, result.stateMap[0]); - ASSERT_EQ(6, result.stateMap[1]); - ASSERT_EQ(7, result.stateMap[2]); - ASSERT_EQ(0, result.stateMap[3]); - ASSERT_EQ(1, result.stateMap[4]); - ASSERT_EQ(2, result.stateMap[5]); - ASSERT_EQ(3, result.stateMap[6]); - ASSERT_EQ(4, result.stateMap[7]); - - action = storm::properties::action::SortAction(storm::properties::action::SortAction::VALUE, false); - ASSERT_NO_THROW(result = action.evaluate(input, mc)); - ASSERT_EQ(0, result.stateMap[0]); - ASSERT_EQ(1, result.stateMap[1]); - ASSERT_EQ(2, result.stateMap[2]); - ASSERT_EQ(3, result.stateMap[3]); - ASSERT_EQ(4, result.stateMap[4]); - ASSERT_EQ(5, result.stateMap[5]); - ASSERT_EQ(6, result.stateMap[6]); - ASSERT_EQ(7, result.stateMap[7]); - - // Test if the resulting order does not depend on the input order. - input.stateResult = storm::storage::BitVector(); - input.pathResult = pathResult; - - action = storm::properties::action::SortAction(storm::properties::action::SortAction::INDEX); - ASSERT_NO_THROW(input = action.evaluate(input, mc)); - action = storm::properties::action::SortAction(storm::properties::action::SortAction::VALUE); - ASSERT_NO_THROW(result = action.evaluate(input, mc)); - ASSERT_EQ(6, result.stateMap[0]); - ASSERT_EQ(7, result.stateMap[1]); - ASSERT_EQ(3, result.stateMap[2]); - ASSERT_EQ(4, result.stateMap[3]); - ASSERT_EQ(1, result.stateMap[4]); - ASSERT_EQ(0, result.stateMap[5]); - ASSERT_EQ(2, result.stateMap[6]); - ASSERT_EQ(5, result.stateMap[7]); - -} - -TEST(ActionTest, SortActionSafety){ - // Check that the path result has priority over the state result if for some erronous reason both are given. - // Setup the modelchecker. - storm::models::Dtmc model = storm::parser::DeterministicModelParser::parseDtmc(STORM_CPP_TESTS_BASE_PATH "/functional/parser/tra_files/dtmc_actionTest.tra", STORM_CPP_TESTS_BASE_PATH "/functional/parser/lab_files/dtmc_actionTest.lab"); - storm::modelchecker::prctl::SparseDtmcPrctlModelChecker mc(model, std::unique_ptr>(new storm::solver::GmmxxLinearEquationSolver())); - - // Build the filter input. - // Basically the modelchecking result of "F a" on the used DTMC. - std::vector pathResult = mc.checkEventually(storm::properties::prctl::Eventually(std::make_shared>("a")), false); - storm::storage::BitVector stateResult = mc.checkAp(storm::properties::prctl::Ap("c")); - std::vector stateMap(pathResult.size()); - for(uint_fast64_t i = 0; i < pathResult.size(); i++) { - stateMap[i] = pathResult.size()-i-1; - } - Result input(storm::storage::BitVector(pathResult.size(), true), stateMap, pathResult, stateResult); - Result result; - - storm::properties::action::SortAction action(storm::properties::action::SortAction::VALUE); - ASSERT_NO_THROW(result = action.evaluate(input, mc)); - ASSERT_EQ(6, result.stateMap[0]); - ASSERT_EQ(7, result.stateMap[1]); - ASSERT_EQ(3, result.stateMap[2]); - ASSERT_EQ(4, result.stateMap[3]); - ASSERT_EQ(1, result.stateMap[4]); - ASSERT_EQ(0, result.stateMap[5]); - ASSERT_EQ(2, result.stateMap[6]); - ASSERT_EQ(5, result.stateMap[7]); -} diff --git a/test/functional/modelchecker/FilterTest.cpp b/test/functional/modelchecker/FilterTest.cpp deleted file mode 100644 index 3d460cbd3..000000000 --- a/test/functional/modelchecker/FilterTest.cpp +++ /dev/null @@ -1,360 +0,0 @@ -/* - * FilterTest.cpp - * - * Created on: Aug 6, 2014 - * Author: Manuel Sascha Weiand - */ - -#include "gtest/gtest.h" -#include "storm-config.h" -#include "src/models/Dtmc.h" -#include "src/parser/DeterministicModelParser.h" -#include "src/modelchecker/prctl/SparseDtmcPrctlModelChecker.h" -#include "src/modelchecker/csl/SparseMarkovAutomatonCslModelChecker.h" -#include "src/solver/GmmxxLinearEquationSolver.h" -#include "src/solver/GmmxxNondeterministicLinearEquationSolver.h" -#include "src/properties/prctl/PrctlFilter.h" -#include "src/properties/csl/CslFilter.h" -#include "src/properties/ltl/LtlFilter.h" -#include "src/parser/PrctlParser.h" -#include "src/parser/CslParser.h" -#include "src/parser/MarkovAutomatonParser.h" -#include "src/properties/actions/InvertAction.h" - -#include - -typedef storm::properties::action::AbstractAction::Result Result; - -TEST(PrctlFilterTest, generalFunctionality) { - // Test filter queries of increasing complexity. - - // Setup model and modelchecker. - storm::models::Dtmc model = storm::parser::DeterministicModelParser::parseDtmc(STORM_CPP_TESTS_BASE_PATH "/functional/parser/tra_files/dtmc_actionTest.tra", STORM_CPP_TESTS_BASE_PATH "/functional/parser/lab_files/dtmc_actionTest.lab"); - storm::modelchecker::prctl::SparseDtmcPrctlModelChecker mc(model, std::unique_ptr>(new storm::solver::GmmxxLinearEquationSolver())); - - // Find the best valued state to finally reach a 'b' state. - std::string input = "filter[sort(value, descending); range(0,0)](F b)"; - std::shared_ptr> formula(nullptr); - ASSERT_NO_THROW( - formula = storm::parser::PrctlParser::parsePrctlFormula(input) - ); - - // Here we test if the check method gives the correct result. - // To capture the output, redirect cout and test the written buffer content. - std::stringstream buffer; - std::streambuf *sbuf = std::cout.rdbuf(); - std::cout.rdbuf(buffer.rdbuf()); - - formula->check(mc); - - // Reset cout to the original buffer. - std::cout.rdbuf(sbuf); - - std::string output = buffer.str(); - ASSERT_NE(std::string::npos, output.find("\t6: 1")); - - // The remaining queries use evaluate directly as its easier to work with in a test environment. - // Get the probability to reach a b state for all states but those that cannot reach a 'b' state or are 'b' states themselves. - // Sorted by value; highest first. - input = "filter[formula(P<=0(F b) | b); invert; sort(value, desc)](F b)"; - ASSERT_NO_THROW( - formula = storm::parser::PrctlParser::parsePrctlFormula(input) - ); - - Result result = formula->evaluate(mc); - - // Test the selection. - ASSERT_EQ(5, result.selection.getNumberOfSetBits()); - ASSERT_TRUE(result.selection[0]); - ASSERT_TRUE(result.selection[1]); - ASSERT_TRUE(result.selection[2]); - ASSERT_TRUE(result.selection[3]); - ASSERT_TRUE(result.selection[4]); - ASSERT_FALSE(result.selection[5]); - ASSERT_FALSE(result.selection[6]); - ASSERT_FALSE(result.selection[7]); - - // Test the sorting. - ASSERT_EQ(6, result.stateMap[0]); - ASSERT_EQ(7, result.stateMap[1]); - ASSERT_EQ(3, result.stateMap[2]); - ASSERT_EQ(4, result.stateMap[3]); - ASSERT_EQ(1, result.stateMap[4]); - ASSERT_EQ(0, result.stateMap[5]); - ASSERT_EQ(2, result.stateMap[6]); - ASSERT_EQ(5, result.stateMap[7]); - - // Get the probability for reaching a 'd' state only for those states that have a probability to do so of at most 0.5. - // Sorted by value; lowest first. - input = "filter[bound(<, 0.5); sort(value, ascending)](F d)"; - ASSERT_NO_THROW( - formula = storm::parser::PrctlParser::parsePrctlFormula(input) - ); - - result = formula->evaluate(mc); - - // Test the selection. - ASSERT_EQ(4, result.selection.getNumberOfSetBits()); - ASSERT_FALSE(result.selection[0]); - ASSERT_FALSE(result.selection[1]); - ASSERT_FALSE(result.selection[2]); - ASSERT_TRUE(result.selection[3]); - ASSERT_FALSE(result.selection[4]); - ASSERT_TRUE(result.selection[5]); - ASSERT_TRUE(result.selection[6]); - ASSERT_TRUE(result.selection[7]); - - // Test the sorting. - ASSERT_EQ(5, result.stateMap[0]); - ASSERT_EQ(6, result.stateMap[1]); - ASSERT_EQ(7, result.stateMap[2]); - ASSERT_EQ(3, result.stateMap[3]); - ASSERT_EQ(4, result.stateMap[4]); - ASSERT_EQ(1, result.stateMap[5]); - ASSERT_EQ(0, result.stateMap[6]); - ASSERT_EQ(2, result.stateMap[7]); - - // Get the three highest indexed states reaching an 'a' state with probability at most 0.3. - input = "filter[sort(value); range(5,7); sort(index, descending)](P<=0.3(F a))"; - ASSERT_NO_THROW( - formula = storm::parser::PrctlParser::parsePrctlFormula(input) - ); - - result = formula->evaluate(mc); - - // Test the selection. - ASSERT_EQ(3, result.selection.getNumberOfSetBits()); - ASSERT_FALSE(result.selection[0]); - ASSERT_FALSE(result.selection[1]); - ASSERT_FALSE(result.selection[2]); - ASSERT_TRUE(result.selection[3]); - ASSERT_FALSE(result.selection[4]); - ASSERT_FALSE(result.selection[5]); - ASSERT_TRUE(result.selection[6]); - ASSERT_TRUE(result.selection[7]); - - // Test the sorting. - ASSERT_EQ(7, result.stateMap[0]); - ASSERT_EQ(6, result.stateMap[1]); - ASSERT_EQ(5, result.stateMap[2]); - ASSERT_EQ(4, result.stateMap[3]); - ASSERT_EQ(3, result.stateMap[4]); - ASSERT_EQ(2, result.stateMap[5]); - ASSERT_EQ(1, result.stateMap[6]); - ASSERT_EQ(0, result.stateMap[7]); - -} - -TEST(PrctlFilterTest, Safety) { - // Setup model and modelchecker. - storm::models::Dtmc model = storm::parser::DeterministicModelParser::parseDtmc(STORM_CPP_TESTS_BASE_PATH "/functional/parser/tra_files/dtmc_actionTest.tra", STORM_CPP_TESTS_BASE_PATH "/functional/parser/lab_files/dtmc_actionTest.lab"); - storm::modelchecker::prctl::SparseDtmcPrctlModelChecker mc(model, std::unique_ptr>(new storm::solver::GmmxxLinearEquationSolver())); - - // Make a stub formula as child. - auto apFormula = std::make_shared>("a"); - - // Test the filter for nullptr action handling. - auto formula = std::make_shared>(apFormula, nullptr); - - ASSERT_EQ(0, formula->getActionCount()); - ASSERT_NO_THROW(formula->evaluate(mc)); - - // Repeat with vector containing only one action but three nullptr. - std::vector>> actions(4, nullptr); - actions[1] = std::make_shared>(); - - formula = std::make_shared>(apFormula, actions); - - ASSERT_EQ(1, formula->getActionCount()); - ASSERT_NO_THROW(formula->evaluate(mc)); - - // Test the filter for nullptr child formula handling. - // It sholud not write anything to the standard out and return an empty result. - formula = std::make_shared>(); - Result result; - - // To capture the output, redirect cout and test the written buffer content. - std::stringstream buffer; - std::streambuf *sbuf = std::cout.rdbuf(); - std::cout.rdbuf(buffer.rdbuf()); - - ASSERT_NO_THROW(result = formula->evaluate(mc)); - - // Reset cout to the original buffer. - std::cout.rdbuf(sbuf); - - ASSERT_EQ(0, buffer.str().length()); - - ASSERT_EQ(0, result.pathResult.size()); - ASSERT_EQ(0, result.stateResult.size()); - ASSERT_EQ(0, result.selection.size()); - ASSERT_EQ(0, result.stateMap.size()); -} - -TEST(CslFilterTest, generalFunctionality) { - // Test filter queries of increasing complexity. - - // Setup model and modelchecker. - storm::models::MarkovAutomaton model = storm::parser::MarkovAutomatonParser::parseMarkovAutomaton(STORM_CPP_TESTS_BASE_PATH "/functional/parser/tra_files/ma_cslFilterTest.tra", STORM_CPP_TESTS_BASE_PATH "/functional/parser/lab_files/ma_cslFilterTest.lab"); - storm::modelchecker::csl::SparseMarkovAutomatonCslModelChecker mc(model, std::make_shared>()); - - // Find the best valued state to finally reach a 'r1' state. - std::string input = "filter[max; sort(value, descending); range(0,0)](F r1)"; - std::shared_ptr> formula(nullptr); - ASSERT_NO_THROW( - formula = storm::parser::CslParser::parseCslFormula(input) - ); - - - // Here we test if the check method gives the correct result. - // To capture the output, redirect cout and test the written buffer content. - std::stringstream buffer; - std::streambuf *sbuf = std::cout.rdbuf(); - std::cout.rdbuf(buffer.rdbuf()); - - formula->check(mc); - - // Reset cout to the original buffer. - std::cout.rdbuf(sbuf); - - std::string output = buffer.str(); - ASSERT_NE(std::string::npos, output.find("\t6: 1")); - - // The remaining queries use evaluate directly as its easier to work with in a test environment. - // Get the maximum probability to reach an 'r1' state for all states but those that cannot reach an 'r1' state or are 'r1' states themselves. - // Sorted by value; highest first. - input = "filter[max; formula(P<=0(F r1) | r1); invert; sort(value, desc)](F r1)"; - ASSERT_NO_THROW( - formula = storm::parser::CslParser::parseCslFormula(input) - ); - - Result result = formula->evaluate(mc); - - // Test the selection. - ASSERT_EQ(6, result.selection.getNumberOfSetBits()); - ASSERT_TRUE(result.selection[0]); - ASSERT_TRUE(result.selection[1]); - ASSERT_TRUE(result.selection[2]); - ASSERT_TRUE(result.selection[3]); - ASSERT_TRUE(result.selection[4]); - ASSERT_TRUE(result.selection[5]); - ASSERT_FALSE(result.selection[6]); - ASSERT_FALSE(result.selection[7]); - - // Test the sorting. - ASSERT_EQ(6, result.stateMap[0]); - ASSERT_EQ(5, result.stateMap[1]); - ASSERT_EQ(2, result.stateMap[2]); - ASSERT_EQ(3, result.stateMap[3]); - ASSERT_EQ(0, result.stateMap[4]); - ASSERT_EQ(4, result.stateMap[5]); - ASSERT_EQ(1, result.stateMap[6]); - ASSERT_EQ(7, result.stateMap[7]); - - // Get the minimum probability for reaching an 'err' state only for those states that have a probability to do so of at most 0.2. - // Sorted by value; lowest first. - input = "filter[min; bound(<, 0.2); sort(value, ascending)](F err)"; - ASSERT_NO_THROW( - formula = storm::parser::CslParser::parseCslFormula(input) - ); - - result = formula->evaluate(mc); - - // Test the selection. - ASSERT_EQ(5, result.selection.getNumberOfSetBits()); - ASSERT_FALSE(result.selection[0]); - ASSERT_TRUE(result.selection[1]); - ASSERT_FALSE(result.selection[2]); - ASSERT_FALSE(result.selection[3]); - ASSERT_TRUE(result.selection[4]); - ASSERT_TRUE(result.selection[5]); - ASSERT_TRUE(result.selection[6]); - ASSERT_TRUE(result.selection[7]); - - // Test the sorting. - ASSERT_EQ(6, result.stateMap[0]); - ASSERT_EQ(7, result.stateMap[1]); - ASSERT_EQ(5, result.stateMap[2]); - ASSERT_EQ(4, result.stateMap[3]); - ASSERT_EQ(1, result.stateMap[4]); - ASSERT_EQ(0, result.stateMap[5]); - ASSERT_EQ(2, result.stateMap[6]); - ASSERT_EQ(3, result.stateMap[7]); - - // Get the three highest indexed states reaching an 'r2' state with probability at most 0.3. - input = "filter[sort(value); range(5,7); sort(index, descending)](P<=0.3(F r2))"; - ASSERT_NO_THROW( - formula = storm::parser::CslParser::parseCslFormula(input) - ); - - result = formula->evaluate(mc); - - // Test the selection. - ASSERT_EQ(3, result.selection.getNumberOfSetBits()); - ASSERT_FALSE(result.selection[0]); - ASSERT_FALSE(result.selection[1]); - ASSERT_FALSE(result.selection[2]); - ASSERT_TRUE(result.selection[3]); - ASSERT_FALSE(result.selection[4]); - ASSERT_TRUE(result.selection[5]); - ASSERT_TRUE(result.selection[6]); - ASSERT_FALSE(result.selection[7]); - - // Test the sorting. - ASSERT_EQ(7, result.stateMap[0]); - ASSERT_EQ(6, result.stateMap[1]); - ASSERT_EQ(5, result.stateMap[2]); - ASSERT_EQ(4, result.stateMap[3]); - ASSERT_EQ(3, result.stateMap[4]); - ASSERT_EQ(2, result.stateMap[5]); - ASSERT_EQ(1, result.stateMap[6]); - ASSERT_EQ(0, result.stateMap[7]); -} - -TEST(CslFilterTest, Safety) { - // Setup model and modelchecker. - storm::models::MarkovAutomaton model = storm::parser::MarkovAutomatonParser::parseMarkovAutomaton(STORM_CPP_TESTS_BASE_PATH "/functional/parser/tra_files/ma_cslFilterTest.tra", STORM_CPP_TESTS_BASE_PATH "/functional/parser/lab_files/ma_cslFilterTest.lab"); - storm::modelchecker::csl::SparseMarkovAutomatonCslModelChecker mc(model, std::make_shared>()); - - // Make a stub formula as child. - auto apFormula = std::make_shared>("r1"); - - // Test the filter for nullptr action handling. - auto formula = std::make_shared>(apFormula, nullptr, storm::properties::MAXIMIZE); - - ASSERT_NO_THROW(formula->evaluate(mc)); - ASSERT_EQ(0, formula->getActionCount()); - - // Repeat with vector containing only one action but three nullptr. - std::vector>> actions(4, nullptr); - actions[1] = std::make_shared>(); - - formula = std::make_shared>(apFormula, actions, storm::properties::MAXIMIZE); - - ASSERT_EQ(1, formula->getActionCount()); - ASSERT_NO_THROW(formula->evaluate(mc)); - - // Test the filter for nullptr child formula handling. - // It sholud not write anything to the standard out and return an empty result. - formula = std::make_shared>(); - Result result; - - // To capture the output, redirect cout and test the written buffer content. - std::stringstream buffer; - std::streambuf *sbuf = std::cout.rdbuf(); - std::cout.rdbuf(buffer.rdbuf()); - - ASSERT_NO_THROW(result = formula->evaluate(mc)); - - // Reset cout to the original buffer. - std::cout.rdbuf(sbuf); - - ASSERT_EQ(0, buffer.str().length()); - - ASSERT_EQ(0, result.pathResult.size()); - ASSERT_EQ(0, result.stateResult.size()); - ASSERT_EQ(0, result.selection.size()); - ASSERT_EQ(0, result.stateMap.size()); -} - -// TODO Set up the LtlFilterTest once an Ltl modelchecker has been implemented. diff --git a/test/functional/modelchecker/GmmxxDtmcPrctlModelCheckerTest.cpp b/test/functional/modelchecker/GmmxxDtmcPrctlModelCheckerTest.cpp index 8bb9fadda..1d914c950 100644 --- a/test/functional/modelchecker/GmmxxDtmcPrctlModelCheckerTest.cpp +++ b/test/functional/modelchecker/GmmxxDtmcPrctlModelCheckerTest.cpp @@ -1,116 +1,116 @@ -#include "gtest/gtest.h" -#include "storm-config.h" - -#include "src/solver/GmmxxLinearEquationSolver.h" -#include "src/modelchecker/prctl/SparseDtmcPrctlModelChecker.h" -#include "src/settings/SettingsManager.h" -#include "src/settings/SettingMemento.h" -#include "src/parser/AutoParser.h" - -TEST(GmmxxDtmcPrctlModelCheckerTest, Die) { - std::shared_ptr> abstractModel = storm::parser::AutoParser::parseModel(STORM_CPP_BASE_PATH "/examples/dtmc/die/die.tra", STORM_CPP_BASE_PATH "/examples/dtmc/die/die.lab", "", STORM_CPP_BASE_PATH "/examples/dtmc/die/die.coin_flips.trans.rew"); - - ASSERT_EQ(abstractModel->getType(), storm::models::DTMC); - - std::shared_ptr> dtmc = abstractModel->as>(); - - ASSERT_EQ(dtmc->getNumberOfStates(), 13ull); - ASSERT_EQ(dtmc->getNumberOfTransitions(), 20ull); - - storm::modelchecker::prctl::SparseDtmcPrctlModelChecker mc(*dtmc, std::unique_ptr>(new storm::solver::GmmxxLinearEquationSolver())); - - auto apFormula = std::make_shared>("one"); - auto eventuallyFormula = std::make_shared>(apFormula); - - std::vector result = eventuallyFormula->check(mc, false); - - ASSERT_LT(std::abs(result[0] - ((double)1.0/6.0)), storm::settings::gmmxxEquationSolverSettings().getPrecision()); - - apFormula = std::make_shared>("two"); - eventuallyFormula = std::make_shared>(apFormula); - - result = eventuallyFormula->check(mc, false); - - ASSERT_LT(std::abs(result[0] - ((double)1.0/6.0)), storm::settings::gmmxxEquationSolverSettings().getPrecision()); - - apFormula = std::make_shared>("three"); - eventuallyFormula = std::make_shared>(apFormula); - - result = eventuallyFormula->check(mc, false); - - ASSERT_LT(std::abs(result[0] - ((double)1.0/6.0)), storm::settings::gmmxxEquationSolverSettings().getPrecision()); - - auto done = std::make_shared>("done"); - auto reachabilityRewardFormula = std::make_shared>(done); - - result = reachabilityRewardFormula->check(mc, false); - - ASSERT_LT(std::abs(result[0] - ((double)11/3)), storm::settings::gmmxxEquationSolverSettings().getPrecision()); -} - -TEST(GmmxxDtmcPrctlModelCheckerTest, Crowds) { - std::shared_ptr> abstractModel = storm::parser::AutoParser::parseModel(STORM_CPP_BASE_PATH "/examples/dtmc/crowds/crowds5_5.tra", STORM_CPP_BASE_PATH "/examples/dtmc/crowds/crowds5_5.lab", "", ""); - - ASSERT_EQ(abstractModel->getType(), storm::models::DTMC); - - std::shared_ptr> dtmc = abstractModel->as>(); - - ASSERT_EQ(8607ull, dtmc->getNumberOfStates()); - ASSERT_EQ(15113ull, dtmc->getNumberOfTransitions()); - - storm::modelchecker::prctl::SparseDtmcPrctlModelChecker mc(*dtmc, std::unique_ptr>(new storm::solver::GmmxxLinearEquationSolver())); - - auto apFormula = std::make_shared>("observe0Greater1"); - auto eventuallyFormula = std::make_shared>(apFormula); - - std::vector result = eventuallyFormula->check(mc, false); - - ASSERT_LT(std::abs(result[0] - 0.3328800375801578281), storm::settings::gmmxxEquationSolverSettings().getPrecision()); - - apFormula = std::make_shared>("observeIGreater1"); - eventuallyFormula = std::make_shared>(apFormula); - - result = eventuallyFormula->check(mc, false); - - ASSERT_LT(std::abs(result[0] - 0.1522194965), storm::settings::gmmxxEquationSolverSettings().getPrecision()); - - apFormula = std::make_shared>("observeOnlyTrueSender"); - eventuallyFormula = std::make_shared>(apFormula); - - result = eventuallyFormula->check(mc, false); - - ASSERT_LT(std::abs(result[0] - 0.32153724292835045), storm::settings::gmmxxEquationSolverSettings().getPrecision()); -} - -TEST(GmmxxDtmcPrctlModelCheckerTest, SynchronousLeader) { - std::shared_ptr> abstractModel = storm::parser::AutoParser::parseModel(STORM_CPP_BASE_PATH "/examples/dtmc/synchronous_leader/leader4_8.tra", STORM_CPP_BASE_PATH "/examples/dtmc/synchronous_leader/leader4_8.lab", "", STORM_CPP_BASE_PATH "/examples/dtmc/synchronous_leader/leader4_8.pick.trans.rew"); - - ASSERT_EQ(abstractModel->getType(), storm::models::DTMC); - std::shared_ptr> dtmc = abstractModel->as>(); - - ASSERT_EQ(12400ull, dtmc->getNumberOfStates()); - ASSERT_EQ(16495ull, dtmc->getNumberOfTransitions()); - - storm::modelchecker::prctl::SparseDtmcPrctlModelChecker mc(*dtmc, std::unique_ptr>(new storm::solver::GmmxxLinearEquationSolver())); - - auto apFormula = std::make_shared>("elected"); - auto eventuallyFormula = std::make_shared>(apFormula); - - std::vector result = eventuallyFormula->check(mc, false); - - ASSERT_LT(std::abs(result[0] - 1.0), storm::settings::gmmxxEquationSolverSettings().getPrecision()); - - apFormula = std::make_shared>("elected"); - auto boundedUntilFormula = std::make_shared>(std::make_shared>("true"), apFormula, 20); - - result = boundedUntilFormula->check(mc, false); - - ASSERT_LT(std::abs(result[0] - 0.9999965911265462636), storm::settings::gmmxxEquationSolverSettings().getPrecision()); - - apFormula = std::make_shared>("elected"); - auto reachabilityRewardFormula = std::make_shared>(apFormula); - - result = reachabilityRewardFormula->check(mc, false); - - ASSERT_LT(std::abs(result[0] - 1.044879046), storm::settings::gmmxxEquationSolverSettings().getPrecision()); -} +//#include "gtest/gtest.h" +//#include "storm-config.h" +// +//#include "src/solver/GmmxxLinearEquationSolver.h" +//#include "src/modelchecker/prctl/SparseDtmcPrctlModelChecker.h" +//#include "src/settings/SettingsManager.h" +//#include "src/settings/SettingMemento.h" +//#include "src/parser/AutoParser.h" +// +//TEST(GmmxxDtmcPrctlModelCheckerTest, Die) { +// std::shared_ptr> abstractModel = storm::parser::AutoParser::parseModel(STORM_CPP_BASE_PATH "/examples/dtmc/die/die.tra", STORM_CPP_BASE_PATH "/examples/dtmc/die/die.lab", "", STORM_CPP_BASE_PATH "/examples/dtmc/die/die.coin_flips.trans.rew"); +// +// ASSERT_EQ(abstractModel->getType(), storm::models::DTMC); +// +// std::shared_ptr> dtmc = abstractModel->as>(); +// +// ASSERT_EQ(dtmc->getNumberOfStates(), 13ull); +// ASSERT_EQ(dtmc->getNumberOfTransitions(), 20ull); +// +// storm::modelchecker::prctl::SparseDtmcPrctlModelChecker mc(*dtmc, std::unique_ptr>(new storm::solver::GmmxxLinearEquationSolver())); +// +// auto apFormula = std::make_shared>("one"); +// auto eventuallyFormula = std::make_shared>(apFormula); +// +// std::vector result = eventuallyFormula->check(mc, false); +// +// ASSERT_LT(std::abs(result[0] - ((double)1.0/6.0)), storm::settings::gmmxxEquationSolverSettings().getPrecision()); +// +// apFormula = std::make_shared>("two"); +// eventuallyFormula = std::make_shared>(apFormula); +// +// result = eventuallyFormula->check(mc, false); +// +// ASSERT_LT(std::abs(result[0] - ((double)1.0/6.0)), storm::settings::gmmxxEquationSolverSettings().getPrecision()); +// +// apFormula = std::make_shared>("three"); +// eventuallyFormula = std::make_shared>(apFormula); +// +// result = eventuallyFormula->check(mc, false); +// +// ASSERT_LT(std::abs(result[0] - ((double)1.0/6.0)), storm::settings::gmmxxEquationSolverSettings().getPrecision()); +// +// auto done = std::make_shared>("done"); +// auto reachabilityRewardFormula = std::make_shared>(done); +// +// result = reachabilityRewardFormula->check(mc, false); +// +// ASSERT_LT(std::abs(result[0] - ((double)11/3)), storm::settings::gmmxxEquationSolverSettings().getPrecision()); +//} +// +//TEST(GmmxxDtmcPrctlModelCheckerTest, Crowds) { +// std::shared_ptr> abstractModel = storm::parser::AutoParser::parseModel(STORM_CPP_BASE_PATH "/examples/dtmc/crowds/crowds5_5.tra", STORM_CPP_BASE_PATH "/examples/dtmc/crowds/crowds5_5.lab", "", ""); +// +// ASSERT_EQ(abstractModel->getType(), storm::models::DTMC); +// +// std::shared_ptr> dtmc = abstractModel->as>(); +// +// ASSERT_EQ(8607ull, dtmc->getNumberOfStates()); +// ASSERT_EQ(15113ull, dtmc->getNumberOfTransitions()); +// +// storm::modelchecker::prctl::SparseDtmcPrctlModelChecker mc(*dtmc, std::unique_ptr>(new storm::solver::GmmxxLinearEquationSolver())); +// +// auto apFormula = std::make_shared>("observe0Greater1"); +// auto eventuallyFormula = std::make_shared>(apFormula); +// +// std::vector result = eventuallyFormula->check(mc, false); +// +// ASSERT_LT(std::abs(result[0] - 0.3328800375801578281), storm::settings::gmmxxEquationSolverSettings().getPrecision()); +// +// apFormula = std::make_shared>("observeIGreater1"); +// eventuallyFormula = std::make_shared>(apFormula); +// +// result = eventuallyFormula->check(mc, false); +// +// ASSERT_LT(std::abs(result[0] - 0.1522194965), storm::settings::gmmxxEquationSolverSettings().getPrecision()); +// +// apFormula = std::make_shared>("observeOnlyTrueSender"); +// eventuallyFormula = std::make_shared>(apFormula); +// +// result = eventuallyFormula->check(mc, false); +// +// ASSERT_LT(std::abs(result[0] - 0.32153724292835045), storm::settings::gmmxxEquationSolverSettings().getPrecision()); +//} +// +//TEST(GmmxxDtmcPrctlModelCheckerTest, SynchronousLeader) { +// std::shared_ptr> abstractModel = storm::parser::AutoParser::parseModel(STORM_CPP_BASE_PATH "/examples/dtmc/synchronous_leader/leader4_8.tra", STORM_CPP_BASE_PATH "/examples/dtmc/synchronous_leader/leader4_8.lab", "", STORM_CPP_BASE_PATH "/examples/dtmc/synchronous_leader/leader4_8.pick.trans.rew"); +// +// ASSERT_EQ(abstractModel->getType(), storm::models::DTMC); +// std::shared_ptr> dtmc = abstractModel->as>(); +// +// ASSERT_EQ(12400ull, dtmc->getNumberOfStates()); +// ASSERT_EQ(16495ull, dtmc->getNumberOfTransitions()); +// +// storm::modelchecker::prctl::SparseDtmcPrctlModelChecker mc(*dtmc, std::unique_ptr>(new storm::solver::GmmxxLinearEquationSolver())); +// +// auto apFormula = std::make_shared>("elected"); +// auto eventuallyFormula = std::make_shared>(apFormula); +// +// std::vector result = eventuallyFormula->check(mc, false); +// +// ASSERT_LT(std::abs(result[0] - 1.0), storm::settings::gmmxxEquationSolverSettings().getPrecision()); +// +// apFormula = std::make_shared>("elected"); +// auto boundedUntilFormula = std::make_shared>(std::make_shared>("true"), apFormula, 20); +// +// result = boundedUntilFormula->check(mc, false); +// +// ASSERT_LT(std::abs(result[0] - 0.9999965911265462636), storm::settings::gmmxxEquationSolverSettings().getPrecision()); +// +// apFormula = std::make_shared>("elected"); +// auto reachabilityRewardFormula = std::make_shared>(apFormula); +// +// result = reachabilityRewardFormula->check(mc, false); +// +// ASSERT_LT(std::abs(result[0] - 1.044879046), storm::settings::gmmxxEquationSolverSettings().getPrecision()); +//} diff --git a/test/functional/modelchecker/SparseMdpPrctlModelCheckerTest.cpp b/test/functional/modelchecker/SparseMdpPrctlModelCheckerTest.cpp index 106502b8f..5bfbae27e 100644 --- a/test/functional/modelchecker/SparseMdpPrctlModelCheckerTest.cpp +++ b/test/functional/modelchecker/SparseMdpPrctlModelCheckerTest.cpp @@ -1,148 +1,148 @@ -#include "gtest/gtest.h" -#include "storm-config.h" - -#include "src/solver/NativeNondeterministicLinearEquationSolver.h" -#include "src/settings/SettingsManager.h" -#include "src/modelchecker/prctl/SparseMdpPrctlModelChecker.h" -#include "src/parser/AutoParser.h" - -TEST(SparseMdpPrctlModelCheckerTest, Dice) { - std::shared_ptr> abstractModel = storm::parser::AutoParser::parseModel(STORM_CPP_BASE_PATH "/examples/mdp/two_dice/two_dice.tra", STORM_CPP_BASE_PATH "/examples/mdp/two_dice/two_dice.lab", "", STORM_CPP_BASE_PATH "/examples/mdp/two_dice/two_dice.flip.trans.rew"); - - ASSERT_EQ(abstractModel->getType(), storm::models::MDP); - - std::shared_ptr> mdp = abstractModel->as>(); - - ASSERT_EQ(mdp->getNumberOfStates(), 169ull); - ASSERT_EQ(mdp->getNumberOfTransitions(), 436ull); - - storm::modelchecker::prctl::SparseMdpPrctlModelChecker mc(*mdp, std::shared_ptr>(new storm::solver::NativeNondeterministicLinearEquationSolver())); - - auto apFormula = std::make_shared>("two"); - auto eventuallyFormula = std::make_shared>(apFormula); - - std::vector result = mc.checkOptimizingOperator(*eventuallyFormula, true); - - ASSERT_LT(std::abs(result[0] - 0.0277777612209320068), storm::settings::nativeEquationSolverSettings().getPrecision()); - - result = mc.checkOptimizingOperator(*eventuallyFormula, false); - - ASSERT_LT(std::abs(result[0] - 0.0277777612209320068), storm::settings::nativeEquationSolverSettings().getPrecision()); - - apFormula = std::make_shared>("three"); - eventuallyFormula = std::make_shared>(apFormula); - - result = mc.checkOptimizingOperator(*eventuallyFormula, true); - - ASSERT_LT(std::abs(result[0] - 0.0555555224418640136), storm::settings::nativeEquationSolverSettings().getPrecision()); - - result = mc.checkOptimizingOperator(*eventuallyFormula, false); - - ASSERT_LT(std::abs(result[0] - 0.0555555224418640136), storm::settings::nativeEquationSolverSettings().getPrecision()); - - apFormula = std::make_shared>("four"); - eventuallyFormula = std::make_shared>(apFormula); - - result = mc.checkOptimizingOperator(*eventuallyFormula, true); - - ASSERT_LT(std::abs(result[0] - 0.083333283662796020508), storm::settings::nativeEquationSolverSettings().getPrecision()); - - result = mc.checkOptimizingOperator(*eventuallyFormula, false); - - ASSERT_LT(std::abs(result[0] - 0.083333283662796020508), storm::settings::nativeEquationSolverSettings().getPrecision()); - - apFormula = std::make_shared>("done"); - auto reachabilityRewardFormula = std::make_shared>(apFormula); - - result = mc.checkOptimizingOperator(*reachabilityRewardFormula, true); - - ASSERT_LT(std::abs(result[0] - 7.333329499), storm::settings::nativeEquationSolverSettings().getPrecision()); - - result = mc.checkOptimizingOperator(*reachabilityRewardFormula, false); - - ASSERT_LT(std::abs(result[0] - 7.333329499), storm::settings::nativeEquationSolverSettings().getPrecision()); - - abstractModel = storm::parser::AutoParser::parseModel(STORM_CPP_BASE_PATH "/examples/mdp/two_dice/two_dice.tra", STORM_CPP_BASE_PATH "/examples/mdp/two_dice/two_dice.lab", STORM_CPP_BASE_PATH "/examples/mdp/two_dice/two_dice.flip.state.rew", ""); - - ASSERT_EQ(abstractModel->getType(), storm::models::MDP); - - std::shared_ptr> stateRewardMdp = abstractModel->as>(); - - storm::modelchecker::prctl::SparseMdpPrctlModelChecker stateRewardModelChecker(*stateRewardMdp, std::shared_ptr>(new storm::solver::NativeNondeterministicLinearEquationSolver())); - - apFormula = std::make_shared>("done"); - reachabilityRewardFormula = std::make_shared>(apFormula); - - result = stateRewardModelChecker.checkOptimizingOperator(*reachabilityRewardFormula, true); - - ASSERT_LT(std::abs(result[0] - 7.333329499), storm::settings::nativeEquationSolverSettings().getPrecision()); - - result = stateRewardModelChecker.checkOptimizingOperator(*reachabilityRewardFormula, false); - - ASSERT_LT(std::abs(result[0] - 7.333329499), storm::settings::nativeEquationSolverSettings().getPrecision()); - - abstractModel = storm::parser::AutoParser::parseModel(STORM_CPP_BASE_PATH "/examples/mdp/two_dice/two_dice.tra", STORM_CPP_BASE_PATH "/examples/mdp/two_dice/two_dice.lab", STORM_CPP_BASE_PATH "/examples/mdp/two_dice/two_dice.flip.state.rew", STORM_CPP_BASE_PATH "/examples/mdp/two_dice/two_dice.flip.trans.rew"); - - ASSERT_EQ(abstractModel->getType(), storm::models::MDP); - - std::shared_ptr> stateAndTransitionRewardMdp = abstractModel->as>(); - - storm::modelchecker::prctl::SparseMdpPrctlModelChecker stateAndTransitionRewardModelChecker(*stateAndTransitionRewardMdp, std::shared_ptr>(new storm::solver::NativeNondeterministicLinearEquationSolver())); - - apFormula = std::make_shared>("done"); - reachabilityRewardFormula = std::make_shared>(apFormula); - - result = stateAndTransitionRewardModelChecker.checkOptimizingOperator(*reachabilityRewardFormula, true); - - ASSERT_LT(std::abs(result[0] - 14.666658998), storm::settings::nativeEquationSolverSettings().getPrecision()); - - result = stateAndTransitionRewardModelChecker.checkOptimizingOperator(*reachabilityRewardFormula, false); - - ASSERT_LT(std::abs(result[0] - 14.666658998), storm::settings::nativeEquationSolverSettings().getPrecision()); -} - -TEST(SparseMdpPrctlModelCheckerTest, AsynchronousLeader) { - std::shared_ptr> abstractModel = storm::parser::AutoParser::parseModel(STORM_CPP_BASE_PATH "/examples/mdp/asynchronous_leader/leader4.tra", STORM_CPP_BASE_PATH "/examples/mdp/asynchronous_leader/leader4.lab", "", STORM_CPP_BASE_PATH "/examples/mdp/asynchronous_leader/leader4.trans.rew"); - - ASSERT_EQ(storm::models::MDP, abstractModel->getType()); - - std::shared_ptr> mdp = abstractModel->as>(); - - ASSERT_EQ(3172ull, mdp->getNumberOfStates()); - ASSERT_EQ(7144ull, mdp->getNumberOfTransitions()); - - storm::modelchecker::prctl::SparseMdpPrctlModelChecker mc(*mdp, std::shared_ptr>(new storm::solver::NativeNondeterministicLinearEquationSolver())); - - auto apFormula = std::make_shared>("elected"); - auto eventuallyFormula = std::make_shared>(apFormula); - - std::vector result = mc.checkOptimizingOperator(*eventuallyFormula, true); - - ASSERT_LT(std::abs(result[0] - 1), storm::settings::nativeEquationSolverSettings().getPrecision()); - - result = mc.checkOptimizingOperator(*eventuallyFormula, false); - - ASSERT_LT(std::abs(result[0] - 1), storm::settings::nativeEquationSolverSettings().getPrecision()); - - apFormula = std::make_shared>("elected"); - auto boundedEventuallyFormula = std::make_shared>(apFormula, 25); - - result = mc.checkOptimizingOperator(*boundedEventuallyFormula, true); - - ASSERT_LT(std::abs(result[0] - 0.0625), storm::settings::nativeEquationSolverSettings().getPrecision()); - - result = mc.checkOptimizingOperator(*boundedEventuallyFormula, false); - - ASSERT_LT(std::abs(result[0] - 0.0625), storm::settings::nativeEquationSolverSettings().getPrecision()); - - apFormula = std::make_shared>("elected"); - auto reachabilityRewardFormula = std::make_shared>(apFormula); - - result = mc.checkOptimizingOperator(*reachabilityRewardFormula, true); - - ASSERT_LT(std::abs(result[0] - 4.285689611), storm::settings::nativeEquationSolverSettings().getPrecision()); - - result = mc.checkOptimizingOperator(*reachabilityRewardFormula, false); - - ASSERT_LT(std::abs(result[0] - 4.285689611), storm::settings::nativeEquationSolverSettings().getPrecision()); -} +//#include "gtest/gtest.h" +//#include "storm-config.h" +// +//#include "src/solver/NativeNondeterministicLinearEquationSolver.h" +//#include "src/settings/SettingsManager.h" +//#include "src/modelchecker/prctl/SparseMdpPrctlModelChecker.h" +//#include "src/parser/AutoParser.h" +// +//TEST(SparseMdpPrctlModelCheckerTest, Dice) { +// std::shared_ptr> abstractModel = storm::parser::AutoParser::parseModel(STORM_CPP_BASE_PATH "/examples/mdp/two_dice/two_dice.tra", STORM_CPP_BASE_PATH "/examples/mdp/two_dice/two_dice.lab", "", STORM_CPP_BASE_PATH "/examples/mdp/two_dice/two_dice.flip.trans.rew"); +// +// ASSERT_EQ(abstractModel->getType(), storm::models::MDP); +// +// std::shared_ptr> mdp = abstractModel->as>(); +// +// ASSERT_EQ(mdp->getNumberOfStates(), 169ull); +// ASSERT_EQ(mdp->getNumberOfTransitions(), 436ull); +// +// storm::modelchecker::prctl::SparseMdpPrctlModelChecker mc(*mdp, std::shared_ptr>(new storm::solver::NativeNondeterministicLinearEquationSolver())); +// +// auto apFormula = std::make_shared>("two"); +// auto eventuallyFormula = std::make_shared>(apFormula); +// +// std::vector result = mc.checkOptimizingOperator(*eventuallyFormula, true); +// +// ASSERT_LT(std::abs(result[0] - 0.0277777612209320068), storm::settings::nativeEquationSolverSettings().getPrecision()); +// +// result = mc.checkOptimizingOperator(*eventuallyFormula, false); +// +// ASSERT_LT(std::abs(result[0] - 0.0277777612209320068), storm::settings::nativeEquationSolverSettings().getPrecision()); +// +// apFormula = std::make_shared>("three"); +// eventuallyFormula = std::make_shared>(apFormula); +// +// result = mc.checkOptimizingOperator(*eventuallyFormula, true); +// +// ASSERT_LT(std::abs(result[0] - 0.0555555224418640136), storm::settings::nativeEquationSolverSettings().getPrecision()); +// +// result = mc.checkOptimizingOperator(*eventuallyFormula, false); +// +// ASSERT_LT(std::abs(result[0] - 0.0555555224418640136), storm::settings::nativeEquationSolverSettings().getPrecision()); +// +// apFormula = std::make_shared>("four"); +// eventuallyFormula = std::make_shared>(apFormula); +// +// result = mc.checkOptimizingOperator(*eventuallyFormula, true); +// +// ASSERT_LT(std::abs(result[0] - 0.083333283662796020508), storm::settings::nativeEquationSolverSettings().getPrecision()); +// +// result = mc.checkOptimizingOperator(*eventuallyFormula, false); +// +// ASSERT_LT(std::abs(result[0] - 0.083333283662796020508), storm::settings::nativeEquationSolverSettings().getPrecision()); +// +// apFormula = std::make_shared>("done"); +// auto reachabilityRewardFormula = std::make_shared>(apFormula); +// +// result = mc.checkOptimizingOperator(*reachabilityRewardFormula, true); +// +// ASSERT_LT(std::abs(result[0] - 7.333329499), storm::settings::nativeEquationSolverSettings().getPrecision()); +// +// result = mc.checkOptimizingOperator(*reachabilityRewardFormula, false); +// +// ASSERT_LT(std::abs(result[0] - 7.333329499), storm::settings::nativeEquationSolverSettings().getPrecision()); +// +// abstractModel = storm::parser::AutoParser::parseModel(STORM_CPP_BASE_PATH "/examples/mdp/two_dice/two_dice.tra", STORM_CPP_BASE_PATH "/examples/mdp/two_dice/two_dice.lab", STORM_CPP_BASE_PATH "/examples/mdp/two_dice/two_dice.flip.state.rew", ""); +// +// ASSERT_EQ(abstractModel->getType(), storm::models::MDP); +// +// std::shared_ptr> stateRewardMdp = abstractModel->as>(); +// +// storm::modelchecker::prctl::SparseMdpPrctlModelChecker stateRewardModelChecker(*stateRewardMdp, std::shared_ptr>(new storm::solver::NativeNondeterministicLinearEquationSolver())); +// +// apFormula = std::make_shared>("done"); +// reachabilityRewardFormula = std::make_shared>(apFormula); +// +// result = stateRewardModelChecker.checkOptimizingOperator(*reachabilityRewardFormula, true); +// +// ASSERT_LT(std::abs(result[0] - 7.333329499), storm::settings::nativeEquationSolverSettings().getPrecision()); +// +// result = stateRewardModelChecker.checkOptimizingOperator(*reachabilityRewardFormula, false); +// +// ASSERT_LT(std::abs(result[0] - 7.333329499), storm::settings::nativeEquationSolverSettings().getPrecision()); +// +// abstractModel = storm::parser::AutoParser::parseModel(STORM_CPP_BASE_PATH "/examples/mdp/two_dice/two_dice.tra", STORM_CPP_BASE_PATH "/examples/mdp/two_dice/two_dice.lab", STORM_CPP_BASE_PATH "/examples/mdp/two_dice/two_dice.flip.state.rew", STORM_CPP_BASE_PATH "/examples/mdp/two_dice/two_dice.flip.trans.rew"); +// +// ASSERT_EQ(abstractModel->getType(), storm::models::MDP); +// +// std::shared_ptr> stateAndTransitionRewardMdp = abstractModel->as>(); +// +// storm::modelchecker::prctl::SparseMdpPrctlModelChecker stateAndTransitionRewardModelChecker(*stateAndTransitionRewardMdp, std::shared_ptr>(new storm::solver::NativeNondeterministicLinearEquationSolver())); +// +// apFormula = std::make_shared>("done"); +// reachabilityRewardFormula = std::make_shared>(apFormula); +// +// result = stateAndTransitionRewardModelChecker.checkOptimizingOperator(*reachabilityRewardFormula, true); +// +// ASSERT_LT(std::abs(result[0] - 14.666658998), storm::settings::nativeEquationSolverSettings().getPrecision()); +// +// result = stateAndTransitionRewardModelChecker.checkOptimizingOperator(*reachabilityRewardFormula, false); +// +// ASSERT_LT(std::abs(result[0] - 14.666658998), storm::settings::nativeEquationSolverSettings().getPrecision()); +//} +// +//TEST(SparseMdpPrctlModelCheckerTest, AsynchronousLeader) { +// std::shared_ptr> abstractModel = storm::parser::AutoParser::parseModel(STORM_CPP_BASE_PATH "/examples/mdp/asynchronous_leader/leader4.tra", STORM_CPP_BASE_PATH "/examples/mdp/asynchronous_leader/leader4.lab", "", STORM_CPP_BASE_PATH "/examples/mdp/asynchronous_leader/leader4.trans.rew"); +// +// ASSERT_EQ(storm::models::MDP, abstractModel->getType()); +// +// std::shared_ptr> mdp = abstractModel->as>(); +// +// ASSERT_EQ(3172ull, mdp->getNumberOfStates()); +// ASSERT_EQ(7144ull, mdp->getNumberOfTransitions()); +// +// storm::modelchecker::prctl::SparseMdpPrctlModelChecker mc(*mdp, std::shared_ptr>(new storm::solver::NativeNondeterministicLinearEquationSolver())); +// +// auto apFormula = std::make_shared>("elected"); +// auto eventuallyFormula = std::make_shared>(apFormula); +// +// std::vector result = mc.checkOptimizingOperator(*eventuallyFormula, true); +// +// ASSERT_LT(std::abs(result[0] - 1), storm::settings::nativeEquationSolverSettings().getPrecision()); +// +// result = mc.checkOptimizingOperator(*eventuallyFormula, false); +// +// ASSERT_LT(std::abs(result[0] - 1), storm::settings::nativeEquationSolverSettings().getPrecision()); +// +// apFormula = std::make_shared>("elected"); +// auto boundedEventuallyFormula = std::make_shared>(apFormula, 25); +// +// result = mc.checkOptimizingOperator(*boundedEventuallyFormula, true); +// +// ASSERT_LT(std::abs(result[0] - 0.0625), storm::settings::nativeEquationSolverSettings().getPrecision()); +// +// result = mc.checkOptimizingOperator(*boundedEventuallyFormula, false); +// +// ASSERT_LT(std::abs(result[0] - 0.0625), storm::settings::nativeEquationSolverSettings().getPrecision()); +// +// apFormula = std::make_shared>("elected"); +// auto reachabilityRewardFormula = std::make_shared>(apFormula); +// +// result = mc.checkOptimizingOperator(*reachabilityRewardFormula, true); +// +// ASSERT_LT(std::abs(result[0] - 4.285689611), storm::settings::nativeEquationSolverSettings().getPrecision()); +// +// result = mc.checkOptimizingOperator(*reachabilityRewardFormula, false); +// +// ASSERT_LT(std::abs(result[0] - 4.285689611), storm::settings::nativeEquationSolverSettings().getPrecision()); +//} diff --git a/test/functional/parser/CslParserTest.cpp b/test/functional/parser/CslParserTest.cpp deleted file mode 100644 index 42b805ac4..000000000 --- a/test/functional/parser/CslParserTest.cpp +++ /dev/null @@ -1,259 +0,0 @@ -/* - * CslParserTest.cpp - * - * Created on: 09.04.2013 - * Author: Thomas Heinemann - */ - -#include "gtest/gtest.h" -#include "storm-config.h" -#include "src/parser/CslParser.h" -#include "src/exceptions/WrongFormatException.h" -#include "src/properties/actions/FormulaAction.h" -#include "src/properties/actions/InvertAction.h" -#include "src/properties/actions/SortAction.h" -#include "src/properties/actions/RangeAction.h" -#include "src/properties/actions/BoundAction.h" - -namespace csl = storm::properties::csl; - -TEST(CslParserTest, parseApOnlyTest) { - std::string input = "ap"; - std::shared_ptr> formula(nullptr); - ASSERT_NO_THROW( - formula = storm::parser::CslParser::parseCslFormula(input); - ); - - // The parser did not falsely recognize the input as a comment. - ASSERT_NE(formula.get(), nullptr); - - ASSERT_TRUE(formula->getChild()->isPropositional()); - ASSERT_FALSE(formula->getChild()->isProbEventuallyAP()); - - // The input was parsed correctly. - ASSERT_EQ(input, formula->toString()); -} - -TEST(CslParserTest, parsePropositionalFormulaTest) { - std::string input = "!(a & b) | a & ! c"; - std::shared_ptr> formula(nullptr); - ASSERT_NO_THROW( - formula = storm::parser::CslParser::parseCslFormula(input); - ); - - // The parser did not falsely recognize the input as a comment. - ASSERT_NE(formula.get(), nullptr); - - ASSERT_TRUE(formula->getChild()->isPropositional()); - ASSERT_FALSE(formula->getChild()->isProbEventuallyAP()); - - // The input was parsed correctly. - ASSERT_EQ("(!(a & b) | (a & !c))", formula->toString()); -} - -TEST(CslParserTest, parsePathFormulaTest) { - std::string input = "X( P<0.9 (a U b))"; - std::shared_ptr> formula(nullptr); - ASSERT_NO_THROW( - formula = storm::parser::CslParser::parseCslFormula(input) - ); - - // The parser did not falsely recognize the input as a comment. - ASSERT_NE(formula, nullptr); - - // The input was parsed correctly. - ASSERT_NE(std::dynamic_pointer_cast>(formula->getChild()).get(), nullptr); - auto nextFormula = std::dynamic_pointer_cast>(formula->getChild()); - ASSERT_FALSE(nextFormula->isPropositional()); - ASSERT_FALSE(nextFormula->isProbEventuallyAP()); - - ASSERT_NE(std::dynamic_pointer_cast>(nextFormula->getChild()).get(), nullptr); - auto probBoundFormula = std::dynamic_pointer_cast>(nextFormula->getChild()); - ASSERT_EQ(0.9, probBoundFormula->getBound()); - ASSERT_EQ(storm::properties::LESS, probBoundFormula->getComparisonOperator()); - ASSERT_FALSE(probBoundFormula->isPropositional()); - ASSERT_TRUE(probBoundFormula->isProbEventuallyAP()); - - ASSERT_NE(std::dynamic_pointer_cast>(probBoundFormula->getChild()).get(), nullptr); - auto untilFormula = std::dynamic_pointer_cast>(probBoundFormula->getChild()); - ASSERT_FALSE(untilFormula->isPropositional()); - ASSERT_FALSE(untilFormula->isProbEventuallyAP()); - - ASSERT_NE(std::dynamic_pointer_cast>(untilFormula->getLeft()).get(), nullptr); - ASSERT_NE(std::dynamic_pointer_cast>(untilFormula->getRight()).get(), nullptr); - ASSERT_EQ("a", std::dynamic_pointer_cast>(untilFormula->getLeft())->getAp()); - ASSERT_EQ("b", std::dynamic_pointer_cast>(untilFormula->getRight())->getAp()); - - - // The string representation is also correct. - ASSERT_EQ("P = ? (X P < 0.900000 (a U b))", formula->toString()); -} - -TEST(CslParserTest, parseProbabilisticFormulaTest) { - std::string input = "P > 0.5 [ F a ]"; - std::shared_ptr> formula(nullptr); - ASSERT_NO_THROW( - formula = storm::parser::CslParser::parseCslFormula(input); - ); - - // The parser did not falsely recognize the input as a comment. - ASSERT_NE(formula.get(), nullptr); - - auto op = std::dynamic_pointer_cast>(formula->getChild()); - ASSERT_NE(op.get(), nullptr); - ASSERT_EQ(storm::properties::GREATER, op->getComparisonOperator()); - ASSERT_EQ(0.5, op->getBound()); - ASSERT_FALSE(op->isPropositional()); - ASSERT_TRUE(op->isProbEventuallyAP()); - - // Test the string representation for the parsed formula. - ASSERT_EQ("P > 0.500000 (F a)", formula->toString()); -} - -TEST(CslParserTest, parseSteadyStateBoundFormulaTest) { - std::string input = "S >= 15 [ P < 0.2 [ a U<=3 b ] ]"; - std::shared_ptr> formula(nullptr); - ASSERT_NO_THROW( - formula = storm::parser::CslParser::parseCslFormula(input); - ); - - // The parser did not falsely recognize the input as a comment. - ASSERT_NE(formula.get(), nullptr); - - auto op = std::dynamic_pointer_cast>(formula->getChild()); - ASSERT_NE(op.get(), nullptr); - ASSERT_EQ(storm::properties::GREATER_EQUAL, op->getComparisonOperator()); - ASSERT_EQ(15.0, op->getBound()); - ASSERT_FALSE(op->isPropositional()); - ASSERT_FALSE(op->isProbEventuallyAP()); - - // Test the string representation for the parsed formula. - ASSERT_EQ("S >= 15.000000 (P < 0.200000 (a U[0.000000,3.000000] b))", formula->toString()); -} - -TEST(CslParserTest, parseSteadyStateNoBoundFormulaTest) { - std::string input = "S = ? [ P <= 0.5 [ F<=3 a ] ]"; - std::shared_ptr> formula(nullptr); - ASSERT_NO_THROW( - formula = storm::parser::CslParser::parseCslFormula(input); - ); - - // The parser did not falsely recognize the input as a comment. - ASSERT_NE(formula.get(), nullptr); - - ASSERT_FALSE(formula->getChild()->isPropositional()); - ASSERT_FALSE(formula->getChild()->isProbEventuallyAP()); - - // The input was parsed correctly. - ASSERT_EQ("S = ? (P <= 0.500000 (F[0.000000,3.000000] a))", formula->toString()); -} - -TEST(CslParserTest, parseProbabilisticNoBoundFormulaTest) { - std::string input = "P = ? [ a U [3,4] b & (!c) ]"; - std::shared_ptr> formula(nullptr); - ASSERT_NO_THROW( - formula = storm::parser::CslParser::parseCslFormula(input); - ); - - // The parser did not falsely recognize the input as a comment. - ASSERT_NE(formula.get(), nullptr); - - ASSERT_FALSE(formula->getChild()->isPropositional()); - ASSERT_FALSE(formula->getChild()->isProbEventuallyAP()); - - // The input was parsed correctly. - ASSERT_EQ("P = ? (a U[3.000000,4.000000] (b & !c))", formula->toString()); -} - - -TEST(CslParserTest, parseComplexFormulaTest) { - std::string input = "S<=0.5 [ P <= 0.5 [ a U c ] ] & (P > 0.5 [ G b] | !P < 0.4 [ G P>0.9 [F >=7 a & b] ]) //and a comment"; - std::shared_ptr> formula(nullptr); - ASSERT_NO_THROW( - formula = storm::parser::CslParser::parseCslFormula(input); - ); - - // The parser did not falsely recognize the input as a comment. - ASSERT_NE(formula.get(), nullptr); - - ASSERT_FALSE(formula->getChild()->isPropositional()); - ASSERT_FALSE(formula->getChild()->isProbEventuallyAP()); - - // The input was parsed correctly. - ASSERT_EQ("S <= 0.500000 ((P <= 0.500000 (a U c) & (P > 0.500000 (G b) | !P < 0.400000 (G P > 0.900000 (F>=7.000000 (a & b))))))", formula->toString()); -} - -TEST(CslParserTest, parseCslFilterTest) { - std::string input = "filter[max; formula(b); invert; bound(<, 0.5); sort(value); range(0,3)](F a)"; - std::shared_ptr> formula(nullptr); - ASSERT_NO_THROW( - formula = storm::parser::CslParser::parseCslFormula(input) - ); - - // The parser did not falsely recognize the input as a comment. - ASSERT_NE(formula, nullptr); - - ASSERT_EQ(storm::properties::MAXIMIZE, formula->getOptimizingOperator()); - - ASSERT_EQ(5, formula->getActionCount()); - ASSERT_NE(std::dynamic_pointer_cast>(formula->getAction(0)).get(), nullptr); - ASSERT_NE(std::dynamic_pointer_cast>(formula->getAction(1)).get(), nullptr); - ASSERT_NE(std::dynamic_pointer_cast>(formula->getAction(2)).get(), nullptr); - ASSERT_NE(std::dynamic_pointer_cast>(formula->getAction(3)).get(), nullptr); - ASSERT_NE(std::dynamic_pointer_cast>(formula->getAction(4)).get(), nullptr); - - ASSERT_FALSE(formula->getChild()->isPropositional()); - ASSERT_FALSE(formula->getChild()->isProbEventuallyAP()); - - // The input was parsed correctly. - ASSERT_EQ("filter[max; formula(b); invert; bound(<, 0.500000); sort(value, ascending); range(0, 3)](F a)", formula->toString()); -} - -TEST(CslParserTest, commentTest) { - std::string input = "// This is a comment. And this is a commented out formula: P<=0.5 [ X a ]"; - std::shared_ptr> formula(nullptr); - ASSERT_NO_THROW( - formula = storm::parser::CslParser::parseCslFormula(input) - ); - - // The parser recognized the input as a comment. - ASSERT_NE(nullptr, formula.get()); - - // Test if the parser recognizes the comment at the end of a line. - input = "P<=0.5 [ X a ] // This is a comment."; - ASSERT_NO_THROW( - formula = storm::parser::CslParser::parseCslFormula(input) - ); - - ASSERT_FALSE(formula->getChild()->isPropositional()); - ASSERT_FALSE(formula->getChild()->isProbEventuallyAP()); - - ASSERT_EQ("P <= 0.500000 (X a)", formula->toString()); -} - -TEST(CslParserTest, wrongProbabilisticFormulaTest) { - std::string input = "P > 0.5 [ a ]"; - std::shared_ptr> formula(nullptr); - ASSERT_THROW( - formula = storm::parser::CslParser::parseCslFormula(input), - storm::exceptions::WrongFormatException - ); -} - -TEST(CslParserTest, wrongFormulaTest) { - std::string input = "(a | b) & +"; - std::shared_ptr> formula(nullptr); - ASSERT_THROW( - formula = storm::parser::CslParser::parseCslFormula(input), - storm::exceptions::WrongFormatException - ); -} - -TEST(CslParserTest, wrongFormulaTest2) { - std::string input = "P>0 [ F & a ]"; - std::shared_ptr> formula(nullptr); - ASSERT_THROW( - formula = storm::parser::CslParser::parseCslFormula(input), - storm::exceptions::WrongFormatException - ); -} diff --git a/test/functional/parser/FormulaParserTest.cpp b/test/functional/parser/FormulaParserTest.cpp new file mode 100644 index 000000000..828a34f74 --- /dev/null +++ b/test/functional/parser/FormulaParserTest.cpp @@ -0,0 +1,235 @@ +#include "gtest/gtest.h" +#include "storm-config.h" +#include "src/parser/FormulaParser.h" +#include "src/exceptions/WrongFormatException.h" + +TEST(FormulaParserTest, parseLabelTest) { + std::string input = "\"label\""; + std::shared_ptr formula(nullptr); + ASSERT_NO_THROW(formula = storm::parser::FormulaParser::parseFromString(input)); + + EXPECT_TRUE(formula->isAtomicLabelFormula()); +} + +//TEST(PrctlParserTest, parsePropositionalFormulaTest) { +// std::string input = "!(a & b) | a & ! c"; +// std::shared_ptr> formula(nullptr); +// ASSERT_NO_THROW( +// formula = storm::parser::PrctlParser::parsePrctlFormula(input) +// ); +// +// // The parser did not falsely recognize the input as a comment. +// ASSERT_NE(formula.get(), nullptr); +// +// ASSERT_TRUE(formula->getChild()->isPropositional()); +// ASSERT_FALSE(formula->getChild()->isProbEventuallyAP()); +// +// // The input was parsed correctly. +// ASSERT_EQ("(!(a & b) | (a & !c))", formula->toString()); +//} +// +//TEST(PrctlParserTest, parsePathFormulaTest) { +// std::string input = "X( P<0.9 (a U b))"; +// std::shared_ptr> formula(nullptr); +// ASSERT_NO_THROW( +// formula = storm::parser::PrctlParser::parsePrctlFormula(input) +// ); +// +// // The parser did not falsely recognize the input as a comment. +// ASSERT_NE(formula.get(), nullptr); +// +// // The input was parsed correctly. +// ASSERT_NE(std::dynamic_pointer_cast>(formula->getChild()).get(), nullptr); +// auto nextFormula = std::dynamic_pointer_cast>(formula->getChild()); +// ASSERT_FALSE(nextFormula->isPropositional()); +// ASSERT_FALSE(nextFormula->isProbEventuallyAP()); +// +// ASSERT_NE(std::dynamic_pointer_cast>(nextFormula->getChild()).get(), nullptr); +// auto probBoundFormula = std::dynamic_pointer_cast>(nextFormula->getChild()); +// ASSERT_EQ(0.9, probBoundFormula->getBound()); +// ASSERT_EQ(storm::properties::LESS, probBoundFormula->getComparisonOperator()); +// ASSERT_FALSE(probBoundFormula->isPropositional()); +// ASSERT_TRUE(probBoundFormula->isProbEventuallyAP()); +// +// ASSERT_NE(std::dynamic_pointer_cast>(probBoundFormula->getChild()).get(), nullptr); +// auto untilFormula = std::dynamic_pointer_cast>(probBoundFormula->getChild()); +// ASSERT_FALSE(untilFormula->isPropositional()); +// ASSERT_FALSE(untilFormula->isProbEventuallyAP()); +// +// ASSERT_NE(std::dynamic_pointer_cast>(untilFormula->getLeft()).get(), nullptr); +// ASSERT_NE(std::dynamic_pointer_cast>(untilFormula->getRight()).get(), nullptr); +// ASSERT_EQ("a", std::dynamic_pointer_cast>(untilFormula->getLeft())->getAp()); +// ASSERT_EQ("b", std::dynamic_pointer_cast>(untilFormula->getRight())->getAp()); +// +// // The string representation is also correct. +// ASSERT_EQ("P = ? (X P < 0.900000 (a U b))", formula->toString()); +//} +// +//TEST(PrctlParserTest, parseProbabilisticFormulaTest) { +// std::string input = "P > 0.5 [ F a ]"; +// std::shared_ptr> formula(nullptr); +// ASSERT_NO_THROW( +// formula = storm::parser::PrctlParser::parsePrctlFormula(input) +// ); +// +// // The parser did not falsely recognize the input as a comment. +// ASSERT_NE(formula.get(), nullptr); +// +// +// ASSERT_NE(std::dynamic_pointer_cast>(formula->getChild()).get(), nullptr); +// std::shared_ptr> op = std::static_pointer_cast>(formula->getChild()); +// +// ASSERT_EQ(storm::properties::GREATER, op->getComparisonOperator()); +// ASSERT_EQ(0.5, op->getBound()); +// ASSERT_FALSE(op->isPropositional()); +// ASSERT_TRUE(op->isProbEventuallyAP()); +// +// // Test the string representation for the parsed formula. +// ASSERT_EQ("P > 0.500000 (F a)", formula->toString()); +//} +// +//TEST(PrctlParserTest, parseRewardFormulaTest) { +// std::string input = "R >= 15 [ I=5 ]"; +// std::shared_ptr>formula(nullptr); +// ASSERT_NO_THROW( +// formula = storm::parser::PrctlParser::parsePrctlFormula(input); +// ); +// +// // The parser did not falsely recognize the input as a comment. +// ASSERT_NE(formula.get(), nullptr); +// +// ASSERT_NE(std::dynamic_pointer_cast>(formula->getChild()).get(), nullptr); +// std::shared_ptr> op = std::static_pointer_cast>(formula->getChild()); +// +// ASSERT_EQ(storm::properties::GREATER_EQUAL, op->getComparisonOperator()); +// ASSERT_EQ(15.0, op->getBound()); +// ASSERT_FALSE(op->isPropositional()); +// ASSERT_FALSE(op->isProbEventuallyAP()); +// +// // Test the string representation for the parsed formula. +// ASSERT_EQ("R >= 15.000000 (I=5)", formula->toString()); +//} +// +//TEST(PrctlParserTest, parseRewardNoBoundFormulaTest) { +// std::string input = "R = ? [ F a ]"; +// std::shared_ptr> formula(nullptr); +// ASSERT_NO_THROW( +// formula = storm::parser::PrctlParser::parsePrctlFormula(input) +// ); +// +// // The parser did not falsely recognize the input as a comment. +// ASSERT_NE(formula.get(), nullptr); +// +// ASSERT_FALSE(formula->getChild()->isPropositional()); +// ASSERT_FALSE(formula->getChild()->isProbEventuallyAP()); +// +// // The input was parsed correctly. +// ASSERT_EQ("R = ? (F a)", formula->toString()); +//} +// +//TEST(PrctlParserTest, parseProbabilisticNoBoundFormulaTest) { +// std::string input = "P = ? [ a U <= 4 b & (!c) ]"; +// std::shared_ptr> formula(nullptr); +// ASSERT_NO_THROW( +// formula = storm::parser::PrctlParser::parsePrctlFormula(input) +// ); +// +// // The parser did not falsely recognize the input as a comment. +// ASSERT_NE(formula.get(), nullptr); +// +// ASSERT_FALSE(formula->getChild()->isPropositional()); +// ASSERT_FALSE(formula->getChild()->isProbEventuallyAP()); +// +// // The input was parsed correctly. +// ASSERT_EQ("P = ? (a U<=4 (b & !c))", formula->toString()); +//} +// +//TEST(PrctlParserTest, parseComplexFormulaTest) { +// std::string input = "R<=0.5 [ S ] & (R > 15 [ C<=0.5 ] | !P < 0.4 [ G P>0.9 [F<=7 a & b] ])"; +// std::shared_ptr> formula(nullptr); +// ASSERT_NO_THROW( +// formula = storm::parser::PrctlParser::parsePrctlFormula(input) +// ); +// +// // The parser did not falsely recognize the input as a comment. +// ASSERT_NE(formula.get(), nullptr); +// +// ASSERT_FALSE(formula->getChild()->isPropositional()); +// ASSERT_FALSE(formula->getChild()->isProbEventuallyAP()); +// +// // The input was parsed correctly. +// ASSERT_EQ("(R <= 0.500000 (S) & (R > 15.000000 (C <= 0.500000) | !P < 0.400000 (G P > 0.900000 (F<=7 (a & b)))))", formula->toString()); +//} +// +//TEST(PrctlParserTest, parsePrctlFilterTest) { +// std::string input = "filter[max; formula(b); invert; bound(<, 0.5); sort(value); range(0,3)](F a)"; +// std::shared_ptr> formula(nullptr); +// ASSERT_NO_THROW( +// formula = storm::parser::PrctlParser::parsePrctlFormula(input) +// ); +// +// // The parser did not falsely recognize the input as a comment. +// ASSERT_NE(formula.get(), nullptr); +// +// ASSERT_EQ(storm::properties::MAXIMIZE, formula->getOptimizingOperator()); +// +// ASSERT_EQ(5, formula->getActionCount()); +// ASSERT_NE(std::dynamic_pointer_cast>(formula->getAction(0)).get(), nullptr); +// ASSERT_NE(std::dynamic_pointer_cast>(formula->getAction(1)).get(), nullptr); +// ASSERT_NE(std::dynamic_pointer_cast>(formula->getAction(2)).get(), nullptr); +// ASSERT_NE(std::dynamic_pointer_cast>(formula->getAction(3)).get(), nullptr); +// ASSERT_NE(std::dynamic_pointer_cast>(formula->getAction(4)).get(), nullptr); +// +// ASSERT_FALSE(formula->getChild()->isPropositional()); +// ASSERT_FALSE(formula->getChild()->isProbEventuallyAP()); +// +// // The input was parsed correctly. +// ASSERT_EQ("filter[max; formula(b); invert; bound(<, 0.500000); sort(value, ascending); range(0, 3)](F a)", formula->toString()); +//} +// +//TEST(PrctlParserTest, commentTest) { +// std::string input = "// This is a comment. And this is a commented out formula: P<=0.5 [ X a ]"; +// std::shared_ptr> formula(nullptr); +// ASSERT_NO_THROW( +// formula = storm::parser::PrctlParser::parsePrctlFormula(input) +// ); +// +// // The parser recognized the input as a comment. +// ASSERT_NE(nullptr, formula.get()); +// +// // Test if the parser recognizes the comment at the end of a line. +// input = "P<=0.5 [ X a ] // This is a comment."; +// ASSERT_NO_THROW( +// formula = storm::parser::PrctlParser::parsePrctlFormula(input) +// ); +// +// ASSERT_FALSE(formula->getChild()->isPropositional()); +// ASSERT_FALSE(formula->getChild()->isProbEventuallyAP()); +// +// ASSERT_EQ("P <= 0.500000 (X a)", formula->toString()); +//} +// +// +//TEST(PrctlParserTest, wrongProbabilisticFormulaTest) { +// std::shared_ptr> formula(nullptr); +// ASSERT_THROW( +// formula = storm::parser::PrctlParser::parsePrctlFormula("P > 0.5 [ a ]"), +// storm::exceptions::WrongFormatException +// ); +//} +// +//TEST(PrctlParserTest, wrongFormulaTest) { +// std::shared_ptr> formula(nullptr); +// ASSERT_THROW( +// formula = storm::parser::PrctlParser::parsePrctlFormula("(a | b) & +"), +// storm::exceptions::WrongFormatException +// ); +//} +// +//TEST(PrctlParserTest, wrongFormulaTest2) { +// std::shared_ptr> formula(nullptr); +// ASSERT_THROW( +// formula = storm::parser::PrctlParser::parsePrctlFormula("P>0 [ F & a ]"), +// storm::exceptions::WrongFormatException +// ); +//} diff --git a/test/functional/parser/LtlParserTest.cpp b/test/functional/parser/LtlParserTest.cpp deleted file mode 100644 index d13c48688..000000000 --- a/test/functional/parser/LtlParserTest.cpp +++ /dev/null @@ -1,191 +0,0 @@ -/* - * LtlParserTest.cpp - * - * Created on: 22.04.2013 - * Author: thomas - */ - -#include "gtest/gtest.h" -#include "storm-config.h" -#include "src/parser/LtlParser.h" -#include "src/exceptions/WrongFormatException.h" -#include "src/properties/actions/InvertAction.h" -#include "src/properties/actions/SortAction.h" -#include "src/properties/actions/RangeAction.h" -#include "src/properties/actions/BoundAction.h" - -namespace ltl = storm::properties::ltl; - -TEST(LtlParserTest, parseApOnlyTest) { - std::string input = "ap"; - std::shared_ptr> formula(nullptr); - ASSERT_NO_THROW( - formula = storm::parser::LtlParser::parseLtlFormula(input); - ); - - ASSERT_TRUE(formula->getChild()->isPropositional()); - - ASSERT_NE(formula.get(), nullptr); - ASSERT_EQ(input, formula->toString()); -} - -TEST(LtlParserTest, parsePropositionalFormulaTest) { - std::string input = "!(a & b) | a & ! c"; - std::shared_ptr> formula(nullptr); - ASSERT_NO_THROW( - formula = storm::parser::LtlParser::parseLtlFormula(input); - ); - - ASSERT_TRUE(formula->getChild()->isPropositional()); - - ASSERT_NE(formula.get(), nullptr); - ASSERT_EQ("(!(a & b) | (a & !c))", formula->toString()); -} - -/*! - * The following test checks whether in the formula "F & b", F is correctly interpreted as proposition instead of the - * "Eventually" operator. - */ -TEST(LtlParserTest, parseAmbiguousFormulaTest) { - std::string input = "F & b"; - std::shared_ptr> formula(nullptr); - ASSERT_NO_THROW( - formula = storm::parser::LtlParser::parseLtlFormula(input); - ); - - ASSERT_TRUE(formula->getChild()->isPropositional()); - - ASSERT_NE(formula.get(), nullptr); - ASSERT_EQ("(F & b)", formula->toString()); -} - -/*! - * The following test checks whether in the formula "F F", F is interpreted as "eventually" operator or atomic proposition, - * depending where it occurs. - */ -TEST(LtlParserTest, parseAmbiguousFormulaTest2) { - std::string input = "F F"; - std::shared_ptr> formula(nullptr); - ASSERT_NO_THROW( - formula = storm::parser::LtlParser::parseLtlFormula(input); - ); - - ASSERT_FALSE(formula->getChild()->isPropositional()); - - ASSERT_NE(formula.get(), nullptr); - ASSERT_EQ("F F", formula->toString()); -} - -TEST(LtlParserTest, parseBoundedEventuallyFormulaTest) { - std::string input = "F<=5 a"; - std::shared_ptr> formula(nullptr); - ASSERT_NO_THROW( - formula = storm::parser::LtlParser::parseLtlFormula(input); - ); - - ASSERT_NE(formula.get(), nullptr); - - ASSERT_FALSE(formula->getChild()->isPropositional()); - - std::shared_ptr> op = std::dynamic_pointer_cast>(formula->getChild()); - ASSERT_NE(op.get(), nullptr); - ASSERT_EQ(static_cast(5), op->getBound()); - - - ASSERT_EQ("F<=5 a", formula->toString()); -} - -TEST(LtlParserTest, parseBoundedUntilFormulaTest) { - std::string input = "a U<=3 b"; - std::shared_ptr> formula(nullptr); - ASSERT_NO_THROW( - formula = storm::parser::LtlParser::parseLtlFormula(input); - ); - - ASSERT_NE(formula.get(), nullptr); - - ASSERT_FALSE(formula->getChild()->isPropositional()); - - std::shared_ptr> op = std::dynamic_pointer_cast>(formula->getChild()); - ASSERT_NE(op.get(), nullptr); - ASSERT_EQ(static_cast(3), op->getBound()); - - - ASSERT_EQ("(a U<=3 b)", formula->toString()); -} - -TEST(LtlParserTest, parseLtlFilterTest) { - std::string input = "filter[max; invert; bound(<, 0.5); sort(value); range(0,3)](X a)"; - std::shared_ptr> formula(nullptr); - ASSERT_NO_THROW( - formula = storm::parser::LtlParser::parseLtlFormula(input) - ); - - // The parser did not falsely recognize the input as a comment. - ASSERT_NE(formula, nullptr); - - ASSERT_FALSE(formula->getChild()->isPropositional()); - - ASSERT_EQ(storm::properties::MAXIMIZE, formula->getOptimizingOperator()); - - ASSERT_EQ(4, formula->getActionCount()); - ASSERT_NE(std::dynamic_pointer_cast>(formula->getAction(0)).get(), nullptr); - ASSERT_NE(std::dynamic_pointer_cast>(formula->getAction(1)).get(), nullptr); - ASSERT_NE(std::dynamic_pointer_cast>(formula->getAction(2)).get(), nullptr); - ASSERT_NE(std::dynamic_pointer_cast>(formula->getAction(3)).get(), nullptr); - - // The input was parsed correctly. - ASSERT_EQ("filter[max; invert; bound(<, 0.500000); sort(value, ascending); range(0, 3)](X a)", formula->toString()); -} - -TEST(LtlParserTest, commentTest) { - std::string input = "// This is a comment. And this is a commented out formula: F X a"; - std::shared_ptr> formula(nullptr); - ASSERT_NO_THROW( - formula = storm::parser::LtlParser::parseLtlFormula(input) - ); - - // The parser recognized the input as a comment. - ASSERT_NE(nullptr, formula.get()); - ASSERT_EQ(nullptr, formula->getChild().get()); - - // Test if the parser recognizes the comment at the end of a line. - input = "F X a // This is a comment."; - ASSERT_NO_THROW( - formula = storm::parser::LtlParser::parseLtlFormula(input) - ); - - ASSERT_FALSE(formula->getChild()->isPropositional()); - - ASSERT_EQ("F X a", formula->toString()); -} - -TEST(LtlParserTest, parseComplexUntilTest) { - std::string input = "a U b U<=3 c"; - std::shared_ptr> formula(nullptr); - ASSERT_NO_THROW( - formula = storm::parser::LtlParser::parseLtlFormula(input); - ); - - ASSERT_NE(formula.get(), nullptr); - ASSERT_EQ("((a U b) U<=3 c)", formula->toString()); -} - -TEST(LtlParserTest, parseComplexFormulaTest) { - std::string input = "a U F b | G a & F<=3 a U<=7 b // and a comment"; - std::shared_ptr> formula(nullptr); - ASSERT_NO_THROW( - formula = storm::parser::LtlParser::parseLtlFormula(input); - ); - - ASSERT_NE(formula.get(), nullptr); - ASSERT_EQ("(a U F (b | G (a & F<=3 (a U<=7 b))))", formula->toString()); -} - -TEST(LtlParserTest, wrongFormulaTest) { - std::string input = "(a | c) & +"; - ASSERT_THROW( - storm::parser::LtlParser::parseLtlFormula(input), - storm::exceptions::WrongFormatException - ); -} diff --git a/test/functional/parser/PrctlParserTest.cpp b/test/functional/parser/PrctlParserTest.cpp deleted file mode 100644 index 22e52e7d1..000000000 --- a/test/functional/parser/PrctlParserTest.cpp +++ /dev/null @@ -1,259 +0,0 @@ -/* - * PrctlParserTest.cpp - * - * Created on: 01.02.2013 - * Author: Thomas Heinemann - */ - - -#include "gtest/gtest.h" -#include "storm-config.h" -#include "src/parser/PrctlParser.h" -#include "src/exceptions/WrongFormatException.h" -#include "src/properties/actions/FormulaAction.h" -#include "src/properties/actions/InvertAction.h" -#include "src/properties/actions/SortAction.h" -#include "src/properties/actions/RangeAction.h" -#include "src/properties/actions/BoundAction.h" - -namespace prctl = storm::properties::prctl; - -TEST(PrctlParserTest, parseApOnlyTest) { - std::string input = "ap"; - std::shared_ptr> formula(nullptr); - ASSERT_NO_THROW( - formula = storm::parser::PrctlParser::parsePrctlFormula(input) - ); - - // The parser did not falsely recognize the input as a comment. - ASSERT_NE(formula.get(), nullptr); - - ASSERT_TRUE(formula->getChild()->isPropositional()); - ASSERT_FALSE(formula->getChild()->isProbEventuallyAP()); - - // The input was parsed correctly. - ASSERT_EQ(input, formula->toString()); -} - -TEST(PrctlParserTest, parsePropositionalFormulaTest) { - std::string input = "!(a & b) | a & ! c"; - std::shared_ptr> formula(nullptr); - ASSERT_NO_THROW( - formula = storm::parser::PrctlParser::parsePrctlFormula(input) - ); - - // The parser did not falsely recognize the input as a comment. - ASSERT_NE(formula.get(), nullptr); - - ASSERT_TRUE(formula->getChild()->isPropositional()); - ASSERT_FALSE(formula->getChild()->isProbEventuallyAP()); - - // The input was parsed correctly. - ASSERT_EQ("(!(a & b) | (a & !c))", formula->toString()); -} - -TEST(PrctlParserTest, parsePathFormulaTest) { - std::string input = "X( P<0.9 (a U b))"; - std::shared_ptr> formula(nullptr); - ASSERT_NO_THROW( - formula = storm::parser::PrctlParser::parsePrctlFormula(input) - ); - - // The parser did not falsely recognize the input as a comment. - ASSERT_NE(formula.get(), nullptr); - - // The input was parsed correctly. - ASSERT_NE(std::dynamic_pointer_cast>(formula->getChild()).get(), nullptr); - auto nextFormula = std::dynamic_pointer_cast>(formula->getChild()); - ASSERT_FALSE(nextFormula->isPropositional()); - ASSERT_FALSE(nextFormula->isProbEventuallyAP()); - - ASSERT_NE(std::dynamic_pointer_cast>(nextFormula->getChild()).get(), nullptr); - auto probBoundFormula = std::dynamic_pointer_cast>(nextFormula->getChild()); - ASSERT_EQ(0.9, probBoundFormula->getBound()); - ASSERT_EQ(storm::properties::LESS, probBoundFormula->getComparisonOperator()); - ASSERT_FALSE(probBoundFormula->isPropositional()); - ASSERT_TRUE(probBoundFormula->isProbEventuallyAP()); - - ASSERT_NE(std::dynamic_pointer_cast>(probBoundFormula->getChild()).get(), nullptr); - auto untilFormula = std::dynamic_pointer_cast>(probBoundFormula->getChild()); - ASSERT_FALSE(untilFormula->isPropositional()); - ASSERT_FALSE(untilFormula->isProbEventuallyAP()); - - ASSERT_NE(std::dynamic_pointer_cast>(untilFormula->getLeft()).get(), nullptr); - ASSERT_NE(std::dynamic_pointer_cast>(untilFormula->getRight()).get(), nullptr); - ASSERT_EQ("a", std::dynamic_pointer_cast>(untilFormula->getLeft())->getAp()); - ASSERT_EQ("b", std::dynamic_pointer_cast>(untilFormula->getRight())->getAp()); - - // The string representation is also correct. - ASSERT_EQ("P = ? (X P < 0.900000 (a U b))", formula->toString()); -} - -TEST(PrctlParserTest, parseProbabilisticFormulaTest) { - std::string input = "P > 0.5 [ F a ]"; - std::shared_ptr> formula(nullptr); - ASSERT_NO_THROW( - formula = storm::parser::PrctlParser::parsePrctlFormula(input) - ); - - // The parser did not falsely recognize the input as a comment. - ASSERT_NE(formula.get(), nullptr); - - - ASSERT_NE(std::dynamic_pointer_cast>(formula->getChild()).get(), nullptr); - std::shared_ptr> op = std::static_pointer_cast>(formula->getChild()); - - ASSERT_EQ(storm::properties::GREATER, op->getComparisonOperator()); - ASSERT_EQ(0.5, op->getBound()); - ASSERT_FALSE(op->isPropositional()); - ASSERT_TRUE(op->isProbEventuallyAP()); - - // Test the string representation for the parsed formula. - ASSERT_EQ("P > 0.500000 (F a)", formula->toString()); -} - -TEST(PrctlParserTest, parseRewardFormulaTest) { - std::string input = "R >= 15 [ I=5 ]"; - std::shared_ptr>formula(nullptr); - ASSERT_NO_THROW( - formula = storm::parser::PrctlParser::parsePrctlFormula(input); - ); - - // The parser did not falsely recognize the input as a comment. - ASSERT_NE(formula.get(), nullptr); - - ASSERT_NE(std::dynamic_pointer_cast>(formula->getChild()).get(), nullptr); - std::shared_ptr> op = std::static_pointer_cast>(formula->getChild()); - - ASSERT_EQ(storm::properties::GREATER_EQUAL, op->getComparisonOperator()); - ASSERT_EQ(15.0, op->getBound()); - ASSERT_FALSE(op->isPropositional()); - ASSERT_FALSE(op->isProbEventuallyAP()); - - // Test the string representation for the parsed formula. - ASSERT_EQ("R >= 15.000000 (I=5)", formula->toString()); -} - -TEST(PrctlParserTest, parseRewardNoBoundFormulaTest) { - std::string input = "R = ? [ F a ]"; - std::shared_ptr> formula(nullptr); - ASSERT_NO_THROW( - formula = storm::parser::PrctlParser::parsePrctlFormula(input) - ); - - // The parser did not falsely recognize the input as a comment. - ASSERT_NE(formula.get(), nullptr); - - ASSERT_FALSE(formula->getChild()->isPropositional()); - ASSERT_FALSE(formula->getChild()->isProbEventuallyAP()); - - // The input was parsed correctly. - ASSERT_EQ("R = ? (F a)", formula->toString()); -} - -TEST(PrctlParserTest, parseProbabilisticNoBoundFormulaTest) { - std::string input = "P = ? [ a U <= 4 b & (!c) ]"; - std::shared_ptr> formula(nullptr); - ASSERT_NO_THROW( - formula = storm::parser::PrctlParser::parsePrctlFormula(input) - ); - - // The parser did not falsely recognize the input as a comment. - ASSERT_NE(formula.get(), nullptr); - - ASSERT_FALSE(formula->getChild()->isPropositional()); - ASSERT_FALSE(formula->getChild()->isProbEventuallyAP()); - - // The input was parsed correctly. - ASSERT_EQ("P = ? (a U<=4 (b & !c))", formula->toString()); -} - -TEST(PrctlParserTest, parseComplexFormulaTest) { - std::string input = "R<=0.5 [ S ] & (R > 15 [ C<=0.5 ] | !P < 0.4 [ G P>0.9 [F<=7 a & b] ])"; - std::shared_ptr> formula(nullptr); - ASSERT_NO_THROW( - formula = storm::parser::PrctlParser::parsePrctlFormula(input) - ); - - // The parser did not falsely recognize the input as a comment. - ASSERT_NE(formula.get(), nullptr); - - ASSERT_FALSE(formula->getChild()->isPropositional()); - ASSERT_FALSE(formula->getChild()->isProbEventuallyAP()); - - // The input was parsed correctly. - ASSERT_EQ("(R <= 0.500000 (S) & (R > 15.000000 (C <= 0.500000) | !P < 0.400000 (G P > 0.900000 (F<=7 (a & b)))))", formula->toString()); -} - -TEST(PrctlParserTest, parsePrctlFilterTest) { - std::string input = "filter[max; formula(b); invert; bound(<, 0.5); sort(value); range(0,3)](F a)"; - std::shared_ptr> formula(nullptr); - ASSERT_NO_THROW( - formula = storm::parser::PrctlParser::parsePrctlFormula(input) - ); - - // The parser did not falsely recognize the input as a comment. - ASSERT_NE(formula.get(), nullptr); - - ASSERT_EQ(storm::properties::MAXIMIZE, formula->getOptimizingOperator()); - - ASSERT_EQ(5, formula->getActionCount()); - ASSERT_NE(std::dynamic_pointer_cast>(formula->getAction(0)).get(), nullptr); - ASSERT_NE(std::dynamic_pointer_cast>(formula->getAction(1)).get(), nullptr); - ASSERT_NE(std::dynamic_pointer_cast>(formula->getAction(2)).get(), nullptr); - ASSERT_NE(std::dynamic_pointer_cast>(formula->getAction(3)).get(), nullptr); - ASSERT_NE(std::dynamic_pointer_cast>(formula->getAction(4)).get(), nullptr); - - ASSERT_FALSE(formula->getChild()->isPropositional()); - ASSERT_FALSE(formula->getChild()->isProbEventuallyAP()); - - // The input was parsed correctly. - ASSERT_EQ("filter[max; formula(b); invert; bound(<, 0.500000); sort(value, ascending); range(0, 3)](F a)", formula->toString()); -} - -TEST(PrctlParserTest, commentTest) { - std::string input = "// This is a comment. And this is a commented out formula: P<=0.5 [ X a ]"; - std::shared_ptr> formula(nullptr); - ASSERT_NO_THROW( - formula = storm::parser::PrctlParser::parsePrctlFormula(input) - ); - - // The parser recognized the input as a comment. - ASSERT_NE(nullptr, formula.get()); - - // Test if the parser recognizes the comment at the end of a line. - input = "P<=0.5 [ X a ] // This is a comment."; - ASSERT_NO_THROW( - formula = storm::parser::PrctlParser::parsePrctlFormula(input) - ); - - ASSERT_FALSE(formula->getChild()->isPropositional()); - ASSERT_FALSE(formula->getChild()->isProbEventuallyAP()); - - ASSERT_EQ("P <= 0.500000 (X a)", formula->toString()); -} - - -TEST(PrctlParserTest, wrongProbabilisticFormulaTest) { - std::shared_ptr> formula(nullptr); - ASSERT_THROW( - formula = storm::parser::PrctlParser::parsePrctlFormula("P > 0.5 [ a ]"), - storm::exceptions::WrongFormatException - ); -} - -TEST(PrctlParserTest, wrongFormulaTest) { - std::shared_ptr> formula(nullptr); - ASSERT_THROW( - formula = storm::parser::PrctlParser::parsePrctlFormula("(a | b) & +"), - storm::exceptions::WrongFormatException - ); -} - -TEST(PrctlParserTest, wrongFormulaTest2) { - std::shared_ptr> formula(nullptr); - ASSERT_THROW( - formula = storm::parser::PrctlParser::parsePrctlFormula("P>0 [ F & a ]"), - storm::exceptions::WrongFormatException - ); -}