diff --git a/src/storm-parsers/parser/FormulaParser.cpp b/src/storm-parsers/parser/FormulaParser.cpp index 37dad72d3..485a4bb18 100644 --- a/src/storm-parsers/parser/FormulaParser.cpp +++ b/src/storm-parsers/parser/FormulaParser.cpp @@ -60,7 +60,7 @@ namespace storm { storm::utility::openFile(filename, inputFileStream); std::vector properties; - + // Now try to parse the contents of the file. try { std::string fileContent((std::istreambuf_iterator(inputFileStream)), (std::istreambuf_iterator())); @@ -70,7 +70,7 @@ namespace storm { storm::utility::closeFile(inputFileStream); throw e; } - + // Close the stream in case everything went smoothly and return result. storm::utility::closeFile(inputFileStream); return properties; diff --git a/src/storm-parsers/parser/FormulaParserGrammar.cpp b/src/storm-parsers/parser/FormulaParserGrammar.cpp index 7b51a552d..9d5f0283e 100644 --- a/src/storm-parsers/parser/FormulaParserGrammar.cpp +++ b/src/storm-parsers/parser/FormulaParserGrammar.cpp @@ -62,7 +62,7 @@ namespace storm { eventuallyFormula = (qi::lit("F") >> (-timeBounds) >> pathFormulaWithoutUntil(qi::_r1))[qi::_val = phoenix::bind(&FormulaParserGrammar::createEventuallyFormula, phoenix::ref(*this), qi::_1, qi::_r1, qi::_2)]; eventuallyFormula.name("eventually formula"); - globallyFormula = (qi::lit("G") >> pathFormulaWithoutUntil(qi::_r1))[qi::_val = phoenix::bind(&FormulaParserGrammar::createGloballyFormula, phoenix::ref(*this), qi::_1)]; + globallyFormula = (qi::lit("G") >> (-timeBounds) >> pathFormulaWithoutUntil(qi::_r1))[qi::_val = phoenix::bind(&FormulaParserGrammar::createGloballyFormula, phoenix::ref(*this), qi::_1, qi::_2)]; globallyFormula.name("globally formula"); nextFormula = (qi::lit("X") >> pathFormulaWithoutUntil(qi::_r1))[qi::_val = phoenix::bind(&FormulaParserGrammar::createNextFormula, phoenix::ref(*this), qi::_1)]; @@ -324,8 +324,20 @@ namespace storm { } } - std::shared_ptr FormulaParserGrammar::createGloballyFormula(std::shared_ptr const& subformula) const { - return std::shared_ptr(new storm::logic::GloballyFormula(subformula)); + 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::createNextFormula(std::shared_ptr const& subformula) const { diff --git a/src/storm-parsers/parser/FormulaParserGrammar.h b/src/storm-parsers/parser/FormulaParserGrammar.h index ad76aa87f..75903d04a 100644 --- a/src/storm-parsers/parser/FormulaParserGrammar.h +++ b/src/storm-parsers/parser/FormulaParserGrammar.h @@ -228,7 +228,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(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 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 createConditionalFormula(std::shared_ptr const& leftSubformula, std::shared_ptr const& rightSubformula, storm::logic::FormulaContext context) const; diff --git a/src/storm/logic/BoundedGloballyFormula.cpp b/src/storm/logic/BoundedGloballyFormula.cpp new file mode 100644 index 000000000..736625d4e --- /dev/null +++ b/src/storm/logic/BoundedGloballyFormula.cpp @@ -0,0 +1,280 @@ +#include "storm/logic/BoundedGloballyFormula.h" + +#include "storm/utility/constants.h" +#include "storm/utility/macros.h" +#include "storm/exceptions/InvalidArgumentException.h" + +#include "storm/logic/FormulaVisitor.h" + +#include "storm/exceptions/InvalidPropertyException.h" +#include "storm/exceptions/InvalidOperationException.h" + +namespace storm { + namespace logic { + BoundedGloballyFormula::BoundedGloballyFormula(std::shared_ptr const& subformula, boost::optional const& lowerBound, boost::optional const& upperBound, TimeBoundReference const& timeBoundReference) : UnaryPathFormula(subformula), subformula({subformula}), timeBoundReference({timeBoundReference}), lowerBound({lowerBound}), upperBound({upperBound}) { + STORM_LOG_THROW(lowerBound || upperBound, storm::exceptions::InvalidArgumentException, "Bounded until formula requires at least one bound."); + } + + BoundedGloballyFormula::BoundedGloballyFormula(std::shared_ptr const& subformula, std::vector> const& lowerBounds, std::vector> const& upperBounds, std::vector const& timeBoundReferences) : UnaryPathFormula(subformula), subformula({subformula}), timeBoundReference(timeBoundReferences), lowerBound(lowerBounds), upperBound(upperBounds) { + assert(timeBoundReferences.size() == upperBound.size()); + assert(timeBoundReferences.size() == lowerBound.size()); + } + + // TODO handle the input for a vector of subformulas to UnaryPathFormula + BoundedGloballyFormula::BoundedGloballyFormula(std::vector> const& subformulas, std::vector> const& lowerBounds, std::vector> const& upperBounds, std::vector const& timeBoundReferences) : UnaryPathFormula(subformulas.at(0)), subformula({subformula}), timeBoundReference(timeBoundReferences), lowerBound(lowerBounds), upperBound(upperBounds) { + assert(subformula.size() == timeBoundReference.size()); + assert(timeBoundReference.size() == lowerBound.size()); + assert(lowerBound.size() == upperBound.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 BoundedGloballyFormula::isBoundedGloballyFormula() const { + return true; + } + + bool BoundedGloballyFormula::isProbabilityPathFormula() const { + return true; + } + + boost::any BoundedGloballyFormula::accept(FormulaVisitor const& visitor, boost::any const& data) const { + return visitor.visit(*this, data); + } + + bool BoundedGloballyFormula::isMultiDimensional() const { + assert(timeBoundReference.size() != 0); + return timeBoundReference.size() > 1; + } + + bool BoundedGloballyFormula::hasMultiDimensionalSubformulas() const { + assert(subformula.size() != 0); + return subformula.size() > 1; + } + + unsigned BoundedGloballyFormula::getDimension() const { + return timeBoundReference.size(); + } + + Formula const& BoundedGloballyFormula::getSubformula() const { + STORM_LOG_ASSERT(subformula.size() == 1, "The subformula is not unique."); + return *subformula.at(0); + } + + Formula const& BoundedGloballyFormula::getSubformula(unsigned i) const { + if (subformula.size() == 1 && i < getDimension()) { + return getSubformula(); + } else { + return *subformula.at(i); + } + } + + TimeBoundReference const& BoundedGloballyFormula::getTimeBoundReference(unsigned i) const { + assert(i < timeBoundReference.size()); + return timeBoundReference.at(i); + } + + bool BoundedGloballyFormula::isLowerBoundStrict(unsigned i) const { + assert(i < lowerBound.size()); + if (!hasLowerBound(i)) { return false; } + return lowerBound.at(i).get().isStrict(); + } + + bool BoundedGloballyFormula::hasLowerBound() const { + for(auto const& lb : lowerBound) { + if (static_cast(lb)) { + return true; + } + } + return false; + } + + bool BoundedGloballyFormula::hasLowerBound(unsigned i) const { + return static_cast(lowerBound.at(i)); + } + + bool BoundedGloballyFormula::hasIntegerLowerBound(unsigned i) const { + if (!hasLowerBound(i)) { return true; } + return lowerBound.at(i).get().getBound().hasIntegerType(); + } + + bool BoundedGloballyFormula::isUpperBoundStrict(unsigned i) const { + return upperBound.at(i).get().isStrict(); + } + + bool BoundedGloballyFormula::hasUpperBound() const { + for (auto const& ub : upperBound) { + if (static_cast(ub)) { + return true; + } + } + return false; + } + + bool BoundedGloballyFormula::hasUpperBound(unsigned i) const { + return static_cast(upperBound.at(i)); + } + + bool BoundedGloballyFormula::hasIntegerUpperBound(unsigned i) const { + return upperBound.at(i).get().getBound().hasIntegerType(); + } + + storm::expressions::Expression const& BoundedGloballyFormula::getLowerBound(unsigned i) const { + return lowerBound.at(i).get().getBound(); + } + + storm::expressions::Expression const& BoundedGloballyFormula::getUpperBound(unsigned i) const { + return upperBound.at(i).get().getBound(); + } + + template <> + double BoundedGloballyFormula::getLowerBound(unsigned i) const { + if (!hasLowerBound(i)) { return 0.0; } + checkNoVariablesInBound(this->getLowerBound()); + 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 BoundedGloballyFormula::getUpperBound(unsigned i) const { + checkNoVariablesInBound(this->getUpperBound()); + 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 BoundedGloballyFormula::getLowerBound(unsigned i) const { + if (!hasLowerBound(i)) { return storm::utility::zero(); } + 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 BoundedGloballyFormula::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 BoundedGloballyFormula::getLowerBound(unsigned i) const { + if (!hasLowerBound(i)) { return 0; } + 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 BoundedGloballyFormula::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 BoundedGloballyFormula::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 BoundedGloballyFormula::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 { + return bound; + } + } + + template <> + double BoundedGloballyFormula::getNonStrictLowerBound(unsigned i) const { + double bound = getLowerBound(i); + STORM_LOG_THROW(!isLowerBoundStrict(i), storm::exceptions::InvalidPropertyException, "Cannot retrieve non-strict lower bound from strict lower-bound."); + return bound; + } + + template <> + uint64_t BoundedGloballyFormula::getNonStrictLowerBound(unsigned i) const { + int_fast64_t bound = getLowerBound(i); + if (isLowerBoundStrict(i)) { + return bound + 1; + } else { + return bound; + } + } + + void BoundedGloballyFormula::checkNoVariablesInBound(storm::expressions::Expression const& bound) { + 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 { + out << "G" ; + if (this->isMultiDimensional()) { + out << "^{"; + } + for (unsigned i = 0; i < this->getDimension(); ++i) { + if (i > 0) { + out << ", "; + } + if (this->getTimeBoundReference(i).isRewardBound()) { + out << "rew"; + if (this->getTimeBoundReference(i).hasRewardAccumulation()) { + out << "[" << this->getTimeBoundReference(i).getRewardAccumulation() << "]"; + } + out << "{\"" << this->getTimeBoundReference(i).getRewardName() << "\"}"; + } else if (this->getTimeBoundReference(i).isStepBound()) { + out << "steps"; + } + 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 { + if (this->isLowerBoundStrict(i)) { + out << ">"; + } else { + out << ">="; + } + out << getLowerBound(i); + } + } else { + if (this->isUpperBoundStrict(i)) { + out << "<"; + } else { + out << "<="; + } + out << this->getUpperBound(i); + } + out << " "; + } + if (this->isMultiDimensional()) { + out << "}"; + } + this->getSubformula().writeToStream(out); + + return out; + } + } +} \ No newline at end of file diff --git a/src/storm/logic/BoundedGloballyFormula.h b/src/storm/logic/BoundedGloballyFormula.h new file mode 100644 index 000000000..644bd950c --- /dev/null +++ b/src/storm/logic/BoundedGloballyFormula.h @@ -0,0 +1,76 @@ +#pragma once + +#include + +#include "storm/logic/UnaryPathFormula.h" + +#include "storm/logic/TimeBound.h" +#include "storm/logic/TimeBoundType.h" + +namespace storm { + namespace logic { + class BoundedGloballyFormula : public UnaryPathFormula { + public: + BoundedGloballyFormula(std::shared_ptr const& subformula, boost::optional const& lowerBound, boost::optional const& upperBound, TimeBoundReference const& timeBoundReference); + BoundedGloballyFormula(std::shared_ptr const& subformula, std::vector> const& lowerBounds, std::vector> const& upperBounds, std::vector const& timeBoundReferences); + BoundedGloballyFormula(std::vector> const& subformulas, std::vector> const& lowerBounds, std::vector> const& upperBounds, std::vector const& timeBoundReferences); + + virtual ~BoundedGloballyFormula() { + // Intentionally left empty. + } + + virtual bool isBoundedGloballyFormula() const override; + virtual bool isProbabilityPathFormula() const override; + + virtual boost::any accept(FormulaVisitor const &visitor, boost::any const &data) const override; + + + + bool isMultiDimensional() const; + bool hasMultiDimensionalSubformulas() const; + unsigned getDimension() const; + + Formula const& getSubformula() const; + Formula const& getSubformula(unsigned i) const; + + TimeBoundReference const& getTimeBoundReference(unsigned i = 0) const; + + bool isLowerBoundStrict(unsigned i = 0) const; + bool hasLowerBound() const; + bool hasLowerBound(unsigned i) const; + bool hasIntegerLowerBound(unsigned i = 0) const; + + bool isUpperBoundStrict(unsigned i = 0) const; + bool hasUpperBound() const; + bool hasUpperBound(unsigned i) const; + bool hasIntegerUpperBound(unsigned i = 0) const; + + storm::expressions::Expression const& getLowerBound(unsigned i = 0) const; + storm::expressions::Expression const& getUpperBound(unsigned i = 0) const; + + template + ValueType getLowerBound(unsigned i = 0) const; + + template + ValueType getUpperBound(unsigned i = 0) const; + + template + ValueType getNonStrictUpperBound(unsigned i = 0) const; + + template + ValueType getNonStrictLowerBound(unsigned i = 0) const; + + + + virtual std::ostream &writeToStream(std::ostream &out) const override; + + private: + static void checkNoVariablesInBound(storm::expressions::Expression const& bound); + + std::vector> subformula; + std::vector timeBoundReference; + std::vector> lowerBound; + std::vector> upperBound; + }; + } +} \ No newline at end of file diff --git a/src/storm/logic/CloneVisitor.cpp b/src/storm/logic/CloneVisitor.cpp index 103c47fc0..57c8ce377 100644 --- a/src/storm/logic/CloneVisitor.cpp +++ b/src/storm/logic/CloneVisitor.cpp @@ -28,6 +28,34 @@ namespace storm { return std::static_pointer_cast(std::make_shared(f)); } + boost::any CloneVisitor::visit(BoundedGloballyFormula const& f, boost::any const& data) const { + std::vector> lowerBounds, upperBounds; + std::vector timeBoundReferences; + for (uint64_t i = 0; i < f.getDimension(); ++i) { + if (f.hasLowerBound(i)) { + lowerBounds.emplace_back(TimeBound(f.isLowerBoundStrict(i), f.getLowerBound(i))); + } else { + lowerBounds.emplace_back(); + } + if (f.hasUpperBound(i)) { + upperBounds.emplace_back(TimeBound(f.isUpperBoundStrict(i), f.getUpperBound(i))); + } else { + upperBounds.emplace_back(); + } + timeBoundReferences.push_back(f.getTimeBoundReference(i)); + } + if (f.hasMultiDimensionalSubformulas()) { + std::vector> subformulas; + for (uint64_t i = 0; i < f.getDimension(); ++i) { + subformulas.push_back(boost::any_cast>(f.getSubformula(i).accept(*this, data))); + } + return std::static_pointer_cast(std::make_shared(subformulas, lowerBounds, upperBounds, timeBoundReferences)); + } else { + std::shared_ptr subformula = boost::any_cast>(f.getSubformula().accept(*this, data)); + return std::static_pointer_cast(std::make_shared(subformula, lowerBounds, upperBounds, timeBoundReferences)); + } + } + boost::any CloneVisitor::visit(BoundedUntilFormula const& f, boost::any const& data) const { std::vector> lowerBounds, upperBounds; std::vector timeBoundReferences; diff --git a/src/storm/logic/CloneVisitor.h b/src/storm/logic/CloneVisitor.h index 5ff29e816..61578bdca 100644 --- a/src/storm/logic/CloneVisitor.h +++ b/src/storm/logic/CloneVisitor.h @@ -16,6 +16,7 @@ namespace storm { 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(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; diff --git a/src/storm/logic/Formula.cpp b/src/storm/logic/Formula.cpp index d8b399e34..b4e6c13bc 100644 --- a/src/storm/logic/Formula.cpp +++ b/src/storm/logic/Formula.cpp @@ -115,6 +115,10 @@ namespace storm { return false; } + bool Formula::isBoundedGloballyFormula() const { + return false; + } + bool Formula::isLongRunAverageOperatorFormula() const { return false; } @@ -373,6 +377,14 @@ namespace storm { return dynamic_cast(*this); } + BoundedGloballyFormula& Formula::asBoundedGloballyFormula() { + return dynamic_cast(*this); + } + + BoundedGloballyFormula const& Formula::asBoundedGloballyFormula() const { + return dynamic_cast(*this); + } + LongRunAverageOperatorFormula& Formula::asLongRunAverageOperatorFormula() { return dynamic_cast(*this); } diff --git a/src/storm/logic/Formula.h b/src/storm/logic/Formula.h index 294637c2e..62aab0dde 100644 --- a/src/storm/logic/Formula.h +++ b/src/storm/logic/Formula.h @@ -71,6 +71,7 @@ namespace storm { virtual bool isGloballyFormula() const; virtual bool isEventuallyFormula() const; virtual bool isReachabilityProbabilityFormula() const; + virtual bool isBoundedGloballyFormula() const; // Reward formulas. virtual bool isCumulativeRewardFormula() const; @@ -172,7 +173,10 @@ namespace storm { NextFormula& asNextFormula(); NextFormula const& asNextFormula() const; - + + BoundedGloballyFormula& asBoundedGloballyFormula(); + BoundedGloballyFormula const& asBoundedGloballyFormula() const; + LongRunAverageOperatorFormula& asLongRunAverageOperatorFormula(); LongRunAverageOperatorFormula const& asLongRunAverageOperatorFormula() const; diff --git a/src/storm/logic/FormulaInformationVisitor.cpp b/src/storm/logic/FormulaInformationVisitor.cpp index 41976aa57..41417eeed 100644 --- a/src/storm/logic/FormulaInformationVisitor.cpp +++ b/src/storm/logic/FormulaInformationVisitor.cpp @@ -24,6 +24,10 @@ namespace storm { boost::any FormulaInformationVisitor::visit(BooleanLiteralFormula const&, boost::any const&) const { return FormulaInformation(); } + + boost::any FormulaInformationVisitor::visit(BoundedGloballyFormula const& f, boost::any const& data) const { + return f.getSubformula().accept(*this, data); + } boost::any FormulaInformationVisitor::visit(BoundedUntilFormula const& f, boost::any const& data) const { FormulaInformation result; diff --git a/src/storm/logic/FormulaInformationVisitor.h b/src/storm/logic/FormulaInformationVisitor.h index 617386961..ecf5a1ab7 100644 --- a/src/storm/logic/FormulaInformationVisitor.h +++ b/src/storm/logic/FormulaInformationVisitor.h @@ -15,6 +15,7 @@ namespace storm { 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(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; diff --git a/src/storm/logic/FormulaVisitor.h b/src/storm/logic/FormulaVisitor.h index 6bf5b8c50..23673ff50 100644 --- a/src/storm/logic/FormulaVisitor.h +++ b/src/storm/logic/FormulaVisitor.h @@ -16,6 +16,7 @@ namespace storm { virtual boost::any visit(AtomicLabelFormula const& f, boost::any const& data) const = 0; virtual boost::any visit(BinaryBooleanStateFormula const& f, boost::any const& data) const = 0; virtual boost::any visit(BooleanLiteralFormula const& f, boost::any const& data) const = 0; + virtual boost::any visit(BoundedGloballyFormula const& f, boost::any const& data) const = 0; virtual boost::any visit(BoundedUntilFormula const& f, boost::any const& data) const = 0; virtual boost::any visit(ConditionalFormula const& f, boost::any const& data) const = 0; virtual boost::any visit(CumulativeRewardFormula const& f, boost::any const& data) const = 0; diff --git a/src/storm/logic/Formulas.h b/src/storm/logic/Formulas.h index f054794e7..cc59b93b6 100644 --- a/src/storm/logic/Formulas.h +++ b/src/storm/logic/Formulas.h @@ -5,6 +5,7 @@ #include "storm/logic/BinaryPathFormula.h" #include "storm/logic/BinaryStateFormula.h" #include "storm/logic/BooleanLiteralFormula.h" +#include "storm/logic/BoundedGloballyFormula.h" #include "storm/logic/BoundedUntilFormula.h" #include "storm/logic/CumulativeRewardFormula.h" #include "storm/logic/EventuallyFormula.h" diff --git a/src/storm/logic/FormulasForwardDeclarations.h b/src/storm/logic/FormulasForwardDeclarations.h index 2d1661418..1a6611f13 100644 --- a/src/storm/logic/FormulasForwardDeclarations.h +++ b/src/storm/logic/FormulasForwardDeclarations.h @@ -11,6 +11,7 @@ namespace storm { class BinaryPathFormula; class BinaryStateFormula; class BooleanLiteralFormula; + class BoundedGloballyFormula; class BoundedUntilFormula; class ConditionalFormula; class CumulativeRewardFormula; diff --git a/src/storm/logic/FragmentChecker.cpp b/src/storm/logic/FragmentChecker.cpp index 06772b6ba..df79d22a5 100644 --- a/src/storm/logic/FragmentChecker.cpp +++ b/src/storm/logic/FragmentChecker.cpp @@ -57,6 +57,16 @@ namespace storm { return inherited.getSpecification().areBooleanLiteralFormulasAllowed(); } + boost::any FragmentChecker::visit(BoundedGloballyFormula const& f, boost::any const& data) const { + InheritedInformation const& inherited = boost::any_cast(data); + bool result = inherited.getSpecification().areGloballyFormulasAllowed(); + if (!inherited.getSpecification().areNestedPathFormulasAllowed()) { + result = result && !f.getSubformula().isPathFormula(); + } + result && boost::any_cast(f.getSubformula().accept(*this, data)); + return result; + } + boost::any FragmentChecker::visit(BoundedUntilFormula const& f, boost::any const& data) const { InheritedInformation const& inherited = boost::any_cast(data); bool result = inherited.getSpecification().areBoundedUntilFormulasAllowed(); diff --git a/src/storm/logic/FragmentChecker.h b/src/storm/logic/FragmentChecker.h index c6e6100ee..0b0d179aa 100644 --- a/src/storm/logic/FragmentChecker.h +++ b/src/storm/logic/FragmentChecker.h @@ -16,6 +16,7 @@ namespace storm { 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(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; diff --git a/src/storm/logic/FragmentSpecification.cpp b/src/storm/logic/FragmentSpecification.cpp index 1e7e1f357..dc93f7f9c 100644 --- a/src/storm/logic/FragmentSpecification.cpp +++ b/src/storm/logic/FragmentSpecification.cpp @@ -68,6 +68,7 @@ namespace storm { rpatl.setUntilFormulasAllowed(true); rpatl.setGloballyFormulasAllowed(true); rpatl.setNextFormulasAllowed(true); + rpatl.setBoundedGloballyFormulasAllowed(true); return rpatl; } @@ -316,6 +317,15 @@ namespace storm { return *this; } + bool FragmentSpecification::areBoundedGloballyFormulasAllowed() const { + return boundedGloballyFormula; + } + + FragmentSpecification& FragmentSpecification::setBoundedGloballyFormulasAllowed(bool newValue) { + this->boundedGloballyFormula = newValue; + return *this; + } + bool FragmentSpecification::areAtomicExpressionFormulasAllowed() const { return atomicExpressionFormula; } diff --git a/src/storm/logic/FragmentSpecification.h b/src/storm/logic/FragmentSpecification.h index 8ac56b885..f097e940f 100644 --- a/src/storm/logic/FragmentSpecification.h +++ b/src/storm/logic/FragmentSpecification.h @@ -52,6 +52,9 @@ namespace storm { bool areBoundedUntilFormulasAllowed() const; FragmentSpecification& setBoundedUntilFormulasAllowed(bool newValue); + bool areBoundedGloballyFormulasAllowed() const; + FragmentSpecification& setBoundedGloballyFormulasAllowed(bool newValue); + bool areAtomicExpressionFormulasAllowed() const; FragmentSpecification& setAtomicExpressionFormulasAllowed(bool newValue); @@ -176,6 +179,7 @@ namespace storm { bool nextFormula; bool untilFormula; bool boundedUntilFormula; + bool boundedGloballyFormula; bool atomicExpressionFormula; bool atomicLabelFormula; diff --git a/src/storm/logic/LiftableTransitionRewardsVisitor.cpp b/src/storm/logic/LiftableTransitionRewardsVisitor.cpp index ce17bb60e..a61dccf7c 100644 --- a/src/storm/logic/LiftableTransitionRewardsVisitor.cpp +++ b/src/storm/logic/LiftableTransitionRewardsVisitor.cpp @@ -30,6 +30,24 @@ namespace storm { return true; } + boost::any LiftableTransitionRewardsVisitor::visit(BoundedGloballyFormula const& f, boost::any const& data) const { + for (unsigned i = 0; i < f.getDimension(); ++i) { + if (f.getTimeBoundReference(i).isRewardBound() && rewardModelHasTransitionRewards(f.getTimeBoundReference(i).getRewardName())) { + return false; + } + } + + bool result = true; + if (f.hasMultiDimensionalSubformulas()) { + for (unsigned i = 0; i < f.getDimension(); ++i) { + result = result && boost::any_cast(f.getSubformula(i).accept(*this, data)); + } + } else { + result = result && boost::any_cast(f.getSubformula().accept(*this, data)); + } + return result; + } + boost::any LiftableTransitionRewardsVisitor::visit(BoundedUntilFormula const& f, boost::any const& data) const { for (unsigned i = 0; i < f.getDimension(); ++i) { if (f.getTimeBoundReference(i).isRewardBound() && rewardModelHasTransitionRewards(f.getTimeBoundReference(i).getRewardName())) { diff --git a/src/storm/logic/LiftableTransitionRewardsVisitor.h b/src/storm/logic/LiftableTransitionRewardsVisitor.h index bbac6b7c2..52a791237 100644 --- a/src/storm/logic/LiftableTransitionRewardsVisitor.h +++ b/src/storm/logic/LiftableTransitionRewardsVisitor.h @@ -22,6 +22,7 @@ namespace storm { 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(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; diff --git a/src/storm/logic/ToExpressionVisitor.cpp b/src/storm/logic/ToExpressionVisitor.cpp index 8eb8444fc..1e6852d84 100644 --- a/src/storm/logic/ToExpressionVisitor.cpp +++ b/src/storm/logic/ToExpressionVisitor.cpp @@ -47,6 +47,10 @@ namespace storm { return result; } + boost::any ToExpressionVisitor::visit(BoundedGloballyFormula const&, boost::any const&) const { + STORM_LOG_THROW(false, storm::exceptions::InvalidOperationException, "Cannot assemble expression from formula that contains illegal elements."); + } + boost::any ToExpressionVisitor::visit(BoundedUntilFormula const&, boost::any const&) const { STORM_LOG_THROW(false, storm::exceptions::InvalidOperationException, "Cannot assemble expression from formula that contains illegal elements."); } diff --git a/src/storm/logic/ToExpressionVisitor.h b/src/storm/logic/ToExpressionVisitor.h index 675dbbcba..b68b5c438 100644 --- a/src/storm/logic/ToExpressionVisitor.h +++ b/src/storm/logic/ToExpressionVisitor.h @@ -16,6 +16,7 @@ namespace storm { 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(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; diff --git a/src/storm/modelchecker/AbstractModelChecker.cpp b/src/storm/modelchecker/AbstractModelChecker.cpp index be7b14ae6..803ddc711 100644 --- a/src/storm/modelchecker/AbstractModelChecker.cpp +++ b/src/storm/modelchecker/AbstractModelChecker.cpp @@ -63,7 +63,9 @@ namespace storm { template std::unique_ptr AbstractModelChecker::computeProbabilities(Environment const& env, CheckTask const& checkTask) { storm::logic::Formula const& formula = checkTask.getFormula(); - if (formula.isBoundedUntilFormula()) { + if (formula.isBoundedGloballyFormula()) { + return this->computeBoundedGloballyProbabilities(env, checkTask.substituteFormula(formula.asBoundedGloballyFormula())); + } else if (formula.isBoundedUntilFormula()) { return this->computeBoundedUntilProbabilities(env, checkTask.substituteFormula(formula.asBoundedUntilFormula())); } else if (formula.isReachabilityProbabilityFormula()) { return this->computeReachabilityProbabilities(env, checkTask.substituteFormula(formula.asReachabilityProbabilityFormula())); @@ -79,6 +81,11 @@ namespace storm { STORM_LOG_THROW(false, storm::exceptions::InvalidArgumentException, "The given formula '" << formula << "' is invalid."); } + template + std::unique_ptr AbstractModelChecker::computeBoundedGloballyProbabilities(Environment const& env, CheckTask const& checkTask) { + STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "This model checker (" << getClassName() << ") does not support the formula: " << checkTask.getFormula() << "."); + } + template std::unique_ptr AbstractModelChecker::computeBoundedUntilProbabilities(Environment const& env, CheckTask const& checkTask) { STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "This model checker (" << getClassName() << ") does not support the formula: " << checkTask.getFormula() << "."); diff --git a/src/storm/modelchecker/AbstractModelChecker.h b/src/storm/modelchecker/AbstractModelChecker.h index 59149711c..578b83f15 100644 --- a/src/storm/modelchecker/AbstractModelChecker.h +++ b/src/storm/modelchecker/AbstractModelChecker.h @@ -57,12 +57,13 @@ namespace storm { // The methods to compute probabilities for path formulas. virtual std::unique_ptr computeProbabilities(Environment const& env, CheckTask const& checkTask); virtual std::unique_ptr computeConditionalProbabilities(Environment const& env, CheckTask const& checkTask); + virtual std::unique_ptr computeBoundedGloballyProbabilities(Environment const& env, CheckTask const& checkTask); virtual std::unique_ptr computeBoundedUntilProbabilities(Environment const& env, CheckTask const& checkTask); virtual std::unique_ptr computeReachabilityProbabilities(Environment const& env, CheckTask const& checkTask); virtual std::unique_ptr computeGloballyProbabilities(Environment const& env, CheckTask const& checkTask); virtual std::unique_ptr computeNextProbabilities(Environment const& env, CheckTask const& checkTask); virtual std::unique_ptr computeUntilProbabilities(Environment const& env, CheckTask const& checkTask); - + // The methods to compute the rewards for path formulas. virtual std::unique_ptr computeRewards(Environment const& env, storm::logic::RewardMeasureType rewardMeasureType, CheckTask const& checkTask); virtual std::unique_ptr computeConditionalRewards(Environment const& env, storm::logic::RewardMeasureType rewardMeasureType, CheckTask const& checkTask); diff --git a/src/storm/modelchecker/rpatl/SparseSmgRpatlModelChecker.cpp b/src/storm/modelchecker/rpatl/SparseSmgRpatlModelChecker.cpp index 767df179e..774ef0014 100644 --- a/src/storm/modelchecker/rpatl/SparseSmgRpatlModelChecker.cpp +++ b/src/storm/modelchecker/rpatl/SparseSmgRpatlModelChecker.cpp @@ -116,6 +116,8 @@ namespace storm { return this->computeGloballyProbabilities(env, checkTask.substituteFormula(formula.asGloballyFormula())); } else if (formula.isNextFormula()) { return this->computeNextProbabilities(env, checkTask.substituteFormula(formula.asNextFormula())); + } else if (formula.isBoundedGloballyFormula()) { + return this->computeBoundedGloballyProbabilities(env, checkTask.substituteFormula(formula.asBoundedGloballyFormula())); } STORM_LOG_THROW(false, storm::exceptions::InvalidArgumentException, "The given formula '" << formula << "' is invalid."); } @@ -173,6 +175,18 @@ namespace storm { return result; } + template + std::unique_ptr SparseSmgRpatlModelChecker::computeBoundedGloballyProbabilities(Environment const& env, CheckTask const& checkTask) { + storm::logic::BoundedGloballyFormula const& pathFormula = checkTask.getFormula(); + STORM_LOG_THROW(checkTask.isOptimizationDirectionSet(), storm::exceptions::InvalidPropertyException, "Formula needs to specify whether minimal or maximal values are to be computed on nondeterministic model."); + std::unique_ptr subResultPointer = this->check(env, pathFormula.getSubformula()); + ExplicitQualitativeCheckResult const& subResult = subResultPointer->asExplicitQualitativeCheckResult(); + + auto ret = storm::modelchecker::helper::SparseSmgRpatlHelper::computeBoundedGloballyProbabilities(env, storm::solver::SolveGoal(this->getModel(), checkTask), this->getModel().getTransitionMatrix(), this->getModel().getBackwardTransitions(), subResult.getTruthValuesVector(), checkTask.isQualitativeSet(), statesOfCoalition, checkTask.isProduceSchedulersSet(), checkTask.getHint(), pathFormula.getNonStrictLowerBound(), pathFormula.getNonStrictUpperBound()); + std::unique_ptr result(new ExplicitQuantitativeCheckResult(std::move(ret.values))); + return result; + } + template std::unique_ptr SparseSmgRpatlModelChecker::computeLongRunAverageProbabilities(Environment const& env, CheckTask const& checkTask) { STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "NYI"); diff --git a/src/storm/modelchecker/rpatl/SparseSmgRpatlModelChecker.h b/src/storm/modelchecker/rpatl/SparseSmgRpatlModelChecker.h index 28b25f9e6..a27e580c5 100644 --- a/src/storm/modelchecker/rpatl/SparseSmgRpatlModelChecker.h +++ b/src/storm/modelchecker/rpatl/SparseSmgRpatlModelChecker.h @@ -39,6 +39,7 @@ namespace storm { std::unique_ptr computeUntilProbabilities(Environment const& env, CheckTask const& checkTask) override; std::unique_ptr computeGloballyProbabilities(Environment const& env, CheckTask const& checkTask) override; std::unique_ptr computeNextProbabilities(Environment const& env, CheckTask const& checkTask) override; + std::unique_ptr computeBoundedGloballyProbabilities(Environment const& env, CheckTask const& checkTask) override; std::unique_ptr computeLongRunAverageProbabilities(Environment const& env, CheckTask const& checkTask) override; std::unique_ptr computeLongRunAverageRewards(Environment const& env, storm::logic::RewardMeasureType rewardMeasureType, CheckTask const& checkTask) override; diff --git a/src/storm/modelchecker/rpatl/helper/SparseSmgRpatlHelper.cpp b/src/storm/modelchecker/rpatl/helper/SparseSmgRpatlHelper.cpp index 779392a3e..ca6e53ea2 100644 --- a/src/storm/modelchecker/rpatl/helper/SparseSmgRpatlHelper.cpp +++ b/src/storm/modelchecker/rpatl/helper/SparseSmgRpatlHelper.cpp @@ -7,7 +7,7 @@ #include "storm/utility/vector.h" #include "storm/modelchecker/rpatl/helper/internal/GameViHelper.h" - +#include "storm/modelchecker/rpatl/helper/internal/BoundedGloballyGameViHelper.h" namespace storm { namespace modelchecker { @@ -106,6 +106,50 @@ namespace storm { return MDPSparseModelCheckingHelperReturnType(std::move(x)); } + template + MDPSparseModelCheckingHelperReturnType SparseSmgRpatlHelper::computeBoundedGloballyProbabilities(Environment const& env, storm::solver::SolveGoal&& goal, storm::storage::SparseMatrix const& transitionMatrix, storm::storage::SparseMatrix const& backwardTransitions, storm::storage::BitVector const& psiStates, bool qualitative, storm::storage::BitVector statesOfCoalition, bool produceScheduler, ModelCheckerHint const& hint,uint64_t lowerBound, uint64_t upperBound) { + auto solverEnv = env; + solverEnv.solver().minMax().setMethod(storm::solver::MinMaxMethod::ValueIteration, false); + + // Relevant states are safe states - the psiStates. + storm::storage::BitVector relevantStates = psiStates; + + // Initialize the solution vector. + std::vector x = std::vector(relevantStates.getNumberOfSetBits(), storm::utility::one()); + + // Reduce the matrix to relevant states + storm::storage::SparseMatrix submatrix = transitionMatrix.getSubmatrix(true, relevantStates, relevantStates, false); + + std::vector constrainedChoiceValues = std::vector(submatrix.getRowCount(), storm::utility::zero()); + + storm::storage::BitVector clippedStatesOfCoalition(relevantStates.getNumberOfSetBits()); + clippedStatesOfCoalition.setClippedStatesOfCoalition(relevantStates, statesOfCoalition); + clippedStatesOfCoalition.complement(); + + // Use the bounded globally game vi helper + storm::modelchecker::helper::internal::BoundedGloballyGameViHelper viHelper(submatrix, clippedStatesOfCoalition); + std::unique_ptr> scheduler; + if (produceScheduler) { + viHelper.setProduceScheduler(true); + } + + // in case of upperBound = 0 the states which are initially "safe" are filled with ones + if(upperBound > 0) + { + viHelper.performValueIteration(env, x, goal.direction(), upperBound, constrainedChoiceValues); +/* if (produceScheduler) { + scheduler = std::make_unique>(expandScheduler(viHelper.extractScheduler(), relevantStates, ~relevantStates)); + + }*/ + } + + viHelper.fillResultVector(x, relevantStates); + + STORM_LOG_DEBUG("x = " << x); + + return MDPSparseModelCheckingHelperReturnType(std::move(x), std::move(scheduler)); + } + template class SparseSmgRpatlHelper; #ifdef STORM_HAVE_CARL template class SparseSmgRpatlHelper; diff --git a/src/storm/modelchecker/rpatl/helper/SparseSmgRpatlHelper.h b/src/storm/modelchecker/rpatl/helper/SparseSmgRpatlHelper.h index 119eec84a..e6a36f2af 100644 --- a/src/storm/modelchecker/rpatl/helper/SparseSmgRpatlHelper.h +++ b/src/storm/modelchecker/rpatl/helper/SparseSmgRpatlHelper.h @@ -39,6 +39,7 @@ namespace storm { static MDPSparseModelCheckingHelperReturnType computeUntilProbabilities(Environment const& env, storm::solver::SolveGoal&& goal, storm::storage::SparseMatrix const& transitionMatrix, storm::storage::SparseMatrix const& backwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, bool qualitative, storm::storage::BitVector statesOfCoalition, bool produceScheduler, ModelCheckerHint const& hint = ModelCheckerHint()); static MDPSparseModelCheckingHelperReturnType computeGloballyProbabilities(Environment const& env, storm::solver::SolveGoal&& goal, storm::storage::SparseMatrix const& transitionMatrix, storm::storage::SparseMatrix const& backwardTransitions, storm::storage::BitVector const& psiStates, bool qualitative, storm::storage::BitVector statesOfCoalition, bool produceScheduler, ModelCheckerHint const& hint = ModelCheckerHint()); static MDPSparseModelCheckingHelperReturnType computeNextProbabilities(Environment const& env, storm::solver::SolveGoal&& goal, storm::storage::SparseMatrix const& transitionMatrix, storm::storage::SparseMatrix const& backwardTransitions, storm::storage::BitVector const& psiStates, bool qualitative, storm::storage::BitVector statesOfCoalition, bool produceScheduler, ModelCheckerHint const& hint); + static MDPSparseModelCheckingHelperReturnType computeBoundedGloballyProbabilities(Environment const& env, storm::solver::SolveGoal&& goal, storm::storage::SparseMatrix const& transitionMatrix, storm::storage::SparseMatrix const& backwardTransitions, storm::storage::BitVector const& psiStates, bool qualitative, storm::storage::BitVector statesOfCoalition, bool produceScheduler, ModelCheckerHint const& hint, uint64_t lowerBound, uint64_t upperBound); private: static storm::storage::Scheduler expandScheduler(storm::storage::Scheduler scheduler, storm::storage::BitVector psiStates, storm::storage::BitVector notPhiStates); diff --git a/src/storm/modelchecker/rpatl/helper/internal/BoundedGloballyGameViHelper.cpp b/src/storm/modelchecker/rpatl/helper/internal/BoundedGloballyGameViHelper.cpp new file mode 100644 index 000000000..9a4db040e --- /dev/null +++ b/src/storm/modelchecker/rpatl/helper/internal/BoundedGloballyGameViHelper.cpp @@ -0,0 +1,117 @@ +#include "BoundedGloballyGameViHelper.h" + +#include "storm/environment/Environment.h" +#include "storm/environment/solver/SolverEnvironment.h" +#include "storm/environment/solver/GameSolverEnvironment.h" + +#include "storm/utility/SignalHandler.h" +#include "storm/utility/vector.h" + +namespace storm { + namespace modelchecker { + namespace helper { + namespace internal { + + template + BoundedGloballyGameViHelper::BoundedGloballyGameViHelper(storm::storage::SparseMatrix const& transitionMatrix, storm::storage::BitVector statesOfCoalition) : _transitionMatrix(transitionMatrix), _statesOfCoalition(statesOfCoalition) { + } + + template + void BoundedGloballyGameViHelper::prepareSolversAndMultipliers(const Environment& env) { + _multiplier = storm::solver::MultiplierFactory().create(env, _transitionMatrix); + } + + template + void BoundedGloballyGameViHelper::performValueIteration(Environment const& env, std::vector& x, storm::solver::OptimizationDirection const dir, uint64_t upperBound, std::vector& constrainedChoiceValues) { + prepareSolversAndMultipliers(env); + _x = x; + + if (this->isProduceSchedulerSet()) { + if (!this->_producedOptimalChoices.is_initialized()) { + this->_producedOptimalChoices.emplace(); + } + this->_producedOptimalChoices->resize(this->_transitionMatrix.getRowGroupCount()); + } + + for (uint64_t iter = 0; iter < upperBound; iter++) { + if(iter == upperBound - 1) { + _multiplier->multiply(env, _x, nullptr, constrainedChoiceValues); + } + performIterationStep(env, dir); + } + + x = _x; + } + + template + void BoundedGloballyGameViHelper::performIterationStep(Environment const& env, storm::solver::OptimizationDirection const dir, std::vector* choices) { + if (!_multiplier) { + prepareSolversAndMultipliers(env); + } + + // multiplyandreducegaussseidel + // Ax = x' + if (choices == nullptr) { + _multiplier->multiplyAndReduce(env, dir, _x, nullptr, _x, nullptr, &_statesOfCoalition); + } else { + // Also keep track of the choices made. + _multiplier->multiplyAndReduce(env, dir, _x, nullptr, _x, choices, &_statesOfCoalition); + } + } + + template + void BoundedGloballyGameViHelper::fillResultVector(std::vector& result, storm::storage::BitVector psiStates) + { + std::vector filledVector = std::vector(psiStates.size(), storm::utility::zero()); + uint bitIndex = 0; + for(uint i = 0; i < filledVector.size(); i++) { + if (psiStates.get(i)) { + filledVector.at(i) = result.at(bitIndex); + bitIndex++; + } + } + result = filledVector; + } + + template + void BoundedGloballyGameViHelper::setProduceScheduler(bool value) { + _produceScheduler = value; + } + + template + bool BoundedGloballyGameViHelper::isProduceSchedulerSet() const { + return _produceScheduler; + } + + template + std::vector const& BoundedGloballyGameViHelper::getProducedOptimalChoices() const { + STORM_LOG_ASSERT(this->isProduceSchedulerSet(), "Trying to get the produced optimal choices although no scheduler was requested."); + STORM_LOG_ASSERT(this->_producedOptimalChoices.is_initialized(), "Trying to get the produced optimal choices but none were available. Was there a computation call before?"); + return this->_producedOptimalChoices.get(); + } + + template + std::vector& BoundedGloballyGameViHelper::getProducedOptimalChoices() { + STORM_LOG_ASSERT(this->isProduceSchedulerSet(), "Trying to get the produced optimal choices although no scheduler was requested."); + STORM_LOG_ASSERT(this->_producedOptimalChoices.is_initialized(), "Trying to get the produced optimal choices but none were available. Was there a computation call before?"); + return this->_producedOptimalChoices.get(); + } + + template + storm::storage::Scheduler BoundedGloballyGameViHelper::extractScheduler() const{ + auto const& optimalChoices = getProducedOptimalChoices(); + storm::storage::Scheduler scheduler(optimalChoices.size()); + for (uint64_t state = 0; state < optimalChoices.size(); ++state) { + scheduler.setChoice(optimalChoices[state], state); + } + return scheduler; + } + + template class BoundedGloballyGameViHelper; +#ifdef STORM_HAVE_CARL + template class BoundedGloballyGameViHelper; +#endif + } + } + } +} diff --git a/src/storm/modelchecker/rpatl/helper/internal/BoundedGloballyGameViHelper.h b/src/storm/modelchecker/rpatl/helper/internal/BoundedGloballyGameViHelper.h new file mode 100644 index 000000000..d2eb985dc --- /dev/null +++ b/src/storm/modelchecker/rpatl/helper/internal/BoundedGloballyGameViHelper.h @@ -0,0 +1,71 @@ +#pragma once + +#include "storm/storage/SparseMatrix.h" +#include "storm/solver/LinearEquationSolver.h" +#include "storm/solver/MinMaxLinearEquationSolver.h" +#include "storm/solver/Multiplier.h" + +namespace storm { + class Environment; + + namespace storage { + template class Scheduler; + } + + namespace modelchecker { + namespace helper { + namespace internal { + + template + class BoundedGloballyGameViHelper { + public: + BoundedGloballyGameViHelper(storm::storage::SparseMatrix const& transitionMatrix, storm::storage::BitVector statesOfCoalition); + + void prepareSolversAndMultipliers(const Environment& env); + + void performValueIteration(Environment const& env, std::vector& x, storm::solver::OptimizationDirection const dir, uint64_t upperBound, std::vector& constrainedChoiceValues); + + /*! + * Fills the result vector to the original size with ones for being psiStates, zeros for being not phiStates + */ + void fillResultVector(std::vector& result, storm::storage::BitVector psiStates); + + /*! + * Sets whether an optimal scheduler shall be constructed during the computation + */ + void setProduceScheduler(bool value); + + /*! + * @return whether an optimal scheduler shall be constructed during the computation + */ + bool isProduceSchedulerSet() const; + + storm::storage::Scheduler extractScheduler() const; + + private: + void performIterationStep(Environment const& env, storm::solver::OptimizationDirection const dir, std::vector* choices = nullptr); + + /*! + * @pre before calling this, a computation call should have been performed during which scheduler production was enabled. + * @return the produced scheduler of the most recent call. + */ + std::vector const& getProducedOptimalChoices() const; + + /*! + * @pre before calling this, a computation call should have been performed during which scheduler production was enabled. + * @return the produced scheduler of the most recent call. + */ + std::vector& getProducedOptimalChoices(); + + storm::storage::SparseMatrix _transitionMatrix; + storm::storage::BitVector _statesOfCoalition; + std::vector _x; + std::unique_ptr> _multiplier; + + bool _produceScheduler = false; + boost::optional> _producedOptimalChoices; + }; + } + } + } +} diff --git a/src/storm/modelchecker/rpatl/helper/internal/GameViHelper.cpp b/src/storm/modelchecker/rpatl/helper/internal/GameViHelper.cpp index 8c354d945..e0fd4eee8 100644 --- a/src/storm/modelchecker/rpatl/helper/internal/GameViHelper.cpp +++ b/src/storm/modelchecker/rpatl/helper/internal/GameViHelper.cpp @@ -20,7 +20,7 @@ namespace storm { } template - void GameViHelper::prepareSolversAndMultipliersReachability(const Environment& env) { + void GameViHelper::prepareSolversAndMultipliers(const Environment& env) { // TODO we get whole transitionmatrix and psistates DONE IN smgrpatlhelper // -> clip statesofcoalition // -> compute b vector from psiStates @@ -32,7 +32,7 @@ namespace storm { template void GameViHelper::performValueIteration(Environment const& env, std::vector& x, std::vector b, storm::solver::OptimizationDirection const dir) { - prepareSolversAndMultipliersReachability(env); + prepareSolversAndMultipliers(env); ValueType precision = storm::utility::convertNumber(env.solver().game().getPrecision()); uint64_t maxIter = env.solver().game().getMaximalNumberOfIterations(); _b = b; @@ -71,7 +71,7 @@ namespace storm { template void GameViHelper::performIterationStep(Environment const& env, storm::solver::OptimizationDirection const dir, std::vector* choices) { if (!_multiplier) { - prepareSolversAndMultipliersReachability(env); + prepareSolversAndMultipliers(env); } _x1IsCurrent = !_x1IsCurrent; diff --git a/src/storm/modelchecker/rpatl/helper/internal/GameViHelper.h b/src/storm/modelchecker/rpatl/helper/internal/GameViHelper.h index d46f9049c..3a1343f90 100644 --- a/src/storm/modelchecker/rpatl/helper/internal/GameViHelper.h +++ b/src/storm/modelchecker/rpatl/helper/internal/GameViHelper.h @@ -21,7 +21,7 @@ namespace storm { public: GameViHelper(storm::storage::SparseMatrix const& transitionMatrix, storm::storage::BitVector statesOfCoalition); - void prepareSolversAndMultipliersReachability(const Environment& env); + void prepareSolversAndMultipliers(const Environment& env); void performValueIteration(Environment const& env, std::vector& x, std::vector b, storm::solver::OptimizationDirection const dir); @@ -30,7 +30,7 @@ namespace storm { */ void fillResultVector(std::vector& result, storm::storage::BitVector relevantStates, storm::storage::BitVector psiStates); - /*h + /*! * Sets whether an optimal scheduler shall be constructed during the computation */ void setProduceScheduler(bool value); diff --git a/src/storm/storage/jani/JSONExporter.cpp b/src/storm/storage/jani/JSONExporter.cpp index 586c81051..7de2329b7 100644 --- a/src/storm/storage/jani/JSONExporter.cpp +++ b/src/storm/storage/jani/JSONExporter.cpp @@ -212,6 +212,54 @@ namespace storm { ExportJsonType opDecl(f.isTrueFormula() ? true : false); return opDecl; } + boost::any FormulaToJaniJson::visit(storm::logic::BoundedGloballyFormula const& f, boost::any const& data) const { + STORM_LOG_THROW(!f.hasMultiDimensionalSubformulas(), storm::exceptions::NotSupportedException, "Jani export of multi-dimensional bounded globally formulas is not supported."); + ExportJsonType opDecl; + opDecl["op"] = "G"; + opDecl["exp"] = anyToJson(f.getSubformula().accept(*this, data)); + + bool hasStepBounds(false), hasTimeBounds(false); + std::vector rewardBounds; + + for (uint64_t i = 0; i < f.getDimension(); ++i) { + boost::optional lower, upper; + boost::optional lowerExclusive, upperExclusive; + if (f.hasLowerBound(i)) { + lower = f.getLowerBound(i); + lowerExclusive = f.isLowerBoundStrict(i); + } + if (f.hasUpperBound(i)) { + upper = f.getUpperBound(i); + upperExclusive = f.isUpperBoundStrict(i); + } + ExportJsonType propertyInterval = constructPropertyInterval(lower, lowerExclusive, upper, upperExclusive); + + auto tbr = f.getTimeBoundReference(i); + if (tbr.isStepBound() || (model.isDiscreteTimeModel() && tbr.isTimeBound())) { + STORM_LOG_THROW(!hasStepBounds, storm::exceptions::NotSupportedException, "Jani export of bounded globally formulas with multiple step bounds is not supported."); + hasStepBounds = true; + opDecl["step-bounds"] = propertyInterval; + } else if(tbr.isRewardBound()) { + ExportJsonType rewbound; + rewbound["exp"] = buildExpression(model.getRewardModelExpression(tbr.getRewardName()), model.getConstants(), model.getGlobalVariables()); + if (tbr.hasRewardAccumulation()) { + rewbound["accumulate"] = constructRewardAccumulation(tbr.getRewardAccumulation(), tbr.getRewardName()); + } else { + rewbound["accumulate"] = constructStandardRewardAccumulation(tbr.getRewardName()); + } + rewbound["bounds"] = propertyInterval; + rewardBounds.push_back(std::move(rewbound)); + } else { + STORM_LOG_THROW(!hasTimeBounds, storm::exceptions::NotSupportedException, "Jani export of bounded globally formulas with multiple time bounds is not supported."); + hasTimeBounds = true; + opDecl["time-bounds"] = propertyInterval; + } + } + if (!rewardBounds.empty()) { + opDecl["reward-bounds"] = ExportJsonType(rewardBounds); + } + return opDecl; + } boost::any FormulaToJaniJson::visit(storm::logic::BoundedUntilFormula const& f, boost::any const& data) const { STORM_LOG_THROW(!f.hasMultiDimensionalSubformulas(), storm::exceptions::NotSupportedException, "Jani export of multi-dimensional bounded until formulas is not supported."); ExportJsonType opDecl; diff --git a/src/storm/storage/jani/JSONExporter.h b/src/storm/storage/jani/JSONExporter.h index 9408cff82..437c10c6c 100644 --- a/src/storm/storage/jani/JSONExporter.h +++ b/src/storm/storage/jani/JSONExporter.h @@ -52,6 +52,7 @@ namespace storm { virtual boost::any visit(storm::logic::AtomicLabelFormula const& f, boost::any const& data) const; virtual boost::any visit(storm::logic::BinaryBooleanStateFormula const& f, boost::any const& data) const; virtual boost::any visit(storm::logic::BooleanLiteralFormula const& f, boost::any const& data) const; + virtual boost::any visit(storm::logic::BoundedGloballyFormula const& f, boost::any const& data) const; virtual boost::any visit(storm::logic::BoundedUntilFormula const& f, boost::any const& data) const; virtual boost::any visit(storm::logic::ConditionalFormula const& f, boost::any const& data) const; virtual boost::any visit(storm::logic::CumulativeRewardFormula const& f, boost::any const& data) const;