From 98969e627ce5477329b6ba70e07e79f2e7660a37 Mon Sep 17 00:00:00 2001 From: Sebastian Junges Date: Sat, 30 Jun 2018 12:36:10 +0200 Subject: [PATCH] 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); } }