From 3ffaa77193881d7499e0e84c09b515c0522a77da Mon Sep 17 00:00:00 2001
From: dehnert <dehnert@cs.rwth-aachen.de>
Date: Tue, 27 Jun 2017 14:27:16 +0200
Subject: [PATCH 1/5] first version of state filters in filter expressions
---
src/storm/cli/cli.cpp | 76 ++++++++++++++++++-----
src/storm/logic/Formula.cpp | 4 ++
src/storm/logic/Formula.h | 4 +-
src/storm/parser/FormulaParserGrammar.cpp | 8 +--
src/storm/parser/FormulaParserGrammar.h | 4 +-
src/storm/storage/jani/Property.cpp | 13 ++--
src/storm/storage/jani/Property.h | 17 ++++-
7 files changed, 94 insertions(+), 32 deletions(-)
diff --git a/src/storm/cli/cli.cpp b/src/storm/cli/cli.cpp
index 0f53aa2d3..fad3709af 100644
--- a/src/storm/cli/cli.cpp
+++ b/src/storm/cli/cli.cpp
@@ -353,15 +353,27 @@ namespace storm {
return input;
}
+ std::vector<std::shared_ptr<storm::logic::Formula const>> createFormulasToRespect(std::vector<storm::jani::Property> const& properties) {
+ std::vector<std::shared_ptr<storm::logic::Formula const>> result = storm::api::extractFormulasFromProperties(properties);
+
+ for (auto const& property : properties) {
+ if (!property.getFilter().getStatesFormula()->isInitialFormula()) {
+ result.push_back(property.getFilter().getStatesFormula());
+ }
+ }
+
+ return result;
+ }
+
template <storm::dd::DdType DdType, typename ValueType>
std::shared_ptr<storm::models::ModelBase> buildModelDd(SymbolicInput const& input) {
- return storm::api::buildSymbolicModel<DdType, ValueType>(input.model.get(), storm::api::extractFormulasFromProperties(input.properties));
+ return storm::api::buildSymbolicModel<DdType, ValueType>(input.model.get(), createFormulasToRespect(input.properties));
}
template <typename ValueType>
std::shared_ptr<storm::models::ModelBase> buildModelSparse(SymbolicInput const& input, storm::settings::modules::IOSettings const& ioSettings) {
auto counterexampleGeneratorSettings = storm::settings::getModule<storm::settings::modules::CounterexampleGeneratorSettings>();
- return storm::api::buildSparseModel<ValueType>(input.model.get(), storm::api::extractFormulasFromProperties(input.properties), ioSettings.isBuildChoiceLabelsSet(), counterexampleGeneratorSettings.isMinimalCommandSetGenerationSet());
+ return storm::api::buildSparseModel<ValueType>(input.model.get(), createFormulasToRespect(input.properties), ioSettings.isBuildChoiceLabelsSet(), counterexampleGeneratorSettings.isMinimalCommandSetGenerationSet());
}
template <typename ValueType>
@@ -379,6 +391,9 @@ namespace storm {
std::shared_ptr<storm::models::ModelBase> buildModel(storm::settings::modules::CoreSettings::Engine const& engine, SymbolicInput const& input, storm::settings::modules::IOSettings const& ioSettings) {
storm::utility::Stopwatch modelBuildingWatch(true);
+
+ // Make sure that states in filter are built as label. ALso for bisimulation.
+
std::shared_ptr<storm::models::ModelBase> result;
if (input.model) {
if (engine == storm::settings::modules::CoreSettings::Engine::Dd || engine == storm::settings::modules::CoreSettings::Engine::Hybrid) {
@@ -622,11 +637,11 @@ namespace storm {
};
template<typename ValueType>
- void verifyProperties(std::vector<storm::jani::Property> const& properties, std::function<std::unique_ptr<storm::modelchecker::CheckResult>(std::shared_ptr<storm::logic::Formula const> const& formula)> const& verificationCallback, std::function<void(std::unique_ptr<storm::modelchecker::CheckResult> const&)> const& postprocessingCallback = PostprocessingIdentity()) {
+ void verifyProperties(std::vector<storm::jani::Property> const& properties, std::function<std::unique_ptr<storm::modelchecker::CheckResult>(std::shared_ptr<storm::logic::Formula const> const& formula, std::shared_ptr<storm::logic::Formula const> const& states)> const& verificationCallback, std::function<void(std::unique_ptr<storm::modelchecker::CheckResult> const&)> const& postprocessingCallback = PostprocessingIdentity()) {
for (auto const& property : properties) {
printModelCheckingProperty(property);
storm::utility::Stopwatch watch(true);
- std::unique_ptr<storm::modelchecker::CheckResult> result = verificationCallback(property.getRawFormula());
+ std::unique_ptr<storm::modelchecker::CheckResult> result = verificationCallback(property.getRawFormula(), property.getFilter().getStatesFormula());
watch.stop();
printInitialStatesResult<ValueType>(result, property, &watch);
postprocessingCallback(result);
@@ -636,7 +651,8 @@ namespace storm {
template <storm::dd::DdType DdType, typename ValueType>
void verifyWithAbstractionRefinementEngine(SymbolicInput const& input) {
STORM_LOG_ASSERT(input.model, "Expected symbolic model description.");
- verifyProperties<ValueType>(input.properties, [&input] (std::shared_ptr<storm::logic::Formula const> const& formula) {
+ verifyProperties<ValueType>(input.properties, [&input] (std::shared_ptr<storm::logic::Formula const> const& formula, std::shared_ptr<storm::logic::Formula const> const& states) {
+ STORM_LOG_THROW(states->isInitialFormula(), storm::exceptions::NotSupportedException, "Abstraction-refinement can only filter initial states.");
return storm::api::verifyWithAbstractionRefinementEngine<DdType, ValueType>(input.model.get(), storm::api::createTask<ValueType>(formula, true));
});
}
@@ -645,7 +661,8 @@ namespace storm {
void verifyWithExplorationEngine(SymbolicInput const& input) {
STORM_LOG_ASSERT(input.model, "Expected symbolic model description.");
STORM_LOG_THROW((std::is_same<ValueType, double>::value), storm::exceptions::NotSupportedException, "Exploration does not support other data-types than floating points.");
- verifyProperties<ValueType>(input.properties, [&input] (std::shared_ptr<storm::logic::Formula const> const& formula) {
+ verifyProperties<ValueType>(input.properties, [&input] (std::shared_ptr<storm::logic::Formula const> const& formula, std::shared_ptr<storm::logic::Formula const> const& states) {
+ STORM_LOG_THROW(states->isInitialFormula(), storm::exceptions::NotSupportedException, "Exploration can only filter initial states.");
return storm::api::verifyWithExplorationEngine<ValueType>(input.model.get(), storm::api::createTask<ValueType>(formula, true));
});
}
@@ -654,9 +671,18 @@ namespace storm {
void verifyWithSparseEngine(std::shared_ptr<storm::models::ModelBase> const& model, SymbolicInput const& input) {
auto sparseModel = model->as<storm::models::sparse::Model<ValueType>>();
verifyProperties<ValueType>(input.properties,
- [&sparseModel] (std::shared_ptr<storm::logic::Formula const> const& formula) {
- std::unique_ptr<storm::modelchecker::CheckResult> result = storm::api::verifyWithSparseEngine<ValueType>(sparseModel, storm::api::createTask<ValueType>(formula, true));
- result->filter(storm::modelchecker::ExplicitQualitativeCheckResult(sparseModel->getInitialStates()));
+ [&sparseModel] (std::shared_ptr<storm::logic::Formula const> const& formula, std::shared_ptr<storm::logic::Formula const> const& states) {
+ bool filterForInitialStates = states->isInitialFormula();
+ auto task = storm::api::createTask<ValueType>(formula, filterForInitialStates);
+ std::unique_ptr<storm::modelchecker::CheckResult> result = storm::api::verifyWithSparseEngine<ValueType>(sparseModel, task);
+
+ std::unique_ptr<storm::modelchecker::CheckResult> filter;
+ if (filterForInitialStates) {
+ filter = std::make_unique<storm::modelchecker::ExplicitQualitativeCheckResult>(sparseModel->getInitialStates());
+ } else {
+ filter = storm::api::verifyWithSparseEngine<ValueType>(sparseModel, storm::api::createTask<ValueType>(states, false));
+ }
+ result->filter(filter->asQualitativeCheckResult());
return result;
},
[&sparseModel] (std::unique_ptr<storm::modelchecker::CheckResult> const& result) {
@@ -670,20 +696,42 @@ namespace storm {
template <storm::dd::DdType DdType, typename ValueType>
void verifyWithHybridEngine(std::shared_ptr<storm::models::ModelBase> const& model, SymbolicInput const& input) {
- verifyProperties<ValueType>(input.properties, [&model] (std::shared_ptr<storm::logic::Formula const> const& formula) {
+ verifyProperties<ValueType>(input.properties, [&model] (std::shared_ptr<storm::logic::Formula const> const& formula, std::shared_ptr<storm::logic::Formula const> const& states) {
+ bool filterForInitialStates = states->isInitialFormula();
+ auto task = storm::api::createTask<ValueType>(formula, filterForInitialStates);
+
auto symbolicModel = model->as<storm::models::symbolic::Model<DdType, ValueType>>();
- std::unique_ptr<storm::modelchecker::CheckResult> result = storm::api::verifyWithHybridEngine<DdType, ValueType>(symbolicModel, storm::api::createTask<ValueType>(formula, true));
- result->filter(storm::modelchecker::SymbolicQualitativeCheckResult<DdType>(symbolicModel->getReachableStates(), symbolicModel->getInitialStates()));
+ std::unique_ptr<storm::modelchecker::CheckResult> result = storm::api::verifyWithHybridEngine<DdType, ValueType>(symbolicModel, task);
+
+ std::unique_ptr<storm::modelchecker::CheckResult> filter;
+ if (filterForInitialStates) {
+ filter = std::make_unique<storm::modelchecker::SymbolicQualitativeCheckResult<DdType>>(symbolicModel->getReachableStates(), symbolicModel->getInitialStates());
+ } else {
+ filter = storm::api::verifyWithHybridEngine<DdType, ValueType>(symbolicModel, storm::api::createTask<ValueType>(states, false));
+ }
+
+ result->filter(filter->asQualitativeCheckResult());
return result;
});
}
template <storm::dd::DdType DdType, typename ValueType>
void verifyWithDdEngine(std::shared_ptr<storm::models::ModelBase> const& model, SymbolicInput const& input) {
- verifyProperties<ValueType>(input.properties, [&model] (std::shared_ptr<storm::logic::Formula const> const& formula) {
+ verifyProperties<ValueType>(input.properties, [&model] (std::shared_ptr<storm::logic::Formula const> const& formula, std::shared_ptr<storm::logic::Formula const> const& states) {
+ bool filterForInitialStates = states->isInitialFormula();
+ auto task = storm::api::createTask<ValueType>(formula, filterForInitialStates);
+
auto symbolicModel = model->as<storm::models::symbolic::Model<DdType, ValueType>>();
std::unique_ptr<storm::modelchecker::CheckResult> result = storm::api::verifyWithDdEngine<DdType, ValueType>(model->as<storm::models::symbolic::Model<DdType, ValueType>>(), storm::api::createTask<ValueType>(formula, true));
- result->filter(storm::modelchecker::SymbolicQualitativeCheckResult<DdType>(symbolicModel->getReachableStates(), symbolicModel->getInitialStates()));
+
+ std::unique_ptr<storm::modelchecker::CheckResult> filter;
+ if (filterForInitialStates) {
+ filter = std::make_unique<storm::modelchecker::SymbolicQualitativeCheckResult<DdType>>(symbolicModel->getReachableStates(), symbolicModel->getInitialStates());
+ } else {
+ filter = storm::api::verifyWithDdEngine<DdType, ValueType>(symbolicModel, storm::api::createTask<ValueType>(states, false));
+ }
+
+ result->filter(filter->asQualitativeCheckResult());
return result;
});
}
diff --git a/src/storm/logic/Formula.cpp b/src/storm/logic/Formula.cpp
index 9038a2307..3f871908e 100644
--- a/src/storm/logic/Formula.cpp
+++ b/src/storm/logic/Formula.cpp
@@ -175,6 +175,10 @@ namespace storm {
return std::shared_ptr<Formula const>(new BooleanLiteralFormula(true));
}
+ bool Formula::isInitialFormula() const {
+ return this->isAtomicLabelFormula() && this->asAtomicLabelFormula().getLabel() == "init";
+ }
+
PathFormula& Formula::asPathFormula() {
return dynamic_cast<PathFormula&>(*this);
}
diff --git a/src/storm/logic/Formula.h b/src/storm/logic/Formula.h
index 2ad5e9477..a76dd0ef7 100644
--- a/src/storm/logic/Formula.h
+++ b/src/storm/logic/Formula.h
@@ -93,10 +93,12 @@ namespace storm {
bool isInFragment(FragmentSpecification const& fragment) const;
FormulaInformation info() const;
-
+
virtual boost::any accept(FormulaVisitor const& visitor, boost::any const& data = boost::any()) const = 0;
static std::shared_ptr<Formula const> getTrueFormula();
+
+ bool isInitialFormula() const;
PathFormula& asPathFormula();
PathFormula const& asPathFormula() const;
diff --git a/src/storm/parser/FormulaParserGrammar.cpp b/src/storm/parser/FormulaParserGrammar.cpp
index bee6b5117..78102f859 100644
--- a/src/storm/parser/FormulaParserGrammar.cpp
+++ b/src/storm/parser/FormulaParserGrammar.cpp
@@ -128,7 +128,7 @@ namespace storm {
#pragma clang diagnostic push
#pragma clang diagnostic ignored "-Woverloaded-shift-op-parentheses"
- filterProperty = (-formulaName >> qi::lit("filter") > qi::lit("(") > filterType_ > qi::lit(",") > stateFormula > -(qi::lit(",") > qi::lit("\"init\"") > qi::lit(")")))[qi::_val = phoenix::bind(&FormulaParserGrammar::createProperty, phoenix::ref(*this), qi::_1, qi::_2, qi::_3)] | (-formulaName >> stateFormula)[qi::_val = phoenix::bind(&FormulaParserGrammar::createPropertyWithDefaultFilterType, phoenix::ref(*this), qi::_1, qi::_2)];
+ filterProperty = (-formulaName >> qi::lit("filter") > qi::lit("(") > filterType_ > qi::lit(",") > stateFormula > qi::lit(",") > stateFormula > qi::lit(")"))[qi::_val = phoenix::bind(&FormulaParserGrammar::createProperty, phoenix::ref(*this), qi::_1, qi::_2, qi::_3, qi::_4)] | (-formulaName >> stateFormula)[qi::_val = phoenix::bind(&FormulaParserGrammar::createPropertyWithDefaultFilterTypeAndStates, phoenix::ref(*this), qi::_1, qi::_2)];
filterProperty.name("filter property");
#pragma clang diagnostic pop
@@ -332,8 +332,8 @@ namespace storm {
return std::shared_ptr<storm::logic::Formula const>(new storm::logic::MultiObjectiveFormula(subformulas));
}
- storm::jani::Property FormulaParserGrammar::createProperty(boost::optional<std::string> const& propertyName, storm::modelchecker::FilterType const& filterType, std::shared_ptr<storm::logic::Formula const> const& formula) {
- storm::jani::FilterExpression filterExpression(formula, filterType);
+ storm::jani::Property FormulaParserGrammar::createProperty(boost::optional<std::string> const& propertyName, storm::modelchecker::FilterType const& filterType, std::shared_ptr<storm::logic::Formula const> const& formula, std::shared_ptr<storm::logic::Formula const> const& states) {
+ storm::jani::FilterExpression filterExpression(formula, filterType, states);
++propertyCount;
if (propertyName) {
@@ -343,7 +343,7 @@ namespace storm {
}
}
- storm::jani::Property FormulaParserGrammar::createPropertyWithDefaultFilterType(boost::optional<std::string> const& propertyName, std::shared_ptr<storm::logic::Formula const> const& formula) {
+ storm::jani::Property FormulaParserGrammar::createPropertyWithDefaultFilterTypeAndStates(boost::optional<std::string> const& propertyName, std::shared_ptr<storm::logic::Formula const> const& formula) {
++propertyCount;
if (propertyName) {
return storm::jani::Property(propertyName.get(), formula);
diff --git a/src/storm/parser/FormulaParserGrammar.h b/src/storm/parser/FormulaParserGrammar.h
index 79b272246..7ae6740b8 100644
--- a/src/storm/parser/FormulaParserGrammar.h
+++ b/src/storm/parser/FormulaParserGrammar.h
@@ -223,8 +223,8 @@ namespace storm {
std::shared_ptr<storm::logic::Formula const> createUnaryBooleanStateFormula(std::shared_ptr<storm::logic::Formula const> const& subformula, boost::optional<storm::logic::UnaryBooleanStateFormula::OperatorType> const& operatorType);
std::shared_ptr<storm::logic::Formula const> createMultiObjectiveFormula(std::vector<std::shared_ptr<storm::logic::Formula const>> const& subformulas);
- storm::jani::Property createProperty(boost::optional<std::string> const& propertyName, storm::modelchecker::FilterType const& filterType, std::shared_ptr<storm::logic::Formula const> const& formula);
- storm::jani::Property createPropertyWithDefaultFilterType(boost::optional<std::string> const& propertyName, std::shared_ptr<storm::logic::Formula const> const& formula);
+ storm::jani::Property createProperty(boost::optional<std::string> const& propertyName, storm::modelchecker::FilterType const& filterType, std::shared_ptr<storm::logic::Formula const> const& formula, std::shared_ptr<storm::logic::Formula const> const& states);
+ storm::jani::Property createPropertyWithDefaultFilterTypeAndStates(boost::optional<std::string> const& propertyName, std::shared_ptr<storm::logic::Formula const> const& formula);
// An error handler function.
phoenix::function<SpiritErrorHandler> handler;
diff --git a/src/storm/storage/jani/Property.cpp b/src/storm/storage/jani/Property.cpp
index e46d2ee50..73c6d0dec 100644
--- a/src/storm/storage/jani/Property.cpp
+++ b/src/storm/storage/jani/Property.cpp
@@ -5,19 +5,17 @@ namespace storm {
std::ostream& operator<<(std::ostream& os, FilterExpression const& fe) {
- return os << "Obtain " << toString(fe.getFilterType()) << " of the 'initial'-states with values described by '" << *fe.getFormula() << "'";
+ return os << "Obtain " << toString(fe.getFilterType()) << " of the '" << fe.getStatesFormula() << "'-states with values described by '" << *fe.getFormula() << "'";
}
Property::Property(std::string const& name, std::shared_ptr<storm::logic::Formula const> const& formula, std::string const& comment)
- : name(name), comment(comment), filterExpression(FilterExpression(formula))
- {
-
+ : name(name), comment(comment), filterExpression(FilterExpression(formula)) {
+ // Intentionally left empty.
}
Property::Property(std::string const& name, FilterExpression const& fe, std::string const& comment)
- : name(name), comment(comment), filterExpression(fe)
- {
-
+ : name(name), comment(comment), filterExpression(fe) {
+ // Intentionally left empty.
}
std::string const& Property::getName() const {
@@ -48,6 +46,5 @@ namespace storm {
return os << "(" << p.getName() << ") : " << p.getFilter();
}
-
}
}
diff --git a/src/storm/storage/jani/Property.h b/src/storm/storage/jani/Property.h
index 52db07fef..74aceab5c 100644
--- a/src/storm/storage/jani/Property.h
+++ b/src/storm/storage/jani/Property.h
@@ -2,6 +2,10 @@
#include "storm/modelchecker/results/FilterType.h"
#include "storm/logic/Formulas.h"
+#include "storm/logic/FragmentSpecification.h"
+
+#include "storm/utility/macros.h"
+#include "storm/exceptions/InvalidArgumentException.h"
namespace storm {
namespace jani {
@@ -30,28 +34,35 @@ namespace storm {
public:
FilterExpression() = default;
- explicit FilterExpression(std::shared_ptr<storm::logic::Formula const> formula, storm::modelchecker::FilterType ft = storm::modelchecker::FilterType::VALUES) : formula(formula), ft(ft) {}
+ explicit FilterExpression(std::shared_ptr<storm::logic::Formula const> formula, storm::modelchecker::FilterType ft = storm::modelchecker::FilterType::VALUES, std::shared_ptr<storm::logic::Formula const> const& statesFormula = std::make_shared<storm::logic::AtomicLabelFormula>("init")) : formula(formula), ft(ft), statesFormula(statesFormula) {
+ STORM_LOG_THROW(statesFormula->isInFragment(storm::logic::propositional()), storm::exceptions::InvalidArgumentException, "Can only filter by propositional formula.");
+ }
std::shared_ptr<storm::logic::Formula const> const& getFormula() const {
return formula;
}
+ std::shared_ptr<storm::logic::Formula const> const& getStatesFormula() const {
+ return statesFormula;
+ }
+
storm::modelchecker::FilterType getFilterType() const {
return ft;
}
FilterExpression substitute(std::map<storm::expressions::Variable, storm::expressions::Expression> const& substitution) const {
- return FilterExpression(formula->substitute(substitution), ft);
+ return FilterExpression(formula->substitute(substitution), ft, statesFormula->substitute(substitution));
}
FilterExpression substituteLabels(std::map<std::string, std::string> const& labelSubstitution) const {
- return FilterExpression(formula->substitute(labelSubstitution), ft);
+ return FilterExpression(formula->substitute(labelSubstitution), ft, statesFormula->substitute(labelSubstitution));
}
private:
// For now, we assume that the states are always the initial states.
std::shared_ptr<storm::logic::Formula const> formula;
storm::modelchecker::FilterType ft;
+ std::shared_ptr<storm::logic::Formula const> statesFormula;
};
From bc373475ff34eb755931453f9b4fed82b5204a77 Mon Sep 17 00:00:00 2001
From: dehnert <dehnert@cs.rwth-aachen.de>
Date: Tue, 27 Jun 2017 14:31:26 +0200
Subject: [PATCH 2/5] respecting state filters in bisimulation
---
src/storm/cli/cli.cpp | 5 +----
1 file changed, 1 insertion(+), 4 deletions(-)
diff --git a/src/storm/cli/cli.cpp b/src/storm/cli/cli.cpp
index fad3709af..8fea01e61 100644
--- a/src/storm/cli/cli.cpp
+++ b/src/storm/cli/cli.cpp
@@ -391,9 +391,6 @@ namespace storm {
std::shared_ptr<storm::models::ModelBase> buildModel(storm::settings::modules::CoreSettings::Engine const& engine, SymbolicInput const& input, storm::settings::modules::IOSettings const& ioSettings) {
storm::utility::Stopwatch modelBuildingWatch(true);
-
- // Make sure that states in filter are built as label. ALso for bisimulation.
-
std::shared_ptr<storm::models::ModelBase> result;
if (input.model) {
if (engine == storm::settings::modules::CoreSettings::Engine::Dd || engine == storm::settings::modules::CoreSettings::Engine::Hybrid) {
@@ -432,7 +429,7 @@ namespace storm {
}
STORM_LOG_INFO("Performing bisimulation minimization...");
- return storm::api::performBisimulationMinimization<ValueType>(model, storm::api::extractFormulasFromProperties(input.properties), bisimType);
+ return storm::api::performBisimulationMinimization<ValueType>(model, createFormulasToRespect(input.properties), bisimType);
}
template <typename ValueType>
From 322808db5b938ebdd896a8bb13cbd7fe5e9f10c6 Mon Sep 17 00:00:00 2001
From: TimQu <tim.quatmann@cs.rwth-aachen.de>
Date: Tue, 4 Jul 2017 10:47:44 +0200
Subject: [PATCH 3/5] getting reward name from reward bounded until formula.
---
src/storm/logic/TimeBoundType.h | 5 +++++
1 file changed, 5 insertions(+)
diff --git a/src/storm/logic/TimeBoundType.h b/src/storm/logic/TimeBoundType.h
index 2488baaaf..7200cc89d 100644
--- a/src/storm/logic/TimeBoundType.h
+++ b/src/storm/logic/TimeBoundType.h
@@ -36,6 +36,11 @@ namespace storm {
bool isRewardBound() const {
return type == TimeBoundType::Reward;
}
+
+ std::string const& getRewardName() const {
+ assert(isRewardBound());
+ return rewardName;
+ }
};
From d0551c1d593a9f4756d75c507c858f8cead9dd76 Mon Sep 17 00:00:00 2001
From: TimQu <tim.quatmann@cs.rwth-aachen.de>
Date: Tue, 4 Jul 2017 10:48:26 +0200
Subject: [PATCH 4/5] getting time/step/reward bounds as rational number
---
src/storm/logic/BoundedUntilFormula.cpp | 17 +++++++++++++++++
1 file changed, 17 insertions(+)
diff --git a/src/storm/logic/BoundedUntilFormula.cpp b/src/storm/logic/BoundedUntilFormula.cpp
index 66b5a29fa..b954d4720 100644
--- a/src/storm/logic/BoundedUntilFormula.cpp
+++ b/src/storm/logic/BoundedUntilFormula.cpp
@@ -1,5 +1,6 @@
#include "storm/logic/BoundedUntilFormula.h"
+#include "storm/utility/constants.h"
#include "storm/utility/macros.h"
#include "storm/exceptions/InvalidArgumentException.h"
@@ -80,6 +81,22 @@ namespace storm {
return bound;
}
+ template <>
+ storm::RationalNumber BoundedUntilFormula::getLowerBound() const {
+ checkNoVariablesInBound(this->getLowerBound());
+ storm::RationalNumber bound = this->getLowerBound().evaluateAsRational();
+ STORM_LOG_THROW(bound >= storm::utility::zero<storm::RationalNumber>(), storm::exceptions::InvalidPropertyException, "Time-bound must not evaluate to negative number.");
+ return bound;
+ }
+
+ template <>
+ storm::RationalNumber BoundedUntilFormula::getUpperBound() const {
+ checkNoVariablesInBound(this->getUpperBound());
+ storm::RationalNumber bound = this->getLowerBound().evaluateAsRational();
+ STORM_LOG_THROW(bound >= storm::utility::zero<storm::RationalNumber>(), storm::exceptions::InvalidPropertyException, "Time-bound must not evaluate to negative number.");
+ return bound;
+ }
+
template <>
uint64_t BoundedUntilFormula::getLowerBound() const {
checkNoVariablesInBound(this->getLowerBound());
From 6471bfdcea68e60831008fbd1f806358e4a328c8 Mon Sep 17 00:00:00 2001
From: dehnert <dehnert@cs.rwth-aachen.de>
Date: Tue, 4 Jul 2017 11:17:01 +0200
Subject: [PATCH 5/5] made cli output respect filters
---
src/storm/cli/cli.cpp | 8 +++++---
src/storm/modelchecker/results/CheckResult.cpp | 18 ++++++++++++++++++
src/storm/modelchecker/results/CheckResult.h | 10 +++-------
3 files changed, 26 insertions(+), 10 deletions(-)
diff --git a/src/storm/cli/cli.cpp b/src/storm/cli/cli.cpp
index 8fea01e61..10f992d96 100644
--- a/src/storm/cli/cli.cpp
+++ b/src/storm/cli/cli.cpp
@@ -615,9 +615,11 @@ namespace storm {
}
template<typename ValueType>
- void printInitialStatesResult(std::unique_ptr<storm::modelchecker::CheckResult> const& result, storm::jani::Property const& property, storm::utility::Stopwatch* watch = nullptr) {
+ void printResult(std::unique_ptr<storm::modelchecker::CheckResult> const& result, storm::jani::Property const& property, storm::utility::Stopwatch* watch = nullptr) {
if (result) {
- STORM_PRINT_AND_LOG("Result (initial states): ");
+ std::stringstream ss;
+ ss << "'" << *property.getFilter().getStatesFormula() << "'";
+ STORM_PRINT_AND_LOG("Result (for " << (property.getFilter().getStatesFormula()->isInitialFormula() ? "initial" : ss.str()) << " states): ");
printFilteredResult<ValueType>(result, property.getFilter().getFilterType());
if (watch) {
STORM_PRINT_AND_LOG("Time for model checking: " << *watch << "." << std::endl);
@@ -640,8 +642,8 @@ namespace storm {
storm::utility::Stopwatch watch(true);
std::unique_ptr<storm::modelchecker::CheckResult> result = verificationCallback(property.getRawFormula(), property.getFilter().getStatesFormula());
watch.stop();
- printInitialStatesResult<ValueType>(result, property, &watch);
postprocessingCallback(result);
+ printResult<ValueType>(result, property, &watch);
}
}
diff --git a/src/storm/modelchecker/results/CheckResult.cpp b/src/storm/modelchecker/results/CheckResult.cpp
index bdcf68c8f..9155057d3 100644
--- a/src/storm/modelchecker/results/CheckResult.cpp
+++ b/src/storm/modelchecker/results/CheckResult.cpp
@@ -113,6 +113,15 @@ namespace storm {
return dynamic_cast<QualitativeCheckResult const&>(*this);
}
+ template<typename ValueType>
+ QuantitativeCheckResult<ValueType>& CheckResult::asQuantitativeCheckResult() {
+ return static_cast<QuantitativeCheckResult<ValueType> &>(*this);
+ }
+
+ template<typename ValueType>
+ QuantitativeCheckResult<ValueType> const& CheckResult::asQuantitativeCheckResult() const {
+ return static_cast<QuantitativeCheckResult<ValueType> const&>(*this);
+ }
template <storm::dd::DdType Type>
SymbolicQualitativeCheckResult<Type>& CheckResult::asSymbolicQualitativeCheckResult() {
@@ -155,6 +164,9 @@ namespace storm {
}
// Explicitly instantiate the template functions.
+ template QuantitativeCheckResult<double>& CheckResult::asQuantitativeCheckResult();
+ template QuantitativeCheckResult<double> const& CheckResult::asQuantitativeCheckResult() const;
+
template ExplicitQuantitativeCheckResult<double>& CheckResult::asExplicitQuantitativeCheckResult();
template ExplicitQuantitativeCheckResult<double> const& CheckResult::asExplicitQuantitativeCheckResult() const;
template ExplicitParetoCurveCheckResult<double>& CheckResult::asExplicitParetoCurveCheckResult();
@@ -184,9 +196,15 @@ namespace storm {
#ifdef STORM_HAVE_CARL
+ template QuantitativeCheckResult<storm::RationalNumber>& CheckResult::asQuantitativeCheckResult();
+ template QuantitativeCheckResult<storm::RationalNumber> const& CheckResult::asQuantitativeCheckResult() const;
+
template ExplicitQuantitativeCheckResult<storm::RationalNumber>& CheckResult::asExplicitQuantitativeCheckResult();
template ExplicitQuantitativeCheckResult<storm::RationalNumber> const& CheckResult::asExplicitQuantitativeCheckResult() const;
+ template QuantitativeCheckResult<storm::RationalFunction>& CheckResult::asQuantitativeCheckResult();
+ template QuantitativeCheckResult<storm::RationalFunction> const& CheckResult::asQuantitativeCheckResult() const;
+
template ExplicitQuantitativeCheckResult<storm::RationalFunction>& CheckResult::asExplicitQuantitativeCheckResult();
template ExplicitQuantitativeCheckResult<storm::RationalFunction> const& CheckResult::asExplicitQuantitativeCheckResult() const;
diff --git a/src/storm/modelchecker/results/CheckResult.h b/src/storm/modelchecker/results/CheckResult.h
index 2cff249c9..43954a220 100644
--- a/src/storm/modelchecker/results/CheckResult.h
+++ b/src/storm/modelchecker/results/CheckResult.h
@@ -66,14 +66,10 @@ namespace storm {
QualitativeCheckResult const& asQualitativeCheckResult() const;
template<typename ValueType>
- QuantitativeCheckResult<ValueType>& asQuantitativeCheckResult() {
- return static_cast<QuantitativeCheckResult<ValueType> &>(*this);
- }
+ QuantitativeCheckResult<ValueType>& asQuantitativeCheckResult();
+
template<typename ValueType>
- QuantitativeCheckResult<ValueType> const& asQuantitativeCheckResult() const {
- return static_cast<QuantitativeCheckResult<ValueType> const&>(*this);
- }
-
+ QuantitativeCheckResult<ValueType> const& asQuantitativeCheckResult() const;
ExplicitQualitativeCheckResult& asExplicitQualitativeCheckResult();
ExplicitQualitativeCheckResult const& asExplicitQualitativeCheckResult() const;