sp
/
tempest
1
0
Fork 0
Code Issues Pull Requests Projects Releases Wiki Activity
Browse Source

extended multidimensional bounded until formulas to have different subformulas in each dimension

tempestpy_adaptions
TimQu 7 years ago
parent
cbe73081f8
commit
8b466f1fa7
12 changed files with 307 additions and 105 deletions
Whitespace
Show all changes Ignore whitespace when comparing lines Ignore changes in amount of whitespace Ignore changes in whitespace at EOL
Split View
Diff Options
Show Stats Download Patch File Download Diff File
  1. 190
      src/storm/logic/BoundedUntilFormula.cpp
  2. 23
      src/storm/logic/BoundedUntilFormula.h
  3. 30
      src/storm/logic/CloneVisitor.cpp
  4. 13
      src/storm/logic/FormulaInformationVisitor.cpp
  5. 42
      src/storm/logic/FragmentChecker.cpp
  6. 15
      src/storm/logic/FragmentSpecification.cpp
  7. 4
      src/storm/logic/FragmentSpecification.h
  8. 37
      src/storm/logic/VariableSubstitutionVisitor.cpp
  9. 2
      src/storm/modelchecker/multiobjective/pcaa/SparseMdpRewardBoundedPcaaWeightVectorChecker.cpp
  10. 46
      src/storm/parser/FormulaParserGrammar.cpp
  11. 4
      src/storm/parser/FormulaParserGrammar.h
  12. 6
      src/test/storm/logic/FragmentCheckerTest.cpp

190
src/storm/logic/BoundedUntilFormula.cpp
View File

