From 241fc880770351b0a650f3af12498ff21c3f6911 Mon Sep 17 00:00:00 2001 From: Sebastian Junges Date: Wed, 19 Jul 2017 20:23:52 +0200 Subject: [PATCH] multi-dimensional time bounds --- src/storm/logic/BoundedUntilFormula.cpp | 190 +++++++++++------- src/storm/logic/BoundedUntilFormula.h | 38 ++-- .../logic/VariableSubstitutionVisitor.cpp | 30 ++- src/storm/parser/JaniParser.cpp | 56 ++++-- 4 files changed, 199 insertions(+), 115 deletions(-) diff --git a/src/storm/logic/BoundedUntilFormula.cpp b/src/storm/logic/BoundedUntilFormula.cpp index ff5df2d2a..fecbf2673 100644 --- a/src/storm/logic/BoundedUntilFormula.cpp +++ b/src/storm/logic/BoundedUntilFormula.cpp @@ -11,10 +11,20 @@ namespace storm { namespace logic { - 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) { + 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."); } - + + BoundedUntilFormula::BoundedUntilFormula(std::shared_ptr const& leftSubformula, std::shared_ptr const& rightSubformula,std::vector> const& lowerBounds, std::vector> const& upperBounds, std::vector const& timeBoundReferences) : BinaryPathFormula(leftSubformula, rightSubformula), timeBoundReference(timeBoundReferences), lowerBound(lowerBounds), upperBound(upperBounds) { + assert(timeBoundReferences.size() == upperBound.size()); + assert(timeBoundReferences.size() == lowerBound.size()); + STORM_LOG_THROW(this->getDimension() != 0, storm::exceptions::InvalidArgumentException, "Bounded until formula requires at least one dimension."); + for(unsigned i = 0; i < timeBoundReferences.size(); ++i) { + STORM_LOG_THROW(hasLowerBound(i) || hasUpperBound(i), storm::exceptions::InvalidArgumentException, "Bounded until formula requires at least one bound in each dimension."); + } + } + + bool BoundedUntilFormula::isBoundedUntilFormula() const { return true; } @@ -28,111 +38,141 @@ namespace storm { } void BoundedUntilFormula::gatherReferencedRewardModels(std::set& referencedRewardModels) const { - if (this->getTimeBoundReference().isRewardBound()) { - referencedRewardModels.insert(this->getTimeBoundReference().getRewardName()); + for (unsigned i = 0; i < this->getDimension(); ++i) { + if (this->getTimeBoundReference(i).isRewardBound()) { + referencedRewardModels.insert(this->getTimeBoundReference().getRewardName()); + } } + this->getLeftSubformula().gatherReferencedRewardModels(referencedRewardModels); this->getRightSubformula().gatherReferencedRewardModels(referencedRewardModels); } - TimeBoundReference const& BoundedUntilFormula::getTimeBoundReference() const { - return timeBoundReference; + TimeBoundReference const& BoundedUntilFormula::getTimeBoundReference(unsigned i) const { + assert(i < timeBoundReference.size()); + return timeBoundReference.at(i); } + bool BoundedUntilFormula::isMultiDimensional() const { + assert(timeBoundReference.size() != 0); + return timeBoundReference.size() > 1; + } + unsigned BoundedUntilFormula::getDimension() const { + return timeBoundReference.size(); + } - bool BoundedUntilFormula::isLowerBoundStrict() const { - return lowerBound.get().isStrict(); + bool BoundedUntilFormula::isLowerBoundStrict(unsigned i) const { + assert(i < lowerBound.size()); + return lowerBound.at(i).get().isStrict(); } bool BoundedUntilFormula::hasLowerBound() const { - return static_cast(lowerBound); + for(auto const& lb : lowerBound) { + if (static_cast(lb)) { + return true; + } + } + return false; + } + + bool BoundedUntilFormula::hasLowerBound(unsigned i) const { + return static_cast(lowerBound.at(i)); } - bool BoundedUntilFormula::hasIntegerLowerBound() const { - return lowerBound.get().getBound().hasIntegerType(); + bool BoundedUntilFormula::hasIntegerLowerBound(unsigned i) const { + return lowerBound.at(i).get().getBound().hasIntegerType(); } - bool BoundedUntilFormula::isUpperBoundStrict() const { - return upperBound.get().isStrict(); + bool BoundedUntilFormula::isUpperBoundStrict(unsigned i) const { + return upperBound.at(i).get().isStrict(); } bool BoundedUntilFormula::hasUpperBound() const { - return static_cast(upperBound); + for(auto const& ub : upperBound) { + if (static_cast(ub)) { + return true; + } + } + return false; } - bool BoundedUntilFormula::hasIntegerUpperBound() const { - return upperBound.get().getBound().hasIntegerType(); + bool BoundedUntilFormula::hasUpperBound(unsigned i) const { + return static_cast(upperBound.at(i)); } - storm::expressions::Expression const& BoundedUntilFormula::getLowerBound() const { - return lowerBound.get().getBound(); + bool BoundedUntilFormula::hasIntegerUpperBound(unsigned i) const { + return upperBound.at(i).get().getBound().hasIntegerType(); + } + + storm::expressions::Expression const& BoundedUntilFormula::getLowerBound(unsigned i) const { + return lowerBound.at(i).get().getBound(); } - storm::expressions::Expression const& BoundedUntilFormula::getUpperBound() const { - return upperBound.get().getBound(); + storm::expressions::Expression const& BoundedUntilFormula::getUpperBound(unsigned i) const { + return upperBound.at(i).get().getBound(); } template <> - double BoundedUntilFormula::getLowerBound() const { + double BoundedUntilFormula::getLowerBound(unsigned i) const { checkNoVariablesInBound(this->getLowerBound()); - double bound = this->getLowerBound().evaluateAsDouble(); + double bound = this->getLowerBound(i).evaluateAsDouble(); STORM_LOG_THROW(bound >= 0, storm::exceptions::InvalidPropertyException, "Time-bound must not evaluate to negative number."); return bound; } template <> - double BoundedUntilFormula::getUpperBound() const { + double BoundedUntilFormula::getUpperBound(unsigned i) const { checkNoVariablesInBound(this->getUpperBound()); - double bound = this->getUpperBound().evaluateAsDouble(); + double bound = this->getUpperBound(i).evaluateAsDouble(); STORM_LOG_THROW(bound >= 0, storm::exceptions::InvalidPropertyException, "Time-bound must not evaluate to negative number."); return bound; } template <> - storm::RationalNumber BoundedUntilFormula::getLowerBound() const { - checkNoVariablesInBound(this->getLowerBound()); - storm::RationalNumber bound = this->getLowerBound().evaluateAsRational(); + storm::RationalNumber BoundedUntilFormula::getLowerBound(unsigned i) const { + checkNoVariablesInBound(this->getLowerBound(i)); + storm::RationalNumber bound = this->getLowerBound(i).evaluateAsRational(); STORM_LOG_THROW(bound >= storm::utility::zero(), storm::exceptions::InvalidPropertyException, "Time-bound must not evaluate to negative number."); return bound; } template <> - storm::RationalNumber BoundedUntilFormula::getUpperBound() const { - checkNoVariablesInBound(this->getUpperBound()); - storm::RationalNumber bound = this->getUpperBound().evaluateAsRational(); + storm::RationalNumber BoundedUntilFormula::getUpperBound(unsigned i) const { + checkNoVariablesInBound(this->getUpperBound(i)); + storm::RationalNumber bound = this->getUpperBound(i).evaluateAsRational(); STORM_LOG_THROW(bound >= storm::utility::zero(), storm::exceptions::InvalidPropertyException, "Time-bound must not evaluate to negative number."); return bound; } template <> - uint64_t BoundedUntilFormula::getLowerBound() const { - checkNoVariablesInBound(this->getLowerBound()); - int_fast64_t bound = this->getLowerBound().evaluateAsInt(); + uint64_t BoundedUntilFormula::getLowerBound(unsigned i) const { + checkNoVariablesInBound(this->getLowerBound(i)); + int_fast64_t bound = this->getLowerBound(i).evaluateAsInt(); STORM_LOG_THROW(bound >= 0, storm::exceptions::InvalidPropertyException, "Time-bound must not evaluate to negative number."); return static_cast(bound); } template <> - uint64_t BoundedUntilFormula::getUpperBound() const { - checkNoVariablesInBound(this->getUpperBound()); - int_fast64_t bound = this->getUpperBound().evaluateAsInt(); + uint64_t BoundedUntilFormula::getUpperBound(unsigned i) const { + checkNoVariablesInBound(this->getUpperBound(i)); + int_fast64_t bound = this->getUpperBound(i).evaluateAsInt(); STORM_LOG_THROW(bound >= 0, storm::exceptions::InvalidPropertyException, "Time-bound must not evaluate to negative number."); return static_cast(bound); } template <> - double BoundedUntilFormula::getNonStrictUpperBound() const { - double bound = getUpperBound(); - STORM_LOG_THROW(!isUpperBoundStrict() || bound > 0, storm::exceptions::InvalidPropertyException, "Cannot retrieve non-strict bound from strict zero-bound."); + double BoundedUntilFormula::getNonStrictUpperBound(unsigned i) const { + double bound = getUpperBound(i); + STORM_LOG_THROW(!isUpperBoundStrict(i) || bound > 0, storm::exceptions::InvalidPropertyException, "Cannot retrieve non-strict bound from strict zero-bound."); return bound; } template <> - uint64_t BoundedUntilFormula::getNonStrictUpperBound() const { - int_fast64_t bound = getUpperBound(); - if (isUpperBoundStrict()) { + uint64_t BoundedUntilFormula::getNonStrictUpperBound(unsigned i) const { + int_fast64_t bound = getUpperBound(i); + if (isUpperBoundStrict(i)) { STORM_LOG_THROW(bound > 0, storm::exceptions::InvalidPropertyException, "Cannot retrieve non-strict bound from strict zero-bound."); return bound - 1; } else { @@ -148,41 +188,53 @@ namespace storm { this->getLeftSubformula().writeToStream(out); out << " U"; - if (this->getTimeBoundReference().isRewardBound()) { - out << "{\"" << this->getTimeBoundReference().getRewardName() << "\"}"; + if (this->isMultiDimensional()) { + out << "["; } - if (this->hasLowerBound()) { - if (this->hasUpperBound()) { - if (this->isLowerBoundStrict()) { - out << "("; - } else { - out << "["; - } - out << this->getLowerBound(); - out << ", "; - out << this->getUpperBound(); - if (this->isUpperBoundStrict()) { - out << ")"; + for(unsigned i = 0; i < this->getDimension(); ++i) { + if (i > 0) { + out << ","; + } + if (this->getTimeBoundReference(i).isRewardBound()) { + out << "{\"" << this->getTimeBoundReference(i).getRewardName() << "\"}"; + } + if (this->hasLowerBound(i)) { + if (this->hasUpperBound(i)) { + if (this->isLowerBoundStrict(i)) { + out << "("; + } else { + out << "["; + } + out << this->getLowerBound(i); + out << ", "; + out << this->getUpperBound(i); + if (this->isUpperBoundStrict(i)) { + out << ")"; + } else { + out << "]"; + } } else { - out << "]"; + if (this->isLowerBoundStrict(i)) { + out << ">"; + } else { + out << ">="; + } + out << getLowerBound(i); } } else { - if (this->isLowerBoundStrict()) { - out << ">"; + if (this->isUpperBoundStrict(i)) { + out << "<"; } else { - out << ">="; + out << "<="; } - out << getLowerBound(); + out << this->getUpperBound(i); } - } else { - if (this->isUpperBoundStrict()) { - out << "<"; - } else { - out << "<="; - } - out << this->getUpperBound(); + out << " "; + } + if (this->isMultiDimensional()) { + out << "]"; } - out << " "; + this->getRightSubformula().writeToStream(out); return out; diff --git a/src/storm/logic/BoundedUntilFormula.h b/src/storm/logic/BoundedUntilFormula.h index 5ff571d84..2b2e33945 100644 --- a/src/storm/logic/BoundedUntilFormula.h +++ b/src/storm/logic/BoundedUntilFormula.h @@ -1,5 +1,4 @@ -#ifndef STORM_LOGIC_BOUNDEDUNTILFORMULA_H_ -#define STORM_LOGIC_BOUNDEDUNTILFORMULA_H_ +#pragma once #include @@ -13,7 +12,8 @@ namespace storm { class BoundedUntilFormula : public BinaryPathFormula { public: BoundedUntilFormula(std::shared_ptr const& leftSubformula, std::shared_ptr const& rightSubformula, boost::optional const& lowerBound, boost::optional const& upperBound, TimeBoundReference const& timeBoundReference); - + BoundedUntilFormula(std::shared_ptr const& leftSubformula, std::shared_ptr const& rightSubformula, std::vector> const& lowerBounds, std::vector> const& upperBounds, std::vector const& timeBoundReferences); + virtual bool isBoundedUntilFormula() const override; virtual bool isProbabilityPathFormula() const override; @@ -22,39 +22,43 @@ namespace storm { virtual void gatherReferencedRewardModels(std::set& referencedRewardModels) const override; - TimeBoundReference const& getTimeBoundReference() const; + TimeBoundReference const& getTimeBoundReference(unsigned i = 0) const; - bool isLowerBoundStrict() const; + bool isLowerBoundStrict(unsigned i = 0) const; bool hasLowerBound() const; - bool hasIntegerLowerBound() const; + bool hasLowerBound(unsigned i) const; + bool hasIntegerLowerBound(unsigned i = 0) const; - bool isUpperBoundStrict() const; + bool isUpperBoundStrict(unsigned i = 0) const; bool hasUpperBound() const; - bool hasIntegerUpperBound() const; + bool hasUpperBound(unsigned i) const; + bool hasIntegerUpperBound(unsigned i = 0) const; + + bool isMultiDimensional() const; + unsigned getDimension() const; - storm::expressions::Expression const& getLowerBound() const; - storm::expressions::Expression const& getUpperBound() const; + storm::expressions::Expression const& getLowerBound(unsigned i = 0) const; + storm::expressions::Expression const& getUpperBound(unsigned i = 0) const; template - ValueType getLowerBound() const; + ValueType getLowerBound(unsigned i = 0) const; template - ValueType getUpperBound() const; + ValueType getUpperBound(unsigned i = 0) const; template - ValueType getNonStrictUpperBound() const; + ValueType getNonStrictUpperBound(unsigned i = 0) const; virtual std::ostream& writeToStream(std::ostream& out) const override; private: static void checkNoVariablesInBound(storm::expressions::Expression const& bound); - TimeBoundReference timeBoundReference; - boost::optional lowerBound; - boost::optional upperBound; + std::vector timeBoundReference; + std::vector> lowerBound; + std::vector> upperBound; }; } } -#endif /* STORM_LOGIC_BOUNDEDUNTILFORMULA_H_ */ diff --git a/src/storm/logic/VariableSubstitutionVisitor.cpp b/src/storm/logic/VariableSubstitutionVisitor.cpp index 8c0945adb..00eee1e01 100644 --- a/src/storm/logic/VariableSubstitutionVisitor.cpp +++ b/src/storm/logic/VariableSubstitutionVisitor.cpp @@ -37,17 +37,29 @@ namespace storm { boost::any VariableSubstitutionVisitor::visit(BoundedUntilFormula const& f, boost::any const& data) const { auto left = boost::any_cast>(f.getLeftSubformula().accept(*this, data)); auto right = boost::any_cast>(f.getRightSubformula().accept(*this, data)); - - boost::optional lowerBound; - if (f.hasLowerBound()) { - lowerBound = TimeBound(f.isLowerBoundStrict(), f.getLowerBound().substitute(substitution)); - } - boost::optional upperBound; - if (f.hasUpperBound()) { - upperBound = TimeBound(f.isUpperBoundStrict(), f.getUpperBound().substitute(substitution)); + + std::vector> lowerBounds; + std::vector> upperBounds; + std::vector tbReferences; + + for (unsigned i = 0; i < f.getDimension(); ++i) { + std::cout << f.hasLowerBound(i) << std::endl; + if (f.hasLowerBound(i)) { + lowerBounds.push_back(TimeBound(f.isLowerBoundStrict(i), f.getLowerBound(i).substitute(substitution))); + } else { + lowerBounds.push_back(boost::none); + } + + if (f.hasUpperBound(i)) { + upperBounds.push_back(TimeBound(f.isUpperBoundStrict(i), f.getUpperBound(i).substitute(substitution))); + } else { + lowerBounds.push_back(boost::none); + } + tbReferences.push_back(f.getTimeBoundReference(i)); } - return std::static_pointer_cast(std::make_shared(left, right, lowerBound, upperBound, f.getTimeBoundReference())); + + return std::static_pointer_cast(std::make_shared(left, right, lowerBounds, upperBounds, tbReferences)); } boost::any VariableSubstitutionVisitor::visit(CumulativeRewardFormula const& f, boost::any const&) const { diff --git a/src/storm/parser/JaniParser.cpp b/src/storm/parser/JaniParser.cpp index 28ac7ae7c..f92acab7a 100644 --- a/src/storm/parser/JaniParser.cpp +++ b/src/storm/parser/JaniParser.cpp @@ -165,9 +165,8 @@ namespace storm { if (piStructure.count("lower") > 0) { pi.lowerBound = parseExpression(piStructure.at("lower"), "Lower bound for property interval", {}, {}); // TODO substitute constants. + std::cout << "have lower bound" << std::endl; STORM_LOG_THROW(!pi.lowerBound.containsVariables(), storm::exceptions::NotSupportedException, "Only constant expressions are supported as lower bounds"); - - } if (piStructure.count("lower-exclusive") > 0) { STORM_LOG_THROW(pi.lowerBound.isInitialized(), storm::exceptions::InvalidJaniException, "Lower-exclusive can only be set if a lower bound is present"); @@ -175,16 +174,17 @@ namespace storm { } if (piStructure.count("upper") > 0) { + std::cout << "have upper bound" << std::endl; pi.upperBound = parseExpression(piStructure.at("upper"), "Upper bound for property interval", {}, {}); // TODO substitute constants. STORM_LOG_THROW(!pi.upperBound.containsVariables(), storm::exceptions::NotSupportedException, "Only constant expressions are supported as upper bounds"); } if (piStructure.count("upper-exclusive") > 0) { - STORM_LOG_THROW(pi.lowerBound.isInitialized(), storm::exceptions::InvalidJaniException, "Lower-exclusive can only be set if a lower bound is present"); - pi.lowerBoundStrict = piStructure.at("upper-exclusive"); + STORM_LOG_THROW(pi.upperBound.isInitialized(), storm::exceptions::InvalidJaniException, "Lower-exclusive can only be set if a lower bound is present"); + pi.upperBoundStrict = piStructure.at("upper-exclusive"); } - STORM_LOG_THROW(pi.lowerBound.isInitialized() || pi.upperBound.isInitialized(), storm::exceptions::InvalidJaniException, "Bounded operators must be bounded"); + STORM_LOG_THROW(pi.lowerBound.isInitialized() || pi.upperBound.isInitialized(), storm::exceptions::InvalidJaniException, "Bounded operator must have a bounded interval, but no bounds found in '" << piStructure << "'"); return pi; @@ -367,22 +367,38 @@ namespace 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(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(); + std::vector> lowerBounds; + std::vector> upperBounds; + std::vector tbReferences; + for (auto const& rbStructure : propertyStructure.at("reward-bounds")) { + storm::jani::PropertyInterval pi = parsePropertyInterval(rbStructure.at("bounds")); + STORM_LOG_THROW(pi.hasUpperBound(), storm::exceptions::NotSupportedException, "Storm only supports time-bounded until with an upper bound."); + STORM_LOG_THROW(rbStructure.count("exp") == 1, storm::exceptions::InvalidJaniException, "Expecting reward-expression for operator " << opString << " in " << context); + storm::expressions::Expression rewExpr = parseExpression(rbStructure.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"); + if (pi.hasLowerBound()) { + lowerBounds.push_back(storm::logic::TimeBound(pi.lowerBoundStrict, pi.lowerBound)); + } else { + lowerBounds.push_back(boost::none); + } + if (pi.hasUpperBound()) { + upperBounds.push_back(storm::logic::TimeBound(pi.upperBoundStrict, pi.upperBound)); + } else { + upperBounds.push_back(boost::none); + } + tbReferences.push_back(storm::logic::TimeBoundReference(rewardName)); } - 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)); + auto res = std::make_shared(args[0], args[1], lowerBounds, upperBounds, tbReferences); + return res; } if (args[0]->isTrueFormula()) {