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

properties now hold information about shield query

tempestpy_adaptions
Stefan Pranger 4 years ago
parent
5a2657346b
commit
16fafbcfcc
2 changed files with 78 additions and 53 deletions
Whitespace
Show all changes Ignore whitespace when comparing lines Ignore changes in amount of whitespace Ignore changes in whitespace at EOL
Split View
Diff Options
Show Stats Download Patch File Download Diff File
  1. 47
      src/storm/storage/jani/Property.cpp
  2. 84
      src/storm/storage/jani/Property.h

47
src/storm/storage/jani/Property.cpp
View File

@ -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<storm::logic::Formula const> const& formula, std::set<storm::expressions::Variable> 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<storm::expressions::Variable> 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<storm::logic::Formula const> const& formula, std::set<storm::expressions::Variable> 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<storm::expressions::Variable, storm::expressions::Expression> const& substitution) const {
std::set<storm::expressions::Variable> 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<storm::expressions::Expression(storm::expressions::Expression const&)> const& substitutionFunction) const {
std::set<storm::expressions::Variable> 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<std::string, std::string> const& substitution) const {
return Property(name, filterExpression.substituteLabels(substitution), undefinedConstants, comment);
}
Property Property::substituteRewardModelNames(std::map<std::string, std::string> 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<storm::logic::Formula const> Property::getRawFormula() const {
return this->filterExpression.getFormula();
}
bool Property::isShieldingProperty() const {
return shieldingExpression.is_initialized();
}
std::set<storm::expressions::Variable> const& Property::getUndefinedConstants() const {
return undefinedConstants;
}
bool Property::containsUndefinedConstants() const {
return !undefinedConstants.empty();
}
std::set<storm::expressions::Variable> Property::getUsedVariablesAndConstants() const {
auto res = getUndefinedConstants();
getFilter().getFormula()->gatherUsedVariables(res);
getFilter().getStatesFormula()->gatherUsedVariables(res);
return res;
}
std::set<std::string> Property::getUsedLabels() const {
std::set<std::string> res;
auto labFormSet = getFilter().getFormula()->getAtomicLabelFormulas();
@ -113,15 +122,15 @@ namespace storm {
}
return res;
}
void Property::gatherReferencedRewardModels(std::set<std::string>& 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();
}
}
}

84
src/storm/storage/jani/Property.h
View File

@ -2,19 +2,22 @@
#include <functional>
#include <boost/optional.hpp>
#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<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;
}
@ -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<storm::expressions::Variable, storm::expressions::Expression> const& substitution) const {
return FilterExpression(formula->substitute(substitution), ft, statesFormula->substitute(substitution));
}
FilterExpression substitute(std::function<storm::expressions::Expression(storm::expressions::Expression const&)> const& substitutionFunction) const {
return FilterExpression(formula->substitute(substitutionFunction), ft, statesFormula->substitute(substitutionFunction));
}
FilterExpression substituteLabels(std::map<std::string, std::string> const& labelSubstitution) const {
return FilterExpression(formula->substitute(labelSubstitution), ft, statesFormula->substitute(labelSubstitution));
}
FilterExpression substituteRewardModelNames(std::map<std::string, std::string> 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<storm::logic::Formula const> formula;
storm::modelchecker::FilterType ft;
std::shared_ptr<storm::logic::Formula const> 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<storm::logic::Formula const> const& formula, std::set<storm::expressions::Variable> 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<storm::expressions::Variable> 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<storm::logic::Formula const> const& formula, std::set<storm::expressions::Variable> 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<storm::expressions::Variable, storm::expressions::Expression> const& substitution) const;
Property substitute(std::function<storm::expressions::Expression(storm::expressions::Expression const&)> const& substitutionFunction) const;
Property substituteLabels(std::map<std::string, std::string> const& labelSubstitution) const;
Property substituteRewardModelNames(std::map<std::string, std::string> const& rewardModelNameSubstitution) const;
Property clone() const;
FilterExpression const& getFilter() const;
std::string asPrismSyntax() const;
std::set<storm::expressions::Variable> const& getUndefinedConstants() const;
bool containsUndefinedConstants() const;
std::set<storm::expressions::Variable> getUsedVariablesAndConstants() const;
std::set<std::string> getUsedLabels() const;
void gatherReferencedRewardModels(std::set<std::string>& rewardModelNames) const;
std::shared_ptr<storm::logic::Formula const> getRawFormula() const;
bool isShieldingProperty() const;
private:
std::string name;
std::string comment;
FilterExpression filterExpression;
std::set<storm::expressions::Variable> undefinedConstants;
// TODO might need refactoring, this cannot be expressed by JANI yet, so this is totally wrong here.
boost::optional<storm::logic::ShieldExpression> shieldingExpression;
};
std::ostream& operator<<(std::ostream& os, Property const& p);
}
}
Write Preview
Loading…
Cancel
Save