Interleave algorithm from CAV'25

CHANGELOG.md

@@ -7,7 +7,8 @@ The releases of major and minor versions contain an overview of changes since th
 
 Version 1.8.x
 -------------
-## Version 1.8.1
+
+## Version 1.8.1 (2023/06)
 - Workaround for issue with Boost >= 1.81
 
 ## Version 1.8.0 (2023/05)

README.md

@@ -5,6 +5,14 @@ Storm - A Modern Probabilistic Model Checker
 [![GitHub release](https://img.shields.io/github/release/moves-rwth/storm.svg)](https://github.com/moves-rwth/storm/releases/)
 [![DOI](https://zenodo.org/badge/DOI/10.5281/zenodo.1181896.svg)](https://doi.org/10.5281/zenodo.1181896)
 
+This is a custom fork of Storm for my Bachelor and Master Thesis at IIT Delhi, titled, "`INTERLEAVE` : An Empirically Faster Symbolic Algorithm for Maximal End Component Decomposition of MDPs" and advised by Suguman Bansal (Georgia Tech) and Subodh Sharma (IIT Delhi). Most of the code (except the new algorithm added -- `INTERLEAVE` and minor bug fixes) has been adapted from [the code for Felix Faber's Bachelor Thesis at RWTH Aachen](https://doi.org/10.5281/zenodo.8311805). I am grateful to Felix for writing an excellent thesis, and for writing code that was easy to understand and extend. Below is a brief description of the relevant files.
+
+- `src/storm/storage/SymbolicMEC.h` and `src/storm/storage/SymbolicMEC_stats.h` contain the algorithm implementations (the `_stats` files additionally count the number of transition BDD operations). The functions `symbolicMECDecompositionInterleave` and `symbolicMECDecompositionInterleave_stats` implement our `INTERLEAVE` algorithm.
+- `src/storm/storage/SymbolicOperations.h` and `src/storm/storage/SymbolicOperations_stats.h` contain the implementations of symbolic operations (including a new implementation of `pick` which I tried out and added support for to the `src/storm/storage/dd`, `src/storm/storage/dd/cudd` and `src/storm/storage/dd/sylvan` folders)
+- `src/storm/storage/SymbolicSCCDecomposition.h` and `src/storm/storage/SymbolicSCCDecomposition_stats.h` contain symbolic SCC decomposition algorithm implementations
+- `src/storm/storage/THESIS_DEBUG.h` contains miscellaneous definitions for the algorithms we benchmarked.
+
+To run any of the symbolic MEC decomposition algorithms, call the `storm` binary as usual, adding the argument `--benchmarkForceMECDecompositionAlgorithm <n>` with `n = 1,3,5` for `NAIVE, LOCKSTEP, INTERLEAVE`. Using `n = 2,4,6` also counts and outputs the number of symbolic operations performed by the `NAIVE, LOCKSTEP, INTERLEAVE` algorithms. Usual Storm GitHub README is below.
 
 Usage
 -----------------------------

src/storm-cli-utilities/model-handling.h

@@ -1,4 +1,5 @@
-#pragma once
+#ifndef STORM_CLI_MODEL_HANDLING_H
+#define STORM_CLI_MODEL_HANDLING_H
 
 #include "storm/api/storm.h"
 
@@ -50,6 +51,8 @@
 
 #include "storm/utility/Stopwatch.h"
 
+#include "storm/storage/THESIS_DEBUG.h"
+
 namespace storm {
 namespace cli {
 
@@ -512,6 +515,7 @@ std::shared_ptr<storm::models::ModelBase> buildModel(SymbolicInput const& input,
         } else if (builderType == storm::builder::BuilderType::Explicit) {
             result = buildModelSparse<ValueType>(input, buildSettings);
         }
+
     } else if (ioSettings.isExplicitSet() || ioSettings.isExplicitDRNSet() || ioSettings.isExplicitIMCASet()) {
         STORM_LOG_THROW(mpi.engine == storm::utility::Engine::Sparse, storm::exceptions::InvalidSettingsException,
                         "Can only use sparse engine with explicit input.");
@@ -1279,6 +1283,17 @@ std::shared_ptr<storm::models::ModelBase> buildPreprocessModelWithValueTypeAndDd
     std::shared_ptr<storm::models::ModelBase> model;
     if (!buildSettings.isNoBuildModelSet()) {
         model = buildModel<DdType, BuildValueType>(input, ioSettings, mpi);
+
+        // THESIS DATA GATHERING [rmnt] - Benchmarking the Symbolic MEC decomposition algorithms. Entry point.
+        auto builderType = storm::utility::getBuilderType(mpi.engine);
+        uint64_t DEBUG_THESIS_BENCHMARK = storm::settings::getModule<storm::settings::modules::DebugSettings>().forceMECDecompositionAlgorithm();
+        if (DEBUG_THESIS_BENCHMARK != 0) {
+            STORM_LOG_THROW(builderType == storm::builder::BuilderType::Dd, storm::exceptions::InvalidSettingsException,
+                            "MEC decomposition benchmarking is only available for symbolic models.");
+            doMecBenchmark<DdType, BuildValueType>((storm::models::ModelBase const&)*model, DEBUG_THESIS_BENCHMARK);
+            return model;
+        }
+
     }
 
     if (model) {
@@ -1287,6 +1302,7 @@ std::shared_ptr<storm::models::ModelBase> buildPreprocessModelWithValueTypeAndDd
 
     STORM_LOG_THROW(model || input.properties.empty(), storm::exceptions::InvalidSettingsException, "No input model.");
 
+
     if (model) {
         auto preprocessingResult = preprocessModel<DdType, BuildValueType, VerificationValueType>(model, input, mpi);
         if (preprocessingResult.second) {
@@ -1300,6 +1316,13 @@ std::shared_ptr<storm::models::ModelBase> buildPreprocessModelWithValueTypeAndDd
 template<storm::dd::DdType DdType, typename BuildValueType, typename VerificationValueType = BuildValueType>
 std::shared_ptr<storm::models::ModelBase> buildPreprocessExportModelWithValueTypeAndDdlib(SymbolicInput const& input, ModelProcessingInformation const& mpi) {
     auto model = buildPreprocessModelWithValueTypeAndDdlib<DdType, BuildValueType, VerificationValueType>(input, mpi);
+
+    // THESIS DATA GATHERING [rmnt] - Benchmarking the Symbolic MEC decomposition algorithms. Early exit.
+    uint64_t DEBUG_THESIS_BENCHMARK = storm::settings::getModule<storm::settings::modules::DebugSettings>().forceMECDecompositionAlgorithm();
+    if (DEBUG_THESIS_BENCHMARK != 0) {
+        return model;
+    }
+
     if (model) {
         exportModel<DdType, BuildValueType>(model, input);
     }
@@ -1320,6 +1343,13 @@ void processInputWithValueTypeAndDdlib(SymbolicInput const& input, ModelProcessi
     } else {
         std::shared_ptr<storm::models::ModelBase> model =
             buildPreprocessExportModelWithValueTypeAndDdlib<DdType, BuildValueType, VerificationValueType>(input, mpi);
+
+        // THESIS DATA GATHERING [rmnt] - Benchmarking the Symbolic MEC decomposition algorithms. Early exit.
+        uint64_t DEBUG_THESIS_BENCHMARK = storm::settings::getModule<storm::settings::modules::DebugSettings>().forceMECDecompositionAlgorithm();
+        if (DEBUG_THESIS_BENCHMARK != 0) {
+            return;
+        }
+
         if (model) {
             if (counterexampleSettings.isCounterexampleSet()) {
                 generateCounterexamples<VerificationValueType>(model, input);
@@ -1356,3 +1386,5 @@ void processInputWithValueType(SymbolicInput const& input, ModelProcessingInform
 }
 }  // namespace cli
 }  // namespace storm
+
+#endif

src/storm/settings/modules/DebugSettings.cpp

@@ -17,6 +17,7 @@ const std::string DebugSettings::additionalChecksOptionName = "additional-checks
 const std::string DebugSettings::logfileOptionName = "logfile";
 const std::string DebugSettings::logfileOptionShortName = "l";
 const std::string DebugSettings::testOptionName = "test";
+const std::string DebugSettings::forceMECDecompositionAlgorithmName = "benchmarkForceMECDecompositionAlgorithm";
 
 DebugSettings::DebugSettings() : ModuleSettings(moduleName) {
     this->addOption(storm::settings::OptionBuilder(moduleName, debugOptionName, false, "Print debug output.").build());
@@ -29,6 +30,13 @@ DebugSettings::DebugSettings() : ModuleSettings(moduleName) {
                         .addArgument(storm::settings::ArgumentBuilder::createStringArgument("filename", "The name of the file to write the log.").build())
                         .build());
     this->addOption(storm::settings::OptionBuilder(moduleName, testOptionName, false, "Activate a test setting.").setIsAdvanced().build());
+    this->addOption(storm::settings::OptionBuilder(moduleName, forceMECDecompositionAlgorithmName, false,
+                                                   "Forces symbolic model on MDP with an mec decomposition with a specific symbolic decomposition algorithm.")
+                        .setIsAdvanced()
+                        .addArgument(storm::settings::ArgumentBuilder::createUnsignedIntegerArgument(
+                                         "value", "1\t\tNaive\n2\t\tLockstep\n3\t\tCollapsing\n4\t\tMyalgo") // TODO change myalgo to nice name
+                                         .build())
+                        .build());
 }
 
 bool DebugSettings::isDebugSet() const {
@@ -55,6 +63,14 @@ bool DebugSettings::isTestSet() const {
     return this->getOption(testOptionName).getHasOptionBeenSet();
 }
 
+uint_fast64_t DebugSettings::forceMECDecompositionAlgorithm() const {
+    if (this->getOption(forceMECDecompositionAlgorithmName).getHasOptionBeenSet()) {
+        return this->getOption(forceMECDecompositionAlgorithmName).getArgumentByName("value").getValueAsUnsignedInteger();
+    } else {
+        return 0;
+    }
+}
+
 }  // namespace modules
 }  // namespace settings
 }  // namespace storm

src/storm/settings/modules/DebugSettings.h

@@ -60,6 +60,9 @@ class DebugSettings : public ModuleSettings {
      */
     bool isTestSet() const;
 
+    // Debug function for the Symbolic MEC decomposition benchmarks
+    uint_fast64_t forceMECDecompositionAlgorithm() const;
+
     // The name of the module.
     static const std::string moduleName;
 
@@ -71,6 +74,7 @@ class DebugSettings : public ModuleSettings {
     static const std::string logfileOptionName;
     static const std::string logfileOptionShortName;
     static const std::string testOptionName;
+    static const std::string forceMECDecompositionAlgorithmName;
 };
 
 }  // namespace modules