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

Integrated non-Markovian state elimination into Storm MA modelchecking

tempestpy_adaptions
Alexander Bork 6 years ago
parent
7b038db6d5
commit
450e074c5b
4 changed files with 62 additions and 5 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. 26
      src/storm-cli-utilities/model-handling.h
  2. 1
      src/storm-dft/modelchecker/dft/DFTModelChecker.cpp
  3. 14
      src/storm-pars-cli/storm-pars.cpp
  4. 26
      src/storm/api/transformation.h

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

@ -42,6 +42,7 @@
#include "storm/settings/modules/AbstractionSettings.h"
#include "storm/settings/modules/ResourceSettings.h"
#include "storm/settings/modules/ModelCheckerSettings.h"
#include "storm/settings/modules/TransformationSettings.h"
#include "storm/storage/Qvbs.h"
#include "storm/utility/Stopwatch.h"
@ -350,11 +351,18 @@ namespace storm {
auto generalSettings = storm::settings::getModule<storm::settings::modules::GeneralSettings>();
auto bisimulationSettings = storm::settings::getModule<storm::settings::modules::BisimulationSettings>();
auto ioSettings = storm::settings::getModule<storm::settings::modules::IOSettings>();
auto transformationSettings = storm::settings::getModule<storm::settings::modules::TransformationSettings>();
std::pair<std::shared_ptr<storm::models::sparse::Model<ValueType>>, bool> result = std::make_pair(model, false);
if (result.first->isOfType(storm::models::ModelType::MarkovAutomaton)) {
result.first = preprocessSparseMarkovAutomaton(result.first->template as<storm::models::sparse::MarkovAutomaton<ValueType>>());
if (transformationSettings.isChainEliminationSet() &&
result.first->isOfType(storm::models::ModelType::MarkovAutomaton)) {
result.first = storm::transformer::NonMarkovianChainTransformer<ValueType>::eliminateNonmarkovianStates(
result.first->template as<storm::models::sparse::MarkovAutomaton<ValueType>>(),
!transformationSettings.isIgnoreLabelingSet());
}
result.second = true;
}
@ -629,19 +637,31 @@ 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()) {
auto transformationSettings = storm::settings::getModule<storm::settings::modules::TransformationSettings>();
auto const& properties = input.preprocessedProperties ? input.preprocessedProperties.get() : input.properties;
for (auto const& property : properties) {
printModelCheckingProperty(property);
bool ignored = false;
storm::utility::Stopwatch watch(true);
std::unique_ptr<storm::modelchecker::CheckResult> result;
try {
result = verificationCallback(property.getRawFormula(), property.getFilter().getStatesFormula());
auto rawFormula = property.getRawFormula();
if (transformationSettings.isChainEliminationSet() &&
!storm::transformer::NonMarkovianChainTransformer<ValueType>::preservesFormula(*rawFormula)) {
STORM_LOG_WARN("Property is not preserved by elimination of non-markovian states.");
ignored = true;
} else {
result = verificationCallback(property.getRawFormula(),
property.getFilter().getStatesFormula());
}
} catch (storm::exceptions::BaseException const& ex) {
STORM_LOG_WARN("Cannot handle property: " << ex.what());
}
watch.stop();
postprocessingCallback(result);
printResult<ValueType>(result, property, &watch);
if (!ignored) {
postprocessingCallback(result);
printResult<ValueType>(result, property, &watch);
}
}
}

1
src/storm-dft/modelchecker/dft/DFTModelChecker.cpp
View File

@ -8,7 +8,6 @@
#include "storm/modelchecker/results/ExplicitQuantitativeCheckResult.h"
#include "storm/modelchecker/results/ExplicitQualitativeCheckResult.h"
#include "storm/models/ModelType.h"
#include "storm/transformer/NonMarkovianChainTransformer.h"
#include "storm-dft/builder/ExplicitDFTModelBuilder.h"
#include "storm-dft/storage/dft/DFTIsomorphism.h"

