From 3de51e28e5ac20f01396a5ec35735d9a3dbfb158 Mon Sep 17 00:00:00 2001 From: Sebastian Junges Date: Mon, 3 Jul 2017 22:53:47 +0200 Subject: [PATCH] towards reward-bounded properties --- src/storm-dft-cli/storm-dyftee.cpp | 2 +- ...SparseDtmcParameterLiftingModelChecker.cpp | 2 +- .../SparseMdpParameterLiftingModelChecker.cpp | 2 +- .../SparseParametricDtmcSimplifier.cpp | 2 +- .../SparseParametricMdpSimplifier.cpp | 2 +- .../SparseParametricModelSimplifier.cpp | 6 ++-- src/storm/logic/BoundedUntilFormula.cpp | 14 +++----- src/storm/logic/BoundedUntilFormula.h | 9 +++-- src/storm/logic/FragmentChecker.cpp | 8 +++-- src/storm/logic/FragmentSpecification.cpp | 12 ++++++- src/storm/logic/FragmentSpecification.h | 4 +++ src/storm/logic/TimeBoundType.h | 35 +++++++++++++++++-- .../logic/VariableSubstitutionVisitor.cpp | 2 +- .../csl/HybridCtmcCslModelChecker.cpp | 2 +- .../csl/SparseCtmcCslModelChecker.cpp | 2 +- .../SparseMarkovAutomatonCslModelChecker.cpp | 2 +- .../SparseMultiObjectivePreprocessor.cpp | 2 +- src/storm/parser/FormulaParserGrammar.cpp | 4 +-- src/storm/parser/JaniParser.cpp | 22 ++++++++++-- src/storm/storage/jani/JSONExporter.cpp | 9 +++-- 20 files changed, 102 insertions(+), 41 deletions(-) diff --git a/src/storm-dft-cli/storm-dyftee.cpp b/src/storm-dft-cli/storm-dyftee.cpp index 5bb379962..b2dc40006 100644 --- a/src/storm-dft-cli/storm-dyftee.cpp +++ b/src/storm-dft-cli/storm-dyftee.cpp @@ -185,7 +185,7 @@ int main(const int argc, const char** argv) { storm::expressions::Expression targetExpression = exprManager->integer(1) == topfailedVar.getExpressionVariable().getExpression(); auto evtlFormula = std::make_shared(targetExpression); - auto tbFormula = std::make_shared(std::make_shared(true), evtlFormula, storm::logic::TimeBound(false, exprManager->integer(0)), storm::logic::TimeBound(false, exprManager->integer(10)), storm::logic::TimeBoundType::Time); + auto tbFormula = std::make_shared(std::make_shared(true), evtlFormula, storm::logic::TimeBound(false, exprManager->integer(0)), storm::logic::TimeBound(false, exprManager->integer(10)), storm::logic::TimeBoundReference(storm::logic::TimeBoundType::Time)); auto tbUntil = std::make_shared(tbFormula); auto evFormula = std::make_shared(evtlFormula, storm::logic::FormulaContext::Time); diff --git a/src/storm-pars/modelchecker/region/SparseDtmcParameterLiftingModelChecker.cpp b/src/storm-pars/modelchecker/region/SparseDtmcParameterLiftingModelChecker.cpp index 5f32c8386..155b13dec 100644 --- a/src/storm-pars/modelchecker/region/SparseDtmcParameterLiftingModelChecker.cpp +++ b/src/storm-pars/modelchecker/region/SparseDtmcParameterLiftingModelChecker.cpp @@ -75,7 +75,7 @@ namespace storm { // get the step bound STORM_LOG_THROW(!checkTask.getFormula().hasLowerBound(), storm::exceptions::NotSupportedException, "Lower step bounds are not supported."); STORM_LOG_THROW(checkTask.getFormula().hasUpperBound(), storm::exceptions::NotSupportedException, "Expected a bounded until formula with an upper bound."); - STORM_LOG_THROW(checkTask.getFormula().isStepBounded(), storm::exceptions::NotSupportedException, "Expected a bounded until formula with step bounds."); + STORM_LOG_THROW(checkTask.getFormula().getTimeBoundReference().isStepBound(), storm::exceptions::NotSupportedException, "Expected a bounded until formula with step bounds."); stepBound = checkTask.getFormula().getUpperBound().evaluateAsInt(); STORM_LOG_THROW(*stepBound > 0, storm::exceptions::NotSupportedException, "Can not apply parameter lifting on step bounded formula: The step bound has to be positive."); if (checkTask.getFormula().isUpperBoundStrict()) { diff --git a/src/storm-pars/modelchecker/region/SparseMdpParameterLiftingModelChecker.cpp b/src/storm-pars/modelchecker/region/SparseMdpParameterLiftingModelChecker.cpp index 6169d22bf..65e16d628 100644 --- a/src/storm-pars/modelchecker/region/SparseMdpParameterLiftingModelChecker.cpp +++ b/src/storm-pars/modelchecker/region/SparseMdpParameterLiftingModelChecker.cpp @@ -76,7 +76,7 @@ namespace storm { // get the step bound STORM_LOG_THROW(!checkTask.getFormula().hasLowerBound(), storm::exceptions::NotSupportedException, "Lower step bounds are not supported."); STORM_LOG_THROW(checkTask.getFormula().hasUpperBound(), storm::exceptions::NotSupportedException, "Expected a bounded until formula with an upper bound."); - STORM_LOG_THROW(checkTask.getFormula().isStepBounded(), storm::exceptions::NotSupportedException, "Expected a bounded until formula with step bounds."); + STORM_LOG_THROW(checkTask.getFormula().getTimeBoundReference().isStepBound(), storm::exceptions::NotSupportedException, "Expected a bounded until formula with step bounds."); stepBound = checkTask.getFormula().getUpperBound().evaluateAsInt(); STORM_LOG_THROW(*stepBound > 0, storm::exceptions::NotSupportedException, "Can not apply parameter lifting on step bounded formula: The step bound has to be positive."); if (checkTask.getFormula().isUpperBoundStrict()) { diff --git a/src/storm-pars/transformer/SparseParametricDtmcSimplifier.cpp b/src/storm-pars/transformer/SparseParametricDtmcSimplifier.cpp index ed05131e4..826e141ff 100644 --- a/src/storm-pars/transformer/SparseParametricDtmcSimplifier.cpp +++ b/src/storm-pars/transformer/SparseParametricDtmcSimplifier.cpp @@ -111,7 +111,7 @@ namespace storm { // obtain the simplified formula for the simplified model auto labelFormula = std::make_shared (targetLabel); - auto boundedUntilFormula = std::make_shared(storm::logic::Formula::getTrueFormula(), labelFormula, boost::none, storm::logic::TimeBound(formula.getSubformula().asBoundedUntilFormula().isUpperBoundStrict(), formula.getSubformula().asBoundedUntilFormula().getUpperBound()), storm::logic::TimeBoundType::Steps); + auto boundedUntilFormula = std::make_shared(storm::logic::Formula::getTrueFormula(), labelFormula, boost::none, storm::logic::TimeBound(formula.getSubformula().asBoundedUntilFormula().isUpperBoundStrict(), formula.getSubformula().asBoundedUntilFormula().getUpperBound()), storm::logic::TimeBoundReference(storm::logic::TimeBoundType::Steps)); this->simplifiedFormula = std::make_shared(boundedUntilFormula, formula.getOperatorInformation()); return true; diff --git a/src/storm-pars/transformer/SparseParametricMdpSimplifier.cpp b/src/storm-pars/transformer/SparseParametricMdpSimplifier.cpp index 1862936f4..97f93cf03 100644 --- a/src/storm-pars/transformer/SparseParametricMdpSimplifier.cpp +++ b/src/storm-pars/transformer/SparseParametricMdpSimplifier.cpp @@ -135,7 +135,7 @@ namespace storm { // obtain the simplified formula for the simplified model auto labelFormula = std::make_shared (targetLabel); - auto boundedUntilFormula = std::make_shared(storm::logic::Formula::getTrueFormula(), labelFormula, boost::none, storm::logic::TimeBound(formula.getSubformula().asBoundedUntilFormula().isUpperBoundStrict(), formula.getSubformula().asBoundedUntilFormula().getUpperBound()), storm::logic::TimeBoundType::Steps); + auto boundedUntilFormula = std::make_shared(storm::logic::Formula::getTrueFormula(), labelFormula, boost::none, storm::logic::TimeBound(formula.getSubformula().asBoundedUntilFormula().isUpperBoundStrict(), formula.getSubformula().asBoundedUntilFormula().getUpperBound()), storm::logic::TimeBoundReference(storm::logic::TimeBoundType::Steps)); this->simplifiedFormula = std::make_shared(boundedUntilFormula, formula.getOperatorInformation()); return true; diff --git a/src/storm-pars/transformer/SparseParametricModelSimplifier.cpp b/src/storm-pars/transformer/SparseParametricModelSimplifier.cpp index 343fc06e3..1679bdcca 100644 --- a/src/storm-pars/transformer/SparseParametricModelSimplifier.cpp +++ b/src/storm-pars/transformer/SparseParametricModelSimplifier.cpp @@ -78,21 +78,21 @@ namespace storm { template bool SparseParametricModelSimplifier::simplifyForBoundedUntilProbabilities(storm::logic::ProbabilityOperatorFormula const& formula) { // If this method was not overriden by any subclass, simplification is not possible - STORM_LOG_DEBUG("Simplification not possible because the formula is not suppoerted. Formula: " << formula); + STORM_LOG_DEBUG("Simplification not possible because the formula is not supported. Formula: " << formula); return false; } template bool SparseParametricModelSimplifier::simplifyForReachabilityRewards(storm::logic::RewardOperatorFormula const& formula) { // If this method was not overriden by any subclass, simplification is not possible - STORM_LOG_DEBUG("Simplification not possible because the formula is not suppoerted. Formula: " << formula); + STORM_LOG_DEBUG("Simplification not possible because the formula is not supported. Formula: " << formula); return false; } template bool SparseParametricModelSimplifier::simplifyForCumulativeRewards(storm::logic::RewardOperatorFormula const& formula) { // If this method was not overriden by any subclass, simplification is not possible - STORM_LOG_DEBUG("Simplification not possible because the formula is not suppoerted. Formula: " << formula); + STORM_LOG_DEBUG("Simplification not possible because the formula is not supported. Formula: " << formula); return false; } diff --git a/src/storm/logic/BoundedUntilFormula.cpp b/src/storm/logic/BoundedUntilFormula.cpp index 10cd7f33e..66b5a29fa 100644 --- a/src/storm/logic/BoundedUntilFormula.cpp +++ b/src/storm/logic/BoundedUntilFormula.cpp @@ -10,7 +10,7 @@ namespace storm { namespace logic { - BoundedUntilFormula::BoundedUntilFormula(std::shared_ptr const& leftSubformula, std::shared_ptr const& rightSubformula, boost::optional const& lowerBound, boost::optional const& upperBound, TimeBoundType const& timeBoundType) : BinaryPathFormula(leftSubformula, rightSubformula), timeBoundType(timeBoundType), lowerBound(lowerBound), upperBound(upperBound) { + BoundedUntilFormula::BoundedUntilFormula(std::shared_ptr const& leftSubformula, std::shared_ptr const& rightSubformula, boost::optional const& lowerBound, boost::optional const& upperBound, TimeBoundReference const& timeBoundReference) : BinaryPathFormula(leftSubformula, rightSubformula), timeBoundReference(timeBoundReference), lowerBound(lowerBound), upperBound(upperBound) { STORM_LOG_THROW(lowerBound || upperBound, storm::exceptions::InvalidArgumentException, "Bounded until formula requires at least one bound."); } @@ -26,17 +26,11 @@ namespace storm { return visitor.visit(*this, data); } - TimeBoundType const& BoundedUntilFormula::getTimeBoundType() const { - return timeBoundType; + TimeBoundReference const& BoundedUntilFormula::getTimeBoundReference() const { + return timeBoundReference; } - bool BoundedUntilFormula::isStepBounded() const { - return timeBoundType == TimeBoundType::Steps; - } - - bool BoundedUntilFormula::isTimeBounded() const { - return timeBoundType == TimeBoundType::Time; - } + bool BoundedUntilFormula::isLowerBoundStrict() const { return lowerBound.get().isStrict(); diff --git a/src/storm/logic/BoundedUntilFormula.h b/src/storm/logic/BoundedUntilFormula.h index 5dc2a3889..754d94cdf 100644 --- a/src/storm/logic/BoundedUntilFormula.h +++ b/src/storm/logic/BoundedUntilFormula.h @@ -12,7 +12,7 @@ namespace storm { namespace logic { class BoundedUntilFormula : public BinaryPathFormula { public: - BoundedUntilFormula(std::shared_ptr const& leftSubformula, std::shared_ptr const& rightSubformula, boost::optional const& lowerBound, boost::optional const& upperBound, TimeBoundType const& timeBoundType = TimeBoundType::Time); + BoundedUntilFormula(std::shared_ptr const& leftSubformula, std::shared_ptr const& rightSubformula, boost::optional const& lowerBound, boost::optional const& upperBound, TimeBoundReference const& timeBoundReference); virtual bool isBoundedUntilFormula() const override; @@ -20,9 +20,8 @@ namespace storm { virtual boost::any accept(FormulaVisitor const& visitor, boost::any const& data) const override; - TimeBoundType const& getTimeBoundType() const; - bool isStepBounded() const; - bool isTimeBounded() const; + TimeBoundReference const& getTimeBoundReference() const; + bool isLowerBoundStrict() const; bool hasLowerBound() const; @@ -49,7 +48,7 @@ namespace storm { private: static void checkNoVariablesInBound(storm::expressions::Expression const& bound); - TimeBoundType timeBoundType; + TimeBoundReference timeBoundReference; boost::optional lowerBound; boost::optional upperBound; }; diff --git a/src/storm/logic/FragmentChecker.cpp b/src/storm/logic/FragmentChecker.cpp index c47b8ea5d..ee0967d22 100644 --- a/src/storm/logic/FragmentChecker.cpp +++ b/src/storm/logic/FragmentChecker.cpp @@ -58,10 +58,14 @@ namespace storm { result = result && !f.getLeftSubformula().isPathFormula(); result = result && !f.getRightSubformula().isPathFormula(); } - if (f.isStepBounded()) { + auto tbr = f.getTimeBoundReference(); + if (tbr.isStepBound()) { result = result && inherited.getSpecification().areStepBoundedUntilFormulasAllowed(); - } else { + } else if(tbr.isTimeBound()) { result = result && inherited.getSpecification().areTimeBoundedUntilFormulasAllowed(); + } else { + assert(tbr.isRewardBound()); + result = result && inherited.getSpecification().areRewardBoundedUntilFormulasAllowed(); } result = result && boost::any_cast(f.getLeftSubformula().accept(*this, data)); result = result && boost::any_cast(f.getRightSubformula().accept(*this, data)); diff --git a/src/storm/logic/FragmentSpecification.cpp b/src/storm/logic/FragmentSpecification.cpp index 0d4771552..19c4116aa 100644 --- a/src/storm/logic/FragmentSpecification.cpp +++ b/src/storm/logic/FragmentSpecification.cpp @@ -141,6 +141,7 @@ namespace storm { onlyEventuallyFormuluasInConditionalFormulas = true; stepBoundedUntilFormulas = false; timeBoundedUntilFormulas = false; + rewardBoundedUntilFormulas = false; varianceAsMeasureType = false; qualitativeOperatorResults = true; @@ -423,7 +424,16 @@ namespace storm { this->timeBoundedUntilFormulas = newValue; return *this; } - + + bool FragmentSpecification::areRewardBoundedUntilFormulasAllowed() const { + return this->rewardBoundedUntilFormulas; + } + + FragmentSpecification& FragmentSpecification::setRewardBoundedUntilFormulasAllowed(bool newValue) { + this->rewardBoundedUntilFormulas = newValue; + return *this; + } + FragmentSpecification& FragmentSpecification::setOperatorsAllowed(bool newValue) { this->setProbabilityOperatorsAllowed(newValue); this->setRewardOperatorsAllowed(newValue); diff --git a/src/storm/logic/FragmentSpecification.h b/src/storm/logic/FragmentSpecification.h index 587d49bf3..619394189 100644 --- a/src/storm/logic/FragmentSpecification.h +++ b/src/storm/logic/FragmentSpecification.h @@ -102,6 +102,9 @@ namespace storm { bool areTimeBoundedUntilFormulasAllowed() const; FragmentSpecification& setTimeBoundedUntilFormulasAllowed(bool newValue); + + bool areRewardBoundedUntilFormulasAllowed() const; + FragmentSpecification& setRewardBoundedUntilFormulasAllowed(bool newValue); bool isVarianceMeasureTypeAllowed() const; FragmentSpecification& setVarianceMeasureTypeAllowed(bool newValue); @@ -162,6 +165,7 @@ namespace storm { bool onlyEventuallyFormuluasInConditionalFormulas; bool stepBoundedUntilFormulas; bool timeBoundedUntilFormulas; + bool rewardBoundedUntilFormulas; bool varianceAsMeasureType; bool quantitativeOperatorResults; bool qualitativeOperatorResults; diff --git a/src/storm/logic/TimeBoundType.h b/src/storm/logic/TimeBoundType.h index aef71b040..2488baaaf 100644 --- a/src/storm/logic/TimeBoundType.h +++ b/src/storm/logic/TimeBoundType.h @@ -2,11 +2,42 @@ namespace storm { namespace logic { - + enum class TimeBoundType { Steps, - Time + Time, + Reward }; + + class TimeBoundReference { + TimeBoundType type; + std::string rewardName; + + public: + explicit TimeBoundReference(TimeBoundType t) : type(t) { + // For rewards, use the other constructor. + assert(t != TimeBoundType::Reward); + } + + explicit TimeBoundReference(std::string const& rewardName) : type(TimeBoundType::Reward), rewardName(rewardName) { + assert(rewardName != ""); // Empty reward name is reserved. + } + + + bool isStepBound() const { + return type == TimeBoundType::Steps; + } + + bool isTimeBound() const { + return type == TimeBoundType::Time; + } + + bool isRewardBound() const { + return type == TimeBoundType::Reward; + } + }; + + } } diff --git a/src/storm/logic/VariableSubstitutionVisitor.cpp b/src/storm/logic/VariableSubstitutionVisitor.cpp index 96ede4769..8c0945adb 100644 --- a/src/storm/logic/VariableSubstitutionVisitor.cpp +++ b/src/storm/logic/VariableSubstitutionVisitor.cpp @@ -47,7 +47,7 @@ namespace storm { upperBound = TimeBound(f.isUpperBoundStrict(), f.getUpperBound().substitute(substitution)); } - return std::static_pointer_cast(std::make_shared(left, right, lowerBound, upperBound, f.getTimeBoundType())); + return std::static_pointer_cast(std::make_shared(left, right, lowerBound, upperBound, f.getTimeBoundReference())); } boost::any VariableSubstitutionVisitor::visit(CumulativeRewardFormula const& f, boost::any const&) const { diff --git a/src/storm/modelchecker/csl/HybridCtmcCslModelChecker.cpp b/src/storm/modelchecker/csl/HybridCtmcCslModelChecker.cpp index 16574947f..ba7a727c4 100644 --- a/src/storm/modelchecker/csl/HybridCtmcCslModelChecker.cpp +++ b/src/storm/modelchecker/csl/HybridCtmcCslModelChecker.cpp @@ -83,7 +83,7 @@ namespace storm { SymbolicQualitativeCheckResult const& leftResult = leftResultPointer->asSymbolicQualitativeCheckResult(); SymbolicQualitativeCheckResult const& rightResult = rightResultPointer->asSymbolicQualitativeCheckResult(); - STORM_LOG_THROW(!pathFormula.isStepBounded(), storm::exceptions::NotImplementedException, "Currently step-bounded properties on CTMCs are not supported."); + STORM_LOG_THROW(!pathFormula.getTimeBoundReference().isStepBound(), storm::exceptions::NotImplementedException, "Currently step-bounded properties on CTMCs are not supported."); double lowerBound = 0; double upperBound = 0; if (pathFormula.hasLowerBound()) { diff --git a/src/storm/modelchecker/csl/SparseCtmcCslModelChecker.cpp b/src/storm/modelchecker/csl/SparseCtmcCslModelChecker.cpp index 5de82a7d1..facfd3da2 100644 --- a/src/storm/modelchecker/csl/SparseCtmcCslModelChecker.cpp +++ b/src/storm/modelchecker/csl/SparseCtmcCslModelChecker.cpp @@ -60,7 +60,7 @@ namespace storm { ExplicitQualitativeCheckResult const& leftResult = leftResultPointer->asExplicitQualitativeCheckResult();; ExplicitQualitativeCheckResult const& rightResult = rightResultPointer->asExplicitQualitativeCheckResult(); - STORM_LOG_THROW(!pathFormula.isStepBounded(), storm::exceptions::NotImplementedException, "Currently step-bounded properties on CTMCs are not supported."); + STORM_LOG_THROW(!pathFormula.getTimeBoundReference().isStepBound(), storm::exceptions::NotImplementedException, "Currently step-bounded properties on CTMCs are not supported."); double lowerBound = 0; double upperBound = 0; if (pathFormula.hasLowerBound()) { diff --git a/src/storm/modelchecker/csl/SparseMarkovAutomatonCslModelChecker.cpp b/src/storm/modelchecker/csl/SparseMarkovAutomatonCslModelChecker.cpp index c444c72a5..2f90c23d5 100644 --- a/src/storm/modelchecker/csl/SparseMarkovAutomatonCslModelChecker.cpp +++ b/src/storm/modelchecker/csl/SparseMarkovAutomatonCslModelChecker.cpp @@ -54,7 +54,7 @@ namespace storm { std::unique_ptr rightResultPointer = this->check(pathFormula.getRightSubformula()); ExplicitQualitativeCheckResult const& rightResult = rightResultPointer->asExplicitQualitativeCheckResult(); - STORM_LOG_THROW(!pathFormula.isStepBounded(), storm::exceptions::NotImplementedException, "Currently step-bounded properties on MAs are not supported."); + STORM_LOG_THROW(!pathFormula.getTimeBoundReference().isStepBound(), storm::exceptions::NotImplementedException, "Currently step-bounded properties on MAs are not supported."); double lowerBound = 0; double upperBound = 0; if (pathFormula.hasLowerBound()) { diff --git a/src/storm/modelchecker/multiobjective/SparseMultiObjectivePreprocessor.cpp b/src/storm/modelchecker/multiobjective/SparseMultiObjectivePreprocessor.cpp index b2da20897..485bc41bf 100644 --- a/src/storm/modelchecker/multiobjective/SparseMultiObjectivePreprocessor.cpp +++ b/src/storm/modelchecker/multiobjective/SparseMultiObjectivePreprocessor.cpp @@ -266,7 +266,7 @@ namespace storm { template void SparseMultiObjectivePreprocessor::preprocessBoundedUntilFormula(storm::logic::BoundedUntilFormula const& formula, PreprocessorData& data) { - STORM_LOG_THROW(!data.originalModel.isOfType(storm::models::ModelType::MarkovAutomaton) || !formula.isStepBounded(), storm::exceptions::InvalidPropertyException, "Multi-objective model checking currently does not support STEP-bounded properties for Markov automata."); + STORM_LOG_THROW(!data.originalModel.isOfType(storm::models::ModelType::MarkovAutomaton) || !formula.getTimeBoundReference().isStepBound(), storm::exceptions::InvalidPropertyException, "Multi-objective model checking currently does not support STEP-bounded properties for Markov automata."); if (formula.hasLowerBound()) { STORM_LOG_THROW(!formula.getLowerBound().containsVariables(), storm::exceptions::InvalidPropertyException, "The lower time bound for the formula " << formula << " still contains variables"); diff --git a/src/storm/parser/FormulaParserGrammar.cpp b/src/storm/parser/FormulaParserGrammar.cpp index bee6b5117..95cb3f860 100644 --- a/src/storm/parser/FormulaParserGrammar.cpp +++ b/src/storm/parser/FormulaParserGrammar.cpp @@ -257,7 +257,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::TimeBoundType::Time)); + return std::shared_ptr(new storm::logic::BoundedUntilFormula(createBooleanLiteralFormula(true), subformula, timeBound.get().first, timeBound.get().second, storm::logic::TimeBoundReference(storm::logic::TimeBoundType::Time))); } else { return std::shared_ptr(new storm::logic::EventuallyFormula(subformula, context)); } @@ -273,7 +273,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::TimeBoundType::Time)); + return std::shared_ptr(new storm::logic::BoundedUntilFormula(leftSubformula, rightSubformula, timeBound.get().first, timeBound.get().second, storm::logic::TimeBoundReference(storm::logic::TimeBoundType::Time))); } else { return std::shared_ptr(new storm::logic::UntilFormula(leftSubformula, rightSubformula)); } diff --git a/src/storm/parser/JaniParser.cpp b/src/storm/parser/JaniParser.cpp index ecb3ed0ff..28ac7ae7c 100644 --- a/src/storm/parser/JaniParser.cpp +++ b/src/storm/parser/JaniParser.cpp @@ -297,7 +297,7 @@ namespace storm { } } } else if (propertyStructure.count("reward-instants") > 0) { - STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "Instant/Cumul. Reward for reward constraints not supported currently."); + STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "Instant Reward for reward constraints not supported currently."); } //STORM_LOG_THROW(!accTime && !accSteps, storm::exceptions::NotSupportedException, "Storm only allows accumulation if a step- or time-bound is given."); @@ -353,7 +353,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], storm::logic::TimeBound(pi.lowerBoundStrict, pi.lowerBound), storm::logic::TimeBound(pi.upperBoundStrict, pi.upperBound), storm::logic::TimeBoundType::Steps); + return std::make_shared(args[0], args[1], storm::logic::TimeBound(pi.lowerBoundStrict, pi.lowerBound), storm::logic::TimeBound(pi.upperBoundStrict, pi.upperBound), storm::logic::TimeBoundReference(storm::logic::TimeBoundType::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."); @@ -364,10 +364,26 @@ 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], storm::logic::TimeBound(pi.lowerBoundStrict, pi.lowerBound), storm::logic::TimeBound(pi.upperBoundStrict, pi.upperBound), storm::logic::TimeBoundType::Time); + return std::make_shared(args[0], args[1], storm::logic::TimeBound(pi.lowerBoundStrict, pi.lowerBound), storm::logic::TimeBound(pi.upperBoundStrict, pi.upperBound), storm::logic::TimeBoundReference(storm::logic::TimeBoundType::Time)); } else if (propertyStructure.count("reward-bounds") > 0 ) { + storm::jani::PropertyInterval pi = parsePropertyInterval(propertyStructure.at("reward-bounds")); + STORM_LOG_THROW(pi.hasUpperBound(), storm::exceptions::NotSupportedException, "Storm only supports time-bounded until with an upper bound."); + STORM_LOG_THROW(propertyStructure.at("reward-bounds").count("exp") == 1, storm::exceptions::InvalidJaniException, "Expecting reward-expression for operator " << opString << " in " << context); + storm::expressions::Expression rewExpr = parseExpression(propertyStructure.at("reward-bounds").at("exp"), "Reward expression in " + context, globalVars, constants); + STORM_LOG_THROW(!rewExpr.isVariable(), storm::exceptions::NotSupportedException, "Storm currently does not support complex reward expressions."); + std::string rewardName = rewExpr.getVariables().begin()->getName(); + STORM_LOG_WARN("Reward-type (steps, time) is deduced from model type."); + double lowerBound = 0.0; + if(pi.hasLowerBound()) { + lowerBound = pi.lowerBound.evaluateAsDouble(); + } + 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"); STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "Reward bounded properties are not supported by storm"); + return std::make_shared(args[0], args[1], storm::logic::TimeBound(pi.lowerBoundStrict, pi.lowerBound), storm::logic::TimeBound(pi.upperBoundStrict, pi.upperBound), storm::logic::TimeBoundReference(rewardName)); + } if (args[0]->isTrueFormula()) { return std::make_shared(args[1], formulaContext); diff --git a/src/storm/storage/jani/JSONExporter.cpp b/src/storm/storage/jani/JSONExporter.cpp index 65cab6fb1..5fde8267a 100644 --- a/src/storm/storage/jani/JSONExporter.cpp +++ b/src/storm/storage/jani/JSONExporter.cpp @@ -194,11 +194,14 @@ namespace storm { upperExclusive = f.isUpperBoundStrict(); } modernjson::json propertyInterval = constructPropertyInterval(lower, lowerExclusive, upper, upperExclusive); - - if(f.isStepBounded()) { + + auto tbr = f.getTimeBoundReference(); + if(tbr.isStepBound()) { opDecl["step-bounds"] = propertyInterval; - } else { + } else if(tbr.isRewardBound()) { opDecl["time-bounds"] = propertyInterval; + } else { + opDecl["reward-bounds"] = propertyInterval; } return opDecl; }