made storm compile again with expressions in time-bounds of until formula

src/storm/abstraction/MenuGame.cpp

@@ -50,6 +50,7 @@ namespace storm {
             } else if (expression.isFalse()) {
                 return this->getManager().getBddZero();
             }
+            
             auto it = expressionToBddMap.find(expression);
             STORM_LOG_THROW(it != expressionToBddMap.end(), storm::exceptions::InvalidArgumentException, "The given expression was not used in the abstraction process and can therefore not be retrieved.");
             if (negated) {

src/storm/logic/BoundedUntilFormula.cpp

@@ -9,7 +9,19 @@
 
 namespace storm {
     namespace logic {
-        BoundedUntilFormula::BoundedUntilFormula(std::shared_ptr<Formula const> const& leftSubformula, std::shared_ptr<Formula const> const& rightSubformula, boost::optional<UntilBound> const& lowerBound, boost::optional<UntilBound> const& upperBound, BoundedType const& boundedType) : BinaryPathFormula(leftSubformula, rightSubformula), lowerBound(lowerBound), upperBound(upperBound), boundedType(boundedType) {
+        UntilBound::UntilBound(bool strict, storm::expressions::Expression const& bound) : strict(strict), bound(bound) {
+            // Intentionally left empty.
+        }
+        
+        storm::expressions::Expression const& UntilBound::getBound() const {
+            return bound;
+        }
+        
+        bool UntilBound::isStrict() const {
+            return strict;
+        }
+        
+        BoundedUntilFormula::BoundedUntilFormula(std::shared_ptr<Formula const> const& leftSubformula, std::shared_ptr<Formula const> const& rightSubformula, boost::optional<UntilBound> const& lowerBound, boost::optional<UntilBound> const& upperBound, BoundedType const& boundedType) : BinaryPathFormula(leftSubformula, rightSubformula), boundedType(boundedType), lowerBound(lowerBound), upperBound(upperBound) {
             STORM_LOG_THROW(lowerBound || upperBound, storm::exceptions::InvalidArgumentException, "Bounded until formula requires at least one bound.");
         }
         
@@ -128,6 +140,7 @@ namespace storm {
                 }
                 out << this->getUpperBound();
             }
+            out << " ";
             
             this->getRightSubformula().writeToStream(out);
             return out;

src/storm/logic/BoundedUntilFormula.h

@@ -9,7 +9,7 @@ namespace storm {
     namespace logic {
         class UntilBound {
         public:
-            UntilBound(bool strict, storm::expressions::Expression bound);
+            UntilBound(bool strict, storm::expressions::Expression const& bound);
             
             storm::expressions::Expression const& getBound() const;
             bool isStrict() const;

src/storm/logic/FragmentSpecification.cpp

@@ -39,6 +39,7 @@ namespace storm {
             pctl.setUntilFormulasAllowed(true);
             pctl.setBoundedUntilFormulasAllowed(true);
             pctl.setStepBoundedUntilFormulasAllowed(true);
+            pctl.setTimeBoundedUntilFormulasAllowed(true);
             
             return pctl;
         }
@@ -97,6 +98,7 @@ namespace storm {
             multiObjective.setTotalRewardFormulasAllowed(true);
             multiObjective.setBoundedUntilFormulasAllowed(true);
             multiObjective.setStepBoundedUntilFormulasAllowed(true);
+            multiObjective.setTimeBoundedUntilFormulasAllowed(true);
 
             return multiObjective;
         }

src/storm/modelchecker/multiobjective/pcaa/SparsePcaaPreprocessor.cpp

@@ -1,4 +1,4 @@
- #include "storm/modelchecker/multiobjective/pcaa/SparsePcaaPreprocessor.h"
+#include "storm/modelchecker/multiobjective/pcaa/SparsePcaaPreprocessor.h"
 
 #include "storm/models/sparse/Mdp.h"
 #include "storm/models/sparse/MarkovAutomaton.h"
@@ -228,11 +228,21 @@ namespace storm {
                 
                 if (formula.hasLowerBound()) {
                     STORM_LOG_THROW(!result.originalModel.isOfType(storm::models::ModelType::Mdp) || formula.hasIntegerLowerBound(), storm::exceptions::InvalidPropertyException, "Expected discrete lower time-bound in formula.");
-                    currentObjective.lowerTimeBound = formula.getLowerBound<ValueType>();
+                    // FIXME: really convert formula bound to value type?
+                    if (formula.hasIntegerLowerBound()) {
+                        currentObjective.lowerTimeBound = storm::utility::convertNumber<ValueType>(formula.getLowerBound<uint64_t>());
+                    } else {
+                        currentObjective.lowerTimeBound = storm::utility::convertNumber<ValueType>(formula.getLowerBound<double>());
+                    }
                 }
                 if (formula.hasUpperBound()) {
                     STORM_LOG_THROW(!result.originalModel.isOfType(storm::models::ModelType::Mdp) || formula.hasIntegerUpperBound(), storm::exceptions::InvalidPropertyException, "Expected discrete lower time-bound in formula.");
-                    currentObjective.upperTimeBound = formula.getUpperBound<ValueType>();
+                    // FIXME: really convert formula bound to value type?
+                    if (formula.hasIntegerUpperBound()) {
+                        currentObjective.upperTimeBound = storm::utility::convertNumber<ValueType>(formula.getUpperBound<uint64_t>());
+                    } else {
+                        currentObjective.upperTimeBound = storm::utility::convertNumber<ValueType>(formula.getUpperBound<double>());
+                    }
                 } else {
                     currentObjective.upperTimeBound = storm::utility::infinity<ValueType>();
                 }

src/storm/modelchecker/prctl/HybridDtmcPrctlModelChecker.cpp

@@ -76,7 +76,7 @@ namespace storm {
             std::unique_ptr<CheckResult> rightResultPointer = this->check(pathFormula.getRightSubformula());
             SymbolicQualitativeCheckResult<DdType> const& leftResult = leftResultPointer->asSymbolicQualitativeCheckResult<DdType>();
             SymbolicQualitativeCheckResult<DdType> const& rightResult = rightResultPointer->asSymbolicQualitativeCheckResult<DdType>();
-            return storm::modelchecker::helper::HybridDtmcPrctlHelper<DdType, ValueType>::computeBoundedUntilProbabilities(this->getModel(), this->getModel().getTransitionMatrix(), leftResult.getTruthValuesVector(), rightResult.getTruthValuesVector(), pathFormula.getUpperBound<uint64_t>(), *this->linearEquationSolverFactory);
+            return storm::modelchecker::helper::HybridDtmcPrctlHelper<DdType, ValueType>::computeBoundedUntilProbabilities(this->getModel(), this->getModel().getTransitionMatrix(), leftResult.getTruthValuesVector(), rightResult.getTruthValuesVector(), pathFormula.getUpperBound<uint64_t>() + (pathFormula.isUpperBoundStrict() ? 1ull : 0ull), *this->linearEquationSolverFactory);
         }
                 
         template<typename ModelType>

src/storm/modelchecker/prctl/HybridMdpPrctlModelChecker.cpp

@@ -74,7 +74,7 @@ namespace storm {
             std::unique_ptr<CheckResult> rightResultPointer = this->check(pathFormula.getRightSubformula());
             SymbolicQualitativeCheckResult<DdType> const& leftResult = leftResultPointer->asSymbolicQualitativeCheckResult<DdType>();
             SymbolicQualitativeCheckResult<DdType> const& rightResult = rightResultPointer->asSymbolicQualitativeCheckResult<DdType>();
-            return storm::modelchecker::helper::HybridMdpPrctlHelper<DdType, ValueType>::computeBoundedUntilProbabilities(checkTask.getOptimizationDirection(), this->getModel(), this->getModel().getTransitionMatrix(), leftResult.getTruthValuesVector(), rightResult.getTruthValuesVector(), pathFormula.getUpperBound<uint64_t>(), *this->linearEquationSolverFactory);
+            return storm::modelchecker::helper::HybridMdpPrctlHelper<DdType, ValueType>::computeBoundedUntilProbabilities(checkTask.getOptimizationDirection(), this->getModel(), this->getModel().getTransitionMatrix(), leftResult.getTruthValuesVector(), rightResult.getTruthValuesVector(), pathFormula.getUpperBound<uint64_t>() + (pathFormula.isUpperBoundStrict() ? 1ull : 0ull), *this->linearEquationSolverFactory);
         }
         
         template<typename ModelType>

src/storm/modelchecker/prctl/SparseDtmcPrctlModelChecker.cpp

@@ -48,7 +48,7 @@ namespace storm {
             std::unique_ptr<CheckResult> rightResultPointer = this->check(pathFormula.getRightSubformula());
             ExplicitQualitativeCheckResult const& leftResult = leftResultPointer->asExplicitQualitativeCheckResult();
             ExplicitQualitativeCheckResult const& rightResult = rightResultPointer->asExplicitQualitativeCheckResult();
-            std::vector<ValueType> numericResult = storm::modelchecker::helper::SparseDtmcPrctlHelper<ValueType>::computeBoundedUntilProbabilities(this->getModel().getTransitionMatrix(), this->getModel().getBackwardTransitions(), leftResult.getTruthValuesVector(), rightResult.getTruthValuesVector(), pathFormula.getUpperBound<uint64_t>(), *linearEquationSolverFactory);
+            std::vector<ValueType> numericResult = storm::modelchecker::helper::SparseDtmcPrctlHelper<ValueType>::computeBoundedUntilProbabilities(this->getModel().getTransitionMatrix(), this->getModel().getBackwardTransitions(), leftResult.getTruthValuesVector(), rightResult.getTruthValuesVector(), pathFormula.getUpperBound<uint64_t>() + (pathFormula.isUpperBoundStrict() ? 1ull : 0ull), *linearEquationSolverFactory);
             std::unique_ptr<CheckResult> result = std::unique_ptr<CheckResult>(new ExplicitQuantitativeCheckResult<ValueType>(std::move(numericResult)));
             return result;
         }

src/storm/modelchecker/prctl/SparseMdpPrctlModelChecker.cpp

@@ -64,7 +64,7 @@ namespace storm {
             std::unique_ptr<CheckResult> rightResultPointer = this->check(pathFormula.getRightSubformula());
             ExplicitQualitativeCheckResult const& leftResult = leftResultPointer->asExplicitQualitativeCheckResult();
             ExplicitQualitativeCheckResult const& rightResult = rightResultPointer->asExplicitQualitativeCheckResult();
-            std::vector<ValueType> numericResult = storm::modelchecker::helper::SparseMdpPrctlHelper<ValueType>::computeBoundedUntilProbabilities(checkTask.getOptimizationDirection(), this->getModel().getTransitionMatrix(), this->getModel().getBackwardTransitions(), leftResult.getTruthValuesVector(), rightResult.getTruthValuesVector(), pathFormula.getUpperBound<uint64_t>(), *minMaxLinearEquationSolverFactory);
+            std::vector<ValueType> numericResult = storm::modelchecker::helper::SparseMdpPrctlHelper<ValueType>::computeBoundedUntilProbabilities(checkTask.getOptimizationDirection(), this->getModel().getTransitionMatrix(), this->getModel().getBackwardTransitions(), leftResult.getTruthValuesVector(), rightResult.getTruthValuesVector(), pathFormula.getUpperBound<uint64_t>() + (pathFormula.isUpperBoundStrict() ? 1ull : 0ull), *minMaxLinearEquationSolverFactory);
             return std::unique_ptr<CheckResult>(new ExplicitQuantitativeCheckResult<ValueType>(std::move(numericResult)));
         }
         

src/storm/modelchecker/prctl/SymbolicDtmcPrctlModelChecker.cpp

@@ -76,7 +76,7 @@ namespace storm {
             std::unique_ptr<CheckResult> rightResultPointer = this->check(pathFormula.getRightSubformula());
             SymbolicQualitativeCheckResult<DdType> const& leftResult = leftResultPointer->asSymbolicQualitativeCheckResult<DdType>();
             SymbolicQualitativeCheckResult<DdType> const& rightResult = rightResultPointer->asSymbolicQualitativeCheckResult<DdType>();
-            storm::dd::Add<DdType> numericResult = storm::modelchecker::helper::SymbolicDtmcPrctlHelper<DdType, ValueType>::computeBoundedUntilProbabilities(this->getModel(), this->getModel().getTransitionMatrix(), leftResult.getTruthValuesVector(), rightResult.getTruthValuesVector(), pathFormula.getUpperBound<uint64_t>(), *this->linearEquationSolverFactory);
+            storm::dd::Add<DdType> numericResult = storm::modelchecker::helper::SymbolicDtmcPrctlHelper<DdType, ValueType>::computeBoundedUntilProbabilities(this->getModel(), this->getModel().getTransitionMatrix(), leftResult.getTruthValuesVector(), rightResult.getTruthValuesVector(), pathFormula.getUpperBound<uint64_t>() + (pathFormula.isUpperBoundStrict() ? 1ull : 0ull), *this->linearEquationSolverFactory);
             return std::unique_ptr<SymbolicQuantitativeCheckResult<DdType>>(new SymbolicQuantitativeCheckResult<DdType>(this->getModel().getReachableStates(), numericResult));
         }
         

src/storm/modelchecker/prctl/SymbolicMdpPrctlModelChecker.cpp

@@ -76,7 +76,7 @@ namespace storm {
             std::unique_ptr<CheckResult> rightResultPointer = this->check(pathFormula.getRightSubformula());
             SymbolicQualitativeCheckResult<DdType> const& leftResult = leftResultPointer->asSymbolicQualitativeCheckResult<DdType>();
             SymbolicQualitativeCheckResult<DdType> const& rightResult = rightResultPointer->asSymbolicQualitativeCheckResult<DdType>();
-            return storm::modelchecker::helper::SymbolicMdpPrctlHelper<DdType, ValueType>::computeBoundedUntilProbabilities(checkTask.getOptimizationDirection(), this->getModel(), this->getModel().getTransitionMatrix(), leftResult.getTruthValuesVector(), rightResult.getTruthValuesVector(), pathFormula.getUpperBound<uint64_t>(), *this->linearEquationSolverFactory);
+            return storm::modelchecker::helper::SymbolicMdpPrctlHelper<DdType, ValueType>::computeBoundedUntilProbabilities(checkTask.getOptimizationDirection(), this->getModel(), this->getModel().getTransitionMatrix(), leftResult.getTruthValuesVector(), rightResult.getTruthValuesVector(), pathFormula.getUpperBound<uint64_t>() + (pathFormula.isUpperBoundStrict() ? 1ull : 0ull), *this->linearEquationSolverFactory);
         }
         
         template<typename ModelType>

src/storm/parser/FormulaParserGrammar.cpp

@@ -224,7 +224,7 @@ namespace storm {
         
         std::shared_ptr<storm::logic::Formula const> FormulaParserGrammar::createEventuallyFormula(boost::optional<std::pair<boost::optional<storm::logic::UntilBound>, boost::optional<storm::logic::UntilBound>>> const& timeBound, storm::logic::FormulaContext context, std::shared_ptr<storm::logic::Formula const> const& subformula) const {
             if (timeBound) {
-                return std::shared_ptr<storm::logic::Formula const>(new storm::logic::BoundedUntilFormula(createBooleanLiteralFormula(true), subformula, timeBound.get().first, timeBound.get().second, storm::logic::BoundedUntil::BoundedType::Time));
+                return std::shared_ptr<storm::logic::Formula const>(new storm::logic::BoundedUntilFormula(createBooleanLiteralFormula(true), subformula, timeBound.get().first, timeBound.get().second, storm::logic::BoundedUntilFormula::BoundedType::Time));
             } else {
                 return std::shared_ptr<storm::logic::Formula const>(new storm::logic::EventuallyFormula(subformula, context));
             }
@@ -240,7 +240,7 @@ namespace storm {
         
         std::shared_ptr<storm::logic::Formula const> FormulaParserGrammar::createUntilFormula(std::shared_ptr<storm::logic::Formula const> const& leftSubformula, boost::optional<std::pair<boost::optional<storm::logic::UntilBound>, boost::optional<storm::logic::UntilBound>>> const& timeBound, std::shared_ptr<storm::logic::Formula const> const& rightSubformula) {
             if (timeBound) {
-                return std::shared_ptr<storm::logic::Formula const>(new storm::logic::BoundedUntilFormula(leftSubformula, rightSubformula, timeBound.get().first, timeBound.get().second, storm::logic::BoundedUntil::BoundedType::Time));
+                return std::shared_ptr<storm::logic::Formula const>(new storm::logic::BoundedUntilFormula(leftSubformula, rightSubformula, timeBound.get().first, timeBound.get().second, storm::logic::BoundedUntilFormula::BoundedType::Time));
             } else {
                 return std::shared_ptr<storm::logic::Formula const>(new storm::logic::UntilFormula(leftSubformula, rightSubformula));
             }

src/storm/parser/FormulaParserGrammar.h

@@ -149,7 +149,7 @@ namespace storm {
             qi::rule<Iterator, std::shared_ptr<storm::logic::Formula const>(storm::logic::FormulaContext), Skipper> globallyFormula;
             qi::rule<Iterator, std::shared_ptr<storm::logic::Formula const>(storm::logic::FormulaContext), Skipper> untilFormula;
             
-            qi::rule<Iterator, std::pair<boost::optional<storm::logic::UntilBound>>(), qi::locals<bool, bool>, Skipper> timeBound;
+            qi::rule<Iterator, std::pair<boost::optional<storm::logic::UntilBound>, boost::optional<storm::logic::UntilBound>>(), qi::locals<bool, bool>, Skipper> timeBound;
             
             qi::rule<Iterator, std::shared_ptr<storm::logic::Formula const>(), Skipper> rewardPathFormula;
             qi::rule<Iterator, std::shared_ptr<storm::logic::Formula const>(), Skipper> cumulativeRewardFormula;

src/storm/parser/JaniParser.cpp

@@ -345,7 +345,7 @@ namespace storm {
                             upperBound--;
                         }
                         STORM_LOG_THROW(upperBound >= 0, storm::exceptions::InvalidJaniException, "Step-bounds cannot be negative");
-                        return std::make_shared<storm::logic::BoundedUntilFormula const>(args[0], args[1], std::make_pair(pi.lowerBound, !pi.lowerBoundStrict), std::make_pair(pi.upperBound, !pi.upperBoundStrict), storm::logic::BoundedUntilFormula::BoundedType::Steps);
+                        return std::make_shared<storm::logic::BoundedUntilFormula const>(args[0], args[1], storm::logic::UntilBound(pi.lowerBoundStrict, pi.lowerBound), storm::logic::UntilBound(pi.upperBoundStrict, pi.upperBound), storm::logic::BoundedUntilFormula::BoundedType::Steps);
                     } else if (propertyStructure.count("time-bounds") > 0) {
                         storm::jani::PropertyInterval pi = parsePropertyInterval(propertyStructure.at("time-bounds"));
                         STORM_LOG_THROW(pi.hasUpperBound(), storm::exceptions::NotSupportedException, "Storm only supports time-bounded until with an upper bound.");
@@ -356,7 +356,7 @@ namespace storm {
                         double upperBound = pi.upperBound.evaluateAsDouble();
                         STORM_LOG_THROW(lowerBound >= 0, storm::exceptions::InvalidJaniException, "(Lower) time-bounds cannot be negative");
                         STORM_LOG_THROW(upperBound >= 0, storm::exceptions::InvalidJaniException, "(Upper) time-bounds cannot be negative");
-                        return std::make_shared<storm::logic::BoundedUntilFormula const>(args[0], args[1], std::make_pair(pi.lowerBound, !pi.lowerBoundStrict), std::make_pair(pi.upperBound, !pi.upperBoundStrict), storm::logic::BoundedUntilFormula::BoundedType::Time);
+                        return std::make_shared<storm::logic::BoundedUntilFormula const>(args[0], args[1], storm::logic::UntilBound(pi.lowerBoundStrict, pi.lowerBound), storm::logic::UntilBound(pi.upperBoundStrict, pi.upperBound), storm::logic::BoundedUntilFormula::BoundedType::Time);
                         
                     } else if (propertyStructure.count("reward-bounds") > 0 ) {
                         STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "Reward bounded properties are not supported by Storm");

src/storm/settings/Option.cpp

@@ -76,6 +76,12 @@ namespace storm {
 				return *argumentIterator->second;
 			}
 
+            ArgumentBase& Option::getArgumentByName(std::string const& argumentName) {
+                auto argumentIterator = this->argumentNameMap.find(argumentName);
+                STORM_LOG_THROW(argumentIterator != this->argumentNameMap.end(), storm::exceptions::IllegalArgumentException, "Unable to retrieve argument with unknown name '" << argumentName << "'.");
+                return *argumentIterator->second;
+            }
+
 			std::string const& Option::getLongName() const {
 				return this->longName;
 			}

src/storm/settings/Option.h

@@ -64,7 +64,7 @@ namespace storm {
              * @param other The other option with which to check compatibility.
              * @return True iff the given argument is compatible with the current one.
              */
-                bool isCompatibleWith(Option const& other);
+            bool isCompatibleWith(Option const& other);
 
             /*!
              * Retrieves the argument count this option expects.
@@ -96,6 +96,14 @@ namespace storm {
              * @return The argument with the given name.
              */
             ArgumentBase const& getArgumentByName(std::string const& argumentName) const;
+                
+            /*!
+             * Returns a reference to the argument with the specified long name.
+             *
+             * @param argumentName The name of the argument to retrieve.
+             * @return The argument with the given name.
+             */
+            ArgumentBase& getArgumentByName(std::string const& argumentName);
 
             /*!
              * Retrieves the long name of this option.

src/storm/settings/SettingsManager.cpp

@@ -504,6 +504,10 @@ namespace storm {
             return dynamic_cast<storm::settings::modules::IOSettings&>(mutableManager().getModule(storm::settings::modules::IOSettings::moduleName));
         }
         
+        storm::settings::modules::AbstractionSettings& mutableAbstractionSettings() {
+            return dynamic_cast<storm::settings::modules::AbstractionSettings&>(mutableManager().getModule(storm::settings::modules::AbstractionSettings::moduleName));
+        }
+        
         void initializeAll(std::string const& name, std::string const& executableName) {
             storm::settings::mutableManager().setName(name, executableName);
 

src/storm/settings/SettingsManager.h

@@ -15,6 +15,7 @@ namespace storm {
             class CoreSettings;
             class IOSettings;
             class ModuleSettings;
+            class AbstractionSettings;
         }
         class Option;
         
@@ -266,10 +267,10 @@ namespace storm {
         }
         
         /*!
-         * Retrieves the markov chain settings in a mutable form. This is only meant to be used for debug purposes or very
+         * Retrieves the core settings in a mutable form. This is only meant to be used for debug purposes or very
          * rare cases where it is necessary.
          *
-         * @return An object that allows accessing and modifying the markov chain settings.
+         * @return An object that allows accessing and modifying the core settings.
          */
         storm::settings::modules::CoreSettings& mutableCoreSettings();
         
@@ -281,6 +282,14 @@ namespace storm {
          */
         storm::settings::modules::IOSettings& mutableIOSettings();
         
+        /*!
+         * Retrieves the abstraction settings in a mutable form. This is only meant to be used for debug purposes or very
+         * rare cases where it is necessary.
+         *
+         * @return An object that allows accessing and modifying the abstraction settings.
+         */
+        storm::settings::modules::AbstractionSettings& mutableAbstractionSettings();
+        
     } // namespace settings
 } // namespace storm
 

src/storm/settings/modules/AbstractionSettings.cpp

@@ -40,7 +40,6 @@ namespace storm {
                                              .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())
@@ -80,6 +79,10 @@ namespace storm {
                 return this->getOption(addAllGuardsOptionName).getArgumentByName("value").getValueAsString() == "on";
             }
             
+            void AbstractionSettings::setAddAllGuards(bool value) {
+                this->getOption(addAllGuardsOptionName).getArgumentByName("value").setFromStringValue(value ? "on" : "off");
+            }
+            
             bool AbstractionSettings::isUseInterpolationSet() const {
                 return this->getOption(useInterpolationOptionName).getArgumentByName("value").getValueAsString() == "on";
             }

src/storm/settings/modules/AbstractionSettings.h

@@ -49,6 +49,13 @@ namespace storm {
                  */
                 bool isAddAllGuardsSet() const;
                 
+                /*!
+                 * Sets the option to add all guards to the specified value.
+                 *
+                 * @param value The new value.
+                 */
+                void setAddAllGuards(bool value);
+                
                 /*!
                  * Retrieves whether the option to use interpolation was set.
                  *

src/storm/settings/modules/ModuleSettings.cpp

@@ -77,6 +77,16 @@ namespace storm {
                 return length;
             }
             
+            void ModuleSettings::restoreDefaults() {
+                for (auto& option : options) {
+                    for (auto& argument : option->getArguments()) {
+                        if (argument->getHasDefaultValue()) {
+                            argument->setFromDefaultValue();
+                        }
+                    }
+                }
+            }
+            
         } // namespace modules
     } // namespace settings
 } // namespace storm

src/storm/settings/modules/ModuleSettings.h

@@ -76,6 +76,11 @@ namespace storm {
                  */
                 uint_fast64_t getPrintLengthOfLongestOption() const;
                 
+                /*!
+                 * Restores the default values for all arguments of all options.
+                 */
+                void restoreDefaults();
+                
             protected:
                 
                 /*!

src/storm/storage/jani/JSONExporter.cpp

@@ -169,10 +169,10 @@ namespace storm {
             opDecl["op"] = "U";
             opDecl["left"] = boost::any_cast<modernjson::json>(f.getLeftSubformula().accept(*this, data));
             opDecl["right"] = boost::any_cast<modernjson::json>(f.getRightSubformula().accept(*this, data));
-            if(f.hasDiscreteTimeBound()) {
-                opDecl["step-bounds"] = constructPropertyInterval(0, f.getDiscreteTimeBound());
+            if(f.isStepBounded()) {
+                opDecl["step-bounds"] = constructPropertyInterval(0, f.getUpperBound<uint64_t>());
             } else {
-                opDecl["time-bounds"] = constructPropertyInterval(f.getIntervalBounds().first, f.getIntervalBounds().second);
+                opDecl["time-bounds"] = constructPropertyInterval(f.getLowerBound<double>(), f.getUpperBound<double>());
             }
             return opDecl;
         }

src/test/abstraction/PrismMenuGameTest.cpp

@@ -19,7 +19,12 @@
 
 #include "storm/adapters/CarlAdapter.h"
 
+#include "storm/settings/SettingsManager.h"
+#include "storm/settings/modules/AbstractionSettings.h"
+
 TEST(PrismMenuGame, DieAbstractionTest_Cudd) {
+    storm::settings::mutableAbstractionSettings().setAddAllGuards(false);
+    
     storm::prism::Program program = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/dtmc/die.pm");
 
     std::vector<storm::expressions::Expression> initialPredicates;
@@ -37,9 +42,13 @@ TEST(PrismMenuGame, DieAbstractionTest_Cudd) {
     EXPECT_EQ(26ull, game.getNumberOfTransitions());
     EXPECT_EQ(4ull, game.getNumberOfStates());
     EXPECT_EQ(2ull, game.getBottomStates().getNonZeroCount());
+    
+    storm::settings::mutableAbstractionSettings().restoreDefaults();
 }
 
 TEST(PrismMenuGame, DieAbstractionTest_Sylvan) {
+    storm::settings::mutableAbstractionSettings().setAddAllGuards(false);
+
     storm::prism::Program program = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/dtmc/die.pm");
     
     std::vector<storm::expressions::Expression> initialPredicates;
@@ -58,6 +67,8 @@ TEST(PrismMenuGame, DieAbstractionTest_Sylvan) {
     EXPECT_EQ(26ull, game.getNumberOfTransitions());
     EXPECT_EQ(4ull, game.getNumberOfStates());
     EXPECT_EQ(2ull, game.getBottomStates().getNonZeroCount());
+
+    storm::settings::mutableAbstractionSettings().restoreDefaults();
 }
 
 #ifdef STORM_HAVE_CARL
@@ -86,6 +97,8 @@ TEST(PrismMenuGame, DieAbstractionTest_Sylvan) {
 #endif
 
 TEST(PrismMenuGame, DieAbstractionAndRefinementTest_Cudd) {
+    storm::settings::mutableAbstractionSettings().setAddAllGuards(false);
+
     storm::prism::Program program = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/dtmc/die.pm");
     
     std::vector<storm::expressions::Expression> initialPredicates;
@@ -106,9 +119,13 @@ TEST(PrismMenuGame, DieAbstractionAndRefinementTest_Cudd) {
     EXPECT_EQ(24ull, game.getNumberOfTransitions());
     EXPECT_EQ(5ull, game.getNumberOfStates());
     EXPECT_EQ(2ull, game.getBottomStates().getNonZeroCount());
+
+    storm::settings::mutableAbstractionSettings().restoreDefaults();
 }
 
 TEST(PrismMenuGame, DieAbstractionAndRefinementTest_Sylvan) {
+    storm::settings::mutableAbstractionSettings().setAddAllGuards(false);
+
     storm::prism::Program program = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/dtmc/die.pm");
     
     std::vector<storm::expressions::Expression> initialPredicates;
@@ -129,9 +146,13 @@ TEST(PrismMenuGame, DieAbstractionAndRefinementTest_Sylvan) {
     EXPECT_EQ(24ull, game.getNumberOfTransitions());
     EXPECT_EQ(5ull, game.getNumberOfStates());
     EXPECT_EQ(2ull, game.getBottomStates().getNonZeroCount());
+
+    storm::settings::mutableAbstractionSettings().restoreDefaults();
 }
 
 TEST(PrismMenuGame, DieFullAbstractionTest_Cudd) {
+    storm::settings::mutableAbstractionSettings().setAddAllGuards(false);
+
     storm::prism::Program program = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/dtmc/die.pm");
     
     std::vector<storm::expressions::Expression> initialPredicates;
@@ -165,9 +186,13 @@ TEST(PrismMenuGame, DieFullAbstractionTest_Cudd) {
     EXPECT_EQ(20ull, game.getNumberOfTransitions());
     EXPECT_EQ(13ull, game.getNumberOfStates());
     EXPECT_EQ(0ull, game.getBottomStates().getNonZeroCount());
+
+    storm::settings::mutableAbstractionSettings().restoreDefaults();
 }
 
 TEST(PrismMenuGame, DieFullAbstractionTest_Sylvan) {
+    storm::settings::mutableAbstractionSettings().setAddAllGuards(false);
+
     storm::prism::Program program = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/dtmc/die.pm");
     
     std::vector<storm::expressions::Expression> initialPredicates;
@@ -201,9 +226,13 @@ TEST(PrismMenuGame, DieFullAbstractionTest_Sylvan) {
     EXPECT_EQ(20ull, game.getNumberOfTransitions());
     EXPECT_EQ(13ull, game.getNumberOfStates());
     EXPECT_EQ(0ull, game.getBottomStates().getNonZeroCount());
+
+    storm::settings::mutableAbstractionSettings().restoreDefaults();
 }
 
 TEST(PrismMenuGame, CrowdsAbstractionTest_Cudd) {
+    storm::settings::mutableAbstractionSettings().setAddAllGuards(false);
+
     storm::prism::Program program = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/dtmc/crowds-5-5.pm");
     program = program.substituteConstants();
     
@@ -223,9 +252,13 @@ TEST(PrismMenuGame, CrowdsAbstractionTest_Cudd) {
     EXPECT_EQ(31ull, game.getNumberOfTransitions());
     EXPECT_EQ(4ull, game.getNumberOfStates());
     EXPECT_EQ(2ull, game.getBottomStates().getNonZeroCount());
+
+    storm::settings::mutableAbstractionSettings().restoreDefaults();
 }
 
 TEST(PrismMenuGame, CrowdsAbstractionTest_Sylvan) {
+    storm::settings::mutableAbstractionSettings().setAddAllGuards(false);
+
     storm::prism::Program program = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/dtmc/crowds-5-5.pm");
     program = program.substituteConstants();
     
@@ -245,9 +278,13 @@ TEST(PrismMenuGame, CrowdsAbstractionTest_Sylvan) {
     EXPECT_EQ(31ull, game.getNumberOfTransitions());
     EXPECT_EQ(4ull, game.getNumberOfStates());
     EXPECT_EQ(2ull, game.getBottomStates().getNonZeroCount());
+
+    storm::settings::mutableAbstractionSettings().restoreDefaults();
 }
 
 TEST(PrismMenuGame, CrowdsAbstractionAndRefinementTest_Cudd) {
+    storm::settings::mutableAbstractionSettings().setAddAllGuards(false);
+
     storm::prism::Program program = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/dtmc/crowds-5-5.pm");
     program = program.substituteConstants();
     
@@ -269,9 +306,13 @@ TEST(PrismMenuGame, CrowdsAbstractionAndRefinementTest_Cudd) {
     EXPECT_EQ(68ull, game.getNumberOfTransitions());
     EXPECT_EQ(8ull, game.getNumberOfStates());
     EXPECT_EQ(4ull, game.getBottomStates().getNonZeroCount());
+
+    storm::settings::mutableAbstractionSettings().restoreDefaults();
 }
 
 TEST(PrismMenuGame, CrowdsAbstractionAndRefinementTest_Sylvan) {
+    storm::settings::mutableAbstractionSettings().setAddAllGuards(false);
+
     storm::prism::Program program = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/dtmc/crowds-5-5.pm");
     program = program.substituteConstants();
     
@@ -293,9 +334,13 @@ TEST(PrismMenuGame, CrowdsAbstractionAndRefinementTest_Sylvan) {
     EXPECT_EQ(68ull, game.getNumberOfTransitions());
     EXPECT_EQ(8ull, game.getNumberOfStates());
     EXPECT_EQ(4ull, game.getBottomStates().getNonZeroCount());
+
+    storm::settings::mutableAbstractionSettings().restoreDefaults();
 }
 
 TEST(PrismMenuGame, CrowdsFullAbstractionTest_Cudd) {
+    storm::settings::mutableAbstractionSettings().setAddAllGuards(false);
+
     storm::prism::Program program = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/dtmc/crowds-5-5.pm");
     program = program.substituteConstants();
     
@@ -369,9 +414,13 @@ TEST(PrismMenuGame, CrowdsFullAbstractionTest_Cudd) {
     EXPECT_EQ(15113ull, game.getNumberOfTransitions());
     EXPECT_EQ(8607ull, game.getNumberOfStates());
     EXPECT_EQ(0ull, game.getBottomStates().getNonZeroCount());
+
+    storm::settings::mutableAbstractionSettings().restoreDefaults();
 }
 
 TEST(PrismMenuGame, CrowdsFullAbstractionTest_Sylvan) {
+    storm::settings::mutableAbstractionSettings().setAddAllGuards(false);
+
     storm::prism::Program program = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/dtmc/crowds-5-5.pm");
     program = program.substituteConstants();
     
@@ -445,9 +494,13 @@ TEST(PrismMenuGame, CrowdsFullAbstractionTest_Sylvan) {
     EXPECT_EQ(15113ull, game.getNumberOfTransitions());
     EXPECT_EQ(8607ull, game.getNumberOfStates());
     EXPECT_EQ(0ull, game.getBottomStates().getNonZeroCount());
+
+    storm::settings::mutableAbstractionSettings().restoreDefaults();
 }
 
 TEST(PrismMenuGame, TwoDiceAbstractionTest_Cudd) {
+    storm::settings::mutableAbstractionSettings().setAddAllGuards(false);
+
     storm::prism::Program program = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/mdp/two_dice.nm");
     program = program.substituteConstants();
     program = program.flattenModules(std::make_shared<storm::utility::solver::MathsatSmtSolverFactory>());
@@ -469,9 +522,13 @@ TEST(PrismMenuGame, TwoDiceAbstractionTest_Cudd) {
     EXPECT_EQ(90ull, game.getNumberOfTransitions());
     EXPECT_EQ(8ull, game.getNumberOfStates());
     EXPECT_EQ(4ull, game.getBottomStates().getNonZeroCount());
+
+    storm::settings::mutableAbstractionSettings().restoreDefaults();
 }
 
 TEST(PrismMenuGame, TwoDiceAbstractionTest_Sylvan) {
+    storm::settings::mutableAbstractionSettings().setAddAllGuards(false);
+
     storm::prism::Program program = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/mdp/two_dice.nm");
     program = program.substituteConstants();
     program = program.flattenModules(std::make_shared<storm::utility::solver::MathsatSmtSolverFactory>());
@@ -493,9 +550,13 @@ TEST(PrismMenuGame, TwoDiceAbstractionTest_Sylvan) {
     EXPECT_EQ(90ull, game.getNumberOfTransitions());
     EXPECT_EQ(8ull, game.getNumberOfStates());
     EXPECT_EQ(4ull, game.getBottomStates().getNonZeroCount());
+
+    storm::settings::mutableAbstractionSettings().restoreDefaults();
 }
 
 TEST(PrismMenuGame, TwoDiceAbstractionAndRefinementTest_Cudd) {
+    storm::settings::mutableAbstractionSettings().setAddAllGuards(false);
+
     storm::prism::Program program = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/mdp/two_dice.nm");
     program = program.substituteConstants();
     program = program.flattenModules(std::make_shared<storm::utility::solver::MathsatSmtSolverFactory>());
@@ -519,9 +580,13 @@ TEST(PrismMenuGame, TwoDiceAbstractionAndRefinementTest_Cudd) {
     EXPECT_EQ(276ull, game.getNumberOfTransitions());
     EXPECT_EQ(16ull, game.getNumberOfStates());
     EXPECT_EQ(8ull, game.getBottomStates().getNonZeroCount());
+
+    storm::settings::mutableAbstractionSettings().restoreDefaults();
 }
 
 TEST(PrismMenuGame, TwoDiceAbstractionAndRefinementTest_Sylvan) {
+    storm::settings::mutableAbstractionSettings().setAddAllGuards(false);
+
     storm::prism::Program program = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/mdp/two_dice.nm");
     program = program.substituteConstants();
     program = program.flattenModules(std::make_shared<storm::utility::solver::MathsatSmtSolverFactory>());
@@ -545,9 +610,13 @@ TEST(PrismMenuGame, TwoDiceAbstractionAndRefinementTest_Sylvan) {
     EXPECT_EQ(276ull, game.getNumberOfTransitions());
     EXPECT_EQ(16ull, game.getNumberOfStates());
     EXPECT_EQ(8ull, game.getBottomStates().getNonZeroCount());
+
+    storm::settings::mutableAbstractionSettings().restoreDefaults();
 }
 
 TEST(PrismMenuGame, TwoDiceFullAbstractionTest_Cudd) {
+    storm::settings::mutableAbstractionSettings().setAddAllGuards(false);
+
     storm::prism::Program program = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/mdp/two_dice.nm");
     program = program.substituteConstants();
     program = program.flattenModules(std::make_shared<storm::utility::solver::MathsatSmtSolverFactory>());
@@ -600,9 +669,13 @@ TEST(PrismMenuGame, TwoDiceFullAbstractionTest_Cudd) {
     EXPECT_EQ(436ull, game.getNumberOfTransitions());
     EXPECT_EQ(169ull, game.getNumberOfStates());
     EXPECT_EQ(0ull, game.getBottomStates().getNonZeroCount());
+
+    storm::settings::mutableAbstractionSettings().restoreDefaults();
 }
 
 TEST(PrismMenuGame, TwoDiceFullAbstractionTest_Sylvan) {
+    storm::settings::mutableAbstractionSettings().setAddAllGuards(false);
+
     storm::prism::Program program = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/mdp/two_dice.nm");
     program = program.substituteConstants();
     program = program.flattenModules(std::make_shared<storm::utility::solver::MathsatSmtSolverFactory>());
@@ -655,9 +728,13 @@ TEST(PrismMenuGame, TwoDiceFullAbstractionTest_Sylvan) {
     EXPECT_EQ(436ull, game.getNumberOfTransitions());
     EXPECT_EQ(169ull, game.getNumberOfStates());
     EXPECT_EQ(0ull, game.getBottomStates().getNonZeroCount());
+
+    storm::settings::mutableAbstractionSettings().restoreDefaults();
 }
 
 TEST(PrismMenuGame, WlanAbstractionTest_Cudd) {
+    storm::settings::mutableAbstractionSettings().setAddAllGuards(false);
+
     storm::prism::Program program = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/mdp/wlan0-2-4.nm");
     program = program.substituteConstants();
     program = program.flattenModules(std::make_shared<storm::utility::solver::MathsatSmtSolverFactory>());
@@ -680,9 +757,13 @@ TEST(PrismMenuGame, WlanAbstractionTest_Cudd) {
     EXPECT_EQ(915ull, game.getNumberOfTransitions());
     EXPECT_EQ(8ull, game.getNumberOfStates());
     EXPECT_EQ(4ull, game.getBottomStates().getNonZeroCount());
+
+    storm::settings::mutableAbstractionSettings().restoreDefaults();
 }
 
 TEST(PrismMenuGame, WlanAbstractionTest_Sylvan) {
+    storm::settings::mutableAbstractionSettings().setAddAllGuards(false);
+
     storm::prism::Program program = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/mdp/wlan0-2-4.nm");
     program = program.substituteConstants();
     program = program.flattenModules(std::make_shared<storm::utility::solver::MathsatSmtSolverFactory>());
@@ -705,9 +786,13 @@ TEST(PrismMenuGame, WlanAbstractionTest_Sylvan) {
     EXPECT_EQ(915ull, game.getNumberOfTransitions());
     EXPECT_EQ(8ull, game.getNumberOfStates());
     EXPECT_EQ(4ull, game.getBottomStates().getNonZeroCount());
+
+    storm::settings::mutableAbstractionSettings().restoreDefaults();
 }
 
 TEST(PrismMenuGame, WlanAbstractionAndRefinementTest_Cudd) {
+    storm::settings::mutableAbstractionSettings().setAddAllGuards(false);
+    
     storm::prism::Program program = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/mdp/wlan0-2-4.nm");
     program = program.substituteConstants();
     program = program.flattenModules(std::make_shared<storm::utility::solver::MathsatSmtSolverFactory>());
@@ -732,9 +817,13 @@ TEST(PrismMenuGame, WlanAbstractionAndRefinementTest_Cudd) {
     EXPECT_EQ(1824ull, game.getNumberOfTransitions());
     EXPECT_EQ(16ull, game.getNumberOfStates());
     EXPECT_EQ(8ull, game.getBottomStates().getNonZeroCount());
+
+    storm::settings::mutableAbstractionSettings().restoreDefaults();
 }
 
 TEST(PrismMenuGame, WlanAbstractionAndRefinementTest_Sylvan) {
+    storm::settings::mutableAbstractionSettings().setAddAllGuards(false);
+
     storm::prism::Program program = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/mdp/wlan0-2-4.nm");
     program = program.substituteConstants();
     program = program.flattenModules(std::make_shared<storm::utility::solver::MathsatSmtSolverFactory>());
@@ -759,9 +848,13 @@ TEST(PrismMenuGame, WlanAbstractionAndRefinementTest_Sylvan) {
     EXPECT_EQ(1824ull, game.getNumberOfTransitions());
     EXPECT_EQ(16ull, game.getNumberOfStates());
     EXPECT_EQ(8ull, game.getBottomStates().getNonZeroCount());
+
+    storm::settings::mutableAbstractionSettings().restoreDefaults();
 }
 
 TEST(PrismMenuGame, WlanFullAbstractionTest_Cudd) {
+    storm::settings::mutableAbstractionSettings().setAddAllGuards(false);
+
     storm::prism::Program program = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/mdp/wlan0-2-4.nm");
     program = program.substituteConstants();
     program = program.flattenModules(std::make_shared<storm::utility::solver::MathsatSmtSolverFactory>());
@@ -882,9 +975,13 @@ TEST(PrismMenuGame, WlanFullAbstractionTest_Cudd) {
     EXPECT_EQ(9503ull, game.getNumberOfTransitions());
     EXPECT_EQ(5523ull, game.getNumberOfStates());
     EXPECT_EQ(0ull, game.getBottomStates().getNonZeroCount());
+
+    storm::settings::mutableAbstractionSettings().restoreDefaults();
 }
 
 TEST(PrismMenuGame, WlanFullAbstractionTest_Sylvan) {
+    storm::settings::mutableAbstractionSettings().setAddAllGuards(false);
+
     storm::prism::Program program = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/mdp/wlan0-2-4.nm");
     program = program.substituteConstants();
     program = program.flattenModules(std::make_shared<storm::utility::solver::MathsatSmtSolverFactory>());
@@ -1005,6 +1102,8 @@ TEST(PrismMenuGame, WlanFullAbstractionTest_Sylvan) {
     EXPECT_EQ(9503ull, game.getNumberOfTransitions());
     EXPECT_EQ(5523ull, game.getNumberOfStates());
     EXPECT_EQ(0ull, game.getBottomStates().getNonZeroCount());
+
+    storm::settings::mutableAbstractionSettings().restoreDefaults();
 }
 
 #endif

src/test/logic/FragmentCheckerTest.cpp

@@ -83,7 +83,7 @@ TEST(FragmentCheckerTest, Prctl) {
     EXPECT_TRUE(checker.conformsToSpecification(*formula, prctl));
 
     ASSERT_NO_THROW(formula = formulaParser.parseSingleFormulaFromString("P=? [F[0,1] \"label\"]"));
-    EXPECT_FALSE(checker.conformsToSpecification(*formula, prctl));
+    EXPECT_TRUE(checker.conformsToSpecification(*formula, prctl));
 }
 
 TEST(FragmentCheckerTest, Csl) {
@@ -160,7 +160,7 @@ TEST(FragmentCheckerTest, MultiObjective) {
     EXPECT_TRUE(checker.conformsToSpecification(*formula, multiobjective));
     
     ASSERT_NO_THROW(formula = formulaParser.parseSingleFormulaFromString("P=? [F[0.5,1] \"label\"]"));
-    EXPECT_FALSE(checker.conformsToSpecification(*formula, multiobjective));
+    EXPECT_TRUE(checker.conformsToSpecification(*formula, multiobjective));
     
     ASSERT_NO_THROW(formula = formulaParser.parseSingleFormulaFromString("multi(R<0.3 [ C ], P<0.6 [F \"label\"] & \"label\" & R<=4[F \"label\"])"));
     EXPECT_FALSE(checker.conformsToSpecification(*formula, multiobjective));

src/test/modelchecker/GmmxxCtmcCslModelCheckerTest.cpp

@@ -68,14 +68,14 @@ TEST(GmmxxCtmcCslModelCheckerTest, Cluster) {
     storm::modelchecker::ExplicitQuantitativeCheckResult<double> quantitativeCheckResult4 = checkResult->asExplicitQuantitativeCheckResult<double>();
     EXPECT_NEAR(1, quantitativeCheckResult4[initialState], storm::settings::getModule<storm::settings::modules::GeneralSettings>().getPrecision());
     
-    formula = formulaParser.parseSingleFormulaFromString("P=? [ !\"minimum\" U[1,inf] \"minimum\"]");
+    formula = formulaParser.parseSingleFormulaFromString("P=? [ !\"minimum\" U>=1 \"minimum\"]");
     checkResult = modelchecker.check(*formula);
     
     ASSERT_TRUE(checkResult->isExplicitQuantitativeCheckResult());
     storm::modelchecker::ExplicitQuantitativeCheckResult<double> quantitativeCheckResult5 = checkResult->asExplicitQuantitativeCheckResult<double>();
     EXPECT_NEAR(0, quantitativeCheckResult5[initialState], storm::settings::getModule<storm::settings::modules::GeneralSettings>().getPrecision());
     
-    formula = formulaParser.parseSingleFormulaFromString("P=? [ \"minimum\" U[1,inf] !\"minimum\"]");
+    formula = formulaParser.parseSingleFormulaFromString("P=? [ \"minimum\" U>=1 !\"minimum\"]");
     checkResult = modelchecker.check(*formula);
     
     ASSERT_TRUE(checkResult->isExplicitQuantitativeCheckResult());

src/test/modelchecker/GmmxxHybridCtmcCslModelCheckerTest.cpp

@@ -85,7 +85,7 @@ TEST(GmmxxHybridCtmcCslModelCheckerTest, Cluster_Cudd) {
     EXPECT_NEAR(1, quantitativeCheckResult4.getMin(), storm::settings::getModule<storm::settings::modules::GeneralSettings>().getPrecision());
     EXPECT_NEAR(1, quantitativeCheckResult4.getMax(), storm::settings::getModule<storm::settings::modules::GeneralSettings>().getPrecision());
     
-    formula = formulaParser.parseSingleFormulaFromString("P=? [ !\"minimum\" U[1,inf] \"minimum\"]");
+    formula = formulaParser.parseSingleFormulaFromString("P=? [ !\"minimum\" U>=1 \"minimum\"]");
     checkResult = modelchecker.check(*formula);
     
     ASSERT_TRUE(checkResult->isHybridQuantitativeCheckResult());
@@ -94,7 +94,7 @@ TEST(GmmxxHybridCtmcCslModelCheckerTest, Cluster_Cudd) {
     EXPECT_NEAR(0, quantitativeCheckResult5.getMin(), storm::settings::getModule<storm::settings::modules::GeneralSettings>().getPrecision());
     EXPECT_NEAR(0, quantitativeCheckResult5.getMax(), storm::settings::getModule<storm::settings::modules::GeneralSettings>().getPrecision());
     
-    formula = formulaParser.parseSingleFormulaFromString("P=? [ \"minimum\" U[1,inf] !\"minimum\"]");
+    formula = formulaParser.parseSingleFormulaFromString("P=? [ \"minimum\" U>=1 !\"minimum\"]");
     checkResult = modelchecker.check(*formula);
     
     ASSERT_TRUE(checkResult->isHybridQuantitativeCheckResult());
@@ -183,7 +183,7 @@ TEST(GmmxxHybridCtmcCslModelCheckerTest, Cluster_Sylvan) {
     EXPECT_NEAR(1, quantitativeCheckResult4.getMin(), storm::settings::getModule<storm::settings::modules::GeneralSettings>().getPrecision());
     EXPECT_NEAR(1, quantitativeCheckResult4.getMax(), storm::settings::getModule<storm::settings::modules::GeneralSettings>().getPrecision());
     
-    formula = formulaParser.parseSingleFormulaFromString("P=? [ !\"minimum\" U[1,inf] \"minimum\"]");
+    formula = formulaParser.parseSingleFormulaFromString("P=? [ !\"minimum\" U>=1 \"minimum\"]");
     checkResult = modelchecker.check(*formula);
     
     ASSERT_TRUE(checkResult->isHybridQuantitativeCheckResult());
@@ -192,7 +192,7 @@ TEST(GmmxxHybridCtmcCslModelCheckerTest, Cluster_Sylvan) {
     EXPECT_NEAR(0, quantitativeCheckResult5.getMin(), storm::settings::getModule<storm::settings::modules::GeneralSettings>().getPrecision());
     EXPECT_NEAR(0, quantitativeCheckResult5.getMax(), storm::settings::getModule<storm::settings::modules::GeneralSettings>().getPrecision());
     
-    formula = formulaParser.parseSingleFormulaFromString("P=? [ \"minimum\" U[1,inf] !\"minimum\"]");
+    formula = formulaParser.parseSingleFormulaFromString("P=? [ \"minimum\" U>=1 !\"minimum\"]");
     checkResult = modelchecker.check(*formula);
     
     ASSERT_TRUE(checkResult->isHybridQuantitativeCheckResult());

src/test/modelchecker/NativeCtmcCslModelCheckerTest.cpp

@@ -63,14 +63,14 @@ TEST(NativeCtmcCslModelCheckerTest, Cluster) {
     storm::modelchecker::ExplicitQuantitativeCheckResult<double> quantitativeCheckResult4 = checkResult->asExplicitQuantitativeCheckResult<double>();
     EXPECT_NEAR(1, quantitativeCheckResult4[initialState], storm::settings::getModule<storm::settings::modules::GeneralSettings>().getPrecision());
     
-    formula = formulaParser.parseSingleFormulaFromString("P=? [ !\"minimum\" U[1,inf] \"minimum\"]");
+    formula = formulaParser.parseSingleFormulaFromString("P=? [ !\"minimum\" U>=1 \"minimum\"]");
     checkResult = modelchecker.check(*formula);
     
     ASSERT_TRUE(checkResult->isExplicitQuantitativeCheckResult());
     storm::modelchecker::ExplicitQuantitativeCheckResult<double> quantitativeCheckResult5 = checkResult->asExplicitQuantitativeCheckResult<double>();
     EXPECT_NEAR(0, quantitativeCheckResult5[initialState], storm::settings::getModule<storm::settings::modules::GeneralSettings>().getPrecision());
     
-    formula = formulaParser.parseSingleFormulaFromString("P=? [ \"minimum\" U[1,inf] !\"minimum\"]");
+    formula = formulaParser.parseSingleFormulaFromString("P=? [ \"minimum\" U>=1 !\"minimum\"]");
     checkResult = modelchecker.check(*formula);
     
     ASSERT_TRUE(checkResult->isExplicitQuantitativeCheckResult());

src/test/modelchecker/NativeHybridCtmcCslModelCheckerTest.cpp

@@ -83,7 +83,7 @@ TEST(NativeHybridCtmcCslModelCheckerTest, Cluster_Cudd) {
     EXPECT_NEAR(1, quantitativeCheckResult4.getMin(), storm::settings::getModule<storm::settings::modules::GeneralSettings>().getPrecision());
     EXPECT_NEAR(1, quantitativeCheckResult4.getMax(), storm::settings::getModule<storm::settings::modules::GeneralSettings>().getPrecision());
     
-    formula = formulaParser.parseSingleFormulaFromString("P=? [ !\"minimum\" U[1,inf] \"minimum\"]");
+    formula = formulaParser.parseSingleFormulaFromString("P=? [ !\"minimum\" U>=1 \"minimum\"]");
     checkResult = modelchecker.check(*formula);
     
     ASSERT_TRUE(checkResult->isHybridQuantitativeCheckResult());
@@ -92,7 +92,7 @@ TEST(NativeHybridCtmcCslModelCheckerTest, Cluster_Cudd) {
     EXPECT_NEAR(0, quantitativeCheckResult5.getMin(), storm::settings::getModule<storm::settings::modules::GeneralSettings>().getPrecision());
     EXPECT_NEAR(0, quantitativeCheckResult5.getMax(), storm::settings::getModule<storm::settings::modules::GeneralSettings>().getPrecision());
     
-    formula = formulaParser.parseSingleFormulaFromString("P=? [ \"minimum\" U[1,inf] !\"minimum\"]");
+    formula = formulaParser.parseSingleFormulaFromString("P=? [ \"minimum\" U>=1 !\"minimum\"]");
     checkResult = modelchecker.check(*formula);
     
     ASSERT_TRUE(checkResult->isHybridQuantitativeCheckResult());
@@ -181,7 +181,7 @@ TEST(NativeHybridCtmcCslModelCheckerTest, Cluster_Sylvan) {
     EXPECT_NEAR(1, quantitativeCheckResult4.getMin(), storm::settings::getModule<storm::settings::modules::GeneralSettings>().getPrecision());
     EXPECT_NEAR(1, quantitativeCheckResult4.getMax(), storm::settings::getModule<storm::settings::modules::GeneralSettings>().getPrecision());
     
-    formula = formulaParser.parseSingleFormulaFromString("P=? [ !\"minimum\" U[1,inf] \"minimum\"]");
+    formula = formulaParser.parseSingleFormulaFromString("P=? [ !\"minimum\" U>=1 \"minimum\"]");
     checkResult = modelchecker.check(*formula);
     
     ASSERT_TRUE(checkResult->isHybridQuantitativeCheckResult());
@@ -190,7 +190,7 @@ TEST(NativeHybridCtmcCslModelCheckerTest, Cluster_Sylvan) {
     EXPECT_NEAR(0, quantitativeCheckResult5.getMin(), storm::settings::getModule<storm::settings::modules::GeneralSettings>().getPrecision());
     EXPECT_NEAR(0, quantitativeCheckResult5.getMax(), storm::settings::getModule<storm::settings::modules::GeneralSettings>().getPrecision());
     
-    formula = formulaParser.parseSingleFormulaFromString("P=? [ \"minimum\" U[1,inf] !\"minimum\"]");
+    formula = formulaParser.parseSingleFormulaFromString("P=? [ \"minimum\" U>=1 !\"minimum\"]");
     checkResult = modelchecker.check(*formula);
     
     ASSERT_TRUE(checkResult->isHybridQuantitativeCheckResult());

src/test/storage/DeterministicModelBisimulationDecompositionTest.cpp

@@ -1,6 +1,7 @@
 #include "gtest/gtest.h"
 #include "storm-config.h"
 #include "storm/parser/AutoParser.h"
+#include "storm/parser/FormulaParser.h"
 #include "storm/storage/bisimulation/DeterministicModelBisimulationDecomposition.h"
 #include "storm/models/sparse/Dtmc.h"
 #include "storm/models/sparse/StandardRewardModel.h"
@@ -45,14 +46,10 @@ TEST(DeterministicModelBisimulationDecomposition, Die) {
     EXPECT_EQ(5ul, result->getNumberOfStates());
     EXPECT_EQ(8ul, result->getNumberOfTransitions());
 
-    auto labelFormula = std::make_shared<storm::logic::AtomicLabelFormula>("one");
-    auto eventuallyFormula = std::make_shared<storm::logic::EventuallyFormula>(labelFormula);
-
-#ifdef WINDOWS
-    storm::storage::DeterministicModelBisimulationDecomposition<storm::models::sparse::Dtmc<double>>::Options options2(*dtmc, *eventuallyFormula);
-#else
-    typename storm::storage::DeterministicModelBisimulationDecomposition<storm::models::sparse::Dtmc<double>>::Options options2(*dtmc, *eventuallyFormula);
-#endif
+    storm::parser::FormulaParser formulaParser;
+    std::shared_ptr<storm::logic::Formula const> formula = formulaParser.parseSingleFormulaFromString("P=? [F \"one\"]");
+    
+    typename storm::storage::DeterministicModelBisimulationDecomposition<storm::models::sparse::Dtmc<double>>::Options options2(*dtmc, *formula);
 
     storm::storage::DeterministicModelBisimulationDecomposition<storm::models::sparse::Dtmc<double>> bisim4(*dtmc, options2);
     ASSERT_NO_THROW(bisim4.computeBisimulationDecomposition());
@@ -102,29 +99,11 @@ TEST(DeterministicModelBisimulationDecomposition, Crowds) {
     EXPECT_EQ(43ul, result->getNumberOfStates());
     EXPECT_EQ(83ul, result->getNumberOfTransitions());
 
-    auto labelFormula = std::make_shared<storm::logic::AtomicLabelFormula>("observe0Greater1");
-    auto eventuallyFormula = std::make_shared<storm::logic::EventuallyFormula>(labelFormula);
-
-#ifdef WINDOWS
-    storm::storage::DeterministicModelBisimulationDecomposition<storm::models::sparse::Dtmc<double>>::Options options2(*dtmc, *eventuallyFormula);
-#else
-    typename storm::storage::DeterministicModelBisimulationDecomposition<storm::models::sparse::Dtmc<double>>::Options options2(*dtmc, *eventuallyFormula);
-#endif
-    storm::storage::DeterministicModelBisimulationDecomposition<storm::models::sparse::Dtmc<double>> bisim4(*dtmc, options2);
-    ASSERT_NO_THROW(bisim4.computeBisimulationDecomposition());
-    ASSERT_NO_THROW(result = bisim4.getQuotient());
-
-    EXPECT_EQ(storm::models::ModelType::Dtmc, result->getType());
-    EXPECT_EQ(64ul, result->getNumberOfStates());
-    EXPECT_EQ(104ul, result->getNumberOfTransitions());
+    storm::parser::FormulaParser formulaParser;
+    std::shared_ptr<storm::logic::Formula const> formula = formulaParser.parseSingleFormulaFromString("P=? [F \"observe0Greater1\"]");
 
-    auto probabilityOperatorFormula = std::make_shared<storm::logic::ProbabilityOperatorFormula>(eventuallyFormula);
+    typename storm::storage::DeterministicModelBisimulationDecomposition<storm::models::sparse::Dtmc<double>>::Options options3(*dtmc, *formula);
 
-#ifdef WINDOWS
-    storm::storage::DeterministicModelBisimulationDecomposition<storm::models::sparse::Dtmc<double>>::Options options3(*dtmc, *probabilityOperatorFormula);
-#else
-    typename storm::storage::DeterministicModelBisimulationDecomposition<storm::models::sparse::Dtmc<double>>::Options options3(*dtmc, *probabilityOperatorFormula);
-#endif
     storm::storage::DeterministicModelBisimulationDecomposition<storm::models::sparse::Dtmc<double>> bisim5(*dtmc, options3);
     ASSERT_NO_THROW(bisim5.computeBisimulationDecomposition());
     ASSERT_NO_THROW(result = bisim5.getQuotient());
@@ -133,13 +112,10 @@ TEST(DeterministicModelBisimulationDecomposition, Crowds) {
     EXPECT_EQ(64ul, result->getNumberOfStates());
     EXPECT_EQ(104ul, result->getNumberOfTransitions());
 
-    auto boundedUntilFormula = std::make_shared<storm::logic::BoundedUntilFormula>(std::make_shared<storm::logic::BooleanLiteralFormula>(true), labelFormula, 50);
+    formula = formulaParser.parseSingleFormulaFromString("P=? [true U<=50 \"observe0Greater1\"] ");
+
+    typename storm::storage::DeterministicModelBisimulationDecomposition<storm::models::sparse::Dtmc<double>>::Options options4(*dtmc, *formula);
 
-#ifdef WINDOWS
-    storm::storage::DeterministicModelBisimulationDecomposition<storm::models::sparse::Dtmc<double>>::Options options4(*dtmc, *boundedUntilFormula);
-#else
-    typename storm::storage::DeterministicModelBisimulationDecomposition<storm::models::sparse::Dtmc<double>>::Options options4(*dtmc, *boundedUntilFormula);
-#endif
     storm::storage::DeterministicModelBisimulationDecomposition<storm::models::sparse::Dtmc<double>> bisim6(*dtmc, options4);
     ASSERT_NO_THROW(bisim6.computeBisimulationDecomposition());
     ASSERT_NO_THROW(result = bisim6.getQuotient());

src/test/utility/GraphTest.cpp

@@ -226,15 +226,15 @@ TEST(GraphTest, SymbolicProb01StochasticGameDieSmall) {
     storm::abstraction::MenuGame<storm::dd::DdType::CUDD, double> game = abstractor.abstract();
     
     // The target states are those states where !(s < 3).
-    storm::dd::Bdd<storm::dd::DdType::CUDD> targetStates = game.getStates(initialPredicates[0], true);
+    storm::dd::Bdd<storm::dd::DdType::CUDD> targetStates = !abstractor.getStates(initialPredicates[0]) && game.getReachableStates();
     
     storm::utility::graph::GameProb01Result<storm::dd::DdType::CUDD> result = storm::utility::graph::performProb0(game, game.getQualitativeTransitionMatrix(), game.getReachableStates(), targetStates, storm::OptimizationDirection::Minimize, storm::OptimizationDirection::Minimize, true, true);
-    EXPECT_EQ(1ull, result.getPlayer1States().getNonZeroCount());
+    EXPECT_EQ(0ull, result.getPlayer1States().getNonZeroCount());
     EXPECT_TRUE(result.hasPlayer1Strategy());
     EXPECT_TRUE(result.hasPlayer2Strategy());
     
     result = storm::utility::graph::performProb1(game, game.getQualitativeTransitionMatrix(), game.getReachableStates(), targetStates, storm::OptimizationDirection::Minimize, storm::OptimizationDirection::Minimize);
-    EXPECT_EQ(3ull, result.getPlayer1States().getNonZeroCount());
+    EXPECT_EQ(8ull, result.getPlayer1States().getNonZeroCount());
     
     result = storm::utility::graph::performProb0(game, game.getQualitativeTransitionMatrix(), game.getReachableStates(), targetStates, storm::OptimizationDirection::Minimize, storm::OptimizationDirection::Maximize);
     EXPECT_EQ(0ull, result.getPlayer1States().getNonZeroCount());
@@ -246,13 +246,13 @@ TEST(GraphTest, SymbolicProb01StochasticGameDieSmall) {
     EXPECT_EQ(0ull, result.getPlayer1States().getNonZeroCount());
     
     result = storm::utility::graph::performProb1(game, game.getQualitativeTransitionMatrix(), game.getReachableStates(), targetStates, storm::OptimizationDirection::Maximize, storm::OptimizationDirection::Minimize);
-    EXPECT_EQ(4ull, result.getPlayer1States().getNonZeroCount());
+    EXPECT_EQ(8ull, result.getPlayer1States().getNonZeroCount());
     
     result = storm::utility::graph::performProb0(game, game.getQualitativeTransitionMatrix(), game.getReachableStates(), targetStates, storm::OptimizationDirection::Maximize, storm::OptimizationDirection::Maximize);
     EXPECT_EQ(0ull, result.getPlayer1States().getNonZeroCount());
     
     result = storm::utility::graph::performProb1(game, game.getQualitativeTransitionMatrix(), game.getReachableStates(), targetStates, storm::OptimizationDirection::Maximize, storm::OptimizationDirection::Maximize, true, true);
-    EXPECT_EQ(4ull, result.getPlayer1States().getNonZeroCount());
+    EXPECT_EQ(8ull, result.getPlayer1States().getNonZeroCount());
     EXPECT_TRUE(result.hasPlayer1Strategy());
     EXPECT_TRUE(result.hasPlayer2Strategy());
     
@@ -260,7 +260,7 @@ TEST(GraphTest, SymbolicProb01StochasticGameDieSmall) {
     game = abstractor.abstract();
     
     // We need to create a new BDD for the target states since the reachable states might have changed.
-    targetStates = game.getStates(initialPredicates[0], true);
+    targetStates = !abstractor.getStates(initialPredicates[0]) && game.getReachableStates();
     
     result = storm::utility::graph::performProb0(game, game.getQualitativeTransitionMatrix(), game.getReachableStates(), targetStates, storm::OptimizationDirection::Minimize, storm::OptimizationDirection::Minimize, true, true);
     EXPECT_EQ(0ull, result.getPlayer1States().getNonZeroCount());
@@ -280,25 +280,25 @@ TEST(GraphTest, SymbolicProb01StochasticGameDieSmall) {
     EXPECT_EQ(0.0, stateDistributionCount.getMax());
     
     result = storm::utility::graph::performProb1(game, game.getQualitativeTransitionMatrix(), game.getReachableStates(), targetStates, storm::OptimizationDirection::Minimize, storm::OptimizationDirection::Minimize);
-    EXPECT_EQ(5ull, result.getPlayer1States().getNonZeroCount());
+    EXPECT_EQ(8ull, result.getPlayer1States().getNonZeroCount());
     
     result = storm::utility::graph::performProb0(game, game.getQualitativeTransitionMatrix(), game.getReachableStates(), targetStates, storm::OptimizationDirection::Minimize, storm::OptimizationDirection::Maximize);
     EXPECT_EQ(0ull, result.getPlayer1States().getNonZeroCount());
     
     result = storm::utility::graph::performProb1(game, game.getQualitativeTransitionMatrix(), game.getReachableStates(), targetStates, storm::OptimizationDirection::Minimize, storm::OptimizationDirection::Maximize);
-    EXPECT_EQ(5ull, result.getPlayer1States().getNonZeroCount());
+    EXPECT_EQ(8ull, result.getPlayer1States().getNonZeroCount());
     
     result = storm::utility::graph::performProb0(game, game.getQualitativeTransitionMatrix(), game.getReachableStates(), targetStates, storm::OptimizationDirection::Maximize, storm::OptimizationDirection::Minimize);
     EXPECT_EQ(0ull, result.getPlayer1States().getNonZeroCount());
     
     result = storm::utility::graph::performProb1(game, game.getQualitativeTransitionMatrix(), game.getReachableStates(), targetStates, storm::OptimizationDirection::Maximize, storm::OptimizationDirection::Minimize);
-    EXPECT_EQ(5ull, result.getPlayer1States().getNonZeroCount());
+    EXPECT_EQ(8ull, result.getPlayer1States().getNonZeroCount());
     
     result = storm::utility::graph::performProb0(game, game.getQualitativeTransitionMatrix(), game.getReachableStates(), targetStates, storm::OptimizationDirection::Maximize, storm::OptimizationDirection::Maximize);
     EXPECT_EQ(0ull, result.getPlayer1States().getNonZeroCount());
     
     result = storm::utility::graph::performProb1(game, game.getQualitativeTransitionMatrix(), game.getReachableStates(), targetStates, storm::OptimizationDirection::Maximize, storm::OptimizationDirection::Maximize, true, true);
-    EXPECT_EQ(5ull, result.getPlayer1States().getNonZeroCount());
+    EXPECT_EQ(8ull, result.getPlayer1States().getNonZeroCount());
     EXPECT_TRUE(result.hasPlayer1Strategy());
     EXPECT_TRUE(result.hasPlayer2Strategy());
     
@@ -308,7 +308,7 @@ TEST(GraphTest, SymbolicProb01StochasticGameDieSmall) {
     
     // Proceed by checking whether they select exactly one action in each state.
     stateDistributionsUnderStrategies = (game.getTransitionMatrix() * result.player1Strategy.get().template toAdd<double>() * result.player2Strategy.get().template toAdd<double>()).sumAbstract(game.getColumnVariables());
-    EXPECT_EQ(5ull, stateDistributionsUnderStrategies.getNonZeroCount());
+    EXPECT_EQ(8ull, stateDistributionsUnderStrategies.getNonZeroCount());
     
     // Check that the number of distributions per state is one (or zero in the case where there are no prob1 states).
     stateDistributionCount = stateDistributionsUnderStrategies.sumAbstract(game.getNondeterminismVariables());
@@ -364,8 +364,8 @@ TEST(GraphTest, SymbolicProb01StochasticGameTwoDice) {
 
     storm::abstraction::MenuGame<storm::dd::DdType::CUDD, double> game = abstractor.abstract();
     
-    // The target states are those states where s1 == 7 & s2 == 7 & d1 + d2 == 1.
-    storm::dd::Bdd<storm::dd::DdType::CUDD> targetStates = game.getStates(initialPredicates[7], false) && game.getStates(initialPredicates[22], false) && game.getStates(initialPredicates[9], false) && game.getStates(initialPredicates[24], false);
+    // The target states are those states where s1 == 7 & s2 == 7 & d1 + d2 == 2.
+    storm::dd::Bdd<storm::dd::DdType::CUDD> targetStates = abstractor.getStates(initialPredicates[7]) && abstractor.getStates(initialPredicates[22]) && abstractor.getStates(initialPredicates[9]) && abstractor.getStates(initialPredicates[24]) && game.getReachableStates();
     
     storm::utility::graph::GameProb01Result<storm::dd::DdType::CUDD> result = storm::utility::graph::performProb0(game, game.getQualitativeTransitionMatrix(), game.getReachableStates(), targetStates, storm::OptimizationDirection::Minimize, storm::OptimizationDirection::Minimize, true, true);
     EXPECT_EQ(153ull, result.getPlayer1States().getNonZeroCount());
@@ -537,7 +537,7 @@ TEST(GraphTest, SymbolicProb01StochasticGameWlan) {
     storm::abstraction::MenuGame<storm::dd::DdType::CUDD, double> game = abstractor.abstract();
     
     // The target states are those states where col == 2.
-    storm::dd::Bdd<storm::dd::DdType::CUDD> targetStates = game.getStates(initialPredicates[2], false);
+    storm::dd::Bdd<storm::dd::DdType::CUDD> targetStates = abstractor.getStates(initialPredicates[2]) && game.getReachableStates();
     
     storm::utility::graph::GameProb01Result<storm::dd::DdType::CUDD> result = storm::utility::graph::performProb0(game, game.getQualitativeTransitionMatrix(), game.getReachableStates(), targetStates, storm::OptimizationDirection::Minimize, storm::OptimizationDirection::Minimize, true, true);
     EXPECT_EQ(2831ull, result.getPlayer1States().getNonZeroCount());