counterexamples record their timings to a structure, and support for rewards fixed

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<storm::models::sparse::Model<ValueType>>();
-            
+            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<storm::settings::modules::CounterexampleGeneratorSettings>();

src/storm-counterexamples/counterexamples/SMTMinimalLabelSetGenerator.h

@@ -59,10 +59,6 @@ namespace storm {
                 std::map<uint_fast64_t, std::list<uint_fast64_t>> relevantChoicesForRelevantStates;
             };
 
-            struct GeneratorStats {
-
-            };
-
             struct VariableInformation {
                 // The manager responsible for the constraints we are building.
                 std::shared_ptr<storm::expressions::ExpressionManager> 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<uint_fast64_t> const& labelSet, std::map<uint_fast64_t, std::set<boost::container::flat_set<uint_fast64_t>>> const& synchronizingLabels, boost::container::flat_map<boost::container::flat_set<uint_fast64_t>, 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<uint_fast64_t> initialLabels;
                 std::set<boost::container::flat_set<uint_fast64_t>> initialCombinations;
                 boost::container::flat_set<uint_fast64_t> 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<z3::expr> 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<storm::expressions::Expression> formulae;
                 boost::container::flat_set<uint_fast64_t> 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<uint64_t> 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<storm::expressions::Expression> formulae;
                 boost::container::flat_set<uint_fast64_t> 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<uint64_t> 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::shared_ptr<storm::models::sparse::Model<T>>, std::vector<boost::container::flat_set<uint_fast64_t>>> restrictModelToLabelSet(storm::models::sparse::Model<T> const& model,  boost::container::flat_set<uint_fast64_t> const& filterLabelSet, boost::optional<uint64_t> absorbState = boost::none) {
+            static std::pair<std::shared_ptr<storm::models::sparse::Model<T>>, std::vector<boost::container::flat_set<uint_fast64_t>>> restrictModelToLabelSet(storm::models::sparse::Model<T> const& model,  boost::container::flat_set<uint_fast64_t> const& filterLabelSet, boost::optional<std::string> const& rewardName = boost::none, boost::optional<uint64_t> 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<storm::models::sparse::Model<T>> resultModel;
                 if (model.isOfType(storm::models::ModelType::Dtmc)) {
-                    resultModel = std::make_shared<storm::models::sparse::Dtmc<T>>(transitionMatrixBuilder.build(), storm::models::sparse::StateLabeling(model.getStateLabeling()));
+                    resultModel = std::make_shared<storm::models::sparse::Dtmc<T>>(transitionMatrixBuilder.build(), storm::models::sparse::StateLabeling(model.getStateLabeling()), model.getRewardModels());
                 } else {
-                    resultModel = std::make_shared<storm::models::sparse::Mdp<T>>(transitionMatrixBuilder.build(), storm::models::sparse::StateLabeling(model.getStateLabeling()));
+                    resultModel = std::make_shared<storm::models::sparse::Mdp<T>>(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<boost::container::flat_set<uint_fast64_t>> getMinimalLabelSet(Environment const& env, storm::storage::SymbolicModelDescription const& symbolicModel, storm::models::sparse::Model<T> const& model, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, double propertyThreshold, boost::optional<std::string> const& rewardName, bool strictBound, boost::container::flat_set<uint_fast64_t> const& dontCareLabels = boost::container::flat_set<uint_fast64_t>(), Options const& options = Options()) {
+            static std::vector<boost::container::flat_set<uint_fast64_t>> getMinimalLabelSet(Environment const& env, GeneratorStats& stats, storm::storage::SymbolicModelDescription const& symbolicModel, storm::models::sparse::Model<T> const& model, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, double propertyThreshold, boost::optional<std::string> const& rewardName, bool strictBound, boost::container::flat_set<uint_fast64_t> const& dontCareLabels = boost::container::flat_set<uint_fast64_t>(), Options const& options = Options()) {
 #ifdef STORM_HAVE_Z3
                 std::vector<boost::container::flat_set<uint_fast64_t>> 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<storm::models::sparse::Model<T>> const& subModel = subChoiceOrigins.first;
                     std::vector<boost::container::flat_set<uint_fast64_t>> 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<std::chrono::milliseconds>(totalAnalysisTime);
+                stats.setupTime = std::chrono::duration_cast<std::chrono::milliseconds>(totalSetupTime);
+                stats.modelCheckingTime = std::chrono::duration_cast<std::chrono::milliseconds>(totalModelCheckingTime);
+                stats.solverTime = std::chrono::duration_cast<std::chrono::milliseconds>(totalSolverTime);
+
                 if (storm::settings::getModule<storm::settings::modules::CoreSettings>().isShowStatisticsSet()) {
                     boost::container::flat_set<uint64_t> 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<T> const& model, boost::container::flat_set<uint_fast64_t>& commandSet, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, bool silent = false) {
+            static void extendLabelSetLowerBound(storm::models::sparse::Model<T> const& model, boost::container::flat_set<uint_fast64_t>& 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<boost::container::flat_set<uint_fast64_t>> computeCounterexampleLabelSet(Environment const& env, storm::storage::SymbolicModelDescription const& symbolicModel, storm::models::sparse::Model<T> const& model, std::shared_ptr<storm::logic::Formula const> const& formula, boost::container::flat_set<uint_fast64_t> const& dontCareLabels = boost::container::flat_set<uint_fast64_t>(),  Options const& options = Options(true)) {
+            static std::vector<boost::container::flat_set<uint_fast64_t>> computeCounterexampleLabelSet(Environment const& env, GeneratorStats& stats, storm::storage::SymbolicModelDescription const& symbolicModel, storm::models::sparse::Model<T> const& model, std::shared_ptr<storm::logic::Formula const> const& formula, boost::container::flat_set<uint_fast64_t> const& dontCareLabels = boost::container::flat_set<uint_fast64_t>(),  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<HighLevelCounterexample> computeCounterexample(Environment const& env, storm::storage::SymbolicModelDescription const& symbolicModel, storm::models::sparse::Model<T> const& model, std::shared_ptr<storm::logic::Formula const> 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()) {

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"