From 7a851901e260c431c47ff3d4e32954ba945a10f9 Mon Sep 17 00:00:00 2001 From: Stefan Pranger Date: Thu, 2 Sep 2021 12:53:46 +0200 Subject: [PATCH] updates after cherry pick --- .../parser/FormulaParserGrammar.cpp | 52 +++++++------------ .../parser/FormulaParserGrammar.h | 38 +++++++------- src/storm/logic/BoundedGloballyFormula.cpp | 4 +- src/storm/logic/BoundedGloballyFormula.h | 7 +-- src/storm/logic/Formula.h | 3 +- src/storm/logic/FragmentSpecification.cpp | 9 ++++ src/storm/logic/ToPrefixStringVisitor.cpp | 48 +++++++++-------- src/storm/logic/ToPrefixStringVisitor.h | 8 +-- .../csl/SparseCtmcCslModelChecker.h | 13 ++--- .../prctl/SparseDtmcPrctlModelChecker.h | 1 + .../prctl/helper/SparseMdpPrctlHelper.cpp | 2 + src/storm/storage/Scheduler.cpp | 3 +- src/storm/storage/Scheduler.h | 1 - 13 files changed, 96 insertions(+), 93 deletions(-) diff --git a/src/storm-parsers/parser/FormulaParserGrammar.cpp b/src/storm-parsers/parser/FormulaParserGrammar.cpp index 18adfc932..1d5360a90 100644 --- a/src/storm-parsers/parser/FormulaParserGrammar.cpp +++ b/src/storm-parsers/parser/FormulaParserGrammar.cpp @@ -29,7 +29,7 @@ namespace storm { rewardMeasureType_.name("reward measure"); operatorKeyword_.name("Operator keyword"); filterType_.name("filter type"); - + // Auxiliary helpers isPathFormula = qi::eps(qi::_r1 == FormulaKind::Path); noAmbiguousNonAssociativeOperator = !(qi::lit(qi::_r2)[qi::_pass = phoenix::bind(&FormulaParserGrammar::raiseAmbiguousNonAssociativeOperatorError, phoenix::ref(*this), qi::_r1, qi::_r2)]); @@ -40,7 +40,7 @@ namespace storm { label.name("label"); quotedString %= qi::as_string[qi::lexeme[qi::omit[qi::char_('"')] > qi::raw[*(!qi::char_('"') >> qi::char_)] > qi::omit[qi::lit('"')]]]; quotedString.name("quoted string"); - + // PCTL-like Operator Formulas operatorInformation = (-optimalityOperator_)[qi::_a = qi::_1] >> ((qi::lit("=") > qi::lit("?"))[qi::_val = phoenix::bind(&FormulaParserGrammar::createOperatorInformation, phoenix::ref(*this), qi::_a, boost::none, boost::none)] @@ -61,7 +61,7 @@ namespace storm { operatorFormula = (operatorKeyword_[qi::_a = qi::_1] > -rewardMeasureType(qi::_a) > -rewardModelName(qi::_a) > operatorInformation > qi::lit("[") > operatorSubFormula(qi::_a) > qi::lit("]")) [qi::_val = phoenix::bind(&FormulaParserGrammar::createOperatorFormula, phoenix::ref(*this), qi::_a, qi::_2, qi::_3, qi::_4, qi::_5)]; operatorFormula.name("operator formula"); - + // Atomic propositions labelFormula = (qi::lit("\"") >> label >> qi::lit("\""))[qi::_val = phoenix::bind(&FormulaParserGrammar::createAtomicLabelFormula, phoenix::ref(*this), qi::_1)]; @@ -72,7 +72,7 @@ namespace storm { expressionFormula.name("expression formula"); atomicPropositionFormula = (booleanLiteralFormula | labelFormula | expressionFormula); atomicPropositionFormula.name("atomic proposition"); - + // Propositional Logic operators // To correctly parse the operator precedences (! binds stronger than & binds stronger than |), we run through different "precedence levels" starting with the weakest binding operator. basicPropositionalFormula = (qi::lit("(") >> (formula(qi::_r1, qi::_r2) > qi::lit(")"))) @@ -94,7 +94,7 @@ namespace storm { > andLevelPropositionalFormula(qi::_r1, qi::_r2)[qi::_val = phoenix::bind(&FormulaParserGrammar::createBinaryBooleanStateOrPathFormula, phoenix::ref(*this), qi::_val, qi::_1, storm::logic::BinaryBooleanStateFormula::OperatorType::Or)]); orLevelPropositionalFormula.name("or precedence level propositional formula"); propositionalFormula = orLevelPropositionalFormula(qi::_r1, qi::_r2); - + // Path operators // Again need to parse precedences correctly. Propositional formulae bind stronger than temporal operators. basicPathFormula = propositionalFormula(FormulaKind::Path, qi::_r1) // Bracketed case is handled here as well @@ -139,7 +139,7 @@ namespace storm { untilLevelPathFormula.name("until precedence level path formula"); pathFormula = untilLevelPathFormula(qi::_r1); pathFormula.name("path formula"); - + // Quantitative path formulae (reward) longRunAverageRewardFormula = (qi::lit("LRA") | qi::lit("S") | qi::lit("MP"))[qi::_val = phoenix::bind(&FormulaParserGrammar::createLongRunAverageRewardFormula, phoenix::ref(*this))]; longRunAverageRewardFormula.name("long run average reward formula"); @@ -149,13 +149,13 @@ namespace storm { cumulativeRewardFormula.name("cumulative reward formula"); totalRewardFormula = (qi::lit("C"))[qi::_val = phoenix::bind(&FormulaParserGrammar::createTotalRewardFormula, phoenix::ref(*this))]; totalRewardFormula.name("total reward formula"); - + // Game Formulae playerCoalition = (-((identifier[phoenix::push_back(qi::_a, qi::_1)] | qi::uint_[phoenix::push_back(qi::_a, qi::_1)]) % ','))[qi::_val = phoenix::bind(&FormulaParserGrammar::createPlayerCoalition, phoenix::ref(*this), qi::_a)]; playerCoalition.name("player coalition"); gameFormula = (qi::lit("<<") > playerCoalition > qi::lit(">>") > operatorFormula)[qi::_val = phoenix::bind(&FormulaParserGrammar::createGameFormula, phoenix::ref(*this), qi::_1, qi::_2)]; gameFormula.name("game formula"); - + // Multi-objective, quantiles multiOperatorFormula = (qi::lit("multi") > qi::lit("(") > (operatorFormula % qi::lit(",")) @@ -165,14 +165,14 @@ namespace storm { quantileBoundVariable.name("quantile bound variable"); quantileFormula = (qi::lit("quantile") > qi::lit("(") > *(quantileBoundVariable) > operatorFormula[qi::_pass = phoenix::bind(&FormulaParserGrammar::isBooleanReturnType, phoenix::ref(*this), qi::_1, true)] > qi::lit(")"))[qi::_val = phoenix::bind(&FormulaParserGrammar::createQuantileFormula, phoenix::ref(*this), qi::_1, qi::_2)]; quantileFormula.name("Quantile formula"); - + // General formulae formula = (isPathFormula(qi::_r1) >> pathFormula(qi::_r2) | propositionalFormula(qi::_r1, qi::_r2)); formula.name("formula"); topLevelFormula = formula(FormulaKind::State, storm::logic::FormulaContext::Undefined); topLevelFormula.name("top-level formula"); - + formulaName = qi::lit("\"") >> identifier >> qi::lit("\"") >> qi::lit(":"); formulaName.name("formula name"); @@ -183,7 +183,7 @@ namespace storm { #pragma clang diagnostic push #pragma clang diagnostic ignored "-Woverloaded-shift-op-parentheses" - + filterProperty = (-formulaName >> qi::lit("filter") > qi::lit("(") > filterType_ > qi::lit(",") > topLevelFormula > qi::lit(",") > formula(FormulaKind::State, storm::logic::FormulaContext::Undefined)> qi::lit(")"))[qi::_val = phoenix::bind(&FormulaParserGrammar::createProperty, phoenix::ref(*this), qi::_1, qi::_2, qi::_3, qi::_4)] | (-formulaName >> topLevelFormula)[qi::_val = phoenix::bind(&FormulaParserGrammar::createPropertyWithDefaultFilterTypeAndStates, phoenix::ref(*this), qi::_1, qi::_2)]; filterProperty.name("filter property"); @@ -236,7 +236,7 @@ namespace storm { // debug(filterProperty) // debug(constantDefinition ) // debug(start) - + // Enable error reporting. qi::on_error(rewardModelName, handler(qi::_1, qi::_2, qi::_3, qi::_4)); qi::on_error(rewardMeasureType, handler(qi::_1, qi::_2, qi::_3, qi::_4)); @@ -388,20 +388,8 @@ namespace storm { } } - std::shared_ptr FormulaParserGrammar::createGloballyFormula(boost::optional, boost::optional, std::shared_ptr>>> const& timeBounds, std::shared_ptr const& subformula) const { - if (timeBounds && !timeBounds.get().empty()) { - std::vector> lowerBounds, upperBounds; - std::vector timeBoundReferences; - for (auto const& timeBound : timeBounds.get()) { - STORM_LOG_ASSERT(!std::get<0>(timeBound), "Cannot use lower time bounds (or intervals) in globally formulas."); - lowerBounds.push_back(std::get<0>(timeBound)); - upperBounds.push_back(std::get<1>(timeBound)); - timeBoundReferences.emplace_back(*std::get<2>(timeBound)); - } - return std::shared_ptr(new storm::logic::BoundedGloballyFormula(subformula, lowerBounds, upperBounds, timeBoundReferences)); - } else { - return std::shared_ptr(new storm::logic::GloballyFormula(subformula)); - } + std::shared_ptr FormulaParserGrammar::createGloballyFormula(std::shared_ptr const& subformula) const { + return std::shared_ptr(new storm::logic::GloballyFormula(subformula)); } std::shared_ptr FormulaParserGrammar::createNextFormula(std::shared_ptr const& subformula) const { @@ -451,7 +439,7 @@ namespace storm { return storm::logic::OperatorInformation(optimizationDirection, boost::none); } } - + std::shared_ptr FormulaParserGrammar::createOperatorFormula(storm::logic::FormulaContext const& context, boost::optional const& rewardMeasureType, boost::optional const& rewardModelName, storm::logic::OperatorInformation const& operatorInformation, std::shared_ptr const& subformula) { switch(context) { case storm::logic::FormulaContext::Probability: @@ -469,7 +457,7 @@ namespace storm { STORM_LOG_THROW(false, storm::exceptions::WrongFormatException, "Unexpected formula context."); } } - + std::shared_ptr FormulaParserGrammar::createLongRunAverageOperatorFormula(storm::logic::OperatorInformation const& operatorInformation, std::shared_ptr const& subformula) const { return std::shared_ptr(new storm::logic::LongRunAverageOperatorFormula(subformula, operatorInformation)); } @@ -570,7 +558,7 @@ namespace storm { } return std::shared_ptr(new storm::logic::BoundedUntilFormula(leftSubformulas, rightSubformulas, lowerBounds, upperBounds, timeBoundReferences)); } - + std::shared_ptr FormulaParserGrammar::createMultiOperatorFormula(std::vector> const& subformulas) { return std::shared_ptr(new storm::logic::MultiObjectiveFormula(subformulas)); } @@ -620,7 +608,7 @@ namespace storm { return storm::jani::Property(std::to_string(propertyCount), formula, this->getUndefinedConstants(formula)); } } - + storm::logic::PlayerCoalition FormulaParserGrammar::createPlayerCoalition(std::vector> const& playerIds) const { return storm::logic::PlayerCoalition(playerIds); } @@ -628,7 +616,7 @@ namespace storm { std::shared_ptr FormulaParserGrammar::createGameFormula(storm::logic::PlayerCoalition const& coalition, std::shared_ptr const& subformula) const { return std::shared_ptr(new storm::logic::GameFormula(coalition, subformula)); } - + bool FormulaParserGrammar::isBooleanReturnType(std::shared_ptr const& formula, bool raiseErrorMessage) { if (formula->hasQualitativeResult()) { return true; @@ -636,7 +624,7 @@ namespace storm { STORM_LOG_ERROR_COND(!raiseErrorMessage, "Formula " << *formula << " does not have a Boolean return type."); return false; } - + bool FormulaParserGrammar::raiseAmbiguousNonAssociativeOperatorError(std::shared_ptr const& formula, std::string const& op) { STORM_LOG_ERROR( "Ambiguous use of non-associative operator '" << op << "' in formula '" << *formula << " U ... '"); return true; diff --git a/src/storm-parsers/parser/FormulaParserGrammar.h b/src/storm-parsers/parser/FormulaParserGrammar.h index 33d9e7935..63ba71f3e 100644 --- a/src/storm-parsers/parser/FormulaParserGrammar.h +++ b/src/storm-parsers/parser/FormulaParserGrammar.h @@ -63,7 +63,7 @@ namespace storm { }; // A parser used for recognizing the standard keywords (that also apply to e.g. PRISM). These shall not coincide with expression variables keywordsStruct keywords_; - + struct nonStandardKeywordsStruct : qi::symbols { nonStandardKeywordsStruct() { add @@ -78,7 +78,7 @@ namespace storm { // A parser used for recognizing non-standard Storm-specific keywords. // For compatibility, we still try to parse expression variables whose identifier is such a keyword and just issue a warning. nonStandardKeywordsStruct nonStandardKeywords_; - + struct relationalOperatorStruct : qi::symbols { relationalOperatorStruct() { add @@ -91,7 +91,7 @@ namespace storm { // A parser used for recognizing the operators at the "relational" precedence level. relationalOperatorStruct relationalOperator_; - + struct optimalityOperatorStruct : qi::symbols { optimalityOperatorStruct() { add @@ -132,7 +132,7 @@ namespace storm { // A parser used for recognizing the filter type. filterTypeStruct filterType_; - + struct operatorKeyword : qi::symbols { operatorKeyword() { add @@ -144,7 +144,7 @@ namespace storm { } }; operatorKeyword operatorKeyword_; - + enum class FormulaKind { State, /// PCTL*-like (boolean) state formula Path, /// PCTL*-like (boolean) path formula (include state formulae) @@ -161,23 +161,23 @@ namespace storm { // A symbol table that is a mapping from identifiers that can be used in expressions to the expressions // they are to be replaced with. qi::symbols identifiers_; - - + + // Rules - + // Auxiliary helpers qi::rule, std::string), Skipper> noAmbiguousNonAssociativeOperator; qi::rule identifier; qi::rule label; qi::rule quotedString; - + // PCTL-like Operator Formulas qi::rule>, Skipper> operatorInformation; qi::rule(storm::logic::FormulaContext), Skipper> operatorSubFormula; qi::rule rewardModelName; qi::rule rewardMeasureType; qi::rule(), qi::locals, Skipper> operatorFormula; - + // Atomic propositions qi::rule(), Skipper> labelFormula; qi::rule(), Skipper> expressionFormula; @@ -190,7 +190,7 @@ namespace storm { qi::rule(FormulaKind, storm::logic::FormulaContext), Skipper> andLevelPropositionalFormula; qi::rule(FormulaKind, storm::logic::FormulaContext), Skipper> orLevelPropositionalFormula; qi::rule(FormulaKind, storm::logic::FormulaContext), Skipper> propositionalFormula; - + // Path operators qi::rule, Skipper> timeBoundReference; qi::rule, boost::optional, std::shared_ptr>(), qi::locals, Skipper> timeBound; @@ -205,13 +205,13 @@ namespace storm { qi::rule(storm::logic::FormulaContext), Skipper> basicPathFormula; qi::rule(storm::logic::FormulaContext), Skipper> untilLevelPathFormula; qi::rule(storm::logic::FormulaContext), Skipper> pathFormula; - + // Quantitative path operators (reward) qi::rule(), Skipper> longRunAverageRewardFormula; qi::rule(), Skipper> instantaneousRewardFormula; qi::rule(), Skipper> cumulativeRewardFormula; qi::rule(), Skipper> totalRewardFormula; - + // Game Formulae qi::rule>>, Skipper> playerCoalition; qi::rule(), Skipper> gameFormula; @@ -220,7 +220,7 @@ namespace storm { qi::rule(), Skipper> multiOperatorFormula; qi::rule quantileBoundVariable; qi::rule(), Skipper> quantileFormula; - + // General formulae qi::rule(FormulaKind, storm::logic::FormulaContext), Skipper> formula; qi::rule(), Skipper> topLevelFormula; @@ -228,7 +228,7 @@ namespace storm { // Properties qi::rule formulaName; qi::rule filterProperty; - + // Constant declarations enum class ConstantDataType { Bool, Integer, Rational @@ -237,7 +237,7 @@ namespace storm { // Start symbol qi::rule(), Skipper> start; - + void addHoaAPMapping(storm::logic::Formula const& hoaFormula, const std::string& ap, std::shared_ptr& expression) const; storm::logic::PlayerCoalition createPlayerCoalition(std::vector> const& playerIds) const; @@ -263,7 +263,7 @@ namespace storm { std::shared_ptr createBooleanLiteralFormula(bool literal) const; std::shared_ptr createAtomicLabelFormula(std::string const& label) const; std::shared_ptr createEventuallyFormula(boost::optional, boost::optional, std::shared_ptr>>> const& timeBounds, storm::logic::FormulaContext context, std::shared_ptr const& subformula) const; - std::shared_ptr createGloballyFormula(boost::optional, boost::optional, std::shared_ptr>>> const& timeBounds, std::shared_ptr const& subformula) const; + std::shared_ptr createGloballyFormula(std::shared_ptr const& subformula) const; std::shared_ptr createNextFormula(std::shared_ptr const& subformula) const; std::shared_ptr createUntilFormula(std::shared_ptr const& leftSubformula, boost::optional, boost::optional, std::shared_ptr>>> const& timeBounds, std::shared_ptr const& rightSubformula); std::shared_ptr createHOAPathFormula(const std::string& automataFile) const; @@ -289,10 +289,10 @@ namespace storm { 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); - + bool isBooleanReturnType(std::shared_ptr const& formula, bool raiseErrorMessage = false); bool raiseAmbiguousNonAssociativeOperatorError(std::shared_ptr const& formula, std::string const& op); - + // An error handler function. phoenix::function handler; diff --git a/src/storm/logic/BoundedGloballyFormula.cpp b/src/storm/logic/BoundedGloballyFormula.cpp index 736625d4e..92cfa80a4 100644 --- a/src/storm/logic/BoundedGloballyFormula.cpp +++ b/src/storm/logic/BoundedGloballyFormula.cpp @@ -218,7 +218,7 @@ namespace storm { STORM_LOG_THROW(!bound.containsVariables(), storm::exceptions::InvalidOperationException, "Cannot evaluate time-bound '" << bound << "' as it contains undefined constants."); } - std::ostream& BoundedGloballyFormula::writeToStream(std::ostream& out) const { + std::ostream& BoundedGloballyFormula::writeToStream(std::ostream& out, bool allowParentheses) const { out << "G" ; if (this->isMultiDimensional()) { out << "^{"; @@ -277,4 +277,4 @@ namespace storm { return out; } } -} \ No newline at end of file +} diff --git a/src/storm/logic/BoundedGloballyFormula.h b/src/storm/logic/BoundedGloballyFormula.h index 644bd950c..c4b7e8004 100644 --- a/src/storm/logic/BoundedGloballyFormula.h +++ b/src/storm/logic/BoundedGloballyFormula.h @@ -60,10 +60,7 @@ namespace storm { template ValueType getNonStrictLowerBound(unsigned i = 0) const; - - - virtual std::ostream &writeToStream(std::ostream &out) const override; - + virtual std::ostream &writeToStream(std::ostream &out, bool allowParentheses = false) const override; private: static void checkNoVariablesInBound(storm::expressions::Expression const& bound); @@ -73,4 +70,4 @@ namespace storm { std::vector> upperBound; }; } -} \ No newline at end of file +} diff --git a/src/storm/logic/Formula.h b/src/storm/logic/Formula.h index 92100326a..29eba01ff 100644 --- a/src/storm/logic/Formula.h +++ b/src/storm/logic/Formula.h @@ -74,6 +74,7 @@ namespace storm { virtual bool isGloballyFormula() const; virtual bool isEventuallyFormula() const; virtual bool isReachabilityProbabilityFormula() const; + virtual bool isHOAPathFormula() const; virtual bool isBoundedGloballyFormula() const; // Reward formulas. @@ -244,7 +245,7 @@ namespace storm { * @return */ virtual std::ostream& writeToStream(std::ostream& out, bool allowParentheses = false) const = 0; - + std::string toPrefixString() const; virtual void gatherAtomicExpressionFormulas(std::vector>& atomicExpressionFormulas) const; diff --git a/src/storm/logic/FragmentSpecification.cpp b/src/storm/logic/FragmentSpecification.cpp index 3bd34e629..9e28eec3e 100644 --- a/src/storm/logic/FragmentSpecification.cpp +++ b/src/storm/logic/FragmentSpecification.cpp @@ -433,6 +433,15 @@ namespace storm { return *this; } + bool FragmentSpecification::areBinaryBooleanStateFormulasAllowed() const { + return binaryBooleanStateFormula; + } + + FragmentSpecification& FragmentSpecification::setBinaryBooleanStateFormulasAllowed(bool newValue) { + this->binaryBooleanStateFormula = newValue; + return *this; + } + bool FragmentSpecification::areBinaryBooleanPathFormulasAllowed() const { return binaryBooleanPathFormula; } diff --git a/src/storm/logic/ToPrefixStringVisitor.cpp b/src/storm/logic/ToPrefixStringVisitor.cpp index 6fc7640e4..af6e3f31c 100644 --- a/src/storm/logic/ToPrefixStringVisitor.cpp +++ b/src/storm/logic/ToPrefixStringVisitor.cpp @@ -7,20 +7,20 @@ namespace storm { namespace logic { - + std::string ToPrefixStringVisitor::toPrefixString(Formula const& f) const { boost::any result = f.accept(*this, boost::any()); return boost::any_cast(result); } - + boost::any ToPrefixStringVisitor::visit(AtomicExpressionFormula const&, boost::any const&) const { STORM_LOG_THROW(false, storm::exceptions::InvalidOperationException, "Can not convert to prefix string"); } - + boost::any ToPrefixStringVisitor::visit(AtomicLabelFormula const& f, boost::any const&) const { return std::string("\"" + f.getLabel() + "\""); } - + boost::any ToPrefixStringVisitor::visit(BinaryBooleanStateFormula const& f, boost::any const& data) const { std::string left = boost::any_cast(f.getLeftSubformula().accept(*this, data)); std::string right = boost::any_cast(f.getRightSubformula().accept(*this, data)); @@ -34,7 +34,7 @@ namespace storm { } return boost::any(); } - + boost::any ToPrefixStringVisitor::visit(BinaryBooleanPathFormula const& f, boost::any const& data) const { std::string left = boost::any_cast(f.getLeftSubformula().accept(*this, data)); std::string right = boost::any_cast(f.getRightSubformula().accept(*this, data)); @@ -58,53 +58,57 @@ namespace storm { } return result; } - + + boost::any ToPrefixStringVisitor::visit(BoundedGloballyFormula const&, boost::any const&) const { + STORM_LOG_THROW(false, storm::exceptions::InvalidOperationException, "Can not convert to prefix string"); + } + boost::any ToPrefixStringVisitor::visit(BoundedUntilFormula const&, boost::any const&) const { STORM_LOG_THROW(false, storm::exceptions::InvalidOperationException, "Can not convert to prefix string"); } - + boost::any ToPrefixStringVisitor::visit(ConditionalFormula const&, boost::any const&) const { STORM_LOG_THROW(false, storm::exceptions::InvalidOperationException, "Can not convert to prefix string"); } - + boost::any ToPrefixStringVisitor::visit(CumulativeRewardFormula const&, boost::any const&) const { STORM_LOG_THROW(false, storm::exceptions::InvalidOperationException, "Can not convert to prefix string"); } - + boost::any ToPrefixStringVisitor::visit(EventuallyFormula const& f, boost::any const& data) const { std::string subexpression = boost::any_cast(f.getSubformula().accept(*this, data)); return std::string("F ") + subexpression; } - + boost::any ToPrefixStringVisitor::visit(TimeOperatorFormula const&, boost::any const&) const { STORM_LOG_THROW(false, storm::exceptions::InvalidOperationException, "Can not convert to prefix string"); } - + boost::any ToPrefixStringVisitor::visit(GloballyFormula const& f, boost::any const& data) const { std::string subexpression = boost::any_cast(f.getSubformula().accept(*this, data)); return std::string("G ") + subexpression; } - + boost::any ToPrefixStringVisitor::visit(GameFormula const&, boost::any const&) const { STORM_LOG_THROW(false, storm::exceptions::InvalidOperationException, "Can not convert to prefix string"); } - + boost::any ToPrefixStringVisitor::visit(InstantaneousRewardFormula const&, boost::any const&) const { STORM_LOG_THROW(false, storm::exceptions::InvalidOperationException, "Can not convert to prefix string"); } - + boost::any ToPrefixStringVisitor::visit(LongRunAverageOperatorFormula const&, boost::any const&) const { STORM_LOG_THROW(false, storm::exceptions::InvalidOperationException, "Can not convert to prefix string"); } - + boost::any ToPrefixStringVisitor::visit(LongRunAverageRewardFormula const&, boost::any const&) const { STORM_LOG_THROW(false, storm::exceptions::InvalidOperationException, "Can not convert to prefix string"); } - + boost::any ToPrefixStringVisitor::visit(MultiObjectiveFormula const&, boost::any const&) const { STORM_LOG_THROW(false, storm::exceptions::InvalidOperationException, "Can not convert to prefix string"); } - + boost::any ToPrefixStringVisitor::visit(QuantileFormula const&, boost::any const&) const { STORM_LOG_THROW(false, storm::exceptions::InvalidOperationException, "Can not convert to prefix string"); } @@ -113,19 +117,19 @@ namespace storm { std::string subexpression = boost::any_cast(f.getSubformula().accept(*this, data)); return std::string("X ") + subexpression; } - + boost::any ToPrefixStringVisitor::visit(ProbabilityOperatorFormula const&, boost::any const&) const { STORM_LOG_THROW(false, storm::exceptions::InvalidOperationException, "Can not convert to prefix string"); } - + boost::any ToPrefixStringVisitor::visit(RewardOperatorFormula const&, boost::any const&) const { STORM_LOG_THROW(false, storm::exceptions::InvalidOperationException, "Can not convert to prefix string"); } - + boost::any ToPrefixStringVisitor::visit(TotalRewardFormula const&, boost::any const&) const { STORM_LOG_THROW(false, storm::exceptions::InvalidOperationException, "Can not convert to prefix string"); } - + boost::any ToPrefixStringVisitor::visit(UnaryBooleanStateFormula const& f, boost::any const& data) const { std::string subexpression = boost::any_cast(f.getSubformula().accept(*this, data)); switch (f.getOperator()) { @@ -151,7 +155,7 @@ namespace storm { std::string right = boost::any_cast(f.getRightSubformula().accept(*this, data)); return std::string("U ") + left + " " + right; } - + boost::any ToPrefixStringVisitor::visit(HOAPathFormula const&, boost::any const&) const { STORM_LOG_THROW(false, storm::exceptions::InvalidOperationException, "Can not convert to prefix string"); } diff --git a/src/storm/logic/ToPrefixStringVisitor.h b/src/storm/logic/ToPrefixStringVisitor.h index 16b8fad4a..38a786458 100644 --- a/src/storm/logic/ToPrefixStringVisitor.h +++ b/src/storm/logic/ToPrefixStringVisitor.h @@ -6,16 +6,17 @@ namespace storm { namespace logic { - + class ToPrefixStringVisitor : public FormulaVisitor { public: std::string toPrefixString(Formula const& f) const; - + virtual boost::any visit(AtomicExpressionFormula const& f, boost::any const& data) const override; virtual boost::any visit(AtomicLabelFormula const& f, boost::any const& data) const override; virtual boost::any visit(BinaryBooleanStateFormula const& f, boost::any const& data) const override; virtual boost::any visit(BinaryBooleanPathFormula const& f, boost::any const& data) const override; virtual boost::any visit(BooleanLiteralFormula const& f, boost::any const& data) const override; + virtual boost::any visit(BoundedGloballyFormula const& f, boost::any const& data) const override; virtual boost::any visit(BoundedUntilFormula const& f, boost::any const& data) const override; virtual boost::any visit(ConditionalFormula const& f, boost::any const& data) const override; virtual boost::any visit(CumulativeRewardFormula const& f, boost::any const& data) const override; @@ -37,7 +38,6 @@ namespace storm { virtual boost::any visit(UntilFormula const& f, boost::any const& data) const override; virtual boost::any visit(HOAPathFormula const& f, boost::any const& data) const override; }; - + } } - diff --git a/src/storm/modelchecker/csl/SparseCtmcCslModelChecker.h b/src/storm/modelchecker/csl/SparseCtmcCslModelChecker.h index fa43b6f9e..48de3aa16 100644 --- a/src/storm/modelchecker/csl/SparseCtmcCslModelChecker.h +++ b/src/storm/modelchecker/csl/SparseCtmcCslModelChecker.h @@ -10,25 +10,26 @@ #include "storm/utility/NumberTraits.h" namespace storm { - + namespace modelchecker { - + template class SparseCtmcCslModelChecker : public SparsePropositionalModelChecker { public: typedef typename SparseCtmcModelType::ValueType ValueType; typedef typename SparseCtmcModelType::RewardModelType RewardModelType; - + explicit SparseCtmcCslModelChecker(SparseCtmcModelType const& model); - + // Returns false, if this task can certainly not be handled by this model checker (independent of the concrete model). static bool canHandleStatic(CheckTask const& checkTask); - + // The implemented methods of the AbstractModelChecker interface. virtual bool canHandle(CheckTask const& checkTask) const override; virtual std::unique_ptr computeBoundedUntilProbabilities(Environment const& env, CheckTask const& checkTask) override; virtual std::unique_ptr computeNextProbabilities(Environment const& env, CheckTask const& checkTask) override; virtual std::unique_ptr computeUntilProbabilities(Environment const& env, CheckTask const& checkTask) override; + virtual std::unique_ptr computeLTLProbabilities(Environment const& env, CheckTask const& checkTask) override; virtual std::unique_ptr computeLongRunAverageProbabilities(Environment const& env, CheckTask const& checkTask) override; virtual std::unique_ptr computeReachabilityTimes(Environment const& env, storm::logic::RewardMeasureType rewardMeasureType, CheckTask const& checkTask) override; @@ -50,7 +51,7 @@ namespace storm { std::unique_ptr computeSteadyStateDistribution(Environment const& env); }; - + } // namespace modelchecker } // namespace storm diff --git a/src/storm/modelchecker/prctl/SparseDtmcPrctlModelChecker.h b/src/storm/modelchecker/prctl/SparseDtmcPrctlModelChecker.h index e03ba42b8..6f49a1a6d 100644 --- a/src/storm/modelchecker/prctl/SparseDtmcPrctlModelChecker.h +++ b/src/storm/modelchecker/prctl/SparseDtmcPrctlModelChecker.h @@ -30,6 +30,7 @@ namespace storm { virtual std::unique_ptr computeNextProbabilities(Environment const& env, CheckTask const& checkTask) override; virtual std::unique_ptr computeUntilProbabilities(Environment const& env, CheckTask const& checkTask) override; virtual std::unique_ptr computeGloballyProbabilities(Environment const& env, CheckTask const& checkTask) override; + virtual std::unique_ptr computeHOAPathProbabilities(Environment const& env, CheckTask const& checkTask) override; virtual std::unique_ptr computeConditionalProbabilities(Environment const& env, CheckTask const& checkTask) override; virtual std::unique_ptr computeLongRunAverageProbabilities(Environment const& env, CheckTask const& checkTask) override; virtual std::unique_ptr computeLTLProbabilities(Environment const& env, CheckTask const& checkTask) override; diff --git a/src/storm/modelchecker/prctl/helper/SparseMdpPrctlHelper.cpp b/src/storm/modelchecker/prctl/helper/SparseMdpPrctlHelper.cpp index de837daa3..85f80667f 100644 --- a/src/storm/modelchecker/prctl/helper/SparseMdpPrctlHelper.cpp +++ b/src/storm/modelchecker/prctl/helper/SparseMdpPrctlHelper.cpp @@ -635,6 +635,8 @@ namespace storm { } } + std::vector maybeStateChoiceValues = std::vector(sizeMaybeStateChoiceValues, storm::utility::zero()); + // Check whether we need to compute exact probabilities for some states. if ((qualitative || maybeStatesNotRelevant) && !goal.isShieldingTask()) { // Set the values for all maybe-states to 0.5 to indicate that their probability values are neither 0 nor 1. diff --git a/src/storm/storage/Scheduler.cpp b/src/storm/storage/Scheduler.cpp index 55b842d37..964346afc 100644 --- a/src/storm/storage/Scheduler.cpp +++ b/src/storm/storage/Scheduler.cpp @@ -274,7 +274,8 @@ namespace storm { } stateString << "model state' = " << entryIt->getColumn() << ": -> " << "(m' = "<memoryStructure->getSuccessorMemoryState(memoryState, entryIt - model->getTransitionMatrix().begin()) <<")"; // out << "model state' = " << entryIt->getColumn() << ": (transition = " << entryIt - model->getTransitionMatrix().begin() << ") -> " << "(m' = "<memoryStructure->getSuccessorMemoryState(memoryState, entryIt - model->getTransitionMatrix().begin()) <<")"; - } + } + } stateString << std::endl; } diff --git a/src/storm/storage/Scheduler.h b/src/storm/storage/Scheduler.h index cacd5b00b..e953e21b7 100644 --- a/src/storm/storage/Scheduler.h +++ b/src/storm/storage/Scheduler.h @@ -154,7 +154,6 @@ namespace storm { std::vector reachableStates; uint_fast64_t numOfUndefinedChoices; // Only consider reachable ones std::vector dontCareStates; // Their choices are neither considered deterministic nor undefined - uint_fast64_t numOfUndefinedChoices; uint_fast64_t numOfDeterministicChoices; uint_fast64_t numOfDontCareStates; };