Merged master in parametricSystems.

Former-commit-id: 2fdc349e9d

examples/pdtmc/die/die.pm

@@ -26,8 +26,8 @@ rewards "coin_flips"
 endrewards
 
 label "one" = s=7&d=1;
-//label "two" = s=7&d=2;
-//label "three" = s=7&d=3;
-//label "four" = s=7&d=4;
-//label "five" = s=7&d=5;
-//label "six" = s=7&d=6;
+label "two" = s=7&d=2;
+label "three" = s=7&d=3;
+label "four" = s=7&d=4;
+label "five" = s=7&d=5;
+label "six" = s=7&d=6;

src/counterexamples/SMTMinimalCommandSetGenerator.h

@@ -1691,7 +1691,7 @@ namespace storm {
                     modelCheckingClock = std::chrono::high_resolution_clock::now();
                     commandSet.insert(relevancyInformation.knownLabels.begin(), relevancyInformation.knownLabels.end());
                     storm::models::Mdp<T> subMdp = labeledMdp.restrictChoiceLabels(commandSet);
-                    storm::modelchecker::prctl::SparseMdpPrctlModelChecker<T> modelchecker(subMdp);
+                    storm::modelchecker::SparseMdpPrctlModelChecker<T> modelchecker(subMdp);
                     LOG4CPLUS_DEBUG(logger, "Invoking model checker.");
                     std::vector<T> result = modelchecker.checkUntil(false, phiStates, psiStates, false).first;
                     LOG4CPLUS_DEBUG(logger, "Computed model checking results.");
@@ -1776,20 +1776,20 @@ namespace storm {
                     std::unique_ptr<storm::modelchecker::CheckResult> leftResult = modelchecker.check(untilFormula.getLeftSubformula());
                     std::unique_ptr<storm::modelchecker::CheckResult> rightResult = modelchecker.check(untilFormula.getRightSubformula());
                     
-                    storm::modelchecker::ExplicitQualitativeCheckResult const& leftQualitativeResult = leftResult.asExplicitQualitativeCheckResult();
-                    storm::modelchecker::ExplicitQualitativeCheckResult const& rightQualitativeResult = rightResult.asExplicitQualitativeCheckResult();
+                    storm::modelchecker::ExplicitQualitativeCheckResult const& leftQualitativeResult = leftResult->asExplicitQualitativeCheckResult();
+                    storm::modelchecker::ExplicitQualitativeCheckResult const& rightQualitativeResult = rightResult->asExplicitQualitativeCheckResult();
                     
                     phiStates = leftQualitativeResult.getTruthValuesVector();
                     psiStates = rightQualitativeResult.getTruthValuesVector();
                 } else if (probabilityOperator.getSubformula().isEventuallyFormula()) {
                     storm::logic::EventuallyFormula const& eventuallyFormula = probabilityOperator.getSubformula().asEventuallyFormula();
                     
-                    std::unique_ptr<storm::modelchecker::CheckResult> subResult = modelchecker.check(untilFormula.getSubformula());
+                    std::unique_ptr<storm::modelchecker::CheckResult> subResult = modelchecker.check(eventuallyFormula.getSubformula());
                     
                     storm::modelchecker::ExplicitQualitativeCheckResult const& subQualitativeResult = subResult.asExplicitQualitativeCheckResult();
                     
                     phiStates = storm::storage::BitVector(labeledMdp.getNumberOfStates(), true);
-                    psiStates = subResult.getTruthValuesVector();
+                    psiStates = subResult->getTruthValuesVector();
                 }
                 
                 // Delegate the actual computation work to the function of equal name.

src/modelchecker/AbstractModelChecker.cpp

@@ -166,7 +166,7 @@ namespace storm {
             
             if (stateFormula.hasBound()) {
                 STORM_LOG_THROW(result->isQuantitative(), storm::exceptions::InvalidOperationException, "Unable to perform comparison operation on non-quantitative result.");
-                return result->asQuantativeResult<>().compareAgainstBound(stateFormula.getComparisonType(), stateFormula.getBound());
+                return result->compareAgainstBound(stateFormula.getComparisonType(), stateFormula.getBound());
             } else {
                 return result;
             }
@@ -192,7 +192,7 @@ namespace storm {
             
             if (stateFormula.hasBound()) {
                 STORM_LOG_THROW(result->isQuantitative(), storm::exceptions::InvalidOperationException, "Unable to perform comparison operation on non-quantitative result.");
-                return result->asQuantativeResult().compareAgainstBound(stateFormula.getComparisonType(), stateFormula.getBound());
+                return result->compareAgainstBound(stateFormula.getComparisonType(), stateFormula.getBound());
             } else {
                 return result;
             }
@@ -218,7 +218,7 @@ namespace storm {
             
             if (stateFormula.hasBound()) {
                 STORM_LOG_THROW(result->isQuantitative(), storm::exceptions::InvalidOperationException, "Unable to perform comparison operation on non-quantitative result.");
-                return result->asQuantativeResult().compareAgainstBound(stateFormula.getComparisonType(), stateFormula.getBound());
+                return result->compareAgainstBound(stateFormula.getComparisonType(), stateFormula.getBound());
             } else {
                 return result;
             }

src/modelchecker/CheckResult.cpp

@@ -22,7 +22,11 @@ namespace storm {
         void CheckResult::complement() {
             STORM_LOG_THROW(false, storm::exceptions::InvalidOperationException, "Unable to perform logical 'not' on the check result.");
         }
-                
+        
+        std::unique_ptr<CheckResult> CheckResult::compareAgainstBound(storm::logic::ComparisonType comparisonType, double bound) const {
+            STORM_LOG_THROW(false, storm::exceptions::InvalidOperationException, "Unable to perform comparison against bound on the check result.");
+        }
+        
         bool CheckResult::isExplicit() const {
             return false;
         }

src/modelchecker/CheckResult.h

@@ -21,7 +21,8 @@ namespace storm {
             virtual CheckResult& operator&=(CheckResult const& other);
             virtual CheckResult& operator|=(CheckResult const& other);
             virtual void complement();
-            
+            virtual std::unique_ptr<CheckResult> compareAgainstBound(storm::logic::ComparisonType comparisonType, double bound) const;
+
             virtual bool isExplicit() const;
             virtual bool isQuantitative() const;
             virtual bool isQualitative() const;

src/modelchecker/ExplicitQualitativeCheckResult.cpp

@@ -111,10 +111,18 @@ namespace storm {
                 out << std::boolalpha;
 
                 map_type const& map = boost::get<map_type>(truthValues);
+
+#ifndef WINDOWS
                 typename map_type::const_iterator it = map.begin();
                 typename map_type::const_iterator itPlusOne = map.begin();
                 ++itPlusOne;
                 typename map_type::const_iterator ite = map.end();
+#else
+				map_type::const_iterator it = map.begin();
+				map_type::const_iterator itPlusOne = map.begin();
+				++itPlusOne;
+				map_type::const_iterator ite = map.end();
+#endif
                 
                 for (; it != ite; ++itPlusOne, ++it) {
                     out << it->second;

src/modelchecker/ExplicitQuantitativeCheckResult.cpp

@@ -123,7 +123,7 @@ namespace storm {
         }
         
         template<typename ValueType>
-        std::unique_ptr<CheckResult> ExplicitQuantitativeCheckResult<ValueType>::compareAgainstBound(storm::logic::ComparisonType comparisonType, ValueType const& bound) const {
+        std::unique_ptr<CheckResult> ExplicitQuantitativeCheckResult<ValueType>::compareAgainstBound(storm::logic::ComparisonType comparisonType, double bound) const {
             if (this->isResultForAllStates()) {
                 vector_type const& valuesAsVector = boost::get<vector_type>(values);
                 storm::storage::BitVector result(valuesAsVector.size());
@@ -188,9 +188,9 @@ namespace storm {
         }
         
         template<>
-        std::unique_ptr<CheckResult> ExplicitQuantitativeCheckResult<storm::RationalFunction>::compareAgainstBound(storm::logic::ComparisonType comparisonType, storm::RationalFunction const& bound) const {
+        std::unique_ptr<CheckResult> ExplicitQuantitativeCheckResult<storm::RationalFunction>::compareAgainstBound(storm::logic::ComparisonType comparisonType, double bound) const {
             // Since it is not possible to compare rational functions against bounds, we simply call the base class method.
-            QuantitativeCheckResult::compareAgainstBound(comparisonType, bound);
+            return QuantitativeCheckResult::compareAgainstBound(comparisonType, bound);
         }
         
         template<typename ValueType>

src/modelchecker/ExplicitQuantitativeCheckResult.h

@@ -34,7 +34,7 @@ namespace storm {
             ValueType& operator[](storm::storage::sparse::state_type state);
             ValueType const& operator[](storm::storage::sparse::state_type state) const;
 
-            virtual std::unique_ptr<CheckResult> compareAgainstBound(storm::logic::ComparisonType comparisonType, ValueType const& bound) const override;
+            virtual std::unique_ptr<CheckResult> compareAgainstBound(storm::logic::ComparisonType comparisonType, double bound) const override;
             
             virtual bool isExplicit() const override;
             virtual bool isResultForAllStates() const override;

src/modelchecker/QuantitativeCheckResult.cpp

@@ -8,11 +8,6 @@
 
 namespace storm {
     namespace modelchecker {
-        template<typename ValueType>
-        std::unique_ptr<CheckResult> QuantitativeCheckResult<ValueType>::compareAgainstBound(storm::logic::ComparisonType comparisonType, ValueType const& bound) const {
-            STORM_LOG_THROW(false, storm::exceptions::InvalidOperationException, "Unable to perform comparison against bound on the check result.");
-        }
-        
         template<typename ValueType>
         bool QuantitativeCheckResult<ValueType>::isQuantitative() const {
             return true;

src/modelchecker/QuantitativeCheckResult.h

@@ -8,8 +8,6 @@ namespace storm {
         template<typename ValueType>
         class QuantitativeCheckResult : public CheckResult {
         public:
-            virtual std::unique_ptr<CheckResult> compareAgainstBound(storm::logic::ComparisonType comparisonType, ValueType const& bound) const;
-            
             virtual bool isQuantitative() const override;
         };
     }

src/modelchecker/reachability/SparseDtmcEliminationModelChecker.cpp

@@ -1,6 +1,7 @@
 #include "src/modelchecker/reachability/SparseDtmcEliminationModelChecker.h"
 
 #include <algorithm>
+#include <chrono>
 
 #ifdef PARAMETRIC_SYSTEMS
 #include "src/storage/parameters.h"

src/settings/modules/ParametricSettings.cpp

@@ -7,24 +7,11 @@ namespace storm {
         namespace modules {
             
             const std::string ParametricSettings::moduleName = "parametric";
-            const std::string ParametricSettings::eliminationMethodOptionName = "method";
-            const std::string ParametricSettings::eliminationOrderOptionName = "order";
-            const std::string ParametricSettings::entryStatesLastOptionName = "entrylast";
-            const std::string ParametricSettings::maximalSccSizeOptionName = "sccsize";
             const std::string ParametricSettings::encodeSmt2StrategyOptionName = "smt2strategy";
             const std::string ParametricSettings::exportSmt2DestinationPathOptionName = "smt2path";
             const std::string ParametricSettings::exportResultDestinationPathOptionName = "resultfile";
             
             ParametricSettings::ParametricSettings(storm::settings::SettingsManager& settingsManager) : ModuleSettings(settingsManager, moduleName) {
-                std::vector<std::string> orders = {"fw", "fwrev", "bw", "bwrev", "rand"};
-                this->addOption(storm::settings::OptionBuilder(moduleName, eliminationOrderOptionName, true, "The order that is to be used for the elimination techniques. Available are {fw, fwrev, bw, bwrev, rand}.").addArgument(storm::settings::ArgumentBuilder::createStringArgument("name", "The name of the order in which states are chosen for elimination.").addValidationFunctionString(storm::settings::ArgumentValidators::stringInListValidator(orders)).setDefaultValueString("bw").build()).build());
-
-                std::vector<std::string> methods = {"state", "hybrid"};
-                this->addOption(storm::settings::OptionBuilder(moduleName, eliminationMethodOptionName, true, "The elimination technique to use. Available are {state, hybrid}.").addArgument(storm::settings::ArgumentBuilder::createStringArgument("name", "The name of the elimination technique to use.").addValidationFunctionString(storm::settings::ArgumentValidators::stringInListValidator(methods)).setDefaultValueString("hybrid").build()).build());
-
-                this->addOption(storm::settings::OptionBuilder(moduleName, entryStatesLastOptionName, true, "Sets whether the entry states are eliminated last.").build());
-                this->addOption(storm::settings::OptionBuilder(moduleName, maximalSccSizeOptionName, true, "Sets the maximal size of the SCCs for which state elimination is applied.")
-                                .addArgument(storm::settings::ArgumentBuilder::createUnsignedIntegerArgument("maxsize", "The maximal size of an SCC on which state elimination is applied.").setDefaultValueUnsignedInteger(20).setIsOptional(true).build()).build());
                 this->addOption(storm::settings::OptionBuilder(moduleName, encodeSmt2StrategyOptionName, true, "Set the smt2 encoding strategy.")
                                 .addArgument(storm::settings::ArgumentBuilder::createStringArgument("strategy", "the used strategy").build()).build());
                 this->addOption(storm::settings::OptionBuilder(moduleName, exportSmt2DestinationPathOptionName, true, "A path to a file where the result should be saved.")
@@ -33,42 +20,6 @@ namespace storm {
                                 .addArgument(storm::settings::ArgumentBuilder::createStringArgument("path", "the location.").build()).build());
             }
             
-            ParametricSettings::EliminationMethod ParametricSettings::getEliminationMethod() const {
-                std::string eliminationMethodAsString = this->getOption(eliminationMethodOptionName).getArgumentByName("name").getValueAsString();
-                if (eliminationMethodAsString == "state") {
-                    return EliminationMethod::State;
-                } else if (eliminationMethodAsString == "hybrid") {
-                    return EliminationMethod::Hybrid;
-                } else {
-                    STORM_LOG_ASSERT(false, "Illegal elimination method selected.");
-                }
-            }
-            
-            ParametricSettings::EliminationOrder ParametricSettings::getEliminationOrder() const {
-                std::string eliminationOrderAsString = this->getOption(eliminationOrderOptionName).getArgumentByName("name").getValueAsString();
-                if (eliminationOrderAsString == "fw") {
-                    return EliminationOrder::Forward;
-                } else if (eliminationOrderAsString == "fwrev") {
-                    return EliminationOrder::ForwardReversed;
-                } else if (eliminationOrderAsString == "bw") {
-                    return EliminationOrder::Backward;
-                } else if (eliminationOrderAsString == "bwrev") {
-                    return EliminationOrder::BackwardReversed;
-                } else if (eliminationOrderAsString == "rand") {
-                    return EliminationOrder::Random;
-                } else {
-                    STORM_LOG_ASSERT(false, "Illegal elimination order selected.");
-                }
-            }
-            
-            bool ParametricSettings::isEliminateEntryStatesLastSet() const {
-                return this->getOption(entryStatesLastOptionName).getHasOptionBeenSet();
-            }
-            
-            uint_fast64_t ParametricSettings::getMaximalSccSize() const {
-                return this->getOption(maximalSccSizeOptionName).getArgumentByName("maxsize").getValueAsUnsignedInteger();
-            }
-            
             bool ParametricSettings::exportResultToFile() const {
                 return this->getOption(exportResultDestinationPathOptionName).getHasOptionBeenSet();
             }

src/settings/modules/ParametricSettings.h

@@ -21,16 +21,6 @@ namespace storm {
 				 * RATIONAL_FUNCTION: The smt file should contain only the rational function.
 				 */
 				enum class Smt2EncodingStrategy {FULL_TRANSITION_SYSTEM, ONLY_SCC_ENTRY_STATES, HIGH_INDEGREE, RATIONAL_FUNCTION};
-				
-                /*!
-                 * An enum that contains all available state elimination orders.
-                 */
-                enum class EliminationOrder { Forward, ForwardReversed, Backward, BackwardReversed, Random };
-				
-                /*!
-                 * An enum that contains all available techniques to solve parametric systems.
-                 */
-                enum class EliminationMethod { State, Scc, Hybrid};
                 
                 /*!
                  * Creates a new set of parametric model checking settings that is managed by the given manager.
@@ -38,34 +28,6 @@ namespace storm {
                  * @param settingsManager The responsible manager.
                  */
                 ParametricSettings(storm::settings::SettingsManager& settingsManager);
-                
-                /*!
-                 * Retrieves the selected elimination method.
-                 *
-                 * @return The selected elimination method.
-                 */
-                EliminationMethod getEliminationMethod() const;
-                
-                /*!
-                 * Retrieves the selected elimination order.
-                 *
-                 * @return The selected elimination order.
-                 */
-                EliminationOrder getEliminationOrder() const;
-                
-                /*!
-                 * Retrieves whether the option to eliminate entry states in the very end is set.
-                 *
-                 * @return True iff the option is set.
-                 */
-                bool isEliminateEntryStatesLastSet() const;
-                
-                /*!
-                 * Retrieves the maximal size of an SCC on which state elimination is to be directly applied.
-                 *
-                 * @return The maximal size of an SCC on which state elimination is to be directly applied.
-                 */
-                uint_fast64_t getMaximalSccSize() const;
 				
 				/**
 				 * Retrieves whether the model checking result should be exported to a file.
@@ -100,10 +62,6 @@ namespace storm {
                 const static std::string moduleName;
                 
             private:
-                const static std::string eliminationMethodOptionName;
-                const static std::string eliminationOrderOptionName;
-                const static std::string entryStatesLastOptionName;
-                const static std::string maximalSccSizeOptionName;
 				const static std::string encodeSmt2StrategyOptionName;
 				const static std::string exportSmt2DestinationPathOptionName;
 				const static std::string exportResultDestinationPathOptionName;

src/solver/MathsatSmtSolver.cpp

@@ -191,6 +191,7 @@ namespace storm {
 #endif
 		}
 
+#ifndef WINDOWS
 		SmtSolver::CheckResult MathsatSmtSolver::checkWithAssumptions(std::initializer_list<storm::expressions::Expression> const& assumptions)
 		{
 #ifdef STORM_HAVE_MSAT
@@ -218,6 +219,7 @@ namespace storm {
 			STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "StoRM is compiled without MathSAT support.");
 #endif
 		}
+#endif
 
 		storm::expressions::SimpleValuation MathsatSmtSolver::getModelAsValuation()
 		{

src/solver/MathsatSmtSolver.h

@@ -79,7 +79,9 @@ namespace storm {
 
 			virtual CheckResult checkWithAssumptions(std::set<storm::expressions::Expression> const& assumptions) override;
 
+#ifndef WINDOWS
 			virtual CheckResult checkWithAssumptions(std::initializer_list<storm::expressions::Expression> const& assumptions) override;
+#endif
 
 			virtual storm::expressions::SimpleValuation getModelAsValuation() override;
 

src/solver/SmtSolver.h

@@ -70,9 +70,15 @@ namespace storm {
 			virtual ~SmtSolver();
             
 			SmtSolver(SmtSolver const& other) = default;
+
+#ifndef WINDOWS
 			SmtSolver(SmtSolver&& other) = default;
+#endif
 			SmtSolver& operator=(SmtSolver const& other) = default;
+
+#ifndef WINDOWS
 			SmtSolver& operator=(SmtSolver&& other) = default;
+#endif
             
 			/*!
              * Pushes a backtracking point on the solver's stack. A following call to pop() deletes exactly those
@@ -146,8 +152,10 @@ namespace storm {
              * @param assumptions The assumptions to add to the call.
              * @return Sat if the conjunction of the asserted expressions together with the provided assumptions is
              * satisfiable, Unsat if it is unsatisfiable and Unknown if the solver could not determine satisfiability.
-             */
+			 */
+#ifndef WINDOWS
 			virtual CheckResult checkWithAssumptions(std::initializer_list<storm::expressions::Expression> const& assumptions) = 0;
+#endif
             
 			/*!
              * If the last call to check() or checkWithAssumptions() returned Sat, this method retrieves a model that

src/solver/Z3SmtSolver.cpp

@@ -155,6 +155,7 @@ namespace storm {
 #endif
 		}
 
+#ifndef WINDOWS
 		SmtSolver::CheckResult Z3SmtSolver::checkWithAssumptions(std::initializer_list<storm::expressions::Expression> const& assumptions)
 		{
 #ifdef STORM_HAVE_Z3
@@ -181,7 +182,7 @@ namespace storm {
 			STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "StoRM is compiled without Z3 support.");
 #endif
 		}
-
+#endif
 		storm::expressions::SimpleValuation Z3SmtSolver::getModelAsValuation()
 		{
 #ifdef STORM_HAVE_Z3
@@ -229,7 +230,7 @@ namespace storm {
 		{
 #ifdef STORM_HAVE_Z3
 			std::vector<storm::expressions::SimpleValuation> valuations;
-			this->allSat(important, [&valuations](storm::expressions::SimpleValuation const& valuation) -> bool { valuations.push_back(valuation); return true; });
+			this->allSat(important, static_cast<std::function<bool(storm::expressions::SimpleValuation&)>>([&valuations](storm::expressions::SimpleValuation const& valuation) -> bool { valuations.push_back(valuation); return true; }));
 			return valuations;
 #else
 			STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "StoRM is compiled without Z3 support.");

src/solver/Z3SmtSolver.h

@@ -51,7 +51,9 @@ namespace storm {
 
 			virtual CheckResult checkWithAssumptions(std::set<storm::expressions::Expression> const& assumptions) override;
 
+#ifndef WINDOWS
 			virtual CheckResult checkWithAssumptions(std::initializer_list<storm::expressions::Expression> const& assumptions) override;
+#endif
 
 			virtual storm::expressions::SimpleValuation getModelAsValuation() override;
             

src/storage/expressions/Expression.h

@@ -325,4 +325,14 @@ namespace storm {
     }
 }
 
+//specialize 
+namespace std {
+	template<>
+	struct less < storm::expressions::Expression > {
+		bool operator()(const storm::expressions::Expression& lhs, const storm::expressions::Expression& rhs) const {
+			return lhs.getBaseExpressionPointer() < rhs.getBaseExpressionPointer();
+		}
+	};
+}
+
 #endif /* STORM_STORAGE_EXPRESSIONS_EXPRESSION_H_ */

src/storage/expressions/LinearCoefficientVisitor.h

@@ -18,8 +18,10 @@ namespace storm {
 
                 VariableCoefficients(VariableCoefficients const& other) = default;
                 VariableCoefficients& operator=(VariableCoefficients const& other) = default;
+#ifndef WINDOWS
                 VariableCoefficients(VariableCoefficients&& other) = default;
                 VariableCoefficients& operator=(VariableCoefficients&& other) = default;
+#endif
                 
                 VariableCoefficients& operator+=(VariableCoefficients&& other);
                 VariableCoefficients& operator-=(VariableCoefficients&& other);

src/stormParametric.cpp

@@ -2,6 +2,7 @@
 #include "storm-config.h"
 
 #include <tuple>
+#include <sstream>
 
 // Include other headers.
 #include "src/exceptions/BaseException.h"
@@ -12,10 +13,9 @@
 
 //#include "src/modelchecker/reachability/DirectEncoding.h"
 #include "src/storage/DeterministicModelBisimulationDecomposition.h"
-#include "src/modelchecker/reachability/SparseSccModelChecker.h"
+#include "src/modelchecker/reachability/SparseDtmcEliminationModelChecker.h"
 #include "src/storage/parameters.h"
 #include "src/models/Dtmc.h"
-#include "src/properties/prctl/PrctlFilter.h"
 
 //std::tuple<storm::RationalFunction, boost::optional<storm::storage::SparseMatrix<storm::RationalFunction>>, boost::optional<std::vector<storm::RationalFunction>>, boost::optional<storm::storage::BitVector>, boost::optional<double>, boost::optional<bool>> computeReachabilityProbability(storm::models::Dtmc<storm::RationalFunction> const& dtmc, std::shared_ptr<storm::properties::prctl::PrctlFilter<double>> const& filterFormula) {
 //    // The first thing we need to do is to make sure the formula is of the correct form and - if so - extract
@@ -145,7 +145,14 @@ void check() {
     std::string const& programFile = storm::settings::generalSettings().getSymbolicModelFilename();
     std::string const& constants = storm::settings::generalSettings().getConstantDefinitionString();
     storm::prism::Program program = storm::parser::PrismParser::parse(programFile);
-    std::shared_ptr<storm::models::AbstractModel<ValueType>> model = storm::builder::ExplicitPrismModelBuilder<ValueType>::translateProgram(program, true, false, storm::settings::generalSettings().isSymbolicRewardModelNameSet() ? storm::settings::generalSettings().getSymbolicRewardModelName() : "", constants);
+
+    STORM_LOG_THROW(storm::settings::generalSettings().isPropertySet(), storm::exceptions::InvalidSettingsException, "Unable to perform model checking without a property.");
+    std::shared_ptr<storm::logic::Formula> formula = storm::parser::FormulaParser(program.getManager().getSharedPointer()).parseFromString(storm::settings::generalSettings().getProperty());
+    
+    typename storm::builder::ExplicitPrismModelBuilder<ValueType>::Options options(*formula);
+    options.addConstantDefinitionsFromString(program, storm::settings::generalSettings().getConstantDefinitionString());
+    
+    std::shared_ptr<storm::models::AbstractModel<ValueType>> model = storm::builder::ExplicitPrismModelBuilder<ValueType>::translateProgram(program, options);
     
     model->printModelInformationToStream(std::cout);
     
@@ -155,47 +162,57 @@ void check() {
     
     std::shared_ptr<storm::models::Dtmc<ValueType>> dtmc = model->template as<storm::models::Dtmc<ValueType>>();
         
-    STORM_LOG_THROW(storm::settings::generalSettings().isPctlPropertySet(), storm::exceptions::InvalidSettingsException, "Unable to perform model checking without a property.");
-    std::shared_ptr<storm::properties::prctl::PrctlFilter<double>> filterFormula = storm::parser::PrctlParser::parsePrctlFormula(storm::settings::generalSettings().getPctlProperty());
-    std::cout << "Checking formula " << *filterFormula << std::endl;
+    storm::modelchecker::SparseDtmcEliminationModelChecker<ValueType> modelchecker(*dtmc);
+    STORM_LOG_THROW(modelchecker.canHandle(*formula), storm::exceptions::InvalidPropertyException, "Model checker cannot handle the property: '" << *formula << "'.");
     
-    bool checkRewards = false;
-    std::shared_ptr<storm::properties::prctl::Ap<double>> phiStateFormulaApFormula = nullptr;
-    std::shared_ptr<storm::properties::prctl::Ap<double>> psiStateFormulaApFormula = nullptr;
+    std::cout << "Checking formula " << *formula << std::endl;
     
-    // The first thing we need to do is to make sure the formula is of the correct form.
-    std::shared_ptr<storm::properties::prctl::Until<double>> untilFormula = std::dynamic_pointer_cast<storm::properties::prctl::Until<double>>(filterFormula->getChild());
-    std::shared_ptr<storm::properties::prctl::AbstractStateFormula<double>> phiStateFormula;
-    std::shared_ptr<storm::properties::prctl::AbstractStateFormula<double>> psiStateFormula;
-    if (untilFormula) {
-        phiStateFormula = untilFormula->getLeft();
-        psiStateFormula = untilFormula->getRight();
-    } else {
-        std::shared_ptr<storm::properties::prctl::Eventually<double>> eventuallyFormula = std::dynamic_pointer_cast<storm::properties::prctl::Eventually<double>>(filterFormula->getChild());
-        if (eventuallyFormula) {
-            
-            phiStateFormula = std::shared_ptr<storm::properties::prctl::Ap<double>>(new storm::properties::prctl::Ap<double>("true"));
-            psiStateFormula = eventuallyFormula->getChild();
-        } else {
-            std::shared_ptr<storm::properties::prctl::ReachabilityReward<double>> reachabilityRewardFormula = std::dynamic_pointer_cast<storm::properties::prctl::ReachabilityReward<double>>(filterFormula->getChild());
-            
-            STORM_LOG_THROW(reachabilityRewardFormula, storm::exceptions::InvalidPropertyException, "Illegal formula " << *filterFormula << " for parametric model checking. Note that only unbounded reachability properties (probabilities/rewards) are admitted.");
-            phiStateFormula = std::shared_ptr<storm::properties::prctl::Ap<double>>(new storm::properties::prctl::Ap<double>("true"));
-            psiStateFormula = reachabilityRewardFormula->getChild();
-            checkRewards = true;
+    bool checkRewards = formula->isRewardOperatorFormula();
+    
+    std::string phiLabel;
+    std::string psiLabel;
+    
+    bool measureDrivenBisimulation = false;
+    if (formula->isProbabilityOperatorFormula()) {
+        storm::logic::Formula const& subformula = formula->asProbabilityOperatorFormula().getSubformula();
+        
+        if (subformula.isEventuallyFormula()) {
+            phiLabel = "true";
+            std::stringstream stream;
+            stream << subformula.asEventuallyFormula().getSubformula();
+            psiLabel = stream.str();
+            measureDrivenBisimulation = true;
+        } else if (subformula.isUntilFormula()) {
+            std::stringstream stream;
+            stream << subformula.asUntilFormula().getLeftSubformula();
+            phiLabel = stream.str();
+
+            std::stringstream stream2;
+            stream2 << subformula.asUntilFormula().getRightSubformula();
+            psiLabel = stream2.str();
+            measureDrivenBisimulation = true;
+        }
+    } else if (formula->isRewardOperatorFormula()) {
+        storm::logic::Formula const& subformula = formula->asRewardOperatorFormula().getSubformula();
+        
+        if (subformula.isReachabilityRewardFormula()) {
+            phiLabel = "true";
+            std::stringstream stream;
+            stream << subformula.asReachabilityRewardFormula().getSubformula();
+            psiLabel = stream.str();
+            measureDrivenBisimulation = true;
         }
     }
     
-    // Now we need to make sure the formulas defining the phi and psi states are just labels.
-    phiStateFormulaApFormula = std::dynamic_pointer_cast<storm::properties::prctl::Ap<double>>(phiStateFormula);
-    psiStateFormulaApFormula = std::dynamic_pointer_cast<storm::properties::prctl::Ap<double>>(psiStateFormula);
-    STORM_LOG_THROW(phiStateFormulaApFormula, storm::exceptions::InvalidPropertyException, "Illegal formula " << *phiStateFormula << " for parametric model checking. Note that only atomic propositions are admitted in that position.");
-    STORM_LOG_THROW(psiStateFormulaApFormula, storm::exceptions::InvalidPropertyException, "Illegal formula " << *psiStateFormula << " for parametric model checking. Note that only atomic propositions are admitted in that position.");
-    
     // Perform bisimulation minimization if requested.
     if (storm::settings::generalSettings().isBisimulationSet()) {
-        storm::storage::DeterministicModelBisimulationDecomposition<ValueType> bisimulationDecomposition(*dtmc, phiStateFormulaApFormula->getAp(), psiStateFormulaApFormula->getAp(), checkRewards, storm::settings::bisimulationSettings().isWeakBisimulationSet(), false, true);
-        dtmc = bisimulationDecomposition.getQuotient()->template as<storm::models::Dtmc<ValueType>>();
+        if (measureDrivenBisimulation) {
+            storm::storage::DeterministicModelBisimulationDecomposition<ValueType> bisimulationDecomposition(*dtmc, phiLabel, psiLabel, checkRewards, storm::settings::bisimulationSettings().isWeakBisimulationSet(), false, true);
+            dtmc = bisimulationDecomposition.getQuotient()->template as<storm::models::Dtmc<ValueType>>();
+        } else {
+            storm::storage::DeterministicModelBisimulationDecomposition<ValueType> bisimulationDecomposition(*dtmc, boost::optional<std::set<std::string>>(), checkRewards, storm::settings::bisimulationSettings().isWeakBisimulationSet(), true);
+            dtmc = bisimulationDecomposition.getQuotient()->template as<storm::models::Dtmc<ValueType>>();
+        }
         
         dtmc->printModelInformationToStream(std::cout);
     }
@@ -205,15 +222,14 @@ void check() {
 //    storm::modelchecker::reachability::CollectConstraints<ValueType> constraintCollector;
 //    constraintCollector(*dtmc);
     
-    storm::modelchecker::reachability::SparseSccModelChecker<ValueType> modelchecker;
-    
-    ValueType valueFunction = modelchecker.computeConditionalProbability(*dtmc, phiStateFormulaApFormula, psiStateFormulaApFormula);
     
-    //        storm::RationalFunction valueFunction = checkRewards ? modelchecker.computeReachabilityReward(*dtmc, phiStateFormulaApFormula, psiStateFormulaApFormula) : modelchecker.computeReachabilityProbability(*dtmc, phiStateFormulaApFormula, psiStateFormulaApFormula);
-    
-    STORM_PRINT_AND_LOG(std::endl << "Result: " << valueFunction << std::endl);
+    std::unique_ptr<storm::modelchecker::CheckResult> result = modelchecker.check(*formula);
+
+    // Report the result.
+    STORM_PRINT_AND_LOG(std::endl << "Result: " << std::endl);
+    result->writeToStream(std::cout, model->getInitialStates());
     if (std::is_same<ValueType, storm::RationalFunction>::value) {
-        printApproximateResult(valueFunction);
+        printApproximateResult(result->asExplicitQuantitativeCheckResult<ValueType>()[*model->getInitialStates().begin()]);
     }
 }