diff --git a/src/storm/cli/cli.cpp b/src/storm/cli/cli.cpp index aaa601d15..84c7c1c96 100644 --- a/src/storm/cli/cli.cpp +++ b/src/storm/cli/cli.cpp @@ -247,19 +247,30 @@ namespace storm { // Then proceed to parsing the properties (if given), since the model we are building may depend on the property. STORM_LOG_TRACE("Parsing properties."); uint64_t i = 0; + + // Get the string that assigns values to the unknown currently undefined constants in the model and formula. + std::string constantDefinitionString = ioSettings.getConstantDefinitionString(); + std::map constantDefinitions; + if (storm::settings::getModule().isPropertySet()) { + std::vector> formulas; if (model.isJaniModel()) { - for(auto const& formula : storm::parseFormulasForJaniModel(storm::settings::getModule().getProperty(), model.asJaniModel())) { - properties.emplace_back(std::to_string(i), formula); - ++i; - } + formulas = storm::parseFormulasForJaniModel(storm::settings::getModule().getProperty(), model.asJaniModel()); } else { - for(auto const& formula :storm::parseFormulasForPrismProgram(storm::settings::getModule().getProperty(), model.asPrismProgram())) { - properties.emplace_back(std::to_string(i), formula); - ++i; - } + formulas = storm::parseFormulasForPrismProgram(storm::settings::getModule().getProperty(), model.asPrismProgram()); } + + constantDefinitions = model.parseConstantDefinitions(constantDefinitionString); + formulas = substituteConstantsInFormulas(formulas, constantDefinitions); + + for (auto const& formula : formulas) { + properties.emplace_back(std::to_string(i), formula); + ++i; + } + } else { + constantDefinitions = model.parseConstantDefinitions(constantDefinitionString); } + model = model.preprocess(constantDefinitions); if (model.isJaniModel() && storm::settings::getModule().isJaniFileSet()) { exportJaniModel(model.asJaniModel(), properties, storm::settings::getModule().getJaniFilename()); @@ -269,10 +280,6 @@ namespace storm { return; } - // Get the string that assigns values to the unknown currently undefined constants in the model. - std::string constantDefinitionString = ioSettings.getConstantDefinitionString(); - model = model.preprocess(constantDefinitionString); - STORM_LOG_TRACE("Building and checking symbolic model."); if (storm::settings::getModule().isParametricSet()) { #ifdef STORM_HAVE_CARL diff --git a/src/storm/counterexamples/SMTMinimalCommandSetGenerator.h b/src/storm/counterexamples/SMTMinimalCommandSetGenerator.h index 6971992d4..e30aade7b 100644 --- a/src/storm/counterexamples/SMTMinimalCommandSetGenerator.h +++ b/src/storm/counterexamples/SMTMinimalCommandSetGenerator.h @@ -14,7 +14,7 @@ #include "storm/settings/modules/CoreSettings.h" #include "storm/utility/counterexamples.h" -#include "storm/utility/prism.h" +#include "storm/utility/cli.h" namespace storm { namespace counterexamples { @@ -1612,7 +1612,7 @@ namespace storm { auto analysisClock = std::chrono::high_resolution_clock::now(); decltype(std::chrono::high_resolution_clock::now() - analysisClock) totalAnalysisTime(0); - std::map constantDefinitions = storm::utility::prism::parseConstantDefinitionString(program, constantDefinitionString); + std::map constantDefinitions = storm::utility::cli::parseConstantDefinitionString(program.getManager(), constantDefinitionString); storm::prism::Program preparedProgram = program.defineUndefinedConstants(constantDefinitions); preparedProgram = preparedProgram.substituteConstants(); diff --git a/src/storm/logic/BoundedUntilFormula.cpp b/src/storm/logic/BoundedUntilFormula.cpp index b3bc3ea1a..67ece142a 100644 --- a/src/storm/logic/BoundedUntilFormula.cpp +++ b/src/storm/logic/BoundedUntilFormula.cpp @@ -6,22 +6,11 @@ #include "storm/logic/FormulaVisitor.h" #include "storm/exceptions/InvalidPropertyException.h" +#include "storm/exceptions/InvalidOperationException.h" namespace storm { namespace logic { - UntilBound::UntilBound(bool strict, storm::expressions::Expression const& bound) : strict(strict), bound(bound) { - // Intentionally left empty. - } - - storm::expressions::Expression const& UntilBound::getBound() const { - return bound; - } - - bool UntilBound::isStrict() const { - return strict; - } - - BoundedUntilFormula::BoundedUntilFormula(std::shared_ptr const& leftSubformula, std::shared_ptr const& rightSubformula, boost::optional const& lowerBound, boost::optional const& upperBound, BoundedType const& boundedType) : BinaryPathFormula(leftSubformula, rightSubformula), boundedType(boundedType), lowerBound(lowerBound), upperBound(upperBound) { + BoundedUntilFormula::BoundedUntilFormula(std::shared_ptr const& leftSubformula, std::shared_ptr const& rightSubformula, boost::optional const& lowerBound, boost::optional const& upperBound, TimeBoundType const& timeBoundType) : BinaryPathFormula(leftSubformula, rightSubformula), timeBoundType(timeBoundType), lowerBound(lowerBound), upperBound(upperBound) { STORM_LOG_THROW(lowerBound || upperBound, storm::exceptions::InvalidArgumentException, "Bounded until formula requires at least one bound."); } @@ -37,12 +26,16 @@ namespace storm { return visitor.visit(*this, data); } + TimeBoundType const& BoundedUntilFormula::getTimeBoundType() const { + return timeBoundType; + } + bool BoundedUntilFormula::isStepBounded() const { - return boundedType == BoundedType::Steps; + return timeBoundType == TimeBoundType::Steps; } bool BoundedUntilFormula::isTimeBounded() const { - return boundedType == BoundedType::Time; + return timeBoundType == TimeBoundType::Time; } bool BoundedUntilFormula::isLowerBoundStrict() const { @@ -79,6 +72,7 @@ namespace storm { template <> double BoundedUntilFormula::getLowerBound() const { + checkNoVariablesInBound(this->getLowerBound()); double bound = this->getLowerBound().evaluateAsDouble(); STORM_LOG_THROW(bound >= 0, storm::exceptions::InvalidPropertyException, "Time-bound must not evaluate to negative number."); return bound; @@ -86,6 +80,7 @@ namespace storm { template <> double BoundedUntilFormula::getUpperBound() const { + checkNoVariablesInBound(this->getUpperBound()); double bound = this->getUpperBound().evaluateAsDouble(); STORM_LOG_THROW(bound >= 0, storm::exceptions::InvalidPropertyException, "Time-bound must not evaluate to negative number."); return bound; @@ -93,6 +88,7 @@ namespace storm { template <> uint64_t BoundedUntilFormula::getLowerBound() const { + checkNoVariablesInBound(this->getLowerBound()); 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(bound); @@ -100,11 +96,16 @@ namespace storm { template <> uint64_t BoundedUntilFormula::getUpperBound() const { + checkNoVariablesInBound(this->getUpperBound()); 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(bound); } + void BoundedUntilFormula::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& BoundedUntilFormula::writeToStream(std::ostream& out) const { this->getLeftSubformula().writeToStream(out); diff --git a/src/storm/logic/BoundedUntilFormula.h b/src/storm/logic/BoundedUntilFormula.h index 24b89d936..862871796 100644 --- a/src/storm/logic/BoundedUntilFormula.h +++ b/src/storm/logic/BoundedUntilFormula.h @@ -5,28 +5,14 @@ #include "storm/logic/BinaryPathFormula.h" +#include "storm/logic/TimeBound.h" +#include "storm/logic/TimeBoundType.h" + namespace storm { namespace logic { - class UntilBound { - public: - UntilBound(bool strict, storm::expressions::Expression const& bound); - - storm::expressions::Expression const& getBound() const; - bool isStrict() const; - - private: - bool strict; - storm::expressions::Expression bound; - }; - class BoundedUntilFormula : public BinaryPathFormula { public: - enum class BoundedType { - Steps, - Time - }; - - BoundedUntilFormula(std::shared_ptr const& leftSubformula, std::shared_ptr const& rightSubformula, boost::optional const& lowerBound, boost::optional const& upperBound, BoundedType const& boundedType = BoundedType::Time); + BoundedUntilFormula(std::shared_ptr const& leftSubformula, std::shared_ptr const& rightSubformula, boost::optional const& lowerBound, boost::optional const& upperBound, TimeBoundType const& timeBoundType = TimeBoundType::Time); virtual bool isBoundedUntilFormula() const override; @@ -34,6 +20,7 @@ namespace storm { virtual boost::any accept(FormulaVisitor const& visitor, boost::any const& data) const override; + TimeBoundType const& getTimeBoundType() const; bool isStepBounded() const; bool isTimeBounded() const; @@ -57,10 +44,11 @@ namespace storm { virtual std::ostream& writeToStream(std::ostream& out) const override; private: - BoundedType boundedType; + static void checkNoVariablesInBound(storm::expressions::Expression const& bound); - boost::optional lowerBound; - boost::optional upperBound; + TimeBoundType timeBoundType; + boost::optional lowerBound; + boost::optional upperBound; }; } } diff --git a/src/storm/logic/CumulativeRewardFormula.cpp b/src/storm/logic/CumulativeRewardFormula.cpp index 6b74a3c0d..05bf0353b 100644 --- a/src/storm/logic/CumulativeRewardFormula.cpp +++ b/src/storm/logic/CumulativeRewardFormula.cpp @@ -2,16 +2,16 @@ #include "storm/logic/FormulaVisitor.h" +#include "storm/utility/macros.h" +#include "storm/exceptions/InvalidPropertyException.h" +#include "storm/exceptions/InvalidOperationException.h" + namespace storm { namespace logic { - CumulativeRewardFormula::CumulativeRewardFormula(uint_fast64_t timeBound) : timeBound(timeBound) { - // Intentionally left empty. - } - - CumulativeRewardFormula::CumulativeRewardFormula(double timeBound) : timeBound(timeBound) { + CumulativeRewardFormula::CumulativeRewardFormula(TimeBound const& bound, TimeBoundType const& timeBoundType) : timeBoundType(timeBoundType), bound(bound) { // Intentionally left empty. } - + bool CumulativeRewardFormula::isCumulativeRewardFormula() const { return true; } @@ -24,32 +24,52 @@ namespace storm { return visitor.visit(*this, data); } - bool CumulativeRewardFormula::hasDiscreteTimeBound() const { - return timeBound.which() == 0; + TimeBoundType const& CumulativeRewardFormula::getTimeBoundType() const { + return timeBoundType; + } + + bool CumulativeRewardFormula::isStepBounded() const { + return timeBoundType == TimeBoundType::Steps; + } + + bool CumulativeRewardFormula::isTimeBounded() const { + return timeBoundType == TimeBoundType::Time; + } + + bool CumulativeRewardFormula::isBoundStrict() const { + return bound.isStrict(); } - uint_fast64_t CumulativeRewardFormula::getDiscreteTimeBound() const { - return boost::get(timeBound); + bool CumulativeRewardFormula::hasIntegerBound() const { + return bound.getBound().hasIntegerType(); } - bool CumulativeRewardFormula::hasContinuousTimeBound() const { - return timeBound.which() == 1; + storm::expressions::Expression const& CumulativeRewardFormula::getBound() const { + return bound.getBound(); + } + + template <> + double CumulativeRewardFormula::getBound() const { + checkNoVariablesInBound(bound.getBound()); + double value = bound.getBound().evaluateAsDouble(); + STORM_LOG_THROW(value >= 0, storm::exceptions::InvalidPropertyException, "Time-bound must not evaluate to negative number."); + return value; + } + + template <> + uint64_t CumulativeRewardFormula::getBound() const { + checkNoVariablesInBound(bound.getBound()); + uint64_t value = bound.getBound().evaluateAsInt(); + STORM_LOG_THROW(value >= 0, storm::exceptions::InvalidPropertyException, "Time-bound must not evaluate to negative number."); + return value; } - double CumulativeRewardFormula::getContinuousTimeBound() const { - if (this->hasDiscreteTimeBound()) { - return this->getDiscreteTimeBound(); - } else { - return boost::get(timeBound); - } + void CumulativeRewardFormula::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& CumulativeRewardFormula::writeToStream(std::ostream& out) const { - if (this->hasDiscreteTimeBound()) { - out << "C<=" << this->getDiscreteTimeBound(); - } else { - out << "C<=" << this->getContinuousTimeBound(); - } + out << "C<=" << this->getBound(); return out; } } diff --git a/src/storm/logic/CumulativeRewardFormula.h b/src/storm/logic/CumulativeRewardFormula.h index 81871b79d..ad9d5e3c0 100644 --- a/src/storm/logic/CumulativeRewardFormula.h +++ b/src/storm/logic/CumulativeRewardFormula.h @@ -1,17 +1,16 @@ #ifndef STORM_LOGIC_CUMULATIVEREWARDFORMULA_H_ #define STORM_LOGIC_CUMULATIVEREWARDFORMULA_H_ -#include - #include "storm/logic/PathFormula.h" +#include "storm/logic/TimeBound.h" +#include "storm/logic/TimeBoundType.h" + namespace storm { namespace logic { class CumulativeRewardFormula : public PathFormula { public: - CumulativeRewardFormula(uint_fast64_t timeBound); - - CumulativeRewardFormula(double timeBound); + CumulativeRewardFormula(TimeBound const& bound, TimeBoundType const& timeBoundType = TimeBoundType::Time); virtual ~CumulativeRewardFormula() { // Intentionally left empty. @@ -24,16 +23,23 @@ namespace storm { virtual std::ostream& writeToStream(std::ostream& out) const override; - bool hasDiscreteTimeBound() const; + TimeBoundType const& getTimeBoundType() const; + bool isStepBounded() const; + bool isTimeBounded() const; - uint_fast64_t getDiscreteTimeBound() const; + bool isBoundStrict() const; + bool hasIntegerBound() const; - bool hasContinuousTimeBound() const; + storm::expressions::Expression const& getBound() const; - double getContinuousTimeBound() const; + template + ValueType getBound() const; private: - boost::variant timeBound; + static void checkNoVariablesInBound(storm::expressions::Expression const& bound); + + TimeBoundType timeBoundType; + TimeBound bound; }; } } diff --git a/src/storm/logic/InstantaneousRewardFormula.cpp b/src/storm/logic/InstantaneousRewardFormula.cpp index d783fac79..f702ca578 100644 --- a/src/storm/logic/InstantaneousRewardFormula.cpp +++ b/src/storm/logic/InstantaneousRewardFormula.cpp @@ -2,16 +2,16 @@ #include "storm/logic/FormulaVisitor.h" +#include "storm/utility/macros.h" +#include "storm/exceptions/InvalidPropertyException.h" +#include "storm/exceptions/InvalidOperationException.h" + namespace storm { namespace logic { - InstantaneousRewardFormula::InstantaneousRewardFormula(uint_fast64_t timeBound) : timeBound(timeBound) { + InstantaneousRewardFormula::InstantaneousRewardFormula(storm::expressions::Expression const& bound, TimeBoundType const& timeBoundType) : timeBoundType(timeBoundType), bound(bound) { // Intentionally left empty. } - InstantaneousRewardFormula::InstantaneousRewardFormula(double timeBound) : timeBound(timeBound) { - // Intentionally left empty. - } - bool InstantaneousRewardFormula::isInstantaneousRewardFormula() const { return true; } @@ -24,32 +24,48 @@ namespace storm { return visitor.visit(*this, data); } - bool InstantaneousRewardFormula::hasDiscreteTimeBound() const { - return timeBound.which() == 0; + TimeBoundType const& InstantaneousRewardFormula::getTimeBoundType() const { + return timeBoundType; + } + + bool InstantaneousRewardFormula::isStepBounded() const { + return timeBoundType == TimeBoundType::Steps; + } + + bool InstantaneousRewardFormula::isTimeBounded() const { + return timeBoundType == TimeBoundType::Time; + } + + bool InstantaneousRewardFormula::hasIntegerBound() const { + return bound.hasIntegerType(); } - uint_fast64_t InstantaneousRewardFormula::getDiscreteTimeBound() const { - return boost::get(timeBound); + storm::expressions::Expression const& InstantaneousRewardFormula::getBound() const { + return bound; } - bool InstantaneousRewardFormula::hasContinuousTimeBound() const { - return timeBound.which() == 1; + template <> + double InstantaneousRewardFormula::getBound() const { + checkNoVariablesInBound(bound); + double value = bound.evaluateAsDouble(); + STORM_LOG_THROW(value >= 0, storm::exceptions::InvalidPropertyException, "Time-bound must not evaluate to negative number."); + return value; } - double InstantaneousRewardFormula::getContinuousTimeBound() const { - if (this->hasDiscreteTimeBound()) { - return this->getDiscreteTimeBound(); - } else { - return boost::get(timeBound); - } + template <> + uint64_t InstantaneousRewardFormula::getBound() const { + checkNoVariablesInBound(bound); + uint64_t value = bound.evaluateAsInt(); + STORM_LOG_THROW(value >= 0, storm::exceptions::InvalidPropertyException, "Time-bound must not evaluate to negative number."); + return value; } - + + void InstantaneousRewardFormula::checkNoVariablesInBound(storm::expressions::Expression const& bound) { + STORM_LOG_THROW(!bound.containsVariables(), storm::exceptions::InvalidOperationException, "Cannot evaluate time-instant '" << bound << "' as it contains undefined constants."); + } + std::ostream& InstantaneousRewardFormula::writeToStream(std::ostream& out) const { - if (this->hasDiscreteTimeBound()) { - out << "I=" << this->getDiscreteTimeBound(); - } else { - out << "I=" << this->getContinuousTimeBound(); - } + out << "I=" << this->getBound(); return out; } } diff --git a/src/storm/logic/InstantaneousRewardFormula.h b/src/storm/logic/InstantaneousRewardFormula.h index beecbfb17..ee9b5b28f 100644 --- a/src/storm/logic/InstantaneousRewardFormula.h +++ b/src/storm/logic/InstantaneousRewardFormula.h @@ -1,18 +1,17 @@ #ifndef STORM_LOGIC_INSTANTANEOUSREWARDFORMULA_H_ #define STORM_LOGIC_INSTANTANEOUSREWARDFORMULA_H_ -#include - #include "storm/logic/PathFormula.h" +#include "storm/logic/TimeBoundType.h" +#include "storm/storage/expressions/Expression.h" + namespace storm { namespace logic { class InstantaneousRewardFormula : public PathFormula { public: - InstantaneousRewardFormula(uint_fast64_t timeBound); - - InstantaneousRewardFormula(double timeBound); - + InstantaneousRewardFormula(storm::expressions::Expression const& bound, TimeBoundType const& timeBoundType = TimeBoundType::Time); + virtual ~InstantaneousRewardFormula() { // Intentionally left empty. } @@ -25,16 +24,22 @@ namespace storm { virtual std::ostream& writeToStream(std::ostream& out) const override; - bool hasDiscreteTimeBound() const; + TimeBoundType const& getTimeBoundType() const; + bool isStepBounded() const; + bool isTimeBounded() const; - uint_fast64_t getDiscreteTimeBound() const; - - bool hasContinuousTimeBound() const; + bool hasIntegerBound() const; + + storm::expressions::Expression const& getBound() const; + + template + ValueType getBound() const; - double getContinuousTimeBound() const; - private: - boost::variant timeBound; + static void checkNoVariablesInBound(storm::expressions::Expression const& bound); + + TimeBoundType timeBoundType; + storm::expressions::Expression bound; }; } } diff --git a/src/storm/logic/TimeBound.cpp b/src/storm/logic/TimeBound.cpp new file mode 100644 index 000000000..7ecd05aea --- /dev/null +++ b/src/storm/logic/TimeBound.cpp @@ -0,0 +1,19 @@ +#include "storm/logic/TimeBound.h" + +namespace storm { + namespace logic { + + TimeBound::TimeBound(bool strict, storm::expressions::Expression const& bound) : strict(strict), bound(bound) { + // Intentionally left empty. + } + + storm::expressions::Expression const& TimeBound::getBound() const { + return bound; + } + + bool TimeBound::isStrict() const { + return strict; + } + + } +} diff --git a/src/storm/logic/TimeBound.h b/src/storm/logic/TimeBound.h new file mode 100644 index 000000000..17a4c2b41 --- /dev/null +++ b/src/storm/logic/TimeBound.h @@ -0,0 +1,21 @@ +#pragma once + +#include "storm/storage/expressions/Expression.h" + +namespace storm { + namespace logic { + + class TimeBound { + public: + TimeBound(bool strict, storm::expressions::Expression const& bound); + + storm::expressions::Expression const& getBound() const; + bool isStrict() const; + + private: + bool strict; + storm::expressions::Expression bound; + }; + + } +} diff --git a/src/storm/logic/TimeBoundType.h b/src/storm/logic/TimeBoundType.h new file mode 100644 index 000000000..aef71b040 --- /dev/null +++ b/src/storm/logic/TimeBoundType.h @@ -0,0 +1,12 @@ +#pragma once + +namespace storm { + namespace logic { + + enum class TimeBoundType { + Steps, + Time + }; + + } +} diff --git a/src/storm/logic/VariableSubstitutionVisitor.cpp b/src/storm/logic/VariableSubstitutionVisitor.cpp index 916542b39..e0fe0630d 100644 --- a/src/storm/logic/VariableSubstitutionVisitor.cpp +++ b/src/storm/logic/VariableSubstitutionVisitor.cpp @@ -14,6 +14,30 @@ namespace storm { return boost::any_cast>(result); } + boost::any VariableSubstitutionVisitor::visit(BoundedUntilFormula const& f, boost::any const& data) const { + auto left = boost::any_cast>(f.getLeftSubformula().accept(*this, data)); + auto right = boost::any_cast>(f.getRightSubformula().accept(*this, data)); + + boost::optional lowerBound; + if (f.hasLowerBound()) { + lowerBound = TimeBound(f.isLowerBoundStrict(), f.getLowerBound().substitute(substitution)); + } + boost::optional upperBound; + if (f.hasUpperBound()) { + upperBound = TimeBound(f.isUpperBoundStrict(), f.getUpperBound().substitute(substitution)); + } + + return std::static_pointer_cast(std::make_shared(left, right, lowerBound, upperBound, f.getTimeBoundType())); + } + + boost::any VariableSubstitutionVisitor::visit(CumulativeRewardFormula const& f, boost::any const& data) const { + return std::static_pointer_cast(std::make_shared(storm::logic::TimeBound(f.isBoundStrict(), f.getBound().substitute(substitution)), f.getTimeBoundType())); + } + + boost::any VariableSubstitutionVisitor::visit(InstantaneousRewardFormula const& f, boost::any const& data) const { + return std::static_pointer_cast(std::make_shared(f.getBound().substitute(substitution), f.getTimeBoundType())); + } + boost::any VariableSubstitutionVisitor::visit(AtomicExpressionFormula const& f, boost::any const&) const { return std::static_pointer_cast(std::make_shared(f.getExpression().substitute(substitution))); } diff --git a/src/storm/logic/VariableSubstitutionVisitor.h b/src/storm/logic/VariableSubstitutionVisitor.h index 4e15980c0..4f5c19e06 100644 --- a/src/storm/logic/VariableSubstitutionVisitor.h +++ b/src/storm/logic/VariableSubstitutionVisitor.h @@ -16,6 +16,9 @@ namespace storm { std::shared_ptr substitute(Formula const& f) const; + virtual boost::any visit(BoundedUntilFormula const& f, boost::any const& data) const override; + virtual boost::any visit(CumulativeRewardFormula const& f, boost::any const& data) const override; + virtual boost::any visit(InstantaneousRewardFormula const& f, boost::any const& data) const override; virtual boost::any visit(AtomicExpressionFormula const& f, boost::any const& data) const override; private: diff --git a/src/storm/modelchecker/csl/HybridCtmcCslModelChecker.cpp b/src/storm/modelchecker/csl/HybridCtmcCslModelChecker.cpp index 21f73b0b7..8585bc92a 100644 --- a/src/storm/modelchecker/csl/HybridCtmcCslModelChecker.cpp +++ b/src/storm/modelchecker/csl/HybridCtmcCslModelChecker.cpp @@ -88,13 +88,17 @@ namespace storm { template std::unique_ptr HybridCtmcCslModelChecker::computeInstantaneousRewards(storm::logic::RewardMeasureType, CheckTask const& checkTask) { storm::logic::InstantaneousRewardFormula const& rewardPathFormula = checkTask.getFormula(); - return storm::modelchecker::helper::HybridCtmcCslHelper::computeInstantaneousRewards(this->getModel(), this->getModel().getTransitionMatrix(), this->getModel().getExitRateVector(), checkTask.isRewardModelSet() ? this->getModel().getRewardModel(checkTask.getRewardModel()) : this->getModel().getRewardModel(""), rewardPathFormula.getContinuousTimeBound(), *linearEquationSolverFactory); + + STORM_LOG_THROW(!rewardPathFormula.isStepBounded(), storm::exceptions::NotImplementedException, "Currently step-bounded properties on CTMCs are not supported."); + return storm::modelchecker::helper::HybridCtmcCslHelper::computeInstantaneousRewards(this->getModel(), this->getModel().getTransitionMatrix(), this->getModel().getExitRateVector(), checkTask.isRewardModelSet() ? this->getModel().getRewardModel(checkTask.getRewardModel()) : this->getModel().getRewardModel(""), rewardPathFormula.getBound(), *linearEquationSolverFactory); } template std::unique_ptr HybridCtmcCslModelChecker::computeCumulativeRewards(storm::logic::RewardMeasureType, CheckTask const& checkTask) { storm::logic::CumulativeRewardFormula const& rewardPathFormula = checkTask.getFormula(); - return storm::modelchecker::helper::HybridCtmcCslHelper::computeCumulativeRewards(this->getModel(), this->getModel().getTransitionMatrix(), this->getModel().getExitRateVector(), checkTask.isRewardModelSet() ? this->getModel().getRewardModel(checkTask.getRewardModel()) : this->getModel().getRewardModel(""), rewardPathFormula.getContinuousTimeBound(), *linearEquationSolverFactory); + + STORM_LOG_THROW(!rewardPathFormula.isStepBounded(), storm::exceptions::NotImplementedException, "Currently step-bounded properties on CTMCs are not supported."); + return storm::modelchecker::helper::HybridCtmcCslHelper::computeCumulativeRewards(this->getModel(), this->getModel().getTransitionMatrix(), this->getModel().getExitRateVector(), checkTask.isRewardModelSet() ? this->getModel().getRewardModel(checkTask.getRewardModel()) : this->getModel().getRewardModel(""), rewardPathFormula.getBound(), *linearEquationSolverFactory); } template diff --git a/src/storm/modelchecker/csl/SparseCtmcCslModelChecker.cpp b/src/storm/modelchecker/csl/SparseCtmcCslModelChecker.cpp index ca224b1a3..cfca43d1f 100644 --- a/src/storm/modelchecker/csl/SparseCtmcCslModelChecker.cpp +++ b/src/storm/modelchecker/csl/SparseCtmcCslModelChecker.cpp @@ -99,14 +99,16 @@ namespace storm { template std::unique_ptr SparseCtmcCslModelChecker::computeInstantaneousRewards(storm::logic::RewardMeasureType, CheckTask const& checkTask) { storm::logic::InstantaneousRewardFormula const& rewardPathFormula = checkTask.getFormula(); - std::vector numericResult = storm::modelchecker::helper::SparseCtmcCslHelper::computeInstantaneousRewards(this->getModel().getTransitionMatrix(), this->getModel().getExitRateVector(), checkTask.isRewardModelSet() ? this->getModel().getRewardModel(checkTask.getRewardModel()) : this->getModel().getRewardModel(""), rewardPathFormula.getContinuousTimeBound(), *linearEquationSolverFactory); + STORM_LOG_THROW(!rewardPathFormula.isStepBounded(), storm::exceptions::NotImplementedException, "Currently step-bounded properties on CTMCs are not supported."); + std::vector numericResult = storm::modelchecker::helper::SparseCtmcCslHelper::computeInstantaneousRewards(this->getModel().getTransitionMatrix(), this->getModel().getExitRateVector(), checkTask.isRewardModelSet() ? this->getModel().getRewardModel(checkTask.getRewardModel()) : this->getModel().getRewardModel(""), rewardPathFormula.getBound(), *linearEquationSolverFactory); return std::unique_ptr(new ExplicitQuantitativeCheckResult(std::move(numericResult))); } template std::unique_ptr SparseCtmcCslModelChecker::computeCumulativeRewards(storm::logic::RewardMeasureType, CheckTask const& checkTask) { storm::logic::CumulativeRewardFormula const& rewardPathFormula = checkTask.getFormula(); - std::vector numericResult = storm::modelchecker::helper::SparseCtmcCslHelper::computeCumulativeRewards(this->getModel().getTransitionMatrix(), this->getModel().getExitRateVector(), checkTask.isRewardModelSet() ? this->getModel().getRewardModel(checkTask.getRewardModel()) : this->getModel().getRewardModel(""), rewardPathFormula.getContinuousTimeBound(), *linearEquationSolverFactory); + STORM_LOG_THROW(!rewardPathFormula.isStepBounded(), storm::exceptions::NotImplementedException, "Currently step-bounded properties on CTMCs are not supported."); + std::vector numericResult = storm::modelchecker::helper::SparseCtmcCslHelper::computeCumulativeRewards(this->getModel().getTransitionMatrix(), this->getModel().getExitRateVector(), checkTask.isRewardModelSet() ? this->getModel().getRewardModel(checkTask.getRewardModel()) : this->getModel().getRewardModel(""), rewardPathFormula.getBound(), *linearEquationSolverFactory); return std::unique_ptr(new ExplicitQuantitativeCheckResult(std::move(numericResult))); } diff --git a/src/storm/modelchecker/multiobjective/pcaa/SparsePcaaPreprocessor.cpp b/src/storm/modelchecker/multiobjective/pcaa/SparsePcaaPreprocessor.cpp index 56f7891c8..60ac261fb 100644 --- a/src/storm/modelchecker/multiobjective/pcaa/SparsePcaaPreprocessor.cpp +++ b/src/storm/modelchecker/multiobjective/pcaa/SparsePcaaPreprocessor.cpp @@ -314,9 +314,9 @@ namespace storm { template void SparsePcaaPreprocessor::preprocessCumulativeRewardFormula(storm::logic::CumulativeRewardFormula const& formula, ReturnType& result, PcaaObjective& currentObjective, boost::optional const& optionalRewardModelName) { STORM_LOG_THROW(result.originalModel.isOfType(storm::models::ModelType::Mdp), storm::exceptions::InvalidPropertyException, "Cumulative reward formulas are not supported for the given model type."); - STORM_LOG_THROW(formula.hasDiscreteTimeBound(), storm::exceptions::InvalidPropertyException, "Expected a cumulativeRewardFormula with a discrete time bound but got " << formula << "."); - STORM_LOG_THROW(formula.getDiscreteTimeBound()>0, storm::exceptions::InvalidPropertyException, "Expected a cumulativeRewardFormula with a positive discrete time bound but got " << formula << "."); - currentObjective.upperTimeBound = storm::utility::convertNumber(formula.getDiscreteTimeBound()); + STORM_LOG_THROW(!formula.hasIntegerBound(), storm::exceptions::InvalidPropertyException, "Expected a cumulativeRewardFormula with a discrete time bound but got " << formula << "."); + // FIXME: really convert to value type? + currentObjective.upperTimeBound = storm::utility::convertNumber(formula.getBound()); RewardModelType objectiveRewards = result.preprocessedModel.getRewardModel(optionalRewardModelName ? optionalRewardModelName.get() : ""); objectiveRewards.reduceToStateBasedRewards(result.preprocessedModel.getTransitionMatrix(), false); diff --git a/src/storm/modelchecker/prctl/HybridDtmcPrctlModelChecker.cpp b/src/storm/modelchecker/prctl/HybridDtmcPrctlModelChecker.cpp index c5f29b568..f018458f0 100644 --- a/src/storm/modelchecker/prctl/HybridDtmcPrctlModelChecker.cpp +++ b/src/storm/modelchecker/prctl/HybridDtmcPrctlModelChecker.cpp @@ -82,15 +82,15 @@ namespace storm { template std::unique_ptr HybridDtmcPrctlModelChecker::computeCumulativeRewards(storm::logic::RewardMeasureType, CheckTask const& checkTask) { storm::logic::CumulativeRewardFormula const& rewardPathFormula = checkTask.getFormula(); - STORM_LOG_THROW(rewardPathFormula.hasDiscreteTimeBound(), storm::exceptions::InvalidArgumentException, "Formula needs to have a discrete time bound."); - return storm::modelchecker::helper::HybridDtmcPrctlHelper::computeCumulativeRewards(this->getModel(), this->getModel().getTransitionMatrix(), checkTask.isRewardModelSet() ? this->getModel().getRewardModel(checkTask.getRewardModel()) : this->getModel().getRewardModel(""), rewardPathFormula.getDiscreteTimeBound(), *this->linearEquationSolverFactory); + STORM_LOG_THROW(rewardPathFormula.hasIntegerBound(), storm::exceptions::InvalidPropertyException, "Formula needs to have a discrete time bound."); + return storm::modelchecker::helper::HybridDtmcPrctlHelper::computeCumulativeRewards(this->getModel(), this->getModel().getTransitionMatrix(), checkTask.isRewardModelSet() ? this->getModel().getRewardModel(checkTask.getRewardModel()) : this->getModel().getRewardModel(""), rewardPathFormula.getBound() + (rewardPathFormula.isBoundStrict() ? 1ull : 0ull), *this->linearEquationSolverFactory); } template std::unique_ptr HybridDtmcPrctlModelChecker::computeInstantaneousRewards(storm::logic::RewardMeasureType, CheckTask const& checkTask) { storm::logic::InstantaneousRewardFormula const& rewardPathFormula = checkTask.getFormula(); - STORM_LOG_THROW(rewardPathFormula.hasDiscreteTimeBound(), storm::exceptions::InvalidArgumentException, "Formula needs to have a discrete time bound."); - return storm::modelchecker::helper::HybridDtmcPrctlHelper::computeInstantaneousRewards(this->getModel(), this->getModel().getTransitionMatrix(), checkTask.isRewardModelSet() ? this->getModel().getRewardModel(checkTask.getRewardModel()) : this->getModel().getRewardModel(""), rewardPathFormula.getDiscreteTimeBound(), *this->linearEquationSolverFactory); + STORM_LOG_THROW(rewardPathFormula.hasIntegerBound(), storm::exceptions::InvalidPropertyException, "Formula needs to have a discrete time bound."); + return storm::modelchecker::helper::HybridDtmcPrctlHelper::computeInstantaneousRewards(this->getModel(), this->getModel().getTransitionMatrix(), checkTask.isRewardModelSet() ? this->getModel().getRewardModel(checkTask.getRewardModel()) : this->getModel().getRewardModel(""), rewardPathFormula.getBound(), *this->linearEquationSolverFactory); } template diff --git a/src/storm/modelchecker/prctl/HybridMdpPrctlModelChecker.cpp b/src/storm/modelchecker/prctl/HybridMdpPrctlModelChecker.cpp index 1a6c7721a..56aed7679 100644 --- a/src/storm/modelchecker/prctl/HybridMdpPrctlModelChecker.cpp +++ b/src/storm/modelchecker/prctl/HybridMdpPrctlModelChecker.cpp @@ -81,16 +81,16 @@ namespace storm { std::unique_ptr HybridMdpPrctlModelChecker::computeCumulativeRewards(storm::logic::RewardMeasureType, CheckTask const& checkTask) { storm::logic::CumulativeRewardFormula const& rewardPathFormula = 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(rewardPathFormula.hasDiscreteTimeBound(), storm::exceptions::InvalidPropertyException, "Formula needs to have a discrete time bound."); - return storm::modelchecker::helper::HybridMdpPrctlHelper::computeCumulativeRewards(checkTask.getOptimizationDirection(), this->getModel(), this->getModel().getTransitionMatrix(), checkTask.isRewardModelSet() ? this->getModel().getRewardModel(checkTask.getRewardModel()) : this->getModel().getRewardModel(""), rewardPathFormula.getDiscreteTimeBound(), *this->linearEquationSolverFactory); + STORM_LOG_THROW(rewardPathFormula.hasIntegerBound(), storm::exceptions::InvalidPropertyException, "Formula needs to have a discrete time bound."); + return storm::modelchecker::helper::HybridMdpPrctlHelper::computeCumulativeRewards(checkTask.getOptimizationDirection(), this->getModel(), this->getModel().getTransitionMatrix(), checkTask.isRewardModelSet() ? this->getModel().getRewardModel(checkTask.getRewardModel()) : this->getModel().getRewardModel(""), rewardPathFormula.getBound() + (rewardPathFormula.isBoundStrict() ? 1ull : 0ll), *this->linearEquationSolverFactory); } template std::unique_ptr HybridMdpPrctlModelChecker::computeInstantaneousRewards(storm::logic::RewardMeasureType, CheckTask const& checkTask) { storm::logic::InstantaneousRewardFormula const& rewardPathFormula = 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(rewardPathFormula.hasDiscreteTimeBound(), storm::exceptions::InvalidPropertyException, "Formula needs to have a discrete time bound."); - return storm::modelchecker::helper::HybridMdpPrctlHelper::computeInstantaneousRewards(checkTask.getOptimizationDirection(), this->getModel(), this->getModel().getTransitionMatrix(), checkTask.isRewardModelSet() ? this->getModel().getRewardModel(checkTask.getRewardModel()) : this->getModel().getRewardModel(""), rewardPathFormula.getDiscreteTimeBound(), *this->linearEquationSolverFactory); + STORM_LOG_THROW(rewardPathFormula.hasIntegerBound(), storm::exceptions::InvalidPropertyException, "Formula needs to have a discrete time bound."); + return storm::modelchecker::helper::HybridMdpPrctlHelper::computeInstantaneousRewards(checkTask.getOptimizationDirection(), this->getModel(), this->getModel().getTransitionMatrix(), checkTask.isRewardModelSet() ? this->getModel().getRewardModel(checkTask.getRewardModel()) : this->getModel().getRewardModel(""), rewardPathFormula.getBound(), *this->linearEquationSolverFactory); } template diff --git a/src/storm/modelchecker/prctl/SparseDtmcPrctlModelChecker.cpp b/src/storm/modelchecker/prctl/SparseDtmcPrctlModelChecker.cpp index e82bef01e..daaee411e 100644 --- a/src/storm/modelchecker/prctl/SparseDtmcPrctlModelChecker.cpp +++ b/src/storm/modelchecker/prctl/SparseDtmcPrctlModelChecker.cpp @@ -85,16 +85,16 @@ namespace storm { template std::unique_ptr SparseDtmcPrctlModelChecker::computeCumulativeRewards(storm::logic::RewardMeasureType, CheckTask const& checkTask) { storm::logic::CumulativeRewardFormula const& rewardPathFormula = checkTask.getFormula(); - STORM_LOG_THROW(rewardPathFormula.hasDiscreteTimeBound(), storm::exceptions::InvalidPropertyException, "Formula needs to have a discrete time bound."); - std::vector numericResult = storm::modelchecker::helper::SparseDtmcPrctlHelper::computeCumulativeRewards(this->getModel().getTransitionMatrix(), checkTask.isRewardModelSet() ? this->getModel().getRewardModel(checkTask.getRewardModel()) : this->getModel().getRewardModel(""), rewardPathFormula.getDiscreteTimeBound(), *linearEquationSolverFactory); + STORM_LOG_THROW(rewardPathFormula.hasIntegerBound(), storm::exceptions::InvalidPropertyException, "Formula needs to have a discrete time bound."); + std::vector numericResult = storm::modelchecker::helper::SparseDtmcPrctlHelper::computeCumulativeRewards(this->getModel().getTransitionMatrix(), checkTask.isRewardModelSet() ? this->getModel().getRewardModel(checkTask.getRewardModel()) : this->getModel().getRewardModel(""), rewardPathFormula.getBound() + (rewardPathFormula.isBoundStrict() ? 1ull : 0ull), *linearEquationSolverFactory); return std::unique_ptr(new ExplicitQuantitativeCheckResult(std::move(numericResult))); } template std::unique_ptr SparseDtmcPrctlModelChecker::computeInstantaneousRewards(storm::logic::RewardMeasureType, CheckTask const& checkTask) { storm::logic::InstantaneousRewardFormula const& rewardPathFormula = checkTask.getFormula(); - STORM_LOG_THROW(rewardPathFormula.hasDiscreteTimeBound(), storm::exceptions::InvalidPropertyException, "Formula needs to have a discrete time bound."); - std::vector numericResult = storm::modelchecker::helper::SparseDtmcPrctlHelper::computeInstantaneousRewards(this->getModel().getTransitionMatrix(), checkTask.isRewardModelSet() ? this->getModel().getRewardModel(checkTask.getRewardModel()) : this->getModel().getRewardModel(""), rewardPathFormula.getDiscreteTimeBound(), *linearEquationSolverFactory); + STORM_LOG_THROW(rewardPathFormula.hasIntegerBound(), storm::exceptions::InvalidPropertyException, "Formula needs to have a discrete time bound."); + std::vector numericResult = storm::modelchecker::helper::SparseDtmcPrctlHelper::computeInstantaneousRewards(this->getModel().getTransitionMatrix(), checkTask.isRewardModelSet() ? this->getModel().getRewardModel(checkTask.getRewardModel()) : this->getModel().getRewardModel(""), rewardPathFormula.getBound(), *linearEquationSolverFactory); return std::unique_ptr(new ExplicitQuantitativeCheckResult(std::move(numericResult))); } diff --git a/src/storm/modelchecker/prctl/SparseMdpPrctlModelChecker.cpp b/src/storm/modelchecker/prctl/SparseMdpPrctlModelChecker.cpp index 2a8bd9f3c..2a7f6d725 100644 --- a/src/storm/modelchecker/prctl/SparseMdpPrctlModelChecker.cpp +++ b/src/storm/modelchecker/prctl/SparseMdpPrctlModelChecker.cpp @@ -26,7 +26,7 @@ #include "storm/storage/MaximalEndComponentDecomposition.h" -#include "storm/exceptions/InvalidArgumentException.h" +#include "storm/exceptions/InvalidPropertyException.h" namespace storm { namespace modelchecker { @@ -57,7 +57,7 @@ namespace storm { template std::unique_ptr SparseMdpPrctlModelChecker::computeBoundedUntilProbabilities(CheckTask 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(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.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 leftResultPointer = this->check(pathFormula.getLeftSubformula()); @@ -71,7 +71,7 @@ namespace storm { template std::unique_ptr SparseMdpPrctlModelChecker::computeNextProbabilities(CheckTask const& checkTask) { storm::logic::NextFormula 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(checkTask.isOptimizationDirectionSet(), storm::exceptions::InvalidPropertyException, "Formula needs to specify whether minimal or maximal values are to be computed on nondeterministic model."); std::unique_ptr subResultPointer = this->check(pathFormula.getSubformula()); ExplicitQualitativeCheckResult const& subResult = subResultPointer->asExplicitQualitativeCheckResult(); std::vector numericResult = storm::modelchecker::helper::SparseMdpPrctlHelper::computeNextProbabilities(checkTask.getOptimizationDirection(), this->getModel().getTransitionMatrix(), subResult.getTruthValuesVector(), *minMaxLinearEquationSolverFactory); @@ -81,7 +81,7 @@ namespace storm { template std::unique_ptr SparseMdpPrctlModelChecker::computeUntilProbabilities(CheckTask const& checkTask) { storm::logic::UntilFormula 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(checkTask.isOptimizationDirectionSet(), storm::exceptions::InvalidPropertyException, "Formula needs to specify whether minimal or maximal values are to be computed on nondeterministic model."); std::unique_ptr leftResultPointer = this->check(pathFormula.getLeftSubformula()); std::unique_ptr rightResultPointer = this->check(pathFormula.getRightSubformula()); ExplicitQualitativeCheckResult const& leftResult = leftResultPointer->asExplicitQualitativeCheckResult(); @@ -97,7 +97,7 @@ namespace storm { template std::unique_ptr SparseMdpPrctlModelChecker::computeGloballyProbabilities(CheckTask const& checkTask) { storm::logic::GloballyFormula 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(checkTask.isOptimizationDirectionSet(), storm::exceptions::InvalidPropertyException, "Formula needs to specify whether minimal or maximal values are to be computed on nondeterministic model."); std::unique_ptr subResultPointer = this->check(pathFormula.getSubformula()); ExplicitQualitativeCheckResult const& subResult = subResultPointer->asExplicitQualitativeCheckResult(); auto ret = storm::modelchecker::helper::SparseMdpPrctlHelper::computeGloballyProbabilities(checkTask.getOptimizationDirection(), this->getModel().getTransitionMatrix(), this->getModel().getBackwardTransitions(), subResult.getTruthValuesVector(), checkTask.isQualitativeSet(), *minMaxLinearEquationSolverFactory); @@ -107,7 +107,7 @@ namespace storm { template std::unique_ptr SparseMdpPrctlModelChecker::computeConditionalProbabilities(CheckTask const& checkTask) { storm::logic::ConditionalFormula const& conditionalFormula = 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(checkTask.isOptimizationDirectionSet(), storm::exceptions::InvalidPropertyException, "Formula needs to specify whether minimal or maximal values are to be computed on nondeterministic model."); STORM_LOG_THROW(this->getModel().getInitialStates().getNumberOfSetBits() == 1, storm::exceptions::InvalidPropertyException, "Cannot compute conditional probabilities on MDPs with more than one initial state."); STORM_LOG_THROW(conditionalFormula.getSubformula().isEventuallyFormula(), storm::exceptions::InvalidPropertyException, "Illegal conditional probability formula."); STORM_LOG_THROW(conditionalFormula.getConditionFormula().isEventuallyFormula(), storm::exceptions::InvalidPropertyException, "Illegal conditional probability formula."); @@ -123,25 +123,25 @@ namespace storm { template std::unique_ptr SparseMdpPrctlModelChecker::computeCumulativeRewards(storm::logic::RewardMeasureType, CheckTask const& checkTask) { storm::logic::CumulativeRewardFormula const& rewardPathFormula = 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(rewardPathFormula.hasDiscreteTimeBound(), storm::exceptions::InvalidArgumentException, "Formula needs to have a discrete time bound."); - std::vector numericResult = storm::modelchecker::helper::SparseMdpPrctlHelper::computeCumulativeRewards(checkTask.getOptimizationDirection(), this->getModel().getTransitionMatrix(), checkTask.isRewardModelSet() ? this->getModel().getRewardModel(checkTask.getRewardModel()) : this->getModel().getRewardModel(""), rewardPathFormula.getDiscreteTimeBound(), *minMaxLinearEquationSolverFactory); + 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(rewardPathFormula.hasIntegerBound(), storm::exceptions::InvalidPropertyException, "Formula needs to have a discrete time bound."); + std::vector numericResult = storm::modelchecker::helper::SparseMdpPrctlHelper::computeCumulativeRewards(checkTask.getOptimizationDirection(), this->getModel().getTransitionMatrix(), checkTask.isRewardModelSet() ? this->getModel().getRewardModel(checkTask.getRewardModel()) : this->getModel().getRewardModel(""), rewardPathFormula.getBound() + (rewardPathFormula.isBoundStrict() ? 1ull : 0ull), *minMaxLinearEquationSolverFactory); return std::unique_ptr(new ExplicitQuantitativeCheckResult(std::move(numericResult))); } template std::unique_ptr SparseMdpPrctlModelChecker::computeInstantaneousRewards(storm::logic::RewardMeasureType, CheckTask const& checkTask) { storm::logic::InstantaneousRewardFormula const& rewardPathFormula = 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(rewardPathFormula.hasDiscreteTimeBound(), storm::exceptions::InvalidArgumentException, "Formula needs to have a discrete time bound."); - std::vector numericResult = storm::modelchecker::helper::SparseMdpPrctlHelper::computeInstantaneousRewards(checkTask.getOptimizationDirection(), this->getModel().getTransitionMatrix(), checkTask.isRewardModelSet() ? this->getModel().getRewardModel(checkTask.getRewardModel()) : this->getModel().getRewardModel(""), rewardPathFormula.getDiscreteTimeBound(), *minMaxLinearEquationSolverFactory); + 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(rewardPathFormula.hasIntegerBound(), storm::exceptions::InvalidPropertyException, "Formula needs to have a discrete time bound."); + std::vector numericResult = storm::modelchecker::helper::SparseMdpPrctlHelper::computeInstantaneousRewards(checkTask.getOptimizationDirection(), this->getModel().getTransitionMatrix(), checkTask.isRewardModelSet() ? this->getModel().getRewardModel(checkTask.getRewardModel()) : this->getModel().getRewardModel(""), rewardPathFormula.getBound(), *minMaxLinearEquationSolverFactory); return std::unique_ptr(new ExplicitQuantitativeCheckResult(std::move(numericResult))); } template std::unique_ptr SparseMdpPrctlModelChecker::computeReachabilityRewards(storm::logic::RewardMeasureType, CheckTask const& checkTask) { storm::logic::EventuallyFormula const& eventuallyFormula = 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(checkTask.isOptimizationDirectionSet(), storm::exceptions::InvalidPropertyException, "Formula needs to specify whether minimal or maximal values are to be computed on nondeterministic model."); std::unique_ptr subResultPointer = this->check(eventuallyFormula.getSubformula()); ExplicitQualitativeCheckResult const& subResult = subResultPointer->asExplicitQualitativeCheckResult(); std::vector numericResult = storm::modelchecker::helper::SparseMdpPrctlHelper::computeReachabilityRewards(checkTask.getOptimizationDirection(), this->getModel().getTransitionMatrix(), this->getModel().getBackwardTransitions(), checkTask.isRewardModelSet() ? this->getModel().getRewardModel(checkTask.getRewardModel()) : this->getModel().getRewardModel(""), subResult.getTruthValuesVector(), checkTask.isQualitativeSet(), *minMaxLinearEquationSolverFactory); @@ -151,7 +151,7 @@ namespace storm { template std::unique_ptr SparseMdpPrctlModelChecker::computeLongRunAverageProbabilities(CheckTask const& checkTask) { storm::logic::StateFormula const& stateFormula = 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(checkTask.isOptimizationDirectionSet(), storm::exceptions::InvalidPropertyException, "Formula needs to specify whether minimal or maximal values are to be computed on nondeterministic model."); std::unique_ptr subResultPointer = this->check(stateFormula); ExplicitQualitativeCheckResult const& subResult = subResultPointer->asExplicitQualitativeCheckResult(); std::vector numericResult = storm::modelchecker::helper::SparseMdpPrctlHelper::computeLongRunAverageProbabilities(checkTask.getOptimizationDirection(), this->getModel().getTransitionMatrix(), this->getModel().getBackwardTransitions(), subResult.getTruthValuesVector(), *minMaxLinearEquationSolverFactory); diff --git a/src/storm/modelchecker/prctl/SymbolicDtmcPrctlModelChecker.cpp b/src/storm/modelchecker/prctl/SymbolicDtmcPrctlModelChecker.cpp index af037f5ef..c52307315 100644 --- a/src/storm/modelchecker/prctl/SymbolicDtmcPrctlModelChecker.cpp +++ b/src/storm/modelchecker/prctl/SymbolicDtmcPrctlModelChecker.cpp @@ -83,16 +83,16 @@ namespace storm { template std::unique_ptr SymbolicDtmcPrctlModelChecker::computeCumulativeRewards(storm::logic::RewardMeasureType, CheckTask const& checkTask) { storm::logic::CumulativeRewardFormula const& rewardPathFormula = checkTask.getFormula(); - STORM_LOG_THROW(rewardPathFormula.hasDiscreteTimeBound(), storm::exceptions::InvalidPropertyException, "Formula needs to have a discrete time bound."); - storm::dd::Add numericResult = storm::modelchecker::helper::SymbolicDtmcPrctlHelper::computeCumulativeRewards(this->getModel(), this->getModel().getTransitionMatrix(), checkTask.isRewardModelSet() ? this->getModel().getRewardModel(checkTask.getRewardModel()) : this->getModel().getRewardModel(""), rewardPathFormula.getDiscreteTimeBound(), *this->linearEquationSolverFactory); + STORM_LOG_THROW(rewardPathFormula.hasIntegerBound(), storm::exceptions::InvalidPropertyException, "Formula needs to have a discrete time bound."); + storm::dd::Add numericResult = storm::modelchecker::helper::SymbolicDtmcPrctlHelper::computeCumulativeRewards(this->getModel(), this->getModel().getTransitionMatrix(), checkTask.isRewardModelSet() ? this->getModel().getRewardModel(checkTask.getRewardModel()) : this->getModel().getRewardModel(""), rewardPathFormula.getBound() + (rewardPathFormula.isBoundStrict() ? 1ull : 0ull), *this->linearEquationSolverFactory); return std::unique_ptr>(new SymbolicQuantitativeCheckResult(this->getModel().getReachableStates(), numericResult)); } template std::unique_ptr SymbolicDtmcPrctlModelChecker::computeInstantaneousRewards(storm::logic::RewardMeasureType, CheckTask const& checkTask) { storm::logic::InstantaneousRewardFormula const& rewardPathFormula = checkTask.getFormula(); - STORM_LOG_THROW(rewardPathFormula.hasDiscreteTimeBound(), storm::exceptions::InvalidPropertyException, "Formula needs to have a discrete time bound."); - storm::dd::Add numericResult = storm::modelchecker::helper::SymbolicDtmcPrctlHelper::computeInstantaneousRewards(this->getModel(), this->getModel().getTransitionMatrix(), checkTask.isRewardModelSet() ? this->getModel().getRewardModel(checkTask.getRewardModel()) : this->getModel().getRewardModel(""), rewardPathFormula.getDiscreteTimeBound(), *this->linearEquationSolverFactory); + STORM_LOG_THROW(rewardPathFormula.hasIntegerBound(), storm::exceptions::InvalidPropertyException, "Formula needs to have a discrete time bound."); + storm::dd::Add numericResult = storm::modelchecker::helper::SymbolicDtmcPrctlHelper::computeInstantaneousRewards(this->getModel(), this->getModel().getTransitionMatrix(), checkTask.isRewardModelSet() ? this->getModel().getRewardModel(checkTask.getRewardModel()) : this->getModel().getRewardModel(""), rewardPathFormula.getBound(), *this->linearEquationSolverFactory); return std::unique_ptr>(new SymbolicQuantitativeCheckResult(this->getModel().getReachableStates(), numericResult)); } diff --git a/src/storm/modelchecker/prctl/SymbolicMdpPrctlModelChecker.cpp b/src/storm/modelchecker/prctl/SymbolicMdpPrctlModelChecker.cpp index 7bb1af89a..2ac26509a 100644 --- a/src/storm/modelchecker/prctl/SymbolicMdpPrctlModelChecker.cpp +++ b/src/storm/modelchecker/prctl/SymbolicMdpPrctlModelChecker.cpp @@ -83,16 +83,16 @@ namespace storm { std::unique_ptr SymbolicMdpPrctlModelChecker::computeCumulativeRewards(storm::logic::RewardMeasureType, CheckTask const& checkTask) { storm::logic::CumulativeRewardFormula const& rewardPathFormula = 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(rewardPathFormula.hasDiscreteTimeBound(), storm::exceptions::InvalidPropertyException, "Formula needs to have a discrete time bound."); - return storm::modelchecker::helper::SymbolicMdpPrctlHelper::computeCumulativeRewards(checkTask.getOptimizationDirection(), this->getModel(), this->getModel().getTransitionMatrix(), checkTask.isRewardModelSet() ? this->getModel().getRewardModel(checkTask.getRewardModel()) : this->getModel().getRewardModel(""), rewardPathFormula.getDiscreteTimeBound(), *this->linearEquationSolverFactory); + STORM_LOG_THROW(rewardPathFormula.hasIntegerBound(), storm::exceptions::InvalidPropertyException, "Formula needs to have a discrete time bound."); + return storm::modelchecker::helper::SymbolicMdpPrctlHelper::computeCumulativeRewards(checkTask.getOptimizationDirection(), this->getModel(), this->getModel().getTransitionMatrix(), checkTask.isRewardModelSet() ? this->getModel().getRewardModel(checkTask.getRewardModel()) : this->getModel().getRewardModel(""), rewardPathFormula.getBound() + (rewardPathFormula.isBoundStrict() ? 1ull : 0ull), *this->linearEquationSolverFactory); } template std::unique_ptr SymbolicMdpPrctlModelChecker::computeInstantaneousRewards(storm::logic::RewardMeasureType, CheckTask const& checkTask) { storm::logic::InstantaneousRewardFormula const& rewardPathFormula = 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(rewardPathFormula.hasDiscreteTimeBound(), storm::exceptions::InvalidPropertyException, "Formula needs to have a discrete time bound."); - return storm::modelchecker::helper::SymbolicMdpPrctlHelper::computeInstantaneousRewards(checkTask.getOptimizationDirection(), this->getModel(), this->getModel().getTransitionMatrix(), checkTask.isRewardModelSet() ? this->getModel().getRewardModel(checkTask.getRewardModel()) : this->getModel().getRewardModel(""), rewardPathFormula.getDiscreteTimeBound(), *this->linearEquationSolverFactory); + STORM_LOG_THROW(rewardPathFormula.hasIntegerBound(), storm::exceptions::InvalidPropertyException, "Formula needs to have a discrete time bound."); + return storm::modelchecker::helper::SymbolicMdpPrctlHelper::computeInstantaneousRewards(checkTask.getOptimizationDirection(), this->getModel(), this->getModel().getTransitionMatrix(), checkTask.isRewardModelSet() ? this->getModel().getRewardModel(checkTask.getRewardModel()) : this->getModel().getRewardModel(""), rewardPathFormula.getBound(), *this->linearEquationSolverFactory); } template diff --git a/src/storm/parser/FormulaParser.cpp b/src/storm/parser/FormulaParser.cpp index 7919d0878..e1ba36dcc 100644 --- a/src/storm/parser/FormulaParser.cpp +++ b/src/storm/parser/FormulaParser.cpp @@ -17,16 +17,18 @@ namespace storm { namespace parser { - FormulaParser::FormulaParser() : manager(new storm::expressions::ExpressionManager()), grammar(new FormulaParserGrammar(manager)) { // Intentionally left empty. } - FormulaParser::FormulaParser(std::shared_ptr const& manager) : manager(manager), grammar(new FormulaParserGrammar(manager)) { // Intentionally left empty. } - + + FormulaParser::FormulaParser(std::shared_ptr const& manager) : manager(manager), grammar(new FormulaParserGrammar(manager)) { + // Intentionally left empty. + } + FormulaParser::FormulaParser(storm::prism::Program const& program) : manager(program.getManager().getSharedPointer()), grammar(new FormulaParserGrammar(manager)) { // Make the formulas of the program available to the parser. for (auto const& formula : program.getFormulas()) { diff --git a/src/storm/parser/FormulaParser.h b/src/storm/parser/FormulaParser.h index 4db23b202..7917be3ac 100644 --- a/src/storm/parser/FormulaParser.h +++ b/src/storm/parser/FormulaParser.h @@ -23,6 +23,7 @@ namespace storm { public: FormulaParser(); explicit FormulaParser(std::shared_ptr const& manager); + explicit FormulaParser(std::shared_ptr const& manager); explicit FormulaParser(storm::prism::Program const& program); FormulaParser(FormulaParser const& other); diff --git a/src/storm/parser/FormulaParserGrammar.cpp b/src/storm/parser/FormulaParserGrammar.cpp index 15f3e8a6e..825b36412 100644 --- a/src/storm/parser/FormulaParserGrammar.cpp +++ b/src/storm/parser/FormulaParserGrammar.cpp @@ -4,7 +4,15 @@ namespace storm { namespace parser { - FormulaParserGrammar::FormulaParserGrammar(std::shared_ptr const& manager) : FormulaParserGrammar::base_type(start), manager(manager), expressionParser(*manager, keywords_, true, true) { + FormulaParserGrammar::FormulaParserGrammar(std::shared_ptr const& manager) : FormulaParserGrammar::base_type(start), constManager(manager), expressionParser(*manager, keywords_, true, true) { + initialize(); + } + + FormulaParserGrammar::FormulaParserGrammar(std::shared_ptr const& manager) : FormulaParserGrammar::base_type(start), constManager(manager), manager(manager), expressionParser(*manager, keywords_, true, true) { + initialize(); + } + + void FormulaParserGrammar::initialize() { // Register all variables so we can parse them in the expressions. for (auto variableTypePair : *manager) { identifiers_.add(variableTypePair.first.getName(), variableTypePair.first); @@ -15,10 +23,10 @@ namespace storm { longRunAverageRewardFormula = (qi::lit("LRA") | qi::lit("S"))[qi::_val = phoenix::bind(&FormulaParserGrammar::createLongRunAverageRewardFormula, phoenix::ref(*this))]; longRunAverageRewardFormula.name("long run average reward formula"); - instantaneousRewardFormula = (qi::lit("I=") >> strict_double)[qi::_val = phoenix::bind(&FormulaParserGrammar::createInstantaneousRewardFormula, phoenix::ref(*this), qi::_1)] | (qi::lit("I=") > qi::uint_)[qi::_val = phoenix::bind(&FormulaParserGrammar::createInstantaneousRewardFormula, phoenix::ref(*this), qi::_1)]; + instantaneousRewardFormula = (qi::lit("I=") > expressionParser)[qi::_val = phoenix::bind(&FormulaParserGrammar::createInstantaneousRewardFormula, phoenix::ref(*this), qi::_1)]; instantaneousRewardFormula.name("instantaneous reward formula"); - cumulativeRewardFormula = (qi::lit("C<=") >> strict_double)[qi::_val = phoenix::bind(&FormulaParserGrammar::createCumulativeRewardFormula, phoenix::ref(*this), qi::_1)] | (qi::lit("C<=") > qi::uint_)[qi::_val = phoenix::bind(&FormulaParserGrammar::createCumulativeRewardFormula, phoenix::ref(*this), qi::_1)]; + cumulativeRewardFormula = ((qi::lit("C<=")[qi::_a = false] | qi::lit("C<")[qi::_a = true]) > expressionParser)[qi::_val = phoenix::bind(&FormulaParserGrammar::createCumulativeRewardFormula, phoenix::ref(*this), qi::_1, qi::_a)]; cumulativeRewardFormula.name("cumulative reward formula"); totalRewardFormula = (qi::lit("C"))[qi::_val = phoenix::bind(&FormulaParserGrammar::createTotalRewardFormula, phoenix::ref(*this))]; @@ -105,12 +113,19 @@ namespace storm { stateFormula = (orStateFormula | multiObjectiveFormula); stateFormula.name("state formula"); - start = qi::eps > (stateFormula % +(qi::char_("\n;"))) >> qi::skip(boost::spirit::ascii::space | qi::lit("//") >> *(qi::char_ - (qi::eol | qi::eoi)))[qi::eps] >> qi::eoi; + identifier %= qi::as_string[qi::raw[qi::lexeme[((qi::alpha | qi::char_('_') | qi::char_('.')) >> *(qi::alnum | qi::char_('_')))]]]; + identifier.name("identifier"); + + constantDefinition = (qi::lit("const") > qi::eps[qi::_a = true] > -(qi::lit("int") | qi::lit("double")[qi::_a = false]) >> identifier)[phoenix::bind(&FormulaParserGrammar::addConstant, phoenix::ref(*this), qi::_1, qi::_a)]; + constantDefinition.name("constant definition"); + + start = qi::eps > ((stateFormula[phoenix::push_back(qi::_val, qi::_1)] | qi::eps(phoenix::bind(&FormulaParserGrammar::areConstantDefinitionsAllowed, phoenix::ref(*this))) >> constantDefinition) % +(qi::char_("\n;"))) >> qi::skip(boost::spirit::ascii::space | qi::lit("//") >> *(qi::char_ - (qi::eol | qi::eoi)))[qi::eps] >> qi::eoi; start.name("start"); - //Enable the following lines to print debug output for most the rules. + // Enable the following lines to print debug output for most the rules. /* debug(start); + debug(constantDefinition); debug(stateFormula); debug(orStateFormula); debug(andStateFormula); @@ -167,38 +182,41 @@ namespace storm { this->identifiers_.add(identifier, expression); } - std::pair, boost::optional> 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); + void FormulaParserGrammar::addConstant(std::string const& name, bool integer) { + STORM_LOG_ASSERT(manager, "Mutable expression manager required to define new constants."); + storm::expressions::Variable newVariable; + if (integer) { + newVariable = manager->declareIntegerVariable(name); + } else { + newVariable = manager->declareRationalVariable(name); + } + addIdentifierExpression(name, newVariable); + } + + bool FormulaParserGrammar::areConstantDefinitionsAllowed() const { + return static_cast(manager); + } + + std::pair, boost::optional> FormulaParserGrammar::createTimeBoundFromInterval(storm::expressions::Expression const& lowerBound, storm::expressions::Expression const& upperBound) const { + storm::logic::TimeBound lower(false, lowerBound); + storm::logic::TimeBound upper(false, upperBound); return std::make_pair(lower, upper); } - std::pair, boost::optional> FormulaParserGrammar::createTimeBoundFromSingleBound(storm::expressions::Expression const& bound, bool upperBound, bool strict) const { + std::pair, boost::optional> 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)); + return std::make_pair(boost::none, storm::logic::TimeBound(strict, bound)); } else { - return std::make_pair(storm::logic::UntilBound(strict, bound), boost::none); + return std::make_pair(storm::logic::TimeBound(strict, bound), boost::none); } } - std::shared_ptr FormulaParserGrammar::createInstantaneousRewardFormula(boost::variant const& timeBound) const { - if (timeBound.which() == 0) { - return std::shared_ptr(new storm::logic::InstantaneousRewardFormula(static_cast(boost::get(timeBound)))); - } else { - double timeBoundAsDouble = boost::get(timeBound); - STORM_LOG_THROW(timeBoundAsDouble >= 0, storm::exceptions::WrongFormatException, "Instantaneous reward property must have non-negative bound."); - return std::shared_ptr(new storm::logic::InstantaneousRewardFormula(timeBoundAsDouble)); - } + std::shared_ptr FormulaParserGrammar::createInstantaneousRewardFormula(storm::expressions::Expression const& timeBound) const { + return std::shared_ptr(new storm::logic::InstantaneousRewardFormula(timeBound)); } - std::shared_ptr FormulaParserGrammar::createCumulativeRewardFormula(boost::variant const& timeBound) const { - if (timeBound.which() == 0) { - return std::shared_ptr(new storm::logic::CumulativeRewardFormula(static_cast(boost::get(timeBound)))); - } else { - double timeBoundAsDouble = boost::get(timeBound); - STORM_LOG_THROW(timeBoundAsDouble >= 0, storm::exceptions::WrongFormatException, "Cumulative reward property must have non-negative bound."); - return std::shared_ptr(new storm::logic::CumulativeRewardFormula(static_cast(timeBoundAsDouble))); - } + std::shared_ptr FormulaParserGrammar::createCumulativeRewardFormula(storm::expressions::Expression const& timeBound, bool strict) const { + return std::shared_ptr(new storm::logic::CumulativeRewardFormula(storm::logic::TimeBound(strict, timeBound))); } std::shared_ptr FormulaParserGrammar::createTotalRewardFormula() const { @@ -222,9 +240,9 @@ namespace storm { return std::shared_ptr(new storm::logic::AtomicLabelFormula(label)); } - std::shared_ptr FormulaParserGrammar::createEventuallyFormula(boost::optional, boost::optional>> const& timeBound, storm::logic::FormulaContext context, std::shared_ptr const& subformula) const { + std::shared_ptr FormulaParserGrammar::createEventuallyFormula(boost::optional, boost::optional>> const& timeBound, storm::logic::FormulaContext context, std::shared_ptr const& subformula) const { if (timeBound) { - return std::shared_ptr(new storm::logic::BoundedUntilFormula(createBooleanLiteralFormula(true), subformula, timeBound.get().first, timeBound.get().second, storm::logic::BoundedUntilFormula::BoundedType::Time)); + return std::shared_ptr(new storm::logic::BoundedUntilFormula(createBooleanLiteralFormula(true), subformula, timeBound.get().first, timeBound.get().second, storm::logic::TimeBoundType::Time)); } else { return std::shared_ptr(new storm::logic::EventuallyFormula(subformula, context)); } @@ -238,9 +256,9 @@ namespace storm { return std::shared_ptr(new storm::logic::NextFormula(subformula)); } - std::shared_ptr FormulaParserGrammar::createUntilFormula(std::shared_ptr const& leftSubformula, boost::optional, boost::optional>> const& timeBound, std::shared_ptr const& rightSubformula) { + std::shared_ptr FormulaParserGrammar::createUntilFormula(std::shared_ptr const& leftSubformula, boost::optional, boost::optional>> const& timeBound, std::shared_ptr const& rightSubformula) { if (timeBound) { - return std::shared_ptr(new storm::logic::BoundedUntilFormula(leftSubformula, rightSubformula, timeBound.get().first, timeBound.get().second, storm::logic::BoundedUntilFormula::BoundedType::Time)); + return std::shared_ptr(new storm::logic::BoundedUntilFormula(leftSubformula, rightSubformula, timeBound.get().first, timeBound.get().second, storm::logic::TimeBoundType::Time)); } else { return std::shared_ptr(new storm::logic::UntilFormula(leftSubformula, rightSubformula)); } diff --git a/src/storm/parser/FormulaParserGrammar.h b/src/storm/parser/FormulaParserGrammar.h index 1b73df00c..32bdbff28 100644 --- a/src/storm/parser/FormulaParserGrammar.h +++ b/src/storm/parser/FormulaParserGrammar.h @@ -20,6 +20,7 @@ namespace storm { class FormulaParserGrammar : public qi::grammar>(), Skipper> { public: FormulaParserGrammar(std::shared_ptr const& manager); + FormulaParserGrammar(std::shared_ptr const& manager); FormulaParserGrammar(FormulaParserGrammar const& other) = default; FormulaParserGrammar& operator=(FormulaParserGrammar const& other) = default; @@ -34,6 +35,8 @@ namespace storm { void addIdentifierExpression(std::string const& identifier, storm::expressions::Expression const& expression); private: + void initialize(); + struct keywordsStruct : qi::symbols { keywordsStruct() { add @@ -108,7 +111,8 @@ namespace storm { rewardMeasureTypeStruct rewardMeasureType_; // The manager used to parse expressions. - std::shared_ptr manager; + std::shared_ptr constManager; + std::shared_ptr manager; // Parser and manager used for recognizing expressions. storm::parser::ExpressionParser expressionParser; @@ -119,6 +123,9 @@ namespace storm { qi::rule>(), Skipper> start; + qi::rule, Skipper> constantDefinition; + qi::rule identifier; + qi::rule, boost::optional, boost::optional>, Skipper> operatorInformation; qi::rule rewardMeasureType; qi::rule(), Skipper> probabilityOperator; @@ -149,10 +156,10 @@ namespace storm { qi::rule(storm::logic::FormulaContext), Skipper> globallyFormula; qi::rule(storm::logic::FormulaContext), Skipper> untilFormula; - qi::rule, boost::optional>(), qi::locals, Skipper> timeBound; + qi::rule, boost::optional>(), qi::locals, Skipper> timeBound; qi::rule(), Skipper> rewardPathFormula; - qi::rule(), Skipper> cumulativeRewardFormula; + qi::rule(), qi::locals, Skipper> cumulativeRewardFormula; qi::rule(), Skipper> totalRewardFormula; qi::rule(), Skipper> instantaneousRewardFormula; qi::rule(), Skipper> longRunAverageRewardFormula; @@ -162,21 +169,24 @@ namespace storm { // Parser that is used to recognize doubles only (as opposed to Spirit's double_ parser). boost::spirit::qi::real_parser> strict_double; - std::pair, boost::optional> createTimeBoundFromInterval(storm::expressions::Expression const& lowerBound, storm::expressions::Expression const& upperBound) const; - std::pair, boost::optional> createTimeBoundFromSingleBound(storm::expressions::Expression const& bound, bool upperBound, bool strict) const; + bool areConstantDefinitionsAllowed() const; + void addConstant(std::string const& name, bool integer); + + std::pair, boost::optional> createTimeBoundFromInterval(storm::expressions::Expression const& lowerBound, storm::expressions::Expression const& upperBound) const; + std::pair, boost::optional> createTimeBoundFromSingleBound(storm::expressions::Expression const& bound, bool upperBound, bool strict) const; // Methods that actually create the expression objects. - std::shared_ptr createInstantaneousRewardFormula(boost::variant const& timeBound) const; - std::shared_ptr createCumulativeRewardFormula(boost::variant const& timeBound) const; + std::shared_ptr createInstantaneousRewardFormula(storm::expressions::Expression const& timeBound) const; + std::shared_ptr createCumulativeRewardFormula(storm::expressions::Expression const& timeBound, bool strict) const; std::shared_ptr createTotalRewardFormula() const; std::shared_ptr createLongRunAverageRewardFormula() const; std::shared_ptr createAtomicExpressionFormula(storm::expressions::Expression const& expression) const; std::shared_ptr createBooleanLiteralFormula(bool literal) const; std::shared_ptr createAtomicLabelFormula(std::string const& label) const; - std::shared_ptr createEventuallyFormula(boost::optional, boost::optional>> const& timeBound, storm::logic::FormulaContext context, std::shared_ptr const& subformula) const; + std::shared_ptr createEventuallyFormula(boost::optional, boost::optional>> const& timeBound, storm::logic::FormulaContext context, std::shared_ptr const& subformula) const; std::shared_ptr createGloballyFormula(std::shared_ptr const& subformula) const; std::shared_ptr createNextFormula(std::shared_ptr const& subformula) const; - std::shared_ptr createUntilFormula(std::shared_ptr const& leftSubformula, boost::optional, boost::optional>> const& timeBound, std::shared_ptr const& rightSubformula); + std::shared_ptr createUntilFormula(std::shared_ptr const& leftSubformula, boost::optional, boost::optional>> const& timeBound, std::shared_ptr const& rightSubformula); std::shared_ptr createConditionalFormula(std::shared_ptr const& leftSubformula, std::shared_ptr const& rightSubformula, storm::logic::FormulaContext context) const; storm::logic::OperatorInformation createOperatorInformation(boost::optional const& optimizationDirection, boost::optional const& comparisonType, boost::optional const& threshold) const; std::shared_ptr createLongRunAverageOperatorFormula(storm::logic::OperatorInformation const& operatorInformation, std::shared_ptr const& subformula) const; diff --git a/src/storm/parser/JaniParser.cpp b/src/storm/parser/JaniParser.cpp index 6e6bb1612..517c663ce 100644 --- a/src/storm/parser/JaniParser.cpp +++ b/src/storm/parser/JaniParser.cpp @@ -256,14 +256,14 @@ namespace storm { if(!accTime && !accSteps) { if (rewExpr.isVariable()) { std::string rewardName = rewExpr.getVariables().begin()->getName(); - return std::make_shared(std::make_shared(static_cast(stepInstant)), rewardName, opInfo); + return std::make_shared(std::make_shared(stepInstantExpr, storm::logic::TimeBoundType::Steps), rewardName, opInfo); } else { STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "Only simple reward expressions are currently supported"); } } else { if (rewExpr.isVariable()) { std::string rewardName = rewExpr.getVariables().begin()->getName(); - return std::make_shared(std::make_shared(static_cast(stepInstant)), rewardName, opInfo); + return std::make_shared(std::make_shared(storm::logic::TimeBound(false, stepInstantExpr), storm::logic::TimeBoundType::Steps), rewardName, opInfo); } else { STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "Only simple reward expressions are currently supported"); } @@ -276,14 +276,14 @@ namespace storm { if(!accTime && !accSteps) { if (rewExpr.isVariable()) { std::string rewardName = rewExpr.getVariables().begin()->getName(); - return std::make_shared(std::make_shared(timeInstant), rewardName, opInfo); + return std::make_shared(std::make_shared(timeInstantExpr, storm::logic::TimeBoundType::Time), rewardName, opInfo); } else { STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "Only simple reward expressions are currently supported"); } } else { if (rewExpr.isVariable()) { std::string rewardName = rewExpr.getVariables().begin()->getName(); - return std::make_shared(std::make_shared(timeInstant), rewardName, opInfo); + return std::make_shared(std::make_shared(storm::logic::TimeBound(false, timeInstantExpr), storm::logic::TimeBoundType::Time), rewardName, opInfo); } else { STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "Only simple reward expressions are currently supported"); } @@ -345,7 +345,7 @@ namespace storm { upperBound--; } STORM_LOG_THROW(upperBound >= 0, storm::exceptions::InvalidJaniException, "Step-bounds cannot be negative"); - return std::make_shared(args[0], args[1], storm::logic::UntilBound(pi.lowerBoundStrict, pi.lowerBound), storm::logic::UntilBound(pi.upperBoundStrict, pi.upperBound), storm::logic::BoundedUntilFormula::BoundedType::Steps); + return std::make_shared(args[0], args[1], storm::logic::TimeBound(pi.lowerBoundStrict, pi.lowerBound), storm::logic::TimeBound(pi.upperBoundStrict, pi.upperBound), storm::logic::TimeBoundType::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(args[0], args[1], storm::logic::UntilBound(pi.lowerBoundStrict, pi.lowerBound), storm::logic::UntilBound(pi.upperBoundStrict, pi.upperBound), storm::logic::BoundedUntilFormula::BoundedType::Time); + return std::make_shared(args[0], args[1], storm::logic::TimeBound(pi.lowerBoundStrict, pi.lowerBound), storm::logic::TimeBound(pi.upperBoundStrict, pi.upperBound), storm::logic::TimeBoundType::Time); } else if (propertyStructure.count("reward-bounds") > 0 ) { STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "Reward bounded properties are not supported by Storm"); diff --git a/src/storm/storage/SymbolicModelDescription.cpp b/src/storm/storage/SymbolicModelDescription.cpp index a9e4488b3..da985d103 100644 --- a/src/storm/storage/SymbolicModelDescription.cpp +++ b/src/storm/storage/SymbolicModelDescription.cpp @@ -1,5 +1,6 @@ #include "storm/storage/SymbolicModelDescription.h" +#include "storm/utility/cli.h" #include "storm/utility/prism.h" #include "storm/utility/jani.h" @@ -84,12 +85,22 @@ namespace storm { STORM_LOG_THROW(isJaniModel(), storm::exceptions::InvalidOperationException, "Cannot retrieve JANI model, because the symbolic description has a different type."); return boost::get(modelDescription.get()); } - + + storm::jani::Model& SymbolicModelDescription::asJaniModel() { + STORM_LOG_THROW(isJaniModel(), storm::exceptions::InvalidOperationException, "Cannot retrieve JANI model, because the symbolic description has a different type."); + return boost::get(modelDescription.get()); + } + storm::prism::Program const& SymbolicModelDescription::asPrismProgram() const { STORM_LOG_THROW(isPrismProgram(), storm::exceptions::InvalidOperationException, "Cannot retrieve JANI model, because the symbolic description has a different type."); return boost::get(modelDescription.get()); } - + + storm::prism::Program& SymbolicModelDescription::asPrismProgram() { + STORM_LOG_THROW(isPrismProgram(), storm::exceptions::InvalidOperationException, "Cannot retrieve JANI model, because the symbolic description has a different type."); + return boost::get(modelDescription.get()); + } + std::vector SymbolicModelDescription::getParameterNames() const { std::vector result; if (isJaniModel()) { @@ -116,17 +127,34 @@ namespace storm { } SymbolicModelDescription SymbolicModelDescription::preprocess(std::string const& constantDefinitionString) const { + std::map substitution = parseConstantDefinitions(constantDefinitionString); if (this->isJaniModel()) { - std::map substitution = storm::utility::jani::parseConstantDefinitionString(this->asJaniModel(), constantDefinitionString); storm::jani::Model preparedModel = this->asJaniModel().defineUndefinedConstants(substitution).substituteConstants(); return SymbolicModelDescription(preparedModel); } else if (this->isPrismProgram()) { - std::map substitution = storm::utility::prism::parseConstantDefinitionString(this->asPrismProgram(), constantDefinitionString); return SymbolicModelDescription(this->asPrismProgram().defineUndefinedConstants(substitution).substituteConstants()); } return *this; } + SymbolicModelDescription SymbolicModelDescription::preprocess(std::map const& constantDefinitions) const { + if (this->isJaniModel()) { + storm::jani::Model preparedModel = this->asJaniModel().defineUndefinedConstants(constantDefinitions).substituteConstants(); + return SymbolicModelDescription(preparedModel); + } else if (this->isPrismProgram()) { + return SymbolicModelDescription(this->asPrismProgram().defineUndefinedConstants(constantDefinitions).substituteConstants()); + } + return *this; + } + + std::map SymbolicModelDescription::parseConstantDefinitions(std::string const& constantDefinitionString) const { + if (this->isJaniModel()) { + return storm::utility::cli::parseConstantDefinitionString(this->asJaniModel().getManager(), constantDefinitionString); + } else { + return storm::utility::cli::parseConstantDefinitionString(this->asPrismProgram().getManager(), constantDefinitionString); + } + } + void SymbolicModelDescription::requireNoUndefinedConstants() const { if (this->isJaniModel()) { storm::utility::jani::requireNoUndefinedConstants(this->asJaniModel()); diff --git a/src/storm/storage/SymbolicModelDescription.h b/src/storm/storage/SymbolicModelDescription.h index 44e80d9f0..8ed9fa7e0 100644 --- a/src/storm/storage/SymbolicModelDescription.h +++ b/src/storm/storage/SymbolicModelDescription.h @@ -32,13 +32,18 @@ namespace storm { void setModel(storm::prism::Program const& program); storm::jani::Model const& asJaniModel() const; + storm::jani::Model& asJaniModel(); storm::prism::Program const& asPrismProgram() const; + storm::prism::Program& asPrismProgram(); std::vector getParameterNames() const; SymbolicModelDescription toJani(bool makeVariablesGlobal = true) const; SymbolicModelDescription preprocess(std::string const& constantDefinitionString = "") const; + SymbolicModelDescription preprocess(std::map const& constantDefinitions) const; + + std::map parseConstantDefinitions(std::string const& constantDefinitionString) const; void requireNoUndefinedConstants() const; diff --git a/src/storm/storage/jani/Model.cpp b/src/storm/storage/jani/Model.cpp index 53d3e84dc..7b1c6e908 100644 --- a/src/storm/storage/jani/Model.cpp +++ b/src/storm/storage/jani/Model.cpp @@ -825,11 +825,6 @@ namespace storm { } } - // As a sanity check, we make sure that the given mapping does not contain any definitions for identifiers - // that are not undefined constants. - for (auto const& constantExpressionPair : constantDefinitions) { - STORM_LOG_THROW(definedUndefinedConstants.find(constantExpressionPair.first) != definedUndefinedConstants.end(), storm::exceptions::InvalidOperationException, "Unable to define non-existant constant '" << constantExpressionPair.first.getName() << "'."); - } return result; } diff --git a/src/storm/storage/prism/Program.cpp b/src/storm/storage/prism/Program.cpp index 210077d04..c521d9c29 100644 --- a/src/storm/storage/prism/Program.cpp +++ b/src/storm/storage/prism/Program.cpp @@ -760,12 +760,6 @@ namespace storm { } } - // As a sanity check, we make sure that the given mapping does not contain any definitions for identifiers - // that are not undefined constants. - for (auto const& constantExpressionPair : constantDefinitions) { - STORM_LOG_THROW(definedUndefinedConstants.find(constantExpressionPair.first) != definedUndefinedConstants.end(), storm::exceptions::InvalidArgumentException, "Unable to define non-existant constant."); - } - return Program(this->manager, this->getModelType(), newConstants, this->getGlobalBooleanVariables(), this->getGlobalIntegerVariables(), this->getFormulas(), this->getModules(), this->getActionNameToIndexMapping(), this->getRewardModels(), this->getLabels(), this->getOptionalInitialConstruct(), this->getOptionalSystemCompositionConstruct()); } diff --git a/src/storm/utility/cli.cpp b/src/storm/utility/cli.cpp new file mode 100644 index 000000000..4009a8883 --- /dev/null +++ b/src/storm/utility/cli.cpp @@ -0,0 +1,65 @@ +#include "storm/utility/cli.h" + +#include "storm/utility/macros.h" +#include "storm/exceptions/WrongFormatException.h" + +namespace storm { + namespace utility { + namespace cli { + + std::map parseConstantDefinitionString(storm::expressions::ExpressionManager const& manager, std::string const& constantDefinitionString) { + std::map constantDefinitions; + std::set definedConstants; + + if (!constantDefinitionString.empty()) { + // Parse the string that defines the undefined constants of the model and make sure that it contains exactly + // one value for each undefined constant of the model. + std::vector definitions; + boost::split(definitions, constantDefinitionString, boost::is_any_of(",")); + for (auto& definition : definitions) { + boost::trim(definition); + + // Check whether the token could be a legal constant definition. + std::size_t positionOfAssignmentOperator = definition.find('='); + STORM_LOG_THROW(positionOfAssignmentOperator != std::string::npos, storm::exceptions::WrongFormatException, "Illegal constant definition string: syntax error."); + + // Now extract the variable name and the value from the string. + std::string constantName = definition.substr(0, positionOfAssignmentOperator); + boost::trim(constantName); + std::string value = definition.substr(positionOfAssignmentOperator + 1); + boost::trim(value); + + // Check whether the constant is a legal undefined constant of the program and if so, of what type it is. + if (manager.hasVariable(constantName)) { + // Get the actual constant and check whether it's in fact undefined. + auto const& variable = manager.getVariable(constantName); + STORM_LOG_THROW(definedConstants.find(variable) == definedConstants.end(), storm::exceptions::WrongFormatException, "Illegally trying to define constant '" << constantName <<"' twice."); + definedConstants.insert(variable); + + if (variable.hasBooleanType()) { + if (value == "true") { + constantDefinitions[variable] = manager.boolean(true); + } else if (value == "false") { + constantDefinitions[variable] = manager.boolean(false); + } else { + throw storm::exceptions::WrongFormatException() << "Illegal value for boolean constant: " << value << "."; + } + } else if (variable.hasIntegerType()) { + int_fast64_t integerValue = std::stoi(value); + constantDefinitions[variable] = manager.integer(integerValue); + } else if (variable.hasRationalType()) { + double doubleValue = std::stod(value); + constantDefinitions[variable] = manager.rational(doubleValue); + } + } else { + STORM_LOG_THROW(false, storm::exceptions::WrongFormatException, "Illegal constant definition string: unknown undefined constant '" << constantName << "'."); + } + } + } + + return constantDefinitions; + } + + } + } +} diff --git a/src/storm/utility/cli.h b/src/storm/utility/cli.h new file mode 100644 index 000000000..bd6d218d6 --- /dev/null +++ b/src/storm/utility/cli.h @@ -0,0 +1,16 @@ +#pragma once + +#include + +#include "storm/storage/expressions/ExpressionManager.h" +#include "storm/storage/expressions/Expression.h" + +namespace storm { + namespace utility { + namespace cli { + + std::map parseConstantDefinitionString(storm::expressions::ExpressionManager const& manager, std::string const& constantDefinitionString); + + } + } +} diff --git a/src/storm/utility/jani.cpp b/src/storm/utility/jani.cpp index eedca0e37..180ee34c1 100644 --- a/src/storm/utility/jani.cpp +++ b/src/storm/utility/jani.cpp @@ -11,61 +11,6 @@ namespace storm { namespace utility { namespace jani { - - std::map parseConstantDefinitionString(storm::jani::Model const& model, std::string const& constantDefinitionString) { - std::map constantDefinitions; - std::set definedConstants; - - if (!constantDefinitionString.empty()) { - // Parse the string that defines the undefined constants of the model and make sure that it contains exactly - // one value for each undefined constant of the model. - std::vector definitions; - boost::split(definitions, constantDefinitionString, boost::is_any_of(",")); - for (auto& definition : definitions) { - boost::trim(definition); - - // Check whether the token could be a legal constant definition. - std::size_t positionOfAssignmentOperator = definition.find('='); - STORM_LOG_THROW(positionOfAssignmentOperator != std::string::npos, storm::exceptions::InvalidArgumentException, "Illegal constant definition string: syntax error."); - - // Now extract the variable name and the value from the string. - std::string constantName = definition.substr(0, positionOfAssignmentOperator); - boost::trim(constantName); - std::string value = definition.substr(positionOfAssignmentOperator + 1); - boost::trim(value); - - // Check whether the constant is a legal undefined constant of the program and if so, of what type it is. - if (model.hasConstant(constantName)) { - // Get the actual constant and check whether it's in fact undefined. - auto const& constant = model.getConstant(constantName); - storm::expressions::Variable variable = constant.getExpressionVariable(); - STORM_LOG_THROW(!constant.isDefined(), storm::exceptions::InvalidArgumentException, "Illegally trying to define already defined constant '" << constantName <<"'."); - STORM_LOG_THROW(definedConstants.find(variable) == definedConstants.end(), storm::exceptions::InvalidArgumentException, "Illegally trying to define constant '" << constantName <<"' twice."); - definedConstants.insert(variable); - - if (constant.getType().isBooleanType()) { - if (value == "true") { - constantDefinitions[variable] = model.getExpressionManager().boolean(true); - } else if (value == "false") { - constantDefinitions[variable] = model.getExpressionManager().boolean(false); - } else { - throw storm::exceptions::InvalidArgumentException() << "Illegal value for boolean constant: " << value << "."; - } - } else if (constant.getType().isIntegerType()) { - int_fast64_t integerValue = std::stoi(value); - constantDefinitions[variable] = model.getExpressionManager().integer(integerValue); - } else if (constant.getType().isRationalType()) { - double doubleValue = std::stod(value); - constantDefinitions[variable] = model.getExpressionManager().rational(doubleValue); - } - } else { - STORM_LOG_THROW(false, storm::exceptions::InvalidArgumentException, "Illegal constant definition string: unknown undefined constant '" << constantName << "'."); - } - } - } - - return constantDefinitions; - } void requireNoUndefinedConstants(storm::jani::Model const& model) { if (model.hasUndefinedConstants()) { diff --git a/src/storm/utility/jani.h b/src/storm/utility/jani.h index 303ef7397..d3af68703 100644 --- a/src/storm/utility/jani.h +++ b/src/storm/utility/jani.h @@ -3,11 +3,6 @@ #include namespace storm { - namespace expressions { - class Variable; - class Expression; - } - namespace jani { class Model; } @@ -15,8 +10,6 @@ namespace storm { namespace utility { namespace jani { - std::map parseConstantDefinitionString(storm::jani::Model const& model, std::string const& constantDefinitionString); - void requireNoUndefinedConstants(storm::jani::Model const& model); } } diff --git a/src/storm/utility/prism.cpp b/src/storm/utility/prism.cpp index 7049ab19c..27e4b8847 100644 --- a/src/storm/utility/prism.cpp +++ b/src/storm/utility/prism.cpp @@ -5,6 +5,7 @@ #include "storm/storage/expressions/ExpressionManager.h" #include "storm/storage/prism/Program.h" +#include "storm/utility/cli.h" #include "storm/utility/macros.h" #include "storm/exceptions/InvalidArgumentException.h" @@ -22,64 +23,7 @@ namespace storm { } storm::prism::Program preprocess(storm::prism::Program const& program, std::string const& constantDefinitionString) { - return preprocess(program, parseConstantDefinitionString(program, constantDefinitionString)); - } - - std::map parseConstantDefinitionString(storm::prism::Program const& program, std::string const& constantDefinitionString) { - std::map constantDefinitions; - std::set definedConstants; - - if (!constantDefinitionString.empty()) { - // Parse the string that defines the undefined constants of the model and make sure that it contains exactly - // one value for each undefined constant of the model. - std::vector definitions; - boost::split(definitions, constantDefinitionString, boost::is_any_of(",")); - for (auto& definition : definitions) { - boost::trim(definition); - - // Check whether the token could be a legal constant definition. - uint_fast64_t positionOfAssignmentOperator = definition.find('='); - if (positionOfAssignmentOperator == std::string::npos) { - throw storm::exceptions::InvalidArgumentException() << "Illegal constant definition string: syntax error."; - } - - // Now extract the variable name and the value from the string. - std::string constantName = definition.substr(0, positionOfAssignmentOperator); - boost::trim(constantName); - std::string value = definition.substr(positionOfAssignmentOperator + 1); - boost::trim(value); - - // Check whether the constant is a legal undefined constant of the program and if so, of what type it is. - if (program.hasConstant(constantName)) { - // Get the actual constant and check whether it's in fact undefined. - auto const& constant = program.getConstant(constantName); - storm::expressions::Variable variable = constant.getExpressionVariable(); - STORM_LOG_THROW(!constant.isDefined(), storm::exceptions::InvalidArgumentException, "Illegally trying to define already defined constant '" << constantName <<"'."); - STORM_LOG_THROW(definedConstants.find(variable) == definedConstants.end(), storm::exceptions::InvalidArgumentException, "Illegally trying to define constant '" << constantName <<"' twice."); - definedConstants.insert(variable); - - if (constant.getType().isBooleanType()) { - if (value == "true") { - constantDefinitions[variable] = program.getManager().boolean(true); - } else if (value == "false") { - constantDefinitions[variable] = program.getManager().boolean(false); - } else { - throw storm::exceptions::InvalidArgumentException() << "Illegal value for boolean constant: " << value << "."; - } - } else if (constant.getType().isIntegerType()) { - int_fast64_t integerValue = std::stoi(value); - constantDefinitions[variable] = program.getManager().integer(integerValue); - } else if (constant.getType().isRationalType()) { - double doubleValue = std::stod(value); - constantDefinitions[variable] = program.getManager().rational(doubleValue); - } - } else { - STORM_LOG_THROW(false, storm::exceptions::InvalidArgumentException, "Illegal constant definition string: unknown undefined constant " << constantName << "."); - } - } - } - - return constantDefinitions; + return preprocess(program, storm::utility::cli::parseConstantDefinitionString(program.getManager(), constantDefinitionString)); } void requireNoUndefinedConstants(storm::prism::Program const& program) { diff --git a/src/storm/utility/prism.h b/src/storm/utility/prism.h index 8abd2f8ec..bb8b3496f 100644 --- a/src/storm/utility/prism.h +++ b/src/storm/utility/prism.h @@ -20,8 +20,6 @@ namespace storm { namespace utility { namespace prism { - std::map parseConstantDefinitionString(storm::prism::Program const& program, std::string const& constantDefinitionString); - storm::prism::Program preprocess(storm::prism::Program const& program, std::map const& constantDefinitions); storm::prism::Program preprocess(storm::prism::Program const& program, std::string const& constantDefinitionString); diff --git a/src/storm/utility/storm.cpp b/src/storm/utility/storm.cpp index 9a0e6faba..9c8ab20f2 100644 --- a/src/storm/utility/storm.cpp +++ b/src/storm/utility/storm.cpp @@ -47,7 +47,7 @@ namespace storm{ * @param FormulaParser * @return The formulas. */ - std::vector> parseFormulas(storm::parser::FormulaParser & formulaParser, std::string const& inputString) { + std::vector> parseFormulas(storm::parser::FormulaParser& formulaParser, std::string const& inputString) { // If the given property looks like a file (containing a dot and there exists a file with that name), // we try to parse it as a file, otherwise we assume it's a property. if (inputString.find(".") != std::string::npos && std::ifstream(inputString).good()) { @@ -65,6 +65,7 @@ namespace storm{ std::vector> substituteConstantsInFormulas(std::vector> const& formulas, std::map const& substitution) { std::vector> preprocessedFormulas; + for (auto const& formula : formulas) { preprocessedFormulas.emplace_back(formula->substitute(substitution)); } @@ -78,7 +79,7 @@ namespace storm{ } std::vector> parseFormulasForPrismProgram(std::string const& inputString, storm::prism::Program const& program) { - storm::parser::FormulaParser formulaParser(program); + storm::parser::FormulaParser formulaParser(program.getManager().getSharedPointer()); auto formulas = parseFormulas(formulaParser, inputString); return substituteConstantsInFormulas(formulas, program.getConstantsSubstitution()); } diff --git a/src/storm/utility/storm.h b/src/storm/utility/storm.h index 589a531a4..fce54187b 100644 --- a/src/storm/utility/storm.h +++ b/src/storm/utility/storm.h @@ -108,6 +108,7 @@ namespace storm { std::vector> formulasInProperties(std::vector const& properties); std::pair> parseJaniModel(std::string const& path); storm::prism::Program parseProgram(std::string const& path); + std::vector> substituteConstantsInFormulas(std::vector> const& formulas, std::map const& substitution); std::vector> parseFormulasForExplicit(std::string const& inputString); std::vector> parseFormulasForPrismProgram(std::string const& inputString, storm::prism::Program const& program); std::vector> parseFormulasForJaniModel(std::string const& inputString, storm::jani::Model const& model); diff --git a/src/test/modelchecker/NativeHybridDtmcPrctlModelCheckerTest.cpp b/src/test/modelchecker/NativeHybridDtmcPrctlModelCheckerTest.cpp index 66dc75a61..6398b2c1e 100644 --- a/src/test/modelchecker/NativeHybridDtmcPrctlModelCheckerTest.cpp +++ b/src/test/modelchecker/NativeHybridDtmcPrctlModelCheckerTest.cpp @@ -18,7 +18,7 @@ #include "storm/settings/modules/GmmxxEquationSolverSettings.h" #include "storm/settings/modules/NativeEquationSolverSettings.h" -TEST(NativeHybridDtmcPrctlModelCheckerTest, Die_CUDD) { +TEST(NativeHybridDtmcPrctlModelCheckerTest, Die_Cudd) { storm::storage::SymbolicModelDescription modelDescription = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/dtmc/die.pm"); storm::prism::Program program = modelDescription.preprocess().asPrismProgram(); @@ -142,7 +142,7 @@ TEST(NativeHybridDtmcPrctlModelCheckerTest, Die_Sylvan) { EXPECT_NEAR(3.6666646003723145, quantitativeResult4.getMax(), storm::settings::getModule().getPrecision()); } -TEST(NativeHybridDtmcPrctlModelCheckerTest, Crowds_CUDD) { +TEST(NativeHybridDtmcPrctlModelCheckerTest, Crowds_Cudd) { storm::storage::SymbolicModelDescription modelDescription = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/dtmc/crowds-5-5.pm"); storm::prism::Program program = modelDescription.preprocess().asPrismProgram(); @@ -232,7 +232,7 @@ TEST(NativeHybridDtmcPrctlModelCheckerTest, Crowds_Sylvan) { EXPECT_NEAR(0.32153900158185761, quantitativeResult3.getMax(), storm::settings::getModule().getPrecision()); } -TEST(NativeHybridDtmcPrctlModelCheckerTest, SynchronousLeader_CUDD) { +TEST(NativeHybridDtmcPrctlModelCheckerTest, SynchronousLeader_Cudd) { storm::storage::SymbolicModelDescription modelDescription = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/dtmc/leader-3-5.pm"); storm::prism::Program program = modelDescription.preprocess().asPrismProgram();