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

added needed methods to class BoundedGloballyFormula

tempestpy_adaptions
Lukas Posch 4 years ago
parent
dbc0cacb45
commit
ef415d4347
2 changed files with 311 additions and 11 deletions
Whitespace
Show all changes Ignore whitespace when comparing lines Ignore changes in amount of whitespace Ignore changes in whitespace at EOL
Unified View
Diff Options
Show Stats Download Patch File Download Diff File
  1. 260
      src/storm/logic/BoundedGloballyFormula.cpp
  2. 62
      src/storm/logic/BoundedGloballyFormula.h

260
src/storm/logic/BoundedGloballyFormula.cpp
View File

@ -1,11 +1,34 @@
#include "storm/logic/BoundedGloballyFormula.h" #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/logic/FormulaVisitor.h"
#include "storm/exceptions/InvalidPropertyException.h"
#include "storm/exceptions/InvalidOperationException.h"
namespace storm { namespace storm {
namespace logic { namespace logic {
// TODO: add 'k' as input to formula, maybe as TimeBound?
BoundedGloballyFormula::BoundedGloballyFormula(std::shared_ptr<Formula const> const& subformula) : UnaryPathFormula(subformula) {
// Intentionally left empty.
BoundedGloballyFormula::BoundedGloballyFormula(std::shared_ptr<Formula const> const& subformula, boost::optional<TimeBound> const& lowerBound, boost::optional<TimeBound> 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<Formula const> const& subformula, std::vector<boost::optional<TimeBound>> const& lowerBounds, std::vector<boost::optional<TimeBound>> const& upperBounds, std::vector<TimeBoundReference> 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<std::shared_ptr<Formula const>> const& subformulas, std::vector<boost::optional<TimeBound>> const& lowerBounds, std::vector<boost::optional<TimeBound>> const& upperBounds, std::vector<TimeBoundReference> 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 { bool BoundedGloballyFormula::isBoundedGloballyFormula() const {
@ -20,10 +43,237 @@ namespace storm {
return visitor.visit(*this, data); 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<bool>(lb)) {
return true;
}
}
return false;
}
bool BoundedGloballyFormula::hasLowerBound(unsigned i) const {
return static_cast<bool>(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<bool>(ub)) {
return true;
}
}
return false;
}
bool BoundedGloballyFormula::hasUpperBound(unsigned i) const {
return static_cast<bool>(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<storm::RationalNumber>(); }
checkNoVariablesInBound(this->getLowerBound(i));
storm::RationalNumber bound = this->getLowerBound(i).evaluateAsRational();
STORM_LOG_THROW(bound >= storm::utility::zero<storm::RationalNumber>(), 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::RationalNumber>(), 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<uint64_t>(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<uint64_t>(bound);
}
template <>
double BoundedGloballyFormula::getNonStrictUpperBound(unsigned i) const {
double bound = getUpperBound<double>(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<uint64_t>(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<double>(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<uint64_t>(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 { std::ostream& BoundedGloballyFormula::writeToStream(std::ostream& out) const {
out << "G < ";
// TODO: write "{<, <=} k"
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); this->getSubformula().writeToStream(out);
return out; return out;
} }
} }

62
src/storm/logic/BoundedGloballyFormula.h
View File

@ -1,13 +1,19 @@
#ifndef STORM_LOGIC_BOUNDEDGLOBALLYFORMULA_H
#define STORM_LOGIC_BOUNDEDGLOBALLYFORMULA_H
#pragma once
#include <boost/optional.hpp>
#include "storm/logic/UnaryPathFormula.h" #include "storm/logic/UnaryPathFormula.h"
#include "storm/logic/TimeBound.h"
#include "storm/logic/TimeBoundType.h"
namespace storm { namespace storm {
namespace logic { namespace logic {
class BoundedGloballyFormula : public UnaryPathFormula { class BoundedGloballyFormula : public UnaryPathFormula {
public: public:
BoundedGloballyFormula(std::shared_ptr<Formula const> const &subformula);
BoundedGloballyFormula(std::shared_ptr<Formula const> const& subformula, boost::optional<TimeBound> const& lowerBound, boost::optional<TimeBound> const& upperBound, TimeBoundReference const& timeBoundReference);
BoundedGloballyFormula(std::shared_ptr<Formula const> const& subformula, std::vector<boost::optional<TimeBound>> const& lowerBounds, std::vector<boost::optional<TimeBound>> const& upperBounds, std::vector<TimeBoundReference> const& timeBoundReferences);
BoundedGloballyFormula(std::vector<std::shared_ptr<Formula const>> const& subformulas, std::vector<boost::optional<TimeBound>> const& lowerBounds, std::vector<boost::optional<TimeBound>> const& upperBounds, std::vector<TimeBoundReference> const& timeBoundReferences);
virtual ~BoundedGloballyFormula() { virtual ~BoundedGloballyFormula() {
// Intentionally left empty. // Intentionally left empty.
@ -18,9 +24,53 @@ namespace storm {
virtual boost::any accept(FormulaVisitor const &visitor, boost::any const &data) 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 <typename ValueType>
ValueType getLowerBound(unsigned i = 0) const;
template <typename ValueType>
ValueType getUpperBound(unsigned i = 0) const;
template <typename ValueType>
ValueType getNonStrictUpperBound(unsigned i = 0) const;
template<typename ValueType>
ValueType getNonStrictLowerBound(unsigned i = 0) const;
virtual std::ostream &writeToStream(std::ostream &out) const override; virtual std::ostream &writeToStream(std::ostream &out) const override;
private:
static void checkNoVariablesInBound(storm::expressions::Expression const& bound);
std::vector<std::shared_ptr<Formula const>> subformula;
std::vector<TimeBoundReference> timeBoundReference;
std::vector<boost::optional<TimeBound>> lowerBound;
std::vector<boost::optional<TimeBound>> upperBound;
}; };
} }
}
#endif /* STORM_LOGIC_BOUNDEDGLOBALLYFORMULA_H */
}
Write Preview
Loading…
Cancel
Save