diff --git a/src/storm/abstraction/MenuGame.cpp b/src/storm/abstraction/MenuGame.cpp index 596f05b39..799003820 100644 --- a/src/storm/abstraction/MenuGame.cpp +++ b/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) { diff --git a/src/storm/logic/BoundedUntilFormula.cpp b/src/storm/logic/BoundedUntilFormula.cpp index 97734340e..b3bc3ea1a 100644 --- a/src/storm/logic/BoundedUntilFormula.cpp +++ b/src/storm/logic/BoundedUntilFormula.cpp @@ -9,7 +9,19 @@ namespace storm { namespace logic { - BoundedUntilFormula::BoundedUntilFormula(std::shared_ptr const& leftSubformula, std::shared_ptr const& rightSubformula, boost::optional const& lowerBound, boost::optional 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 const& leftSubformula, std::shared_ptr const& rightSubformula, boost::optional const& lowerBound, boost::optional 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; diff --git a/src/storm/logic/BoundedUntilFormula.h b/src/storm/logic/BoundedUntilFormula.h index 6780061f8..24b89d936 100644 --- a/src/storm/logic/BoundedUntilFormula.h +++ b/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; diff --git a/src/storm/logic/FragmentSpecification.cpp b/src/storm/logic/FragmentSpecification.cpp index 4720c2e6b..0790c48a6 100644 --- a/src/storm/logic/FragmentSpecification.cpp +++ b/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; } diff --git a/src/storm/modelchecker/multiobjective/pcaa/SparsePcaaPreprocessor.cpp b/src/storm/modelchecker/multiobjective/pcaa/SparsePcaaPreprocessor.cpp index daef0687c..56f7891c8 100644 --- a/src/storm/modelchecker/multiobjective/pcaa/SparsePcaaPreprocessor.cpp +++ b/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(); + // FIXME: really convert formula bound to value type? + if (formula.hasIntegerLowerBound()) { + currentObjective.lowerTimeBound = storm::utility::convertNumber(formula.getLowerBound()); + } else { + currentObjective.lowerTimeBound = storm::utility::convertNumber(formula.getLowerBound()); + } } 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(); + // FIXME: really convert formula bound to value type? + if (formula.hasIntegerUpperBound()) { + currentObjective.upperTimeBound = storm::utility::convertNumber(formula.getUpperBound()); + } else { + currentObjective.upperTimeBound = storm::utility::convertNumber(formula.getUpperBound()); + } } else { currentObjective.upperTimeBound = storm::utility::infinity(); } diff --git a/src/storm/modelchecker/prctl/HybridDtmcPrctlModelChecker.cpp b/src/storm/modelchecker/prctl/HybridDtmcPrctlModelChecker.cpp index 723c2ca1b..c5f29b568 100644 --- a/src/storm/modelchecker/prctl/HybridDtmcPrctlModelChecker.cpp +++ b/src/storm/modelchecker/prctl/HybridDtmcPrctlModelChecker.cpp @@ -76,7 +76,7 @@ namespace storm { std::unique_ptr rightResultPointer = this->check(pathFormula.getRightSubformula()); SymbolicQualitativeCheckResult const& leftResult = leftResultPointer->asSymbolicQualitativeCheckResult(); SymbolicQualitativeCheckResult const& rightResult = rightResultPointer->asSymbolicQualitativeCheckResult(); - return storm::modelchecker::helper::HybridDtmcPrctlHelper::computeBoundedUntilProbabilities(this->getModel(), this->getModel().getTransitionMatrix(), leftResult.getTruthValuesVector(), rightResult.getTruthValuesVector(), pathFormula.getUpperBound(), *this->linearEquationSolverFactory); + return storm::modelchecker::helper::HybridDtmcPrctlHelper::computeBoundedUntilProbabilities(this->getModel(), this->getModel().getTransitionMatrix(), leftResult.getTruthValuesVector(), rightResult.getTruthValuesVector(), pathFormula.getUpperBound() + (pathFormula.isUpperBoundStrict() ? 1ull : 0ull), *this->linearEquationSolverFactory); } template diff --git a/src/storm/modelchecker/prctl/HybridMdpPrctlModelChecker.cpp b/src/storm/modelchecker/prctl/HybridMdpPrctlModelChecker.cpp index 6ef453636..1a6c7721a 100644 --- a/src/storm/modelchecker/prctl/HybridMdpPrctlModelChecker.cpp +++ b/src/storm/modelchecker/prctl/HybridMdpPrctlModelChecker.cpp @@ -74,7 +74,7 @@ namespace storm { std::unique_ptr rightResultPointer = this->check(pathFormula.getRightSubformula()); SymbolicQualitativeCheckResult const& leftResult = leftResultPointer->asSymbolicQualitativeCheckResult(); SymbolicQualitativeCheckResult const& rightResult = rightResultPointer->asSymbolicQualitativeCheckResult(); - return storm::modelchecker::helper::HybridMdpPrctlHelper::computeBoundedUntilProbabilities(checkTask.getOptimizationDirection(), this->getModel(), this->getModel().getTransitionMatrix(), leftResult.getTruthValuesVector(), rightResult.getTruthValuesVector(), pathFormula.getUpperBound(), *this->linearEquationSolverFactory); + return storm::modelchecker::helper::HybridMdpPrctlHelper::computeBoundedUntilProbabilities(checkTask.getOptimizationDirection(), this->getModel(), this->getModel().getTransitionMatrix(), leftResult.getTruthValuesVector(), rightResult.getTruthValuesVector(), pathFormula.getUpperBound() + (pathFormula.isUpperBoundStrict() ? 1ull : 0ull), *this->linearEquationSolverFactory); } template diff --git a/src/storm/modelchecker/prctl/SparseDtmcPrctlModelChecker.cpp b/src/storm/modelchecker/prctl/SparseDtmcPrctlModelChecker.cpp index 509a8db06..e82bef01e 100644 --- a/src/storm/modelchecker/prctl/SparseDtmcPrctlModelChecker.cpp +++ b/src/storm/modelchecker/prctl/SparseDtmcPrctlModelChecker.cpp @@ -48,7 +48,7 @@ namespace storm { std::unique_ptr rightResultPointer = this->check(pathFormula.getRightSubformula()); ExplicitQualitativeCheckResult const& leftResult = leftResultPointer->asExplicitQualitativeCheckResult(); ExplicitQualitativeCheckResult const& rightResult = rightResultPointer->asExplicitQualitativeCheckResult(); - std::vector numericResult = storm::modelchecker::helper::SparseDtmcPrctlHelper::computeBoundedUntilProbabilities(this->getModel().getTransitionMatrix(), this->getModel().getBackwardTransitions(), leftResult.getTruthValuesVector(), rightResult.getTruthValuesVector(), pathFormula.getUpperBound(), *linearEquationSolverFactory); + std::vector numericResult = storm::modelchecker::helper::SparseDtmcPrctlHelper::computeBoundedUntilProbabilities(this->getModel().getTransitionMatrix(), this->getModel().getBackwardTransitions(), leftResult.getTruthValuesVector(), rightResult.getTruthValuesVector(), pathFormula.getUpperBound() + (pathFormula.isUpperBoundStrict() ? 1ull : 0ull), *linearEquationSolverFactory); std::unique_ptr result = std::unique_ptr(new ExplicitQuantitativeCheckResult(std::move(numericResult))); return result; } diff --git a/src/storm/modelchecker/prctl/SparseMdpPrctlModelChecker.cpp b/src/storm/modelchecker/prctl/SparseMdpPrctlModelChecker.cpp index 637380920..2a8bd9f3c 100644 --- a/src/storm/modelchecker/prctl/SparseMdpPrctlModelChecker.cpp +++ b/src/storm/modelchecker/prctl/SparseMdpPrctlModelChecker.cpp @@ -64,7 +64,7 @@ namespace storm { std::unique_ptr rightResultPointer = this->check(pathFormula.getRightSubformula()); ExplicitQualitativeCheckResult const& leftResult = leftResultPointer->asExplicitQualitativeCheckResult(); ExplicitQualitativeCheckResult const& rightResult = rightResultPointer->asExplicitQualitativeCheckResult(); - std::vector numericResult = storm::modelchecker::helper::SparseMdpPrctlHelper::computeBoundedUntilProbabilities(checkTask.getOptimizationDirection(), this->getModel().getTransitionMatrix(), this->getModel().getBackwardTransitions(), leftResult.getTruthValuesVector(), rightResult.getTruthValuesVector(), pathFormula.getUpperBound(), *minMaxLinearEquationSolverFactory); + std::vector numericResult = storm::modelchecker::helper::SparseMdpPrctlHelper::computeBoundedUntilProbabilities(checkTask.getOptimizationDirection(), this->getModel().getTransitionMatrix(), this->getModel().getBackwardTransitions(), leftResult.getTruthValuesVector(), rightResult.getTruthValuesVector(), pathFormula.getUpperBound() + (pathFormula.isUpperBoundStrict() ? 1ull : 0ull), *minMaxLinearEquationSolverFactory); return std::unique_ptr(new ExplicitQuantitativeCheckResult(std::move(numericResult))); } diff --git a/src/storm/modelchecker/prctl/SymbolicDtmcPrctlModelChecker.cpp b/src/storm/modelchecker/prctl/SymbolicDtmcPrctlModelChecker.cpp index 7f32c666d..af037f5ef 100644 --- a/src/storm/modelchecker/prctl/SymbolicDtmcPrctlModelChecker.cpp +++ b/src/storm/modelchecker/prctl/SymbolicDtmcPrctlModelChecker.cpp @@ -76,7 +76,7 @@ namespace storm { std::unique_ptr rightResultPointer = this->check(pathFormula.getRightSubformula()); SymbolicQualitativeCheckResult const& leftResult = leftResultPointer->asSymbolicQualitativeCheckResult(); SymbolicQualitativeCheckResult const& rightResult = rightResultPointer->asSymbolicQualitativeCheckResult(); - storm::dd::Add numericResult = storm::modelchecker::helper::SymbolicDtmcPrctlHelper::computeBoundedUntilProbabilities(this->getModel(), this->getModel().getTransitionMatrix(), leftResult.getTruthValuesVector(), rightResult.getTruthValuesVector(), pathFormula.getUpperBound(), *this->linearEquationSolverFactory); + storm::dd::Add numericResult = storm::modelchecker::helper::SymbolicDtmcPrctlHelper::computeBoundedUntilProbabilities(this->getModel(), this->getModel().getTransitionMatrix(), leftResult.getTruthValuesVector(), rightResult.getTruthValuesVector(), pathFormula.getUpperBound() + (pathFormula.isUpperBoundStrict() ? 1ull : 0ull), *this->linearEquationSolverFactory); return std::unique_ptr>(new SymbolicQuantitativeCheckResult(this->getModel().getReachableStates(), numericResult)); } diff --git a/src/storm/modelchecker/prctl/SymbolicMdpPrctlModelChecker.cpp b/src/storm/modelchecker/prctl/SymbolicMdpPrctlModelChecker.cpp index 55b5f4539..7bb1af89a 100644 --- a/src/storm/modelchecker/prctl/SymbolicMdpPrctlModelChecker.cpp +++ b/src/storm/modelchecker/prctl/SymbolicMdpPrctlModelChecker.cpp @@ -76,7 +76,7 @@ namespace storm { std::unique_ptr rightResultPointer = this->check(pathFormula.getRightSubformula()); SymbolicQualitativeCheckResult const& leftResult = leftResultPointer->asSymbolicQualitativeCheckResult(); SymbolicQualitativeCheckResult const& rightResult = rightResultPointer->asSymbolicQualitativeCheckResult(); - return storm::modelchecker::helper::SymbolicMdpPrctlHelper::computeBoundedUntilProbabilities(checkTask.getOptimizationDirection(), this->getModel(), this->getModel().getTransitionMatrix(), leftResult.getTruthValuesVector(), rightResult.getTruthValuesVector(), pathFormula.getUpperBound(), *this->linearEquationSolverFactory); + return storm::modelchecker::helper::SymbolicMdpPrctlHelper::computeBoundedUntilProbabilities(checkTask.getOptimizationDirection(), this->getModel(), this->getModel().getTransitionMatrix(), leftResult.getTruthValuesVector(), rightResult.getTruthValuesVector(), pathFormula.getUpperBound() + (pathFormula.isUpperBoundStrict() ? 1ull : 0ull), *this->linearEquationSolverFactory); } template diff --git a/src/storm/parser/FormulaParserGrammar.cpp b/src/storm/parser/FormulaParserGrammar.cpp index d30f29f94..15f3e8a6e 100644 --- a/src/storm/parser/FormulaParserGrammar.cpp +++ b/src/storm/parser/FormulaParserGrammar.cpp @@ -224,7 +224,7 @@ namespace storm { std::shared_ptr FormulaParserGrammar::createEventuallyFormula(boost::optional, boost::optional>> const& timeBound, storm::logic::FormulaContext context, std::shared_ptr const& subformula) const { if (timeBound) { - return std::shared_ptr(new storm::logic::BoundedUntilFormula(createBooleanLiteralFormula(true), subformula, timeBound.get().first, timeBound.get().second, storm::logic::BoundedUntil::BoundedType::Time)); + return std::shared_ptr(new storm::logic::BoundedUntilFormula(createBooleanLiteralFormula(true), subformula, timeBound.get().first, timeBound.get().second, storm::logic::BoundedUntilFormula::BoundedType::Time)); } else { return std::shared_ptr(new storm::logic::EventuallyFormula(subformula, context)); } @@ -240,7 +240,7 @@ namespace storm { std::shared_ptr FormulaParserGrammar::createUntilFormula(std::shared_ptr const& leftSubformula, boost::optional, boost::optional>> const& timeBound, std::shared_ptr const& rightSubformula) { if (timeBound) { - return std::shared_ptr(new storm::logic::BoundedUntilFormula(leftSubformula, rightSubformula, timeBound.get().first, timeBound.get().second, storm::logic::BoundedUntil::BoundedType::Time)); + return std::shared_ptr(new storm::logic::BoundedUntilFormula(leftSubformula, rightSubformula, timeBound.get().first, timeBound.get().second, storm::logic::BoundedUntilFormula::BoundedType::Time)); } else { return std::shared_ptr(new storm::logic::UntilFormula(leftSubformula, rightSubformula)); } diff --git a/src/storm/parser/FormulaParserGrammar.h b/src/storm/parser/FormulaParserGrammar.h index affbd96b0..1b73df00c 100644 --- a/src/storm/parser/FormulaParserGrammar.h +++ b/src/storm/parser/FormulaParserGrammar.h @@ -149,7 +149,7 @@ namespace storm { qi::rule(storm::logic::FormulaContext), Skipper> globallyFormula; qi::rule(storm::logic::FormulaContext), Skipper> untilFormula; - qi::rule>(), qi::locals, Skipper> timeBound; + qi::rule, boost::optional>(), qi::locals, Skipper> timeBound; qi::rule(), Skipper> rewardPathFormula; qi::rule(), Skipper> cumulativeRewardFormula; diff --git a/src/storm/parser/JaniParser.cpp b/src/storm/parser/JaniParser.cpp index 06b0a83c2..6e6bb1612 100644 --- a/src/storm/parser/JaniParser.cpp +++ b/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(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(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(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(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"); diff --git a/src/storm/settings/Option.cpp b/src/storm/settings/Option.cpp index 6de9ecc46..338289fe6 100644 --- a/src/storm/settings/Option.cpp +++ b/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; } diff --git a/src/storm/settings/Option.h b/src/storm/settings/Option.h index b043a03f2..1adf8ddff 100644 --- a/src/storm/settings/Option.h +++ b/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. diff --git a/src/storm/settings/SettingsManager.cpp b/src/storm/settings/SettingsManager.cpp index 2d5698c59..7dc541a2a 100644 --- a/src/storm/settings/SettingsManager.cpp +++ b/src/storm/settings/SettingsManager.cpp @@ -504,6 +504,10 @@ namespace storm { return dynamic_cast(mutableManager().getModule(storm::settings::modules::IOSettings::moduleName)); } + storm::settings::modules::AbstractionSettings& mutableAbstractionSettings() { + return dynamic_cast(mutableManager().getModule(storm::settings::modules::AbstractionSettings::moduleName)); + } + void initializeAll(std::string const& name, std::string const& executableName) { storm::settings::mutableManager().setName(name, executableName); diff --git a/src/storm/settings/SettingsManager.h b/src/storm/settings/SettingsManager.h index 6b1afe5db..1ae89382e 100644 --- a/src/storm/settings/SettingsManager.h +++ b/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 diff --git a/src/storm/settings/modules/AbstractionSettings.cpp b/src/storm/settings/modules/AbstractionSettings.cpp index 4c7b3fd14..a4eb86fb7 100644 --- a/src/storm/settings/modules/AbstractionSettings.cpp +++ b/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"; } diff --git a/src/storm/settings/modules/AbstractionSettings.h b/src/storm/settings/modules/AbstractionSettings.h index 187eaf387..9786f2957 100644 --- a/src/storm/settings/modules/AbstractionSettings.h +++ b/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. * diff --git a/src/storm/settings/modules/ModuleSettings.cpp b/src/storm/settings/modules/ModuleSettings.cpp index 3fb7d327f..a938e42db 100644 --- a/src/storm/settings/modules/ModuleSettings.cpp +++ b/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 diff --git a/src/storm/settings/modules/ModuleSettings.h b/src/storm/settings/modules/ModuleSettings.h index 2145d5267..4bda74eb0 100644 --- a/src/storm/settings/modules/ModuleSettings.h +++ b/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: /*! diff --git a/src/storm/storage/jani/JSONExporter.cpp b/src/storm/storage/jani/JSONExporter.cpp index 491605c35..ba6a54f8a 100644 --- a/src/storm/storage/jani/JSONExporter.cpp +++ b/src/storm/storage/jani/JSONExporter.cpp @@ -169,10 +169,10 @@ namespace storm { opDecl["op"] = "U"; opDecl["left"] = boost::any_cast(f.getLeftSubformula().accept(*this, data)); opDecl["right"] = boost::any_cast(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()); } else { - opDecl["time-bounds"] = constructPropertyInterval(f.getIntervalBounds().first, f.getIntervalBounds().second); + opDecl["time-bounds"] = constructPropertyInterval(f.getLowerBound(), f.getUpperBound()); } return opDecl; } diff --git a/src/test/abstraction/PrismMenuGameTest.cpp b/src/test/abstraction/PrismMenuGameTest.cpp index 9fc283cdb..e95760b93 100644 --- a/src/test/abstraction/PrismMenuGameTest.cpp +++ b/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 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 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 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 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 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 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()); @@ -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()); @@ -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()); @@ -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()); @@ -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()); @@ -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()); @@ -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()); @@ -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()); @@ -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()); @@ -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()); @@ -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()); @@ -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()); @@ -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 diff --git a/src/test/logic/FragmentCheckerTest.cpp b/src/test/logic/FragmentCheckerTest.cpp index 3767660e8..643742bbf 100644 --- a/src/test/logic/FragmentCheckerTest.cpp +++ b/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)); diff --git a/src/test/modelchecker/GmmxxCtmcCslModelCheckerTest.cpp b/src/test/modelchecker/GmmxxCtmcCslModelCheckerTest.cpp index b4af59d2d..56a1a498f 100644 --- a/src/test/modelchecker/GmmxxCtmcCslModelCheckerTest.cpp +++ b/src/test/modelchecker/GmmxxCtmcCslModelCheckerTest.cpp @@ -68,14 +68,14 @@ TEST(GmmxxCtmcCslModelCheckerTest, Cluster) { storm::modelchecker::ExplicitQuantitativeCheckResult quantitativeCheckResult4 = checkResult->asExplicitQuantitativeCheckResult(); EXPECT_NEAR(1, quantitativeCheckResult4[initialState], storm::settings::getModule().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 quantitativeCheckResult5 = checkResult->asExplicitQuantitativeCheckResult(); EXPECT_NEAR(0, quantitativeCheckResult5[initialState], storm::settings::getModule().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()); diff --git a/src/test/modelchecker/GmmxxHybridCtmcCslModelCheckerTest.cpp b/src/test/modelchecker/GmmxxHybridCtmcCslModelCheckerTest.cpp index 93e3a4b65..e6a167fc9 100644 --- a/src/test/modelchecker/GmmxxHybridCtmcCslModelCheckerTest.cpp +++ b/src/test/modelchecker/GmmxxHybridCtmcCslModelCheckerTest.cpp @@ -85,7 +85,7 @@ TEST(GmmxxHybridCtmcCslModelCheckerTest, Cluster_Cudd) { EXPECT_NEAR(1, quantitativeCheckResult4.getMin(), storm::settings::getModule().getPrecision()); EXPECT_NEAR(1, quantitativeCheckResult4.getMax(), storm::settings::getModule().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().getPrecision()); EXPECT_NEAR(0, quantitativeCheckResult5.getMax(), storm::settings::getModule().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().getPrecision()); EXPECT_NEAR(1, quantitativeCheckResult4.getMax(), storm::settings::getModule().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().getPrecision()); EXPECT_NEAR(0, quantitativeCheckResult5.getMax(), storm::settings::getModule().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()); diff --git a/src/test/modelchecker/NativeCtmcCslModelCheckerTest.cpp b/src/test/modelchecker/NativeCtmcCslModelCheckerTest.cpp index a9ace55cc..ed79b2db8 100644 --- a/src/test/modelchecker/NativeCtmcCslModelCheckerTest.cpp +++ b/src/test/modelchecker/NativeCtmcCslModelCheckerTest.cpp @@ -63,14 +63,14 @@ TEST(NativeCtmcCslModelCheckerTest, Cluster) { storm::modelchecker::ExplicitQuantitativeCheckResult quantitativeCheckResult4 = checkResult->asExplicitQuantitativeCheckResult(); EXPECT_NEAR(1, quantitativeCheckResult4[initialState], storm::settings::getModule().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 quantitativeCheckResult5 = checkResult->asExplicitQuantitativeCheckResult(); EXPECT_NEAR(0, quantitativeCheckResult5[initialState], storm::settings::getModule().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()); diff --git a/src/test/modelchecker/NativeHybridCtmcCslModelCheckerTest.cpp b/src/test/modelchecker/NativeHybridCtmcCslModelCheckerTest.cpp index d9f83d23a..6daa4a818 100644 --- a/src/test/modelchecker/NativeHybridCtmcCslModelCheckerTest.cpp +++ b/src/test/modelchecker/NativeHybridCtmcCslModelCheckerTest.cpp @@ -83,7 +83,7 @@ TEST(NativeHybridCtmcCslModelCheckerTest, Cluster_Cudd) { EXPECT_NEAR(1, quantitativeCheckResult4.getMin(), storm::settings::getModule().getPrecision()); EXPECT_NEAR(1, quantitativeCheckResult4.getMax(), storm::settings::getModule().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().getPrecision()); EXPECT_NEAR(0, quantitativeCheckResult5.getMax(), storm::settings::getModule().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().getPrecision()); EXPECT_NEAR(1, quantitativeCheckResult4.getMax(), storm::settings::getModule().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().getPrecision()); EXPECT_NEAR(0, quantitativeCheckResult5.getMax(), storm::settings::getModule().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()); diff --git a/src/test/storage/DeterministicModelBisimulationDecompositionTest.cpp b/src/test/storage/DeterministicModelBisimulationDecompositionTest.cpp index 8c8954e62..3ebeca7a5 100644 --- a/src/test/storage/DeterministicModelBisimulationDecompositionTest.cpp +++ b/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("one"); - auto eventuallyFormula = std::make_shared(labelFormula); - -#ifdef WINDOWS - storm::storage::DeterministicModelBisimulationDecomposition>::Options options2(*dtmc, *eventuallyFormula); -#else - typename storm::storage::DeterministicModelBisimulationDecomposition>::Options options2(*dtmc, *eventuallyFormula); -#endif + storm::parser::FormulaParser formulaParser; + std::shared_ptr formula = formulaParser.parseSingleFormulaFromString("P=? [F \"one\"]"); + + typename storm::storage::DeterministicModelBisimulationDecomposition>::Options options2(*dtmc, *formula); storm::storage::DeterministicModelBisimulationDecomposition> 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("observe0Greater1"); - auto eventuallyFormula = std::make_shared(labelFormula); - -#ifdef WINDOWS - storm::storage::DeterministicModelBisimulationDecomposition>::Options options2(*dtmc, *eventuallyFormula); -#else - typename storm::storage::DeterministicModelBisimulationDecomposition>::Options options2(*dtmc, *eventuallyFormula); -#endif - storm::storage::DeterministicModelBisimulationDecomposition> 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 formula = formulaParser.parseSingleFormulaFromString("P=? [F \"observe0Greater1\"]"); - auto probabilityOperatorFormula = std::make_shared(eventuallyFormula); + typename storm::storage::DeterministicModelBisimulationDecomposition>::Options options3(*dtmc, *formula); -#ifdef WINDOWS - storm::storage::DeterministicModelBisimulationDecomposition>::Options options3(*dtmc, *probabilityOperatorFormula); -#else - typename storm::storage::DeterministicModelBisimulationDecomposition>::Options options3(*dtmc, *probabilityOperatorFormula); -#endif storm::storage::DeterministicModelBisimulationDecomposition> 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(std::make_shared(true), labelFormula, 50); + formula = formulaParser.parseSingleFormulaFromString("P=? [true U<=50 \"observe0Greater1\"] "); + + typename storm::storage::DeterministicModelBisimulationDecomposition>::Options options4(*dtmc, *formula); -#ifdef WINDOWS - storm::storage::DeterministicModelBisimulationDecomposition>::Options options4(*dtmc, *boundedUntilFormula); -#else - typename storm::storage::DeterministicModelBisimulationDecomposition>::Options options4(*dtmc, *boundedUntilFormula); -#endif storm::storage::DeterministicModelBisimulationDecomposition> bisim6(*dtmc, options4); ASSERT_NO_THROW(bisim6.computeBisimulationDecomposition()); ASSERT_NO_THROW(result = bisim6.getQuotient()); diff --git a/src/test/utility/GraphTest.cpp b/src/test/utility/GraphTest.cpp index 7e7e170c0..051612984 100644 --- a/src/test/utility/GraphTest.cpp +++ b/src/test/utility/GraphTest.cpp @@ -226,15 +226,15 @@ TEST(GraphTest, SymbolicProb01StochasticGameDieSmall) { storm::abstraction::MenuGame game = abstractor.abstract(); // The target states are those states where !(s < 3). - storm::dd::Bdd targetStates = game.getStates(initialPredicates[0], true); + storm::dd::Bdd targetStates = !abstractor.getStates(initialPredicates[0]) && game.getReachableStates(); storm::utility::graph::GameProb01Result 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() * result.player2Strategy.get().template toAdd()).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 game = abstractor.abstract(); - // The target states are those states where s1 == 7 & s2 == 7 & d1 + d2 == 1. - storm::dd::Bdd 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 targetStates = abstractor.getStates(initialPredicates[7]) && abstractor.getStates(initialPredicates[22]) && abstractor.getStates(initialPredicates[9]) && abstractor.getStates(initialPredicates[24]) && game.getReachableStates(); storm::utility::graph::GameProb01Result 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 game = abstractor.abstract(); // The target states are those states where col == 2. - storm::dd::Bdd targetStates = game.getStates(initialPredicates[2], false); + storm::dd::Bdd targetStates = abstractor.getStates(initialPredicates[2]) && game.getReachableStates(); storm::utility::graph::GameProb01Result 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());