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

added printout for shielding queries

main
Stefan Pranger 5 years ago
parent
283f4ea6a2
commit
00479b4877
1 changed files with 148 additions and 138 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. 28
      src/storm-cli-utilities/model-handling.h

28
src/storm-cli-utilities/model-handling.h
View File

@ -837,6 +837,9 @@ namespace storm {
}
void printModelCheckingProperty(storm::jani::Property const& property) {
if(property.isShieldingProperty()) {
STORM_PRINT(std::endl << "Creating " << *(property.getShieldingExpression()) << " for ...");
}
STORM_PRINT(std::endl << "Model checking property \"" << property.getName() << "\": " << *property.getRawFormula() << " ..." << std::endl);
}
@ -862,7 +865,7 @@ namespace storm {
};
template<typename ValueType>
void verifyProperties(SymbolicInput const& input, 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()) {
void verifyProperties(SymbolicInput const& input, 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, std::shared_ptr<storm::logic::ShieldExpression const> const& shieldExpression)> const& verificationCallback, std::function<void(std::unique_ptr<storm::modelchecker::CheckResult> const&)> const& postprocessingCallback = PostprocessingIdentity()) {
auto transformationSettings = storm::settings::getModule<storm::settings::modules::TransformationSettings>();
auto const& properties = input.preprocessedProperties ? input.preprocessedProperties.get() : input.properties;
for (auto const& property : properties) {
@ -880,13 +883,15 @@ namespace storm {
auto propertyFormula = storm::api::checkAndTransformContinuousToDiscreteTimeFormula<ValueType>(*property.getRawFormula());
auto filterFormula = storm::api::checkAndTransformContinuousToDiscreteTimeFormula<ValueType>(*property.getFilter().getStatesFormula());
if (propertyFormula && filterFormula) {
result = verificationCallback(propertyFormula, filterFormula);
STORM_LOG_WARN_COND(!property.isShieldingProperty(), "The creation of shields for continuous time models is currently not supported.");
result = verificationCallback(propertyFormula, filterFormula, nullptr);
} else {
ignored = true;
}
} else {
result = verificationCallback(property.getRawFormula(),
property.getFilter().getStatesFormula());
property.getFilter().getStatesFormula(),
property.getShieldingExpression());
}
} catch (storm::exceptions::BaseException const& ex) {
STORM_LOG_WARN("Cannot handle property: " << ex.what());
@ -975,7 +980,7 @@ namespace storm {
storm::settings::modules::AbstractionSettings const& abstractionSettings = storm::settings::getModule<storm::settings::modules::AbstractionSettings>();
storm::api::AbstractionRefinementOptions options(parseConstraints(input.model->getManager(), abstractionSettings.getConstraintString()), parseInjectedRefinementPredicates(input.model->getManager(), abstractionSettings.getInjectedRefinementPredicates()));
verifyProperties<ValueType>(input, [&input,&options,&mpi] (std::shared_ptr<storm::logic::Formula const> const& formula, std::shared_ptr<storm::logic::Formula const> const& states) {
verifyProperties<ValueType>(input, [&input,&options,&mpi] (std::shared_ptr<storm::logic::Formula const> const& formula, std::shared_ptr<storm::logic::Formula const> const& states, std::shared_ptr<storm::logic::ShieldExpression const> const& shieldExpression) {
STORM_LOG_THROW(states->isInitialFormula(), storm::exceptions::NotSupportedException, "Abstraction-refinement can only filter initial states.");
return storm::api::verifyWithAbstractionRefinementEngine<DdType, ValueType>(mpi.env, input.model.get(), storm::api::createTask<ValueType>(formula, true), options);
});
@ -985,7 +990,7 @@ namespace storm {
void verifyWithExplorationEngine(SymbolicInput const& input, ModelProcessingInformation const& mpi) {
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, [&input,&mpi] (std::shared_ptr<storm::logic::Formula const> const& formula, std::shared_ptr<storm::logic::Formula const> const& states) {
verifyProperties<ValueType>(input, [&input,&mpi] (std::shared_ptr<storm::logic::Formula const> const& formula, std::shared_ptr<storm::logic::Formula const> const& states, std::shared_ptr<storm::logic::ShieldExpression const> const& shieldExpression) {
STORM_LOG_THROW(states->isInitialFormula(), storm::exceptions::NotSupportedException, "Exploration can only filter initial states.");
return storm::api::verifyWithExplorationEngine<ValueType>(mpi.env, input.model.get(), storm::api::createTask<ValueType>(formula, true));
});
@ -995,9 +1000,14 @@ namespace storm {
void verifyWithSparseEngine(std::shared_ptr<storm::models::ModelBase> const& model, SymbolicInput const& input, ModelProcessingInformation const& mpi) {
auto sparseModel = model->as<storm::models::sparse::Model<ValueType>>();
auto const& ioSettings = storm::settings::getModule<storm::settings::modules::IOSettings>();
auto verificationCallback = [&sparseModel,&ioSettings,&mpi] (std::shared_ptr<storm::logic::Formula const> const& formula, std::shared_ptr<storm::logic::Formula const> const& states) {
auto verificationCallback = [&sparseModel,&ioSettings,&mpi] (std::shared_ptr<storm::logic::Formula const> const& formula, std::shared_ptr<storm::logic::Formula const> const& states, std::shared_ptr<storm::logic::ShieldExpression const> const& shieldingExpression) {
bool filterForInitialStates = states->isInitialFormula();
std::cout << "verificationCallback shieldingExpression: " << *shieldingExpression << " ";
auto task = storm::api::createTask<ValueType>(formula, filterForInitialStates);
if(shieldingExpression) {
task.setShieldingExpression(shieldingExpression);
}
std::cout << "isShieldingTask ? " << task.isShieldingTask() << std::endl;
if (ioSettings.isExportSchedulerSet()) {
task.setProduceSchedulers(true);
}
@ -1060,7 +1070,7 @@ namespace storm {
template <storm::dd::DdType DdType, typename ValueType>
void verifyWithHybridEngine(std::shared_ptr<storm::models::ModelBase> const& model, SymbolicInput const& input, ModelProcessingInformation const& mpi) {
verifyProperties<ValueType>(input, [&model,&mpi] (std::shared_ptr<storm::logic::Formula const> const& formula, std::shared_ptr<storm::logic::Formula const> const& states) {
verifyProperties<ValueType>(input, [&model,&mpi] (std::shared_ptr<storm::logic::Formula const> const& formula, std::shared_ptr<storm::logic::Formula const> const& states, std::shared_ptr<storm::logic::ShieldExpression const> const& shieldExpression) {
bool filterForInitialStates = states->isInitialFormula();
auto task = storm::api::createTask<ValueType>(formula, filterForInitialStates);
@ -1082,7 +1092,7 @@ namespace storm {
template <storm::dd::DdType DdType, typename ValueType>
void verifyWithDdEngine(std::shared_ptr<storm::models::ModelBase> const& model, SymbolicInput const& input, ModelProcessingInformation const& mpi) {
verifyProperties<ValueType>(input, [&model,&mpi] (std::shared_ptr<storm::logic::Formula const> const& formula, std::shared_ptr<storm::logic::Formula const> const& states) {
verifyProperties<ValueType>(input, [&model,&mpi] (std::shared_ptr<storm::logic::Formula const> const& formula, std::shared_ptr<storm::logic::Formula const> const& states, std::shared_ptr<storm::logic::ShieldExpression const> const& shieldExpression) {
bool filterForInitialStates = states->isInitialFormula();
auto task = storm::api::createTask<ValueType>(formula, filterForInitialStates);
@ -1104,7 +1114,7 @@ namespace storm {
template <storm::dd::DdType DdType, typename ValueType>
void verifyWithAbstractionRefinementEngine(std::shared_ptr<storm::models::ModelBase> const& model, SymbolicInput const& input, ModelProcessingInformation const& mpi) {
verifyProperties<ValueType>(input, [&model,&mpi] (std::shared_ptr<storm::logic::Formula const> const& formula, std::shared_ptr<storm::logic::Formula const> const& states) {
verifyProperties<ValueType>(input, [&model,&mpi] (std::shared_ptr<storm::logic::Formula const> const& formula, std::shared_ptr<storm::logic::Formula const> const& states, std::shared_ptr<storm::logic::ShieldExpression const> const& shieldExpression) {
STORM_LOG_THROW(states->isInitialFormula(), storm::exceptions::NotSupportedException, "Abstraction-refinement can only filter initial states.");
auto symbolicModel = model->as<storm::models::symbolic::Model<DdType, ValueType>>();
return storm::api::verifyWithAbstractionRefinementEngine<DdType, ValueType>(mpi.env, symbolicModel, storm::api::createTask<ValueType>(formula, true));

Write Preview
Loading…
Cancel
Save