From 16fafbcfccd40adc65d3338e82772465aca7b6f2 Mon Sep 17 00:00:00 2001 From: Stefan Pranger Date: Tue, 16 Feb 2021 17:16:47 +0100 Subject: [PATCH] properties now hold information about shield query --- src/storm/storage/jani/Property.cpp | 47 +++++++++------- src/storm/storage/jani/Property.h | 84 +++++++++++++++++------------ 2 files changed, 78 insertions(+), 53 deletions(-) diff --git a/src/storm/storage/jani/Property.cpp b/src/storm/storage/jani/Property.cpp index add01f24d..988d23da4 100644 --- a/src/storm/storage/jani/Property.cpp +++ b/src/storm/storage/jani/Property.cpp @@ -2,21 +2,26 @@ namespace storm { namespace jani { - + std::ostream& operator<<(std::ostream& os, FilterExpression const& fe) { 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 const& formula, std::set const& undefinedConstants, std::string const& comment) : name(name), comment(comment), filterExpression(FilterExpression(formula)), undefinedConstants(undefinedConstants) { // Intentionally left empty. } - + Property::Property(std::string const& name, FilterExpression const& fe, std::set const& undefinedConstants, std::string const& comment) : name(name), comment(comment), filterExpression(fe), undefinedConstants(undefinedConstants) { // Intentionally left empty. } + Property::Property(std::string const& name, std::shared_ptr const& formula, std::set const& undefinedConstants, storm::logic::ShieldExpression shieldExpression, std::string const& comment) + : name(name), comment(comment), filterExpression(FilterExpression(formula)), undefinedConstants(undefinedConstants), shieldingExpression(shieldingExpression) { + // Intentionally left empty. + } + std::string const& Property::getName() const { return this->name; } @@ -24,7 +29,7 @@ namespace storm { std::string const& Property::getComment() const { return this->comment; } - + std::string Property::asPrismSyntax() const { std::stringstream stream; if (!this->getName().empty()) { @@ -41,13 +46,13 @@ namespace storm { stream << ")"; } stream << ";"; - + if (!this->getComment().empty()) { stream << " // " << this->getComment(); } return stream.str(); } - + Property Property::substitute(std::map const& substitution) const { std::set remainingUndefinedConstants; for (auto const& constant : undefinedConstants) { @@ -57,7 +62,7 @@ namespace storm { } return Property(name, filterExpression.substitute(substitution), remainingUndefinedConstants, comment); } - + Property Property::substitute(std::function const& substitutionFunction) const { std::set remainingUndefinedConstants; for (auto const& constant : undefinedConstants) { @@ -65,42 +70,46 @@ namespace storm { } return Property(name, filterExpression.substitute(substitutionFunction), remainingUndefinedConstants, comment); } - + Property Property::substituteLabels(std::map const& substitution) const { return Property(name, filterExpression.substituteLabels(substitution), undefinedConstants, comment); } - + Property Property::substituteRewardModelNames(std::map const& rewardModelNameSubstitution) const { return Property(name, filterExpression.substituteRewardModelNames(rewardModelNameSubstitution), undefinedConstants, comment); } - + Property Property::clone() const { return Property(name, filterExpression.clone(), undefinedConstants, comment); } - + FilterExpression const& Property::getFilter() const { return this->filterExpression; } - + std::shared_ptr Property::getRawFormula() const { return this->filterExpression.getFormula(); } - + + bool Property::isShieldingProperty() const { + return shieldingExpression.is_initialized(); + } + std::set const& Property::getUndefinedConstants() const { return undefinedConstants; } - + bool Property::containsUndefinedConstants() const { return !undefinedConstants.empty(); } - + std::set Property::getUsedVariablesAndConstants() const { auto res = getUndefinedConstants(); getFilter().getFormula()->gatherUsedVariables(res); getFilter().getStatesFormula()->gatherUsedVariables(res); return res; } - + std::set Property::getUsedLabels() const { std::set res; auto labFormSet = getFilter().getFormula()->getAtomicLabelFormulas(); @@ -113,15 +122,15 @@ namespace storm { } return res; } - + void Property::gatherReferencedRewardModels(std::set& rewardModelNames) const { getFilter().getFormula()->gatherReferencedRewardModels(rewardModelNames); getFilter().getStatesFormula()->gatherReferencedRewardModels(rewardModelNames); } - + std::ostream& operator<<(std::ostream& os, Property const& p) { return os << "(" << p.getName() << "): " << p.getFilter(); } - + } } diff --git a/src/storm/storage/jani/Property.h b/src/storm/storage/jani/Property.h index 757db04a8..91bb9a22a 100644 --- a/src/storm/storage/jani/Property.h +++ b/src/storm/storage/jani/Property.h @@ -2,19 +2,22 @@ #include +#include + #include "storm/modelchecker/results/FilterType.h" #include "storm/logic/Formulas.h" #include "storm/logic/FragmentSpecification.h" #include "storm/logic/CloneVisitor.h" +#include "storm/logic/ShieldExpression.h" #include "storm/utility/macros.h" #include "storm/exceptions/InvalidArgumentException.h" namespace storm { namespace jani { - + /** - * Property intervals as per Jani Specification. + * Property intervals as per Jani Specification. * Currently mainly used to help parsing. */ struct PropertyInterval { @@ -22,29 +25,29 @@ namespace storm { bool lowerBoundStrict = false; storm::expressions::Expression upperBound; bool upperBoundStrict = false; - + bool hasLowerBound() const { return lowerBound.isInitialized(); } - + bool hasUpperBound() const { return upperBound.isInitialized(); } }; - - + + class FilterExpression { public: FilterExpression() = default; - + explicit FilterExpression(std::shared_ptr formula, storm::modelchecker::FilterType ft = storm::modelchecker::FilterType::VALUES, std::shared_ptr const& statesFormula = std::make_shared("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 const& getFormula() const { return formula; } - + std::shared_ptr const& getStatesFormula() const { return statesFormula; } @@ -52,48 +55,48 @@ namespace storm { storm::modelchecker::FilterType getFilterType() const { return ft; } - + bool isDefault() const { return (ft == storm::modelchecker::FilterType::VALUES) && statesFormula && statesFormula->isInitialFormula(); } - + FilterExpression substitute(std::map const& substitution) const { return FilterExpression(formula->substitute(substitution), ft, statesFormula->substitute(substitution)); } - + FilterExpression substitute(std::function const& substitutionFunction) const { return FilterExpression(formula->substitute(substitutionFunction), ft, statesFormula->substitute(substitutionFunction)); } - + FilterExpression substituteLabels(std::map const& labelSubstitution) const { return FilterExpression(formula->substitute(labelSubstitution), ft, statesFormula->substitute(labelSubstitution)); } - + FilterExpression substituteRewardModelNames(std::map const& rewardModelNameSubstitution) const { return FilterExpression(formula->substituteRewardModelNames(rewardModelNameSubstitution), ft, statesFormula->substituteRewardModelNames(rewardModelNameSubstitution)); } - + FilterExpression clone() const { storm::logic::CloneVisitor cv; return FilterExpression(cv.clone(*formula), ft, cv.clone(*statesFormula)); } - + private: // For now, we assume that the states are always the initial states. std::shared_ptr formula; storm::modelchecker::FilterType ft; std::shared_ptr statesFormula; }; - - + + std::ostream& operator<<(std::ostream& os, FilterExpression const& fe); - - - + + + class Property { public: Property() = default; - + /** * Constructs the property * @param name the name @@ -102,7 +105,7 @@ namespace storm { * @param comment An optional comment */ Property(std::string const& name, std::shared_ptr const& formula, std::set const& undefinedConstants, std::string const& comment = ""); - + /** * Constructs the property * @param name the name @@ -110,46 +113,59 @@ namespace storm { * @param comment An optional comment */ Property(std::string const& name, FilterExpression const& fe, std::set const& undefinedConstants, std::string const& comment = ""); - + + /** + * Constructs the property + * @param name the name + * @param formula the formula representation + * @param shieldExpression the shielding expression + * @param comment An optional comment + */ + Property(std::string const& name, std::shared_ptr const& formula, std::set const& undefinedConstants, storm::logic::ShieldExpression shieldExpression, std::string const& comment = ""); + /** * Get the provided name * @return the name */ std::string const& getName() const; - + /** * Get the provided comment, if any * @return the comment */ std::string const& getComment() const; - + Property substitute(std::map const& substitution) const; Property substitute(std::function const& substitutionFunction) const; Property substituteLabels(std::map const& labelSubstitution) const; Property substituteRewardModelNames(std::map const& rewardModelNameSubstitution) const; Property clone() const; - + FilterExpression const& getFilter() const; - + std::string asPrismSyntax() const; - + std::set const& getUndefinedConstants() const; bool containsUndefinedConstants() const; std::set getUsedVariablesAndConstants() const; std::set getUsedLabels() const; void gatherReferencedRewardModels(std::set& rewardModelNames) const; - + std::shared_ptr getRawFormula() const; - + + bool isShieldingProperty() const; + private: std::string name; std::string comment; FilterExpression filterExpression; std::set undefinedConstants; + + // TODO might need refactoring, this cannot be expressed by JANI yet, so this is totally wrong here. + boost::optional shieldingExpression; }; - - + + std::ostream& operator<<(std::ostream& os, Property const& p); } } -