option to add initial predicates

src/storm/abstraction/MenuGameAbstractor.h

@@ -76,7 +76,7 @@ namespace storm {
              * computation.
              */
             virtual void notifyGuardsArePredicates() = 0;
-            
+                        
         protected:
             bool isRestrictToRelevantStatesSet() const;
             

src/storm/abstraction/MenuGameRefiner.cpp

@@ -93,6 +93,10 @@ namespace storm {
                 this->abstractor.get().notifyGuardsArePredicates();
                 addedAllGuardsFlag = true;
             }
+            if (abstractionSettings.isAddAllInitialExpressionsSet()) {
+                storm::expressions::Expression initialExpression = this->abstractor.get().getInitialExpression();
+                performRefinement(createGlobalRefinement(preprocessPredicates({initialExpression}, RefinementPredicates::Source::InitialExpression)));
+            }
             
             if (abstractionSettings.isInjectRefinementPredicatesSet()) {
                 std::string predicatesString = abstractionSettings.getInjectedRefinementPredicates();

src/storm/abstraction/MenuGameRefiner.h

@@ -40,7 +40,7 @@ namespace storm {
         class RefinementPredicates {
         public:
             enum class Source {
-                WeakestPrecondition, InitialGuard, Guard, Interpolation, Manual
+                WeakestPrecondition, InitialGuard, InitialExpression, Guard, Interpolation, Manual
             };
             
             RefinementPredicates() = default;

src/storm/abstraction/prism/PrismMenuGameAbstractor.cpp

@@ -276,7 +276,7 @@ namespace storm {
                     module.notifyGuardsArePredicates();
                 }
             }
-            
+                        
             // Explicitly instantiate the class.
             template class PrismMenuGameAbstractor<storm::dd::DdType::CUDD, double>;
             template class PrismMenuGameAbstractor<storm::dd::DdType::Sylvan, double>;

src/storm/settings/modules/AbstractionSettings.cpp

@@ -17,6 +17,7 @@ namespace storm {
             const std::string AbstractionSettings::useDecompositionOptionName = "decomposition";
             const std::string AbstractionSettings::splitModeOptionName = "split";
             const std::string AbstractionSettings::addAllGuardsOptionName = "all-guards";
+            const std::string AbstractionSettings::addInitialExpressionsOptionName = "all-inits";
             const std::string AbstractionSettings::useInterpolationOptionName = "interpolation";
             const std::string AbstractionSettings::precisionOptionName = "precision";
             const std::string AbstractionSettings::relativeOptionName = "relative";
@@ -65,7 +66,12 @@ namespace storm {
                                 .addArgument(storm::settings::ArgumentBuilder::createStringArgument("value", "The value of the flag.").addValidatorString(ArgumentValidatorFactory::createMultipleChoiceValidator(onOff))
                                              .setDefaultValueString("on").build())
                                 .build());
-                
+
+                this->addOption(storm::settings::OptionBuilder(moduleName, addInitialExpressionsOptionName, true, "Sets whether all initial expressions are added as initial predicates.")
+                                .addArgument(storm::settings::ArgumentBuilder::createStringArgument("value", "The value of the flag.").addValidatorString(ArgumentValidatorFactory::createMultipleChoiceValidator(onOff))
+                                             .setDefaultValueString("on").build())
+                                .build());
+
                 this->addOption(storm::settings::OptionBuilder(moduleName, useInterpolationOptionName, true, "Sets whether interpolation is to be used to eliminate spurious pivot blocks.")
                                 .addArgument(storm::settings::ArgumentBuilder::createStringArgument("value", "The value of the flag.").addValidatorString(ArgumentValidatorFactory::createMultipleChoiceValidator(onOff))
                                              .setDefaultValueString("on").build())
@@ -166,6 +172,10 @@ namespace storm {
                 return this->getOption(addAllGuardsOptionName).getArgumentByName("value").getValueAsString() == "on";
             }
             
+            bool AbstractionSettings::isAddAllInitialExpressionsSet() const {
+                return this->getOption(addInitialExpressionsOptionName).getArgumentByName("value").getValueAsString() == "on";
+            }
+            
             void AbstractionSettings::setAddAllGuards(bool value) {
                 this->getOption(addAllGuardsOptionName).getArgumentByName("value").setFromStringValue(value ? "on" : "off");
             }

src/storm/settings/modules/AbstractionSettings.h

@@ -62,6 +62,13 @@ namespace storm {
                  */
                 bool isAddAllGuardsSet() const;
                 
+                /*!
+                 * Retrieves whether the option to add all initial expressions was set.
+                 *
+                 * @return True iff the option was set.
+                 */
+                bool isAddAllInitialExpressionsSet() const;
+                
                 /*!
                  * Sets the option to add all guards to the specified value.
                  *
@@ -179,6 +186,7 @@ namespace storm {
                 const static std::string useDecompositionOptionName;
                 const static std::string splitModeOptionName;
                 const static std::string addAllGuardsOptionName;
+                const static std::string addInitialExpressionsOptionName;
                 const static std::string useInterpolationOptionName;
                 const static std::string precisionOptionName;
                 const static std::string relativeOptionName;