added abstraction settings and menu game abstractor

Former-commit-id: 4cac25ac94

src/abstraction/MenuGameAbstractor.cpp

@@ -1 +0,0 @@
-#include "src/abstraction/MenuGameAbstractor.h"

src/abstraction/prism/PrismMenuGameAbstractor.cpp

@@ -0,0 +1,27 @@
+#include "src/abstraction/prism/PrismMenuGameAbstractor.h"
+
+#include "src/settings/SettingsManager.h"
+#include "src/settings/modules/AbstractionSettings.h"
+
+namespace storm {
+    namespace abstraction {
+        namespace prism {
+            
+            template <storm::dd::DdType DdType, typename ValueType>
+            PrismMenuGameAbstractor<DdType, ValueType>::PrismMenuGameAbstractor(storm::expressions::ExpressionManager& expressionManager, storm::prism::Program const& program, std::vector<storm::expressions::Expression> const& initialPredicates, std::unique_ptr<storm::utility::solver::SmtSolverFactory>&& smtSolverFactory) : abstractProgram(expressionManager, program, initialPredicates, std::move(smtSolverFactory), storm::settings::getModule<storm::settings::modules::AbstractionSettings>().isAddAllGuardsSet()) {
+                // Intentionally left empty.
+            }
+            
+            template <storm::dd::DdType DdType, typename ValueType>
+            storm::abstraction::MenuGame<DdType, ValueType> PrismMenuGameAbstractor<DdType, ValueType>::abstract() {
+                return abstractProgram.getAbstractGame();
+            }
+            
+            template <storm::dd::DdType DdType, typename ValueType>
+            void PrismMenuGameAbstractor<DdType, ValueType>::refine(std::vector<storm::expressions::Expression> const& predicates) {
+                abstractProgram.refine(predicates);
+            }
+            
+        }
+    }
+}

src/abstraction/prism/PrismMenuGameAbstractor.h

@@ -0,0 +1,26 @@
+#pragma once
+
+#include "src/abstraction/MenuGameAbstractor.h"
+
+#include "src/abstraction/prism/AbstractProgram.h"
+
+namespace storm {
+    namespace abstraction {
+        namespace prism {
+            
+            template <storm::dd::DdType DdType, typename ValueType>
+            class PrismMenuGameAbstractor : public MenuGameAbstractor<DdType, ValueType> {
+            public:
+                PrismMenuGameAbstractor(storm::expressions::ExpressionManager& expressionManager, storm::prism::Program const& program, std::vector<storm::expressions::Expression> const& initialPredicates, std::unique_ptr<storm::utility::solver::SmtSolverFactory>&& smtSolverFactory = std::make_unique<storm::utility::solver::MathsatSmtSolverFactory>());
+                
+                virtual storm::abstraction::MenuGame<DdType, ValueType> abstract() override;
+                virtual void refine(std::vector<storm::expressions::Expression> const& predicates) override;
+
+            private:
+                /// The abstract program that performs the actual abstraction.
+                AbstractProgram<DdType, ValueType> abstractProgram;
+            };
+            
+        }
+    }
+}

src/modelchecker/abstraction/GameBasedMdpModelChecker.cpp

