a bit more work toward CheckSettings objects

Former-commit-id: e8026b85e1

src/modelchecker/AbstractModelChecker.cpp

@@ -11,7 +11,7 @@
 
 namespace storm {
     namespace modelchecker {
-        std::unique_ptr<CheckResult> AbstractModelChecker::check(storm::logic::Formula const& formula) {
+        std::unique_ptr<CheckResult> AbstractModelChecker::check(storm::logic::Formula const& formula, boost::optional<CheckSettings<double>> const& checkSettings) {
             STORM_LOG_THROW(this->canHandle(formula), storm::exceptions::InvalidArgumentException, "The model checker is not able to check the formula '" << formula << "'.");
             if (formula.isStateFormula()) {
                 return this->checkStateFormula(formula.asStateFormula());

src/modelchecker/AbstractModelChecker.h

@@ -3,6 +3,7 @@
 
 #include <boost/optional.hpp>
 
+#include "src/modelchecker/CheckSettings.h"
 #include "src/logic/Formulas.h"
 #include "src/solver/OptimizationDirection.h"
 
@@ -29,9 +30,10 @@ namespace storm {
              * Checks the provided formula.
              *
              * @param formula The formula to check.
+             * @param checkSettings If provided, this object is used to customize the checking process.
              * @return The verification result.
              */
-            virtual std::unique_ptr<CheckResult> check(storm::logic::Formula const& formula);
+            virtual std::unique_ptr<CheckResult> check(storm::logic::Formula const& formula, boost::optional<CheckSettings<double>> const& checkSettings = boost::none);
                         
             // The methods to compute probabilities for path formulas.
             virtual std::unique_ptr<CheckResult> computeProbabilities(storm::logic::PathFormula const& pathFormula, bool qualitative = false, boost::optional<OptimizationDirection> const& optimalityType = boost::optional<OptimizationDirection>());

src/modelchecker/CheckSettings.cpp

@@ -1,9 +1,108 @@
 #include "src/modelchecker/CheckSettings.h"
 
+#include "src/logic/Formulas.h"
+
+#include "src/utility/constants.h"
+
 namespace storm {
     namespace modelchecker {
-        class CheckSettings {
+
+        template<typename ValueType>
+        CheckSettings<ValueType>::CheckSettings() : CheckSettings(boost::none, false, boost::none, false, false) {
+            // Intentionally left empty.
+        }
+        
+        template<typename ValueType>
+        CheckSettings<ValueType>::CheckSettings(boost::optional<storm::OptimizationDirection> const& optimizationDirection, bool onlyInitialStatesRelevant, boost::optional<std::pair<storm::logic::ComparisonType, ValueType>> const& initialStatesBound, bool qualitative, bool produceStrategies) : optimizationDirection(optimizationDirection), onlyInitialStatesRelevant(onlyInitialStatesRelevant), initialStatesBound(initialStatesBound), qualitative(qualitative), produceStrategies(produceStrategies) {
+            // Intentionally left empty.
+        }
+        
+        template<typename ValueType>
+        CheckSettings<ValueType> CheckSettings<ValueType>::fromToplevelFormula(storm::logic::Formula const& formula) {
+            return fromFormula(formula, true);
+        }
+        
+        template<typename ValueType>
+        CheckSettings<ValueType> CheckSettings<ValueType>::fromNestedFormula(storm::logic::Formula const& formula) {
+            return fromFormula(formula, false);
+        }
+        
+        template<typename ValueType>
+        CheckSettings<ValueType> CheckSettings<ValueType>::fromFormula(storm::logic::Formula const& formula, bool toplevel) {
+            boost::optional<storm::OptimizationDirection> optimizationDirection;
+            boost::optional<std::pair<storm::logic::ComparisonType, ValueType>> initialStatesBound;
+            bool qualitative = false;
+            bool onlyInitialStatesRelevant = !toplevel;
+            bool produceStrategies = false;
             
-        };
+            if (formula.isProbabilityOperatorFormula()) {
+                storm::logic::ProbabilityOperatorFormula const& probabilityOperatorFormula = formula.asProbabilityOperatorFormula();
+                if (probabilityOperatorFormula.hasOptimalityType()) {
+                    optimizationDirection = probabilityOperatorFormula.getOptimalityType();
+                }
+                
+                if (probabilityOperatorFormula.hasBound()) {
+                    if (onlyInitialStatesRelevant) {
+                        initialStatesBound = std::make_pair(probabilityOperatorFormula.getComparisonType(), static_cast<ValueType>(probabilityOperatorFormula.getBound()));
+                    }
+                    if (probabilityOperatorFormula.getBound() == storm::utility::zero<ValueType>() || probabilityOperatorFormula.getBound() == storm::utility::one<ValueType>()) {
+                        qualitative = true;
+                    }
+                }
+            } else if (formula.isRewardOperatorFormula()) {
+                storm::logic::RewardOperatorFormula const& rewardOperatorFormula = formula.asRewardOperatorFormula();
+                if (rewardOperatorFormula.hasOptimalityType()) {
+                    optimizationDirection = rewardOperatorFormula.getOptimalityType();
+                }
+                
+                if (rewardOperatorFormula.hasBound()) {
+                    if (onlyInitialStatesRelevant) {
+                        initialStatesBound = std::make_pair(rewardOperatorFormula.getComparisonType(), static_cast<ValueType>(rewardOperatorFormula.getBound()));
+                    }
+                    if (rewardOperatorFormula.getBound() == storm::utility::zero<ValueType>()) {
+                        qualitative = true;
+                    }
+                }
+            }
+            return CheckSettings<ValueType>(optimizationDirection, onlyInitialStatesRelevant, initialStatesBound, qualitative, produceStrategies);
+        }
+        
+        template<typename ValueType>
+        bool CheckSettings<ValueType>::isOptimizationDirectionSet() const {
+            return static_cast<bool>(optimizationDirection);
+        }
+        
+        template<typename ValueType>
+        storm::OptimizationDirection const& CheckSettings<ValueType>::getOptimizationDirection() const {
+            return optimizationDirection.get();
+        }
+        
+        template<typename ValueType>
+        bool CheckSettings<ValueType>::isOnlyInitialStatesRelevantSet() const {
+            return onlyInitialStatesRelevant;
+        }
+        
+        template<typename ValueType>
+        bool CheckSettings<ValueType>::isInitialStatesBoundSet() const {
+            return static_cast<bool>(initialStatesBound);
+        }
+        
+        template<typename ValueType>
+        std::pair<storm::logic::ComparisonType, ValueType> const& CheckSettings<ValueType>::getInitialStatesBound() const {
+            return initialStatesBound.get();
+        }
+        
+        template<typename ValueType>
+        bool CheckSettings<ValueType>::isQualitativeSet() const {
+            return qualitative;
+        }
+        
+        template<typename ValueType>
+        bool CheckSettings<ValueType>::isProduceStrategiesSet() const {
+            return produceStrategies;
+        }
+        
+        template class CheckSettings<double>;
+        
     }
 }

src/modelchecker/CheckSettings.h

@@ -7,6 +7,10 @@
 #include "src/logic/ComparisonType.h"
 
 namespace storm {
+    namespace logic {
+        class Formula;
+    }
+    
     namespace modelchecker {
         
         /*
@@ -20,6 +24,57 @@ namespace storm {
              */
             CheckSettings();
             
+            /*!
+             * Creates a settings object for the given top-level formula.
+             *
+             * @param formula The formula for which to create the settings.
+             */
+            static CheckSettings fromToplevelFormula(storm::logic::Formula const& formula);
+            
+            /*!
+             * Creates a settings object for the given formula that is nested within another formula.
+             *
+             * @param formula The formula for which to create the settings.
+             */
+            static CheckSettings fromNestedFormula(storm::logic::Formula const& formula);
+            
+            /*!
+             * Retrieves whether an optimization direction was set.
+             */
+            bool isOptimizationDirectionSet() const;
+            
+            /*!
+             * Retrieves the optimization direction (if set).
+             */
+            storm::OptimizationDirection const& getOptimizationDirection() const;
+            
+            /*!
+             * Retrieves whether only the initial states are relevant in the computation.
+             */
+            bool isOnlyInitialStatesRelevantSet() const;
+            
+            /*!
+             * Retrieves whether there is a bound with which the values for the initial states will be compared.
+             */
+            bool isInitialStatesBoundSet() const;
+            
+            /*!
+             * Retrieves the bound for the initial states (if set).
+             */
+            std::pair<storm::logic::ComparisonType, ValueType> const& getInitialStatesBound() const;
+            
+            /*!
+             * Retrieves whether the computation only needs to be performed qualitatively, because the values will only
+             * be compared to 0/1.
+             */
+            bool isQualitativeSet() const;
+            
+            /*!
+             * Retrieves whether strategies are to be produced (if supported).
+             */
+            bool isProduceStrategiesSet() const;
+            
+        private:
             /*!
              * Creates a settings object with the given options.
              *
@@ -35,12 +90,29 @@ namespace storm {
              */
             CheckSettings(boost::optional<storm::OptimizationDirection> const& optimizationDirection, bool onlyInitialStatesRelevant, boost::optional<std::pair<storm::logic::ComparisonType, ValueType>> const& initialStatesBound, bool qualitative, bool produceStrategies);
             
-        private:
-            boost::optional<std::pair<storm::logic::ComparisonType, ValueType>> initialStatesBound;
+            /*!
+             * Creates a settings object for the given formula.
+             *
+             * @param formula The formula for which to create the settings.
+             * @param toplevel Indicates whether this formula is the top-level formula.
+             */
+            static CheckSettings fromFormula(storm::logic::Formula const& formula, bool toplevel);
+            
+            // If set, the probabilities will be minimized/maximized.
             boost::optional<storm::OptimizationDirection> optimizationDirection;
+
+            // If set to true, the model checker may decide to only compute the values for the initial states.
+            bool onlyInitialStatesRelevant;
+
+            // The bound with which the initial states will be compared.
+            boost::optional<std::pair<storm::logic::ComparisonType, ValueType>> initialStatesBound;
+            
+            // A flag specifying whether the property needs to be checked qualitatively, i.e. compared with bounds 0/1.
             bool qualitative;
+            
+            // If supported by the model checker and the model formalism, strategies to achieve a value will be produced
+            // if this flag is set.
             bool produceStrategies;
-            bool onlyInitialStatesRelevant;
         };
         
     }