diff --git a/src/storm-cli-utilities/model-handling.h b/src/storm-cli-utilities/model-handling.h index 3f9967a3a..3d3dceae9 100644 --- a/src/storm-cli-utilities/model-handling.h +++ b/src/storm-cli-utilities/model-handling.h @@ -426,7 +426,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 4de23e767..4a829b9cb 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 @@ -338,7 +319,7 @@ namespace storm { // * identify labels that can directly precede a given action // * identify labels that directly reach a target state // * identify labels that can directly follow a given action - + boost::container::flat_set initialLabels; std::set> initialCombinations; boost::container::flat_set targetLabels; @@ -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. @@ -1387,7 +1353,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 +1457,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) { @@ -1510,7 +1482,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); @@ -1550,13 +1522,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)); @@ -1605,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. @@ -1618,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. @@ -1742,7 +1727,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; @@ -1809,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; @@ -1839,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. @@ -1923,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; @@ -1952,7 +1944,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(); @@ -2014,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) { @@ -2036,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"