14
src/storm-pars-cli/storm-pars.cpp
View File

@ -21,6 +21,7 @@
#include "storm/settings/modules/CoreSettings.h"
#include "storm/settings/modules/IOSettings.h"
#include "storm/settings/modules/BisimulationSettings.h"
#include "storm/settings/modules/TransformationSettings.h"
#include "storm/exceptions/BaseException.h"
#include "storm/exceptions/InvalidSettingsException.h"
@ -141,6 +142,7 @@ namespace storm {
auto generalSettings = storm::settings::getModule<storm::settings::modules::GeneralSettings>();
auto bisimulationSettings = storm::settings::getModule<storm::settings::modules::BisimulationSettings>();
auto parametricSettings = storm::settings::getModule<storm::settings::modules::ParametricSettings>();
auto transformationSettings = storm::settings::getModule<storm::settings::modules::TransformationSettings>();
PreprocessResult result(model, false);
@ -153,6 +155,18 @@ namespace storm {
result.model = storm::cli::preprocessSparseModelBisimulation(result.model->template as<storm::models::sparse::Model<ValueType>>(), input, bisimulationSettings);
result.changed = true;
}
if (transformationSettings.isChainEliminationSet() &&
model->isOfType(storm::models::ModelType::MarkovAutomaton)) {
auto eliminationResult = storm::api::eliminateNonMarkovianChains(
result.model->template as<storm::models::sparse::MarkovAutomaton<ValueType>>(),
storm::api::extractFormulasFromProperties(input.properties),
transformationSettings.isIgnoreLabelingSet());
result.model = eliminationResult.first;
// Set transformed properties as new properties in input
result.formulas = eliminationResult.second;
result.changed = true;
}
if (parametricSettings.transformContinuousModel() && (model->isOfType(storm::models::ModelType::Ctmc) || model->isOfType(storm::models::ModelType::MarkovAutomaton))) {
auto transformResult = storm::api::transformContinuousToDiscreteTimeSparseModel(std::move(*model->template as<storm::models::sparse::Model<ValueType>>()), storm::api::extractFormulasFromProperties(input.properties));

26
src/storm/api/transformation.h
View File

@ -2,6 +2,7 @@
#include "storm/transformer/ContinuousToDiscreteTimeModelTransformer.h"
#include "storm/transformer/SymbolicToSparseTransformer.h"
#include "storm/transformer/NonMarkovianChainTransformer.h"
#include "storm/utility/macros.h"
#include "storm/utility/builder.h"
@ -10,7 +11,30 @@
namespace storm {
namespace api {
/*!
* Eliminates chains of non-Markovian states from a given Markov Automaton
*/
template<typename ValueType>
std::pair<std::shared_ptr<storm::models::sparse::Model<ValueType>>, std::vector<std::shared_ptr<storm::logic::Formula const>>>
eliminateNonMarkovianChains(std::shared_ptr<storm::models::sparse::MarkovAutomaton<ValueType>> const &ma,
std::vector<std::shared_ptr<storm::logic::Formula const>> const &formulas,
bool ignoreLabeling) {
auto newFormulas = storm::transformer::NonMarkovianChainTransformer<ValueType>::checkAndTransformFormulas(
formulas);
STORM_LOG_WARN_COND(newFormulas.size() == formulas.size(),
"The state elimination does not preserve all properties.");
STORM_LOG_WARN_COND(!ignoreLabeling,
"Labels are ignored for the state elimination. This may cause incorrect results.");
return std::make_pair(
storm::transformer::NonMarkovianChainTransformer<ValueType>::eliminateNonmarkovianStates(ma,
!ignoreLabeling),
newFormulas);
}
/*!
* Transforms the given continuous model to a discrete time model.
* If such a transformation does not preserve one of the given formulas, a warning is issued.

Write Preview
Loading…
Cancel
Save