Add possibility to output only failing traces (#24)

Signed-off-by: Marco Lampacrescia <[email protected]>

.github/workflows/build_executable.yml

@@ -5,7 +5,6 @@ on:
   push:
     branches: 
       - "main"
-      - "add-clang-format-check"
     tags:
       - "[0-9]+.[0-9]+.[0-9]+"
   schedule:  # This is a weekly schedule, running only on the "main" branch every Sunday at midnight
@@ -66,6 +65,8 @@ jobs:
                     make
             - name: Run linting
               run: |
+                    clang-format --version
+                    clang-tidy --version
                     ./scripts/check-clang-style.bash
             - name: Run tests
               run: |

include/samples/traces_exporter.hpp

@@ -36,6 +36,10 @@ class TracesExporter {
     TracesExporter(const std::filesystem::path& path_to_file, const storm::generator::VariableInformation& var_info);
     ~TracesExporter();
 
+    inline void setExportOnlyFailures() {
+        _export_only_failures = true;
+    }
+
     // TODO: Add information about the taken action and the current reward
     /*!
      * @brief Add a new line to the current trace, using the provided state
@@ -49,8 +53,16 @@ class TracesExporter {
     void addCurrentTraceResult(const TraceInformation& result);
 
   private:
+    /*!
+     * @brief Write the provided state into the loaded file.
+     * @param state The state description to write in the file.
+     */
+    void writeNextState(const storm::generator::CompressedState& state);
+
     std::ofstream _file;
     const storm::generator::VariableInformation& _var_info;
+    bool _export_only_failures = false;
+    std::vector<storm::generator::CompressedState> _current_trace_states;
     size_t _trace_counter;
     size_t _n_variables;
 };

include/settings/cmd_settings.hpp

@@ -55,6 +55,14 @@ class CmdSettings {
             .default_value(_loaded_settings.max_n_traces)
             .help("Maximum number of traces to generate (for debugging reasons, "
                   "overrides stat_method. 0 -> unset).");
+        _parser.add_argument("--store-only-not-verified-traces")
+            .default_value(false)
+            .implicit_value(true)
+            .help("When exporting traces, discard all the ones that are not failing.");
+        _parser.add_argument("--stop-after-failure")
+            .default_value(false)
+            .implicit_value(true)
+            .help("Stop generating traces after the first non-verified one is found.");
         _parser.add_argument("--n-threads").scan<'i', size_t>().default_value(_loaded_settings.n_threads).help("Number of threads to use.");
         _parser.add_argument("--batch-size")
             .scan<'i', size_t>()
@@ -88,6 +96,8 @@ class CmdSettings {
             _loaded_settings.epsilon = _parser.get<double>("--epsilon");
             _loaded_settings.max_trace_length = _parser.get<int>("--max-trace-length");
             _loaded_settings.max_n_traces = _parser.get<size_t>("--max-n-traces");
+            _loaded_settings.store_only_not_verified = _parser.get<bool>("--store-only-not-verified-traces");
+            _loaded_settings.stop_after_failure = _parser.get<bool>("--stop-after-failure");
             _loaded_settings.n_threads = _parser.get<size_t>("--n-threads");
             _loaded_settings.batch_size = _parser.get<size_t>("--batch-size");
             _loaded_settings.cache_explored_states = !_parser.get<bool>("--disable-explored-states-caching");

include/settings/smc_settings.hpp

@@ -34,13 +34,16 @@ struct SmcSettings {
     const size_t max_n_traces;
     const size_t n_threads;
     const size_t batch_size;
+    const bool stop_after_failure;
+    const bool store_only_not_verified;
     const bool cache_explored_states;
     const bool show_statistics;
 
     SmcSettings(const UserSettings& user_settings)
         : stat_method{user_settings.stat_method}, traces_file{user_settings.traces_file},
           confidence{user_settings.confidence}, epsilon{user_settings.epsilon}, max_trace_length{user_settings.max_trace_length},
           max_n_traces{user_settings.max_n_traces}, n_threads{user_settings.n_threads}, batch_size{user_settings.batch_size},
+          stop_after_failure{user_settings.stop_after_failure}, store_only_not_verified{user_settings.store_only_not_verified},
           cache_explored_states{user_settings.cache_explored_states}, show_statistics{user_settings.show_statistics} {}
 };
 }  // namespace smc_storm::settings

include/settings/user_settings.hpp

@@ -37,6 +37,8 @@ struct UserSettings {
     size_t max_n_traces{0U};
     size_t n_threads{1U};
     size_t batch_size{100U};
+    bool stop_after_failure{false};
+    bool store_only_not_verified{false};
     bool cache_explored_states{true};
     bool show_statistics{false};
 

src/model_checker/statistical_model_checking_engine.cpp

@@ -135,11 +135,12 @@ bool StatisticalModelCheckingEngine<ModelType, StoreExploredStates>::verifySetti
             is_settings_valid = false;
         }
         STORM_LOG_WARN_COND(
-            _settings.max_n_traces > 0U,
+            _settings.max_n_traces > 0U || (_settings.stop_after_failure && _settings.store_only_not_verified),
             "The amount of generated traces might be very large if left unbounded. Consider setting `--max-n-traces`.");
     } else {
         STORM_LOG_WARN_COND(
-            _settings.max_n_traces == 0U, "The amount of generated traces is bounded. This might affect reliability of the results.");
+            _settings.max_n_traces == 0U && !_settings.stop_after_failure,
+            "The amount of generated traces is limited. This might affect reliability of the results.");
     }
     return is_settings_valid;
 }
