diff --git a/src/storm-cli-utilities/model-handling.h b/src/storm-cli-utilities/model-handling.h index aaca1ec04..67a3dbbe9 100644 --- a/src/storm-cli-utilities/model-handling.h +++ b/src/storm-cli-utilities/model-handling.h @@ -131,6 +131,19 @@ namespace storm { } } + // Make sure there are no undefined constants remaining in any property. + for (auto const& property : output.properties) { + std::set usedUndefinedConstants = property.getUndefinedConstants(); + if (!usedUndefinedConstants.empty()) { + std::vector undefinedConstantsNames; + for (auto const& constant : usedUndefinedConstants) { + undefinedConstantsNames.emplace_back(constant.getName()); + } + + STORM_LOG_THROW(false, storm::exceptions::InvalidArgumentException, "The property '" << property << " still refers to the undefined constants " << boost::algorithm::join(undefinedConstantsNames, ",") << "."); + } + } + // Check whether conversion for PRISM to JANI is requested or necessary. if (input.model && input.model.get().isPrismProgram()) { bool transformToJani = ioSettings.isPrismToJaniSet(); @@ -567,6 +580,10 @@ namespace storm { expressionParser.setIdentifierMapping(variableMapping); for (auto const& constraintString : constraintsAsStrings) { + if (constraintString.empty()) { + continue; + } + storm::expressions::Expression constraint = expressionParser.parseFromString(constraintString); STORM_LOG_TRACE("Adding special (user-provided) constraint " << constraint << "."); constraints.emplace_back(constraint); @@ -588,25 +605,34 @@ namespace storm { std::vector predicateGroupsAsStrings; boost::split(predicateGroupsAsStrings, refinementPredicatesString, boost::is_any_of(";")); - for (auto const& predicateGroupString : predicateGroupsAsStrings) { - std::vector predicatesAsStrings; - boost::split(predicatesAsStrings, predicateGroupString, boost::is_any_of(":")); - - injectedRefinementPredicates.emplace_back(); - for (auto const& predicateString : predicatesAsStrings) { - storm::expressions::Expression predicate = expressionParser.parseFromString(predicateString); - STORM_LOG_TRACE("Adding special (user-provided) refinement predicate " << predicateString << "."); - injectedRefinementPredicates.back().emplace_back(predicate); + if (!predicateGroupsAsStrings.empty()) { + for (auto const& predicateGroupString : predicateGroupsAsStrings) { + if (predicateGroupString.empty()) { + continue; + } + + std::vector predicatesAsStrings; + boost::split(predicatesAsStrings, predicateGroupString, boost::is_any_of(":")); + + if (!predicatesAsStrings.empty()) { + injectedRefinementPredicates.emplace_back(); + for (auto const& predicateString : predicatesAsStrings) { + storm::expressions::Expression predicate = expressionParser.parseFromString(predicateString); + STORM_LOG_TRACE("Adding special (user-provided) refinement predicate " << predicateString << "."); + injectedRefinementPredicates.back().emplace_back(predicate); + } + + STORM_LOG_THROW(!injectedRefinementPredicates.back().empty(), storm::exceptions::InvalidArgumentException, "Expecting non-empty list of predicates to inject for each (mentioned) refinement step."); + + // Finally reverse the list, because we take the predicates from the back. + std::reverse(injectedRefinementPredicates.back().begin(), injectedRefinementPredicates.back().end()); + } } - STORM_LOG_THROW(!injectedRefinementPredicates.back().empty(), storm::exceptions::InvalidArgumentException, "Expecting non-empty list of predicates to inject for each (mentioned) refinement step."); // Finally reverse the list, because we take the predicates from the back. - std::reverse(injectedRefinementPredicates.back().begin(), injectedRefinementPredicates.back().end()); + std::reverse(injectedRefinementPredicates.begin(), injectedRefinementPredicates.end()); } - // Finally reverse the list, because we take the predicates from the back. - std::reverse(injectedRefinementPredicates.begin(), injectedRefinementPredicates.end()); - return injectedRefinementPredicates; } diff --git a/src/storm-dft/api/storm-dft.cpp b/src/storm-dft/api/storm-dft.cpp index c2431d8e9..b8794372c 100644 --- a/src/storm-dft/api/storm-dft.cpp +++ b/src/storm-dft/api/storm-dft.cpp @@ -57,7 +57,7 @@ namespace storm { auto evFormula = std::make_shared(evtlFormula, storm::logic::FormulaContext::Time); auto rewFormula = std::make_shared(evFormula, storm::logic::OperatorInformation(), storm::logic::RewardMeasureType::Expectation); - std::vector res({storm::jani::Property("time-bounded", tbUntil), storm::jani::Property("mttf", rewFormula)}); + std::vector res({storm::jani::Property("time-bounded", tbUntil, {}), storm::jani::Property("mttf", rewFormula, {})}); return res; } ); diff --git a/src/storm-gspn/builder/JaniGSPNBuilder.cpp b/src/storm-gspn/builder/JaniGSPNBuilder.cpp index 744b76eb4..0e723cdbd 100644 --- a/src/storm-gspn/builder/JaniGSPNBuilder.cpp +++ b/src/storm-gspn/builder/JaniGSPNBuilder.cpp @@ -275,11 +275,12 @@ namespace storm { auto const& deadlockVar = addDeadlockTransientVariable(model, getUniqueVarName(*expressionManager, "deadl")); auto deadlock = std::make_shared(deadlockVar.getExpressionVariable().getExpression()); auto trueFormula = std::make_shared(true); + std::set emptyVariableSet; auto maxReachDeadlock = std::make_shared( std::make_shared(deadlock, storm::logic::FormulaContext::Probability), storm::logic::OperatorInformation(storm::solver::OptimizationDirection::Maximize)); - standardProperties.emplace_back("MaxPrReachDeadlock", maxReachDeadlock, "The maximal probability to eventually reach a deadlock."); + standardProperties.emplace_back("MaxPrReachDeadlock", maxReachDeadlock, emptyVariableSet, "The maximal probability to eventually reach a deadlock."); auto exprTB = expressionManager->declareRationalVariable(getUniqueVarName(*expressionManager, "TIME_BOUND")); auto janiTB = storm::jani::Constant(exprTB.getName(), exprTB); @@ -289,15 +290,15 @@ namespace storm { auto maxReachDeadlockTimeBounded = std::make_shared( std::make_shared(trueFormula, deadlock, boost::none, tb, tbr), storm::logic::OperatorInformation(storm::solver::OptimizationDirection::Maximize)); - standardProperties.emplace_back("MaxPrReachDeadlockTB", maxReachDeadlockTimeBounded, "The maximal probability to reach a deadlock within 'TIME_BOUND' steps."); + standardProperties.emplace_back("MaxPrReachDeadlockTB", maxReachDeadlockTimeBounded, emptyVariableSet, "The maximal probability to reach a deadlock within 'TIME_BOUND' steps."); auto expTimeDeadlock = std::make_shared( std::make_shared(deadlock, storm::logic::FormulaContext::Time), storm::logic::OperatorInformation(storm::solver::OptimizationDirection::Maximize)); - standardProperties.emplace_back("MinExpTimeDeadlock", expTimeDeadlock, "The minimal expected time to reach a deadlock."); + standardProperties.emplace_back("MinExpTimeDeadlock", expTimeDeadlock, emptyVariableSet, "The minimal expected time to reach a deadlock."); } } -} \ No newline at end of file +} diff --git a/src/storm-parsers/parser/FormulaParserGrammar.cpp b/src/storm-parsers/parser/FormulaParserGrammar.cpp index 31e436c2d..ceca76e8e 100644 --- a/src/storm-parsers/parser/FormulaParserGrammar.cpp +++ b/src/storm-parsers/parser/FormulaParserGrammar.cpp @@ -224,6 +224,7 @@ namespace storm { if (expression) { addIdentifierExpression(name, expression.get()); } else { + undefinedConstants.insert(newVariable); addIdentifierExpression(name, newVariable); } } @@ -417,24 +418,31 @@ namespace storm { return std::shared_ptr(new storm::logic::MultiObjectiveFormula(subformulas)); } } - + + std::set FormulaParserGrammar::getUndefinedConstants(std::shared_ptr const& formula) const { + std::set result; + std::set usedVariables = formula->getUsedVariables(); + std::set_intersection(usedVariables.begin(), usedVariables.end(), undefinedConstants.begin(), undefinedConstants.end(), std::inserter(result, result.begin())); + return result; + } + storm::jani::Property FormulaParserGrammar::createProperty(boost::optional const& propertyName, storm::modelchecker::FilterType const& filterType, std::shared_ptr const& formula, std::shared_ptr const& states) { storm::jani::FilterExpression filterExpression(formula, filterType, states); ++propertyCount; if (propertyName) { - return storm::jani::Property(propertyName.get(), filterExpression); + return storm::jani::Property(propertyName.get(), filterExpression, this->getUndefinedConstants(formula)); } else { - return storm::jani::Property(std::to_string(propertyCount -1 ), filterExpression); + return storm::jani::Property(std::to_string(propertyCount - 1), filterExpression, this->getUndefinedConstants(formula)); } } storm::jani::Property FormulaParserGrammar::createPropertyWithDefaultFilterTypeAndStates(boost::optional const& propertyName, std::shared_ptr const& formula) { ++propertyCount; if (propertyName) { - return storm::jani::Property(propertyName.get(), formula); + return storm::jani::Property(propertyName.get(), formula, this->getUndefinedConstants(formula)); } else { - return storm::jani::Property(std::to_string(propertyCount), formula); + return storm::jani::Property(std::to_string(propertyCount), formula, this->getUndefinedConstants(formula)); } } diff --git a/src/storm-parsers/parser/FormulaParserGrammar.h b/src/storm-parsers/parser/FormulaParserGrammar.h index c9f7e8327..75012aaf4 100644 --- a/src/storm-parsers/parser/FormulaParserGrammar.h +++ b/src/storm-parsers/parser/FormulaParserGrammar.h @@ -230,6 +230,7 @@ namespace storm { std::shared_ptr createUnaryBooleanStateFormula(std::shared_ptr const& subformula, boost::optional const& operatorType); std::shared_ptr createMultiFormula(std::vector> const& subformulas); + std::set getUndefinedConstants(std::shared_ptr const& formula) const; storm::jani::Property createProperty(boost::optional const& propertyName, storm::modelchecker::FilterType const& filterType, std::shared_ptr const& formula, std::shared_ptr const& states); storm::jani::Property createPropertyWithDefaultFilterTypeAndStates(boost::optional const& propertyName, std::shared_ptr const& formula); @@ -237,6 +238,8 @@ namespace storm { phoenix::function handler; uint64_t propertyCount; + + std::set undefinedConstants; }; } diff --git a/src/storm-parsers/parser/JaniParser.cpp b/src/storm-parsers/parser/JaniParser.cpp index 881bc5785..1909a47ef 100644 --- a/src/storm-parsers/parser/JaniParser.cpp +++ b/src/storm-parsers/parser/JaniParser.cpp @@ -560,7 +560,7 @@ namespace storm { STORM_LOG_THROW(statesFormula, storm::exceptions::NotImplementedException, "Could not derive states formula."); STORM_LOG_THROW(expressionStructure.count("values") == 1, storm::exceptions::InvalidJaniException, "Values as input for a filter must be given"); auto formula = parseFormula(expressionStructure.at("values"), storm::logic::FormulaContext::Undefined, globalVars, constants, "Values of property " + name); - return storm::jani::Property(name, storm::jani::FilterExpression(formula, ft, statesFormula), comment); + return storm::jani::Property(name, storm::jani::FilterExpression(formula, ft, statesFormula), {}, comment); } std::shared_ptr JaniParser::parseConstant(json const& constantStructure, std::unordered_map> const& constants, std::string const& scopeDescription) { diff --git a/src/storm/logic/BoundedUntilFormula.cpp b/src/storm/logic/BoundedUntilFormula.cpp index e06327511..89be6a2ba 100644 --- a/src/storm/logic/BoundedUntilFormula.cpp +++ b/src/storm/logic/BoundedUntilFormula.cpp @@ -89,14 +89,22 @@ namespace storm { for (unsigned i = 0; i < this->getDimension(); ++i) { this->getLeftSubformula(i).gatherUsedVariables(usedVariables); this->getRightSubformula(i).gatherUsedVariables(usedVariables); - this->getLowerBound(i).gatherVariables(usedVariables); - this->getUpperBound(i).gatherVariables(usedVariables); + if (this->hasLowerBound(i)) { + this->getLowerBound(i).gatherVariables(usedVariables); + } + if (this->hasUpperBound(i)) { + this->getUpperBound(i).gatherVariables(usedVariables); + } } } else { this->getLeftSubformula().gatherUsedVariables(usedVariables); this->getRightSubformula().gatherUsedVariables(usedVariables); - this->getLowerBound().gatherVariables(usedVariables); - this->getUpperBound().gatherVariables(usedVariables); + if (this->hasLowerBound()) { + this->getLowerBound().gatherVariables(usedVariables); + } + if (this->hasUpperBound()) { + this->getUpperBound().gatherVariables(usedVariables); + } } } diff --git a/src/storm/logic/OperatorFormula.cpp b/src/storm/logic/OperatorFormula.cpp index 40ac6d307..a86e5a47a 100644 --- a/src/storm/logic/OperatorFormula.cpp +++ b/src/storm/logic/OperatorFormula.cpp @@ -86,7 +86,10 @@ namespace storm { } void OperatorFormula::gatherUsedVariables(std::set& usedVariables) const { - this->getThreshold().gatherVariables(usedVariables); + UnaryStateFormula::gatherUsedVariables(usedVariables); + if (this->hasBound()) { + this->getThreshold().gatherVariables(usedVariables); + } } std::ostream& OperatorFormula::writeToStream(std::ostream& out) const { diff --git a/src/storm/logic/RewardAccumulationEliminationVisitor.cpp b/src/storm/logic/RewardAccumulationEliminationVisitor.cpp index 710f959f1..e78948dce 100644 --- a/src/storm/logic/RewardAccumulationEliminationVisitor.cpp +++ b/src/storm/logic/RewardAccumulationEliminationVisitor.cpp @@ -25,7 +25,7 @@ namespace storm { auto formula = eliminateRewardAccumulations(*p.getFilter().getFormula()); auto states = eliminateRewardAccumulations(*p.getFilter().getStatesFormula()); storm::jani::FilterExpression fe(formula, p.getFilter().getFilterType(), states); - p = storm::jani::Property(p.getName(), storm::jani::FilterExpression(formula, p.getFilter().getFilterType(), states), p.getComment()); + p = storm::jani::Property(p.getName(), storm::jani::FilterExpression(formula, p.getFilter().getFilterType(), states), p.getUndefinedConstants(), p.getComment()); } } diff --git a/src/storm/settings/modules/AbstractionSettings.cpp b/src/storm/settings/modules/AbstractionSettings.cpp index 7300f8451..d437e81e8 100644 --- a/src/storm/settings/modules/AbstractionSettings.cpp +++ b/src/storm/settings/modules/AbstractionSettings.cpp @@ -111,11 +111,11 @@ namespace storm { .build()); this->addOption(storm::settings::OptionBuilder(moduleName, constraintsOptionName, true, "Specifies additional constraints used by the abstraction.") - .addArgument(storm::settings::ArgumentBuilder::createStringArgument("constraints", "The constraints to use.").build()) + .addArgument(storm::settings::ArgumentBuilder::createStringArgument("constraints", "The constraints to use.").setDefaultValueString("").build()) .build()); this->addOption(storm::settings::OptionBuilder(moduleName, injectRefinementPredicatesOptionName, true, "Specifies predicates used by the refinement instead of the derived predicates.") - .addArgument(storm::settings::ArgumentBuilder::createStringArgument("predicates", "The (semicolon-separated) refinement predicates to use.").build()) + .addArgument(storm::settings::ArgumentBuilder::createStringArgument("predicates", "The (semicolon-separated) refinement predicates to use.").setDefaultValueString("").build()) .build()); this->addOption(storm::settings::OptionBuilder(moduleName, fixPlayer1StrategyOptionName, true, "Sets whether to fix player 1 strategies.") diff --git a/src/storm/storage/jani/Property.cpp b/src/storm/storage/jani/Property.cpp index 73c6d0dec..fbf84edeb 100644 --- a/src/storm/storage/jani/Property.cpp +++ b/src/storm/storage/jani/Property.cpp @@ -1,20 +1,19 @@ #include "Property.h" + namespace storm { namespace jani { - - std::ostream& operator<<(std::ostream& os, FilterExpression const& fe) { - return os << "Obtain " << toString(fe.getFilterType()) << " of the '" << fe.getStatesFormula() << "'-states with values described by '" << *fe.getFormula() << "'"; + return os << "Obtain " << toString(fe.getFilterType()) << " of the '" << *fe.getStatesFormula() << "'-states with values described by '" << *fe.getFormula() << "'"; } - Property::Property(std::string const& name, std::shared_ptr const& formula, std::string const& comment) - : name(name), comment(comment), filterExpression(FilterExpression(formula)) { + Property::Property(std::string const& name, std::shared_ptr const& formula, std::set const& undefinedConstants, std::string const& comment) + : name(name), comment(comment), filterExpression(FilterExpression(formula)), undefinedConstants(undefinedConstants) { // Intentionally left empty. } - Property::Property(std::string const& name, FilterExpression const& fe, std::string const& comment) - : name(name), comment(comment), filterExpression(fe) { + Property::Property(std::string const& name, FilterExpression const& fe, std::set const& undefinedConstants, std::string const& comment) + : name(name), comment(comment), filterExpression(fe), undefinedConstants(undefinedConstants) { // Intentionally left empty. } @@ -27,11 +26,17 @@ namespace storm { } Property Property::substitute(std::map const& substitution) const { - return Property(name, filterExpression.substitute(substitution), comment); + std::set remainingUndefinedConstants; + for (auto const& constant : undefinedConstants) { + if (substitution.find(constant) == substitution.end()) { + remainingUndefinedConstants.insert(constant); + } + } + return Property(name, filterExpression.substitute(substitution), remainingUndefinedConstants, comment); } Property Property::substituteLabels(std::map const& substitution) const { - return Property(name, filterExpression.substituteLabels(substitution), comment); + return Property(name, filterExpression.substituteLabels(substitution), undefinedConstants, comment); } FilterExpression const& Property::getFilter() const { @@ -42,8 +47,16 @@ namespace storm { return this->filterExpression.getFormula(); } + std::set const& Property::getUndefinedConstants() const { + return undefinedConstants; + } + + bool Property::containsUndefinedConstants() const { + return !undefinedConstants.empty(); + } + std::ostream& operator<<(std::ostream& os, Property const& p) { - return os << "(" << p.getName() << ") : " << p.getFilter(); + return os << "(" << p.getName() << "): " << p.getFilter(); } } diff --git a/src/storm/storage/jani/Property.h b/src/storm/storage/jani/Property.h index 74aceab5c..6207ff1de 100644 --- a/src/storm/storage/jani/Property.h +++ b/src/storm/storage/jani/Property.h @@ -78,9 +78,10 @@ namespace storm { * Constructs the property * @param name the name * @param formula the formula representation + * @param undefinedConstants the undefined constants used in the property * @param comment An optional comment */ - Property(std::string const& name, std::shared_ptr const& formula, std::string const& comment = ""); + Property(std::string const& name, std::shared_ptr const& formula, std::set const& undefinedConstants, std::string const& comment = ""); /** * Constructs the property @@ -88,7 +89,7 @@ namespace storm { * @param formula the formula representation * @param comment An optional comment */ - Property(std::string const& name, FilterExpression const& fe, std::string const& comment = ""); + Property(std::string const& name, FilterExpression const& fe, std::set const& undefinedConstants, std::string const& comment = ""); /** * Get the provided name @@ -107,11 +108,15 @@ namespace storm { FilterExpression const& getFilter() const; + std::set const& getUndefinedConstants() const; + bool containsUndefinedConstants() const; + std::shared_ptr getRawFormula() const; private: std::string name; std::string comment; FilterExpression filterExpression; + std::set undefinedConstants; };