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

first version of state filters in filter expressions

main
dehnert 8 years ago
parent
e5cbc25f00
commit
3ffaa77193
7 changed files with 94 additions and 32 deletions
Split View
  1. 76
      src/storm/cli/cli.cpp
  2. 4
      src/storm/logic/Formula.cpp
  3. 4
      src/storm/logic/Formula.h
  4. 8
      src/storm/parser/FormulaParserGrammar.cpp
  5. 4
      src/storm/parser/FormulaParserGrammar.h
  6. 13
      src/storm/storage/jani/Property.cpp
  7. 17
      src/storm/storage/jani/Property.h

76
src/storm/cli/cli.cpp
View File

@ -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;
});
}

4
src/storm/logic/Formula.cpp
View File

@ -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);
}

4
src/storm/logic/Formula.h
View File

@ -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;

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

@ -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);

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

@ -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;

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

@ -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();
}
}
}

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

@ -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;
};

Write Preview
|||||||
100:0
Loading…
Cancel
Save