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

started working on allowing expressions in time-bounds of formulas

tempestpy_adaptions
dehnert 8 years ago
parent
ce36601f7c
commit
8d3f633cbc
18 changed files with 229 additions and 99 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. 118
      src/storm/logic/BoundedUntilFormula.cpp
  2. 49
      src/storm/logic/BoundedUntilFormula.h
  3. 6
      src/storm/logic/CloneVisitor.cpp
  4. 2
      src/storm/logic/FragmentChecker.cpp
  5. 15
      src/storm/modelchecker/csl/HybridCtmcCslModelChecker.cpp
  6. 15
      src/storm/modelchecker/csl/SparseCtmcCslModelChecker.cpp
  7. 15
      src/storm/modelchecker/csl/SparseMarkovAutomatonCslModelChecker.cpp
  8. 24
      src/storm/modelchecker/multiobjective/pcaa/SparsePcaaPreprocessor.cpp
  9. 5
      src/storm/modelchecker/prctl/HybridDtmcPrctlModelChecker.cpp
  10. 5
      src/storm/modelchecker/prctl/HybridMdpPrctlModelChecker.cpp
  11. 5
      src/storm/modelchecker/prctl/SparseDtmcPrctlModelChecker.cpp
  12. 4
      src/storm/modelchecker/prctl/SparseMdpPrctlModelChecker.cpp
  13. 5
      src/storm/modelchecker/prctl/SymbolicDtmcPrctlModelChecker.cpp
  14. 5
      src/storm/modelchecker/prctl/SymbolicMdpPrctlModelChecker.cpp
  15. 7
      src/storm/modelchecker/reachability/SparseDtmcEliminationModelChecker.cpp
  16. 34
      src/storm/parser/FormulaParserGrammar.cpp
  17. 10
      src/storm/parser/FormulaParserGrammar.h
  18. 4
      src/storm/parser/JaniParser.cpp

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

