From 84783520304a97e7bacabdea5af89c753dfac559 Mon Sep 17 00:00:00 2001 From: sjunges Date: Sun, 10 Jun 2018 23:00:12 +0200 Subject: [PATCH 1/5] dynamic constraints and minimality labels --- .../counterexamples/SMTMinimalLabelSetGenerator.h | 10 ++++++++-- 1 file changed, 8 insertions(+), 2 deletions(-) diff --git a/src/storm-counterexamples/counterexamples/SMTMinimalLabelSetGenerator.h b/src/storm-counterexamples/counterexamples/SMTMinimalLabelSetGenerator.h index 4de23e767..a3dfbd066 100644 --- a/src/storm-counterexamples/counterexamples/SMTMinimalLabelSetGenerator.h +++ b/src/storm-counterexamples/counterexamples/SMTMinimalLabelSetGenerator.h @@ -1387,7 +1387,10 @@ namespace storm { std::vector formulae; boost::container::flat_set unknownReachableLabels; std::set_difference(reachableLabels.begin(), reachableLabels.end(), relevancyInformation.knownLabels.begin(), relevancyInformation.knownLabels.end(), std::inserter(unknownReachableLabels, unknownReachableLabels.end())); - for (auto label : unknownReachableLabels) { + boost::container::flat_set unknownReachableMinimalityLabels; + std::set_intersection(unknownReachableLabels.begin(), unknownReachableLabels.end(), relevancyInformation.minimalityLabels.begin(), relevancyInformation.minimalityLabels.end(), std::inserter(unknownReachableMinimalityLabels, unknownReachableMinimalityLabels.end())); + + for (auto label : unknownReachableMinimalityLabels) { formulae.push_back(!variableInformation.labelVariables.at(variableInformation.labelToIndexMap.at(label))); } for (auto const& cutLabelSet : cutLabels) { @@ -1488,7 +1491,10 @@ namespace storm { std::vector formulae; boost::container::flat_set unknownReachableLabels; std::set_difference(reachableLabels.begin(), reachableLabels.end(), relevancyInformation.knownLabels.begin(), relevancyInformation.knownLabels.end(), std::inserter(unknownReachableLabels, unknownReachableLabels.end())); - for (auto label : unknownReachableLabels) { + boost::container::flat_set unknownReachableMinimalityLabels; + std::set_intersection(unknownReachableLabels.begin(), unknownReachableLabels.end(), relevancyInformation.minimalityLabels.begin(), relevancyInformation.minimalityLabels.end(), std::inserter(unknownReachableMinimalityLabels, unknownReachableMinimalityLabels.end())); + + for (auto label : unknownReachableMinimalityLabels) { formulae.push_back(!variableInformation.labelVariables.at(variableInformation.labelToIndexMap.at(label))); } for (auto const& cutLabelSet : cutLabels) { From 0be012609552e11ba920107c00b51556b96e45a4 Mon Sep 17 00:00:00 2001 From: Sebastian Junges Date: Sun, 24 Jun 2018 15:07:23 +0200 Subject: [PATCH 2/5] fixed support for highlevel counterex for expected rewards in dtmcs --- src/storm-cli-utilities/model-handling.h | 5 ++++- .../SMTMinimalLabelSetGenerator.h | 19 +++++++++++++------ 2 files changed, 17 insertions(+), 7 deletions(-) diff --git a/src/storm-cli-utilities/model-handling.h b/src/storm-cli-utilities/model-handling.h index 41faf8732..41df3fabf 100644 --- a/src/storm-cli-utilities/model-handling.h +++ b/src/storm-cli-utilities/model-handling.h @@ -422,7 +422,10 @@ namespace storm { STORM_LOG_THROW(model->isSparseModel(), storm::exceptions::NotSupportedException, "Counterexample generation is currently only supported for sparse models."); auto sparseModel = model->as>(); - + for (auto& rewModel : sparseModel->getRewardModels()) { + rewModel.second.reduceToStateBasedRewards(sparseModel->getTransitionMatrix(), true); + } + STORM_LOG_THROW(sparseModel->isOfType(storm::models::ModelType::Dtmc) || sparseModel->isOfType(storm::models::ModelType::Mdp), storm::exceptions::NotSupportedException, "Counterexample is currently only supported for discrete-time models."); auto counterexampleSettings = storm::settings::getModule(); diff --git a/src/storm-counterexamples/counterexamples/SMTMinimalLabelSetGenerator.h b/src/storm-counterexamples/counterexamples/SMTMinimalLabelSetGenerator.h index a3dfbd066..52a24d0dd 100644 --- a/src/storm-counterexamples/counterexamples/SMTMinimalLabelSetGenerator.h +++ b/src/storm-counterexamples/counterexamples/SMTMinimalLabelSetGenerator.h @@ -1516,7 +1516,7 @@ namespace storm { * Returns the sub-model obtained from removing all choices that do not originate from the specified filterLabelSet. * Also returns the Labelsets of the sub-model. */ - static std::pair>, std::vector>> restrictModelToLabelSet(storm::models::sparse::Model const& model, boost::container::flat_set const& filterLabelSet, boost::optional absorbState = boost::none) { + static std::pair>, std::vector>> restrictModelToLabelSet(storm::models::sparse::Model const& model, boost::container::flat_set const& filterLabelSet, boost::optional const& rewardName = boost::none, boost::optional absorbState = boost::none) { bool customRowGrouping = model.isOfType(storm::models::ModelType::Mdp); @@ -1556,13 +1556,19 @@ namespace storm { resultLabelSet.emplace_back(); ++currentRow; } + } - + + if (rewardName) { + auto const &origRewModel = model.getRewardModel(rewardName.get()); + assert(origRewModel.hasOnlyStateRewards()); + } + std::shared_ptr> resultModel; if (model.isOfType(storm::models::ModelType::Dtmc)) { - resultModel = std::make_shared>(transitionMatrixBuilder.build(), storm::models::sparse::StateLabeling(model.getStateLabeling())); + resultModel = std::make_shared>(transitionMatrixBuilder.build(), storm::models::sparse::StateLabeling(model.getStateLabeling()), model.getRewardModels()); } else { - resultModel = std::make_shared>(transitionMatrixBuilder.build(), storm::models::sparse::StateLabeling(model.getStateLabeling())); + resultModel = std::make_shared>(transitionMatrixBuilder.build(), storm::models::sparse::StateLabeling(model.getStateLabeling()), model.getRewardModels()); } return std::make_pair(resultModel, std::move(resultLabelSet)); @@ -1748,7 +1754,7 @@ namespace storm { } - auto subChoiceOrigins = restrictModelToLabelSet(model, commandSet, psiStates.getNextSetIndex(0)); + auto subChoiceOrigins = restrictModelToLabelSet(model, commandSet, rewardName, psiStates.getNextSetIndex(0)); std::shared_ptr> const& subModel = subChoiceOrigins.first; std::vector> const& subLabelSets = subChoiceOrigins.second; @@ -1958,7 +1964,8 @@ namespace storm { rewardName = rewardOperator.getRewardModelName(); STORM_LOG_THROW(!storm::logic::isLowerBound(comparisonType), storm::exceptions::NotSupportedException, "Lower bounds in counterexamples are only supported for probability formulas."); - + STORM_LOG_THROW(model.hasRewardModel(rewardName.get()), storm::exceptions::InvalidPropertyException, "Property refers to reward " << rewardName.get() << " but model does not contain such a reward model."); + STORM_LOG_THROW(model.getRewardModel(rewardName.get()).hasOnlyStateRewards(), storm::exceptions::NotSupportedException, "We only support state-based rewards at the moment."); } bool strictBound = comparisonType == storm::logic::ComparisonType::Less; storm::logic::Formula const& subformula = formula->asOperatorFormula().getSubformula(); From 98969e627ce5477329b6ba70e07e79f2e7660a37 Mon Sep 17 00:00:00 2001 From: Sebastian Junges Date: Sat, 30 Jun 2018 12:36:10 +0200 Subject: [PATCH 3/5] updated counterexamples to support statistics to be exported --- .../SMTMinimalLabelSetGenerator.h | 63 +++++++------------ .../CounterexampleGeneratorSettings.cpp | 2 +- src/storm/api/export.cpp | 11 +++- 3 files changed, 31 insertions(+), 45 deletions(-) diff --git a/src/storm-counterexamples/counterexamples/SMTMinimalLabelSetGenerator.h b/src/storm-counterexamples/counterexamples/SMTMinimalLabelSetGenerator.h index 52a24d0dd..8a43e6cc5 100644 --- a/src/storm-counterexamples/counterexamples/SMTMinimalLabelSetGenerator.h +++ b/src/storm-counterexamples/counterexamples/SMTMinimalLabelSetGenerator.h @@ -59,10 +59,6 @@ namespace storm { std::map> relevantChoicesForRelevantStates; }; - struct GeneratorStats { - - }; - struct VariableInformation { // The manager responsible for the constraints we are building. std::shared_ptr manager; @@ -271,21 +267,6 @@ namespace storm { return variableInformation; } - /*! - * Asserts the constraints that are initially needed for the Fu-Malik procedure. - * - * @param solver The solver in which to assert the constraints. - * @param variableInformation A structure with information about the variables for the labels. - */ - static void assertFuMalikInitialConstraints(z3::solver& solver, VariableInformation const& variableInformation) { - // Assert that at least one of the labels must be taken. - z3::expr formula = variableInformation.labelVariables.at(0); - for (uint_fast64_t index = 1; index < variableInformation.labelVariables.size(); ++index) { - formula = formula || variableInformation.labelVariables.at(index); - } - solver.add(formula); - } - static storm::expressions::Expression getOtherSynchronizationEnabledFormula(boost::container::flat_set const& labelSet, std::map>> const& synchronizingLabels, boost::container::flat_map, storm::expressions::Expression> const& labelSetToFormula, VariableInformation const& variableInformation, RelevancyInformation const& relevancyInformation) { // Taking all commands of a combination does not necessarily mean that a following label set needs to be taken. // This is because it could be that the commands are taken to enable other synchronizations. Therefore, we need @@ -970,22 +951,7 @@ namespace storm { } solver.add(disjunction); } - - /*! - * Asserts that the conjunction of the given formulae holds. If the content of the conjunction is empty, - * this corresponds to asserting true. - * - * @param context The Z3 context in which to build the expressions. - * @param solver The solver to use for the satisfiability evaluation. - * @param formulaVector A vector of expressions that shall form the conjunction. - */ - static void assertConjunction(z3::context& context, z3::solver& solver, std::vector const& formulaVector) { - z3::expr conjunction = context.bool_val(true); - for (auto expr : formulaVector) { - conjunction = conjunction && expr; - } - solver.add(conjunction); - } + /*! * Creates a full-adder for the two inputs and returns the resulting bit as well as the carry bit. @@ -1617,6 +1583,13 @@ namespace storm { uint64_t maximumCounterexamples = 1; uint64_t multipleCounterexampleSizeCap = 100000000; }; + + struct GeneratorStats { + std::chrono::milliseconds setupTime; + std::chrono::milliseconds solverTime; + std::chrono::milliseconds modelCheckingTime; + std::chrono::milliseconds analysisTime; + }; /*! * Computes the minimal command set that is needed in the given model to exceed the given probability threshold for satisfying phi until psi. @@ -1630,7 +1603,7 @@ namespace storm { * @param strictBound Indicates whether the threshold needs to be achieved (true) or exceeded (false). * @param options A set of options for customization. */ - static std::vector> getMinimalLabelSet(Environment const& env, storm::storage::SymbolicModelDescription const& symbolicModel, storm::models::sparse::Model const& model, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, double propertyThreshold, boost::optional const& rewardName, bool strictBound, boost::container::flat_set const& dontCareLabels = boost::container::flat_set(), Options const& options = Options()) { + static std::vector> getMinimalLabelSet(Environment const& env, GeneratorStats& stats, storm::storage::SymbolicModelDescription const& symbolicModel, storm::models::sparse::Model const& model, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, double propertyThreshold, boost::optional const& rewardName, bool strictBound, boost::container::flat_set const& dontCareLabels = boost::container::flat_set(), Options const& options = Options()) { #ifdef STORM_HAVE_Z3 std::vector> result; // Set up all clocks used for time measurement. @@ -1821,12 +1794,19 @@ namespace storm { // Compute and emit the time measurements if the corresponding flag was set. totalTime = std::chrono::high_resolution_clock::now() - totalClock; + + stats.analysisTime = std::chrono::duration_cast(totalAnalysisTime); + stats.setupTime = std::chrono::duration_cast(totalSetupTime); + stats.modelCheckingTime = std::chrono::duration_cast(totalModelCheckingTime); + stats.solverTime = std::chrono::duration_cast(totalSolverTime); + if (storm::settings::getModule().isShowStatisticsSet()) { boost::container::flat_set allLabels; for (auto const& e : labelSets) { allLabels.insert(e.begin(), e.end()); } - + + std::cout << "Metrics:" << std::endl; std::cout << " * all labels: " << allLabels.size() << std::endl; std::cout << " * known labels: " << relevancyInformation.knownLabels.size() << std::endl; @@ -1851,7 +1831,7 @@ namespace storm { #endif } - static void extendLabelSetLowerBound(storm::models::sparse::Model const& model, boost::container::flat_set& commandSet, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, bool silent = false) { + static void extendLabelSetLowerBound(storm::models::sparse::Model const& model, boost::container::flat_set& commandSet, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, bool silent = false) { auto startTime = std::chrono::high_resolution_clock::now(); // Create sub-model that only contains the choices allowed by the given command set. @@ -1935,7 +1915,7 @@ namespace storm { } - static std::vector> computeCounterexampleLabelSet(Environment const& env, storm::storage::SymbolicModelDescription const& symbolicModel, storm::models::sparse::Model const& model, std::shared_ptr const& formula, boost::container::flat_set const& dontCareLabels = boost::container::flat_set(), Options const& options = Options(true)) { + static std::vector> computeCounterexampleLabelSet(Environment const& env, GeneratorStats& stats, storm::storage::SymbolicModelDescription const& symbolicModel, storm::models::sparse::Model const& model, std::shared_ptr const& formula, boost::container::flat_set const& dontCareLabels = boost::container::flat_set(), Options const& options = Options(true)) { STORM_LOG_THROW(model.isOfType(storm::models::ModelType::Dtmc) || model.isOfType(storm::models::ModelType::Mdp), storm::exceptions::NotSupportedException, "MaxSAT-based counterexample generation is supported only for discrete-time models."); if (!options.silent) { std::cout << std::endl << "Generating minimal label counterexample for formula " << *formula << std::endl; @@ -2027,7 +2007,7 @@ namespace storm { // Delegate the actual computation work to the function of equal name. auto startTime = std::chrono::high_resolution_clock::now(); - auto labelSets = getMinimalLabelSet(env, symbolicModel, model, phiStates, psiStates, threshold, rewardName, strictBound, dontCareLabels, options); + auto labelSets = getMinimalLabelSet(env, stats, symbolicModel, model, phiStates, psiStates, threshold, rewardName, strictBound, dontCareLabels, options); auto endTime = std::chrono::high_resolution_clock::now(); if (!options.silent) { for (auto const& labelSet : labelSets) { @@ -2049,7 +2029,8 @@ namespace storm { static std::shared_ptr computeCounterexample(Environment const& env, storm::storage::SymbolicModelDescription const& symbolicModel, storm::models::sparse::Model const& model, std::shared_ptr const& formula) { #ifdef STORM_HAVE_Z3 - auto labelSets = computeCounterexampleLabelSet(env, symbolicModel, model, formula); + GeneratorStats stats; + auto labelSets = computeCounterexampleLabelSet(env, stats, symbolicModel, model, formula); if (symbolicModel.isPrismProgram()) { diff --git a/src/storm-counterexamples/settings/modules/CounterexampleGeneratorSettings.cpp b/src/storm-counterexamples/settings/modules/CounterexampleGeneratorSettings.cpp index 9fe9d3d36..5b2142ee3 100644 --- a/src/storm-counterexamples/settings/modules/CounterexampleGeneratorSettings.cpp +++ b/src/storm-counterexamples/settings/modules/CounterexampleGeneratorSettings.cpp @@ -1,4 +1,4 @@ -#include "CounterexampleGeneratorSettings.h" +#include "storm-counterexamples/settings/modules/CounterexampleGeneratorSettings.h" #include "storm/settings/SettingsManager.h" #include "storm/exceptions/InvalidSettingsException.h" diff --git a/src/storm/api/export.cpp b/src/storm/api/export.cpp index 193ec0668..e1acf9b8d 100644 --- a/src/storm/api/export.cpp +++ b/src/storm/api/export.cpp @@ -5,13 +5,18 @@ namespace storm { void exportJaniModel(storm::jani::Model const& model, std::vector const& properties, std::string const& filename) { auto janiSettings = storm::settings::getModule(); - + + storm::jani::Model modelForExport = model; + if (janiSettings.isExportFlattenedSet()) { + modelForExport = modelForExport.flattenComposition(); + } + if (janiSettings.isExportAsStandardJaniSet()) { - storm::jani::Model normalisedModel = model; + storm::jani::Model normalisedModel = modelForExport; normalisedModel.makeStandardJaniCompliant(); storm::jani::JsonExporter::toFile(normalisedModel, properties, filename); } else { - storm::jani::JsonExporter::toFile(model, properties, filename); + storm::jani::JsonExporter::toFile(modelForExport, properties, filename); } } From f2a7621e0abceaa7166a18e9db984e7d097abf21 Mon Sep 17 00:00:00 2001 From: Sebastian Junges Date: Wed, 11 Jul 2018 15:52:48 +0200 Subject: [PATCH 4/5] updated changelog --- CHANGELOG.md | 5 ++++- 1 file changed, 4 insertions(+), 1 deletion(-) diff --git a/CHANGELOG.md b/CHANGELOG.md index 150d5ef1b..bda25081d 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -13,7 +13,10 @@ Version 1.2.x - Sound value iteration (SVI) for DTMCs and MDPs - Topological solver for linear equation systems and MinMax equation systems. - Added support for expected total rewards in the sparse engine - +- `storm-parsers` extracted to reduce linking time +- `storm-counterexamples` extracted to reduce linking time +- Improved export for jani models +- Several extensions to high-level counterexamples ### Version 1.2.1 (2018/02) - Multi-dimensional reward bounded reachability properties for DTMCs. From 54c0bbb7c349c8f9558ad68230c8147081eae1c8 Mon Sep 17 00:00:00 2001 From: Sebastian Junges Date: Wed, 11 Jul 2018 19:50:03 +0200 Subject: [PATCH 5/5] flatten of jani models before export via appropriate setting --- src/storm/api/export.cpp | 4 ++++ 1 file changed, 4 insertions(+) diff --git a/src/storm/api/export.cpp b/src/storm/api/export.cpp index 78951fd27..1a69a34da 100644 --- a/src/storm/api/export.cpp +++ b/src/storm/api/export.cpp @@ -16,6 +16,10 @@ namespace storm { } } + if (janiSettings.isExportFlattenedSet()) { + exportModel = exportModel.flattenComposition(); + } + if (janiSettings.isExportAsStandardJaniSet()) { storm::jani::Model normalisedModel = exportModel; normalisedModel.makeStandardJaniCompliant();