@@ -15,7 +15,7 @@ namespace storm {
     namespace modelchecker {
         template<storm::dd::DdType Type, typename ValueType>
         GameBasedMdpModelChecker<Type, ValueType>::GameBasedMdpModelChecker(storm::prism::Program const& program, std::unique_ptr<storm::utility::solver::SmtSolverFactory>&& smtSolverFactory) : originalProgram(program), smtSolverFactory(std::move(smtSolverFactory)) {
-            STORM_LOG_THROW(program.getModelType() == storm::prism::Program::ModelType::MDP, storm::exceptions::NotSupportedException, "Currently only MDPs are supported by the game-based model checker.");
+            STORM_LOG_THROW(program.getModelType() == storm::prism::Program::ModelType::DTMC || program.getModelType() == storm::prism::Program::ModelType::MDP, storm::exceptions::NotSupportedException, "Currently only DTMCs/MDPs are supported by the game-based model checker.");
                         
             // Start by preparing the program. That is, we flatten the modules if there is more than one.
             if (originalProgram.getNumberOfModules() > 1) {
@@ -46,12 +46,11 @@ namespace storm {
         template<storm::dd::DdType Type, typename ValueType>
         std::unique_ptr<CheckResult> GameBasedMdpModelChecker<Type, ValueType>::computeReachabilityProbabilities(CheckTask<storm::logic::EventuallyFormula> const& checkTask) {
             storm::logic::EventuallyFormula const& pathFormula = checkTask.getFormula();
-            return performGameBasedAbstractionRefinement(CheckTask<storm::logic::Formula>(pathFormula), originalProgram.getManager().boolean(true), getExpression(pathFormula.getSubformula()));
+            return performGameBasedAbstractionRefinement(checkTask.substituteFormula<storm::logic::Formula>(pathFormula), originalProgram.getManager().boolean(true), getExpression(pathFormula.getSubformula()));
         }
         
         template<storm::dd::DdType Type, typename ValueType>
         std::unique_ptr<CheckResult> GameBasedMdpModelChecker<Type, ValueType>::performGameBasedAbstractionRefinement(CheckTask<storm::logic::Formula> const& checkTask, storm::expressions::Expression const& constraintExpression, storm::expressions::Expression const& targetStateExpression) {
-            
             STORM_LOG_THROW(checkTask.isOnlyInitialStatesRelevantSet(), storm::exceptions::InvalidPropertyException, "The game-based abstraction refinement model checker can only compute the result for the initial states.");
             
             // 1. build initial abstraction based on the the constraint expression (if not 'true') and the target state expression.

src/settings/SettingsManager.cpp

@@ -32,6 +32,7 @@
 #include "src/settings/modules/TopologicalValueIterationEquationSolverSettings.h"
 #include "src/settings/modules/ExplorationSettings.h"
 #include "src/settings/modules/ResourceSettings.h"
+#include "src/settings/modules/AbstractionSettings.h"
 #include "src/utility/macros.h"
 #include "src/settings/Option.h"
 
@@ -522,6 +523,7 @@ namespace storm {
             storm::settings::addModule<storm::settings::modules::ParametricSettings>();
             storm::settings::addModule<storm::settings::modules::ExplorationSettings>();
             storm::settings::addModule<storm::settings::modules::ResourceSettings>();
+            storm::settings::addModule<storm::settings::modules::AbstractionSettings>();
         }
 
     }

src/settings/modules/AbstractionSettings.cpp

@@ -0,0 +1,23 @@
+#include "src/settings/modules/AbstractionSettings.h"
+
+#include "src/settings/Option.h"
+#include "src/settings/OptionBuilder.h"
+
+namespace storm {
+    namespace settings {
+        namespace modules {
+         
+            const std::string AbstractionSettings::moduleName = "abstraction";
+            const std::string AbstractionSettings::addAllGuardsOptionName = "allguards";
+            
+            AbstractionSettings::AbstractionSettings() : ModuleSettings(moduleName) {
+                this->addOption(storm::settings::OptionBuilder(moduleName, addAllGuardsOptionName, true, "Sets whether all guards are added as initial predicates.").build());
+            }
+            
+            bool AbstractionSettings::isAddAllGuardsSet() const {
+                return this->getOption(addAllGuardsOptionName).getHasOptionBeenSet();
+            }
+            
+        }
+    }
+}

src/settings/modules/AbstractionSettings.h

@@ -0,0 +1,34 @@
+#pragma once
+
+#include "src/settings/modules/ModuleSettings.h"
+
+namespace storm {
+    namespace settings {
+        namespace modules {
+            
+            /*!
+             * This class represents the settings for the abstraction procedures.
+             */
+            class AbstractionSettings : public ModuleSettings {
+            public:
+                /*!
+                 * Creates a new set of abstraction settings.
+                 */
+                AbstractionSettings();
+                
+                /*!
+                 * Retrieves whether the option to add all guards was set.
+                 *
+                 * @return True iff the option was set.
+                 */
+                bool isAddAllGuardsSet() const;
+                
+                const static std::string moduleName;
+                
+            private:
+                const static std::string addAllGuardsOptionName;
+            };
+            
+        }
+    }
+}

src/utility/storm.h

@@ -441,7 +441,7 @@ namespace storm {
     
     template<storm::dd::DdType DdType, typename ValueType>
     std::unique_ptr<storm::modelchecker::CheckResult> verifyProgramWithAbstractionRefinementEngine(storm::prism::Program const& program, std::shared_ptr<const storm::logic::Formula> const& formula, bool onlyInitialStatesRelevant = false) {
-        STORM_LOG_THROW(program.getModelType() == storm::prism::Program::ModelType::MDP, storm::exceptions::InvalidSettingsException, "Cannot treat non-MDP model using the abstraction refinement engine.");
+        STORM_LOG_THROW(program.getModelType() == storm::prism::Program::ModelType::DTMC || program.getModelType() == storm::prism::Program::ModelType::MDP, storm::exceptions::InvalidSettingsException, "Can only treat DTMCs/MDPs using the abstraction refinement engine.");
         
         // FIXME: Cudd -> ValueType, double -> ValueType
         storm::modelchecker::GameBasedMdpModelChecker<storm::dd::DdType::CUDD, double> modelchecker(program);