@ -11,20 +11,26 @@
namespace storm {
namespace logic {
BoundedUntilFormula::BoundedUntilFormula(std::shared_ptr<Formula const> const& leftSubformula, std::shared_ptr<Formula const> const& rightSubformula, boost::optional<TimeBound> const& lowerBound, boost::optional<TimeBound> const& upperBound, TimeBoundReference const& timeBoundReference) : BinaryPathFormula(leftSubformula, rightSubformula), timeBoundReference({timeBoundReference}), lowerBound({lowerBound}), upperBound({upperBound}) {
BoundedUntilFormula::BoundedUntilFormula(std::shared_ptr<Formula const> const& leftSubformula, std::shared_ptr<Formula const> const& rightSubformula, boost::optional<TimeBound> const& lowerBound, boost::optional<TimeBound> 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<Formula const> const& leftSubformula, std::shared_ptr<Formula const> const& rightSubformula,std::vector<boost::optional<TimeBound>> const& lowerBounds, std::vector<boost::optional<TimeBound>> const& upperBounds, std::vector<TimeBoundReference> const& timeBoundReferences) : BinaryPathFormula(leftSubformula, rightSubformula), timeBoundReference(timeBoundReferences), lowerBound(lowerBounds), upperBound(upperBounds) {
BoundedUntilFormula::BoundedUntilFormula(std::shared_ptr<Formula const> const& leftSubformula, std::shared_ptr<Formula const> const& rightSubformula,std::vector<boost::optional<TimeBound>> const& lowerBounds, std::vector<boost::optional<TimeBound>> const& upperBounds, std::vector<TimeBoundReference> 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<std::shared_ptr<Formula const>> const& leftSubformulas, std::vector<std::shared_ptr<Formula const>> const& rightSubformulas, std::vector<boost::optional<TimeBound>> const& lowerBounds, std::vector<boost::optional<TimeBound>> const& upperBounds, std::vector<TimeBoundReference> 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<std::shared_ptr<AtomicExpressionFormula const>>& 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<std::shared_ptr<AtomicLabelFormula const>>& 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<std::string>& 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 const> BoundedUntilFormula::restrictToDimension(unsigned i) const {
return std::make_shared<BoundedUntilFormula const>(this->getLeftSubformula().asSharedPointer(), this->getRightSubformula().asSharedPointer(), lowerBound.at(i), upperBound.at(i), this->getTimeBoundReference(i));
return std::make_shared<BoundedUntilFormula const>(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 << "]";
}

23
src/storm/logic/BoundedUntilFormula.h
View File

@ -9,10 +9,11 @@
namespace storm {
namespace logic {
class BoundedUntilFormula : public BinaryPathFormula {
class BoundedUntilFormula : public PathFormula {
public:
BoundedUntilFormula(std::shared_ptr<Formula const> const& leftSubformula, std::shared_ptr<Formula const> const& rightSubformula, boost::optional<TimeBound> const& lowerBound, boost::optional<TimeBound> const& upperBound, TimeBoundReference const& timeBoundReference);
BoundedUntilFormula(std::shared_ptr<Formula const> const& leftSubformula, std::shared_ptr<Formula const> const& rightSubformula, std::vector<boost::optional<TimeBound>> const& lowerBounds, std::vector<boost::optional<TimeBound>> const& upperBounds, std::vector<TimeBoundReference> const& timeBoundReferences);
BoundedUntilFormula(std::vector<std::shared_ptr<Formula const>> const& leftSubformulas, std::vector<std::shared_ptr<Formula const>> const& rightSubformulas, std::vector<boost::optional<TimeBound>> const& lowerBounds, std::vector<boost::optional<TimeBound>> const& upperBounds, std::vector<TimeBoundReference> 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<std::shared_ptr<AtomicExpressionFormula const>>& atomicExpressionFormulas) const override;
virtual void gatherAtomicLabelFormulas(std::vector<std::shared_ptr<AtomicLabelFormula const>>& atomicLabelFormulas) const override;
virtual void gatherReferencedRewardModels(std::set<std::string>& 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<std::shared_ptr<Formula const>> leftSubformula;
std::vector<std::shared_ptr<Formula const>> rightSubformula;
std::vector<TimeBoundReference> timeBoundReference;
std::vector<boost::optional<TimeBound>> lowerBound;
std::vector<boost::optional<TimeBound>> upperBound;

30
src/storm/logic/CloneVisitor.cpp
View File

@ -29,9 +29,33 @@ namespace storm {
}
boost::any CloneVisitor::visit(BoundedUntilFormula const& f, boost::any const& data) const {
std::shared_ptr<Formula> left = boost::any_cast<std::shared_ptr<Formula>>(f.getLeftSubformula().accept(*this, data));
std::shared_ptr<Formula> right = boost::any_cast<std::shared_ptr<Formula>>(f.getRightSubformula().accept(*this, data));
return std::static_pointer_cast<Formula>(std::make_shared<BoundedUntilFormula>(f));
std::vector<boost::optional<TimeBound>> lowerBounds, upperBounds;
std::vector<TimeBoundReference> 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<std::shared_ptr<Formula const>> leftSubformulas, rightSubformulas;
for (uint64_t i = 0; i < f.getDimension(); ++i) {
leftSubformulas.push_back(boost::any_cast<std::shared_ptr<Formula>>(f.getLeftSubformula(i).accept(*this, data)));
rightSubformulas.push_back(boost::any_cast<std::shared_ptr<Formula>>(f.getRightSubformula(i).accept(*this, data)));
}
return std::static_pointer_cast<Formula>(std::make_shared<BoundedUntilFormula>(leftSubformulas, rightSubformulas, lowerBounds, upperBounds, timeBoundReferences));
} else {
std::shared_ptr<Formula> left = boost::any_cast<std::shared_ptr<Formula>>(f.getLeftSubformula().accept(*this, data));
std::shared_ptr<Formula> right = boost::any_cast<std::shared_ptr<Formula>>(f.getRightSubformula().accept(*this, data));
return std::static_pointer_cast<Formula>(std::make_shared<BoundedUntilFormula>(left, right, lowerBounds, upperBounds, timeBoundReferences));
}
}
boost::any CloneVisitor::visit(ConditionalFormula const& f, boost::any const& data) const {

13
src/storm/logic/FormulaInformationVisitor.cpp
View File

@ -26,7 +26,18 @@ namespace storm {
}
boost::any FormulaInformationVisitor::visit(BoundedUntilFormula const& f, boost::any const& data) const {
return boost::any_cast<FormulaInformation>(f.getLeftSubformula().accept(*this, data)).join(boost::any_cast<FormulaInformation>(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<FormulaInformation>(f.getLeftSubformula(i).accept(*this, data)));
result.join(boost::any_cast<FormulaInformation>(f.getRightSubformula(i).accept(*this, data)));
}
} else {
result.join(boost::any_cast<FormulaInformation>(f.getLeftSubformula().accept(*this, data)));
result.join(boost::any_cast<FormulaInformation>(f.getRightSubformula().accept(*this, data)));
}
return result;
}
boost::any FormulaInformationVisitor::visit(ConditionalFormula const& f, boost::any const& data) const {

42
src/storm/logic/FragmentChecker.cpp
View File

@ -57,21 +57,39 @@ namespace storm {
boost::any FragmentChecker::visit(BoundedUntilFormula const& f, boost::any const& data) const {
InheritedInformation const& inherited = boost::any_cast<InheritedInformation const&>(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<bool>(f.getLeftSubformula(i).accept(*this, data));
result = result && boost::any_cast<bool>(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<bool>(f.getLeftSubformula().accept(*this, data));
result = result && boost::any_cast<bool>(f.getRightSubformula().accept(*this, data));
}
result = result && boost::any_cast<bool>(f.getLeftSubformula().accept(*this, data));
result = result && boost::any_cast<bool>(f.getRightSubformula().accept(*this, data));
return result;
}

15
src/storm/logic/FragmentSpecification.cpp
View File

@ -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);

4
src/storm/logic/FragmentSpecification.h
View File

@ -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;

37
src/storm/logic/VariableSubstitutionVisitor.cpp
View File

@ -35,30 +35,33 @@ namespace storm {
}
boost::any VariableSubstitutionVisitor::visit(BoundedUntilFormula const& f, boost::any const& data) const {
auto left = boost::any_cast<std::shared_ptr<Formula>>(f.getLeftSubformula().accept(*this, data));
auto right = boost::any_cast<std::shared_ptr<Formula>>(f.getRightSubformula().accept(*this, data));
std::vector<boost::optional<storm::logic::TimeBound>> lowerBounds;
std::vector<boost::optional<storm::logic::TimeBound>> upperBounds;
std::vector<storm::logic::TimeBoundReference> tbReferences;
for (unsigned i = 0; i < f.getDimension(); ++i) {
std::vector<boost::optional<TimeBound>> lowerBounds, upperBounds;
std::vector<TimeBoundReference> 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<std::shared_ptr<Formula const>> leftSubformulas, rightSubformulas;
for (uint64_t i = 0; i < f.getDimension(); ++i) {
leftSubformulas.push_back(boost::any_cast<std::shared_ptr<Formula>>(f.getLeftSubformula(i).accept(*this, data)));
rightSubformulas.push_back(boost::any_cast<std::shared_ptr<Formula>>(f.getRightSubformula(i).accept(*this, data)));
}
return std::static_pointer_cast<Formula>(std::make_shared<BoundedUntilFormula>(leftSubformulas, rightSubformulas, lowerBounds, upperBounds, timeBoundReferences));
} else {
std::shared_ptr<Formula> left = boost::any_cast<std::shared_ptr<Formula>>(f.getLeftSubformula().accept(*this, data));
std::shared_ptr<Formula> right = boost::any_cast<std::shared_ptr<Formula>>(f.getRightSubformula().accept(*this, data));
return std::static_pointer_cast<Formula>(std::make_shared<BoundedUntilFormula>(left, right, lowerBounds, upperBounds, timeBoundReferences));
}
return std::static_pointer_cast<Formula>(std::make_shared<BoundedUntilFormula>(left, right, lowerBounds, upperBounds, tbReferences));
}
boost::any VariableSubstitutionVisitor::visit(CumulativeRewardFormula const& f, boost::any const&) const {

2
src/storm/modelchecker/multiobjective/pcaa/SparseMdpRewardBoundedPcaaWeightVectorChecker.cpp
View File

@ -21,7 +21,7 @@ namespace storm {
namespace multiobjective {
template <class SparseMdpModelType>
SparseMdpRewardBoundedPcaaWeightVectorChecker<SparseMdpModelType>::SparseMdpRewardBoundedPcaaWeightVectorChecker(SparseMultiObjectivePreprocessorResult<SparseMdpModelType> const& preprocessorResult) : PcaaWeightVectorChecker<SparseMdpModelType>(preprocessorResult.objectives), swAll(true), rewardUnfolding(*preprocessorResult.preprocessedModel, this->objectives, storm::storage::BitVector(preprocessorResult.preprocessedModel->getNumberOfChoices(), true), preprocessorResult.reward0EStates) {
SparseMdpRewardBoundedPcaaWeightVectorChecker<SparseMdpModelType>::SparseMdpRewardBoundedPcaaWeightVectorChecker(SparseMultiObjectivePreprocessorResult<SparseMdpModelType> const& preprocessorResult) : PcaaWeightVectorChecker<SparseMdpModelType>(preprocessorResult.objectives), swAll(true), rewardUnfolding(*preprocessorResult.preprocessedModel, preprocessorResult.objectives) {
STORM_LOG_THROW(preprocessorResult.rewardFinitenessType == SparseMultiObjectivePreprocessorResult<SparseMdpModelType>::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.");

46
src/storm/parser/FormulaParserGrammar.cpp
View File

@ -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<qi::fail>(start, handler(qi::_1, qi::_2, qi::_3, qi::_4));
@ -193,7 +193,7 @@ namespace storm {
qi::on_error<qi::fail>(cumulativeRewardFormula, handler(qi::_1, qi::_2, qi::_3, qi::_4));
qi::on_error<qi::fail>(totalRewardFormula, handler(qi::_1, qi::_2, qi::_3, qi::_4));
qi::on_error<qi::fail>(instantaneousRewardFormula, handler(qi::_1, qi::_2, qi::_3, qi::_4));
qi::on_error<qi::fail>(multiObjectiveFormula, handler(qi::_1, qi::_2, qi::_3, qi::_4));
qi::on_error<qi::fail>(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<storm::logic::Formula const> FormulaParserGrammar::createMultiObjectiveFormula(std::vector<std::shared_ptr<storm::logic::Formula const>> const& subformulas) {
return std::shared_ptr<storm::logic::Formula const>(new storm::logic::MultiObjectiveFormula(subformulas));
std::shared_ptr<storm::logic::Formula const> FormulaParserGrammar::createMultiFormula(std::vector<std::shared_ptr<storm::logic::Formula const>> const& subformulas) {
bool isMultiDimensionalBoundedUntilFormula = !subformulas.empty();
for (auto const& subformula : subformulas) {
if (!subformula->isBoundedUntilFormula()) {
isMultiDimensionalBoundedUntilFormula = false;
break;
}
}
if (isMultiDimensionalBoundedUntilFormula) {
std::vector<std::shared_ptr<storm::logic::Formula const>> leftSubformulas, rightSubformulas;
std::vector<boost::optional<storm::logic::TimeBound>> lowerBounds, upperBounds;
std::vector<storm::logic::TimeBoundReference> 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<storm::logic::Formula const>(new storm::logic::BoundedUntilFormula(leftSubformulas, rightSubformulas, lowerBounds, upperBounds, timeBoundReferences));
} else {
return std::shared_ptr<storm::logic::Formula const>(new storm::logic::MultiObjectiveFormula(subformulas));
}
}
storm::jani::Property FormulaParserGrammar::createProperty(boost::optional<std::string> const& propertyName, storm::modelchecker::FilterType const& filterType, std::shared_ptr<storm::logic::Formula const> const& formula, std::shared_ptr<storm::logic::Formula const> const& states) {

4
src/storm/parser/FormulaParserGrammar.h
View File

@ -189,7 +189,7 @@ namespace storm {
qi::rule<Iterator, std::shared_ptr<storm::logic::Formula const>(), Skipper> instantaneousRewardFormula;
qi::rule<Iterator, std::shared_ptr<storm::logic::Formula const>(), Skipper> longRunAverageRewardFormula;
qi::rule<Iterator, std::shared_ptr<storm::logic::Formula const>(), Skipper> multiObjectiveFormula;
qi::rule<Iterator, std::shared_ptr<storm::logic::Formula const>(), Skipper> multiFormula;
// Parser that is used to recognize doubles only (as opposed to Spirit's double_ parser).
boost::spirit::qi::real_parser<double, boost::spirit::qi::strict_real_policies<double>> strict_double;
@ -221,7 +221,7 @@ namespace storm {
std::shared_ptr<storm::logic::Formula const> createProbabilityOperatorFormula(storm::logic::OperatorInformation const& operatorInformation, std::shared_ptr<storm::logic::Formula const> const& subformula);
std::shared_ptr<storm::logic::Formula const> createBinaryBooleanStateFormula(std::shared_ptr<storm::logic::Formula const> const& leftSubformula, std::shared_ptr<storm::logic::Formula const> const& rightSubformula, storm::logic::BinaryBooleanStateFormula::OperatorType operatorType);
std::shared_ptr<storm::logic::Formula const> createUnaryBooleanStateFormula(std::shared_ptr<storm::logic::Formula const> const& subformula, boost::optional<storm::logic::UnaryBooleanStateFormula::OperatorType> const& operatorType);
std::shared_ptr<storm::logic::Formula const> createMultiObjectiveFormula(std::vector<std::shared_ptr<storm::logic::Formula const>> const& subformulas);
std::shared_ptr<storm::logic::Formula const> createMultiFormula(std::vector<std::shared_ptr<storm::logic::Formula const>> const& subformulas);
storm::jani::Property createProperty(boost::optional<std::string> const& propertyName, storm::modelchecker::FilterType const& filterType, std::shared_ptr<storm::logic::Formula const> const& formula, std::shared_ptr<storm::logic::Formula const> const& states);
storm::jani::Property createPropertyWithDefaultFilterTypeAndStates(boost::optional<std::string> const& propertyName, std::shared_ptr<storm::logic::Formula const> const& formula);

6
src/test/storm/logic/FragmentCheckerTest.cpp
View File

@ -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));

Write Preview
Loading…
Cancel
Save