From 4d4b1788533f8939f27c6c07e4c10ade6c32b43c Mon Sep 17 00:00:00 2001 From: Sebastian Junges Date: Sat, 31 Mar 2018 16:32:30 +0200 Subject: [PATCH] counterexamples options: add silent and open to outside --- .../SMTMinimalLabelSetGenerator.h | 26 +++++++++++++------ 1 file changed, 18 insertions(+), 8 deletions(-) diff --git a/src/storm/counterexamples/SMTMinimalLabelSetGenerator.h b/src/storm/counterexamples/SMTMinimalLabelSetGenerator.h index 8a8edb0e6..dfd9942b8 100644 --- a/src/storm/counterexamples/SMTMinimalLabelSetGenerator.h +++ b/src/storm/counterexamples/SMTMinimalLabelSetGenerator.h @@ -1647,6 +1647,7 @@ namespace storm { bool checkThresholdFeasible; bool encodeReachability; bool useDynamicConstraints; + bool silent = false; }; /*! @@ -1848,7 +1849,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) { + 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. @@ -1914,12 +1915,17 @@ namespace storm { } auto endTime = std::chrono::high_resolution_clock::now(); - std::cout << std::endl << "Extended command for lower bounded property to size " << commandSet.size() << " in " << std::chrono::duration_cast(endTime - startTime).count() << "ms." << std::endl; + if (!silent) { + std::cout << std::endl << "Extended command for lower bounded property to size " << commandSet.size() << " in " << std::chrono::duration_cast(endTime - startTime).count() << "ms." << std::endl; + } + } - static boost::container::flat_set computeCounterexampleLabelSet(Environment const& env, storm::storage::SymbolicModelDescription const& symbolicModel, storm::models::sparse::Model const& model, std::shared_ptr const& formula) { + static boost::container::flat_set 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)) { 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."); - std::cout << std::endl << "Generating minimal label counterexample for formula " << *formula << std::endl; + if (!options.silent) { + std::cout << std::endl << "Generating minimal label counterexample for formula " << *formula << std::endl; + } STORM_LOG_THROW(formula->isProbabilityOperatorFormula(), storm::exceptions::InvalidPropertyException, "Counterexample generation does not support this kind of formula. Expecting a probability operator as the outermost formula element."); storm::logic::ProbabilityOperatorFormula const& probabilityOperator = formula->asProbabilityOperatorFormula(); @@ -1967,7 +1973,9 @@ namespace storm { // This means that from all states in prob0E(psi) we need to include labels such that \sigma_0 // is actually included in the resulting model. This prevents us from guaranteeing the minimality of // the returned counterexample, so we warn about that. - STORM_LOG_WARN("Generating counterexample for lower-bounded property. The resulting command set need not be minimal."); + if (!options.silent) { + STORM_LOG_WARN("Generating counterexample for lower-bounded property. The resulting command set need not be minimal."); + } // Modify bound appropriately. comparisonType = storm::logic::invertPreserveStrictness(comparisonType); @@ -1985,13 +1993,15 @@ namespace storm { // Delegate the actual computation work to the function of equal name. auto startTime = std::chrono::high_resolution_clock::now(); - auto labelSet = getMinimalLabelSet(env, symbolicModel, model, phiStates, psiStates, threshold, strictBound, boost::container::flat_set(), true); + auto labelSet = getMinimalLabelSet(env, symbolicModel, model, phiStates, psiStates, threshold, strictBound, dontCareLabels, options); auto endTime = std::chrono::high_resolution_clock::now(); - std::cout << std::endl << "Computed minimal label set of size " << labelSet.size() << " in " << std::chrono::duration_cast(endTime - startTime).count() << "ms." << std::endl; + if (!options.silent) { + std::cout << std::endl << "Computed minimal label set of size " << labelSet.size() << " in " << std::chrono::duration_cast(endTime - startTime).count() << "ms." << std::endl; + } // Extend the command set properly. if (lowerBoundedFormula) { - extendLabelSetLowerBound(model, labelSet, phiStates, psiStates); + extendLabelSetLowerBound(model, labelSet, phiStates, psiStates, options.silent); } return labelSet; }