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

Merge remote-tracking branch 'upstream/master'

tempestpy_adaptions
Matthias Volk 7 years ago
parent
c770649f26 5b35927ecb
commit
069a1ae85e
6 changed files with 201 additions and 117 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. 38
      src/storm/logic/BoundedUntilFormula.h
  3. 30
      src/storm/logic/VariableSubstitutionVisitor.cpp
  4. 2
      src/storm/modelchecker/multiobjective/pcaa/SparsePcaaWeightVectorChecker.cpp
  5. 56
      src/storm/parser/JaniParser.cpp
  6. 2
      src/storm/storage/memorystructure/SparseModelMemoryProduct.cpp

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

@ -11,10 +11,20 @@
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) : BinaryPathFormula(leftSubformula, rightSubformula), timeBoundReference({timeBoundReference}), lowerBound({lowerBound}), upperBound({upperBound}) {
STORM_LOG_THROW(lowerBound || upperBound, storm::exceptions::InvalidArgumentException, "Bounded until formula requires at least one bound.");
}
BoundedUntilFormula::BoundedUntilFormula(std::shared_ptr<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) {
assert(timeBoundReferences.size() == upperBound.size());
assert(timeBoundReferences.size() == lowerBound.size());
STORM_LOG_THROW(this->getDimension() != 0, storm::exceptions::InvalidArgumentException, "Bounded until formula requires at least one dimension.");
for(unsigned i = 0; i < timeBoundReferences.size(); ++i) {
STORM_LOG_THROW(hasLowerBound(i) || hasUpperBound(i), storm::exceptions::InvalidArgumentException, "Bounded until formula requires at least one bound in each dimension.");
}
}
bool BoundedUntilFormula::isBoundedUntilFormula() const {
return true;
}
@ -28,111 +38,141 @@ namespace storm {
}
void BoundedUntilFormula::gatherReferencedRewardModels(std::set<std::string>& referencedRewardModels) const {
if (this->getTimeBoundReference().isRewardBound()) {
referencedRewardModels.insert(this->getTimeBoundReference().getRewardName());
for (unsigned i = 0; i < this->getDimension(); ++i) {
if (this->getTimeBoundReference(i).isRewardBound()) {
referencedRewardModels.insert(this->getTimeBoundReference().getRewardName());
}
}
this->getLeftSubformula().gatherReferencedRewardModels(referencedRewardModels);
this->getRightSubformula().gatherReferencedRewardModels(referencedRewardModels);
}
TimeBoundReference const& BoundedUntilFormula::getTimeBoundReference() const {
return timeBoundReference;
TimeBoundReference const& BoundedUntilFormula::getTimeBoundReference(unsigned i) const {
assert(i < timeBoundReference.size());
return timeBoundReference.at(i);
}
bool BoundedUntilFormula::isMultiDimensional() const {
assert(timeBoundReference.size() != 0);
return timeBoundReference.size() > 1;
}
unsigned BoundedUntilFormula::getDimension() const {
return timeBoundReference.size();
}
bool BoundedUntilFormula::isLowerBoundStrict() const {
return lowerBound.get().isStrict();
bool BoundedUntilFormula::isLowerBoundStrict(unsigned i) const {
assert(i < lowerBound.size());
return lowerBound.at(i).get().isStrict();
}
bool BoundedUntilFormula::hasLowerBound() const {
return static_cast<bool>(lowerBound);
for(auto const& lb : lowerBound) {
if (static_cast<bool>(lb)) {
return true;
}
}
return false;
}
bool BoundedUntilFormula::hasLowerBound(unsigned i) const {
return static_cast<bool>(lowerBound.at(i));
}
bool BoundedUntilFormula::hasIntegerLowerBound() const {
return lowerBound.get().getBound().hasIntegerType();
bool BoundedUntilFormula::hasIntegerLowerBound(unsigned i) const {
return lowerBound.at(i).get().getBound().hasIntegerType();
}
bool BoundedUntilFormula::isUpperBoundStrict() const {
return upperBound.get().isStrict();
bool BoundedUntilFormula::isUpperBoundStrict(unsigned i) const {
return upperBound.at(i).get().isStrict();
}
bool BoundedUntilFormula::hasUpperBound() const {
return static_cast<bool>(upperBound);
for(auto const& ub : upperBound) {
if (static_cast<bool>(ub)) {
return true;
}
}
return false;
}
bool BoundedUntilFormula::hasIntegerUpperBound() const {
return upperBound.get().getBound().hasIntegerType();
bool BoundedUntilFormula::hasUpperBound(unsigned i) const {
return static_cast<bool>(upperBound.at(i));
}
storm::expressions::Expression const& BoundedUntilFormula::getLowerBound() const {
return lowerBound.get().getBound();
bool BoundedUntilFormula::hasIntegerUpperBound(unsigned i) const {
return upperBound.at(i).get().getBound().hasIntegerType();
}
storm::expressions::Expression const& BoundedUntilFormula::getLowerBound(unsigned i) const {
return lowerBound.at(i).get().getBound();
}
storm::expressions::Expression const& BoundedUntilFormula::getUpperBound() const {
return upperBound.get().getBound();
storm::expressions::Expression const& BoundedUntilFormula::getUpperBound(unsigned i) const {
return upperBound.at(i).get().getBound();
}
template <>
double BoundedUntilFormula::getLowerBound() const {
double BoundedUntilFormula::getLowerBound(unsigned i) const {
checkNoVariablesInBound(this->getLowerBound());
double bound = this->getLowerBound().evaluateAsDouble();
double bound = this->getLowerBound(i).evaluateAsDouble();
STORM_LOG_THROW(bound >= 0, storm::exceptions::InvalidPropertyException, "Time-bound must not evaluate to negative number.");
return bound;
}
template <>
double BoundedUntilFormula::getUpperBound() const {
double BoundedUntilFormula::getUpperBound(unsigned i) const {
checkNoVariablesInBound(this->getUpperBound());
double bound = this->getUpperBound().evaluateAsDouble();
double bound = this->getUpperBound(i).evaluateAsDouble();
STORM_LOG_THROW(bound >= 0, storm::exceptions::InvalidPropertyException, "Time-bound must not evaluate to negative number.");
return bound;
}
template <>
storm::RationalNumber BoundedUntilFormula::getLowerBound() const {
checkNoVariablesInBound(this->getLowerBound());
storm::RationalNumber bound = this->getLowerBound().evaluateAsRational();
storm::RationalNumber BoundedUntilFormula::getLowerBound(unsigned i) const {
checkNoVariablesInBound(this->getLowerBound(i));
storm::RationalNumber bound = this->getLowerBound(i).evaluateAsRational();
STORM_LOG_THROW(bound >= storm::utility::zero<storm::RationalNumber>(), storm::exceptions::InvalidPropertyException, "Time-bound must not evaluate to negative number.");
return bound;
}
template <>
storm::RationalNumber BoundedUntilFormula::getUpperBound() const {
checkNoVariablesInBound(this->getUpperBound());
storm::RationalNumber bound = this->getUpperBound().evaluateAsRational();
storm::RationalNumber BoundedUntilFormula::getUpperBound(unsigned i) const {
checkNoVariablesInBound(this->getUpperBound(i));
storm::RationalNumber bound = this->getUpperBound(i).evaluateAsRational();
STORM_LOG_THROW(bound >= storm::utility::zero<storm::RationalNumber>(), storm::exceptions::InvalidPropertyException, "Time-bound must not evaluate to negative number.");
return bound;
}
template <>
uint64_t BoundedUntilFormula::getLowerBound() const {
checkNoVariablesInBound(this->getLowerBound());
int_fast64_t bound = this->getLowerBound().evaluateAsInt();
uint64_t BoundedUntilFormula::getLowerBound(unsigned i) const {
checkNoVariablesInBound(this->getLowerBound(i));
int_fast64_t bound = this->getLowerBound(i).evaluateAsInt();
STORM_LOG_THROW(bound >= 0, storm::exceptions::InvalidPropertyException, "Time-bound must not evaluate to negative number.");
return static_cast<uint64_t>(bound);
}
template <>
uint64_t BoundedUntilFormula::getUpperBound() const {
checkNoVariablesInBound(this->getUpperBound());
int_fast64_t bound = this->getUpperBound().evaluateAsInt();
uint64_t BoundedUntilFormula::getUpperBound(unsigned i) const {
checkNoVariablesInBound(this->getUpperBound(i));
int_fast64_t bound = this->getUpperBound(i).evaluateAsInt();
STORM_LOG_THROW(bound >= 0, storm::exceptions::InvalidPropertyException, "Time-bound must not evaluate to negative number.");
return static_cast<uint64_t>(bound);
}
template <>
double BoundedUntilFormula::getNonStrictUpperBound() const {
double bound = getUpperBound<double>();
STORM_LOG_THROW(!isUpperBoundStrict() || bound > 0, storm::exceptions::InvalidPropertyException, "Cannot retrieve non-strict bound from strict zero-bound.");
double BoundedUntilFormula::getNonStrictUpperBound(unsigned i) const {
double bound = getUpperBound<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 BoundedUntilFormula::getNonStrictUpperBound() const {
int_fast64_t bound = getUpperBound<uint64_t>();
if (isUpperBoundStrict()) {
uint64_t BoundedUntilFormula::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 {
@ -148,41 +188,53 @@ namespace storm {
this->getLeftSubformula().writeToStream(out);
out << " U";
if (this->getTimeBoundReference().isRewardBound()) {
out << "{\"" << this->getTimeBoundReference().getRewardName() << "\"}";
if (this->isMultiDimensional()) {
out << "[";
}
if (this->hasLowerBound()) {
if (this->hasUpperBound()) {
if (this->isLowerBoundStrict()) {
out << "(";
} else {
out << "[";
}
out << this->getLowerBound();
out << ", ";
out << this->getUpperBound();
if (this->isUpperBoundStrict()) {
out << ")";
for(unsigned i = 0; i < this->getDimension(); ++i) {
if (i > 0) {
out << ",";
}
if (this->getTimeBoundReference(i).isRewardBound()) {
out << "{\"" << this->getTimeBoundReference(i).getRewardName() << "\"}";
}
if (this->hasLowerBound(i)) {
if (this->hasUpperBound(i)) {
if (this->isLowerBoundStrict(i)) {
out << "(";
} else {
out << "[";
}
out << this->getLowerBound(i);
out << ", ";
out << this->getUpperBound(i);
if (this->isUpperBoundStrict(i)) {
out << ")";
} else {
out << "]";
}
} else {
out << "]";
if (this->isLowerBoundStrict(i)) {
out << ">";
} else {
out << ">=";
}
out << getLowerBound(i);
}
} else {
if (this->isLowerBoundStrict()) {
out << ">";
if (this->isUpperBoundStrict(i)) {
out << "<";
} else {
out << ">=";
out << "<=";
}
out << getLowerBound();
out << this->getUpperBound(i);
}
} else {
if (this->isUpperBoundStrict()) {
out << "<";
} else {
out << "<=";
}
out << this->getUpperBound();
out << " ";
}
if (this->isMultiDimensional()) {
out << "]";
}
out << " ";
this->getRightSubformula().writeToStream(out);
return out;

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

@ -1,5 +1,4 @@
#ifndef STORM_LOGIC_BOUNDEDUNTILFORMULA_H_
#define STORM_LOGIC_BOUNDEDUNTILFORMULA_H_
#pragma once
#include <boost/optional.hpp>
@ -13,7 +12,8 @@ namespace storm {
class BoundedUntilFormula : public BinaryPathFormula {
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);
virtual bool isBoundedUntilFormula() const override;
virtual bool isProbabilityPathFormula() const override;
@ -22,39 +22,43 @@ namespace storm {
virtual void gatherReferencedRewardModels(std::set<std::string>& referencedRewardModels) const override;
TimeBoundReference const& getTimeBoundReference() const;
TimeBoundReference const& getTimeBoundReference(unsigned i = 0) const;
bool isLowerBoundStrict() const;
bool isLowerBoundStrict(unsigned i = 0) const;
bool hasLowerBound() const;
bool hasIntegerLowerBound() const;
bool hasLowerBound(unsigned i) const;
bool hasIntegerLowerBound(unsigned i = 0) const;
bool isUpperBoundStrict() const;
bool isUpperBoundStrict(unsigned i = 0) const;
bool hasUpperBound() const;
bool hasIntegerUpperBound() const;
bool hasUpperBound(unsigned i) const;
bool hasIntegerUpperBound(unsigned i = 0) const;
bool isMultiDimensional() const;
unsigned getDimension() const;
storm::expressions::Expression const& getLowerBound() const;
storm::expressions::Expression const& getUpperBound() const;
storm::expressions::Expression const& getLowerBound(unsigned i = 0) const;
storm::expressions::Expression const& getUpperBound(unsigned i = 0) const;
template <typename ValueType>
ValueType getLowerBound() const;
ValueType getLowerBound(unsigned i = 0) const;
template <typename ValueType>
ValueType getUpperBound() const;
ValueType getUpperBound(unsigned i = 0) const;
template <typename ValueType>
ValueType getNonStrictUpperBound() const;
ValueType getNonStrictUpperBound(unsigned i = 0) const;
virtual std::ostream& writeToStream(std::ostream& out) const override;
private:
static void checkNoVariablesInBound(storm::expressions::Expression const& bound);
TimeBoundReference timeBoundReference;
boost::optional<TimeBound> lowerBound;
boost::optional<TimeBound> upperBound;
std::vector<TimeBoundReference> timeBoundReference;
std::vector<boost::optional<TimeBound>> lowerBound;
std::vector<boost::optional<TimeBound>> upperBound;
};
}
}
#endif /* STORM_LOGIC_BOUNDEDUNTILFORMULA_H_ */

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

@ -37,17 +37,29 @@ 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));
boost::optional<TimeBound> lowerBound;
if (f.hasLowerBound()) {
lowerBound = TimeBound(f.isLowerBoundStrict(), f.getLowerBound().substitute(substitution));
}
boost::optional<TimeBound> upperBound;
if (f.hasUpperBound()) {
upperBound = TimeBound(f.isUpperBoundStrict(), f.getUpperBound().substitute(substitution));
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::cout << f.hasLowerBound(i) << std::endl;
if (f.hasLowerBound(i)) {
lowerBounds.push_back(TimeBound(f.isLowerBoundStrict(i), f.getLowerBound(i).substitute(substitution)));
} else {
lowerBounds.push_back(boost::none);
}
if (f.hasUpperBound(i)) {
upperBounds.push_back(TimeBound(f.isUpperBoundStrict(i), f.getUpperBound(i).substitute(substitution)));
} else {
lowerBounds.push_back(boost::none);
}
tbReferences.push_back(f.getTimeBoundReference(i));
}
return std::static_pointer_cast<Formula>(std::make_shared<BoundedUntilFormula>(left, right, lowerBound, upperBound, f.getTimeBoundReference()));
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/SparsePcaaWeightVectorChecker.cpp
View File

@ -270,8 +270,8 @@ namespace storm {
// Set the result for this objective accordingly
storm::utility::vector::setVectorValues<ValueType>(objectiveResults[objIndex], maybeStates, x);
storm::utility::vector::setVectorValues<ValueType>(objectiveResults[objIndex], ~maybeStates, storm::utility::zero<ValueType>());
}
storm::utility::vector::setVectorValues<ValueType>(objectiveResults[objIndex], ~maybeStates, storm::utility::zero<ValueType>());
// Update the estimate for the next objectives.
if (!storm::utility::isZero(weightVector[objIndex])) {

56
src/storm/parser/JaniParser.cpp
View File

@ -165,9 +165,8 @@ namespace storm {
if (piStructure.count("lower") > 0) {
pi.lowerBound = parseExpression(piStructure.at("lower"), "Lower bound for property interval", {}, {});
// TODO substitute constants.
std::cout << "have lower bound" << std::endl;
STORM_LOG_THROW(!pi.lowerBound.containsVariables(), storm::exceptions::NotSupportedException, "Only constant expressions are supported as lower bounds");
}
if (piStructure.count("lower-exclusive") > 0) {
STORM_LOG_THROW(pi.lowerBound.isInitialized(), storm::exceptions::InvalidJaniException, "Lower-exclusive can only be set if a lower bound is present");
@ -175,16 +174,17 @@ namespace storm {
}
if (piStructure.count("upper") > 0) {
std::cout << "have upper bound" << std::endl;
pi.upperBound = parseExpression(piStructure.at("upper"), "Upper bound for property interval", {}, {});
// TODO substitute constants.
STORM_LOG_THROW(!pi.upperBound.containsVariables(), storm::exceptions::NotSupportedException, "Only constant expressions are supported as upper bounds");
}
if (piStructure.count("upper-exclusive") > 0) {
STORM_LOG_THROW(pi.lowerBound.isInitialized(), storm::exceptions::InvalidJaniException, "Lower-exclusive can only be set if a lower bound is present");
pi.lowerBoundStrict = piStructure.at("upper-exclusive");
STORM_LOG_THROW(pi.upperBound.isInitialized(), storm::exceptions::InvalidJaniException, "Lower-exclusive can only be set if a lower bound is present");
pi.upperBoundStrict = piStructure.at("upper-exclusive");
}
STORM_LOG_THROW(pi.lowerBound.isInitialized() || pi.upperBound.isInitialized(), storm::exceptions::InvalidJaniException, "Bounded operators must be bounded");
STORM_LOG_THROW(pi.lowerBound.isInitialized() || pi.upperBound.isInitialized(), storm::exceptions::InvalidJaniException, "Bounded operator must have a bounded interval, but no bounds found in '" << piStructure << "'");
return pi;
@ -367,22 +367,38 @@ namespace storm {
return std::make_shared<storm::logic::BoundedUntilFormula const>(args[0], args[1], storm::logic::TimeBound(pi.lowerBoundStrict, pi.lowerBound), storm::logic::TimeBound(pi.upperBoundStrict, pi.upperBound), storm::logic::TimeBoundReference(storm::logic::TimeBoundType::Time));
} else if (propertyStructure.count("reward-bounds") > 0 ) {
storm::jani::PropertyInterval pi = parsePropertyInterval(propertyStructure.at("reward-bounds"));
STORM_LOG_THROW(pi.hasUpperBound(), storm::exceptions::NotSupportedException, "Storm only supports time-bounded until with an upper bound.");
STORM_LOG_THROW(propertyStructure.at("reward-bounds").count("exp") == 1, storm::exceptions::InvalidJaniException, "Expecting reward-expression for operator " << opString << " in " << context);
storm::expressions::Expression rewExpr = parseExpression(propertyStructure.at("reward-bounds").at("exp"), "Reward expression in " + context, globalVars, constants);
STORM_LOG_THROW(!rewExpr.isVariable(), storm::exceptions::NotSupportedException, "Storm currently does not support complex reward expressions.");
std::string rewardName = rewExpr.getVariables().begin()->getName();
STORM_LOG_WARN("Reward-type (steps, time) is deduced from model type.");
double lowerBound = 0.0;
if(pi.hasLowerBound()) {
lowerBound = pi.lowerBound.evaluateAsDouble();
std::vector<boost::optional<storm::logic::TimeBound>> lowerBounds;
std::vector<boost::optional<storm::logic::TimeBound>> upperBounds;
std::vector<storm::logic::TimeBoundReference> tbReferences;
for (auto const& rbStructure : propertyStructure.at("reward-bounds")) {
storm::jani::PropertyInterval pi = parsePropertyInterval(rbStructure.at("bounds"));
STORM_LOG_THROW(pi.hasUpperBound(), storm::exceptions::NotSupportedException, "Storm only supports time-bounded until with an upper bound.");
STORM_LOG_THROW(rbStructure.count("exp") == 1, storm::exceptions::InvalidJaniException, "Expecting reward-expression for operator " << opString << " in " << context);
storm::expressions::Expression rewExpr = parseExpression(rbStructure.at("exp"), "Reward expression in " + context, globalVars, constants);
STORM_LOG_THROW(rewExpr.isVariable(), storm::exceptions::NotSupportedException, "Storm currently does not support complex reward expressions.");
std::string rewardName = rewExpr.getVariables().begin()->getName();
STORM_LOG_WARN("Reward-type (steps, time) is deduced from model type.");
double lowerBound = 0.0;
if(pi.hasLowerBound()) {
lowerBound = pi.lowerBound.evaluateAsDouble();
}
double upperBound = pi.upperBound.evaluateAsDouble();
STORM_LOG_THROW(lowerBound >= 0, storm::exceptions::InvalidJaniException, "(Lower) time-bounds cannot be negative");
STORM_LOG_THROW(upperBound >= 0, storm::exceptions::InvalidJaniException, "(Upper) time-bounds cannot be negative");
if (pi.hasLowerBound()) {
lowerBounds.push_back(storm::logic::TimeBound(pi.lowerBoundStrict, pi.lowerBound));
} else {
lowerBounds.push_back(boost::none);
}
if (pi.hasUpperBound()) {
upperBounds.push_back(storm::logic::TimeBound(pi.upperBoundStrict, pi.upperBound));
} else {
upperBounds.push_back(boost::none);
}
tbReferences.push_back(storm::logic::TimeBoundReference(rewardName));
}
double upperBound = pi.upperBound.evaluateAsDouble();
STORM_LOG_THROW(lowerBound >= 0, storm::exceptions::InvalidJaniException, "(Lower) time-bounds cannot be negative");
STORM_LOG_THROW(upperBound >= 0, storm::exceptions::InvalidJaniException, "(Upper) time-bounds cannot be negative");
STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "Reward bounded properties are not supported by storm");
return std::make_shared<storm::logic::BoundedUntilFormula const>(args[0], args[1], storm::logic::TimeBound(pi.lowerBoundStrict, pi.lowerBound), storm::logic::TimeBound(pi.upperBoundStrict, pi.upperBound), storm::logic::TimeBoundReference(rewardName));
auto res = std::make_shared<storm::logic::BoundedUntilFormula const>(args[0], args[1], lowerBounds, upperBounds, tbReferences);
return res;
}
if (args[0]->isTrueFormula()) {

2
src/storm/storage/memorystructure/SparseModelMemoryProduct.cpp
View File

@ -248,7 +248,7 @@ namespace storm {
uint64_t modelRow = model.getTransitionMatrix().getRowGroupIndices()[modelState];
uint64_t groupEnd = model.getTransitionMatrix().getRowGroupIndices()[modelState + 1];
hasTrivialNondeterminism = hasTrivialNondeterminism && (groupEnd == modelRow + 1);
for (; groupEnd; ++modelRow) {
for (; modelRow < groupEnd; ++modelRow) {
++numResChoices;
numResTransitions += model.getTransitionMatrix().getRow(modelRow).getNumberOfEntries();
}

Write Preview
Loading…
Cancel
Save