Browse Source

Integrated symbolic verification of parametric systems into storm-pars

tempestpy_adaptions
Matthias Volk 6 years ago
parent
commit
a1c5aa946c
  1. 53
      src/storm-pars-cli/storm-pars.cpp

53
src/storm-pars-cli/storm-pars.cpp

@ -154,12 +154,14 @@ namespace storm {
template <storm::dd::DdType DdType, typename ValueType>
std::pair<std::shared_ptr<storm::models::ModelBase>, bool> preprocessDdModel(std::shared_ptr<storm::models::symbolic::Model<DdType, ValueType>> const& model, SymbolicInput const& input) {
auto coreSettings = storm::settings::getModule<storm::settings::modules::CoreSettings>();
auto generalSettings = storm::settings::getModule<storm::settings::modules::GeneralSettings>();
auto bisimulationSettings = storm::settings::getModule<storm::settings::modules::BisimulationSettings>();
std::pair<std::shared_ptr<storm::models::ModelBase>, bool> result = std::make_pair(model, false);
auto coreSettings = storm::settings::getModule<storm::settings::modules::CoreSettings>();
if (coreSettings.getEngine() == storm::settings::modules::CoreSettings::Engine::Hybrid) {
// Currently, hybrid engine for parametric models just referrs to building the model symbolically.
// Currently, hybrid engine for parametric models just refers to building the model symbolically.
STORM_LOG_INFO("Translating symbolic model to sparse model...");
result.first = storm::api::transformSymbolicToSparseModel(model);
result.second = true;
@ -168,6 +170,13 @@ namespace storm {
if (sparsePreprocessingResult.second) {
result.first = sparsePreprocessingResult.first;
}
} else {
STORM_LOG_ASSERT(coreSettings.getEngine() == storm::settings::modules::CoreSettings::Engine::Dd, "Expected Dd engine.");
if (generalSettings.isBisimulationSet()) {
STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "Bisimulation is not supported for symbolic parametric models.");
//result.first = storm::cli::preprocessDdModelBisimulation(result.first->template as<storm::models::symbolic::Model<DdType, ValueType>>(), input, bisimulationSettings);
//result.second = true;
}
}
return result;
}
@ -462,10 +471,46 @@ namespace storm {
}
}
template <storm::dd::DdType DdType, typename ValueType>
void verifyPropertiesWithSymbolicEngine(std::shared_ptr<storm::models::symbolic::Model<DdType, ValueType>> const& model, SymbolicInput const& input, SampleInformation<ValueType> const& samples) {
if (samples.empty()) {
verifyProperties<ValueType>(input.properties,
[&model] (std::shared_ptr<storm::logic::Formula const> const& formula) {
std::unique_ptr<storm::modelchecker::CheckResult> result = storm::api::verifyWithDdEngine<DdType, ValueType>(model, storm::api::createTask<ValueType>(formula, true));
if (result) {
result->filter(storm::modelchecker::SymbolicQualitativeCheckResult<DdType>(model->getReachableStates(), model->getInitialStates()));
}
return result;
},
[&model] (std::unique_ptr<storm::modelchecker::CheckResult> const& result) {
auto parametricSettings = storm::settings::getModule<storm::settings::modules::ParametricSettings>();
if (parametricSettings.exportResultToFile() && model->isOfType(storm::models::ModelType::Dtmc)) {
//auto dtmc = model->template as<storm::models::symbolic::Dtmc<DdType, ValueType>>();
//boost::optional<ValueType> rationalFunction = result->asSymbolicQuantitativeCheckResult<DdType, ValueType>().sum();
//storm::api::exportParametricResultToFile(rationalFunction, storm::analysis::ConstraintCollector<ValueType>(*dtmc), parametricSettings.exportResultPath());
}
});
} else {
STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "Sampling is not supported in the symbolic engine.");
}
}
template <storm::dd::DdType DdType, typename ValueType>
void verifyWithDdEngine(std::shared_ptr<storm::models::symbolic::Model<DdType, ValueType>> const& model, SymbolicInput const& input, std::vector<storm::storage::ParameterRegion<ValueType>> const& regions, SampleInformation<ValueType> const& samples) {
if (regions.empty()) {
storm::pars::verifyPropertiesWithSymbolicEngine(model, input, samples);
} else {
STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "Region verification is not supported in the symbolic engine.");
}
}
template <storm::dd::DdType DdType, typename ValueType>
void verifyParametricModel(std::shared_ptr<storm::models::ModelBase> const& model, SymbolicInput const& input, std::vector<storm::storage::ParameterRegion<ValueType>> const& regions, SampleInformation<ValueType> const& samples) {
STORM_LOG_ASSERT(model->isSparseModel(), "Unexpected model type.");
storm::pars::verifyWithSparseEngine<ValueType>(model->as<storm::models::sparse::Model<ValueType>>(), input, regions, samples);
if (model->isSparseModel()) {
storm::pars::verifyWithSparseEngine<ValueType>(model->as<storm::models::sparse::Model<ValueType>>(), input, regions, samples);
} else {
storm::pars::verifyWithDdEngine<DdType, ValueType>(model->as<storm::models::symbolic::Model<DdType, ValueType>>(), input, regions, samples);
}
}
template <storm::dd::DdType DdType, typename ValueType>

Loading…
Cancel
Save