More work on logic classes.

Former-commit-id: 9d94e02b74

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})

src/properties/logic/AtomicExpressionFormula.cpp → 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;
         }

src/properties/logic/AtomicExpressionFormula.h → 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.
             }

src/properties/logic/AtomicLabelFormula.cpp → 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;
         }

src/properties/logic/AtomicLabelFormula.h → src/logic/AtomicLabelFormula.h

@@ -3,12 +3,14 @@
 
 #include <string>
 
-#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.
             }

src/properties/logic/BinaryBooleanStateFormula.cpp → 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<StateFormula> const& leftSubformula, std::shared_ptr<StateFormula> const& rightSubformula) : BinaryStateFormula(leftSubformula, rightSubformula), operatorType(operatorType) {
+        BinaryBooleanStateFormula::BinaryBooleanStateFormula(OperatorType operatorType, std::shared_ptr<Formula> const& leftSubformula, std::shared_ptr<Formula> const& rightSubformula) : BinaryStateFormula(leftSubformula, rightSubformula), operatorType(operatorType) {
             // Intentionally left empty.
         }
         

src/properties/logic/BinaryBooleanStateFormula.h → 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<StateFormula> const& leftSubformula, std::shared_ptr<StateFormula> const& rightSubformula);
+            BinaryBooleanStateFormula(OperatorType operatorType, std::shared_ptr<Formula> const& leftSubformula, std::shared_ptr<Formula> const& rightSubformula);
             
             virtual ~BinaryBooleanStateFormula() {
                 // Intentionally left empty.

src/properties/logic/BinaryPathFormula.cpp → src/logic/BinaryPathFormula.cpp

@@ -1,4 +1,4 @@
-#include "src/properties/logic/BinaryPathFormula.h"
+#include "src/logic/BinaryPathFormula.h"
 
 namespace storm {
     namespace logic {

src/properties/logic/BinaryPathFormula.h → src/logic/BinaryPathFormula.h

@@ -3,7 +3,7 @@
 
 #include <memory>
 
-#include "src/properties/logic/PathFormula.h"
+#include "src/logic/PathFormula.h"
 
 namespace storm {
     namespace logic {

src/properties/logic/BinaryStateFormula.cpp → src/logic/BinaryStateFormula.cpp

@@ -1,4 +1,4 @@
-#include "src/properties/logic/BinaryStateFormula.h"
+#include "src/logic/BinaryStateFormula.h"
 
 namespace storm {
     namespace logic {

src/properties/logic/BinaryStateFormula.h → 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 {

src/properties/logic/BooleanLiteralFormula.cpp → src/logic/BooleanLiteralFormula.cpp

@@ -1,4 +1,4 @@
-#include "src/properties/logic/BooleanLiteralFormula.h"
+#include "src/logic/BooleanLiteralFormula.h"
 
 namespace storm {
     namespace logic {

src/properties/logic/BooleanLiteralFormula.h → 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 {

src/properties/logic/BoundedUntilFormula.cpp → src/logic/BoundedUntilFormula.cpp

@@ -1,4 +1,4 @@
-#include "src/properties/logic/BoundedUntilFormula.h"
+#include "src/logic/BoundedUntilFormula.h"
 
 namespace storm {
     namespace logic {

src/properties/logic/BoundedUntilFormula.h → src/logic/BoundedUntilFormula.h

@@ -3,7 +3,7 @@
 
 #include <boost/variant.hpp>
 
-#include "src/properties/logic/BinaryPathFormula.h"
+#include "src/logic/BinaryPathFormula.h"
 
 namespace storm {
     namespace logic {

src/properties/logic/ComparisonType.cpp → src/logic/ComparisonType.cpp

@@ -1,4 +1,4 @@
-#include "src/properties/logic/ComparisonType.h"
+#include "src/logic/ComparisonType.h"
 
 namespace storm {
     namespace logic {

src/properties/logic/ConditionalPathFormula.cpp → 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;
         }

src/properties/logic/ConditionalPathFormula.h → 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 {

src/properties/logic/CumulativeRewardFormula.cpp → src/logic/CumulativeRewardFormula.cpp

@@ -1,4 +1,4 @@
-#include "src/properties/logic/CumulativeRewardFormula.h"
+#include "src/logic/CumulativeRewardFormula.h"
 
 namespace storm {
     namespace logic {

src/properties/logic/CumulativeRewardFormula.h → 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 {

src/properties/logic/EventuallyFormula.cpp → src/logic/EventuallyFormula.cpp

@@ -1,4 +1,4 @@
-#include "src/properties/logic/EventuallyFormula.h"
+#include "src/logic/EventuallyFormula.h"
 
 namespace storm {
     namespace logic {

src/properties/logic/EventuallyFormula.h → 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 {

src/properties/logic/Formula.cpp → 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<NextFormula const&>(*this);
         }
         
-        SteadyStateFormula& Formula::asSteadyStateFormula() {
-            return dynamic_cast<SteadyStateFormula&>(*this);
+        SteadyStateOperatorFormula& Formula::asSteadyStateFormula() {
+            return dynamic_cast<SteadyStateOperatorFormula&>(*this);
         }
         
-        SteadyStateFormula const& Formula::asSteadyStateFormula() const {
-            return dynamic_cast<SteadyStateFormula const&>(*this);
+        SteadyStateOperatorFormula const& Formula::asSteadyStateFormula() const {
+            return dynamic_cast<SteadyStateOperatorFormula const&>(*this);
         }
         
         PathRewardFormula& Formula::asPathRewardFormula() {

src/properties/logic/Formula.h → 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;

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"

src/properties/logic/GloballyFormula.cpp → src/logic/GloballyFormula.cpp

@@ -1,4 +1,4 @@
-#include "src/properties/logic/GloballyFormula.h"
+#include "src/logic/GloballyFormula.h"
 
 namespace storm {
     namespace logic {

src/properties/logic/GloballyFormula.h → 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 {

src/properties/logic/InstantaneousRewardFormula.cpp → src/logic/InstantaneousRewardFormula.cpp

@@ -1,4 +1,4 @@
-#include "src/properties/logic/InstantaneousRewardFormula.h"
+#include "src/logic/InstantaneousRewardFormula.h"
 
 namespace storm {
     namespace logic {

src/properties/logic/InstantaneousRewardFormula.h → 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 {

src/properties/logic/NextFormula.cpp → src/logic/NextFormula.cpp

@@ -1,4 +1,4 @@
-#include "src/properties/logic/NextFormula.h"
+#include "src/logic/NextFormula.h"
 
 namespace storm {
     namespace logic {

src/properties/logic/NextFormula.h → 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 {

src/properties/logic/OperatorFormula.cpp → 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> comparisonType, boost::optional<double> bound, boost::optional<OptimalityType> optimalityType, std::shared_ptr<Formula> const& subformula) : UnaryStateFormula(subformula), comparisonType(comparisonType), bound(bound), optimalityType(optimalityType) {
+        OperatorFormula::OperatorFormula(boost::optional<OptimalityType> optimalityType, boost::optional<ComparisonType> comparisonType, boost::optional<double> bound, std::shared_ptr<Formula> const& subformula) : UnaryStateFormula(subformula), comparisonType(comparisonType), bound(bound), optimalityType(optimalityType) {
             // Intentionally left empty.
         }
         

src/properties/logic/OperatorFormula.h → src/logic/OperatorFormula.h

@@ -3,15 +3,15 @@
 
 #include <boost/optional.hpp>
 
-#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> comparisonType, boost::optional<double> bound, boost::optional<OptimalityType> optimalityType, std::shared_ptr<Formula> const& subformula);
+            OperatorFormula(boost::optional<OptimalityType> optimalityType, boost::optional<ComparisonType> comparisonType, boost::optional<double> bound, std::shared_ptr<Formula> const& subformula);
             
             virtual ~OperatorFormula() {
                 // Intentionally left empty.

src/properties/logic/OptimalityType.cpp → src/logic/OptimalityType.cpp

@@ -1,4 +1,4 @@
-#include "src/properties/logic/OptimalityType.h"
+#include "src/logic/OptimalityType.h"
 
 namespace storm {
     namespace logic {

src/properties/logic/PathFormula.cpp → src/logic/PathFormula.cpp

@@ -1,4 +1,4 @@
-#include "src/properties/logic/PathFormula.h"
+#include "src/logic/PathFormula.h"
 
 namespace storm {
     namespace logic {

src/properties/logic/PathFormula.h → 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 {

src/properties/logic/PathRewardFormula.cpp → src/logic/PathRewardFormula.cpp

@@ -1,4 +1,4 @@
-#include "src/properties/logic/PathRewardFormula.h"
+#include "src/logic/PathRewardFormula.h"
 
 namespace storm {
     namespace logic {

src/properties/logic/PathRewardFormula.h → 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 {

src/properties/logic/ProbabilityOperatorFormula.cpp → 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<Formula> const& subformula) : ProbabilityOperatorFormula(boost::optional<ComparisonType>(), boost::optional<double>(), boost::optional<OptimalityType>(), subformula) {
+        ProbabilityOperatorFormula::ProbabilityOperatorFormula(std::shared_ptr<Formula> const& subformula) : ProbabilityOperatorFormula(boost::optional<OptimalityType>(), boost::optional<ComparisonType>(), boost::optional<double>(), subformula) {
             // Intentionally left empty.
         }
         
-        ProbabilityOperatorFormula::ProbabilityOperatorFormula(ComparisonType comparisonType, double bound, std::shared_ptr<Formula> const& subformula) : ProbabilityOperatorFormula(boost::optional<ComparisonType>(comparisonType), boost::optional<double>(bound), boost::optional<OptimalityType>(), subformula) {
+        ProbabilityOperatorFormula::ProbabilityOperatorFormula(ComparisonType comparisonType, double bound, std::shared_ptr<Formula> const& subformula) : ProbabilityOperatorFormula(boost::optional<OptimalityType>(), boost::optional<ComparisonType>(comparisonType), boost::optional<double>(bound), subformula) {
             // Intentionally left empty.
         }
         
-        ProbabilityOperatorFormula::ProbabilityOperatorFormula(ComparisonType comparisonType, double bound, OptimalityType optimalityType, std::shared_ptr<Formula> const& subformula) : ProbabilityOperatorFormula(boost::optional<ComparisonType>(comparisonType), boost::optional<double>(bound), boost::optional<OptimalityType>(optimalityType), subformula) {
+        ProbabilityOperatorFormula::ProbabilityOperatorFormula(OptimalityType optimalityType, ComparisonType comparisonType, double bound, std::shared_ptr<Formula> const& subformula) : ProbabilityOperatorFormula(boost::optional<OptimalityType>(optimalityType), boost::optional<ComparisonType>(comparisonType), boost::optional<double>(bound), subformula) {
             // Intentionally left empty.
         }
         
-        ProbabilityOperatorFormula::ProbabilityOperatorFormula(OptimalityType optimalityType, std::shared_ptr<Formula> const& subformula) : ProbabilityOperatorFormula(boost::optional<ComparisonType>(), boost::optional<double>(), boost::optional<OptimalityType>(optimalityType), subformula) {
+        ProbabilityOperatorFormula::ProbabilityOperatorFormula(OptimalityType optimalityType, std::shared_ptr<Formula> const& subformula) : ProbabilityOperatorFormula(boost::optional<OptimalityType>(optimalityType), boost::optional<ComparisonType>(), boost::optional<double>(), subformula) {
             // Intentionally left empty.
         }
         
@@ -22,7 +22,7 @@ namespace storm {
             return true;
         }
         
-        ProbabilityOperatorFormula::ProbabilityOperatorFormula(boost::optional<ComparisonType> comparisonType, boost::optional<double> bound, boost::optional<OptimalityType> optimalityType, std::shared_ptr<Formula> const& subformula) : OperatorFormula(comparisonType, bound, optimalityType, subformula) {
+        ProbabilityOperatorFormula::ProbabilityOperatorFormula(boost::optional<OptimalityType> optimalityType, boost::optional<ComparisonType> comparisonType, boost::optional<double> bound, std::shared_ptr<Formula> const& subformula) : OperatorFormula(optimalityType, comparisonType, bound, subformula) {
             // Intentionally left empty.
         }
         

src/properties/logic/ProbabilityOperatorFormula.h → 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<Formula> const& subformula);
             ProbabilityOperatorFormula(ComparisonType comparisonType, double bound, std::shared_ptr<Formula> const& subformula);
-            ProbabilityOperatorFormula(ComparisonType comparisonType, double bound, OptimalityType optimalityType, std::shared_ptr<Formula> const& subformula);
+            ProbabilityOperatorFormula(OptimalityType optimalityType, ComparisonType comparisonType, double bound, std::shared_ptr<Formula> const& subformula);
             ProbabilityOperatorFormula(OptimalityType optimalityType, std::shared_ptr<Formula> const& subformula);
-            
+            ProbabilityOperatorFormula(boost::optional<OptimalityType> optimalityType, boost::optional<ComparisonType> comparisonType, boost::optional<double> bound, std::shared_ptr<Formula> 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> comparisonType, boost::optional<double> bound, boost::optional<OptimalityType> optimalityType, std::shared_ptr<Formula> const& subformula);
         };
     }
 }

src/properties/logic/ReachabilityRewardFormula.cpp → 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<StateFormula> const& subformula) : subformula(subformula) {
+        ReachabilityRewardFormula::ReachabilityRewardFormula(std::shared_ptr<Formula> 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;
         }
         

src/properties/logic/ReachabilityRewardFormula.h → src/logic/ReachabilityRewardFormula.h

@@ -3,14 +3,14 @@
 
 #include <memory>
 
-#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<StateFormula> const& subformula);
+            ReachabilityRewardFormula(std::shared_ptr<Formula> 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<StateFormula> const& subformula;
+            std::shared_ptr<Formula> const& subformula;
         };
     }
 }

src/properties/logic/RewardOperatorFormula.cpp → 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<Formula> const& subformula) : RewardOperatorFormula(boost::optional<ComparisonType>(), boost::optional<double>(), boost::optional<OptimalityType>(), subformula) {
+        RewardOperatorFormula::RewardOperatorFormula(std::shared_ptr<Formula> const& subformula) : RewardOperatorFormula(boost::optional<OptimalityType>(), boost::optional<ComparisonType>(), boost::optional<double>(), subformula) {
             // Intentionally left empty.
         }
         
-        RewardOperatorFormula::RewardOperatorFormula(ComparisonType comparisonType, double bound, std::shared_ptr<Formula> const& subformula) : RewardOperatorFormula(boost::optional<ComparisonType>(comparisonType), boost::optional<double>(bound), boost::optional<OptimalityType>(), subformula) {
+        RewardOperatorFormula::RewardOperatorFormula(ComparisonType comparisonType, double bound, std::shared_ptr<Formula> const& subformula) : RewardOperatorFormula(boost::optional<OptimalityType>(), boost::optional<ComparisonType>(comparisonType), boost::optional<double>(bound), subformula) {
             // Intentionally left empty.
         }
         
-        RewardOperatorFormula::RewardOperatorFormula(ComparisonType comparisonType, double bound, OptimalityType optimalityType, std::shared_ptr<Formula> const& subformula) : RewardOperatorFormula(boost::optional<ComparisonType>(comparisonType), boost::optional<double>(bound), boost::optional<OptimalityType>(optimalityType), subformula) {
+        RewardOperatorFormula::RewardOperatorFormula(OptimalityType optimalityType, ComparisonType comparisonType, double bound, std::shared_ptr<Formula> const& subformula) : RewardOperatorFormula(boost::optional<OptimalityType>(optimalityType), boost::optional<ComparisonType>(comparisonType), boost::optional<double>(bound), subformula) {
             // Intentionally left empty.
         }
         
-        RewardOperatorFormula::RewardOperatorFormula(OptimalityType optimalityType, std::shared_ptr<Formula> const& subformula) : RewardOperatorFormula(boost::optional<ComparisonType>(), boost::optional<double>(), boost::optional<OptimalityType>(optimalityType), subformula) {
+        RewardOperatorFormula::RewardOperatorFormula(OptimalityType optimalityType, std::shared_ptr<Formula> const& subformula) : RewardOperatorFormula(boost::optional<OptimalityType>(optimalityType), boost::optional<ComparisonType>(), boost::optional<double>(), subformula) {
             // Intentionally left empty.
         }
         
@@ -22,7 +22,7 @@ namespace storm {
             return true;
         }
         
-        RewardOperatorFormula::RewardOperatorFormula(boost::optional<ComparisonType> comparisonType, boost::optional<double> bound, boost::optional<OptimalityType> optimalityType, std::shared_ptr<Formula> const& subformula) : OperatorFormula(comparisonType, bound, optimalityType, subformula) {
+        RewardOperatorFormula::RewardOperatorFormula(boost::optional<OptimalityType> optimalityType, boost::optional<ComparisonType> comparisonType, boost::optional<double> bound, std::shared_ptr<Formula> const& subformula) : OperatorFormula(optimalityType, comparisonType, bound, subformula) {
             // Intentionally left empty.
         }
         

src/properties/logic/RewardOperatorFormula.h → 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<Formula> const& subformula);
             RewardOperatorFormula(ComparisonType comparisonType, double bound, std::shared_ptr<Formula> const& subformula);
-            RewardOperatorFormula(ComparisonType comparisonType, double bound, OptimalityType optimalityType, std::shared_ptr<Formula> const& subformula);
+            RewardOperatorFormula(OptimalityType optimalityType, ComparisonType comparisonType, double bound, std::shared_ptr<Formula> const& subformula);
             RewardOperatorFormula(OptimalityType optimalityType, std::shared_ptr<Formula> const& subformula);
-            
+            RewardOperatorFormula(boost::optional<OptimalityType> optimalityType, boost::optional<ComparisonType> comparisonType, boost::optional<double> bound, std::shared_ptr<Formula> 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> comparisonType, boost::optional<double> bound, boost::optional<OptimalityType> optimalityType, std::shared_ptr<Formula> const& subformula);
         };
     }
 }

src/properties/logic/StateFormula.cpp → src/logic/StateFormula.cpp

@@ -1,4 +1,4 @@
-#include "src/properties/logic/StateFormula.h"
+#include "src/logic/StateFormula.h"
 
 namespace storm {
     namespace logic {

src/properties/logic/StateFormula.h → 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 {

src/logic/SteadyStateOperatorFormula.cpp

@@ -0,0 +1,35 @@
+#include "src/logic/SteadyStateOperatorFormula.h"
+
+namespace storm {
+    namespace logic {
+        SteadyStateOperatorFormula::SteadyStateOperatorFormula(std::shared_ptr<Formula> const& subformula) : SteadyStateOperatorFormula(boost::optional<OptimalityType>(), boost::optional<ComparisonType>(), boost::optional<double>(), subformula) {
+            // Intentionally left empty.
+        }
+        
+        SteadyStateOperatorFormula::SteadyStateOperatorFormula(ComparisonType comparisonType, double bound, std::shared_ptr<Formula> const& subformula) : SteadyStateOperatorFormula(boost::optional<OptimalityType>(), boost::optional<ComparisonType>(comparisonType), boost::optional<double>(bound), subformula) {
+            // Intentionally left empty.
+        }
+        
+        SteadyStateOperatorFormula::SteadyStateOperatorFormula(OptimalityType optimalityType, ComparisonType comparisonType, double bound, std::shared_ptr<Formula> const& subformula) : SteadyStateOperatorFormula(boost::optional<OptimalityType>(optimalityType), boost::optional<ComparisonType>(comparisonType), boost::optional<double>(bound), subformula) {
+            // Intentionally left empty.
+        }
+        
+        SteadyStateOperatorFormula::SteadyStateOperatorFormula(OptimalityType optimalityType, std::shared_ptr<Formula> const& subformula) : SteadyStateOperatorFormula(boost::optional<OptimalityType>(optimalityType), boost::optional<ComparisonType>(), boost::optional<double>(), subformula) {
+            // Intentionally left empty.
+        }
+                
+        bool SteadyStateOperatorFormula::isSteadyStateOperatorFormula() const {
+            return true;
+        }
+        
+        SteadyStateOperatorFormula::SteadyStateOperatorFormula(boost::optional<OptimalityType> optimalityType, boost::optional<ComparisonType> comparisonType, boost::optional<double> bound, std::shared_ptr<Formula> 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;
+        }
+    }
+}

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<Formula> const& subformula);
+            SteadyStateOperatorFormula(ComparisonType comparisonType, double bound, std::shared_ptr<Formula> const& subformula);
+            SteadyStateOperatorFormula(OptimalityType optimalityType, ComparisonType comparisonType, double bound, std::shared_ptr<Formula> const& subformula);
+            SteadyStateOperatorFormula(OptimalityType optimalityType, std::shared_ptr<Formula> const& subformula);
+            SteadyStateOperatorFormula(boost::optional<OptimalityType> optimalityType, boost::optional<ComparisonType> comparisonType, boost::optional<double> bound, std::shared_ptr<Formula> 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_ */

src/properties/logic/UnaryBooleanStateFormula.cpp → src/logic/UnaryBooleanStateFormula.cpp

@@ -1,4 +1,4 @@
-#include "src/properties/logic/UnaryBooleanStateFormula.h"
+#include "src/logic/UnaryBooleanStateFormula.h"
 
 namespace storm {
     namespace logic {

src/properties/logic/UnaryBooleanStateFormula.h → 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 {

src/properties/logic/UnaryPathFormula.cpp → src/logic/UnaryPathFormula.cpp

@@ -1,4 +1,4 @@
-#include "src/properties/logic/UnaryPathFormula.h"
+#include "src/logic/UnaryPathFormula.h"
 
 namespace storm {
     namespace logic {

src/properties/logic/UnaryPathFormula.h → src/logic/UnaryPathFormula.h

@@ -3,7 +3,7 @@
 
 #include <memory>
 
-#include "src/properties/logic/PathFormula.h"
+#include "src/logic/PathFormula.h"
 
 namespace storm {
     namespace logic {

src/properties/logic/UnaryStateFormula.cpp → src/logic/UnaryStateFormula.cpp

@@ -1,4 +1,4 @@
-#include "src/properties/logic/UnaryStateFormula.h"
+#include "src/logic/UnaryStateFormula.h"
 
 namespace storm {
     namespace logic {

src/properties/logic/UnaryStateFormula.h → 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 {

src/properties/logic/UntilFormula.cpp → src/logic/UntilFormula.cpp

@@ -1,4 +1,4 @@
-#include "src/properties/logic/UntilFormula.h"
+#include "src/logic/UntilFormula.h"
 
 namespace storm {
     namespace logic {

src/properties/logic/UntilFormula.h → 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 {

src/parser/CslParser.cpp

@@ -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 <boost/typeof/typeof.hpp>
-#include <boost/spirit/include/qi.hpp>
-#include <boost/spirit/include/phoenix.hpp>
-
-// Include headers for spirit iterators. Needed for diagnostics and input stream iteration.
-#include <boost/spirit/include/classic_position_iterator.hpp>
-#include <boost/spirit/include/support_multi_pass.hpp>
-
-// Needed for file IO.
-#include <fstream>
-#include <iomanip>
-#include <map>
-
-
-// Some typedefs and namespace definitions to reduce code size.
-#define MAKE(Type, ...) phoenix::construct<std::shared_ptr<Type>>(phoenix::new_<Type>(__VA_ARGS__))
-typedef std::string::const_iterator BaseIteratorType;
-typedef boost::spirit::classic::position_iterator2<BaseIteratorType> PositionIteratorType;
-namespace qi = boost::spirit::qi;
-namespace phoenix = boost::phoenix;
-namespace csl = storm::properties::csl;
-
-namespace storm {
-namespace parser {
-
-template<typename Iterator, typename Skipper>
-struct CslParser::CslGrammar : qi::grammar<Iterator, std::shared_ptr<csl::CslFilter<double>>(), 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<double>::INDEX] |
-				(qi::lit("value"))[qi::_val = storm::properties::action::SortAction<double>::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<double>, qi::_val, qi::_1)];
-		orFormula.name("or formula");
-		andFormula = notFormula[qi::_val = qi::_1] > *(qi::lit("&") > notFormula)[qi::_val =
-				MAKE(csl::And<double>, qi::_val, qi::_1)];
-		andFormula.name("and formula");
-		notFormula = atomicStateFormula[qi::_val = qi::_1] | (qi::lit("!") > atomicStateFormula)[qi::_val =
-				MAKE(csl::Not<double>, 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<double>, qi::_1)] | (qi::lit("\"") > (freeIdentifierName)[qi::_val = MAKE(csl::Ap<double>, qi::_1)] > qi::lit("\""));
-		atomicProposition.name("atomic proposition");
-		probabilisticBoundOperator = (
-				(qi::lit("P") >> comparisonType > qi::double_ > pathFormula )[qi::_val =
-						MAKE(csl::ProbabilisticBoundOperator<double> , qi::_1, qi::_2, qi::_3)]
-				);
-		probabilisticBoundOperator.name("probabilistic bound operator");
-		steadyStateBoundOperator = (
-				(qi::lit("S") >> comparisonType > qi::double_ > stateFormula )[qi::_val =
-						MAKE(csl::SteadyStateBoundOperator<double> , 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<double>, qi::_1, qi::_2, qi::_3)] |
-				((qi::lit("F") >> (qi::lit("<=") | qi::lit("<"))) > qi::double_ > stateFormula)[qi::_val =
-								MAKE(csl::TimeBoundedEventually<double>, 0, qi::_1, qi::_2)] |
-				((qi::lit("F") >> (qi::lit(">=") | qi::lit(">"))) > qi::double_ > stateFormula)[qi::_val =
-								MAKE(csl::TimeBoundedEventually<double>, qi::_1, std::numeric_limits<double>::infinity(), qi::_2)]
-				);
-		timeBoundedEventually.name("time bounded eventually");
-		eventually = (qi::lit("F") > stateFormula)[qi::_val =
-				MAKE(csl::Eventually<double> , qi::_1)];
-		eventually.name("eventually");
-		next = (qi::lit("X") > stateFormula)[qi::_val =
-				MAKE(csl::Next<double> , qi::_1)];
-		next.name("next");
-		globally = (qi::lit("G") > stateFormula)[qi::_val =
-				MAKE(csl::Globally<double> , 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<double>, 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<double>, 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<double>, qi::_2, std::numeric_limits<double>::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<double>, 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<double>, qi::_1, storm::properties::MINIMIZE)] |
-				((qi::lit("P") >> qi::lit("max") >> qi::lit("=")) > qi::lit("?") >> pathFormula)[qi::_val =
-						MAKE(csl::CslFilter<double>, qi::_1, storm::properties::MAXIMIZE)] |
-				((qi::lit("P") >> qi::lit("=")) > qi::lit("?") >> pathFormula)[qi::_val =
-						MAKE(csl::CslFilter<double>, qi::_1)];
-		probabilisticNoBoundOperator.name("probabilistic no bound operator");
-		steadyStateNoBoundOperator = ((qi::lit("S") >> qi::lit("=")) > qi::lit("?") >> stateFormula )[qi::_val =
-				MAKE(csl::CslFilter<double>, 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<double> ,qi::_1, qi::_2)];
-		boundAction.name("bound action");
-
-		invertAction = qi::lit("invert")[qi::_val = MAKE(storm::properties::action::InvertAction<double>, )];
-		invertAction.name("invert action");
-
-		formulaAction = (qi::lit("formula") > qi::lit("(") >> stateFormula >> qi::lit(")"))[qi::_val =
-						MAKE(storm::properties::action::FormulaAction<double>, 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<double>, qi::_1, qi::_2)] |
-				(qi::lit("range") >> qi::lit("(") >> qi::uint_ >> qi::lit(")"))[qi::_val =
-						MAKE(storm::properties::action::RangeAction<double>, 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<double>, 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<double>, 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<double>, 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<double>, 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<double>, 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<double>, qi::_2, qi::_1, storm::properties::MINIMIZE)] |
-				 (noBoundOperator)[qi::_val =
-					qi::_1] |
-				 (formula)[qi::_val =
-					MAKE(csl::CslFilter<double>, qi::_1)];
-
-		filter.name("CSL formula filter");
-
-		start = (((filter) > (comment | qi::eps))[qi::_val = qi::_1] | comment[qi::_val = MAKE(csl::CslFilter<double>, nullptr)] ) > qi::eoi;
-		start.name("CSL formula filter start");
-
-	}
-
-	qi::rule<Iterator, std::shared_ptr<csl::CslFilter<double>>(), Skipper> start;
-	qi::rule<Iterator, std::shared_ptr<csl::CslFilter<double>>(), Skipper> filter;
-
-	qi::rule<Iterator, std::shared_ptr<csl::CslFilter<double>>(), Skipper> noBoundOperator;
-	qi::rule<Iterator, std::shared_ptr<csl::CslFilter<double>>(), Skipper> probabilisticNoBoundOperator;
-	qi::rule<Iterator, std::shared_ptr<csl::CslFilter<double>>(), Skipper> steadyStateNoBoundOperator;
-
-	qi::rule<Iterator, std::shared_ptr<storm::properties::action::AbstractAction<double>>(), Skipper> abstractAction;
-	qi::rule<Iterator, std::shared_ptr<storm::properties::action::BoundAction<double>>(), Skipper> boundAction;
-	qi::rule<Iterator, std::shared_ptr<storm::properties::action::InvertAction<double>>(), Skipper> invertAction;
-	qi::rule<Iterator, std::shared_ptr<storm::properties::action::FormulaAction<double>>(), Skipper> formulaAction;
-	qi::rule<Iterator, std::shared_ptr<storm::properties::action::RangeAction<double>>(), Skipper> rangeAction;
-	qi::rule<Iterator, std::shared_ptr<storm::properties::action::SortAction<double>>(), Skipper> sortAction;
-
-	qi::rule<Iterator, std::shared_ptr<csl::AbstractCslFormula<double>>(), Skipper> formula;
-	qi::rule<Iterator, std::shared_ptr<csl::AbstractCslFormula<double>>(), Skipper> comment;
-
-	qi::rule<Iterator, std::shared_ptr<csl::AbstractStateFormula<double>>(), Skipper> stateFormula;
-	qi::rule<Iterator, std::shared_ptr<csl::AbstractStateFormula<double>>(), Skipper> atomicStateFormula;
-
-	qi::rule<Iterator, std::shared_ptr<csl::AbstractStateFormula<double>>(), Skipper> andFormula;
-	qi::rule<Iterator, std::shared_ptr<csl::AbstractStateFormula<double>>(), Skipper> atomicProposition;
-	qi::rule<Iterator, std::shared_ptr<csl::AbstractStateFormula<double>>(), Skipper> orFormula;
-	qi::rule<Iterator, std::shared_ptr<csl::AbstractStateFormula<double>>(), Skipper> notFormula;
-	qi::rule<Iterator, std::shared_ptr<csl::ProbabilisticBoundOperator<double>>(), Skipper> probabilisticBoundOperator;
-	qi::rule<Iterator, std::shared_ptr<csl::SteadyStateBoundOperator<double>>(), Skipper> steadyStateBoundOperator;
-
-	qi::rule<Iterator, std::shared_ptr<csl::AbstractPathFormula<double>>(), Skipper> pathFormula;
-	qi::rule<Iterator, std::shared_ptr<csl::TimeBoundedEventually<double>>(), Skipper> timeBoundedEventually;
-	qi::rule<Iterator, std::shared_ptr<csl::Eventually<double>>(), Skipper> eventually;
-	qi::rule<Iterator, std::shared_ptr<csl::Next<double>>(), Skipper> next;
-	qi::rule<Iterator, std::shared_ptr<csl::Globally<double>>(), Skipper> globally;
-	qi::rule<Iterator, std::shared_ptr<csl::TimeBoundedUntil<double>>(), qi::locals< std::shared_ptr<storm::properties::csl::AbstractStateFormula<double>>>, Skipper> timeBoundedUntil;
-	qi::rule<Iterator, std::shared_ptr<csl::Until<double>>(), qi::locals< std::shared_ptr<storm::properties::csl::AbstractStateFormula<double>>>, Skipper> until;
-
-
-	qi::rule<Iterator, std::string(), Skipper> freeIdentifierName;
-	qi::rule<Iterator, storm::properties::ComparisonType(), Skipper> comparisonType;
-	qi::rule<Iterator, storm::properties::action::SortAction<double>::SortingCategory(), Skipper> sortingCategory;
-
-};
-
-std::shared_ptr<storm::properties::csl::CslFilter<double>> 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<storm::properties::csl::CslFilter<double>> result_pointer(nullptr);
-
-	CslGrammar<PositionIteratorType,  BOOST_TYPEOF(boost::spirit::ascii::space)> 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<PositionIteratorType>& 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<std::string>& 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 */

src/parser/CslParser.h

@@ -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 <functional>
-
-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<storm::properties::csl::CslFilter<double>> parseCslFormula(std::string formulaString);
-
-private:
-
-	/*!
-	 * Struct for the CSL grammar, that Boost::Spirit uses to parse the formulas.
-	 */
-	template<typename Iterator, typename Skipper>
-	struct CslGrammar;
-
-};
-
-} /* namespace parser */
-} /* namespace storm */
-#endif /* STORM_PARSER_CSLPARSER_H_ */

src/parser/ExpressionParser.cpp

@@ -5,7 +5,7 @@
 
 namespace storm {
     namespace parser {
-        ExpressionParser::ExpressionParser(storm::expressions::ExpressionManager& manager, qi::symbols<char, uint_fast64_t> 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<char, uint_fast64_t> 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");
             

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<char, uint_fast64_t> const& invalidIdentifiers_);
+            ExpressionParser(storm::expressions::ExpressionManager const& manager, qi::symbols<char, uint_fast64_t> 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<char, storm::expressions::Expression> {
-                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.

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<storm::expressions::ExpressionManager const> 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<std::tuple<boost::optional<storm::logic::OptimalityType>, boost::optional<storm::logic::ComparisonType>, boost::optional<double>>>(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<qi::fail>(start, handler(qi::_1, qi::_2, qi::_3, qi::_4));
+            qi::on_error<qi::fail>(stateFormula, handler(qi::_1, qi::_2, qi::_3, qi::_4));
+            qi::on_error<qi::fail>(orStateFormula, handler(qi::_1, qi::_2, qi::_3, qi::_4));
+            qi::on_error<qi::fail>(andStateFormula, handler(qi::_1, qi::_2, qi::_3, qi::_4));
+            qi::on_error<qi::fail>(probabilityOperator, handler(qi::_1, qi::_2, qi::_3, qi::_4));
+            qi::on_error<qi::fail>(rewardOperator, handler(qi::_1, qi::_2, qi::_3, qi::_4));
+            qi::on_error<qi::fail>(steadyStateOperator, handler(qi::_1, qi::_2, qi::_3, qi::_4));
+            qi::on_error<qi::fail>(operatorInformation, handler(qi::_1, qi::_2, qi::_3, qi::_4));
+            qi::on_error<qi::fail>(formula, handler(qi::_1, qi::_2, qi::_3, qi::_4));
+            qi::on_error<qi::fail>(pathFormula, handler(qi::_1, qi::_2, qi::_3, qi::_4));
+            qi::on_error<qi::fail>(conditionalFormula, handler(qi::_1, qi::_2, qi::_3, qi::_4));
+            qi::on_error<qi::fail>(untilFormula, handler(qi::_1, qi::_2, qi::_3, qi::_4));
+            qi::on_error<qi::fail>(nextFormula, handler(qi::_1, qi::_2, qi::_3, qi::_4));
+            qi::on_error<qi::fail>(globallyFormula, handler(qi::_1, qi::_2, qi::_3, qi::_4));
+            qi::on_error<qi::fail>(eventuallyFormula, handler(qi::_1, qi::_2, qi::_3, qi::_4));
+            qi::on_error<qi::fail>(atomicStateFormula, handler(qi::_1, qi::_2, qi::_3, qi::_4));
+            qi::on_error<qi::fail>(booleanLiteralFormula, handler(qi::_1, qi::_2, qi::_3, qi::_4));
+            qi::on_error<qi::fail>(labelFormula, handler(qi::_1, qi::_2, qi::_3, qi::_4));
+            qi::on_error<qi::fail>(expressionFormula, handler(qi::_1, qi::_2, qi::_3, qi::_4));
+            qi::on_error<qi::fail>(rewardPathFormula, handler(qi::_1, qi::_2, qi::_3, qi::_4));
+            qi::on_error<qi::fail>(reachabilityRewardFormula, handler(qi::_1, qi::_2, qi::_3, qi::_4));
+            qi::on_error<qi::fail>(cumulativeRewardFormula, handler(qi::_1, qi::_2, qi::_3, qi::_4));
+            qi::on_error<qi::fail>(instantaneousRewardFormula, handler(qi::_1, qi::_2, qi::_3, qi::_4));
+        }
+        
+        std::shared_ptr<storm::logic::Formula> FormulaParser::parseFromString(std::string const& formulaString, std::shared_ptr<storm::expressions::ExpressionManager const> const& manager) {
+            PositionIteratorType first(formulaString.begin());
+            PositionIteratorType iter = first;
+            PositionIteratorType last(formulaString.end());
+            
+            // Create empty result;
+            std::shared_ptr<storm::logic::Formula> 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<PositionIteratorType> const& e) {
+                STORM_LOG_THROW(false, storm::exceptions::WrongFormatException, e.what_);
+            }
+            
+            return result;
+        }
+        
+        std::shared_ptr<storm::logic::Formula> FormulaParser::createInstantaneousRewardFormula(unsigned stepCount) const {
+            return std::shared_ptr<storm::logic::Formula>(new storm::logic::InstantaneousRewardFormula(static_cast<uint_fast64_t>(stepCount)));
+        }
+        
+        std::shared_ptr<storm::logic::Formula> FormulaParser::createCumulativeRewardFormula(unsigned stepBound) const {
+            return std::shared_ptr<storm::logic::Formula>(new storm::logic::CumulativeRewardFormula(static_cast<uint_fast64_t>(stepBound)));
+        }
+        
+        std::shared_ptr<storm::logic::Formula> FormulaParser::createReachabilityRewardFormula(std::shared_ptr<storm::logic::Formula> const& stateFormula) const {
+            return std::shared_ptr<storm::logic::Formula>(new storm::logic::ReachabilityRewardFormula(stateFormula));
+        }
+        
+        std::shared_ptr<storm::logic::Formula> FormulaParser::createAtomicExpressionFormula(storm::expressions::Expression const& expression) const {
+            return std::shared_ptr<storm::logic::Formula>(new storm::logic::AtomicExpressionFormula(expression));
+        }
+        
+        std::shared_ptr<storm::logic::Formula> FormulaParser::createBooleanLiteralFormula(bool literal) const {
+            return std::shared_ptr<storm::logic::Formula>(new storm::logic::BooleanLiteralFormula(literal));
+        }
+        
+        std::shared_ptr<storm::logic::Formula> FormulaParser::createAtomicLabelFormula(std::string const& label) const {
+            std::cout << "creating atomic label formula" << std::endl;
+            return std::shared_ptr<storm::logic::Formula>(new storm::logic::AtomicLabelFormula(label));
+        }
+        
+        std::shared_ptr<storm::logic::Formula> FormulaParser::createEventuallyFormula(std::shared_ptr<storm::logic::Formula> const& subformula) const {
+            return std::shared_ptr<storm::logic::Formula>(new storm::logic::EventuallyFormula(subformula));
+        }
+        
+        std::shared_ptr<storm::logic::Formula> FormulaParser::createGloballyFormula(std::shared_ptr<storm::logic::Formula> const& subformula) const {
+            return std::shared_ptr<storm::logic::Formula>(new storm::logic::GloballyFormula(subformula));
+        }
+        
+        std::shared_ptr<storm::logic::Formula> FormulaParser::createNextFormula(std::shared_ptr<storm::logic::Formula> const& subformula) const {
+            return std::shared_ptr<storm::logic::Formula>(new storm::logic::NextFormula(subformula));
+        }
+        
+        std::shared_ptr<storm::logic::Formula> FormulaParser::createUntilFormula(std::shared_ptr<storm::logic::Formula> const& leftSubformula, std::shared_ptr<storm::logic::Formula> const& rightSubformula) {
+            return std::shared_ptr<storm::logic::Formula>(new storm::logic::UntilFormula(leftSubformula, rightSubformula));
+        }
+        
+        std::shared_ptr<storm::logic::Formula> FormulaParser::createBoundedUntilFormula(std::shared_ptr<storm::logic::Formula> const& leftSubformula, unsigned stepBound, std::shared_ptr<storm::logic::Formula> const& rightSubformula) const {
+            return std::shared_ptr<storm::logic::Formula>(new storm::logic::BoundedUntilFormula(leftSubformula, rightSubformula, static_cast<uint_fast64_t>(stepBound)));
+        }
+        
+        std::shared_ptr<storm::logic::Formula> FormulaParser::createConditionalFormula(std::shared_ptr<storm::logic::Formula> const& leftSubformula, std::shared_ptr<storm::logic::Formula> const& rightSubformula) const {
+            return std::shared_ptr<storm::logic::Formula>(new storm::logic::ConditionalPathFormula(leftSubformula, rightSubformula));
+        }
+        
+        std::shared_ptr<storm::logic::Formula> FormulaParser::createSteadyStateOperatorFormula(std::tuple<boost::optional<storm::logic::OptimalityType>, boost::optional<storm::logic::ComparisonType>, boost::optional<double>> const& operatorInformation, std::shared_ptr<storm::logic::Formula> const& subformula) const {
+            return std::shared_ptr<storm::logic::Formula>(new storm::logic::SteadyStateOperatorFormula(std::get<0>(operatorInformation), std::get<1>(operatorInformation), std::get<2>(operatorInformation), subformula));
+        }
+        
+        std::shared_ptr<storm::logic::Formula> FormulaParser::createRewardOperatorFormula(std::tuple<boost::optional<storm::logic::OptimalityType>, boost::optional<storm::logic::ComparisonType>, boost::optional<double>> const& operatorInformation, std::shared_ptr<storm::logic::Formula> const& subformula) const {
+            return std::shared_ptr<storm::logic::Formula>(new storm::logic::RewardOperatorFormula(std::get<0>(operatorInformation), std::get<1>(operatorInformation), std::get<2>(operatorInformation), subformula));
+        }
+        
+        std::shared_ptr<storm::logic::Formula> FormulaParser::createProbabilityOperatorFormula(std::tuple<boost::optional<storm::logic::OptimalityType>, boost::optional<storm::logic::ComparisonType>, boost::optional<double>> const& operatorInformation, std::shared_ptr<storm::logic::Formula> const& subformula) {
+            return std::shared_ptr<storm::logic::Formula>(new storm::logic::ProbabilityOperatorFormula(std::get<0>(operatorInformation), std::get<1>(operatorInformation), std::get<2>(operatorInformation), subformula));
+        }
+        
+        std::shared_ptr<storm::logic::Formula> FormulaParser::createBinaryBooleanStateFormula(std::shared_ptr<storm::logic::Formula> const& leftSubformula, std::shared_ptr<storm::logic::Formula> const& rightSubformula, storm::logic::BinaryBooleanStateFormula::OperatorType operatorType) {
+            return std::shared_ptr<storm::logic::Formula>(new storm::logic::BinaryBooleanStateFormula(operatorType, leftSubformula, rightSubformula));
+        }
+    } // namespace parser
+} // namespace storm

src/parser/FormulaParser.h

@@ -0,0 +1,152 @@
+#ifndef STORM_PARSER_PRCTLPARSER_H_
+#define STORM_PARSER_PRCTLPARSER_H_
+
+#include <sstream>
+
+#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<Iterator, std::shared_ptr<storm::logic::Formula>(), 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<storm::logic::Formula> parseFromString(std::string const& formulaString, std::shared_ptr<storm::expressions::ExpressionManager const> const& manager = std::shared_ptr<storm::expressions::ExpressionManager>(new storm::expressions::ExpressionManager()));
+            
+        private:
+            FormulaParser(std::shared_ptr<storm::expressions::ExpressionManager const> const& manager);
+            
+            struct keywordsStruct : qi::symbols<char, uint_fast64_t> {
+                keywordsStruct() {
+                    add
+                    ("true", 1)
+                    ("false", 2)
+                    ("min", 3)
+                    ("max", 4);
+                }
+            };
+            
+            // A parser used for recognizing the keywords.
+            keywordsStruct keywords_;
+            
+            struct relationalOperatorStruct : qi::symbols<char, storm::logic::ComparisonType> {
+                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<char, storm::logic::BinaryBooleanStateFormula::OperatorType> {
+                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<char, storm::logic::OptimalityType> {
+                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<typename T1, typename T2, typename T3, typename T4>
+                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<ErrorHandler> handler;
+            
+            qi::rule<Iterator, std::shared_ptr<storm::logic::Formula>(), Skipper> start;
+            
+            qi::rule<Iterator, std::tuple<boost::optional<storm::logic::OptimalityType>, boost::optional<storm::logic::ComparisonType>, boost::optional<double>>(), qi::locals<boost::optional<storm::logic::OptimalityType>, boost::optional<storm::logic::ComparisonType>, boost::optional<double>>, Skipper> operatorInformation;
+            qi::rule<Iterator, std::shared_ptr<storm::logic::Formula>(), Skipper> probabilityOperator;
+            qi::rule<Iterator, std::shared_ptr<storm::logic::Formula>(), Skipper> rewardOperator;
+            qi::rule<Iterator, std::shared_ptr<storm::logic::Formula>(), Skipper> steadyStateOperator;
+            
+            qi::rule<Iterator, std::shared_ptr<storm::logic::Formula>(), Skipper> formula;
+            qi::rule<Iterator, std::shared_ptr<storm::logic::Formula>(), Skipper> stateFormula;
+            qi::rule<Iterator, std::shared_ptr<storm::logic::Formula>(), Skipper> pathFormula;
+            
+            qi::rule<Iterator, std::shared_ptr<storm::logic::Formula>(), Skipper> atomicStateFormula;
+            qi::rule<Iterator, std::string(), Skipper> label;
+            
+            qi::rule<Iterator, std::shared_ptr<storm::logic::Formula>(), Skipper> andStateFormula;
+            qi::rule<Iterator, std::shared_ptr<storm::logic::Formula>(), Skipper> orStateFormula;
+            qi::rule<Iterator, std::shared_ptr<storm::logic::Formula>(), Skipper> notStateFormula;
+            qi::rule<Iterator, std::shared_ptr<storm::logic::Formula>(), Skipper> labelFormula;
+            qi::rule<Iterator, std::shared_ptr<storm::logic::Formula>(), Skipper> expressionFormula;
+            qi::rule<Iterator, std::shared_ptr<storm::logic::Formula>(), qi::locals<bool>, Skipper> booleanLiteralFormula;
+
+            qi::rule<Iterator, std::shared_ptr<storm::logic::Formula>(), Skipper> conditionalFormula;
+            qi::rule<Iterator, std::shared_ptr<storm::logic::Formula>(), Skipper> eventuallyFormula;
+            qi::rule<Iterator, std::shared_ptr<storm::logic::Formula>(), Skipper> nextFormula;
+            qi::rule<Iterator, std::shared_ptr<storm::logic::Formula>(), Skipper> globallyFormula;
+            qi::rule<Iterator, std::shared_ptr<storm::logic::Formula>(), Skipper> boundedUntilFormula;
+            qi::rule<Iterator, std::shared_ptr<storm::logic::Formula>(), Skipper> untilFormula;
+            
+            qi::rule<Iterator, std::shared_ptr<storm::logic::Formula>(), Skipper> rewardPathFormula;
+            qi::rule<Iterator, std::shared_ptr<storm::logic::Formula>(), Skipper> cumulativeRewardFormula;
+            qi::rule<Iterator, std::shared_ptr<storm::logic::Formula>(), Skipper> reachabilityRewardFormula;
+            qi::rule<Iterator, std::shared_ptr<storm::logic::Formula>(), Skipper> instantaneousRewardFormula;
+            
+            // Methods that actually create the expression objects.
+            std::shared_ptr<storm::logic::Formula> createInstantaneousRewardFormula(unsigned stepCount) const;
+            std::shared_ptr<storm::logic::Formula> createCumulativeRewardFormula(unsigned stepBound) const;
+            std::shared_ptr<storm::logic::Formula> createReachabilityRewardFormula(std::shared_ptr<storm::logic::Formula> const& stateFormula) const;
+            std::shared_ptr<storm::logic::Formula> createAtomicExpressionFormula(storm::expressions::Expression const& expression) const;
+            std::shared_ptr<storm::logic::Formula> createBooleanLiteralFormula(bool literal) const;
+            std::shared_ptr<storm::logic::Formula> createAtomicLabelFormula(std::string const& label) const;
+            std::shared_ptr<storm::logic::Formula> createEventuallyFormula(std::shared_ptr<storm::logic::Formula> const& subformula) const;
+            std::shared_ptr<storm::logic::Formula> createGloballyFormula(std::shared_ptr<storm::logic::Formula> const& subformula) const;
+            std::shared_ptr<storm::logic::Formula> createNextFormula(std::shared_ptr<storm::logic::Formula> const& subformula) const;
+            std::shared_ptr<storm::logic::Formula> createUntilFormula(std::shared_ptr<storm::logic::Formula> const& leftSubformula, std::shared_ptr<storm::logic::Formula> const& rightSubformula);
+            std::shared_ptr<storm::logic::Formula> createBoundedUntilFormula(std::shared_ptr<storm::logic::Formula> const& leftSubformula, unsigned stepBound, std::shared_ptr<storm::logic::Formula> const& rightSubformula) const;
+            std::shared_ptr<storm::logic::Formula> createConditionalFormula(std::shared_ptr<storm::logic::Formula> const& leftSubformula, std::shared_ptr<storm::logic::Formula> const& rightSubformula) const;
+            std::shared_ptr<storm::logic::Formula> createSteadyStateOperatorFormula(std::tuple<boost::optional<storm::logic::OptimalityType>, boost::optional<storm::logic::ComparisonType>, boost::optional<double>> const& operatorInformation, std::shared_ptr<storm::logic::Formula> const& subformula) const;
+            std::shared_ptr<storm::logic::Formula> createRewardOperatorFormula(std::tuple<boost::optional<storm::logic::OptimalityType>, boost::optional<storm::logic::ComparisonType>, boost::optional<double>> const& operatorInformation, std::shared_ptr<storm::logic::Formula> const& subformula) const;
+            std::shared_ptr<storm::logic::Formula> createProbabilityOperatorFormula(std::tuple<boost::optional<storm::logic::OptimalityType>, boost::optional<storm::logic::ComparisonType>, boost::optional<double>> const& operatorInformation, std::shared_ptr<storm::logic::Formula> const& subformula);
+            std::shared_ptr<storm::logic::Formula> createBinaryBooleanStateFormula(std::shared_ptr<storm::logic::Formula> const& leftSubformula, std::shared_ptr<storm::logic::Formula> const& rightSubformula, storm::logic::BinaryBooleanStateFormula::OperatorType operatorType);
+            
+        };
+        
+    } // namespace parser
+} // namespace storm
+
+#endif /* STORM_PARSER_PRCTLPARSER_H_ */

src/parser/LtlFileParser.cpp

@@ -1,43 +0,0 @@
-/*
- * LtlFileParser.cpp
- *
- *  Created on: 13.05.2013
- *      Author: thomas
- */
-
-#include <fstream>
-
-#include "LtlFileParser.h"
-#include "LtlParser.h"
-
-#include "src/exceptions/FileIoException.h"
-
-namespace storm {
-namespace parser {
-
-std::list<std::shared_ptr<storm::properties::ltl::LtlFilter<double>>> 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<std::shared_ptr<storm::properties::ltl::LtlFilter<double>>> 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
-
-

src/parser/LtlFileParser.h

@@ -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 <list>
-
-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<std::shared_ptr<storm::properties::ltl::LtlFilter<double>>> parseLtlFile(std::string filename);
-};
-
-} //namespace parser
-} //namespace storm
-
-#endif /* LTLFILEPARSER_H_ */

src/parser/LtlParser.cpp

@@ -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 <boost/typeof/typeof.hpp>
-#include <boost/spirit/include/qi.hpp>
-#include <boost/spirit/include/phoenix.hpp>
-
-// Include headers for spirit iterators. Needed for diagnostics and input stream iteration.
-#include <boost/spirit/include/classic_position_iterator.hpp>
-#include <boost/spirit/include/support_multi_pass.hpp>
-
-// Needed for file IO.
-#include <fstream>
-#include <iomanip>
-#include <map>
-
-
-// Some typedefs and namespace definitions to reduce code size.
-#define MAKE(Type, ...) phoenix::construct<std::shared_ptr<Type>>(phoenix::new_<Type>(__VA_ARGS__))
-typedef std::string::const_iterator BaseIteratorType;
-typedef boost::spirit::classic::position_iterator2<BaseIteratorType> PositionIteratorType;
-namespace qi = boost::spirit::qi;
-namespace phoenix = boost::phoenix;
-namespace ltl = storm::properties::ltl;
-
-
-namespace storm {
-
-namespace parser {
-
-template<typename Iterator, typename Skipper>
-struct LtlParser::LtlGrammar : qi::grammar<Iterator, std::shared_ptr<storm::properties::ltl::LtlFilter<double>>(), 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<double>::INDEX] |
-				(qi::lit("value"))[qi::_val = storm::properties::action::SortAction<double>::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<double>, qi::_val, qi::_1)];
-		orFormula.name("Or");
-		andFormula = untilFormula[qi::_val = qi::_1] > *(qi::lit("&") > untilFormula)[qi::_val =
-				MAKE(ltl::And<double>, 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<double>, qi::_val, qi::_2, qi::_1)] |
-				  (qi::lit("U") > notFormula)[qi::_val = MAKE(ltl::Until<double>, qi::_val, qi::_1)]);
-		until.name("Until");
-		notFormula = atomicLtlFormula[qi::_val = qi::_1] | (qi::lit("!") > atomicLtlFormula)[qi::_val =
-				MAKE(ltl::Not<double>, 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<double>, qi::_1)] | (qi::lit("\"") > (freeIdentifierName)[qi::_val = MAKE(ltl::Ap<double>, 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<double>, qi::_2, qi::_1)];
-		boundedEventually.name("Bounded Eventually");
-		eventually = (qi::lit("F") >> formula)[qi::_val =
-				MAKE(ltl::Eventually<double>, qi::_1)];
-		eventually.name("Eventually");
-		globally = (qi::lit("G") >> formula)[qi::_val =
-				MAKE(ltl::Globally<double>, qi::_1)];
-		globally.name("Globally");
-		next = (qi::lit("X") >> formula)[qi::_val =
-				MAKE(ltl::Next<double>, 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<double> ,qi::_1, qi::_2)];
-		boundAction.name("bound action");
-
-		invertAction = qi::lit("invert")[qi::_val = MAKE(storm::properties::action::InvertAction<double>, )];
-		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<double>, qi::_1, qi::_2)] |
-				(qi::lit("range") >> qi::lit("(") >> qi::uint_ >> qi::lit(")"))[qi::_val =
-						MAKE(storm::properties::action::RangeAction<double>, 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<double>, 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<double>, 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<double>, 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<double>, 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<double>, 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<double>, qi::_2, qi::_1, storm::properties::MINIMIZE)] |
-				 (formula)[qi::_val =
-					MAKE(ltl::LtlFilter<double>, qi::_1)];
-		filter.name("LTL formula filter");
-
-		start = (((filter) > (comment | qi::eps))[qi::_val = qi::_1] | comment[qi::_val = MAKE(ltl::LtlFilter<double>, nullptr)] ) > qi::eoi;
-		start.name("start");
-	}
-
-	qi::rule<Iterator, std::shared_ptr<storm::properties::ltl::LtlFilter<double>>(), Skipper> start;
-	qi::rule<Iterator, std::shared_ptr<storm::properties::ltl::LtlFilter<double>>(), Skipper> filter;
-
-	qi::rule<Iterator, std::shared_ptr<storm::properties::action::AbstractAction<double>>(), Skipper> abstractAction;
-	qi::rule<Iterator, std::shared_ptr<storm::properties::action::BoundAction<double>>(), Skipper> boundAction;
-	qi::rule<Iterator, std::shared_ptr<storm::properties::action::InvertAction<double>>(), Skipper> invertAction;
-	qi::rule<Iterator, std::shared_ptr<storm::properties::action::RangeAction<double>>(), Skipper> rangeAction;
-	qi::rule<Iterator, std::shared_ptr<storm::properties::action::SortAction<double>>(), Skipper> sortAction;
-
-	qi::rule<Iterator, std::shared_ptr<storm::properties::ltl::AbstractLtlFormula<double>>(), Skipper> comment;
-	qi::rule<Iterator, std::shared_ptr<storm::properties::ltl::AbstractLtlFormula<double>>(), Skipper> formula;
-	qi::rule<Iterator, std::shared_ptr<storm::properties::ltl::AbstractLtlFormula<double>>(), Skipper> atomicLtlFormula;
-
-	qi::rule<Iterator, std::shared_ptr<storm::properties::ltl::AbstractLtlFormula<double>>(), Skipper> andFormula;
-	qi::rule<Iterator, std::shared_ptr<storm::properties::ltl::AbstractLtlFormula<double>>(), Skipper> untilFormula;
-	qi::rule<Iterator, std::shared_ptr<storm::properties::ltl::AbstractLtlFormula<double>>(), Skipper> atomicProposition;
-	qi::rule<Iterator, std::shared_ptr<storm::properties::ltl::AbstractLtlFormula<double>>(), Skipper> orFormula;
-	qi::rule<Iterator, std::shared_ptr<storm::properties::ltl::AbstractLtlFormula<double>>(), Skipper> notFormula;
-
-	qi::rule<Iterator, std::shared_ptr<storm::properties::ltl::AbstractLtlFormula<double>>(), Skipper> pathFormula;
-	qi::rule<Iterator, std::shared_ptr<storm::properties::ltl::BoundedEventually<double>>(), Skipper> boundedEventually;
-	qi::rule<Iterator, std::shared_ptr<storm::properties::ltl::Eventually<double>>(), Skipper> eventually;
-	qi::rule<Iterator, std::shared_ptr<storm::properties::ltl::Globally<double>>(), Skipper> globally;
-	qi::rule<Iterator, std::shared_ptr<storm::properties::ltl::Next<double>>(), Skipper> next;
-	qi::rule<Iterator, std::shared_ptr<storm::properties::ltl::AbstractLtlFormula<double>>(), qi::locals< std::shared_ptr<storm::properties::ltl::AbstractLtlFormula<double>>>, Skipper> boundedUntil;
-	qi::rule<Iterator, std::shared_ptr<storm::properties::ltl::AbstractLtlFormula<double>>(), qi::locals< std::shared_ptr<storm::properties::ltl::AbstractLtlFormula<double>>>, Skipper> until;
-
-	qi::rule<Iterator, std::string(), Skipper> freeIdentifierName;
-	qi::rule<Iterator, storm::properties::ComparisonType(), Skipper> comparisonType;
-	qi::rule<Iterator, storm::properties::action::SortAction<double>::SortingCategory(), Skipper> sortingCategory;
-};
-
-std::shared_ptr<storm::properties::ltl::LtlFilter<double>> 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<storm::properties::ltl::LtlFilter<double>> result_pointer(nullptr);
-
-	LtlGrammar<PositionIteratorType,  BOOST_TYPEOF(boost::spirit::ascii::space)> 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<PositionIteratorType>& 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<std::string>& 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

src/parser/LtlParser.h

@@ -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<storm::properties::ltl::LtlFilter<double>> parseLtlFormula(std::string formulaString);
-
-private:
-
-	/*!
-	 * Struct for the Ltl grammar, that Boost::Spirit uses to parse the formulas.
-	 */
-	template<typename Iterator, typename Skipper>
-	struct LtlGrammar;
-
-};
-
-} /* namespace parser */
-} /* namespace storm */
-#endif /* STORM_PARSER_LTLPARSER_H_ */

src/parser/PrctlFileParser.cpp

@@ -1,44 +0,0 @@
-/*
- * PrctlFileParser.cpp
- *
- *  Created on: 06.02.2013
- *      Author: Thomas Heinemann
- */
-
-#include <sstream>
-
-#include "PrctlFileParser.h"
-#include "PrctlParser.h"
-#include "src/exceptions/FileIoException.h"
-
-namespace storm {
-namespace parser {
-
-std::list<std::shared_ptr<storm::properties::prctl::PrctlFilter<double>>> 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<std::shared_ptr<storm::properties::prctl::PrctlFilter<double>>> result;
-
-	std::string line;
-	//The while loop reads the input file line by line
-	while (std::getline(inputFileStream, line)) {
-		std::shared_ptr<storm::properties::prctl::PrctlFilter<double>> 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 */

src/parser/PrctlFileParser.h

@@ -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 <list>
-
-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<std::shared_ptr<storm::properties::prctl::PrctlFilter<double>>> parsePrctlFile(std::string filename);
-
-};
-
-} /* namespace parser */
-} /* namespace storm */
-
-#endif /* STORM_PARSER_PRCTLFILEPARSER_H_ */

src/parser/PrctlParser.cpp

@@ -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 <boost/typeof/typeof.hpp>
-#include <boost/spirit/include/qi.hpp>
-#include <boost/spirit/include/phoenix.hpp>
-#include <boost/spirit/include/phoenix_function.hpp>
-
-// Include headers for spirit iterators. Needed for diagnostics and input stream iteration.
-#include <boost/spirit/include/classic_position_iterator.hpp>
-#include <boost/spirit/include/support_multi_pass.hpp>
-
-// Needed for file IO.
-#include <fstream>
-#include <iomanip>
-#include <map>
-
-
-// Some typedefs, namespace definitions and a macro to reduce code size.
-#define MAKE(Type, ...) phoenix::construct<std::shared_ptr<Type>>(phoenix::new_<Type>(__VA_ARGS__))
-typedef std::string::const_iterator BaseIteratorType;
-typedef boost::spirit::classic::position_iterator2<BaseIteratorType> PositionIteratorType;
-namespace qi = boost::spirit::qi;
-namespace phoenix = boost::phoenix;
-namespace prctl = storm::properties::prctl;
-
-
-namespace storm {
-
-namespace parser {
-
-template<typename Iterator, typename Skipper>
-struct PrctlParser::PrctlGrammar : qi::grammar<Iterator, std::shared_ptr<storm::properties::prctl::PrctlFilter<double>>(), 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<double>::INDEX] |
-				(qi::lit("value"))[qi::_val = storm::properties::action::SortAction<double>::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<double>, qi::_val, qi::_1)];
-		orFormula.name("or formula");
-		andFormula = notFormula[qi::_val = qi::_1] > *(qi::lit("&") > notFormula)[qi::_val =
-				MAKE(prctl::And<double>, qi::_val, qi::_1)];
-		andFormula.name("and formula");
-		notFormula = atomicStateFormula[qi::_val = qi::_1] | (qi::lit("!") > atomicStateFormula)[qi::_val =
-				MAKE(prctl::Not<double>, 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<double>, qi::_1)] | (qi::lit("\"") > (freeIdentifierName)[qi::_val = MAKE(prctl::Ap<double>, qi::_1)] > qi::lit("\""));
-		atomicProposition.name("atomic proposition");
-		probabilisticBoundOperator = ((qi::lit("P") >> comparisonType > qi::double_ > pathFormula)[qi::_val =
-				MAKE(prctl::ProbabilisticBoundOperator<double>, qi::_1, qi::_2, qi::_3)]);
-		probabilisticBoundOperator.name("probabilistic bound operator");
-		rewardBoundOperator = ((qi::lit("R") >> comparisonType > qi::double_ > rewardPathFormula)[qi::_val =
-				MAKE(prctl::RewardBoundOperator<double>, 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<double>, qi::_2, qi::_1)];
-		boundedEventually.name("bounded eventually");
-		eventually = (qi::lit("F") > stateFormula)[qi::_val =
-				MAKE(prctl::Eventually<double>, qi::_1)];
-		eventually.name("eventually");
-		next = (qi::lit("X") > stateFormula)[qi::_val =
-				MAKE(prctl::Next<double>, qi::_1)];
-		next.name("next");
-		globally = (qi::lit("G") > stateFormula)[qi::_val =
-				MAKE(prctl::Globally<double>, qi::_1)];
-		globally.name("globally");
-		boundedUntil = (stateFormula[qi::_a = qi::_1] >> qi::lit("U") >> qi::lit("<=") > qi::int_ > stateFormula)[qi::_val =
-				MAKE(prctl::BoundedUntil<double>, qi::_a, qi::_3, qi::_2)];
-		boundedUntil.name("boundedUntil");
-		until = (stateFormula[qi::_a = qi::_1] >> qi::lit("U") > stateFormula)[qi::_val =
-				MAKE(prctl::Until<double>, 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<double>, qi::_1)];
-		cumulativeReward.name("path formula (for reward operator)");
-		reachabilityReward = (qi::lit("F") > stateFormula)[qi::_val =
-				MAKE(prctl::ReachabilityReward<double>, qi::_1)];
-		reachabilityReward.name("path formula (for reward operator)");
-		instantaneousReward = (qi::lit("I") > qi::lit("=") > qi::uint_)[qi::_val =
-				MAKE(prctl::InstantaneousReward<double>, qi::_1)];
-		instantaneousReward.name("path formula (for reward operator)");
-		steadyStateReward = (qi::lit("S"))[qi::_val =
-				MAKE(prctl::SteadyStateReward<double>, )];
-
-		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<double>, qi::_1, storm::properties::MINIMIZE)] |
-				((qi::lit("P") >> qi::lit("max") >> qi::lit("=")) > qi::lit("?") >> pathFormula )[qi::_val =
-						MAKE(prctl::PrctlFilter<double>, qi::_1, storm::properties::MAXIMIZE)] |
-				((qi::lit("P") >> qi::lit("=")) > qi::lit("?") >> pathFormula )[qi::_val =
-						MAKE(prctl::PrctlFilter<double>, qi::_1)]
-				);
-		probabilisticNoBoundOperator.name("no bound operator");
-
-		rewardNoBoundOperator = (
-				((qi::lit("R") >> qi::lit("min") >> qi::lit("=")) > qi::lit("?") >> rewardPathFormula )[qi::_val =
-						MAKE(prctl::PrctlFilter<double>, qi::_1, storm::properties::MINIMIZE)] |
-				((qi::lit("R") >> qi::lit("max") >> qi::lit("=")) > qi::lit("?") >> rewardPathFormula )[qi::_val =
-						MAKE(prctl::PrctlFilter<double>, qi::_1, storm::properties::MAXIMIZE)] |
-				((qi::lit("R") >> qi::lit("=")) > qi::lit("?") >> rewardPathFormula )[qi::_val =
-						MAKE(prctl::PrctlFilter<double>, 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<double> ,qi::_1, qi::_2)];
-		boundAction.name("bound action");
-
-		invertAction = qi::lit("invert")[qi::_val = MAKE(storm::properties::action::InvertAction<double>, )];
-		invertAction.name("invert action");
-
-		formulaAction = (qi::lit("formula") > qi::lit("(") >> stateFormula >> qi::lit(")"))[qi::_val =
-						MAKE(storm::properties::action::FormulaAction<double>, 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<double>, qi::_1, qi::_2)] |
-				(qi::lit("range") >> qi::lit("(") >> qi::uint_ >> qi::lit(")"))[qi::_val =
-						MAKE(storm::properties::action::RangeAction<double>, 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<double>, 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<double>, 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<double>, 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<double>, 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<double>, 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<double>, qi::_2, qi::_1, storm::properties::MINIMIZE)] |
-				 (noBoundOperator)[qi::_val =
-					qi::_1] |
-				 (formula)[qi::_val =
-					MAKE(prctl::PrctlFilter<double>, qi::_1)];
-		filter.name("PRCTL formula filter");
-
-		start = (((filter) > (comment | qi::eps))[qi::_val = qi::_1] | comment[qi::_val = MAKE(prctl::PrctlFilter<double>, nullptr)]) > qi::eoi;
-		start.name("start");
-
-	}
-
-	qi::rule<Iterator, std::shared_ptr<storm::properties::prctl::PrctlFilter<double>>(), Skipper> start;
-	qi::rule<Iterator, std::shared_ptr<storm::properties::prctl::PrctlFilter<double>>(), Skipper> filter;
-
-	qi::rule<Iterator, std::shared_ptr<storm::properties::prctl::PrctlFilter<double>>(), Skipper> noBoundOperator;
-	qi::rule<Iterator, std::shared_ptr<storm::properties::prctl::PrctlFilter<double>>(), Skipper> probabilisticNoBoundOperator;
-	qi::rule<Iterator, std::shared_ptr<storm::properties::prctl::PrctlFilter<double>>(), Skipper> rewardNoBoundOperator;
-
-	qi::rule<Iterator, std::shared_ptr<storm::properties::action::AbstractAction<double>>(), Skipper> abstractAction;
-	qi::rule<Iterator, std::shared_ptr<storm::properties::action::BoundAction<double>>(), Skipper> boundAction;
-	qi::rule<Iterator, std::shared_ptr<storm::properties::action::InvertAction<double>>(), Skipper> invertAction;
-	qi::rule<Iterator, std::shared_ptr<storm::properties::action::FormulaAction<double>>(), Skipper> formulaAction;
-	qi::rule<Iterator, std::shared_ptr<storm::properties::action::RangeAction<double>>(), Skipper> rangeAction;
-	qi::rule<Iterator, std::shared_ptr<storm::properties::action::SortAction<double>>(), Skipper> sortAction;
-
-	qi::rule<Iterator, std::shared_ptr<storm::properties::prctl::AbstractPrctlFormula<double>>(), Skipper> formula;
-	qi::rule<Iterator, std::shared_ptr<storm::properties::prctl::AbstractPrctlFormula<double>>(), Skipper> comment;
-
-	qi::rule<Iterator, std::shared_ptr<storm::properties::prctl::AbstractStateFormula<double>>(), Skipper> stateFormula;
-	qi::rule<Iterator, std::shared_ptr<storm::properties::prctl::AbstractStateFormula<double>>(), Skipper> atomicStateFormula;
-
-	qi::rule<Iterator, std::shared_ptr<storm::properties::prctl::AbstractStateFormula<double>>(), Skipper> andFormula;
-	qi::rule<Iterator, std::shared_ptr<storm::properties::prctl::AbstractStateFormula<double>>(), Skipper> atomicProposition;
-	qi::rule<Iterator, std::shared_ptr<storm::properties::prctl::AbstractStateFormula<double>>(), Skipper> orFormula;
-	qi::rule<Iterator, std::shared_ptr<storm::properties::prctl::AbstractStateFormula<double>>(), Skipper> notFormula;
-	qi::rule<Iterator, std::shared_ptr<storm::properties::prctl::ProbabilisticBoundOperator<double>>(), Skipper> probabilisticBoundOperator;
-	qi::rule<Iterator, std::shared_ptr<storm::properties::prctl::RewardBoundOperator<double>>(), Skipper> rewardBoundOperator;
-
-	qi::rule<Iterator, std::shared_ptr<storm::properties::prctl::AbstractPathFormula<double>>(), Skipper> pathFormula;
-	qi::rule<Iterator, std::shared_ptr<storm::properties::prctl::BoundedEventually<double>>(), Skipper> boundedEventually;
-	qi::rule<Iterator, std::shared_ptr<storm::properties::prctl::Eventually<double>>(), Skipper> eventually;
-	qi::rule<Iterator, std::shared_ptr<storm::properties::prctl::Next<double>>(), Skipper> next;
-	qi::rule<Iterator, std::shared_ptr<storm::properties::prctl::Globally<double>>(), Skipper> globally;
-	qi::rule<Iterator, std::shared_ptr<storm::properties::prctl::BoundedUntil<double>>(), qi::locals< std::shared_ptr<storm::properties::prctl::AbstractStateFormula<double>>>, Skipper> boundedUntil;
-	qi::rule<Iterator, std::shared_ptr<storm::properties::prctl::Until<double>>(), qi::locals< std::shared_ptr<storm::properties::prctl::AbstractStateFormula<double>>>, Skipper> until;
-
-	qi::rule<Iterator, std::shared_ptr<storm::properties::prctl::AbstractRewardPathFormula<double>>(), Skipper> rewardPathFormula;
-	qi::rule<Iterator, std::shared_ptr<storm::properties::prctl::CumulativeReward<double>>(), Skipper> cumulativeReward;
-	qi::rule<Iterator, std::shared_ptr<storm::properties::prctl::ReachabilityReward<double>>(), Skipper> reachabilityReward;
-	qi::rule<Iterator, std::shared_ptr<storm::properties::prctl::InstantaneousReward<double>>(), Skipper> instantaneousReward;
-	qi::rule<Iterator, std::shared_ptr<storm::properties::prctl::SteadyStateReward<double>>(), Skipper> steadyStateReward;
-
-
-	qi::rule<Iterator, std::string(), Skipper> freeIdentifierName;
-	qi::rule<Iterator, storm::properties::ComparisonType(), Skipper> comparisonType;
-	qi::rule<Iterator, storm::properties::action::SortAction<double>::SortingCategory(), Skipper> sortingCategory;
-};
-
-std::shared_ptr<storm::properties::prctl::PrctlFilter<double>> 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<storm::properties::prctl::PrctlFilter<double>> result_pointer(nullptr);
-
-	PrctlGrammar<PositionIteratorType,  BOOST_TYPEOF(boost::spirit::ascii::space)> 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<PositionIteratorType>& 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<std::string>& 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

src/parser/PrctlParser.h

@@ -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<storm::properties::prctl::PrctlFilter<double>> parsePrctlFormula(std::string formulaString);
-
-private:
-
-	/*!
-	 * Struct for the Prctl grammar, that Boost::Spirit uses to parse the formulas.
-	 */
-	template<typename Iterator, typename Skipper>
-	struct PrctlGrammar;
-
-};
-
-} // namespace parser
-} // namespace storm
-
-#endif /* STORM_PARSER_PRCTLPARSER_H_ */

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);
                 }
             };
             

src/properties/logic/Formulas.h

@@ -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"
-
-
-
-
-
-
-

src/properties/logic/SteadyStateFormula.cpp

@@ -1,35 +0,0 @@
-#include "src/properties/logic/SteadyStateFormula.h"
-
-namespace storm {
-    namespace logic {
-        SteadyStateFormula::SteadyStateFormula(std::shared_ptr<Formula> const& subformula) : SteadyStateFormula(boost::optional<ComparisonType>(), boost::optional<double>(), boost::optional<OptimalityType>(), subformula) {
-            // Intentionally left empty.
-        }
-        
-        SteadyStateFormula::SteadyStateFormula(ComparisonType comparisonType, double bound, std::shared_ptr<Formula> const& subformula) : SteadyStateFormula(boost::optional<ComparisonType>(comparisonType), boost::optional<double>(bound), boost::optional<OptimalityType>(), subformula) {
-            // Intentionally left empty.
-        }
-        
-        SteadyStateFormula::SteadyStateFormula(ComparisonType comparisonType, double bound, OptimalityType optimalityType, std::shared_ptr<Formula> const& subformula) : SteadyStateFormula(boost::optional<ComparisonType>(comparisonType), boost::optional<double>(bound), boost::optional<OptimalityType>(optimalityType), subformula) {
-            // Intentionally left empty.
-        }
-        
-        SteadyStateFormula::SteadyStateFormula(OptimalityType optimalityType, std::shared_ptr<Formula> const& subformula) : SteadyStateFormula(boost::optional<ComparisonType>(), boost::optional<double>(), boost::optional<OptimalityType>(optimalityType), subformula) {
-            // Intentionally left empty.
-        }
-        
-        bool SteadyStateFormula::isSteadyStateFormula() const {
-            return true;
-        }
-        
-        SteadyStateFormula::SteadyStateFormula(boost::optional<ComparisonType> comparisonType, boost::optional<double> bound, boost::optional<OptimalityType> optimalityType, std::shared_ptr<Formula> 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;
-        }
-    }
-}

src/properties/logic/SteadyStateFormula.h

@@ -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<Formula> const& subformula);
-            SteadyStateFormula(ComparisonType comparisonType, double bound, std::shared_ptr<Formula> const& subformula);
-            SteadyStateFormula(ComparisonType comparisonType, double bound, OptimalityType optimalityType, std::shared_ptr<Formula> const& subformula);
-            SteadyStateFormula(OptimalityType optimalityType, std::shared_ptr<Formula> 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> comparisonType, boost::optional<double> bound, boost::optional<OptimalityType> optimalityType, std::shared_ptr<Formula> const& subformula);
-        };
-    }
-}
-
-#endif /* STORM_LOGIC_STEADYSTATEFORMULA_H_ */

test/functional/modelchecker/ActionTest.cpp

@@ -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<double>::Result Result;
-
-TEST(ActionTest, BoundActionFunctionality) {
-
-	// Setup the modelchecker.
-	storm::models::Dtmc<double> 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<double> mc(model, std::unique_ptr<storm::solver::LinearEquationSolver<double>>(new storm::solver::GmmxxLinearEquationSolver<double>()));
-
-	// Build the filter input.
-	// Basically the modelchecking result of "F a" on the used DTMC.
-	std::vector<double> pathResult = mc.checkEventually(storm::properties::prctl::Eventually<double>(std::make_shared<storm::properties::prctl::Ap<double>>("a")), false);
-	std::vector<uint_fast64_t> 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<double> 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<double>(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<double>(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<double>(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<double>();
-	input.stateResult = mc.checkAp(storm::properties::prctl::Ap<double>("a"));
-	action = storm::properties::action::BoundAction<double>(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<double> 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<double> 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<double> 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<double> mc(model, std::unique_ptr<storm::solver::LinearEquationSolver<double>>(new storm::solver::GmmxxLinearEquationSolver<double>()));
-
-	// Build the filter input.
-	// Basically the modelchecking result of "F a" on the used DTMC.
-	std::vector<double> pathResult = mc.checkEventually(storm::properties::prctl::Eventually<double>(std::make_shared<storm::properties::prctl::Ap<double>>("a")), false);
-	storm::storage::BitVector stateResult = mc.checkAp(storm::properties::prctl::Ap<double>("a"));
-	std::vector<uint_fast64_t> 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<double> 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<double>(storm::properties::GREATER_EQUAL, 5879);
-
-	ASSERT_NO_THROW(result = action.evaluate(input, mc));
-	ASSERT_EQ(0, result.selection.getNumberOfSetBits());
-
-	action = storm::properties::action::BoundAction<double>(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<double>(static_cast<storm::properties::ComparisonType>(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<double>(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<double> 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<double> mc(model, std::unique_ptr<storm::solver::LinearEquationSolver<double>>(new storm::solver::GmmxxLinearEquationSolver<double>()));
-
-	// Build the filter input.
-	// Basically the modelchecking result of "F a" on the used DTMC.
-	std::vector<double> pathResult = mc.checkEventually(storm::properties::prctl::Eventually<double>(std::make_shared<storm::properties::prctl::Ap<double>>("a")), false);
-	storm::storage::BitVector stateResult = mc.checkAp(storm::properties::prctl::Ap<double>("c"));
-	std::vector<uint_fast64_t> 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<double> 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<double>(std::make_shared<storm::properties::prctl::ProbabilisticBoundOperator<double>>(storm::properties::LESS, 0.5, std::make_shared<storm::properties::prctl::Eventually<double>>(std::make_shared<storm::properties::prctl::Ap<double>>("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<double>();
-	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<double> 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<double> mc(model, std::unique_ptr<storm::solver::LinearEquationSolver<double>>(new storm::solver::GmmxxLinearEquationSolver<double>()));
-
-	// Build the filter input.
-	// Basically the modelchecking result of "F a" on the used DTMC.
-	std::vector<double> pathResult = mc.checkEventually(storm::properties::prctl::Eventually<double>(std::make_shared<storm::properties::prctl::Ap<double>>("a")), false);
-	std::vector<uint_fast64_t> 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<double> action(std::shared_ptr<storm::properties::csl::AbstractStateFormula<double>>(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<double> 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<double> mc(model, std::unique_ptr<storm::solver::LinearEquationSolver<double>>(new storm::solver::GmmxxLinearEquationSolver<double>()));
-
-	// Build the filter input.
-	// Basically the modelchecking result of "F a" on the used DTMC.
-	std::vector<double> pathResult = mc.checkEventually(storm::properties::prctl::Eventually<double>(std::make_shared<storm::properties::prctl::Ap<double>>("a")), false);
-	storm::storage::BitVector stateResult = mc.checkAp(storm::properties::prctl::Ap<double>("c"));
-	std::vector<uint_fast64_t> 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<double> 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<double> 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<double> mc(model, std::unique_ptr<storm::solver::LinearEquationSolver<double>>(new storm::solver::GmmxxLinearEquationSolver<double>()));
-
-	// Build the filter input.
-	// Basically the modelchecking result of "F a" on the used DTMC.
-	std::vector<double> pathResult = mc.checkEventually(storm::properties::prctl::Eventually<double>(std::make_shared<storm::properties::prctl::Ap<double>>("a")), false);
-	storm::storage::BitVector stateResult = mc.checkAp(storm::properties::prctl::Ap<double>("c"));
-	std::vector<uint_fast64_t> 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<double> 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<double>(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<double> 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<double> mc(model, std::unique_ptr<storm::solver::LinearEquationSolver<double>>(new storm::solver::GmmxxLinearEquationSolver<double>()));
-
-	// Build the filter input.
-	// Basically the modelchecking result of "F a" on the used DTMC.
-	std::vector<double> pathResult = mc.checkEventually(storm::properties::prctl::Eventually<double>(std::make_shared<storm::properties::prctl::Ap<double>>("a")), false);
-	storm::storage::BitVector stateResult = mc.checkAp(storm::properties::prctl::Ap<double>("c"));
-	std::vector<uint_fast64_t> 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<double> 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<double>(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<double>(3,1), storm::exceptions::IllegalArgumentValueException);
-}
-
-TEST(ActionTest, SortActionFunctionality){
-	// Setup the modelchecker.
-	storm::models::Dtmc<double> 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<double> mc(model, std::unique_ptr<storm::solver::LinearEquationSolver<double>>(new storm::solver::GmmxxLinearEquationSolver<double>()));
-
-	// Build the filter input.
-	// Basically the modelchecking result of "F a" on the used DTMC.
-	std::vector<double> pathResult = mc.checkEventually(storm::properties::prctl::Eventually<double>(std::make_shared<storm::properties::prctl::Ap<double>>("a")), false);
-	storm::storage::BitVector stateResult = mc.checkAp(storm::properties::prctl::Ap<double>("c"));
-	std::vector<uint_fast64_t> 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<double> 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<double>(storm::properties::action::SortAction<double>::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<double>(storm::properties::action::SortAction<double>::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<double>(storm::properties::action::SortAction<double>::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<double>();
-	input.stateResult = stateResult;
-
-	action = storm::properties::action::SortAction<double>(storm::properties::action::SortAction<double>::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<double>(storm::properties::action::SortAction<double>::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<double>(storm::properties::action::SortAction<double>::INDEX);
-	ASSERT_NO_THROW(input = action.evaluate(input, mc));
-	action = storm::properties::action::SortAction<double>(storm::properties::action::SortAction<double>::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<double> 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<double> mc(model, std::unique_ptr<storm::solver::LinearEquationSolver<double>>(new storm::solver::GmmxxLinearEquationSolver<double>()));
-
-	// Build the filter input.
-	// Basically the modelchecking result of "F a" on the used DTMC.
-	std::vector<double> pathResult = mc.checkEventually(storm::properties::prctl::Eventually<double>(std::make_shared<storm::properties::prctl::Ap<double>>("a")), false);
-	storm::storage::BitVector stateResult = mc.checkAp(storm::properties::prctl::Ap<double>("c"));
-	std::vector<uint_fast64_t> 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<double> action(storm::properties::action::SortAction<double>::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/functional/modelchecker/FilterTest.cpp

@@ -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 <memory>
-
-typedef storm::properties::action::AbstractAction<double>::Result Result;
-
-TEST(PrctlFilterTest, generalFunctionality) {
-	// Test filter queries of increasing complexity.
-
-	// Setup model and modelchecker.
-	storm::models::Dtmc<double> 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<double> mc(model, std::unique_ptr<storm::solver::LinearEquationSolver<double>>(new storm::solver::GmmxxLinearEquationSolver<double>()));
-
-	// 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<storm::properties::prctl::PrctlFilter<double>> 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<double> 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<double> mc(model, std::unique_ptr<storm::solver::LinearEquationSolver<double>>(new storm::solver::GmmxxLinearEquationSolver<double>()));
-
-	// Make a stub formula as child.
-	auto apFormula = std::make_shared<storm::properties::prctl::Ap<double>>("a");
-
-	// Test the filter for nullptr action handling.
-	auto formula = std::make_shared<storm::properties::prctl::PrctlFilter<double>>(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<std::shared_ptr<storm::properties::action::AbstractAction<double>>> actions(4, nullptr);
-	actions[1] = std::make_shared<storm::properties::action::InvertAction<double>>();
-
-	formula = std::make_shared<storm::properties::prctl::PrctlFilter<double>>(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<storm::properties::prctl::PrctlFilter<double>>();
-	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<double> 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<double> mc(model, std::make_shared<storm::solver::GmmxxNondeterministicLinearEquationSolver<double>>());
-
-	// 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<storm::properties::csl::CslFilter<double>> 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<double> 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<double> mc(model, std::make_shared<storm::solver::GmmxxNondeterministicLinearEquationSolver<double>>());
-
-	// Make a stub formula as child.
-	auto apFormula = std::make_shared<storm::properties::csl::Ap<double>>("r1");
-
-	// Test the filter for nullptr action handling.
-	auto formula = std::make_shared<storm::properties::csl::CslFilter<double>>(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<std::shared_ptr<storm::properties::action::AbstractAction<double>>> actions(4, nullptr);
-	actions[1] = std::make_shared<storm::properties::action::InvertAction<double>>();
-
-	formula = std::make_shared<storm::properties::csl::CslFilter<double>>(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<storm::properties::csl::CslFilter<double>>();
-	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.

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<storm::models::AbstractModel<double>> 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<storm::models::Dtmc<double>> dtmc = abstractModel->as<storm::models::Dtmc<double>>();
-
-	ASSERT_EQ(dtmc->getNumberOfStates(), 13ull);
-	ASSERT_EQ(dtmc->getNumberOfTransitions(), 20ull);
-
-	storm::modelchecker::prctl::SparseDtmcPrctlModelChecker<double> mc(*dtmc, std::unique_ptr<storm::solver::LinearEquationSolver<double>>(new storm::solver::GmmxxLinearEquationSolver<double>()));
-
-	auto apFormula = std::make_shared<storm::properties::prctl::Ap<double>>("one");
-	auto eventuallyFormula = std::make_shared<storm::properties::prctl::Eventually<double>>(apFormula);
-
-	std::vector<double> result = eventuallyFormula->check(mc, false);
-
-	ASSERT_LT(std::abs(result[0] - ((double)1.0/6.0)), storm::settings::gmmxxEquationSolverSettings().getPrecision());
-
-	apFormula = std::make_shared<storm::properties::prctl::Ap<double>>("two");
-	eventuallyFormula = std::make_shared<storm::properties::prctl::Eventually<double>>(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<storm::properties::prctl::Ap<double>>("three");
-	eventuallyFormula = std::make_shared<storm::properties::prctl::Eventually<double>>(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<storm::properties::prctl::Ap<double>>("done");
-	auto reachabilityRewardFormula = std::make_shared<storm::properties::prctl::ReachabilityReward<double>>(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<storm::models::AbstractModel<double>> 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<storm::models::Dtmc<double>> dtmc = abstractModel->as<storm::models::Dtmc<double>>();
-
-	ASSERT_EQ(8607ull, dtmc->getNumberOfStates());
-	ASSERT_EQ(15113ull, dtmc->getNumberOfTransitions());
-
-	storm::modelchecker::prctl::SparseDtmcPrctlModelChecker<double> mc(*dtmc, std::unique_ptr<storm::solver::LinearEquationSolver<double>>(new storm::solver::GmmxxLinearEquationSolver<double>()));
-
-	auto apFormula = std::make_shared<storm::properties::prctl::Ap<double>>("observe0Greater1");
-	auto eventuallyFormula = std::make_shared<storm::properties::prctl::Eventually<double>>(apFormula);
-
-	std::vector<double> result = eventuallyFormula->check(mc, false);
-
-	ASSERT_LT(std::abs(result[0] - 0.3328800375801578281), storm::settings::gmmxxEquationSolverSettings().getPrecision());
-
-	apFormula = std::make_shared<storm::properties::prctl::Ap<double>>("observeIGreater1");
-	eventuallyFormula = std::make_shared<storm::properties::prctl::Eventually<double>>(apFormula);
-
-	result = eventuallyFormula->check(mc, false);
-
-	ASSERT_LT(std::abs(result[0] - 0.1522194965), storm::settings::gmmxxEquationSolverSettings().getPrecision());
-
-	apFormula = std::make_shared<storm::properties::prctl::Ap<double>>("observeOnlyTrueSender");
-	eventuallyFormula = std::make_shared<storm::properties::prctl::Eventually<double>>(apFormula);
-
-	result = eventuallyFormula->check(mc, false);
-
-	ASSERT_LT(std::abs(result[0] - 0.32153724292835045), storm::settings::gmmxxEquationSolverSettings().getPrecision());
-}
-
-TEST(GmmxxDtmcPrctlModelCheckerTest, SynchronousLeader) {
-	std::shared_ptr<storm::models::AbstractModel<double>> 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<storm::models::Dtmc<double>> dtmc = abstractModel->as<storm::models::Dtmc<double>>();
-
-	ASSERT_EQ(12400ull, dtmc->getNumberOfStates());
-	ASSERT_EQ(16495ull, dtmc->getNumberOfTransitions());
-
-	storm::modelchecker::prctl::SparseDtmcPrctlModelChecker<double> mc(*dtmc, std::unique_ptr<storm::solver::LinearEquationSolver<double>>(new storm::solver::GmmxxLinearEquationSolver<double>()));
-
-	auto apFormula = std::make_shared<storm::properties::prctl::Ap<double>>("elected");
-	auto eventuallyFormula = std::make_shared<storm::properties::prctl::Eventually<double>>(apFormula);
-
-	std::vector<double> result = eventuallyFormula->check(mc, false);
-
-	ASSERT_LT(std::abs(result[0] - 1.0), storm::settings::gmmxxEquationSolverSettings().getPrecision());
-
-	apFormula = std::make_shared<storm::properties::prctl::Ap<double>>("elected");
-	auto boundedUntilFormula = std::make_shared<storm::properties::prctl::BoundedUntil<double>>(std::make_shared<storm::properties::prctl::Ap<double>>("true"), apFormula, 20);
-
-	result = boundedUntilFormula->check(mc, false);
-
-	ASSERT_LT(std::abs(result[0] - 0.9999965911265462636), storm::settings::gmmxxEquationSolverSettings().getPrecision());
-
-	apFormula = std::make_shared<storm::properties::prctl::Ap<double>>("elected");
-	auto reachabilityRewardFormula = std::make_shared<storm::properties::prctl::ReachabilityReward<double>>(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<storm::models::AbstractModel<double>> 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<storm::models::Dtmc<double>> dtmc = abstractModel->as<storm::models::Dtmc<double>>();
+//
+//	ASSERT_EQ(dtmc->getNumberOfStates(), 13ull);
+//	ASSERT_EQ(dtmc->getNumberOfTransitions(), 20ull);
+//
+//	storm::modelchecker::prctl::SparseDtmcPrctlModelChecker<double> mc(*dtmc, std::unique_ptr<storm::solver::LinearEquationSolver<double>>(new storm::solver::GmmxxLinearEquationSolver<double>()));
+//
+//	auto apFormula = std::make_shared<storm::properties::prctl::Ap<double>>("one");
+//	auto eventuallyFormula = std::make_shared<storm::properties::prctl::Eventually<double>>(apFormula);
+//
+//	std::vector<double> result = eventuallyFormula->check(mc, false);
+//
+//	ASSERT_LT(std::abs(result[0] - ((double)1.0/6.0)), storm::settings::gmmxxEquationSolverSettings().getPrecision());
+//
+//	apFormula = std::make_shared<storm::properties::prctl::Ap<double>>("two");
+//	eventuallyFormula = std::make_shared<storm::properties::prctl::Eventually<double>>(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<storm::properties::prctl::Ap<double>>("three");
+//	eventuallyFormula = std::make_shared<storm::properties::prctl::Eventually<double>>(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<storm::properties::prctl::Ap<double>>("done");
+//	auto reachabilityRewardFormula = std::make_shared<storm::properties::prctl::ReachabilityReward<double>>(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<storm::models::AbstractModel<double>> 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<storm::models::Dtmc<double>> dtmc = abstractModel->as<storm::models::Dtmc<double>>();
+//
+//	ASSERT_EQ(8607ull, dtmc->getNumberOfStates());
+//	ASSERT_EQ(15113ull, dtmc->getNumberOfTransitions());
+//
+//	storm::modelchecker::prctl::SparseDtmcPrctlModelChecker<double> mc(*dtmc, std::unique_ptr<storm::solver::LinearEquationSolver<double>>(new storm::solver::GmmxxLinearEquationSolver<double>()));
+//
+//	auto apFormula = std::make_shared<storm::properties::prctl::Ap<double>>("observe0Greater1");
+//	auto eventuallyFormula = std::make_shared<storm::properties::prctl::Eventually<double>>(apFormula);
+//
+//	std::vector<double> result = eventuallyFormula->check(mc, false);
+//
+//	ASSERT_LT(std::abs(result[0] - 0.3328800375801578281), storm::settings::gmmxxEquationSolverSettings().getPrecision());
+//
+//	apFormula = std::make_shared<storm::properties::prctl::Ap<double>>("observeIGreater1");
+//	eventuallyFormula = std::make_shared<storm::properties::prctl::Eventually<double>>(apFormula);
+//
+//	result = eventuallyFormula->check(mc, false);
+//
+//	ASSERT_LT(std::abs(result[0] - 0.1522194965), storm::settings::gmmxxEquationSolverSettings().getPrecision());
+//
+//	apFormula = std::make_shared<storm::properties::prctl::Ap<double>>("observeOnlyTrueSender");
+//	eventuallyFormula = std::make_shared<storm::properties::prctl::Eventually<double>>(apFormula);
+//
+//	result = eventuallyFormula->check(mc, false);
+//
+//	ASSERT_LT(std::abs(result[0] - 0.32153724292835045), storm::settings::gmmxxEquationSolverSettings().getPrecision());
+//}
+//
+//TEST(GmmxxDtmcPrctlModelCheckerTest, SynchronousLeader) {
+//	std::shared_ptr<storm::models::AbstractModel<double>> 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<storm::models::Dtmc<double>> dtmc = abstractModel->as<storm::models::Dtmc<double>>();
+//
+//	ASSERT_EQ(12400ull, dtmc->getNumberOfStates());
+//	ASSERT_EQ(16495ull, dtmc->getNumberOfTransitions());
+//
+//	storm::modelchecker::prctl::SparseDtmcPrctlModelChecker<double> mc(*dtmc, std::unique_ptr<storm::solver::LinearEquationSolver<double>>(new storm::solver::GmmxxLinearEquationSolver<double>()));
+//
+//	auto apFormula = std::make_shared<storm::properties::prctl::Ap<double>>("elected");
+//	auto eventuallyFormula = std::make_shared<storm::properties::prctl::Eventually<double>>(apFormula);
+//
+//	std::vector<double> result = eventuallyFormula->check(mc, false);
+//
+//	ASSERT_LT(std::abs(result[0] - 1.0), storm::settings::gmmxxEquationSolverSettings().getPrecision());
+//
+//	apFormula = std::make_shared<storm::properties::prctl::Ap<double>>("elected");
+//	auto boundedUntilFormula = std::make_shared<storm::properties::prctl::BoundedUntil<double>>(std::make_shared<storm::properties::prctl::Ap<double>>("true"), apFormula, 20);
+//
+//	result = boundedUntilFormula->check(mc, false);
+//
+//	ASSERT_LT(std::abs(result[0] - 0.9999965911265462636), storm::settings::gmmxxEquationSolverSettings().getPrecision());
+//
+//	apFormula = std::make_shared<storm::properties::prctl::Ap<double>>("elected");
+//	auto reachabilityRewardFormula = std::make_shared<storm::properties::prctl::ReachabilityReward<double>>(apFormula);
+//
+//	result = reachabilityRewardFormula->check(mc, false);
+//
+//	ASSERT_LT(std::abs(result[0] - 1.044879046), storm::settings::gmmxxEquationSolverSettings().getPrecision());
+//}

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<storm::models::AbstractModel<double>> 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<storm::models::Mdp<double>> mdp = abstractModel->as<storm::models::Mdp<double>>();
-    
-	ASSERT_EQ(mdp->getNumberOfStates(), 169ull);
-	ASSERT_EQ(mdp->getNumberOfTransitions(), 436ull);
-    
-	storm::modelchecker::prctl::SparseMdpPrctlModelChecker<double> mc(*mdp, std::shared_ptr<storm::solver::NativeNondeterministicLinearEquationSolver<double>>(new storm::solver::NativeNondeterministicLinearEquationSolver<double>()));
-    
-	auto apFormula = std::make_shared<storm::properties::prctl::Ap<double>>("two");
-	auto eventuallyFormula = std::make_shared<storm::properties::prctl::Eventually<double>>(apFormula);
-    
-	std::vector<double> 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<storm::properties::prctl::Ap<double>>("three");
-	eventuallyFormula = std::make_shared<storm::properties::prctl::Eventually<double>>(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<storm::properties::prctl::Ap<double>>("four");
-	eventuallyFormula = std::make_shared<storm::properties::prctl::Eventually<double>>(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<storm::properties::prctl::Ap<double>>("done");
-	auto reachabilityRewardFormula = std::make_shared<storm::properties::prctl::ReachabilityReward<double>>(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<storm::models::Mdp<double>> stateRewardMdp = abstractModel->as<storm::models::Mdp<double>>();
-    
-    storm::modelchecker::prctl::SparseMdpPrctlModelChecker<double> stateRewardModelChecker(*stateRewardMdp, std::shared_ptr<storm::solver::NativeNondeterministicLinearEquationSolver<double>>(new storm::solver::NativeNondeterministicLinearEquationSolver<double>()));
-
-	apFormula = std::make_shared<storm::properties::prctl::Ap<double>>("done");
-	reachabilityRewardFormula = std::make_shared<storm::properties::prctl::ReachabilityReward<double>>(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<storm::models::Mdp<double>> stateAndTransitionRewardMdp = abstractModel->as<storm::models::Mdp<double>>();
-    
-	storm::modelchecker::prctl::SparseMdpPrctlModelChecker<double> stateAndTransitionRewardModelChecker(*stateAndTransitionRewardMdp, std::shared_ptr<storm::solver::NativeNondeterministicLinearEquationSolver<double>>(new storm::solver::NativeNondeterministicLinearEquationSolver<double>()));
-    
-	apFormula = std::make_shared<storm::properties::prctl::Ap<double>>("done");
-	reachabilityRewardFormula = std::make_shared<storm::properties::prctl::ReachabilityReward<double>>(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<storm::models::AbstractModel<double>> 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<storm::models::Mdp<double>> mdp = abstractModel->as<storm::models::Mdp<double>>();
-
-	ASSERT_EQ(3172ull, mdp->getNumberOfStates());
-	ASSERT_EQ(7144ull, mdp->getNumberOfTransitions());
-
-	storm::modelchecker::prctl::SparseMdpPrctlModelChecker<double> mc(*mdp, std::shared_ptr<storm::solver::NativeNondeterministicLinearEquationSolver<double>>(new storm::solver::NativeNondeterministicLinearEquationSolver<double>()));
-
-	auto apFormula = std::make_shared<storm::properties::prctl::Ap<double>>("elected");
-	auto eventuallyFormula = std::make_shared<storm::properties::prctl::Eventually<double>>(apFormula);
-
-	std::vector<double> 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<storm::properties::prctl::Ap<double>>("elected");
-	auto boundedEventuallyFormula = std::make_shared<storm::properties::prctl::BoundedEventually<double>>(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<storm::properties::prctl::Ap<double>>("elected");
-	auto reachabilityRewardFormula = std::make_shared<storm::properties::prctl::ReachabilityReward<double>>(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<storm::models::AbstractModel<double>> 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<storm::models::Mdp<double>> mdp = abstractModel->as<storm::models::Mdp<double>>();
+//    
+//	ASSERT_EQ(mdp->getNumberOfStates(), 169ull);
+//	ASSERT_EQ(mdp->getNumberOfTransitions(), 436ull);
+//    
+//	storm::modelchecker::prctl::SparseMdpPrctlModelChecker<double> mc(*mdp, std::shared_ptr<storm::solver::NativeNondeterministicLinearEquationSolver<double>>(new storm::solver::NativeNondeterministicLinearEquationSolver<double>()));
+//    
+//	auto apFormula = std::make_shared<storm::properties::prctl::Ap<double>>("two");
+//	auto eventuallyFormula = std::make_shared<storm::properties::prctl::Eventually<double>>(apFormula);
+//    
+//	std::vector<double> 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<storm::properties::prctl::Ap<double>>("three");
+//	eventuallyFormula = std::make_shared<storm::properties::prctl::Eventually<double>>(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<storm::properties::prctl::Ap<double>>("four");
+//	eventuallyFormula = std::make_shared<storm::properties::prctl::Eventually<double>>(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<storm::properties::prctl::Ap<double>>("done");
+//	auto reachabilityRewardFormula = std::make_shared<storm::properties::prctl::ReachabilityReward<double>>(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<storm::models::Mdp<double>> stateRewardMdp = abstractModel->as<storm::models::Mdp<double>>();
+//    
+//    storm::modelchecker::prctl::SparseMdpPrctlModelChecker<double> stateRewardModelChecker(*stateRewardMdp, std::shared_ptr<storm::solver::NativeNondeterministicLinearEquationSolver<double>>(new storm::solver::NativeNondeterministicLinearEquationSolver<double>()));
+//
+//	apFormula = std::make_shared<storm::properties::prctl::Ap<double>>("done");
+//	reachabilityRewardFormula = std::make_shared<storm::properties::prctl::ReachabilityReward<double>>(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<storm::models::Mdp<double>> stateAndTransitionRewardMdp = abstractModel->as<storm::models::Mdp<double>>();
+//    
+//	storm::modelchecker::prctl::SparseMdpPrctlModelChecker<double> stateAndTransitionRewardModelChecker(*stateAndTransitionRewardMdp, std::shared_ptr<storm::solver::NativeNondeterministicLinearEquationSolver<double>>(new storm::solver::NativeNondeterministicLinearEquationSolver<double>()));
+//    
+//	apFormula = std::make_shared<storm::properties::prctl::Ap<double>>("done");
+//	reachabilityRewardFormula = std::make_shared<storm::properties::prctl::ReachabilityReward<double>>(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<storm::models::AbstractModel<double>> 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<storm::models::Mdp<double>> mdp = abstractModel->as<storm::models::Mdp<double>>();
+//
+//	ASSERT_EQ(3172ull, mdp->getNumberOfStates());
+//	ASSERT_EQ(7144ull, mdp->getNumberOfTransitions());
+//
+//	storm::modelchecker::prctl::SparseMdpPrctlModelChecker<double> mc(*mdp, std::shared_ptr<storm::solver::NativeNondeterministicLinearEquationSolver<double>>(new storm::solver::NativeNondeterministicLinearEquationSolver<double>()));
+//
+//	auto apFormula = std::make_shared<storm::properties::prctl::Ap<double>>("elected");
+//	auto eventuallyFormula = std::make_shared<storm::properties::prctl::Eventually<double>>(apFormula);
+//
+//	std::vector<double> 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<storm::properties::prctl::Ap<double>>("elected");
+//	auto boundedEventuallyFormula = std::make_shared<storm::properties::prctl::BoundedEventually<double>>(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<storm::properties::prctl::Ap<double>>("elected");
+//	auto reachabilityRewardFormula = std::make_shared<storm::properties::prctl::ReachabilityReward<double>>(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());
+//}

test/functional/parser/CslParserTest.cpp

@@ -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<csl::CslFilter<double>> 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<csl::CslFilter<double>> 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<csl::CslFilter<double>> 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<csl::Next<double>>(formula->getChild()).get(), nullptr);
-	auto nextFormula = std::dynamic_pointer_cast<csl::Next<double>>(formula->getChild());
-	ASSERT_FALSE(nextFormula->isPropositional());
-	ASSERT_FALSE(nextFormula->isProbEventuallyAP());
-
-	ASSERT_NE(std::dynamic_pointer_cast<csl::ProbabilisticBoundOperator<double>>(nextFormula->getChild()).get(), nullptr);
-	auto probBoundFormula = std::dynamic_pointer_cast<csl::ProbabilisticBoundOperator<double>>(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<csl::Until<double>>(probBoundFormula->getChild()).get(), nullptr);
-	auto untilFormula = std::dynamic_pointer_cast<csl::Until<double>>(probBoundFormula->getChild());
-	ASSERT_FALSE(untilFormula->isPropositional());
-	ASSERT_FALSE(untilFormula->isProbEventuallyAP());
-
-	ASSERT_NE(std::dynamic_pointer_cast<csl::Ap<double>>(untilFormula->getLeft()).get(), nullptr);
-	ASSERT_NE(std::dynamic_pointer_cast<csl::Ap<double>>(untilFormula->getRight()).get(), nullptr);
-	ASSERT_EQ("a", std::dynamic_pointer_cast<csl::Ap<double>>(untilFormula->getLeft())->getAp());
-	ASSERT_EQ("b", std::dynamic_pointer_cast<csl::Ap<double>>(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<csl::CslFilter<double>> 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<storm::properties::csl::ProbabilisticBoundOperator<double>>(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<csl::CslFilter<double>> 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<storm::properties::csl::SteadyStateBoundOperator<double>>(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<csl::CslFilter<double>> 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<csl::CslFilter<double>> 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<csl::CslFilter<double>> 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<csl::CslFilter<double>> 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<storm::properties::action::FormulaAction<double>>(formula->getAction(0)).get(), nullptr);
-	ASSERT_NE(std::dynamic_pointer_cast<storm::properties::action::InvertAction<double>>(formula->getAction(1)).get(), nullptr);
-	ASSERT_NE(std::dynamic_pointer_cast<storm::properties::action::BoundAction<double>>(formula->getAction(2)).get(), nullptr);
-	ASSERT_NE(std::dynamic_pointer_cast<storm::properties::action::SortAction<double>>(formula->getAction(3)).get(), nullptr);
-	ASSERT_NE(std::dynamic_pointer_cast<storm::properties::action::RangeAction<double>>(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<csl::CslFilter<double>> 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<csl::CslFilter<double>> formula(nullptr);
-	ASSERT_THROW(
-		formula = storm::parser::CslParser::parseCslFormula(input),
-		storm::exceptions::WrongFormatException
-	);
-}
-
-TEST(CslParserTest, wrongFormulaTest) {
-	std::string input = "(a | b) & +";
-	std::shared_ptr<csl::CslFilter<double>> 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<csl::CslFilter<double>> formula(nullptr);
-	ASSERT_THROW(
-		formula = storm::parser::CslParser::parseCslFormula(input),
-		storm::exceptions::WrongFormatException
-	);
-}

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<storm::logic::Formula> 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<prctl::PrctlFilter<double>> 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<prctl::PrctlFilter<double>> 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<prctl::Next<double>>(formula->getChild()).get(), nullptr);
+//	auto nextFormula = std::dynamic_pointer_cast<prctl::Next<double>>(formula->getChild());
+//	ASSERT_FALSE(nextFormula->isPropositional());
+//	ASSERT_FALSE(nextFormula->isProbEventuallyAP());
+//
+//	ASSERT_NE(std::dynamic_pointer_cast<prctl::ProbabilisticBoundOperator<double>>(nextFormula->getChild()).get(), nullptr);
+//	auto probBoundFormula = std::dynamic_pointer_cast<prctl::ProbabilisticBoundOperator<double>>(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<prctl::Until<double>>(probBoundFormula->getChild()).get(), nullptr);
+//	auto untilFormula = std::dynamic_pointer_cast<prctl::Until<double>>(probBoundFormula->getChild());
+//	ASSERT_FALSE(untilFormula->isPropositional());
+//	ASSERT_FALSE(untilFormula->isProbEventuallyAP());
+//
+//	ASSERT_NE(std::dynamic_pointer_cast<prctl::Ap<double>>(untilFormula->getLeft()).get(), nullptr);
+//	ASSERT_NE(std::dynamic_pointer_cast<prctl::Ap<double>>(untilFormula->getRight()).get(), nullptr);
+//	ASSERT_EQ("a", std::dynamic_pointer_cast<prctl::Ap<double>>(untilFormula->getLeft())->getAp());
+//	ASSERT_EQ("b", std::dynamic_pointer_cast<prctl::Ap<double>>(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<prctl::PrctlFilter<double>> 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<prctl::ProbabilisticBoundOperator<double>>(formula->getChild()).get(), nullptr);
+//	std::shared_ptr<prctl::ProbabilisticBoundOperator<double>> op = std::static_pointer_cast<prctl::ProbabilisticBoundOperator<double>>(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<prctl::PrctlFilter<double>>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<prctl::RewardBoundOperator<double>>(formula->getChild()).get(), nullptr);
+//	std::shared_ptr<prctl::RewardBoundOperator<double>> op = std::static_pointer_cast<prctl::RewardBoundOperator<double>>(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<prctl::PrctlFilter<double>> 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<prctl::PrctlFilter<double>> 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<prctl::PrctlFilter<double>> 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<prctl::PrctlFilter<double>> 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<storm::properties::action::FormulaAction<double>>(formula->getAction(0)).get(), nullptr);
+//	ASSERT_NE(std::dynamic_pointer_cast<storm::properties::action::InvertAction<double>>(formula->getAction(1)).get(), nullptr);
+//	ASSERT_NE(std::dynamic_pointer_cast<storm::properties::action::BoundAction<double>>(formula->getAction(2)).get(), nullptr);
+//	ASSERT_NE(std::dynamic_pointer_cast<storm::properties::action::SortAction<double>>(formula->getAction(3)).get(), nullptr);
+//	ASSERT_NE(std::dynamic_pointer_cast<storm::properties::action::RangeAction<double>>(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<prctl::PrctlFilter<double>> 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<prctl::PrctlFilter<double>> formula(nullptr);
+//	ASSERT_THROW(
+//			formula = storm::parser::PrctlParser::parsePrctlFormula("P > 0.5 [ a ]"),
+//			storm::exceptions::WrongFormatException
+//	);
+//}
+//
+//TEST(PrctlParserTest, wrongFormulaTest) {
+//	std::shared_ptr<prctl::PrctlFilter<double>> formula(nullptr);
+//	ASSERT_THROW(
+//			formula = storm::parser::PrctlParser::parsePrctlFormula("(a | b) & +"),
+//			storm::exceptions::WrongFormatException
+//	);
+//}
+//
+//TEST(PrctlParserTest, wrongFormulaTest2) {
+//	std::shared_ptr<prctl::PrctlFilter<double>> formula(nullptr);
+//	ASSERT_THROW(
+//			formula = storm::parser::PrctlParser::parsePrctlFormula("P>0 [ F & a ]"),
+//			storm::exceptions::WrongFormatException
+//	);
+//}

test/functional/parser/LtlParserTest.cpp

@@ -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<storm::properties::ltl::LtlFilter<double>> 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<ltl::LtlFilter<double>> 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<ltl::LtlFilter<double>> 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<ltl::LtlFilter<double>> 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<ltl::LtlFilter<double>> formula(nullptr);
-	ASSERT_NO_THROW(
-		formula = storm::parser::LtlParser::parseLtlFormula(input);
-	);
-
-	ASSERT_NE(formula.get(), nullptr);
-
-	ASSERT_FALSE(formula->getChild()->isPropositional());
-
-	std::shared_ptr<storm::properties::ltl::BoundedEventually<double>> op = std::dynamic_pointer_cast<storm::properties::ltl::BoundedEventually<double>>(formula->getChild());
-	ASSERT_NE(op.get(), nullptr);
-	ASSERT_EQ(static_cast<uint_fast64_t>(5), op->getBound());
-
-
-	ASSERT_EQ("F<=5 a", formula->toString());
-}
-
-TEST(LtlParserTest, parseBoundedUntilFormulaTest) {
-	std::string input = "a U<=3 b";
-	std::shared_ptr<ltl::LtlFilter<double>> formula(nullptr);
-	ASSERT_NO_THROW(
-		formula = storm::parser::LtlParser::parseLtlFormula(input);
-	);
-
-	ASSERT_NE(formula.get(), nullptr);
-
-	ASSERT_FALSE(formula->getChild()->isPropositional());
-
-	std::shared_ptr<storm::properties::ltl::BoundedUntil<double>> op = std::dynamic_pointer_cast<storm::properties::ltl::BoundedUntil<double>>(formula->getChild());
-	ASSERT_NE(op.get(), nullptr);
-	ASSERT_EQ(static_cast<uint_fast64_t>(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<ltl::LtlFilter<double>> 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<storm::properties::action::InvertAction<double>>(formula->getAction(0)).get(), nullptr);
-	ASSERT_NE(std::dynamic_pointer_cast<storm::properties::action::BoundAction<double>>(formula->getAction(1)).get(), nullptr);
-	ASSERT_NE(std::dynamic_pointer_cast<storm::properties::action::SortAction<double>>(formula->getAction(2)).get(), nullptr);
-	ASSERT_NE(std::dynamic_pointer_cast<storm::properties::action::RangeAction<double>>(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<ltl::LtlFilter<double>> 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<ltl::LtlFilter<double>> 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<ltl::LtlFilter<double>> 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
-	);
-}

test/functional/parser/PrctlParserTest.cpp

@@ -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<prctl::PrctlFilter<double>> 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<prctl::PrctlFilter<double>> 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<prctl::PrctlFilter<double>> 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<prctl::Next<double>>(formula->getChild()).get(), nullptr);
-	auto nextFormula = std::dynamic_pointer_cast<prctl::Next<double>>(formula->getChild());
-	ASSERT_FALSE(nextFormula->isPropositional());
-	ASSERT_FALSE(nextFormula->isProbEventuallyAP());
-
-	ASSERT_NE(std::dynamic_pointer_cast<prctl::ProbabilisticBoundOperator<double>>(nextFormula->getChild()).get(), nullptr);
-	auto probBoundFormula = std::dynamic_pointer_cast<prctl::ProbabilisticBoundOperator<double>>(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<prctl::Until<double>>(probBoundFormula->getChild()).get(), nullptr);
-	auto untilFormula = std::dynamic_pointer_cast<prctl::Until<double>>(probBoundFormula->getChild());
-	ASSERT_FALSE(untilFormula->isPropositional());
-	ASSERT_FALSE(untilFormula->isProbEventuallyAP());
-
-	ASSERT_NE(std::dynamic_pointer_cast<prctl::Ap<double>>(untilFormula->getLeft()).get(), nullptr);
-	ASSERT_NE(std::dynamic_pointer_cast<prctl::Ap<double>>(untilFormula->getRight()).get(), nullptr);
-	ASSERT_EQ("a", std::dynamic_pointer_cast<prctl::Ap<double>>(untilFormula->getLeft())->getAp());
-	ASSERT_EQ("b", std::dynamic_pointer_cast<prctl::Ap<double>>(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<prctl::PrctlFilter<double>> 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<prctl::ProbabilisticBoundOperator<double>>(formula->getChild()).get(), nullptr);
-	std::shared_ptr<prctl::ProbabilisticBoundOperator<double>> op = std::static_pointer_cast<prctl::ProbabilisticBoundOperator<double>>(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<prctl::PrctlFilter<double>>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<prctl::RewardBoundOperator<double>>(formula->getChild()).get(), nullptr);
-	std::shared_ptr<prctl::RewardBoundOperator<double>> op = std::static_pointer_cast<prctl::RewardBoundOperator<double>>(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<prctl::PrctlFilter<double>> 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<prctl::PrctlFilter<double>> 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<prctl::PrctlFilter<double>> 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<prctl::PrctlFilter<double>> 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<storm::properties::action::FormulaAction<double>>(formula->getAction(0)).get(), nullptr);
-	ASSERT_NE(std::dynamic_pointer_cast<storm::properties::action::InvertAction<double>>(formula->getAction(1)).get(), nullptr);
-	ASSERT_NE(std::dynamic_pointer_cast<storm::properties::action::BoundAction<double>>(formula->getAction(2)).get(), nullptr);
-	ASSERT_NE(std::dynamic_pointer_cast<storm::properties::action::SortAction<double>>(formula->getAction(3)).get(), nullptr);
-	ASSERT_NE(std::dynamic_pointer_cast<storm::properties::action::RangeAction<double>>(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<prctl::PrctlFilter<double>> 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<prctl::PrctlFilter<double>> formula(nullptr);
-	ASSERT_THROW(
-			formula = storm::parser::PrctlParser::parsePrctlFormula("P > 0.5 [ a ]"),
-			storm::exceptions::WrongFormatException
-	);
-}
-
-TEST(PrctlParserTest, wrongFormulaTest) {
-	std::shared_ptr<prctl::PrctlFilter<double>> formula(nullptr);
-	ASSERT_THROW(
-			formula = storm::parser::PrctlParser::parsePrctlFormula("(a | b) & +"),
-			storm::exceptions::WrongFormatException
-	);
-}
-
-TEST(PrctlParserTest, wrongFormulaTest2) {
-	std::shared_ptr<prctl::PrctlFilter<double>> formula(nullptr);
-	ASSERT_THROW(
-			formula = storm::parser::PrctlParser::parsePrctlFormula("P>0 [ F & a ]"),
-			storm::exceptions::WrongFormatException
-	);
-}