From 8b466f1fa742f7836916e158904866237f3c7dd8 Mon Sep 17 00:00:00 2001 From: TimQu Date: Mon, 11 Sep 2017 15:28:36 +0200 Subject: [PATCH] extended multidimensional bounded until formulas to have different subformulas in each dimension --- src/storm/logic/BoundedUntilFormula.cpp | 190 +++++++++++++----- src/storm/logic/BoundedUntilFormula.h | 23 ++- src/storm/logic/CloneVisitor.cpp | 30 ++- src/storm/logic/FormulaInformationVisitor.cpp | 13 +- src/storm/logic/FragmentChecker.cpp | 42 ++-- src/storm/logic/FragmentSpecification.cpp | 15 +- src/storm/logic/FragmentSpecification.h | 4 + .../logic/VariableSubstitutionVisitor.cpp | 37 ++-- ...dpRewardBoundedPcaaWeightVectorChecker.cpp | 2 +- src/storm/parser/FormulaParserGrammar.cpp | 46 ++++- src/storm/parser/FormulaParserGrammar.h | 4 +- src/test/storm/logic/FragmentCheckerTest.cpp | 6 +- 12 files changed, 307 insertions(+), 105 deletions(-) diff --git a/src/storm/logic/BoundedUntilFormula.cpp b/src/storm/logic/BoundedUntilFormula.cpp index 5dca64e2b..3b2f2999b 100644 --- a/src/storm/logic/BoundedUntilFormula.cpp +++ b/src/storm/logic/BoundedUntilFormula.cpp @@ -11,20 +11,26 @@ 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) : PathFormula(), leftSubformula({leftSubformula}), rightSubformula({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) { + + BoundedUntilFormula::BoundedUntilFormula(std::shared_ptr const& leftSubformula, std::shared_ptr const& rightSubformula,std::vector> const& lowerBounds, std::vector> const& upperBounds, std::vector const& timeBoundReferences) : PathFormula(), leftSubformula({leftSubformula}), rightSubformula({rightSubformula}), timeBoundReference(timeBoundReferences), lowerBound(lowerBounds), upperBound(upperBounds) { assert(timeBoundReferences.size() == upperBound.size()); assert(timeBoundReferences.size() == lowerBound.size()); + } + + BoundedUntilFormula::BoundedUntilFormula(std::vector> const& leftSubformulas, std::vector> const& rightSubformulas, std::vector> const& lowerBounds, std::vector> const& upperBounds, std::vector const& timeBoundReferences) : PathFormula(), leftSubformula(leftSubformulas), rightSubformula(rightSubformulas), timeBoundReference(timeBoundReferences), lowerBound(lowerBounds), upperBound(upperBounds) { + assert(leftSubformula.size() == rightSubformula.size()); + assert(rightSubformula.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) { + 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; } @@ -37,32 +43,101 @@ namespace storm { return visitor.visit(*this, data); } + void BoundedUntilFormula::gatherAtomicExpressionFormulas(std::vector>& atomicExpressionFormulas) const { + if (hasMultiDimensionalSubformulas()) { + for (unsigned i = 0; i < this->getDimension(); ++i) { + this->getLeftSubformula(i).gatherAtomicExpressionFormulas(atomicExpressionFormulas); + this->getRightSubformula(i).gatherAtomicExpressionFormulas(atomicExpressionFormulas); + } + } else { + this->getLeftSubformula().gatherAtomicExpressionFormulas(atomicExpressionFormulas); + this->getRightSubformula().gatherAtomicExpressionFormulas(atomicExpressionFormulas); + } + } + + void BoundedUntilFormula::gatherAtomicLabelFormulas(std::vector>& atomicLabelFormulas) const { + if (hasMultiDimensionalSubformulas()) { + for (unsigned i = 0; i < this->getDimension(); ++i) { + this->getLeftSubformula(i).gatherAtomicLabelFormulas(atomicLabelFormulas); + this->getRightSubformula(i).gatherAtomicLabelFormulas(atomicLabelFormulas); + } + } else { + this->getLeftSubformula().gatherAtomicLabelFormulas(atomicLabelFormulas); + this->getRightSubformula().gatherAtomicLabelFormulas(atomicLabelFormulas); + } + } + void BoundedUntilFormula::gatherReferencedRewardModels(std::set& referencedRewardModels) const { for (unsigned i = 0; i < this->getDimension(); ++i) { if (this->getTimeBoundReference(i).isRewardBound()) { - referencedRewardModels.insert(this->getTimeBoundReference().getRewardName()); + referencedRewardModels.insert(this->getTimeBoundReference(i).getRewardName()); } } - - this->getLeftSubformula().gatherReferencedRewardModels(referencedRewardModels); - this->getRightSubformula().gatherReferencedRewardModels(referencedRewardModels); + if (hasMultiDimensionalSubformulas()) { + for (unsigned i = 0; i < this->getDimension(); ++i) { + this->getLeftSubformula(i).gatherReferencedRewardModels(referencedRewardModels); + this->getRightSubformula(i).gatherReferencedRewardModels(referencedRewardModels); + } + } else { + this->getLeftSubformula().gatherReferencedRewardModels(referencedRewardModels); + this->getRightSubformula().gatherReferencedRewardModels(referencedRewardModels); + } } + bool BoundedUntilFormula::hasQualitativeResult() const { + return false; + } - TimeBoundReference const& BoundedUntilFormula::getTimeBoundReference(unsigned i) const { - assert(i < timeBoundReference.size()); - return timeBoundReference.at(i); + bool BoundedUntilFormula::hasQuantitativeResult() const { + return true; } bool BoundedUntilFormula::isMultiDimensional() const { assert(timeBoundReference.size() != 0); return timeBoundReference.size() > 1; } + + bool BoundedUntilFormula::hasMultiDimensionalSubformulas() const { + assert(leftSubformula.size() != 0); + assert(leftSubformula.size() == rightSubformula.size()); + return leftSubformula.size() > 1; + } unsigned BoundedUntilFormula::getDimension() const { return timeBoundReference.size(); } + Formula const& BoundedUntilFormula::getLeftSubformula() const { + STORM_LOG_ASSERT(leftSubformula.size() == 1, "The left subformula is not unique."); + return *leftSubformula.at(0); + } + + Formula const& BoundedUntilFormula::getLeftSubformula(unsigned i) const { + if (leftSubformula.size() == 1 && i < getDimension()) { + return getLeftSubformula(); + } else { + return *leftSubformula.at(i); + } + } + + Formula const& BoundedUntilFormula::getRightSubformula() const { + STORM_LOG_ASSERT(leftSubformula.size() == 1, "The right subformula is not unique."); + return *rightSubformula.at(0); + } + + Formula const& BoundedUntilFormula::getRightSubformula(unsigned i) const { + if (rightSubformula.size() == 1 && i < getDimension()) { + return getRightSubformula(); + } else { + return *rightSubformula.at(i); + } + } + + TimeBoundReference const& BoundedUntilFormula::getTimeBoundReference(unsigned i) const { + assert(i < timeBoundReference.size()); + return timeBoundReference.at(i); + } + bool BoundedUntilFormula::isLowerBoundStrict(unsigned i) const { assert(i < lowerBound.size()); return lowerBound.at(i).get().isStrict(); @@ -185,58 +260,69 @@ namespace storm { } std::shared_ptr BoundedUntilFormula::restrictToDimension(unsigned i) const { - return std::make_shared(this->getLeftSubformula().asSharedPointer(), this->getRightSubformula().asSharedPointer(), lowerBound.at(i), upperBound.at(i), this->getTimeBoundReference(i)); + return std::make_shared(getLeftSubformula(i).asSharedPointer(), getRightSubformula(i).asSharedPointer(), lowerBound.at(i), upperBound.at(i), getTimeBoundReference(i)); } std::ostream& BoundedUntilFormula::writeToStream(std::ostream& out) const { - this->getLeftSubformula().writeToStream(out); - - out << " U"; - if (this->isMultiDimensional()) { - out << "["; - } - for(unsigned i = 0; i < this->getDimension(); ++i) { - if (i > 0) { - out << ","; + if (hasMultiDimensionalSubformulas()) { + out << "multi("; + restrictToDimension(0)->writeToStream(out); + for (unsigned i = 1; i < this->getDimension(); ++i) { + out << ", "; + restrictToDimension(i)->writeToStream(out); } - if (this->getTimeBoundReference(i).isRewardBound()) { - out << "{\"" << this->getTimeBoundReference(i).getRewardName() << "\"}"; + out << ")"; + } else { + + this->getLeftSubformula().writeToStream(out); + + out << " U"; + if (this->isMultiDimensional()) { + out << "["; } - 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 << ")"; + 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(i)) { - out << ">"; + if (this->isUpperBoundStrict(i)) { + out << "<"; } else { - out << ">="; + out << "<="; } - out << getLowerBound(i); - } - } else { - if (this->isUpperBoundStrict(i)) { - out << "<"; - } else { - out << "<="; + out << this->getUpperBound(i); } - out << this->getUpperBound(i); + out << " "; + } + if (this->isMultiDimensional()) { + out << "]"; } - out << " "; - } - if (this->isMultiDimensional()) { - out << "]"; } diff --git a/src/storm/logic/BoundedUntilFormula.h b/src/storm/logic/BoundedUntilFormula.h index 6b31301ac..eed5c5220 100644 --- a/src/storm/logic/BoundedUntilFormula.h +++ b/src/storm/logic/BoundedUntilFormula.h @@ -9,10 +9,11 @@ namespace storm { namespace logic { - class BoundedUntilFormula : public BinaryPathFormula { + class BoundedUntilFormula : public PathFormula { 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); + BoundedUntilFormula(std::vector> const& leftSubformulas, std::vector> const& rightSubformulas, std::vector> const& lowerBounds, std::vector> const& upperBounds, std::vector const& timeBoundReferences); virtual bool isBoundedUntilFormula() const override; @@ -20,10 +21,23 @@ namespace storm { virtual boost::any accept(FormulaVisitor const& visitor, boost::any const& data) const override; + virtual void gatherAtomicExpressionFormulas(std::vector>& atomicExpressionFormulas) const override; + virtual void gatherAtomicLabelFormulas(std::vector>& atomicLabelFormulas) const override; virtual void gatherReferencedRewardModels(std::set& referencedRewardModels) const override; + virtual bool hasQualitativeResult() const override; + virtual bool hasQuantitativeResult() const override; + + bool isMultiDimensional() const; + bool hasMultiDimensionalSubformulas() const; + unsigned getDimension() const; + + Formula const& getLeftSubformula() const; + Formula const& getLeftSubformula(unsigned i) const; + Formula const& getRightSubformula() const; + Formula const& getRightSubformula(unsigned i) const; + TimeBoundReference const& getTimeBoundReference(unsigned i = 0) const; - bool isLowerBoundStrict(unsigned i = 0) const; bool hasLowerBound() const; @@ -35,9 +49,6 @@ namespace storm { bool hasUpperBound(unsigned i) const; bool hasIntegerUpperBound(unsigned i = 0) const; - bool isMultiDimensional() const; - unsigned getDimension() const; - storm::expressions::Expression const& getLowerBound(unsigned i = 0) const; storm::expressions::Expression const& getUpperBound(unsigned i = 0) const; @@ -57,6 +68,8 @@ namespace storm { private: static void checkNoVariablesInBound(storm::expressions::Expression const& bound); + std::vector> leftSubformula; + std::vector> rightSubformula; std::vector timeBoundReference; std::vector> lowerBound; std::vector> upperBound; diff --git a/src/storm/logic/CloneVisitor.cpp b/src/storm/logic/CloneVisitor.cpp index e19d9477d..d97dd41d6 100644 --- a/src/storm/logic/CloneVisitor.cpp +++ b/src/storm/logic/CloneVisitor.cpp @@ -29,9 +29,33 @@ namespace storm { } boost::any CloneVisitor::visit(BoundedUntilFormula const& f, boost::any const& data) const { - std::shared_ptr left = boost::any_cast>(f.getLeftSubformula().accept(*this, data)); - std::shared_ptr right = boost::any_cast>(f.getRightSubformula().accept(*this, data)); - return std::static_pointer_cast(std::make_shared(f)); + 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> leftSubformulas, rightSubformulas; + for (uint64_t i = 0; i < f.getDimension(); ++i) { + leftSubformulas.push_back(boost::any_cast>(f.getLeftSubformula(i).accept(*this, data))); + rightSubformulas.push_back(boost::any_cast>(f.getRightSubformula(i).accept(*this, data))); + } + return std::static_pointer_cast(std::make_shared(leftSubformulas, rightSubformulas, lowerBounds, upperBounds, timeBoundReferences)); + } else { + std::shared_ptr left = boost::any_cast>(f.getLeftSubformula().accept(*this, data)); + std::shared_ptr right = boost::any_cast>(f.getRightSubformula().accept(*this, data)); + return std::static_pointer_cast(std::make_shared(left, right, lowerBounds, upperBounds, timeBoundReferences)); + } } boost::any CloneVisitor::visit(ConditionalFormula const& f, boost::any const& data) const { diff --git a/src/storm/logic/FormulaInformationVisitor.cpp b/src/storm/logic/FormulaInformationVisitor.cpp index 319fbf2f8..08cd7ffaf 100644 --- a/src/storm/logic/FormulaInformationVisitor.cpp +++ b/src/storm/logic/FormulaInformationVisitor.cpp @@ -26,7 +26,18 @@ namespace storm { } boost::any FormulaInformationVisitor::visit(BoundedUntilFormula const& f, boost::any const& data) const { - return boost::any_cast(f.getLeftSubformula().accept(*this, data)).join(boost::any_cast(f.getRightSubformula().accept(*this))).setContainsBoundedUntilFormula(); + FormulaInformation result; + result.setContainsBoundedUntilFormula(true); + if (f.hasMultiDimensionalSubformulas()) { + for (unsigned i = 0; i < f.getDimension(); ++i){ + result.join(boost::any_cast(f.getLeftSubformula(i).accept(*this, data))); + result.join(boost::any_cast(f.getRightSubformula(i).accept(*this, data))); + } + } else { + result.join(boost::any_cast(f.getLeftSubformula().accept(*this, data))); + result.join(boost::any_cast(f.getRightSubformula().accept(*this, data))); + } + return result; } boost::any FormulaInformationVisitor::visit(ConditionalFormula const& f, boost::any const& data) const { diff --git a/src/storm/logic/FragmentChecker.cpp b/src/storm/logic/FragmentChecker.cpp index 63a6ffd78..59514a884 100644 --- a/src/storm/logic/FragmentChecker.cpp +++ b/src/storm/logic/FragmentChecker.cpp @@ -57,21 +57,39 @@ namespace storm { boost::any FragmentChecker::visit(BoundedUntilFormula const& f, boost::any const& data) const { InheritedInformation const& inherited = boost::any_cast(data); bool result = inherited.getSpecification().areBoundedUntilFormulasAllowed(); - if (!inherited.getSpecification().areNestedPathFormulasAllowed()) { - result = result && !f.getLeftSubformula().isPathFormula(); - result = result && !f.getRightSubformula().isPathFormula(); + if (f.isMultiDimensional()) { + result = result && inherited.getSpecification().areMultiDimensionalBoundedUntilFormulasAllowed(); + } + + for (uint64_t i = 0; i < f.getDimension(); ++i) { + auto tbr = f.getTimeBoundReference(i); + if (tbr.isStepBound()) { + result = result && inherited.getSpecification().areStepBoundedUntilFormulasAllowed(); + } else if(tbr.isTimeBound()) { + result = result && inherited.getSpecification().areTimeBoundedUntilFormulasAllowed(); + } else { + assert(tbr.isRewardBound()); + result = result && inherited.getSpecification().areRewardBoundedUntilFormulasAllowed(); + } } - auto tbr = f.getTimeBoundReference(); - if (tbr.isStepBound()) { - result = result && inherited.getSpecification().areStepBoundedUntilFormulasAllowed(); - } else if(tbr.isTimeBound()) { - result = result && inherited.getSpecification().areTimeBoundedUntilFormulasAllowed(); + + if (f.hasMultiDimensionalSubformulas()) { + for (uint64_t i = 0; i < f.getDimension(); ++i) { + if (!inherited.getSpecification().areNestedPathFormulasAllowed()) { + result = result && !f.getLeftSubformula(i).isPathFormula(); + result = result && !f.getRightSubformula(i).isPathFormula(); + } + result = result && boost::any_cast(f.getLeftSubformula(i).accept(*this, data)); + result = result && boost::any_cast(f.getRightSubformula(i).accept(*this, data)); + } } else { - assert(tbr.isRewardBound()); - result = result && inherited.getSpecification().areRewardBoundedUntilFormulasAllowed(); + if (!inherited.getSpecification().areNestedPathFormulasAllowed()) { + result = result && !f.getLeftSubformula().isPathFormula(); + result = result && !f.getRightSubformula().isPathFormula(); + } + result = result && boost::any_cast(f.getLeftSubformula().accept(*this, data)); + result = result && boost::any_cast(f.getRightSubformula().accept(*this, data)); } - result = result && boost::any_cast(f.getLeftSubformula().accept(*this, data)); - result = result && boost::any_cast(f.getRightSubformula().accept(*this, data)); return result; } diff --git a/src/storm/logic/FragmentSpecification.cpp b/src/storm/logic/FragmentSpecification.cpp index eba4087e3..9af898490 100644 --- a/src/storm/logic/FragmentSpecification.cpp +++ b/src/storm/logic/FragmentSpecification.cpp @@ -89,8 +89,9 @@ namespace storm { multiObjective.setMultiObjectiveFormulasAllowed(true); multiObjective.setMultiObjectiveFormulaAtTopLevelRequired(true); - multiObjective.setNestedMultiObjectiveFormulasAllowed(true); - multiObjective.setOperatorsAtTopLevelOfMultiObjectiveFormulasRequired(false); + multiObjective.setNestedMultiObjectiveFormulasAllowed(false); + multiObjective.setOperatorsAtTopLevelOfMultiObjectiveFormulasRequired(true); + multiObjective.setNestedOperatorsInsideMultiObjectiveFormulasAllowed(false); multiObjective.setProbabilityOperatorsAllowed(true); multiObjective.setUntilFormulasAllowed(true); multiObjective.setGloballyFormulasAllowed(true); @@ -144,6 +145,7 @@ namespace storm { stepBoundedUntilFormulas = false; timeBoundedUntilFormulas = false; rewardBoundedUntilFormulas = false; + multiDimensionalBoundedUntilFormulas = false; varianceAsMeasureType = false; qualitativeOperatorResults = true; @@ -436,6 +438,15 @@ namespace storm { this->rewardBoundedUntilFormulas = newValue; return *this; } + + bool FragmentSpecification::areMultiDimensionalBoundedUntilFormulasAllowed() const { + return this->multiDimensionalBoundedUntilFormulas; + } + + FragmentSpecification& FragmentSpecification::setMultiDimensionalBoundedUntilFormulasAllowed(bool newValue) { + this->multiDimensionalBoundedUntilFormulas = newValue; + return *this; + } FragmentSpecification& FragmentSpecification::setOperatorsAllowed(bool newValue) { this->setProbabilityOperatorsAllowed(newValue); diff --git a/src/storm/logic/FragmentSpecification.h b/src/storm/logic/FragmentSpecification.h index 74d420f5b..338907872 100644 --- a/src/storm/logic/FragmentSpecification.h +++ b/src/storm/logic/FragmentSpecification.h @@ -106,6 +106,9 @@ namespace storm { bool areRewardBoundedUntilFormulasAllowed() const; FragmentSpecification& setRewardBoundedUntilFormulasAllowed(bool newValue); + bool areMultiDimensionalBoundedUntilFormulasAllowed() const; + FragmentSpecification& setMultiDimensionalBoundedUntilFormulasAllowed(bool newValue); + bool isVarianceMeasureTypeAllowed() const; FragmentSpecification& setVarianceMeasureTypeAllowed(bool newValue); @@ -169,6 +172,7 @@ namespace storm { bool stepBoundedUntilFormulas; bool timeBoundedUntilFormulas; bool rewardBoundedUntilFormulas; + bool multiDimensionalBoundedUntilFormulas; bool varianceAsMeasureType; bool quantitativeOperatorResults; bool qualitativeOperatorResults; diff --git a/src/storm/logic/VariableSubstitutionVisitor.cpp b/src/storm/logic/VariableSubstitutionVisitor.cpp index bc5c43ed9..316bff867 100644 --- a/src/storm/logic/VariableSubstitutionVisitor.cpp +++ b/src/storm/logic/VariableSubstitutionVisitor.cpp @@ -35,30 +35,33 @@ 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)); - - std::vector> lowerBounds; - std::vector> upperBounds; - std::vector tbReferences; - - for (unsigned i = 0; i < f.getDimension(); ++i) { + std::vector> lowerBounds, upperBounds; + std::vector timeBoundReferences; + for (uint64_t i = 0; i < f.getDimension(); ++i) { if (f.hasLowerBound(i)) { - lowerBounds.push_back(TimeBound(f.isLowerBoundStrict(i), f.getLowerBound(i).substitute(substitution))); + lowerBounds.emplace_back(TimeBound(f.isLowerBoundStrict(i), f.getLowerBound(i).substitute(substitution))); } else { - lowerBounds.push_back(boost::none); + lowerBounds.emplace_back(); } - if (f.hasUpperBound(i)) { - upperBounds.push_back(TimeBound(f.isUpperBoundStrict(i), f.getUpperBound(i).substitute(substitution))); + upperBounds.emplace_back(TimeBound(f.isUpperBoundStrict(i), f.getUpperBound(i).substitute(substitution))); } else { - upperBounds.push_back(boost::none); + upperBounds.emplace_back(); } - tbReferences.push_back(f.getTimeBoundReference(i)); + timeBoundReferences.push_back(f.getTimeBoundReference(i)); + } + if (f.hasMultiDimensionalSubformulas()) { + std::vector> leftSubformulas, rightSubformulas; + for (uint64_t i = 0; i < f.getDimension(); ++i) { + leftSubformulas.push_back(boost::any_cast>(f.getLeftSubformula(i).accept(*this, data))); + rightSubformulas.push_back(boost::any_cast>(f.getRightSubformula(i).accept(*this, data))); + } + return std::static_pointer_cast(std::make_shared(leftSubformulas, rightSubformulas, lowerBounds, upperBounds, timeBoundReferences)); + } else { + std::shared_ptr left = boost::any_cast>(f.getLeftSubformula().accept(*this, data)); + std::shared_ptr right = boost::any_cast>(f.getRightSubformula().accept(*this, data)); + return std::static_pointer_cast(std::make_shared(left, right, lowerBounds, upperBounds, timeBoundReferences)); } - - - 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/modelchecker/multiobjective/pcaa/SparseMdpRewardBoundedPcaaWeightVectorChecker.cpp b/src/storm/modelchecker/multiobjective/pcaa/SparseMdpRewardBoundedPcaaWeightVectorChecker.cpp index 609366759..32578be5c 100644 --- a/src/storm/modelchecker/multiobjective/pcaa/SparseMdpRewardBoundedPcaaWeightVectorChecker.cpp +++ b/src/storm/modelchecker/multiobjective/pcaa/SparseMdpRewardBoundedPcaaWeightVectorChecker.cpp @@ -21,7 +21,7 @@ namespace storm { namespace multiobjective { template - SparseMdpRewardBoundedPcaaWeightVectorChecker::SparseMdpRewardBoundedPcaaWeightVectorChecker(SparseMultiObjectivePreprocessorResult const& preprocessorResult) : PcaaWeightVectorChecker(preprocessorResult.objectives), swAll(true), rewardUnfolding(*preprocessorResult.preprocessedModel, this->objectives, storm::storage::BitVector(preprocessorResult.preprocessedModel->getNumberOfChoices(), true), preprocessorResult.reward0EStates) { + SparseMdpRewardBoundedPcaaWeightVectorChecker::SparseMdpRewardBoundedPcaaWeightVectorChecker(SparseMultiObjectivePreprocessorResult const& preprocessorResult) : PcaaWeightVectorChecker(preprocessorResult.objectives), swAll(true), rewardUnfolding(*preprocessorResult.preprocessedModel, preprocessorResult.objectives) { STORM_LOG_THROW(preprocessorResult.rewardFinitenessType == SparseMultiObjectivePreprocessorResult::RewardFinitenessType::AllFinite, storm::exceptions::NotSupportedException, "There is a scheduler that yields infinite reward for one objective. This is not supported."); STORM_LOG_THROW(preprocessorResult.preprocessedModel->getInitialStates().getNumberOfSetBits() == 1, storm::exceptions::NotSupportedException, "The model has multiple initial states."); diff --git a/src/storm/parser/FormulaParserGrammar.cpp b/src/storm/parser/FormulaParserGrammar.cpp index 30b4f4e38..719fdea7d 100644 --- a/src/storm/parser/FormulaParserGrammar.cpp +++ b/src/storm/parser/FormulaParserGrammar.cpp @@ -113,10 +113,10 @@ namespace storm { orStateFormula = andStateFormula[qi::_val = qi::_1] >> *(qi::lit("|") >> andStateFormula)[qi::_val = phoenix::bind(&FormulaParserGrammar::createBinaryBooleanStateFormula, phoenix::ref(*this), qi::_val, qi::_1, storm::logic::BinaryBooleanStateFormula::OperatorType::Or)]; orStateFormula.name("or state formula"); - multiObjectiveFormula = (qi::lit("multi") > qi::lit("(") >> ((pathFormula(storm::logic::FormulaContext::Probability) | stateFormula) % qi::lit(",")) >> qi::lit(")"))[qi::_val = phoenix::bind(&FormulaParserGrammar::createMultiObjectiveFormula, phoenix::ref(*this), qi::_1)]; - multiObjectiveFormula.name("Multi-objective formula"); + multiFormula = (qi::lit("multi") > qi::lit("(") >> ((pathFormula(storm::logic::FormulaContext::Probability) | stateFormula) % qi::lit(",")) >> qi::lit(")"))[qi::_val = phoenix::bind(&FormulaParserGrammar::createMultiFormula, phoenix::ref(*this), qi::_1)]; + multiFormula.name("Multi formula"); - stateFormula = (orStateFormula | multiObjectiveFormula); + stateFormula = (orStateFormula | multiFormula); stateFormula.name("state formula"); identifier %= qi::as_string[qi::raw[qi::lexeme[((qi::alpha | qi::char_('_') | qi::char_('.')) >> *(qi::alnum | qi::char_('_')))]]]; @@ -166,7 +166,7 @@ namespace storm { // debug(cumulativeRewardFormula); // debug(totalRewardFormula); // debug(instantaneousRewardFormula); -// debug(multiObjectiveFormula); +// debug(multiFormula); // Enable error reporting. qi::on_error(start, handler(qi::_1, qi::_2, qi::_3, qi::_4)); @@ -193,7 +193,7 @@ namespace storm { qi::on_error(cumulativeRewardFormula, handler(qi::_1, qi::_2, qi::_3, qi::_4)); qi::on_error(totalRewardFormula, handler(qi::_1, qi::_2, qi::_3, qi::_4)); qi::on_error(instantaneousRewardFormula, handler(qi::_1, qi::_2, qi::_3, qi::_4)); - qi::on_error(multiObjectiveFormula, handler(qi::_1, qi::_2, qi::_3, qi::_4)); + qi::on_error(multiFormula, handler(qi::_1, qi::_2, qi::_3, qi::_4)); } void FormulaParserGrammar::addIdentifierExpression(std::string const& identifier, storm::expressions::Expression const& expression) { @@ -343,8 +343,40 @@ namespace storm { } } - std::shared_ptr FormulaParserGrammar::createMultiObjectiveFormula(std::vector> const& subformulas) { - return std::shared_ptr(new storm::logic::MultiObjectiveFormula(subformulas)); + std::shared_ptr FormulaParserGrammar::createMultiFormula(std::vector> const& subformulas) { + bool isMultiDimensionalBoundedUntilFormula = !subformulas.empty(); + for (auto const& subformula : subformulas) { + if (!subformula->isBoundedUntilFormula()) { + isMultiDimensionalBoundedUntilFormula = false; + break; + } + } + + if (isMultiDimensionalBoundedUntilFormula) { + std::vector> leftSubformulas, rightSubformulas; + std::vector> lowerBounds, upperBounds; + std::vector timeBoundReferences; + for (auto const& subformula : subformulas) { + auto const& f = subformula->asBoundedUntilFormula(); + STORM_LOG_THROW(!f.isMultiDimensional(), storm::exceptions::WrongFormatException, "Composition of multidimensional bounded until formula must consist of single dimension subformulas. Got '" << f << "' instead."); + leftSubformulas.push_back(f.getLeftSubformula().asSharedPointer()); + rightSubformulas.push_back(f.getRightSubformula().asSharedPointer()); + if (f.hasLowerBound()) { + lowerBounds.emplace_back(storm::logic::TimeBound(f.isLowerBoundStrict(), f.getLowerBound())); + } else { + lowerBounds.emplace_back(); + } + if (f.hasUpperBound()) { + upperBounds.emplace_back(storm::logic::TimeBound(f.isUpperBoundStrict(), f.getUpperBound())); + } else { + upperBounds.emplace_back(); + } + timeBoundReferences.push_back(f.getTimeBoundReference()); + } + return std::shared_ptr(new storm::logic::BoundedUntilFormula(leftSubformulas, rightSubformulas, lowerBounds, upperBounds, timeBoundReferences)); + } else { + return std::shared_ptr(new storm::logic::MultiObjectiveFormula(subformulas)); + } } storm::jani::Property FormulaParserGrammar::createProperty(boost::optional const& propertyName, storm::modelchecker::FilterType const& filterType, std::shared_ptr const& formula, std::shared_ptr const& states) { diff --git a/src/storm/parser/FormulaParserGrammar.h b/src/storm/parser/FormulaParserGrammar.h index d8039bade..de6cc2284 100644 --- a/src/storm/parser/FormulaParserGrammar.h +++ b/src/storm/parser/FormulaParserGrammar.h @@ -189,7 +189,7 @@ namespace storm { qi::rule(), Skipper> instantaneousRewardFormula; qi::rule(), Skipper> longRunAverageRewardFormula; - qi::rule(), Skipper> multiObjectiveFormula; + qi::rule(), Skipper> multiFormula; // Parser that is used to recognize doubles only (as opposed to Spirit's double_ parser). boost::spirit::qi::real_parser> strict_double; @@ -221,7 +221,7 @@ namespace storm { std::shared_ptr createProbabilityOperatorFormula(storm::logic::OperatorInformation const& operatorInformation, std::shared_ptr const& subformula); std::shared_ptr createBinaryBooleanStateFormula(std::shared_ptr const& leftSubformula, std::shared_ptr const& rightSubformula, storm::logic::BinaryBooleanStateFormula::OperatorType operatorType); std::shared_ptr createUnaryBooleanStateFormula(std::shared_ptr const& subformula, boost::optional const& operatorType); - std::shared_ptr createMultiObjectiveFormula(std::vector> const& subformulas); + std::shared_ptr createMultiFormula(std::vector> const& subformulas); storm::jani::Property createProperty(boost::optional const& propertyName, storm::modelchecker::FilterType const& filterType, std::shared_ptr const& formula, std::shared_ptr const& states); storm::jani::Property createPropertyWithDefaultFilterTypeAndStates(boost::optional const& propertyName, std::shared_ptr const& formula); diff --git a/src/test/storm/logic/FragmentCheckerTest.cpp b/src/test/storm/logic/FragmentCheckerTest.cpp index dd0fc524c..c846f7f68 100644 --- a/src/test/storm/logic/FragmentCheckerTest.cpp +++ b/src/test/storm/logic/FragmentCheckerTest.cpp @@ -151,13 +151,13 @@ TEST(FragmentCheckerTest, MultiObjective) { EXPECT_FALSE(checker.conformsToSpecification(*formula, multiobjective)); ASSERT_NO_THROW(formula = formulaParser.parseSingleFormulaFromString("multi(R<0.3 [ C ], P<0.6 [F \"label\"] & \"label\" & R<=4[F \"label\"])")); - // TODO EXPECT_FALSE(checker.conformsToSpecification(*formula, multiobjective)); + EXPECT_FALSE(checker.conformsToSpecification(*formula, multiobjective)); ASSERT_NO_THROW(formula = formulaParser.parseSingleFormulaFromString("Pmax=? [ F multi(R<0.3 [ C ], P<0.6 [F \"label\"] & \"label\" & R<=4[F \"label\"])]")); EXPECT_FALSE(checker.conformsToSpecification(*formula, multiobjective)); ASSERT_NO_THROW(formula = formulaParser.parseSingleFormulaFromString("multi(R<0.3 [ C ], P<0.6 [F \"label\"], \"label\", R<=4[F \"label\"])")); - // TODO EXPECT_FALSE(checker.conformsToSpecification(*formula, multiobjective)); + EXPECT_FALSE(checker.conformsToSpecification(*formula, multiobjective)); ASSERT_NO_THROW(formula = formulaParser.parseSingleFormulaFromString("multi(R<0.3 [ C ], P<0.6 [F \"label\"], R<=4[F \"label\"])")); EXPECT_TRUE(checker.conformsToSpecification(*formula, multiobjective)); @@ -166,7 +166,7 @@ TEST(FragmentCheckerTest, MultiObjective) { EXPECT_FALSE(checker.conformsToSpecification(*formula, multiobjective)); ASSERT_NO_THROW(formula = formulaParser.parseSingleFormulaFromString("multi(R<0.3 [ C ], multi(P<0.6 [F \"label\"], R<=4[F \"label\"]))")); - // TODO EXPECT_FALSE(checker.conformsToSpecification(*formula, multiobjective)); + EXPECT_FALSE(checker.conformsToSpecification(*formula, multiobjective)); ASSERT_NO_THROW(formula = formulaParser.parseSingleFormulaFromString("multi(R<0.3 [ C ], P<0.6 [F \"label\" & \"otherlabel\"], P<=4[\"label\" U<=42 \"otherlabel\"])")); EXPECT_TRUE(checker.conformsToSpecification(*formula, multiobjective));