Refactored part of the API / more functions

Former-commit-id: eb8deb537c

src/cli/cli.cpp

@@ -214,27 +214,20 @@ namespace storm {
                 boost::optional<storm::prism::Program> program;
                 if (settings.isSymbolicSet()) {
                     std::string const& programFile = settings.getSymbolicModelFilename();
-                    program = storm::parser::PrismParser::parse(programFile).simplify().simplify();
-                    
-                    program->checkValidity();
+                    program = storm::parseProgram(programFile);
                 }
                 
                 // Then proceed to parsing the property (if given), since the model we are building may depend on the property.
                 std::vector<std::shared_ptr<storm::logic::Formula>> formulas;
                 if (settings.isPropertySet()) {
-                    storm::parser::FormulaParser formulaParser;
-                    if (program) {
-                        formulaParser = storm::parser::FormulaParser(program.get().getManager().getSharedPointer());
-                    }
+                    std::string properties = settings.getProperty();
                     
-                    // If the given property looks like a file (containing a dot and there exists a file with that name),
-                    // we try to parse it as a file, otherwise we assume it's a property.
-                    std::string property = settings.getProperty();
-                    if (property.find(".") != std::string::npos && std::ifstream(property).good()) {
-                        formulas = formulaParser.parseFromFile(settings.getProperty());
+                    if(program) {
+                        formulas = storm::parseFormulasForProgram(properties, program.get());
                     } else {
-                        formulas = formulaParser.parseFromString(settings.getProperty());
+                        formulas = storm::parseFormulasForExplicit(properties);
                     }
+                    
                 }
 
                 if (settings.isSymbolicSet()) {

src/parser/FormulaParser.cpp

@@ -184,13 +184,13 @@ namespace storm {
             return *this;
         }
         
-        std::shared_ptr<storm::logic::Formula> FormulaParser::parseSingleFormulaFromString(std::string const& formulaString) {
+        std::shared_ptr<storm::logic::Formula> FormulaParser::parseSingleFormulaFromString(std::string const& formulaString) const {
             std::vector<std::shared_ptr<storm::logic::Formula>> formulas = parseFromString(formulaString);
             STORM_LOG_THROW(formulas.size() == 1, storm::exceptions::WrongFormatException, "Expected exactly one formula, but found " << formulas.size() << " instead.");
             return formulas.front();
         }
         
-        std::vector<std::shared_ptr<storm::logic::Formula>> FormulaParser::parseFromFile(std::string const& filename) {
+        std::vector<std::shared_ptr<storm::logic::Formula>> FormulaParser::parseFromFile(std::string const& filename) const {
             // Open file and initialize result.
             std::ifstream inputFileStream(filename, std::ios::in);
             STORM_LOG_THROW(inputFileStream.good(), storm::exceptions::WrongFormatException, "Unable to read from file '" << filename << "'.");
@@ -212,7 +212,7 @@ namespace storm {
             return formulas;
         }
         
-        std::vector<std::shared_ptr<storm::logic::Formula>> FormulaParser::parseFromString(std::string const& formulaString) {
+        std::vector<std::shared_ptr<storm::logic::Formula>> FormulaParser::parseFromString(std::string const& formulaString) const {
             PositionIteratorType first(formulaString.begin());
             PositionIteratorType iter = first;
             PositionIteratorType last(formulaString.end());

src/parser/FormulaParser.h

@@ -28,7 +28,7 @@ namespace storm {
              * @param formulaString The formula as a string.
              * @return The resulting formula.
              */
-            std::shared_ptr<storm::logic::Formula> parseSingleFormulaFromString(std::string const& formulaString);
+            std::shared_ptr<storm::logic::Formula> parseSingleFormulaFromString(std::string const& formulaString) const;
             
             /*!
              * Parses the formula given by the provided string.
@@ -36,7 +36,7 @@ namespace storm {
              * @param formulaString The formula as a string.
              * @return The contained formulas.
              */
-            std::vector<std::shared_ptr<storm::logic::Formula>> parseFromString(std::string const& formulaString);
+            std::vector<std::shared_ptr<storm::logic::Formula>> parseFromString(std::string const& formulaString) const;
             
             /*!
              * Parses the formulas in the given file.
@@ -44,7 +44,7 @@ namespace storm {
              * @param filename The name of the file to parse.
              * @return The contained formulas.
              */
-            std::vector<std::shared_ptr<storm::logic::Formula>> parseFromFile(std::string const& filename);
+            std::vector<std::shared_ptr<storm::logic::Formula>> parseFromFile(std::string const& filename) const;
             
             /*!
              * Adds an identifier and the expression it is supposed to be replaced with. This can, for example be used

src/utility/storm.cpp

@@ -0,0 +1,41 @@
+#include "storm.h"
+
+// Headers related to parsing.
+#include "src/parser/PrismParser.h"
+#include "src/parser/FormulaParser.h"
+
+
+
+namespace storm {
+   
+     storm::prism::Program parseProgram(std::string const& path) {
+        storm::prism::Program program= storm::parser::PrismParser::parse(path).simplify().simplify();
+        program.checkValidity();
+        return program;
+    }
+     
+    /**
+     * Helper
+     * @param FormulaParser
+     * @return The formulas.
+     */
+    std::vector<std::shared_ptr<storm::logic::Formula>> parseFormulas(storm::parser::FormulaParser & formulaParser, std::string const& inputString) {
+        // If the given property looks like a file (containing a dot and there exists a file with that name),
+        // we try to parse it as a file, otherwise we assume it's a property.
+        if (inputString.find(".") != std::string::npos && std::ifstream(inputString).good()) {
+            return formulaParser.parseFromFile(inputString);
+        } else {
+            return formulaParser.parseFromString(inputString);
+        }
+    }
+
+    std::vector<std::shared_ptr<storm::logic::Formula>> parseFormulasForExplicit(std::string const& inputString)    {
+        storm::parser::FormulaParser formulaParser;
+        return parseFormulas(formulaParser, inputString);
+    }
+
+    std::vector<std::shared_ptr<storm::logic::Formula>> parseFormulasForProgram(std::string const& inputString, storm::prism::Program const& program) {
+        storm::parser::FormulaParser formulaParser(program.getManager().getSharedPointer());
+        return parseFormulas(formulaParser, inputString);
+    } 
+}

src/utility/storm.h

@@ -22,10 +22,6 @@
 #include "src/settings/modules/BisimulationSettings.h"
 #include "src/settings/modules/ParametricSettings.h"
 
-// Headers related to parsing.
-#include "src/parser/AutoParser.h"
-#include "src/parser/PrismParser.h"
-#include "src/parser/FormulaParser.h"
 
 // Formula headers.
 #include "src/logic/Formulas.h"
@@ -40,6 +36,8 @@
 #include "src/storage/dd/CuddAdd.h"
 #include "src/storage/dd/CuddBdd.h"
 
+#include "src/parser/AutoParser.h"
+
 // Headers of builders.
 #include "src/builder/ExplicitPrismModelBuilder.h"
 #include "src/builder/DdPrismModelBuilder.h"
@@ -79,6 +77,12 @@ namespace storm {
        return storm::parser::AutoParser::parseModel(transitionsFile, labelingFile, stateRewardsFile ? stateRewardsFile.get() : "", transitionRewardsFile ? transitionRewardsFile.get() : "");
    }
             
+    storm::prism::Program parseProgram(std::string const& path);
+    std::vector<std::shared_ptr<storm::logic::Formula>> parseFormulasForExplicit(std::string const& inputString);
+    std::vector<std::shared_ptr<storm::logic::Formula>> parseFormulasForProgram(std::string const& inputString, storm::prism::Program const& program);
+            
+ 
+ 
     template<typename ValueType>
     std::shared_ptr<storm::models::ModelBase> buildSymbolicModel(storm::prism::Program const& program, std::vector<std::shared_ptr<storm::logic::Formula>> const& formulas) {
         std::shared_ptr<storm::models::ModelBase> result(nullptr);
@@ -92,7 +96,7 @@ namespace storm {
         if (settings.getEngine() == storm::settings::modules::GeneralSettings::Engine::Sparse) {
             typename storm::builder::ExplicitPrismModelBuilder<ValueType>::Options options;
             options = typename storm::builder::ExplicitPrismModelBuilder<ValueType>::Options(formulas);
-                    options.addConstantDefinitionsFromString(program, settings.getConstantDefinitionString());
+            options.addConstantDefinitionsFromString(program, constants);
 
             // Generate command labels if we are going to build a counterexample later.
             if (storm::settings::counterexampleGeneratorSettings().isMinimalCommandSetGenerationSet()) {
@@ -103,7 +107,7 @@ namespace storm {
         } else if (settings.getEngine() == storm::settings::modules::GeneralSettings::Engine::Dd || settings.getEngine() == storm::settings::modules::GeneralSettings::Engine::Hybrid) {
             typename storm::builder::DdPrismModelBuilder<storm::dd::DdType::CUDD>::Options options;
             options = typename storm::builder::DdPrismModelBuilder<storm::dd::DdType::CUDD>::Options(formulas);
-                    options.addConstantDefinitionsFromString(program, settings.getConstantDefinitionString());
+            options.addConstantDefinitionsFromString(program, constants);
 
             result = storm::builder::DdPrismModelBuilder<storm::dd::DdType::CUDD>::translateProgram(program, options);
         }
@@ -169,15 +173,9 @@ namespace storm {
 #endif
             
     template<typename ValueType>
-            void verifySparseModel(boost::optional<storm::prism::Program> const& program, std::shared_ptr<storm::models::sparse::Model<ValueType>> model, std::vector<std::shared_ptr<storm::logic::Formula>> const& formulas) {
-                storm::settings::modules::GeneralSettings const& settings = storm::settings::generalSettings();
-                
+    void verifySparseModel(std::shared_ptr<storm::models::sparse::Model<ValueType>> model, std::vector<std::shared_ptr<storm::logic::Formula>> const& formulas) {
         for (auto const& formula : formulas) {
-                    // If we were requested to generate a counterexample, we now do so.
-                    if (settings.isCounterexampleSet()) {
-                        STORM_LOG_THROW(program, storm::exceptions::InvalidSettingsException, "Unable to generate counterexample for non-symbolic model.");
-                        generateCounterexample<ValueType>(program.get(), model, formula);
-                    } else {
+
             std::cout << std::endl << "Model checking property: " << *formula << " ...";
             std::unique_ptr<storm::modelchecker::CheckResult> result;
             if (model->getType() == storm::models::ModelType::Dtmc) {
@@ -222,7 +220,6 @@ namespace storm {
             }
         }
     }
-            }
             
 #ifdef STORM_HAVE_CARL
     inline void exportParametricResultToFile(storm::RationalFunction const& result, storm::models::sparse::Dtmc<storm::RationalFunction>::ConstraintCollector const& constraintCollector, std::string const& path) {
@@ -242,7 +239,7 @@ namespace storm {
     }
             
     template<>
-            inline void verifySparseModel(boost::optional<storm::prism::Program> const& program, std::shared_ptr<storm::models::sparse::Model<storm::RationalFunction>> model, std::vector<std::shared_ptr<storm::logic::Formula>> const& formulas) {
+    inline void verifySparseModel(std::shared_ptr<storm::models::sparse::Model<storm::RationalFunction>> model, std::vector<std::shared_ptr<storm::logic::Formula>> const& formulas) {
 
         for (auto const& formula : formulas) {
             STORM_LOG_THROW(model->getType() == storm::models::ModelType::Dtmc, storm::exceptions::InvalidSettingsException, "Currently parametric verification is only available for DTMCs.");
@@ -276,7 +273,7 @@ namespace storm {
 #endif
             
     template<storm::dd::DdType DdType>
-            void verifySymbolicModelWithHybridEngine(boost::optional<storm::prism::Program> const& program, std::shared_ptr<storm::models::symbolic::Model<DdType>> model, std::vector<std::shared_ptr<storm::logic::Formula>> const& formulas) {
+    void verifySymbolicModelWithHybridEngine(std::shared_ptr<storm::models::symbolic::Model<DdType>> model, std::vector<std::shared_ptr<storm::logic::Formula>> const& formulas) {
         for (auto const& formula : formulas) {
             std::cout << std::endl << "Model checking property: " << *formula << " ...";
             std::unique_ptr<storm::modelchecker::CheckResult> result;
@@ -314,7 +311,7 @@ namespace storm {
     }
             
     template<storm::dd::DdType DdType>
-            void verifySymbolicModelWithSymbolicEngine(boost::optional<storm::prism::Program> const& program, std::shared_ptr<storm::models::symbolic::Model<DdType>> model, std::vector<std::shared_ptr<storm::logic::Formula>> const& formulas) {
+    void verifySymbolicModelWithSymbolicEngine(std::shared_ptr<storm::models::symbolic::Model<DdType>> model, std::vector<std::shared_ptr<storm::logic::Formula>> const& formulas) {
         for (auto const& formula : formulas) {
             std::cout << std::endl << "Model checking property: " << *formula << " ...";
             std::unique_ptr<storm::modelchecker::CheckResult> result;
@@ -345,12 +342,10 @@ namespace storm {
         }
     }
             
-            template<typename ValueType>
-            void buildAndCheckSymbolicModel(boost::optional<storm::prism::Program> const& program, std::vector<std::shared_ptr<storm::logic::Formula>> const& formulas) {
-                // Now we are ready to actually build the model.
-                STORM_LOG_THROW(program, storm::exceptions::InvalidStateException, "Program has not been successfully parsed.");
-                std::shared_ptr<storm::models::ModelBase> model = buildSymbolicModel<ValueType>(program.get(), formulas);
      
+    template<typename ValueType>
+    void buildAndCheckSymbolicModel(storm::prism::Program const& program, std::vector<std::shared_ptr<storm::logic::Formula>> const& formulas) {
+        std::shared_ptr<storm::models::ModelBase> model = buildSymbolicModel<ValueType>(program, formulas);
         STORM_LOG_THROW(model != nullptr, storm::exceptions::InvalidStateException, "Model could not be constructed for an unknown reason.");
 
         // Preprocess the model if needed.
@@ -362,12 +357,19 @@ namespace storm {
         // Verify the model, if a formula was given.
         if (!formulas.empty()) {
             if (model->isSparseModel()) {
-                        verifySparseModel<ValueType>(program, model->as<storm::models::sparse::Model<ValueType>>(), formulas);
+                if(storm::settings::generalSettings().isCounterexampleSet()) {
+                    // If we were requested to generate a counterexample, we now do so for each formula.
+                    for(auto const& formula : formulas) {
+                        generateCounterexample<ValueType>(program, model->as<storm::models::sparse::Model<ValueType>>(), formula);
+                    }
+                } else {
+                    verifySparseModel<ValueType>(model->as<storm::models::sparse::Model<ValueType>>(), formulas);
+                }
             } else if (model->isSymbolicModel()) {
                 if (storm::settings::generalSettings().getEngine() == storm::settings::modules::GeneralSettings::Engine::Hybrid) {
-                            verifySymbolicModelWithHybridEngine(program, model->as<storm::models::symbolic::Model<storm::dd::DdType::CUDD>>(), formulas);
+                    verifySymbolicModelWithHybridEngine(model->as<storm::models::symbolic::Model<storm::dd::DdType::CUDD>>(), formulas);
                 } else {
-                            verifySymbolicModelWithSymbolicEngine(program, model->as<storm::models::symbolic::Model<storm::dd::DdType::CUDD>>(), formulas);
+                    verifySymbolicModelWithSymbolicEngine(model->as<storm::models::symbolic::Model<storm::dd::DdType::CUDD>>(), formulas);
                 }
             } else {
                 STORM_LOG_THROW(false, storm::exceptions::InvalidSettingsException, "Invalid input model type.");
@@ -391,7 +393,7 @@ namespace storm {
         // Verify the model, if a formula was given.
         if (!formulas.empty()) {
             STORM_LOG_THROW(model->isSparseModel(), storm::exceptions::InvalidStateException, "Expected sparse model.");
-                    verifySparseModel<ValueType>(boost::optional<storm::prism::Program>(), model->as<storm::models::sparse::Model<ValueType>>(), formulas);
+            verifySparseModel<ValueType>(model->as<storm::models::sparse::Model<ValueType>>(), formulas);
         }
     }