@ -5,19 +5,12 @@
#include "storm/logic/FormulaVisitor.h"
#include "storm/exceptions/InvalidPropertyException.h"
namespace storm {
namespace logic {
BoundedUntilFormula::BoundedUntilFormula(std::shared_ptr<Formula const> const& leftSubformula, std::shared_ptr<Formula const> const& rightSubformula, double lowerBound, double upperBound) : BinaryPathFormula(leftSubformula, rightSubformula), bounds(std::make_pair(lowerBound, upperBound)) {
STORM_LOG_THROW(lowerBound >= 0 && upperBound >= 0, storm::exceptions::InvalidArgumentException, "Bounded until formula requires non-negative time bounds.");
STORM_LOG_THROW(lowerBound <= upperBound, storm::exceptions::InvalidArgumentException, "Lower bound of bounded until formula is required to be smaller than the upper bound.");
}
BoundedUntilFormula::BoundedUntilFormula(std::shared_ptr<Formula const> const& leftSubformula, std::shared_ptr<Formula const> const& rightSubformula, uint_fast64_t upperBound) : BinaryPathFormula(leftSubformula, rightSubformula), bounds(upperBound) {
// Intentionally left empty.
}
BoundedUntilFormula::BoundedUntilFormula(std::shared_ptr<Formula const> const& leftSubformula, std::shared_ptr<Formula const> const& rightSubformula, boost::variant<uint_fast64_t, std::pair<double, double>> const& bounds) : BinaryPathFormula(leftSubformula, rightSubformula), bounds(bounds) {
// Intentionally left empty.
BoundedUntilFormula::BoundedUntilFormula(std::shared_ptr<Formula const> const& leftSubformula, std::shared_ptr<Formula const> const& rightSubformula, boost::optional<UntilBound> const& lowerBound, boost::optional<UntilBound> const& upperBound, BoundedType const& boundedType) : BinaryPathFormula(leftSubformula, rightSubformula), lowerBound(lowerBound), upperBound(upperBound), boundedType(boundedType) {
STORM_LOG_THROW(lowerBound || upperBound, storm::exceptions::InvalidArgumentException, "Bounded until formula requires at least one bound.");
}
bool BoundedUntilFormula::isBoundedUntilFormula() const {
@ -31,28 +24,109 @@ namespace storm {
boost::any BoundedUntilFormula::accept(FormulaVisitor const& visitor, boost::any const& data) const {
return visitor.visit(*this, data);
}
bool BoundedUntilFormula::isStepBounded() const {
return boundedType == BoundedType::Steps;
}
bool BoundedUntilFormula::isTimeBounded() const {
return boundedType == BoundedType::Time;
}
bool BoundedUntilFormula::isLowerBoundStrict() const {
return lowerBound.get().isStrict();
}
bool BoundedUntilFormula::hasLowerBound() const {
return static_cast<bool>(lowerBound);
}
bool BoundedUntilFormula::hasIntegerLowerBound() const {
return lowerBound.get().getBound().hasIntegerType();
}
bool BoundedUntilFormula::isUpperBoundStrict() const {
return upperBound.get().isStrict();
}
bool BoundedUntilFormula::hasUpperBound() const {
return static_cast<bool>(upperBound);
}
bool BoundedUntilFormula::hasIntegerUpperBound() const {
return upperBound.get().getBound().hasIntegerType();
}
bool BoundedUntilFormula::hasDiscreteTimeBound() const {
return bounds.which() == 0;
storm::expressions::Expression const& BoundedUntilFormula::getLowerBound() const {
return lowerBound.get().getBound();
}
std::pair<double, double> const& BoundedUntilFormula::getIntervalBounds() const {
return boost::get<std::pair<double, double>>(bounds);
storm::expressions::Expression const& BoundedUntilFormula::getUpperBound() const {
return upperBound.get().getBound();
}
template <>
double BoundedUntilFormula::getLowerBound() const {
double bound = this->getLowerBound().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 bound = this->getUpperBound().evaluateAsDouble();
STORM_LOG_THROW(bound >= 0, storm::exceptions::InvalidPropertyException, "Time-bound must not evaluate to negative number.");
return bound;
}
template <>
uint64_t BoundedUntilFormula::getLowerBound() const {
int_fast64_t bound = this->getLowerBound().evaluateAsInt();
STORM_LOG_THROW(bound >= 0, storm::exceptions::InvalidPropertyException, "Time-bound must not evaluate to negative number.");
return static_cast<uint64_t>(bound);
}
uint_fast64_t BoundedUntilFormula::getDiscreteTimeBound() const {
return boost::get<uint_fast64_t>(bounds);
template <>
uint64_t BoundedUntilFormula::getUpperBound() const {
int_fast64_t bound = this->getUpperBound().evaluateAsInt();
STORM_LOG_THROW(bound >= 0, storm::exceptions::InvalidPropertyException, "Time-bound must not evaluate to negative number.");
return static_cast<uint64_t>(bound);
}
std::ostream& BoundedUntilFormula::writeToStream(std::ostream& out) const {
this->getLeftSubformula().writeToStream(out);
out << " U";
if (!this->hasDiscreteTimeBound()) {
std::pair<double, double> const& intervalBounds = getIntervalBounds();
out << "[" << intervalBounds.first << "," << intervalBounds.second << "] ";
if (this->hasLowerBound()) {
if (this->hasUpperBound()) {
if (this->isLowerBoundStrict()) {
out << "(";
} else {
out << "[";
}
out << this->getLowerBound();
out << ", ";
out << this->getUpperBound();
if (this->isUpperBoundStrict()) {
out << ")";
} else {
out << "]";
}
} else {
if (this->isLowerBoundStrict()) {
out << ">";
} else {
out << ">=";
}
out << getLowerBound();
}
} else {
out << "<=" << getDiscreteTimeBound() << " ";
if (this->isUpperBoundStrict()) {
out << "<";
} else {
out << "<=";
}
out << this->getUpperBound();
}
this->getRightSubformula().writeToStream(out);

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

@ -1,17 +1,32 @@
#ifndef STORM_LOGIC_BOUNDEDUNTILFORMULA_H_
#define STORM_LOGIC_BOUNDEDUNTILFORMULA_H_
#include <boost/variant.hpp>
#include <boost/optional.hpp>
#include "storm/logic/BinaryPathFormula.h"
namespace storm {
namespace logic {
class UntilBound {
public:
UntilBound(bool strict, storm::expressions::Expression bound);
storm::expressions::Expression const& getBound() const;
bool isStrict() const;
private:
bool strict;
storm::expressions::Expression bound;
};
class BoundedUntilFormula : public BinaryPathFormula {
public:
BoundedUntilFormula(std::shared_ptr<Formula const> const& leftSubformula, std::shared_ptr<Formula const> const& rightSubformula, double lowerBound, double upperBound);
BoundedUntilFormula(std::shared_ptr<Formula const> const& leftSubformula, std::shared_ptr<Formula const> const& rightSubformula, uint_fast64_t upperBound);
BoundedUntilFormula(std::shared_ptr<Formula const> const& leftSubformula, std::shared_ptr<Formula const> const& rightSubformula, boost::variant<uint_fast64_t, std::pair<double, double>> const& bounds);
enum class BoundedType {
Steps,
Time
};
BoundedUntilFormula(std::shared_ptr<Formula const> const& leftSubformula, std::shared_ptr<Formula const> const& rightSubformula, boost::optional<UntilBound> const& lowerBound, boost::optional<UntilBound> const& upperBound, BoundedType const& boundedType = BoundedType::Time);
virtual bool isBoundedUntilFormula() const override;
@ -19,15 +34,33 @@ namespace storm {
virtual boost::any accept(FormulaVisitor const& visitor, boost::any const& data) const override;
bool hasDiscreteTimeBound() const;
bool isStepBounded() const;
bool isTimeBounded() const;
std::pair<double, double> const& getIntervalBounds() const;
uint_fast64_t getDiscreteTimeBound() const;
bool isLowerBoundStrict() const;
bool hasLowerBound() const;
bool hasIntegerLowerBound() const;
bool isUpperBoundStrict() const;
bool hasUpperBound() const;
bool hasIntegerUpperBound() const;
storm::expressions::Expression const& getLowerBound() const;
storm::expressions::Expression const& getUpperBound() const;
template <typename ValueType>
ValueType getLowerBound() const;
template <typename ValueType>
ValueType getUpperBound() const;
virtual std::ostream& writeToStream(std::ostream& out) const override;
private:
boost::variant<uint_fast64_t, std::pair<double, double>> bounds;
BoundedType boundedType;
boost::optional<UntilBound> lowerBound;
boost::optional<UntilBound> upperBound;
};
}
}

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

@ -31,11 +31,7 @@ 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));
if (f.hasDiscreteTimeBound()) {
return std::static_pointer_cast<Formula>(std::make_shared<BoundedUntilFormula>(left, right, f.getDiscreteTimeBound()));
} else {
return std::static_pointer_cast<Formula>(std::make_shared<BoundedUntilFormula>(left, right, f.getIntervalBounds()));
}
return std::static_pointer_cast<Formula>(std::make_shared<BoundedUntilFormula>(f));
}
boost::any CloneVisitor::visit(ConditionalFormula const& f, boost::any const& data) const {

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

@ -58,7 +58,7 @@ namespace storm {
result = result && !f.getLeftSubformula().isPathFormula();
result = result && !f.getRightSubformula().isPathFormula();
}
if (f.hasDiscreteTimeBound()) {
if (f.isStepBounded()) {
result = result && inherited.getSpecification().areStepBoundedUntilFormulasAllowed();
} else {
result = result && inherited.getSpecification().areTimeBoundedUntilFormulasAllowed();

15
src/storm/modelchecker/csl/HybridCtmcCslModelChecker.cpp
View File

@ -12,6 +12,8 @@
#include "storm/logic/FragmentSpecification.h"
#include "storm/exceptions/NotImplementedException.h"
namespace storm {
namespace modelchecker {
template<typename ModelType>
@ -67,14 +69,17 @@ namespace storm {
std::unique_ptr<CheckResult> rightResultPointer = this->check(pathFormula.getRightSubformula());
SymbolicQualitativeCheckResult<DdType> const& leftResult = leftResultPointer->asSymbolicQualitativeCheckResult<DdType>();
SymbolicQualitativeCheckResult<DdType> const& rightResult = rightResultPointer->asSymbolicQualitativeCheckResult<DdType>();
STORM_LOG_THROW(!pathFormula.isStepBounded(), storm::exceptions::NotImplementedException, "Currently step-bounded properties on CTMCs are not supported.");
double lowerBound = 0;
double upperBound = 0;
if (!pathFormula.hasDiscreteTimeBound()) {
std::pair<double, double> const& intervalBounds = pathFormula.getIntervalBounds();
lowerBound = intervalBounds.first;
upperBound = intervalBounds.second;
if (pathFormula.hasLowerBound()) {
lowerBound = pathFormula.getLowerBound<double>();
}
if (pathFormula.hasUpperBound()) {
upperBound = pathFormula.getUpperBound<double>();
} else {
upperBound = pathFormula.getDiscreteTimeBound();
upperBound = storm::utility::infinity<double>();
}
return storm::modelchecker::helper::HybridCtmcCslHelper<DdType, ValueType>::computeBoundedUntilProbabilities(this->getModel(), this->getModel().getTransitionMatrix(), this->getModel().getExitRateVector(), leftResult.getTruthValuesVector(), rightResult.getTruthValuesVector(), checkTask.isQualitativeSet(), lowerBound, upperBound, *linearEquationSolverFactory);

15
src/storm/modelchecker/csl/SparseCtmcCslModelChecker.cpp
View File

@ -59,16 +59,19 @@ namespace storm {
std::unique_ptr<CheckResult> rightResultPointer = this->check(pathFormula.getRightSubformula());
ExplicitQualitativeCheckResult const& leftResult = leftResultPointer->asExplicitQualitativeCheckResult();;
ExplicitQualitativeCheckResult const& rightResult = rightResultPointer->asExplicitQualitativeCheckResult();
STORM_LOG_THROW(!pathFormula.isStepBounded(), storm::exceptions::NotImplementedException, "Currently step-bounded properties on CTMCs are not supported.");
double lowerBound = 0;
double upperBound = 0;
if (!pathFormula.hasDiscreteTimeBound()) {
std::pair<double, double> const& intervalBounds = pathFormula.getIntervalBounds();
lowerBound = intervalBounds.first;
upperBound = intervalBounds.second;
if (pathFormula.hasLowerBound()) {
lowerBound = pathFormula.getLowerBound<double>();
}
if (pathFormula.hasUpperBound()) {
upperBound = pathFormula.getUpperBound<double>();
} else {
upperBound = pathFormula.getDiscreteTimeBound();
upperBound = storm::utility::infinity<double>();
}
std::vector<ValueType> numericResult = storm::modelchecker::helper::SparseCtmcCslHelper::computeBoundedUntilProbabilities(this->getModel().getTransitionMatrix(), this->getModel().getBackwardTransitions(), leftResult.getTruthValuesVector(), rightResult.getTruthValuesVector(), this->getModel().getExitRateVector(), checkTask.isQualitativeSet(), lowerBound, upperBound, *linearEquationSolverFactory);
return std::unique_ptr<CheckResult>(new ExplicitQuantitativeCheckResult<ValueType>(std::move(numericResult)));
}

15
src/storm/modelchecker/csl/SparseMarkovAutomatonCslModelChecker.cpp
View File

@ -53,16 +53,19 @@ namespace storm {
STORM_LOG_THROW(this->getModel().isClosed(), storm::exceptions::InvalidPropertyException, "Unable to compute time-bounded reachability probabilities in non-closed Markov automaton.");
std::unique_ptr<CheckResult> rightResultPointer = this->check(pathFormula.getRightSubformula());
ExplicitQualitativeCheckResult const& rightResult = rightResultPointer->asExplicitQualitativeCheckResult();
STORM_LOG_THROW(!pathFormula.isStepBounded(), storm::exceptions::NotImplementedException, "Currently step-bounded properties on MAs are not supported.");
double lowerBound = 0;
double upperBound = 0;
if (!pathFormula.hasDiscreteTimeBound()) {
std::pair<double, double> const& intervalBounds = pathFormula.getIntervalBounds();
lowerBound = intervalBounds.first;
upperBound = intervalBounds.second;
if (pathFormula.hasLowerBound()) {
lowerBound = pathFormula.getLowerBound<double>();
}
if (pathFormula.hasUpperBound()) {
upperBound = pathFormula.getUpperBound<double>();
} else {
upperBound = pathFormula.getDiscreteTimeBound();
upperBound = storm::utility::infinity<double>();
}
std::vector<ValueType> result = storm::modelchecker::helper::SparseMarkovAutomatonCslHelper<ValueType>::computeBoundedUntilProbabilities(checkTask.getOptimizationDirection(), this->getModel().getTransitionMatrix(), this->getModel().getExitRates(), this->getModel().getMarkovianStates(), rightResult.getTruthValuesVector(), std::make_pair(lowerBound, upperBound), *minMaxLinearEquationSolverFactory);
return std::unique_ptr<CheckResult>(new ExplicitQuantitativeCheckResult<ValueType>(std::move(result)));
}

24
src/storm/modelchecker/multiobjective/pcaa/SparsePcaaPreprocessor.cpp
View File

@ -224,22 +224,20 @@ namespace storm {
template<typename SparseModelType>
void SparsePcaaPreprocessor<SparseModelType>::preprocessBoundedUntilFormula(storm::logic::BoundedUntilFormula const& formula, ReturnType& result, PcaaObjective<ValueType>& currentObjective) {
STORM_LOG_THROW(!result.originalModel.isOfType(storm::models::ModelType::MarkovAutomaton) || !formula.isStepBounded(), storm::exceptions::InvalidPropertyException, "Multi-objective model checking currently does not support step-bounded properties for Markov automata.");
if(formula.hasDiscreteTimeBound()) {
currentObjective.upperTimeBound = storm::utility::convertNumber<ValueType>(formula.getDiscreteTimeBound());
if (formula.hasLowerBound()) {
STORM_LOG_THROW(!result.originalModel.isOfType(storm::models::ModelType::Mdp) || formula.hasIntegerLowerBound(), storm::exceptions::InvalidPropertyException, "Expected discrete lower time-bound in formula.");
currentObjective.lowerTimeBound = formula.getLowerBound<ValueType>();
}
if (formula.hasUpperBound()) {
STORM_LOG_THROW(!result.originalModel.isOfType(storm::models::ModelType::Mdp) || formula.hasIntegerUpperBound(), storm::exceptions::InvalidPropertyException, "Expected discrete lower time-bound in formula.");
currentObjective.upperTimeBound = formula.getUpperBound<ValueType>();
} else {
if(result.originalModel.isOfType(storm::models::ModelType::Mdp)) {
STORM_LOG_THROW(formula.getIntervalBounds().first == std::round(formula.getIntervalBounds().first), storm::exceptions::InvalidPropertyException, "Expected a boundedUntilFormula with discrete lower time bound but got " << formula << ".");
STORM_LOG_THROW(formula.getIntervalBounds().second == std::round(formula.getIntervalBounds().second), storm::exceptions::InvalidPropertyException, "Expected a boundedUntilFormula with discrete upper time bound but got " << formula << ".");
} else {
STORM_LOG_THROW(result.originalModel.isOfType(storm::models::ModelType::MarkovAutomaton), storm::exceptions::InvalidPropertyException, "Got a boundedUntilFormula which can not be checked for the current model type.");
STORM_LOG_THROW(formula.getIntervalBounds().second > formula.getIntervalBounds().first, storm::exceptions::InvalidPropertyException, "Neither empty nor point intervalls are allowed but got " << formula << ".");
}
if(!storm::utility::isZero(formula.getIntervalBounds().first)) {
currentObjective.lowerTimeBound = storm::utility::convertNumber<ValueType>(formula.getIntervalBounds().first);
}
currentObjective.upperTimeBound = storm::utility::convertNumber<ValueType>(formula.getIntervalBounds().second);
currentObjective.upperTimeBound = storm::utility::infinity<ValueType>();
}
STORM_LOG_THROW(currentObjective.lowerTimeBound < currentObjective.upperTimeBound, storm::exceptions::InvalidPropertyException, "Empty or point time intervals are currently not supported by multi-objective model checking.");
preprocessUntilFormula(storm::logic::UntilFormula(formula.getLeftSubformula().asSharedPointer(), formula.getRightSubformula().asSharedPointer()), result, currentObjective);
}

5
src/storm/modelchecker/prctl/HybridDtmcPrctlModelChecker.cpp
View File

@ -70,12 +70,13 @@ namespace storm {
template<typename ModelType>
std::unique_ptr<CheckResult> HybridDtmcPrctlModelChecker<ModelType>::computeBoundedUntilProbabilities(CheckTask<storm::logic::BoundedUntilFormula, ValueType> const& checkTask) {
storm::logic::BoundedUntilFormula const& pathFormula = checkTask.getFormula();
STORM_LOG_THROW(pathFormula.hasDiscreteTimeBound(), storm::exceptions::InvalidArgumentException, "Formula needs to have a discrete time bound.");
STORM_LOG_THROW(!pathFormula.hasLowerBound() && pathFormula.hasUpperBound(), storm::exceptions::InvalidPropertyException, "Formula needs to have single upper time bound.");
STORM_LOG_THROW(pathFormula.hasIntegerUpperBound(), storm::exceptions::InvalidPropertyException, "Formula needs to have discrete upper time bound.");
std::unique_ptr<CheckResult> leftResultPointer = this->check(pathFormula.getLeftSubformula());
std::unique_ptr<CheckResult> rightResultPointer = this->check(pathFormula.getRightSubformula());
SymbolicQualitativeCheckResult<DdType> const& leftResult = leftResultPointer->asSymbolicQualitativeCheckResult<DdType>();
SymbolicQualitativeCheckResult<DdType> const& rightResult = rightResultPointer->asSymbolicQualitativeCheckResult<DdType>();
return storm::modelchecker::helper::HybridDtmcPrctlHelper<DdType, ValueType>::computeBoundedUntilProbabilities(this->getModel(), this->getModel().getTransitionMatrix(), leftResult.getTruthValuesVector(), rightResult.getTruthValuesVector(), pathFormula.getDiscreteTimeBound(), *this->linearEquationSolverFactory);
return storm::modelchecker::helper::HybridDtmcPrctlHelper<DdType, ValueType>::computeBoundedUntilProbabilities(this->getModel(), this->getModel().getTransitionMatrix(), leftResult.getTruthValuesVector(), rightResult.getTruthValuesVector(), pathFormula.getUpperBound<uint64_t>(), *this->linearEquationSolverFactory);
}
template<typename ModelType>

5
src/storm/modelchecker/prctl/HybridMdpPrctlModelChecker.cpp
View File

@ -68,12 +68,13 @@ namespace storm {
std::unique_ptr<CheckResult> HybridMdpPrctlModelChecker<ModelType>::computeBoundedUntilProbabilities(CheckTask<storm::logic::BoundedUntilFormula, ValueType> const& checkTask) {
storm::logic::BoundedUntilFormula const& pathFormula = checkTask.getFormula();
STORM_LOG_THROW(checkTask.isOptimizationDirectionSet(), storm::exceptions::InvalidPropertyException, "Formula needs to specify whether minimal or maximal values are to be computed on nondeterministic model.");
STORM_LOG_THROW(pathFormula.hasDiscreteTimeBound(), storm::exceptions::InvalidPropertyException, "Formula needs to have a discrete time bound.");
STORM_LOG_THROW(!pathFormula.hasLowerBound() && pathFormula.hasUpperBound(), storm::exceptions::InvalidPropertyException, "Formula needs to have single upper time bound.");
STORM_LOG_THROW(pathFormula.hasIntegerUpperBound(), storm::exceptions::InvalidPropertyException, "Formula needs to have discrete upper time bound.");
std::unique_ptr<CheckResult> leftResultPointer = this->check(pathFormula.getLeftSubformula());
std::unique_ptr<CheckResult> rightResultPointer = this->check(pathFormula.getRightSubformula());
SymbolicQualitativeCheckResult<DdType> const& leftResult = leftResultPointer->asSymbolicQualitativeCheckResult<DdType>();
SymbolicQualitativeCheckResult<DdType> const& rightResult = rightResultPointer->asSymbolicQualitativeCheckResult<DdType>();
return storm::modelchecker::helper::HybridMdpPrctlHelper<DdType, ValueType>::computeBoundedUntilProbabilities(checkTask.getOptimizationDirection(), this->getModel(), this->getModel().getTransitionMatrix(), leftResult.getTruthValuesVector(), rightResult.getTruthValuesVector(), pathFormula.getDiscreteTimeBound(), *this->linearEquationSolverFactory);
return storm::modelchecker::helper::HybridMdpPrctlHelper<DdType, ValueType>::computeBoundedUntilProbabilities(checkTask.getOptimizationDirection(), this->getModel(), this->getModel().getTransitionMatrix(), leftResult.getTruthValuesVector(), rightResult.getTruthValuesVector(), pathFormula.getUpperBound<uint64_t>(), *this->linearEquationSolverFactory);
}
template<typename ModelType>

5
src/storm/modelchecker/prctl/SparseDtmcPrctlModelChecker.cpp
View File

@ -42,12 +42,13 @@ namespace storm {
template<typename SparseDtmcModelType>
std::unique_ptr<CheckResult> SparseDtmcPrctlModelChecker<SparseDtmcModelType>::computeBoundedUntilProbabilities(CheckTask<storm::logic::BoundedUntilFormula, ValueType> const& checkTask) {
storm::logic::BoundedUntilFormula const& pathFormula = checkTask.getFormula();
STORM_LOG_THROW(pathFormula.hasDiscreteTimeBound(), storm::exceptions::InvalidPropertyException, "Formula needs to have a discrete time bound.");
STORM_LOG_THROW(!pathFormula.hasLowerBound() && pathFormula.hasUpperBound(), storm::exceptions::InvalidPropertyException, "Formula needs to have single upper time bound.");
STORM_LOG_THROW(pathFormula.hasIntegerUpperBound(), storm::exceptions::InvalidPropertyException, "Formula needs to have discrete upper time bound.");
std::unique_ptr<CheckResult> leftResultPointer = this->check(pathFormula.getLeftSubformula());
std::unique_ptr<CheckResult> rightResultPointer = this->check(pathFormula.getRightSubformula());
ExplicitQualitativeCheckResult const& leftResult = leftResultPointer->asExplicitQualitativeCheckResult();
ExplicitQualitativeCheckResult const& rightResult = rightResultPointer->asExplicitQualitativeCheckResult();
std::vector<ValueType> numericResult = storm::modelchecker::helper::SparseDtmcPrctlHelper<ValueType>::computeBoundedUntilProbabilities(this->getModel().getTransitionMatrix(), this->getModel().getBackwardTransitions(), leftResult.getTruthValuesVector(), rightResult.getTruthValuesVector(), pathFormula.getDiscreteTimeBound(), *linearEquationSolverFactory);
std::vector<ValueType> numericResult = storm::modelchecker::helper::SparseDtmcPrctlHelper<ValueType>::computeBoundedUntilProbabilities(this->getModel().getTransitionMatrix(), this->getModel().getBackwardTransitions(), leftResult.getTruthValuesVector(), rightResult.getTruthValuesVector(), pathFormula.getUpperBound<uint64_t>(), *linearEquationSolverFactory);
std::unique_ptr<CheckResult> result = std::unique_ptr<CheckResult>(new ExplicitQuantitativeCheckResult<ValueType>(std::move(numericResult)));
return result;
}

4
src/storm/modelchecker/prctl/SparseMdpPrctlModelChecker.cpp
View File

@ -58,11 +58,13 @@ namespace storm {
std::unique_ptr<CheckResult> SparseMdpPrctlModelChecker<SparseMdpModelType>::computeBoundedUntilProbabilities(CheckTask<storm::logic::BoundedUntilFormula, ValueType> const& checkTask) {
storm::logic::BoundedUntilFormula const& pathFormula = checkTask.getFormula();
STORM_LOG_THROW(checkTask.isOptimizationDirectionSet(), storm::exceptions::InvalidArgumentException, "Formula needs to specify whether minimal or maximal values are to be computed on nondeterministic model.");
STORM_LOG_THROW(!pathFormula.hasLowerBound() && pathFormula.hasUpperBound(), storm::exceptions::InvalidPropertyException, "Formula needs to have single upper time bound.");
STORM_LOG_THROW(pathFormula.hasIntegerUpperBound(), storm::exceptions::InvalidPropertyException, "Formula needs to have discrete upper time bound.");
std::unique_ptr<CheckResult> leftResultPointer = this->check(pathFormula.getLeftSubformula());
std::unique_ptr<CheckResult> rightResultPointer = this->check(pathFormula.getRightSubformula());
ExplicitQualitativeCheckResult const& leftResult = leftResultPointer->asExplicitQualitativeCheckResult();
ExplicitQualitativeCheckResult const& rightResult = rightResultPointer->asExplicitQualitativeCheckResult();
std::vector<ValueType> numericResult = storm::modelchecker::helper::SparseMdpPrctlHelper<ValueType>::computeBoundedUntilProbabilities(checkTask.getOptimizationDirection(), this->getModel().getTransitionMatrix(), this->getModel().getBackwardTransitions(), leftResult.getTruthValuesVector(), rightResult.getTruthValuesVector(), pathFormula.getDiscreteTimeBound(), *minMaxLinearEquationSolverFactory);
std::vector<ValueType> numericResult = storm::modelchecker::helper::SparseMdpPrctlHelper<ValueType>::computeBoundedUntilProbabilities(checkTask.getOptimizationDirection(), this->getModel().getTransitionMatrix(), this->getModel().getBackwardTransitions(), leftResult.getTruthValuesVector(), rightResult.getTruthValuesVector(), pathFormula.getUpperBound<uint64_t>(), *minMaxLinearEquationSolverFactory);
return std::unique_ptr<CheckResult>(new ExplicitQuantitativeCheckResult<ValueType>(std::move(numericResult)));
}

5
src/storm/modelchecker/prctl/SymbolicDtmcPrctlModelChecker.cpp
View File

@ -70,12 +70,13 @@ namespace storm {
template<typename ModelType>
std::unique_ptr<CheckResult> SymbolicDtmcPrctlModelChecker<ModelType>::computeBoundedUntilProbabilities(CheckTask<storm::logic::BoundedUntilFormula, ValueType> const& checkTask) {
storm::logic::BoundedUntilFormula const& pathFormula = checkTask.getFormula();
STORM_LOG_THROW(pathFormula.hasDiscreteTimeBound(), storm::exceptions::InvalidPropertyException, "Formula needs to have a discrete time bound.");
STORM_LOG_THROW(!pathFormula.hasLowerBound() && pathFormula.hasUpperBound(), storm::exceptions::InvalidPropertyException, "Formula needs to have single upper time bound.");
STORM_LOG_THROW(pathFormula.hasIntegerUpperBound(), storm::exceptions::InvalidPropertyException, "Formula needs to have discrete upper time bound.");
std::unique_ptr<CheckResult> leftResultPointer = this->check(pathFormula.getLeftSubformula());
std::unique_ptr<CheckResult> rightResultPointer = this->check(pathFormula.getRightSubformula());
SymbolicQualitativeCheckResult<DdType> const& leftResult = leftResultPointer->asSymbolicQualitativeCheckResult<DdType>();
SymbolicQualitativeCheckResult<DdType> const& rightResult = rightResultPointer->asSymbolicQualitativeCheckResult<DdType>();
storm::dd::Add<DdType> numericResult = storm::modelchecker::helper::SymbolicDtmcPrctlHelper<DdType, ValueType>::computeBoundedUntilProbabilities(this->getModel(), this->getModel().getTransitionMatrix(), leftResult.getTruthValuesVector(), rightResult.getTruthValuesVector(), pathFormula.getDiscreteTimeBound(), *this->linearEquationSolverFactory);
storm::dd::Add<DdType> numericResult = storm::modelchecker::helper::SymbolicDtmcPrctlHelper<DdType, ValueType>::computeBoundedUntilProbabilities(this->getModel(), this->getModel().getTransitionMatrix(), leftResult.getTruthValuesVector(), rightResult.getTruthValuesVector(), pathFormula.getUpperBound<uint64_t>(), *this->linearEquationSolverFactory);
return std::unique_ptr<SymbolicQuantitativeCheckResult<DdType>>(new SymbolicQuantitativeCheckResult<DdType>(this->getModel().getReachableStates(), numericResult));
}

5
src/storm/modelchecker/prctl/SymbolicMdpPrctlModelChecker.cpp
View File

@ -70,12 +70,13 @@ namespace storm {
std::unique_ptr<CheckResult> SymbolicMdpPrctlModelChecker<ModelType>::computeBoundedUntilProbabilities(CheckTask<storm::logic::BoundedUntilFormula, ValueType> const& checkTask) {
storm::logic::BoundedUntilFormula const& pathFormula = checkTask.getFormula();
STORM_LOG_THROW(checkTask.isOptimizationDirectionSet(), storm::exceptions::InvalidArgumentException, "Formula needs to specify whether minimal or maximal values are to be computed on nondeterministic model.");
STORM_LOG_THROW(pathFormula.hasDiscreteTimeBound(), storm::exceptions::InvalidPropertyException, "Formula needs to have a discrete time bound.");
STORM_LOG_THROW(!pathFormula.hasLowerBound() && pathFormula.hasUpperBound(), storm::exceptions::InvalidPropertyException, "Formula needs to have single upper time bound.");
STORM_LOG_THROW(pathFormula.hasIntegerUpperBound(), storm::exceptions::InvalidPropertyException, "Formula needs to have discrete upper time bound.");
std::unique_ptr<CheckResult> leftResultPointer = this->check(pathFormula.getLeftSubformula());
std::unique_ptr<CheckResult> rightResultPointer = this->check(pathFormula.getRightSubformula());
SymbolicQualitativeCheckResult<DdType> const& leftResult = leftResultPointer->asSymbolicQualitativeCheckResult<DdType>();
SymbolicQualitativeCheckResult<DdType> const& rightResult = rightResultPointer->asSymbolicQualitativeCheckResult<DdType>();
return storm::modelchecker::helper::SymbolicMdpPrctlHelper<DdType, ValueType>::computeBoundedUntilProbabilities(checkTask.getOptimizationDirection(), this->getModel(), this->getModel().getTransitionMatrix(), leftResult.getTruthValuesVector(), rightResult.getTruthValuesVector(), pathFormula.getDiscreteTimeBound(), *this->linearEquationSolverFactory);
return storm::modelchecker::helper::SymbolicMdpPrctlHelper<DdType, ValueType>::computeBoundedUntilProbabilities(checkTask.getOptimizationDirection(), this->getModel(), this->getModel().getTransitionMatrix(), leftResult.getTruthValuesVector(), rightResult.getTruthValuesVector(), pathFormula.getUpperBound<uint64_t>(), *this->linearEquationSolverFactory);
}
template<typename ModelType>

7
src/storm/modelchecker/reachability/SparseDtmcEliminationModelChecker.cpp
View File

@ -323,6 +323,9 @@ namespace storm {
std::unique_ptr<CheckResult> SparseDtmcEliminationModelChecker<SparseDtmcModelType>::computeBoundedUntilProbabilities(CheckTask<storm::logic::BoundedUntilFormula, ValueType> const& checkTask) {
storm::logic::BoundedUntilFormula const& pathFormula = checkTask.getFormula();
STORM_LOG_THROW(!pathFormula.hasLowerBound() && pathFormula.hasUpperBound(), storm::exceptions::InvalidPropertyException, "Formula needs to have single upper time bound.");
STORM_LOG_THROW(pathFormula.hasIntegerUpperBound(), storm::exceptions::InvalidPropertyException, "Formula needs to have discrete upper time bound.");
// Retrieve the appropriate bitvectors by model checking the subformulas.
std::unique_ptr<CheckResult> leftResultPointer = this->check(pathFormula.getLeftSubformula());
std::unique_ptr<CheckResult> rightResultPointer = this->check(pathFormula.getRightSubformula());
@ -331,7 +334,7 @@ namespace storm {
// Start by determining the states that have a non-zero probability of reaching the target states within the
// time bound.
storm::storage::BitVector statesWithProbabilityGreater0 = storm::utility::graph::performProbGreater0(this->getModel().getBackwardTransitions(), phiStates, psiStates, true, pathFormula.getDiscreteTimeBound());
storm::storage::BitVector statesWithProbabilityGreater0 = storm::utility::graph::performProbGreater0(this->getModel().getBackwardTransitions(), phiStates, psiStates, true, pathFormula.getUpperBound<uint64_t>());
statesWithProbabilityGreater0 &= ~psiStates;
// Determine whether we need to perform some further computation.
@ -350,7 +353,7 @@ namespace storm {
std::vector<ValueType> result(transitionMatrix.getRowCount(), storm::utility::zero<ValueType>());
if (furtherComputationNeeded) {
uint_fast64_t timeBound = pathFormula.getDiscreteTimeBound();
uint_fast64_t timeBound = pathFormula.getUpperBound<uint64_t>();
if (checkTask.isOnlyInitialStatesRelevantSet()) {
// Determine the set of states that is reachable from the initial state without jumping over a target state.

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

@ -66,7 +66,7 @@ namespace storm {
conditionalFormula = untilFormula(qi::_r1)[qi::_val = qi::_1] >> *(qi::lit("||") >> untilFormula(storm::logic::FormulaContext::Probability))[qi::_val = phoenix::bind(&FormulaParserGrammar::createConditionalFormula, phoenix::ref(*this), qi::_val, qi::_1, qi::_r1)];
conditionalFormula.name("conditional formula");
timeBound = (qi::lit("[") > qi::double_ > qi::lit(",") > qi::double_ > qi::lit("]"))[qi::_val = phoenix::construct<std::pair<double, double>>(qi::_1, qi::_2)] | (qi::lit("<=") >> strict_double)[qi::_val = phoenix::construct<std::pair<double, double>>(0, qi::_1)] | (qi::lit("<=") > qi::uint_)[qi::_val = qi::_1];
timeBound = (qi::lit("[") > expressionParser > qi::lit(",") > expressionParser > qi::lit("]"))[qi::_val = phoenix::bind(&FormulaParserGrammar::createTimeBoundFromInterval, phoenix::ref(*this), qi::_1, qi::_2)] | ((qi::lit("<=")[qi::_a = true, qi::_b = false] | qi::lit("<")[qi::_a = true, qi::_b = true] | qi::lit(">=")[qi::_a = false, qi::_b = false] | qi::lit(">")[qi::_a = false, qi::_b = true]) >> expressionParser)[qi::_val = phoenix::bind(&FormulaParserGrammar::createTimeBoundFromSingleBound, phoenix::ref(*this), qi::_1, qi::_a, qi::_b)];
timeBound.name("time bound");
pathFormula = conditionalFormula(qi::_r1);
@ -167,6 +167,20 @@ namespace storm {
this->identifiers_.add(identifier, expression);
}
std::pair<boost::optional<storm::logic::UntilBound>, boost::optional<storm::logic::UntilBound>> FormulaParserGrammar::createTimeBoundFromInterval(storm::expressions::Expression const& lowerBound, storm::expressions::Expression const& upperBound) const {
storm::logic::UntilBound lower(false, lowerBound);
storm::logic::UntilBound upper(false, upperBound);
return std::make_pair(lower, upper);
}
std::pair<boost::optional<storm::logic::UntilBound>, boost::optional<storm::logic::UntilBound>> FormulaParserGrammar::createTimeBoundFromSingleBound(storm::expressions::Expression const& bound, bool upperBound, bool strict) const {
if (upperBound) {
return std::make_pair(boost::none, storm::logic::UntilBound(strict, bound));
} else {
return std::make_pair(storm::logic::UntilBound(strict, bound), boost::none);
}
}
std::shared_ptr<storm::logic::Formula const> FormulaParserGrammar::createInstantaneousRewardFormula(boost::variant<unsigned, double> const& timeBound) const {
if (timeBound.which() == 0) {
return std::shared_ptr<storm::logic::Formula const>(new storm::logic::InstantaneousRewardFormula(static_cast<uint_fast64_t>(boost::get<unsigned>(timeBound))));
@ -208,14 +222,9 @@ namespace storm {
return std::shared_ptr<storm::logic::Formula const>(new storm::logic::AtomicLabelFormula(label));
}
std::shared_ptr<storm::logic::Formula const> FormulaParserGrammar::createEventuallyFormula(boost::optional<boost::variant<std::pair<double, double>, uint_fast64_t>> const& timeBound, storm::logic::FormulaContext context, std::shared_ptr<storm::logic::Formula const> const& subformula) const {
std::shared_ptr<storm::logic::Formula const> FormulaParserGrammar::createEventuallyFormula(boost::optional<std::pair<boost::optional<storm::logic::UntilBound>, boost::optional<storm::logic::UntilBound>>> const& timeBound, storm::logic::FormulaContext context, std::shared_ptr<storm::logic::Formula const> const& subformula) const {
if (timeBound) {
if (timeBound.get().which() == 0) {
std::pair<double, double> const& bounds = boost::get<std::pair<double, double>>(timeBound.get());
return std::shared_ptr<storm::logic::Formula const>(new storm::logic::BoundedUntilFormula(createBooleanLiteralFormula(true), subformula, bounds.first, bounds.second));
} else {
return std::shared_ptr<storm::logic::Formula const>(new storm::logic::BoundedUntilFormula(createBooleanLiteralFormula(true), subformula, static_cast<uint_fast64_t>(boost::get<uint_fast64_t>(timeBound.get()))));
}
return std::shared_ptr<storm::logic::Formula const>(new storm::logic::BoundedUntilFormula(createBooleanLiteralFormula(true), subformula, timeBound.get().first, timeBound.get().second, storm::logic::BoundedUntil::BoundedType::Time));
} else {
return std::shared_ptr<storm::logic::Formula const>(new storm::logic::EventuallyFormula(subformula, context));
}
@ -229,14 +238,9 @@ namespace storm {
return std::shared_ptr<storm::logic::Formula const>(new storm::logic::NextFormula(subformula));
}
std::shared_ptr<storm::logic::Formula const> FormulaParserGrammar::createUntilFormula(std::shared_ptr<storm::logic::Formula const> const& leftSubformula, boost::optional<boost::variant<std::pair<double, double>, uint_fast64_t>> const& timeBound, std::shared_ptr<storm::logic::Formula const> const& rightSubformula) {
std::shared_ptr<storm::logic::Formula const> FormulaParserGrammar::createUntilFormula(std::shared_ptr<storm::logic::Formula const> const& leftSubformula, boost::optional<std::pair<boost::optional<storm::logic::UntilBound>, boost::optional<storm::logic::UntilBound>>> const& timeBound, std::shared_ptr<storm::logic::Formula const> const& rightSubformula) {
if (timeBound) {
if (timeBound.get().which() == 0) {
std::pair<double, double> const& bounds = boost::get<std::pair<double, double>>(timeBound.get());
return std::shared_ptr<storm::logic::Formula const>(new storm::logic::BoundedUntilFormula(leftSubformula, rightSubformula, bounds.first, bounds.second));
} else {
return std::shared_ptr<storm::logic::Formula const>(new storm::logic::BoundedUntilFormula(leftSubformula, rightSubformula, static_cast<uint_fast64_t>(boost::get<uint_fast64_t>(timeBound.get()))));
}
return std::shared_ptr<storm::logic::Formula const>(new storm::logic::BoundedUntilFormula(leftSubformula, rightSubformula, timeBound.get().first, timeBound.get().second, storm::logic::BoundedUntil::BoundedType::Time));
} else {
return std::shared_ptr<storm::logic::Formula const>(new storm::logic::UntilFormula(leftSubformula, rightSubformula));
}

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

@ -148,7 +148,8 @@ namespace storm {
qi::rule<Iterator, std::shared_ptr<storm::logic::Formula const>(storm::logic::FormulaContext), Skipper> nextFormula;
qi::rule<Iterator, std::shared_ptr<storm::logic::Formula const>(storm::logic::FormulaContext), Skipper> globallyFormula;
qi::rule<Iterator, std::shared_ptr<storm::logic::Formula const>(storm::logic::FormulaContext), Skipper> untilFormula;
qi::rule<Iterator, boost::variant<std::pair<double, double>, uint_fast64_t>(), Skipper> timeBound;
qi::rule<Iterator, std::pair<boost::optional<storm::logic::UntilBound>>(), qi::locals<bool, bool>, Skipper> timeBound;
qi::rule<Iterator, std::shared_ptr<storm::logic::Formula const>(), Skipper> rewardPathFormula;
qi::rule<Iterator, std::shared_ptr<storm::logic::Formula const>(), Skipper> cumulativeRewardFormula;
@ -160,6 +161,9 @@ namespace storm {
// 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;
std::pair<boost::optional<storm::logic::UntilBound>, boost::optional<storm::logic::UntilBound>> createTimeBoundFromInterval(storm::expressions::Expression const& lowerBound, storm::expressions::Expression const& upperBound) const;
std::pair<boost::optional<storm::logic::UntilBound>, boost::optional<storm::logic::UntilBound>> createTimeBoundFromSingleBound(storm::expressions::Expression const& bound, bool upperBound, bool strict) const;
// Methods that actually create the expression objects.
std::shared_ptr<storm::logic::Formula const> createInstantaneousRewardFormula(boost::variant<unsigned, double> const& timeBound) const;
@ -169,10 +173,10 @@ namespace storm {
std::shared_ptr<storm::logic::Formula const> createAtomicExpressionFormula(storm::expressions::Expression const& expression) const;
std::shared_ptr<storm::logic::Formula const> createBooleanLiteralFormula(bool literal) const;
std::shared_ptr<storm::logic::Formula const> createAtomicLabelFormula(std::string const& label) const;
std::shared_ptr<storm::logic::Formula const> createEventuallyFormula(boost::optional<boost::variant<std::pair<double, double>, uint_fast64_t>> const& timeBound, storm::logic::FormulaContext context, std::shared_ptr<storm::logic::Formula const> const& subformula) const;
std::shared_ptr<storm::logic::Formula const> createEventuallyFormula(boost::optional<std::pair<boost::optional<storm::logic::UntilBound>, boost::optional<storm::logic::UntilBound>>> const& timeBound, storm::logic::FormulaContext context, std::shared_ptr<storm::logic::Formula const> const& subformula) const;
std::shared_ptr<storm::logic::Formula const> createGloballyFormula(std::shared_ptr<storm::logic::Formula const> const& subformula) const;
std::shared_ptr<storm::logic::Formula const> createNextFormula(std::shared_ptr<storm::logic::Formula const> const& subformula) const;
std::shared_ptr<storm::logic::Formula const> createUntilFormula(std::shared_ptr<storm::logic::Formula const> const& leftSubformula, boost::optional<boost::variant<std::pair<double, double>, uint_fast64_t>> const& timeBound, std::shared_ptr<storm::logic::Formula const> const& rightSubformula);
std::shared_ptr<storm::logic::Formula const> createUntilFormula(std::shared_ptr<storm::logic::Formula const> const& leftSubformula, boost::optional<std::pair<boost::optional<storm::logic::UntilBound>, boost::optional<storm::logic::UntilBound>>> const& timeBound, std::shared_ptr<storm::logic::Formula const> const& rightSubformula);
std::shared_ptr<storm::logic::Formula const> createConditionalFormula(std::shared_ptr<storm::logic::Formula const> const& leftSubformula, std::shared_ptr<storm::logic::Formula const> const& rightSubformula, storm::logic::FormulaContext context) const;
storm::logic::OperatorInformation createOperatorInformation(boost::optional<storm::OptimizationDirection> const& optimizationDirection, boost::optional<storm::logic::ComparisonType> const& comparisonType, boost::optional<storm::expressions::Expression> const& threshold) const;
std::shared_ptr<storm::logic::Formula const> createLongRunAverageOperatorFormula(storm::logic::OperatorInformation const& operatorInformation, std::shared_ptr<storm::logic::Formula const> const& subformula) const;

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

@ -345,7 +345,7 @@ namespace storm {
upperBound--;
}
STORM_LOG_THROW(upperBound >= 0, storm::exceptions::InvalidJaniException, "Step-bounds cannot be negative");
return std::make_shared<storm::logic::BoundedUntilFormula const>(args[0], args[1], upperBound);
return std::make_shared<storm::logic::BoundedUntilFormula const>(args[0], args[1], std::make_pair(pi.lowerBound, !pi.lowerBoundStrict), std::make_pair(pi.upperBound, !pi.upperBoundStrict), storm::logic::BoundedUntilFormula::BoundedType::Steps);
} else if (propertyStructure.count("time-bounds") > 0) {
storm::jani::PropertyInterval pi = parsePropertyInterval(propertyStructure.at("time-bounds"));
STORM_LOG_THROW(pi.hasUpperBound(), storm::exceptions::NotSupportedException, "Storm only supports time-bounded until with an upper bound.");
@ -356,7 +356,7 @@ namespace storm {
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");
return std::make_shared<storm::logic::BoundedUntilFormula const>(args[0], args[1], upperBound);
return std::make_shared<storm::logic::BoundedUntilFormula const>(args[0], args[1], std::make_pair(pi.lowerBound, !pi.lowerBoundStrict), std::make_pair(pi.upperBound, !pi.upperBoundStrict), storm::logic::BoundedUntilFormula::BoundedType::Time);
} else if (propertyStructure.count("reward-bounds") > 0 ) {
STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "Reward bounded properties are not supported by Storm");

Write Preview
Loading…
Cancel
Save