Merge branch 'future' into menu_games

Former-commit-id: 55e0868f96

src/cli/entrypoints.h

@@ -123,52 +123,41 @@ namespace storm {
     
         template<typename ValueType, storm::dd::DdType LibraryType>
         void buildAndCheckSymbolicModel(storm::prism::Program const& program, std::vector<std::shared_ptr<storm::logic::Formula>> const& formulas) {
+
             storm::settings::modules::GeneralSettings const& settings = storm::settings::generalSettings();
 
             if (settings.getEngine() == storm::settings::modules::GeneralSettings::Engine::AbstractionRefinement) {
                 verifySymbolicModelWithAbstractionRefinementEngine<ValueType, LibraryType>(program, formulas);
             } else {
-                storm::storage::ModelProgramPair modelProgramPair = buildSymbolicModel<ValueType, LibraryType>(program, formulas);
-                STORM_LOG_THROW(modelProgramPair.model != nullptr, storm::exceptions::InvalidStateException, "Model could not be constructed for an unknown reason.");
+                storm::storage::ModelFormulasPair modelFormulasPair = buildSymbolicModel<ValueType, LibraryType>(program, formulas);
+                STORM_LOG_THROW(modelFormulasPair.model != nullptr, storm::exceptions::InvalidStateException,
+                                "Model could not be constructed for an unknown reason.");
 
                 // Preprocess the model if needed.
-                BRANCH_ON_MODELTYPE(modelProgramPair.model, modelProgramPair.model, ValueType, LibraryType, preprocessModel, formulas);
+                BRANCH_ON_MODELTYPE(modelFormulasPair.model, modelFormulasPair.model, ValueType, LibraryType, preprocessModel, formulas);
 
                 // Print some information about the model.
-                modelProgramPair.model->printModelInformationToStream(std::cout);
+                modelFormulasPair.model->printModelInformationToStream(std::cout);
 
                 // Verify the model, if a formula was given.
                 if (!formulas.empty()) {
-                    // There may be constants of the model appearing in the formulas, so we replace all their occurrences
-                    // by their definitions in the translated program.
-                    
-                    // Start by building a mapping from constants of the (translated) model to their defining expressions.
-                    std::map<storm::expressions::Variable, storm::expressions::Expression> constantSubstitution;
-                    for (auto const& constant : modelProgramPair.program.getConstants()) {
-                        if (constant.isDefined()) {
-                            constantSubstitution.emplace(constant.getExpressionVariable(), constant.getExpression());
-                        }
-                    }
-                    
-                    std::vector<std::shared_ptr<storm::logic::Formula>> preparedFormulas;
-                    for (auto const& formula : formulas) {
-                        preparedFormulas.emplace_back(formula->substitute(constantSubstitution));
-                    }
 
-                    if (modelProgramPair.model->isSparseModel()) {
-                        if(settings.isCounterexampleSet()) {
+                    if (modelFormulasPair.model->isSparseModel()) {
+                        if (storm::settings::generalSettings().isCounterexampleSet()) {
                             // If we were requested to generate a counterexample, we now do so for each formula.
-                            for(auto const& formula : preparedFormulas) {
-                                generateCounterexample<ValueType>(program, modelProgramPair.model->as<storm::models::sparse::Model<ValueType>>(), formula);
+                            for (auto const &formula : modelFormulasPair.formulas) {
+                                generateCounterexample<ValueType>(program, modelFormulasPair.model->as<storm::models::sparse::Model<ValueType>>(), formula);
                             }
                         } else {
-                            verifySparseModel<ValueType>(modelProgramPair.model->as<storm::models::sparse::Model<ValueType>>(), preparedFormulas);
+                            verifySparseModel<ValueType>(modelFormulasPair.model->as<storm::models::sparse::Model<ValueType>>(), modelFormulasPair.formulas);
                         }
-                    } else if (modelProgramPair.model->isSymbolicModel()) {
-                        if (settings.getEngine() == storm::settings::modules::GeneralSettings::Engine::Hybrid) {
-                            verifySymbolicModelWithHybridEngine(modelProgramPair.model->as<storm::models::symbolic::Model<LibraryType>>(), preparedFormulas);
+                    } else if (modelFormulasPair.model->isSymbolicModel()) {
+                        if (storm::settings::generalSettings().getEngine() == storm::settings::modules::GeneralSettings::Engine::Hybrid) {
+                            verifySymbolicModelWithHybridEngine(modelFormulasPair.model->as<storm::models::symbolic::Model<LibraryType>>(),
+                                                                modelFormulasPair.formulas);
                         } else {
-                            verifySymbolicModelWithSymbolicEngine(modelProgramPair.model->as<storm::models::symbolic::Model<LibraryType>>(), preparedFormulas);
+                            verifySymbolicModelWithSymbolicEngine(modelFormulasPair.model->as<storm::models::symbolic::Model<LibraryType>>(),
+                                                                  modelFormulasPair.formulas);
                         }
                     } else {
                         STORM_LOG_THROW(false, storm::exceptions::InvalidSettingsException, "Invalid input model type.");

src/storage/ModelFormulasPair.h

@@ -0,0 +1,16 @@
+#pragma once
+#include "../models/ModelBase.h"
+
+
+namespace storm {
+    namespace logic {
+        class Formula;
+    }
+
+    namespace storage {
+        struct ModelFormulasPair {
+            std::shared_ptr<storm::models::ModelBase> model;
+            std::vector<std::shared_ptr<storm::logic::Formula>> formulas;
+        };
+    }
+}

src/storage/ModelProgramPair.h

@@ -1,12 +0,0 @@
-#include "../models/ModelBase.h"
-#include "prism/Program.h"
-
-
-namespace storm {
-    namespace storage {
-        struct ModelProgramPair {
-            std::shared_ptr<storm::models::ModelBase> model;
-            storm::prism::Program program;
-        };
-    }
-}

src/storage/prism/Program.cpp

@@ -172,6 +172,21 @@ namespace storm {
             return result;
         }
 
+        std::string Program::getUndefinedConstantsAsString() const {
+            std::stringstream stream;
+            bool printComma = false;
+            for (auto const& constant : getUndefinedConstants()) {
+                if (printComma) {
+                    stream << ", ";
+                } else {
+                    printComma = true;
+                }
+                stream << constant.get().getName() << " (" << constant.get().getType() << ")";
+            }
+            stream << ".";
+            return stream.str();
+        }
+        
         bool Program::hasConstant(std::string const& constantName) const {
             return this->constantToIndexMap.find(constantName) != this->constantToIndexMap.end();
         }

src/storage/prism/Program.h

@@ -90,6 +90,13 @@ namespace storm {
              */
             std::vector<std::reference_wrapper<storm::prism::Constant const>> getUndefinedConstants() const;
 
+            /*!
+             * Retrieves the undefined constants in the program as a comma-separated string.
+             *
+             * @return A string with the undefined constants in the program, separated by a comma
+             */
+            std::string getUndefinedConstantsAsString() const;
+
             /*!
              * Retrieves whether the given constant exists in the program.
              *

src/utility/initialize.cpp

@@ -1,5 +1,6 @@
 #include "initialize.h"
 
+#include "macros.h"
 #include "src/settings/SettingsManager.h"
 #include "src/settings/modules/DebugSettings.h"
 

src/utility/initialize.h

@@ -8,8 +8,7 @@
 #include "log4cplus/loggingmacros.h"
 #include "log4cplus/consoleappender.h"
 #include "log4cplus/fileappender.h"
-extern log4cplus::Logger logger;
-extern log4cplus::Logger printer;
+#include "macros.h"
 
 #include "src/settings/SettingsManager.h"
 

src/utility/storm.h

@@ -8,6 +8,7 @@
 #include <cstdio>
 #include <sstream>
 #include <memory>
+#include <src/storage/ModelFormulasPair.h>
 
 #include "initialize.h"
 
@@ -46,7 +47,7 @@
 // Headers for model processing.
 #include "src/storage/bisimulation/DeterministicModelBisimulationDecomposition.h"
 #include "src/storage/bisimulation/NondeterministicModelBisimulationDecomposition.h"
-#include "src/storage/ModelProgramPair.h"
+#include "src/storage/ModelFormulasPair.h"
 
 // Headers for model checking.
 #include "src/modelchecker/prctl/SparseDtmcPrctlModelChecker.h"
@@ -84,9 +85,12 @@ namespace storm {
     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, storm::dd::DdType LibraryType = storm::dd::DdType::CUDD>
-    storm::storage::ModelProgramPair buildSymbolicModel(storm::prism::Program const& program, std::vector<std::shared_ptr<storm::logic::Formula>> const& formulas) {
-        storm::storage::ModelProgramPair result;
+    storm::storage::ModelFormulasPair buildSymbolicModel(storm::prism::Program const& program, std::vector<std::shared_ptr<storm::logic::Formula>> const& formulas) {
+        storm::storage::ModelFormulasPair result;
+        storm::prism::Program translatedProgram;
 
         storm::settings::modules::GeneralSettings settings = storm::settings::generalSettings();
 
@@ -106,7 +110,7 @@ namespace storm {
 
             storm::builder::ExplicitPrismModelBuilder<ValueType> builder;
             result.model = builder.translateProgram(program, options);
-            result.program = builder.getTranslatedProgram();
+            translatedProgram = builder.getTranslatedProgram();
         } else if (settings.getEngine() == storm::settings::modules::GeneralSettings::Engine::Dd || settings.getEngine() == storm::settings::modules::GeneralSettings::Engine::Hybrid) {
             typename storm::builder::DdPrismModelBuilder<LibraryType>::Options options;
             options = typename storm::builder::DdPrismModelBuilder<LibraryType>::Options(formulas);
@@ -114,9 +118,22 @@ namespace storm {
 
             storm::builder::DdPrismModelBuilder<LibraryType> builder;
             result.model = builder.translateProgram(program, options);
-            result.program = builder.getTranslatedProgram();
+            translatedProgram = builder.getTranslatedProgram();
+        }
+        // There may be constants of the model appearing in the formulas, so we replace all their occurrences
+        // by their definitions in the translated program.
+
+        // Start by building a mapping from constants of the (translated) model to their defining expressions.
+        std::map<storm::expressions::Variable, storm::expressions::Expression> constantSubstitution;
+        for (auto const& constant : translatedProgram.getConstants()) {
+            if (constant.isDefined()) {
+                constantSubstitution.emplace(constant.getExpressionVariable(), constant.getExpression());
+            }
         }
 
+        for (auto const& formula : formulas) {
+            result.formulas.emplace_back(formula->substitute(constantSubstitution));
+        }
         return result;
     }