@@ -220,6 +221,9 @@ void StatisticalModelCheckingEngine<ModelType, StoreExploredStates>::performSamp
     if (export_traces) {
         // Prepare the traces export object
         _traces_exporter_ptr = std::make_unique<samples::TracesExporter>(_settings.traces_file, state_generation.getVariableInformation());
+        if (_settings.store_only_not_verified) {
+            _traces_exporter_ptr->setExportOnlyFailures();
+        }
     }
     samples::BatchResults batch_results = sampling_results.getBatchResultInstance();
 

src/samples/sampling_results.cpp

@@ -286,6 +286,10 @@ void SamplingResults::updateSamplingStatus() {
         _keep_sampling = false;
         return;
     }
+    if (_settings.stop_after_failure && _n_not_verified > 0U) {
+        _keep_sampling = false;
+        return;
+    }
     if (!minIterationsReached()) {
         _keep_sampling = true;
         return;

src/samples/traces_exporter.cpp

@@ -52,23 +52,39 @@ TracesExporter::TracesExporter(const std::filesystem::path& path_to_file, const
     }
     // No real variables, since they can only be transient
     _file << "\n\n";
+    _current_trace_states.clear();
 }
 
 TracesExporter::~TracesExporter() {
     storm::utility::closeFile(_file);
 }
 
 void TracesExporter::addCurrentTraceResult(const TraceInformation& result) {
-    _file << _trace_counter << ";;" << toString(result.outcome) << ";;";
-    _trace_counter++;
-    // Add one to account for the empty column between locations and remaining variables
-    for (size_t i = 0; i < _n_variables + 1U; i++) {
-        _file << ";";
+    if (!_export_only_failures || result.outcome == smc_storm::samples::TraceResult::NOT_VERIFIED) {
+        // In case we are not exporting only failures, this vector will be empty
+        for (const auto& state : _current_trace_states) {
+            writeNextState(state);
+        }
+        _file << _trace_counter << ";;" << toString(result.outcome) << ";;";
+        _trace_counter++;
+        // Add one to account for the empty column between locations and remaining variables
+        for (size_t i = 0; i < _n_variables + 1U; i++) {
+            _file << ";";
+        }
+        _file << "\n\n";
     }
-    _file << "\n\n";
+    _current_trace_states.clear();
 }
 
 void TracesExporter::addNextState(const storm::generator::CompressedState& state) {
+    if (_export_only_failures) {
+        _current_trace_states.emplace_back(state);
+    } else {
+        writeNextState(state);
+    }
+}
+
+void TracesExporter::writeNextState(const storm::generator::CompressedState& state) {
     _file << _trace_counter << ";;;;";
     // Locations
     for (const auto& loc_info : _var_info.locationVariables) {
@@ -88,4 +104,5 @@ void TracesExporter::addNextState(const storm::generator::CompressedState& state
     }
     _file << "\n";
 }
+
 }  // namespace smc_storm::samples