refactoring up to tests done

Former-commit-id: 943a396fab

src/cli/entrypoints.h

@@ -55,27 +55,44 @@ namespace storm {
         
         template<typename ValueType>
         void verifySymbolicModelWithExplorationEngine(storm::prism::Program const& program, std::vector<std::shared_ptr<storm::logic::Formula const>> const& formulas, bool onlyInitialStatesRelevant = false) {
-            
+            STORM_LOG_THROW(program.getModelType() == storm::prism::Program::ModelType::DTMC || program.getModelType() == storm::prism::Program::ModelType::MDP, storm::exceptions::InvalidSettingsException, "Currently exploration-based verification is only available for DTMCs and MDPs.");
+
             for (auto const& formula : formulas) {
-                STORM_LOG_THROW(program.getModelType() == storm::prism::Program::ModelType::DTMC || program.getModelType() == storm::prism::Program::ModelType::MDP, storm::exceptions::InvalidSettingsException, "Currently exploration-based verification is only available for DTMCs and MDPs.");
                 std::cout << std::endl << "Model checking property: " << *formula << " ...";
-                
-                storm::modelchecker::SparseExplorationModelChecker<ValueType> checker(program);
-
-                storm::modelchecker::CheckTask<storm::logic::Formula> task(*formula, onlyInitialStatesRelevant);
+                bool supportFormula;
                 std::unique_ptr<storm::modelchecker::CheckResult> result;
-                if (checker.canHandle(task)) {
-                    result = checker.check(task);
-                    if (result) {
-                        std::cout << " done." << std::endl;
-                        std::cout << "Result (initial states): ";
-                        std::cout << *result << std::endl;
-                    } else {
-                        std::cout << " skipped, because the modelling formalism is currently unsupported." << std::endl;
+
+                if(program.getModelType() == storm::prism::Program::ModelType::DTMC) {
+                    storm::modelchecker::SparseExplorationModelChecker<storm::models::sparse::Dtmc<ValueType>> checker(program);
+                    storm::modelchecker::CheckTask<storm::logic::Formula> task(*formula, onlyInitialStatesRelevant);
+
+                    supportFormula = checker.canHandle(task);
+                    if (supportFormula) {
+                        result = checker.check(task);
+                    }
+                } else if(program.getModelType() == storm::prism::Program::ModelType::MDP) {
+                    storm::modelchecker::SparseExplorationModelChecker<storm::models::sparse::Mdp<ValueType>> checker(program);
+                    storm::modelchecker::CheckTask<storm::logic::Formula> task(*formula, onlyInitialStatesRelevant);
+
+                    supportFormula = checker.canHandle(task);
+                    if (supportFormula) {
+                        result = checker.check(task);
                     }
                 } else {
+                    // Should be catched before.
+                    assert(false);
+                }
+                if(!supportFormula) {
                     std::cout << " skipped, because the formula cannot be handled by the selected engine/method." << std::endl;
                 }
+
+                if (result) {
+                    std::cout << " done." << std::endl;
+                    std::cout << "Result (initial states): ";
+                    std::cout << *result << std::endl;
+                } else {
+                    std::cout << " skipped, because the modelling formalism is currently unsupported." << std::endl;
+                }
             }
         }
         

src/logic/Bound.h

@@ -12,10 +12,10 @@ namespace storm {
                 // Intentionally left empty.
             }
 
-            //template<typename OtherValueType>
-            //Bound<OtherValueType> convertToOtherValueType() const {
-            //    return Bound<OtherValueType>(comparisonType, storm::utility::convertNumber<OtherValueType>(threshold));
-            //}
+            template<typename OtherValueType>
+            Bound<OtherValueType> convertToOtherValueType() const {
+                return Bound<OtherValueType>(comparisonType, storm::utility::convertNumber<OtherValueType>(threshold));
+            }
             
             ComparisonType comparisonType;
             ValueType threshold;

src/utility/constants.cpp

@@ -165,6 +165,11 @@ namespace storm {
         RationalFunction convertNumber(double const& number){
             return RationalFunction(carl::rationalize<RationalNumber>(number));
         }
+
+        template<>
+        RationalFunction convertNumber(RationalNumber const& number) {
+            return RationalFunction(number);
+        }
         
         template<>
         storm::RationalNumber abs(storm::RationalNumber const& number) {

src/utility/storm.h

@@ -370,7 +370,7 @@ namespace storm {
 
     template<>
     inline std::unique_ptr<storm::modelchecker::CheckResult> verifySparseModel(std::shared_ptr<storm::models::sparse::Model<storm::RationalFunction>> model, std::shared_ptr<storm::logic::Formula const> const& formula, bool onlyInitialStatesRelevant) {
-        storm::modelchecker::CheckTask<storm::logic::Formula, storm::RationalNumber> task(*formula, onlyInitialStatesRelevant);
+        storm::modelchecker::CheckTask<storm::logic::Formula, storm::RationalFunction> task(*formula, onlyInitialStatesRelevant);
 
         std::unique_ptr<storm::modelchecker::CheckResult> result;
         if (model->getType() == storm::models::ModelType::Dtmc) {