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; } diff --git a/src/storm/storage/jani/Model.cpp b/src/storm/storage/jani/Model.cpp index 37031bb4b..da95f426f 100644 --- a/src/storm/storage/jani/Model.cpp +++ b/src/storm/storage/jani/Model.cpp @@ -689,14 +689,10 @@ namespace storm { return false; } - storm::expressions::ExpressionManager& Model::getExpressionManager() { + storm::expressions::ExpressionManager& Model::getExpressionManager() const { return *expressionManager; } - - storm::expressions::ExpressionManager const& Model::getExpressionManager() const { - return *expressionManager; - } - + uint64_t Model::addAutomaton(Automaton const& automaton) { auto it = automatonToIndex.find(automaton.getName()); STORM_LOG_THROW(it == automatonToIndex.end(), storm::exceptions::WrongFormatException, "Automaton with name '" << automaton.getName() << "' already exists."); @@ -1156,11 +1152,11 @@ namespace storm { return false; } - uint64_t Model::encodeAutomatonAndEdgeIndices(uint64_t automatonIndex, uint64_t edgeIndex) const { + uint64_t Model::encodeAutomatonAndEdgeIndices(uint64_t automatonIndex, uint64_t edgeIndex) { return automatonIndex << 32 | edgeIndex; } - std::pair Model::decodeAutomatonAndEdgeIndices(uint64_t index) const { + std::pair Model::decodeAutomatonAndEdgeIndices(uint64_t index) { return std::make_pair(index >> 32, index & ((1ull << 32) - 1)); } diff --git a/src/storm/storage/jani/Model.h b/src/storm/storage/jani/Model.h index f45f78b29..2dc69d147 100644 --- a/src/storm/storage/jani/Model.h +++ b/src/storm/storage/jani/Model.h @@ -228,13 +228,8 @@ namespace storm { /*! * Retrieves the manager responsible for the expressions in the JANI model. */ - storm::expressions::ExpressionManager& getExpressionManager(); + storm::expressions::ExpressionManager& getExpressionManager() const; - /*! - * Retrieves the manager responsible for the expressions in the JANI model. - */ - storm::expressions::ExpressionManager const& getExpressionManager() const; - /*! * Adds the given automaton to the automata of this model. */ @@ -452,8 +447,8 @@ namespace storm { /*! * Encode and decode a tuple of automaton and edge index in one 64-bit index. */ - uint64_t encodeAutomatonAndEdgeIndices(uint64_t automatonIndex, uint64_t edgeIndex) const; - std::pair decodeAutomatonAndEdgeIndices(uint64_t index) const; + static uint64_t encodeAutomatonAndEdgeIndices(uint64_t automatonIndex, uint64_t edgeIndex); + static std::pair decodeAutomatonAndEdgeIndices(uint64_t index); /*! * Creates a new model that only contains the selected edges. The edge indices encode the automata and