From 5e5fe707a7ec4bfe21ec619f4ad95eabea6cae54 Mon Sep 17 00:00:00 2001 From: Matthias Volk Date: Thu, 15 Jun 2023 20:03:16 +0200 Subject: [PATCH 01/25] Storm version 1.8.1 (#390) --- CHANGELOG.md | 3 ++- version.cmake | 2 +- 2 files changed, 3 insertions(+), 2 deletions(-) diff --git a/CHANGELOG.md b/CHANGELOG.md index 2f7a73528f..f4c054df12 100644 --- a/CHANGELOG.md +++ b/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) diff --git a/version.cmake b/version.cmake index d5b9534394..c4c844edfb 100644 --- a/version.cmake +++ b/version.cmake @@ -1,4 +1,4 @@ set(STORM_VERSION_MAJOR 1) set(STORM_VERSION_MINOR 8) -set(STORM_VERSION_PATCH 0) +set(STORM_VERSION_PATCH 1) From 12a48d6a7c8778cddd2e4bce8381a7969a3ee4b8 Mon Sep 17 00:00:00 2001 From: Ramneet Singh Date: Mon, 27 May 2024 19:55:31 +0530 Subject: [PATCH 02/25] Add --benchmarkForceMECDecompositionAlgorithm Command Line Setting --- src/storm/settings/modules/DebugSettings.cpp | 16 ++++++++++++++++ src/storm/settings/modules/DebugSettings.h | 4 ++++ 2 files changed, 20 insertions(+) diff --git a/src/storm/settings/modules/DebugSettings.cpp b/src/storm/settings/modules/DebugSettings.cpp index 8a01dbd790..e8712115fc 100644 --- a/src/storm/settings/modules/DebugSettings.cpp +++ b/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 diff --git a/src/storm/settings/modules/DebugSettings.h b/src/storm/settings/modules/DebugSettings.h index 408e4a27a2..c3efada240 100644 --- a/src/storm/settings/modules/DebugSettings.h +++ b/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 From 673d9252108d3c9b0796cb25ce92f67bda90bf08 Mon Sep 17 00:00:00 2001 From: Ramneet Singh Date: Mon, 3 Jun 2024 12:30:44 +0530 Subject: [PATCH 03/25] Setup Benchmarking Skeleton | Next step is to fill in MEC Decomp Algos --- src/storm-cli-utilities/model-handling.h | 9 ++ src/storm/storage/THESIS_DEBUG.h | 181 +++++++++++++++++++++++ 2 files changed, 190 insertions(+) create mode 100644 src/storm/storage/THESIS_DEBUG.h diff --git a/src/storm-cli-utilities/model-handling.h b/src/storm-cli-utilities/model-handling.h index af1a5e6b55..33662fbb21 100644 --- a/src/storm-cli-utilities/model-handling.h +++ b/src/storm-cli-utilities/model-handling.h @@ -518,6 +518,15 @@ std::shared_ptr buildModel(SymbolicInput const& input, result = buildModelExplicit(ioSettings, buildSettings); } + // THESIS DATA GATHERING [rmnt] - Benchmarking the Symbolic MEC decomposition algorithms. Entry point. + uint64_t DEBUG_THESIS_BENCHMARK = storm::settings::getModule().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((storm::models::ModelBase const &)*result, DEBUG_THESIS_BENCHMARK); + exit(0); + } + modelBuildingWatch.stop(); if (result) { STORM_PRINT("Time for model construction: " << modelBuildingWatch << ".\n\n"); diff --git a/src/storm/storage/THESIS_DEBUG.h b/src/storm/storage/THESIS_DEBUG.h new file mode 100644 index 0000000000..0432f30f74 --- /dev/null +++ b/src/storm/storage/THESIS_DEBUG.h @@ -0,0 +1,181 @@ +#pragma once + +#ifndef STORM_THESIS_DEBUG_H +#define STORM_THESIS_DEBUG_H + +#include "storm/storage/dd/DdType.h" +#include "storm/models/Model.h" +#include "storm/models/symbolic/NondeterministicModel.h" +#include "storm/utility/macros.h" +#include "storm/utility/Stopwatch.h" + +#include + +enum class MecBenchmarkType { + NAIVE, + NAIVE_STATS, + LOCKSTEP, + LOCKSTEP_STATS, + INTERLEAVE, + INTERLEAVE_STATS +}; + +MecBenchmarkType debugIntToBenchmarkType(uint64_t forcedMecAlgorithm) +{ + switch(forcedMecAlgorithm) { + case 1 : return MecBenchmarkType::NAIVE; + case 2 : return MecBenchmarkType::NAIVE_STATS; + case 3 : return MecBenchmarkType::LOCKSTEP; + case 4 : return MecBenchmarkType::LOCKSTEP_STATS; + case 5 : return MecBenchmarkType::INTERLEAVE; + case 6 : return MecBenchmarkType::INTERLEAVE_STATS; + default: STORM_LOG_ASSERT(false, "Unexpected symbolic benchmark int"); + } + STORM_LOG_ASSERT(false, "Unreachable"); +} + +std::string benchmarkToString(const MecBenchmarkType type) +{ + switch(type) { + case MecBenchmarkType::NAIVE : return "NAIVE"; + case MecBenchmarkType::NAIVE_STATS : return "NAIVE-STATS"; + case MecBenchmarkType::LOCKSTEP : return "LOCKSTEP"; + case MecBenchmarkType::LOCKSTEP_STATS : return "LOCKSTEP-STATS"; + case MecBenchmarkType::INTERLEAVE : return "INTERLEAVE"; + case MecBenchmarkType::INTERLEAVE_STATS : return "INTERLEAVE-STATS"; + } +} + +struct BenchmarkResult { + MecBenchmarkType type; + uint_fast64_t mecCount; + storm::utility::Stopwatch::NanosecondType decompositionTimeInNanoseconds; + + BenchmarkResult(MecBenchmarkType type, uint_fast64_t mecCount, storm::utility::Stopwatch::NanosecondType decompositionTimeInNanoseconds) { + this->type = type; + this->mecCount = mecCount; + this->decompositionTimeInNanoseconds = decompositionTimeInNanoseconds; + } + + void print() { + std::string algorithm = benchmarkToString(type); + std::cout << "BENCHMARK MEC DECOMPOSITION (algorithm, time, mecCount[, conversionTime]): " + << algorithm << ", " << decompositionTimeInNanoseconds << ", " + << mecCount << "\n"; + } +}; + +template +uint_fast64_t getDdVariablesCount(storm::dd::DdManager& manager, std::set variables) { + uint_fast64_t count = 0; + for (auto const& metaVariable : variables) { + count += manager.getMetaVariable(metaVariable).getNumberOfDdVariables(); + } + return count; +} + +template +BenchmarkResult doSymbolicBenchmark(storm::models::symbolic::NondeterministicModel const& symbolicModel, + MecBenchmarkType type) { + auto & manager = symbolicModel.getManager(); + std::vector> mecs; + std::chrono::high_resolution_clock::time_point decompositionTimestampStart; + std::chrono::high_resolution_clock::time_point decompositionTimestampEnd; + + switch (type) + { + case MecBenchmarkType::NAIVE: + decompositionTimestampStart = std::chrono::high_resolution_clock::now(); + mecs = symbolicMEC::symbolicMECDecompositionBasic( + symbolicModel.getReachableStates(), symbolicModel.getTransitionMatrix().toBDD(), + symbolicModel.getRowVariables(), symbolicModel.getColumnVariables(), symbolicModel.getNondeterminismVariables(), + symbolicModel.getRowColumnMetaVariablePairs() + ); + decompositionTimestampEnd = std::chrono::high_resolution_clock::now(); + break; + + case MecBenchmarkType::NAIVE_STATS: + decompositionTimestampStart = std::chrono::high_resolution_clock::now(); + mecs = symbolicMEC_EBA::symbolicMECDecompositionBasic_stats( + symbolicModel.getReachableStates(), symbolicModel.getTransitionMatrix().toBdd(), + symbolicModel.getRowVariables(), symbolicModel.getColumnVariables(), symbolicModel.getNondeterminismVariables(), + symbolicModel.getRowColumnMetaVariablePairs()); + decompositionTimestampEnd = std::chrono::high_resolution_clock::now(); + break; + + case MecBenchmarkType::LOCKSTEP: + decompositionTimestampStart = std::chrono::high_resolution_clock::now(); + mecs = symbolicMEC_EBA::symbolicMECDecompositionLockstep( + symbolicModel.getReachableStates(), symbolicModel.getTransitionMatrix().toBdd(), + symbolicModel.getRowVariables(), symbolicModel.getColumnVariables(), symbolicModel.getNondeterminismVariables(), + symbolicModel.getRowColumnMetaVariablePairs()); + decompositionTimestampEnd = std::chrono::high_resolution_clock::now(); + break; + + case MecBenchmarkType::LOCKSTEP_STATS: + decompositionTimestampStart = std::chrono::high_resolution_clock::now(); + mecs = symbolicMEC_EBA::symbolicMECDecompositionLockstep_stats( + symbolicModel.getReachableStates(), symbolicModel.getTransitionMatrix().toBdd(), + symbolicModel.getRowVariables(), symbolicModel.getColumnVariables(), symbolicModel.getNondeterminismVariables(), + symbolicModel.getRowColumnMetaVariablePairs()); + decompositionTimestampEnd = std::chrono::high_resolution_clock::now(); + break; + + case MecBenchmarkType::INTERLEAVE: + decompositionTimestampStart = std::chrono::high_resolution_clock::now(); + mecs = symbolicMEC_EBA::symbolicMECDecompositionInterleave( + symbolicModel.getReachableStates(), symbolicModel.getTransitionMatrix().toBdd(), + symbolicModel.getRowVariables(), symbolicModel.getColumnVariables(), symbolicModel.getNondeterminismVariables(), + symbolicModel.getRowColumnMetaVariablePairs()); + decompositionTimestampEnd = std::chrono::high_resolution_clock::now(); + break; + + case MecBenchmarkType::INTERLEAVE_STATS: + decompositionTimestampStart = std::chrono::high_resolution_clock::now(); + mecs = symbolicMEC_EBA::symbolicMECDecompositionInterleave_stats( + symbolicModel.getReachableStates(), symbolicModel.getTransitionMatrix().toBdd(), + symbolicModel.getRowVariables(), symbolicModel.getColumnVariables(), symbolicModel.getNondeterminismVariables(), + symbolicModel.getRowColumnMetaVariablePairs()); + decompositionTimestampEnd = std::chrono::high_resolution_clock::now(); + break; + + default: + STORM_LOG_ASSERT(false, "Unexpected symbolic benchmark type"); + break; + } + + // Output Model stats + uint_fast64_t ddRowVariableCount = getDdVariablesCount(manager, symbolicModel.getRowVariables()); + uint_fast64_t ddColumnVariableCount = getDdVariablesCount(manager, symbolicModel.getColumnVariables()); + uint_fast64_t ddNondeterminismCount = getDdVariablesCount(manager, symbolicModel.getNondeterminismVariables()); + std::cout << "Symbolic model stats: " << std::endl + << "Type: " << symbolicModel.getType() << std::endl + << "States: " << symbolicModel.getNumberOfStates() << " (" << symbolicModel.getReachableStates().getNodeCount() << " nodes)" + << std::endl + << "Transitions: " << symbolicModel.getNumberOfTransitions() << " (" << symbolicModel.getTransitionMatrix().toBdd().getNodeCount() + << " nodes)" << std::endl + << "Choices: " << symbolicModel.getNumberOfChoices() << std::endl + << "Variables Total: " + << (symbolicModel.getRowVariables().size() + symbolicModel.getColumnVariables().size() + + symbolicModel.getNondeterminismVariables().size()) + << " (" << (ddRowVariableCount + ddColumnVariableCount + ddNondeterminismCount) << " DD variables)" << std::endl + << "Variables Row: " << symbolicModel.getRowVariables().size() << " (" << ddRowVariableCount << " DD variables)" << std::endl + << "Variables Column: " << symbolicModel.getColumnVariables().size() << " (" << ddColumnVariableCount << " DD variables)" << std::endl + << "Variables Nondeterminism: " << symbolicModel.getNondeterminismVariables().size() << " (" << ddNondeterminismCount + << " DD variables)" << std::endl + << std::endl; + + uint_fast64_t decompositionTimeInNanoseconds = (decompositionTimestampEnd - decompositionTimestampStart).count(); + return BenchmarkResult(type, mecs.size(), decompositionTimeInNanoseconds); +} + +template +void doMecBenchmark(storm::models::ModelBase const& model, + uint64_t forcedMecAlgorithm) { + assert(forcedMecAlgorithm > 0); + MecBenchmarkType type = debugIntToBenchmarkType(forcedMecAlgorithm); + BenchmarkResult benchmark = doSymbolicBenchmark((storm::models::symbolic::NondeterministicModel&)model, type); + benchmark.print(); +} + +#endif \ No newline at end of file From aca586371103e551d8fb29264824c3ca3d995131 Mon Sep 17 00:00:00 2001 From: Ramneet Singh Date: Fri, 14 Jun 2024 12:53:32 +0530 Subject: [PATCH 04/25] Add pickOneCube Bdd Op to Sylvan and Cudd | Add _stats and normal implementations for Naive,Lockstep | Change #pragma once discipline --- src/storm-cli-utilities/model-handling.h | 5 +- src/storm/storage/SymbolicMEC.h | 236 ++++++++++++++++ src/storm/storage/SymbolicMEC_stats.h | 262 ++++++++++++++++++ src/storm/storage/SymbolicOperations.h | 67 +++++ src/storm/storage/SymbolicOperations_stats.h | 73 +++++ src/storm/storage/SymbolicSCCDecomposition.h | 113 ++++++++ .../storage/SymbolicSCCDecomposition_stats.h | 114 ++++++++ src/storm/storage/THESIS_DEBUG.h | 30 +- src/storm/storage/dd/Bdd.cpp | 7 + src/storm/storage/dd/Bdd.h | 8 + src/storm/storage/dd/cudd/InternalCuddBdd.cpp | 12 + src/storm/storage/dd/cudd/InternalCuddBdd.h | 8 + .../storage/dd/sylvan/InternalSylvanBdd.cpp | 5 + .../storage/dd/sylvan/InternalSylvanBdd.h | 8 + 14 files changed, 934 insertions(+), 14 deletions(-) create mode 100644 src/storm/storage/SymbolicMEC.h create mode 100644 src/storm/storage/SymbolicMEC_stats.h create mode 100644 src/storm/storage/SymbolicOperations.h create mode 100644 src/storm/storage/SymbolicOperations_stats.h create mode 100644 src/storm/storage/SymbolicSCCDecomposition.h create mode 100644 src/storm/storage/SymbolicSCCDecomposition_stats.h diff --git a/src/storm-cli-utilities/model-handling.h b/src/storm-cli-utilities/model-handling.h index 33662fbb21..7851b43334 100644 --- a/src/storm-cli-utilities/model-handling.h +++ b/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" @@ -1365,3 +1366,5 @@ void processInputWithValueType(SymbolicInput const& input, ModelProcessingInform } } // namespace cli } // namespace storm + +#endif \ No newline at end of file diff --git a/src/storm/storage/SymbolicMEC.h b/src/storm/storage/SymbolicMEC.h new file mode 100644 index 0000000000..3983ada952 --- /dev/null +++ b/src/storm/storage/SymbolicMEC.h @@ -0,0 +1,236 @@ +#ifndef STORM_STORAGE_SYMBOLICMEC_H +#define STORM_STORAGE_SYMBOLICMEC_H + +#include +#include +#include "storm/storage/dd/DdType.h" +#include "storm/storage/dd/Bdd.h" +#include "storm/storage/SymbolicSCCDecomposition.h" + +namespace symbolicMEC { + +template +struct StateActionPair { + storm::dd::Bdd states; + storm::dd::Bdd actions; // [rmnt]: Actions is really state-action pairs. + + StateActionPair& operator|=(StateActionPair const & other) { + states |= other.states; + actions |= other.actions; + return *this; + } +}; + +template +static bool isTrivialSccWithoutSelfEdge(StateActionPair const & scc, + storm::dd::Bdd const & transitionsWithActions, + std::vector> const & metaVariablesRowColumnPairs) { + bool isTrivialScc = (1 == scc.states.getNonZeroCount()); + // [rmnt] TODO : Review the noSelfEdge condition. Do you need && scc.states also? + bool noSelfEdge = (transitionsWithActions && scc.actions && scc.states.swapVariables(metaVariablesRowColumnPairs)).isZero(); + return (isTrivialScc && noSelfEdge); +} + + +/* Given a set of vertices T, the random attractor Attr_R(T) + * is a set of vertices consisting of + * (1) T, + * (2) random vertices with an edge to some vertex in Attr_R(T), + * (3) player-1 vertices with all outgoing edges in Attr_R(T). + */ +template +static StateActionPair computeRandomAttractor(storm::dd::Bdd const & actionsToApplyOn, + storm::dd::Bdd const & allStates, + storm::dd::Bdd const & transitionsWithActions, + std::set const & metaVariablesColumn, + std::set const & metaVariablesActions, + std::vector> const & metaVariablesRowColumnPairs) { + StateActionPair nextSet = { .states = allStates.getDdManager().getBddZero(), .actions = actionsToApplyOn }; + StateActionPair currentSet; + do { + currentSet = nextSet; + + // Vertices + storm::dd::Bdd actionsCannotIntoCurrent = ( transitionsWithActions && ( ! currentSet.actions) + ).existsAbstract(metaVariablesColumn); // [rmnt]: All (s,a) pairs which aren't included in currentSet + storm::dd::Bdd newVertices = currentSet.actions.existsAbstract(metaVariablesActions) + && ( ! (actionsCannotIntoCurrent.existsAbstract(metaVariablesActions))); + // [rmnt]: All states s such that some (s,a1) in currentSet and all (s,a) pairs in currentSet + nextSet.states = (currentSet.states || newVertices) && allStates; + + // Actions [rmnt] Actions is really state-action pairs. + storm::dd::Bdd currentVerticesAsColumn = nextSet.states.swapVariables(metaVariablesRowColumnPairs); + storm::dd::Bdd actionsCanIntoCurrentVertices = (transitionsWithActions && currentVerticesAsColumn).existsAbstract(metaVariablesColumn); + nextSet.actions = currentSet.actions || actionsCanIntoCurrentVertices; + } while (currentSet.states != nextSet.states); + return currentSet; +} + +// For a set of states S, +// return all actions which have a non-zero-probability of leaving S. +template +static storm::dd::Bdd ROut(storm::dd::Bdd const & sccStates, + storm::dd::Bdd const & transitionsWithActions, + std::set const & metaVariablesColumn, + std::vector> const & metaVariablesRowColumnPairs) { + storm::dd::Bdd transitionsFromSccToOutside = sccStates && transitionsWithActions && ( ! sccStates.swapVariables(metaVariablesRowColumnPairs)); + storm::dd::Bdd actionsLeavingScc = transitionsFromSccToOutside.existsAbstract(metaVariablesColumn); + return actionsLeavingScc; +} + + +// As described in +// "Symbolic algorithms for graphs and Markov decision processes with fairness objectives" +template +std::vector> symbolicMECDecompositionNaive(storm::dd::Bdd const & allStates, + storm::dd::Bdd const & transitionsWithActions, + std::set const & metaVariablesRow, + std::set const & metaVariablesColumn, + std::set const & metaVariablesActions, + std::vector> const & metaVariablesRowColumnPairs) { + storm::dd::Bdd workingCopyTransitionsWithActions(transitionsWithActions); + std::vector> result{}; + std::stack> mecCandidates{}; + for (const auto& scc : symbolicScc::decomposition(allStates, workingCopyTransitionsWithActions.existsAbstract(metaVariablesActions), + metaVariablesRow, metaVariablesColumn)) { + mecCandidates.push(scc); + } + while ( ! mecCandidates.empty()) { + storm::dd::Bdd scc = mecCandidates.top(); + mecCandidates.pop(); + + if (isTrivialSccWithoutSelfEdge(scc, workingCopyTransitionsWithActions, metaVariablesRowColumnPairs)) { + continue; + } + + storm::dd::Bdd sccROut = ROut(scc, workingCopyTransitionsWithActions, metaVariablesColumn, metaVariablesRowColumnPairs); + if (sccROut.isZero()) { + result.template emplace_back(scc); + } else { + StateActionPair attractor = computeRandomAttractor(sccROut, scc, workingCopyTransitionsWithActions, metaVariablesColumn, metaVariablesActions, metaVariablesRowColumnPairs); + workingCopyTransitionsWithActions &= !attractor.actions; + for (auto const& subScc : symbolicScc::decomposition( + scc && !attractor.states, workingCopyTransitionsWithActions.existsAbstract(metaVariablesActions), metaVariablesRow, metaVariablesColumn)) { + mecCandidates.push(subScc); + } + } + } + return result; +} + +// As described in +// "Symbolic Algorithms for Graphs and Markov Decision Processes with Fairness Objectives" +// Slightly simplified we only care about the bottom scc +template +storm::dd::Bdd LockStepSearch(storm::dd::Bdd const & states, // S + storm::dd::Bdd const & statesWithRemovedEdges, // T_S + storm::dd::Bdd const & transitionsWithoutActions, + std::set const & metaVariablesRow, + std::set const & metaVariablesColumn) { + storm::dd::Bdd ts = storm::dd::Bdd(statesWithRemovedEdges); + std::unordered_map, storm::dd::Bdd> c{}; + while ( ! ts.isZero()) { + storm::dd::Bdd v = pick(ts); + ts &= ! v; + c[v] = storm::dd::Bdd(v); + } + + ts = storm::dd::Bdd(statesWithRemovedEdges); + while (true) { + for (auto it = c.cbegin(); it != c.cend(); ) { + storm::dd::Bdd t = storm::dd::Bdd(it->first); + storm::dd::Bdd ct = storm::dd::Bdd(it->second); + storm::dd::Bdd ctNew = ct || post(ct, states, transitionsWithoutActions, metaVariablesRow, metaVariablesColumn); + if ((ctNew && ts).getNonZeroCount() > 1) { // [rmnt] there was another state in T_S in the same SCC as t, so we can ignore t. + ts &= ! t; + c.erase(it++); + } else { + if (ctNew == ct) { + return ctNew; + } + c[t] = ctNew; + ++it; + } + } + } +} + +// As described in +// "Symbolic Algorithms for Graphs and Markov Decision Processes with Fairness Objectives" +// Uses a lockstep search +template +std::vector> symbolicMECDecompositionLockstep(storm::dd::Bdd const & allStates, + storm::dd::Bdd const & transitionsWithActions, + std::set const & metaVariablesRow, + std::set const & metaVariablesColumn, + std::set const & metaVariablesActions, + std::vector> const & metaVariablesRowColumnPairs) { + struct MecCandidate { + storm::dd::Bdd states; // In paper: S + storm::dd::Bdd statesWithRemovedEdge; // In Paper: T_s + }; + + // Helper function for better readability + auto hasAtLeastOneEdge = + [metaVariablesActions, metaVariablesRow, metaVariablesColumn, metaVariablesRowColumnPairs] + (storm::dd::Bdd scc, storm::dd::Bdd transitionsWithActions) { + // Paper suggestion + return ! (post(scc, scc, transitionsWithActions.existsAbstract(metaVariablesActions), metaVariablesRow, metaVariablesColumn)).isZero(); + }; + + uint_fast64_t m = (transitionsWithActions.existsAbstract(metaVariablesActions) && allStates).getNonZeroCount(); + storm::dd::Bdd workingCopyTransitionsWithActions(transitionsWithActions); + std::vector> result{}; // In paper: "goodC" + std::stack mecCandidates{}; // In paper: X + for (const auto & scc : symbolicScc::decomposition(allStates, workingCopyTransitionsWithActions.existsAbstract(metaVariablesActions), metaVariablesRow, metaVariablesColumn)) { + MecCandidate pair = { scc, scc.getDdManager().getBddZero() }; + mecCandidates.push(pair); + } + while ( ! mecCandidates.empty()) { + MecCandidate currentCandidate = mecCandidates.top(); + storm::dd::Bdd scc = currentCandidate.states; + storm::dd::Bdd sccTs = currentCandidate.statesWithRemovedEdge; + mecCandidates.pop(); + + storm::dd::Bdd sccROut = ROut(scc, workingCopyTransitionsWithActions, metaVariablesColumn, metaVariablesRowColumnPairs); + StateActionPair randomAttractor = computeRandomAttractor(sccROut, scc, workingCopyTransitionsWithActions, metaVariablesColumn, metaVariablesActions, metaVariablesRowColumnPairs); + scc &= ! randomAttractor.states; + workingCopyTransitionsWithActions &= ! randomAttractor.actions; + sccTs = (sccTs || randomAttractor.actions.existsAbstract(metaVariablesActions)) && scc; + if (hasAtLeastOneEdge(scc, workingCopyTransitionsWithActions)) { + if (sccTs.isZero()) { + result.template emplace_back(scc); + } else if (sccTs.getNonZeroCount() >= sqrt(m)) { + std::vector> subSccs = symbolicScc::decomposition( + scc, workingCopyTransitionsWithActions.existsAbstract(metaVariablesActions), metaVariablesRow, metaVariablesColumn); + if (subSccs.size() == 1) { + result.template emplace_back(scc); + } else { + for (auto const& subScc : subSccs) { + MecCandidate toProcess = {subScc, scc.getDdManager().getBddZero()}; + mecCandidates.push(toProcess); + } + } + } else { + // bottomScc is "C" in paper + storm::dd::Bdd bottomScc = LockStepSearch(scc, sccTs, + workingCopyTransitionsWithActions.existsAbstract(metaVariablesActions), + metaVariablesRow, metaVariablesColumn); + if (hasAtLeastOneEdge(bottomScc, workingCopyTransitionsWithActions)) { + result.template emplace_back(bottomScc); + } + + storm::dd::Bdd statesLeadingIntoBottomScc = pre(bottomScc, scc, workingCopyTransitionsWithActions.existsAbstract(metaVariablesActions), metaVariablesRow, metaVariablesColumn); + mecCandidates.emplace((MecCandidate) { + scc && ( ! bottomScc), + (scc && ( ! bottomScc)) && (statesLeadingIntoBottomScc || sccTs), + }); + } + } + } + return result; +} + +} // namespace symbolicMEC + +#endif \ No newline at end of file diff --git a/src/storm/storage/SymbolicMEC_stats.h b/src/storm/storage/SymbolicMEC_stats.h new file mode 100644 index 0000000000..98afbb4381 --- /dev/null +++ b/src/storm/storage/SymbolicMEC_stats.h @@ -0,0 +1,262 @@ +#ifndef STORM_STORAGE_SYMBOLICMEC_STATS_H +#define STORM_STORAGE_SYMBOLICMEC_STATS_H + +#include +#include +#include "storm/storage/dd/DdType.h" +#include "storm/storage/dd/Bdd.h" +#include "storm/storage/SymbolicSCCDecomposition_stats.h" + +namespace symbolicMEC_stats { + +template +struct StateActionPair { + storm::dd::Bdd states; + storm::dd::Bdd actions; // [rmnt]: Actions is really state-action pairs. + + StateActionPair& operator|=(StateActionPair const & other) { + states |= other.states; + actions |= other.actions; + return *this; + } +}; + +template +static bool isTrivialSccWithoutSelfEdge_stats(StateActionPair const & scc, + storm::dd::Bdd const & transitionsWithActions, + std::vector> const & metaVariablesRowColumnPairs, + uint_fast64_t &countSymbolicOps) { + bool isTrivialScc = (1 == scc.states.getNonZeroCount()); // [rmnt] TODO : Check if this should be counted as a symbolic op + countSymbolicOps++; + // [rmnt] TODO : Review the noSelfEdge condition. Do you need && scc.states also? + bool noSelfEdge = (transitionsWithActions && scc.actions && scc.states.swapVariables(metaVariablesRowColumnPairs)).isZero(); + return (isTrivialScc && noSelfEdge); +} + + +/* Given a set of vertices T, the random attractor Attr_R(T) + * is a set of vertices consisting of + * (1) T, + * (2) random vertices with an edge to some vertex in Attr_R(T), + * (3) player-1 vertices with all outgoing edges in Attr_R(T). + */ +template +static StateActionPair computeRandomAttractor_stats(storm::dd::Bdd const & actionsToApplyOn, + storm::dd::Bdd const & allStates, + storm::dd::Bdd const & transitionsWithActions, + std::set const & metaVariablesColumn, + std::set const & metaVariablesActions, + std::vector> const & metaVariablesRowColumnPairs, + uint_fast64_t &countSymbolicOps) { + StateActionPair nextSet = { .states = allStates.getDdManager().getBddZero(), .actions = actionsToApplyOn }; + StateActionPair currentSet; + do { + currentSet = nextSet; + + // Vertices + storm::dd::Bdd actionsCannotIntoCurrent = ( transitionsWithActions && ( ! currentSet.actions) + ).existsAbstract(metaVariablesColumn); // [rmnt]: All (s,a) pairs which aren't included in currentSet + countSymbolicOps++; + storm::dd::Bdd newVertices = currentSet.actions.existsAbstract(metaVariablesActions) + && ( ! (actionsCannotIntoCurrent.existsAbstract(metaVariablesActions))); + // [rmnt]: All states s such that some (s,a1) in currentSet and all (s,a) pairs in currentSet + countSymbolicOps++; + nextSet.states = (currentSet.states || newVertices) && allStates; + + // Actions [rmnt] Actions is really state-action pairs. + storm::dd::Bdd currentVerticesAsColumn = nextSet.states.swapVariables(metaVariablesRowColumnPairs); + storm::dd::Bdd actionsCanIntoCurrentVertices = (transitionsWithActions && currentVerticesAsColumn).existsAbstract(metaVariablesColumn); + countSymbolicOps++; + nextSet.actions = currentSet.actions || actionsCanIntoCurrentVertices; + } while (currentSet.states != nextSet.states); + return currentSet; +} + +// For a set of states S, +// return all actions which have a non-zero-probability of leaving S. +template +static storm::dd::Bdd ROut_stats(storm::dd::Bdd const & sccStates, + storm::dd::Bdd const & transitionsWithActions, + std::set const & metaVariablesColumn, + std::vector> const & metaVariablesRowColumnPairs, + uint_fast64_t &countSymbolicOps) { + storm::dd::Bdd transitionsFromSccToOutside = sccStates && transitionsWithActions && ( ! sccStates.swapVariables(metaVariablesRowColumnPairs)); + storm::dd::Bdd actionsLeavingScc = transitionsFromSccToOutside.existsAbstract(metaVariablesColumn); + countSymbolicOps++; + return actionsLeavingScc; +} + +// As described in +// "Symbolic algorithms for graphs and Markov decision processes with fairness objectives" +template +std::vector> symbolicMECDecompositionNaive_stats(storm::dd::Bdd const & allStates, + storm::dd::Bdd const & transitionsWithActions, + std::set const & metaVariablesRow, + std::set const & metaVariablesColumn, + std::set const & metaVariablesActions, + std::vector> const & metaVariablesRowColumnPairs, + uint_fast64_t &countSymbolicOps) { + storm::dd::Bdd workingCopyTransitionsWithActions(transitionsWithActions); + std::vector> result{}; + std::stack> mecCandidates{}; + for (const auto& scc : symbolicScc_stats::decomposition_stats(allStates, workingCopyTransitionsWithActions.existsAbstract(metaVariablesActions), + metaVariablesRow, metaVariablesColumn, countSymbolicOps)) { + mecCandidates.push(scc); + } + while ( ! mecCandidates.empty()) { + storm::dd::Bdd scc = mecCandidates.top(); + mecCandidates.pop(); + + if (isTrivialSccWithoutSelfEdge_stats(scc, workingCopyTransitionsWithActions, metaVariablesRowColumnPairs, countSymbolicOps)) { + continue; + } + + storm::dd::Bdd sccROut = ROut_stats(scc, workingCopyTransitionsWithActions, + metaVariablesColumn, metaVariablesRowColumnPairs, countSymbolicOps); + if (sccROut.isZero()) { + result.template emplace_back(scc); + } else { + StateActionPair attractor = computeRandomAttractor_stats(sccROut, scc, workingCopyTransitionsWithActions, + metaVariablesColumn, metaVariablesActions, metaVariablesRowColumnPairs, countSymbolicOps); + workingCopyTransitionsWithActions &= !attractor.actions; + countSymbolicOps++; // [rmnt] For the existsAbstract call in args to scc decomp + for (auto const& subScc : symbolicScc_stats::decomposition_stats( + scc && !attractor.states, workingCopyTransitionsWithActions.existsAbstract(metaVariablesActions), + metaVariablesRow, metaVariablesColumn, countSymbolicOps)) { + mecCandidates.push(subScc); + } + } + std::cout << "DEBUG Transition BDD stats: " + << workingCopyTransitionsWithActions.getNonZeroCount() << " Transitions (" << workingCopyTransitionsWithActions.getNodeCount() << " nodes), " + << workingCopyTransitionsWithActions.existsAbstract(metaVariablesActions).getNonZeroCount() << " Transitions (" << workingCopyTransitionsWithActions.existsAbstract(metaVariablesActions).getNodeCount() << " nodes)" + << std::endl; + } + return result; +} + +// As described in +// "Symbolic Algorithms for Graphs and Markov Decision Processes with Fairness Objectives" +// Slightly simplified we only care about the bottom scc +template +storm::dd::Bdd LockStepSearch_stats(storm::dd::Bdd const & states, // S + storm::dd::Bdd const & statesWithRemovedEdges, // T_S + storm::dd::Bdd const & transitionsWithoutActions, + std::set const & metaVariablesRow, + std::set const & metaVariablesColumn, + uint_fast64_t &countSymbolicOps) { + storm::dd::Bdd ts = storm::dd::Bdd(statesWithRemovedEdges); + std::unordered_map, storm::dd::Bdd> c{}; + while ( ! ts.isZero()) { + storm::dd::Bdd v = pick_stats(ts, countSymbolicOps); + ts &= ! v; + c[v] = storm::dd::Bdd(v); + } + + ts = storm::dd::Bdd(statesWithRemovedEdges); + while (true) { + for (auto it = c.cbegin(); it != c.cend(); ) { + storm::dd::Bdd t = storm::dd::Bdd(it->first); + storm::dd::Bdd ct = storm::dd::Bdd(it->second); + storm::dd::Bdd ctNew = ct || post_stats(ct, states, transitionsWithoutActions, metaVariablesRow, metaVariablesColumn, countSymbolicOps); + if ((ctNew && ts).getNonZeroCount() > 1) { // [rmnt] there was another state in T_S in the same SCC as t, so we can ignore t. + ts &= ! t; + c.erase(it++); + } else { + if (ctNew == ct) { + return ctNew; + } + c[t] = ctNew; + ++it; + } + } + } +} + +// As described in +// "Symbolic Algorithms for Graphs and Markov Decision Processes with Fairness Objectives" +// Uses a lockstep search +template +std::vector> symbolicMECDecompositionLockstep_stats(storm::dd::Bdd const & allStates, + storm::dd::Bdd const & transitionsWithActions, + std::set const & metaVariablesRow, + std::set const & metaVariablesColumn, + std::set const & metaVariablesActions, + std::vector> const & metaVariablesRowColumnPairs, + uint_fast64_t &countSymbolicOps) { + struct MecCandidate { + storm::dd::Bdd states; // In paper: S + storm::dd::Bdd statesWithRemovedEdge; // In Paper: T_s + }; + + // Helper function for better readability + auto hasAtLeastOneEdge_stats = + [metaVariablesActions, metaVariablesRow, metaVariablesColumn, metaVariablesRowColumnPairs] + (storm::dd::Bdd scc, storm::dd::Bdd transitionsWithActions, uint_fast64_t &countSymbolicOps) { + countSymbolicOps++; // [rmnt] For the exists abstract in the arguments + // Paper suggestion + return ! (post_stats(scc, scc, transitionsWithActions.existsAbstract(metaVariablesActions), metaVariablesRow, metaVariablesColumn, countSymbolicOps)).isZero(); + }; + + countSymbolicOps++; // [rmnt] exists + countSymbolicOps++; // [rmnt] getNonZeroCount + uint_fast64_t m = (transitionsWithActions.existsAbstract(metaVariablesActions) && allStates).getNonZeroCount(); + storm::dd::Bdd workingCopyTransitionsWithActions(transitionsWithActions); + std::vector> result{}; // In paper: "goodC" + std::stack mecCandidates{}; // In paper: X + countSymbolicOps++; // [rmnt] For the exists abstract in the arguments + for (const auto & scc : symbolicScc_stats::decomposition_stats(allStates, workingCopyTransitionsWithActions.existsAbstract(metaVariablesActions), metaVariablesRow, metaVariablesColumn, countSymbolicOps)) { + MecCandidate pair = { scc, scc.getDdManager().getBddZero() }; + mecCandidates.push(pair); + } + while ( ! mecCandidates.empty()) { + MecCandidate currentCandidate = mecCandidates.top(); + storm::dd::Bdd scc = currentCandidate.states; + storm::dd::Bdd sccTs = currentCandidate.statesWithRemovedEdge; + mecCandidates.pop(); + + storm::dd::Bdd sccROut = ROut_stats(scc, workingCopyTransitionsWithActions, metaVariablesColumn, metaVariablesRowColumnPairs, countSymbolicOps); + StateActionPair randomAttractor = computeRandomAttractor_stats(sccROut, scc, workingCopyTransitionsWithActions, metaVariablesColumn, metaVariablesActions, metaVariablesRowColumnPairs, countSymbolicOps); + scc &= ! randomAttractor.states; + workingCopyTransitionsWithActions &= ! randomAttractor.actions; + countSymbolicOps++; + sccTs = (sccTs || randomAttractor.actions.existsAbstract(metaVariablesActions)) && scc; + if (hasAtLeastOneEdge_stats(scc, workingCopyTransitionsWithActions, countSymbolicOps)) { + if (sccTs.isZero()) { + result.template emplace_back(scc); + } else if (sccTs.getNonZeroCount() >= sqrt(m)) { + countSymbolicOps++; // [rmnt] for the else if condition + countSymbolicOps++; // [rmnt] for the exists below + std::vector> subSccs = symbolicScc_stats::decomposition_stats( + scc, workingCopyTransitionsWithActions.existsAbstract(metaVariablesActions), metaVariablesRow, metaVariablesColumn, countSymbolicOps); + if (subSccs.size() == 1) { + result.template emplace_back(scc); + } else { + for (auto const& subScc : subSccs) { + MecCandidate toProcess = {subScc, scc.getDdManager().getBddZero()}; + mecCandidates.push(toProcess); + } + } + } else { + countSymbolicOps++; // [rmnt] for the else if condition + // bottomScc is "C" in paper + storm::dd::Bdd bottomScc = LockStepSearch_stats(scc, sccTs, + workingCopyTransitionsWithActions.existsAbstract(metaVariablesActions), + metaVariablesRow, metaVariablesColumn, countSymbolicOps); + if (hasAtLeastOneEdge_stats(bottomScc, workingCopyTransitionsWithActions, countSymbolicOps)) { + result.template emplace_back(bottomScc); + } + + countSymbolicOps++; // [rmnt] for the exists below + storm::dd::Bdd statesLeadingIntoBottomScc = pre_stats(bottomScc, scc, workingCopyTransitionsWithActions.existsAbstract(metaVariablesActions), metaVariablesRow, metaVariablesColumn, countSymbolicOps); + mecCandidates.emplace((MecCandidate) { + scc && ( ! bottomScc), + (scc && ( ! bottomScc)) && (statesLeadingIntoBottomScc || sccTs), + }); + } + } + } + return result; +} +} // namespace symbolicMEC_stats + +#endif \ No newline at end of file diff --git a/src/storm/storage/SymbolicOperations.h b/src/storm/storage/SymbolicOperations.h new file mode 100644 index 0000000000..872111a1d9 --- /dev/null +++ b/src/storm/storage/SymbolicOperations.h @@ -0,0 +1,67 @@ +#ifndef STORM_STORAGE_SYMBOLICOPERATIONS_H +#define STORM_STORAGE_SYMBOLICOPERATIONS_H + +#include "storm/storage/dd/Add.h" +#include "storm/storage/dd/Bdd.h" +#include "storm/storage/expressions/SimpleValuation.h" + +template +static storm::dd::Bdd pick(storm::dd::Bdd const & states) { + assert (states.getNonZeroCount() > 0); + storm::dd::DdManager const & manager = states.getDdManager(); + storm::dd::Add add = states.template toAdd(); + storm::expressions::SimpleValuation firstNonZeroAssigned = (*add.begin()).first; + storm::dd::Bdd result = manager.getBddOne(); + for (auto && variable : add.getContainedMetaVariables()) { + // Get Value to encode + int_fast64_t value = 0; + { + // variable is either boolean, integer or rational + storm::expressions::Type variableType = variable.getType(); + if (variableType.isBooleanType()) { + value = (int_fast64_t)firstNonZeroAssigned.getBooleanValue(variable); + } else if (variableType.isIntegerType()) { + value = firstNonZeroAssigned.getIntegerValue(variable); + } else { + // How do I even convert this to int_fast64_t for the 'getEncoding'-call? + assert( ! "Unexpected variable type" ); + } + } + + // Copy value encoding of meta variable onto BDD + result &= manager.getEncoding(variable, value); + } + assert (result.getNonZeroCount() == 1); + return result; +} + +// [rmnt] Adding new pick version to see if it's faster. +template +static storm::dd::Bdd pickv2(storm::dd::Bdd const & states) { + assert (! states.isZero()); + storm::dd::Bdd result = states.existsAbstractRepresentative(states.getContainedMetaVariables()); + assert (result.getNonZeroCount() == 1); + return result; +} + +// NOTE(Felix): Modified from dd.cpp:computeReachableStates +template +static storm::dd::Bdd post(storm::dd::Bdd const & statesToApplyPostOn, + storm::dd::Bdd const & allStates, + storm::dd::Bdd const & transitions, + std::set const & metaVariablesRow, + std::set const & metaVariablesColumn) { + return allStates && statesToApplyPostOn.relationalProduct(transitions, metaVariablesRow, metaVariablesColumn); +} + +// NOTE(Felix): Modified from dd.cpp:computeBackwardsReachableStates +template +static storm::dd::Bdd pre(storm::dd::Bdd const & statesToApplyPreOn, + storm::dd::Bdd const & allStates, + storm::dd::Bdd const & transitions, + std::set const & metaVariablesRow, + std::set const & metaVariablesColumn) { + return allStates && statesToApplyPreOn.inverseRelationalProduct(transitions, metaVariablesRow, metaVariablesColumn); +} + +#endif \ No newline at end of file diff --git a/src/storm/storage/SymbolicOperations_stats.h b/src/storm/storage/SymbolicOperations_stats.h new file mode 100644 index 0000000000..9c31a957a6 --- /dev/null +++ b/src/storm/storage/SymbolicOperations_stats.h @@ -0,0 +1,73 @@ +#ifndef STORM_STORAGE_SYMBOLICOPERATIONS_STATS_H +#define STORM_STORAGE_SYMBOLICOPERATIONS_STATS_H + +#include "storm/storage/dd/Add.h" +#include "storm/storage/dd/Bdd.h" +#include "storm/storage/expressions/SimpleValuation.h" + +template +static storm::dd::Bdd pick_stats(storm::dd::Bdd const & states, uint_fast64_t &countSymbolicOps) { + assert (states.getNonZeroCount() > 0); + countSymbolicOps++; // [rmnt] TODO : Counting each pick as one symbolic op. Ok? + storm::dd::DdManager const & manager = states.getDdManager(); + storm::dd::Add add = states.template toAdd(); + storm::expressions::SimpleValuation firstNonZeroAssigned = (*add.begin()).first; + storm::dd::Bdd result = manager.getBddOne(); + for (auto && variable : add.getContainedMetaVariables()) { + // Get Value to encode + int_fast64_t value = 0; + { + // variable is either boolean, integer or rational + storm::expressions::Type variableType = variable.getType(); + if (variableType.isBooleanType()) { + value = (int_fast64_t)firstNonZeroAssigned.getBooleanValue(variable); + } else if (variableType.isIntegerType()) { + value = firstNonZeroAssigned.getIntegerValue(variable); + } else { + // How do I even convert this to int_fast64_t for the 'getEncoding'-call? + assert( ! "Unexpected variable type" ); + } + } + + // Copy value encoding of meta variable onto BDD + result &= manager.getEncoding(variable, value); + } + assert (result.getNonZeroCount() == 1); + return result; +} + +// [rmnt] Adding new pick version to see if it's faster. +template +static storm::dd::Bdd pickv2_stats(storm::dd::Bdd const & states, uint_fast64_t &countSymbolicOps) { + assert (! states.isZero()); + countSymbolicOps++; // [rmnt] TODO : Counting each pick as one symbolic op. Ok? + storm::dd::Bdd result = states.existsAbstractRepresentative(states.getContainedMetaVariables()); + assert (result.getNonZeroCount() == 1); + return result; +} + +// NOTE(Felix): Modified from dd.cpp:computeReachableStates +template +static storm::dd::Bdd post_stats(storm::dd::Bdd const & statesToApplyPostOn, + storm::dd::Bdd const & allStates, + storm::dd::Bdd const & transitions, + std::set const & metaVariablesRow, + std::set const & metaVariablesColumn, + uint_fast64_t &countSymbolicOps) { + countSymbolicOps++; // [rmnt] TODO : Counting each post as one symbolic op. Ok? + return allStates && statesToApplyPostOn.relationalProduct(transitions, metaVariablesRow, metaVariablesColumn); +} + +// NOTE(Felix): Modified from dd.cpp:computeBackwardsReachableStates +template +static storm::dd::Bdd pre_stats(storm::dd::Bdd const & statesToApplyPreOn, + storm::dd::Bdd const & allStates, + storm::dd::Bdd const & transitions, + std::set const & metaVariablesRow, + std::set const & metaVariablesColumn, + uint_fast64_t &countSymbolicOps) { + countSymbolicOps++; // [rmnt] TODO : Counting each pre as one symbolic op. Ok? + return allStates && statesToApplyPreOn.inverseRelationalProduct(transitions, metaVariablesRow, metaVariablesColumn); +} + +#endif \ No newline at end of file diff --git a/src/storm/storage/SymbolicSCCDecomposition.h b/src/storm/storage/SymbolicSCCDecomposition.h new file mode 100644 index 0000000000..ef758d5bd8 --- /dev/null +++ b/src/storm/storage/SymbolicSCCDecomposition.h @@ -0,0 +1,113 @@ +#ifndef STORM_STORAGE_SYMBOLICSCCDECOMPOSITION_H +#define STORM_STORAGE_SYMBOLICSCCDECOMPOSITION_H + +#include +#include "storm/storage/SymbolicOperations.h" + +namespace symbolicSCC { + +template +struct TaskEntry { + storm::dd::Bdd states; + storm::dd::Bdd s; + storm::dd::Bdd node; +}; + +/* Ported from the paper + * "Computing Strongly Connected Components in a Number of Symbolic Steps" + * Modified to not use recursion, but a queue instead + * (Gentilini, Piazza, Policriti) */ +template +static std::vector> decomposition(storm::dd::Bdd const& allStates, storm::dd::Bdd const& transitions, + std::set const& metaVariablesRow, + std::set const& metaVariablesColumn) { + std::vector> result = {}; + if (allStates.isZero()) { return result; } + std::stack> workQueue; + { + TaskEntry initialTask = {allStates, allStates.getDdManager().getBddZero(), allStates.getDdManager().getBddZero()}; + workQueue.push(initialTask); + } + + // Work through tasks + while (!workQueue.empty()) { + TaskEntry currentTask = workQueue.top(); + workQueue.pop(); + assert( ! currentTask.states.isZero()); + + // "Determine the node for which the scc is computed" + if (currentTask.node.isZero() && currentTask.s.isZero()) { // Modified to allow for specification of a starting vertex + currentTask.node = pick(currentTask.states); + } + + // "Compute the forward-set of the vertex in NODE together with a skeleton" + storm::dd::Bdd fw = allStates.getDdManager().getBddZero(); + storm::dd::Bdd newS; + storm::dd::Bdd newNode; + { + // Inlined Skel_Forward function + + // "Compute the Forward-set and push onto STACK the onion rings" + std::stack> stack; + storm::dd::Bdd level = storm::dd::Bdd(currentTask.node); + while (!level.isZero()) { + stack.push(level); + fw |= level; + level = (!fw) && post(level, currentTask.states, transitions, metaVariablesRow, metaVariablesColumn); + } + + // "Determine a Skeleton of the Forward-Set" + level = stack.top(); + stack.pop(); + newNode = pick(level); // TODO: Better Name + newS = storm::dd::Bdd(newNode); // TODO: Better name for this variable + while (!stack.empty()) { + level = stack.top(); + stack.pop(); + storm::dd::Bdd toPickFrom = level && pre(newS, currentTask.states, transitions, metaVariablesRow, metaVariablesColumn); + newS |= pick(toPickFrom); + } + } + + // "Determine the scc containing NODE" + storm::dd::Bdd scc = storm::dd::Bdd(currentTask.node); + { + bool changed = true; + while (changed) { + storm::dd::Bdd updatedScc = fw && pre(scc, currentTask.states, transitions, metaVariablesRow, metaVariablesColumn); + storm::dd::Bdd addedStates = updatedScc && (!scc); + scc |= updatedScc; + changed = (!addedStates.isZero()); + } + } + + // "Insert the scc in the scc Partition" + result.push_back(scc); + + // "First recursive call: Computation of the scc's in V \ FW" + { + storm::dd::Bdd sToCheck = currentTask.s && (!scc); + TaskEntry newTask = { + currentTask.states && (!fw), + sToCheck, + sToCheck && pre(scc && currentTask.s, currentTask.states, transitions, metaVariablesRow, metaVariablesColumn), + }; + if ( ! newTask.states.isZero()) { workQueue.push(newTask); } + } + + // "Second recursive call : Computation of the scc's in FW \ SCC" + { + TaskEntry newTask = { + fw && (!scc), + newS && (!scc), + newNode && (!scc), + }; + if ( ! newTask.states.isZero()) { workQueue.push(newTask); } + } + } + return result; +} + +} // namespace symbolicSCC + +#endif diff --git a/src/storm/storage/SymbolicSCCDecomposition_stats.h b/src/storm/storage/SymbolicSCCDecomposition_stats.h new file mode 100644 index 0000000000..57801b8f89 --- /dev/null +++ b/src/storm/storage/SymbolicSCCDecomposition_stats.h @@ -0,0 +1,114 @@ +#ifndef STORM_STORAGE_SYMBOLICSCCDECOMPOSITION_STATS_H +#define STORM_STORAGE_SYMBOLICSCCDECOMPOSITION_STATS_H + +#include +#include "storm/storage/SymbolicOperations_stats.h" + +namespace symbolicSCC_stats { + +template +struct TaskEntry { + storm::dd::Bdd states; + storm::dd::Bdd s; + storm::dd::Bdd node; +}; + +/* Ported from the paper + * "Computing Strongly Connected Components in a Number of Symbolic Steps" + * Modified to not use recursion, but a queue instead + * (Gentilini, Piazza, Policriti) */ +template +static std::vector> decomposition_stats(storm::dd::Bdd const& allStates, storm::dd::Bdd const& transitions, + std::set const& metaVariablesRow, + std::set const& metaVariablesColumn, + uint_fast64_t &countSymbolicOps) { + std::vector> result = {}; + if (allStates.isZero()) { return result; } + std::stack> workQueue; + { + TaskEntry initialTask = {allStates, allStates.getDdManager().getBddZero(), allStates.getDdManager().getBddZero()}; + workQueue.push(initialTask); + } + + // Work through tasks + while (!workQueue.empty()) { + TaskEntry currentTask = workQueue.top(); + workQueue.pop(); + assert( ! currentTask.states.isZero()); + + // "Determine the node for which the scc is computed" + if (currentTask.node.isZero() && currentTask.s.isZero()) { // Modified to allow for specification of a starting vertex + currentTask.node = pick_stats(currentTask.states, countSymbolicOps); + } + + // "Compute the forward-set of the vertex in NODE together with a skeleton" + storm::dd::Bdd fw = allStates.getDdManager().getBddZero(); + storm::dd::Bdd newS; + storm::dd::Bdd newNode; + { + // Inlined Skel_Forward function + + // "Compute the Forward-set and push onto STACK the onion rings" + std::stack> stack; + storm::dd::Bdd level = storm::dd::Bdd(currentTask.node); + while (!level.isZero()) { + stack.push(level); + fw |= level; + level = (!fw) && post_stats(level, currentTask.states, transitions, metaVariablesRow, metaVariablesColumn, countSymbolicOps); + } + + // "Determine a Skeleton of the Forward-Set" + level = stack.top(); + stack.pop(); + newNode = pick_stats(level, countSymbolicOps); // TODO: Better Name + newS = storm::dd::Bdd(newNode); // TODO: Better name for this variable + while (!stack.empty()) { + level = stack.top(); + stack.pop(); + storm::dd::Bdd toPickFrom = level && pre_stats(newS, currentTask.states, transitions, metaVariablesRow, metaVariablesColumn, countSymbolicOps); + newS |= pick_stats(toPickFrom, countSymbolicOps); + } + } + + // "Determine the scc containing NODE" + storm::dd::Bdd scc = storm::dd::Bdd(currentTask.node); + { + bool changed = true; + while (changed) { + storm::dd::Bdd updatedScc = fw && pre_stats(scc, currentTask.states, transitions, metaVariablesRow, metaVariablesColumn, countSymbolicOps); + storm::dd::Bdd addedStates = updatedScc && (!scc); + scc |= updatedScc; + changed = (!addedStates.isZero()); + } + } + + // "Insert the scc in the scc Partition" + result.push_back(scc); + + // "First recursive call: Computation of the scc's in V \ FW" + { + storm::dd::Bdd sToCheck = currentTask.s && (!scc); + TaskEntry newTask = { + currentTask.states && (!fw), + sToCheck, + sToCheck && pre_stats(scc && currentTask.s, currentTask.states, transitions, metaVariablesRow, metaVariablesColumn, countSymbolicOps), + }; + if ( ! newTask.states.isZero()) { workQueue.push(newTask); } + } + + // "Second recursive call : Computation of the scc's in FW \ SCC" + { + TaskEntry newTask = { + fw && (!scc), + newS && (!scc), + newNode && (!scc), + }; + if ( ! newTask.states.isZero()) { workQueue.push(newTask); } + } + } + return result; +} + +} // namespace symbolicSCC_stats + +#endif \ No newline at end of file diff --git a/src/storm/storage/THESIS_DEBUG.h b/src/storm/storage/THESIS_DEBUG.h index 0432f30f74..41292b00e3 100644 --- a/src/storm/storage/THESIS_DEBUG.h +++ b/src/storm/storage/THESIS_DEBUG.h @@ -1,13 +1,13 @@ -#pragma once - -#ifndef STORM_THESIS_DEBUG_H -#define STORM_THESIS_DEBUG_H +#ifndef STORM_STORAGE_THESIS_DEBUG_H +#define STORM_STORAGE_THESIS_DEBUG_H #include "storm/storage/dd/DdType.h" #include "storm/models/Model.h" #include "storm/models/symbolic/NondeterministicModel.h" #include "storm/utility/macros.h" #include "storm/utility/Stopwatch.h" +#include "storm/storage/SymbolicMEC.h" +#include "storm/storage/SymbolicMEC_stats.h" #include @@ -81,12 +81,13 @@ BenchmarkResult doSymbolicBenchmark(storm::models::symbolic::NondeterministicMod std::vector> mecs; std::chrono::high_resolution_clock::time_point decompositionTimestampStart; std::chrono::high_resolution_clock::time_point decompositionTimestampEnd; + uint_fast64_t countSymbolicOps = 0; switch (type) { case MecBenchmarkType::NAIVE: decompositionTimestampStart = std::chrono::high_resolution_clock::now(); - mecs = symbolicMEC::symbolicMECDecompositionBasic( + mecs = symbolicMEC::symbolicMECDecompositionNaive( symbolicModel.getReachableStates(), symbolicModel.getTransitionMatrix().toBDD(), symbolicModel.getRowVariables(), symbolicModel.getColumnVariables(), symbolicModel.getNondeterminismVariables(), symbolicModel.getRowColumnMetaVariablePairs() @@ -96,16 +97,17 @@ BenchmarkResult doSymbolicBenchmark(storm::models::symbolic::NondeterministicMod case MecBenchmarkType::NAIVE_STATS: decompositionTimestampStart = std::chrono::high_resolution_clock::now(); - mecs = symbolicMEC_EBA::symbolicMECDecompositionBasic_stats( + mecs = symbolicMEC_stats::symbolicMECDecompositionNaive_stats( symbolicModel.getReachableStates(), symbolicModel.getTransitionMatrix().toBdd(), symbolicModel.getRowVariables(), symbolicModel.getColumnVariables(), symbolicModel.getNondeterminismVariables(), - symbolicModel.getRowColumnMetaVariablePairs()); + symbolicModel.getRowColumnMetaVariablePairs(), countSymbolicOps); decompositionTimestampEnd = std::chrono::high_resolution_clock::now(); + std::cout << "DEBUG SYMBOLIC OPS " << countSymbolicOps << std::endl; break; case MecBenchmarkType::LOCKSTEP: decompositionTimestampStart = std::chrono::high_resolution_clock::now(); - mecs = symbolicMEC_EBA::symbolicMECDecompositionLockstep( + mecs = symbolicMEC::symbolicMECDecompositionLockstep( symbolicModel.getReachableStates(), symbolicModel.getTransitionMatrix().toBdd(), symbolicModel.getRowVariables(), symbolicModel.getColumnVariables(), symbolicModel.getNondeterminismVariables(), symbolicModel.getRowColumnMetaVariablePairs()); @@ -114,16 +116,17 @@ BenchmarkResult doSymbolicBenchmark(storm::models::symbolic::NondeterministicMod case MecBenchmarkType::LOCKSTEP_STATS: decompositionTimestampStart = std::chrono::high_resolution_clock::now(); - mecs = symbolicMEC_EBA::symbolicMECDecompositionLockstep_stats( + mecs = symbolicMEC_stats::symbolicMECDecompositionLockstep_stats( symbolicModel.getReachableStates(), symbolicModel.getTransitionMatrix().toBdd(), symbolicModel.getRowVariables(), symbolicModel.getColumnVariables(), symbolicModel.getNondeterminismVariables(), - symbolicModel.getRowColumnMetaVariablePairs()); + symbolicModel.getRowColumnMetaVariablePairs(), countSymbolicOps); decompositionTimestampEnd = std::chrono::high_resolution_clock::now(); + std::cout << "DEBUG SYMBOLIC OPS " << countSymbolicOps << std::endl; break; case MecBenchmarkType::INTERLEAVE: decompositionTimestampStart = std::chrono::high_resolution_clock::now(); - mecs = symbolicMEC_EBA::symbolicMECDecompositionInterleave( + mecs = symbolicMEC::symbolicMECDecompositionInterleave( symbolicModel.getReachableStates(), symbolicModel.getTransitionMatrix().toBdd(), symbolicModel.getRowVariables(), symbolicModel.getColumnVariables(), symbolicModel.getNondeterminismVariables(), symbolicModel.getRowColumnMetaVariablePairs()); @@ -132,10 +135,11 @@ BenchmarkResult doSymbolicBenchmark(storm::models::symbolic::NondeterministicMod case MecBenchmarkType::INTERLEAVE_STATS: decompositionTimestampStart = std::chrono::high_resolution_clock::now(); - mecs = symbolicMEC_EBA::symbolicMECDecompositionInterleave_stats( + mecs = symbolicMEC_stats::symbolicMECDecompositionInterleave_stats( symbolicModel.getReachableStates(), symbolicModel.getTransitionMatrix().toBdd(), symbolicModel.getRowVariables(), symbolicModel.getColumnVariables(), symbolicModel.getNondeterminismVariables(), - symbolicModel.getRowColumnMetaVariablePairs()); + symbolicModel.getRowColumnMetaVariablePairs(), countSymbolicOps); + std::cout << "DEBUG SYMBOLIC OPS " << countSymbolicOps << std::endl; decompositionTimestampEnd = std::chrono::high_resolution_clock::now(); break; diff --git a/src/storm/storage/dd/Bdd.cpp b/src/storm/storage/dd/Bdd.cpp index ea56ce91d4..fe1f617ade 100644 --- a/src/storm/storage/dd/Bdd.cpp +++ b/src/storm/storage/dd/Bdd.cpp @@ -187,6 +187,13 @@ Bdd Bdd::existsAbstractRepresentative(std::set(this->getDdManager(), internalBdd.existsAbstractRepresentative(cube.getInternalBdd()), this->getContainedMetaVariables()); } +// [rmnt] +template +Bdd Bdd::pickOneCube() const { + return Bdd(this->getDdManager(), internalBdd.pickOneCube(), this->getDdManager().getAllMetaVariables()) + // [rmnt] TODO : Is getAllMetaVariables() the right choice? +} + template Bdd Bdd::universalAbstract(std::set const& metaVariables) const { Bdd cube = getCube(this->getDdManager(), metaVariables); diff --git a/src/storm/storage/dd/Bdd.h b/src/storm/storage/dd/Bdd.h index a221e2bbe0..b9f82992a9 100644 --- a/src/storm/storage/dd/Bdd.h +++ b/src/storm/storage/dd/Bdd.h @@ -207,6 +207,14 @@ class Bdd : public Dd { */ Bdd existsAbstractRepresentative(std::set const& metaVariables) const; + /*! + * [rmnt] + * Gets a cube that satisfies this Bdd. + * + * @return The BDD representing the cube. + */ + Bdd pickOneCube() const; + /*! * Universally abstracts from the given meta variables. * diff --git a/src/storm/storage/dd/cudd/InternalCuddBdd.cpp b/src/storm/storage/dd/cudd/InternalCuddBdd.cpp index b1f8e1fb3a..d0a1750320 100644 --- a/src/storm/storage/dd/cudd/InternalCuddBdd.cpp +++ b/src/storm/storage/dd/cudd/InternalCuddBdd.cpp @@ -128,6 +128,18 @@ InternalBdd InternalBdd::existsAbstractRepresentativ return InternalBdd(ddManager, this->getCuddBdd().ExistAbstractRepresentative(cube.getCuddBdd())); } +// [rmnt] +InternalBdd InternalBdd::pickOneCube() const { + int numVars = ddManager->getCuddManager().ReadSize(); + std::vector varBdds; + // [rmnt] TODO : Does the order of pushing vars matter to perfornance? + // [rmnt] See the implementation of Cudd_Support() in cuddUtil.c where this is done in reverse order + for(int index = 0; index < numVars; ++index) { + varBdds.push_back(ddManager->getCuddManager().bddVar(index)); + } + return InternalBdd(ddManager, this->getCuddBdd().PickOneMinterm(varBdds)); +} + InternalBdd InternalBdd::universalAbstract(InternalBdd const& cube) const { return InternalBdd(ddManager, this->getCuddBdd().UnivAbstract(cube.getCuddBdd())); } diff --git a/src/storm/storage/dd/cudd/InternalCuddBdd.h b/src/storm/storage/dd/cudd/InternalCuddBdd.h index 60061e9037..38266a0033 100644 --- a/src/storm/storage/dd/cudd/InternalCuddBdd.h +++ b/src/storm/storage/dd/cudd/InternalCuddBdd.h @@ -224,6 +224,14 @@ class InternalBdd { */ InternalBdd existsAbstractRepresentative(InternalBdd const& cube) const; + /*! + * [rmnt] + * Gets a cube that satisfies this Bdd. + * + * @return The BDD representing the cube. + */ + InternalBdd pickOneCube() const; + /*! * Universally abstracts from the given cube. * diff --git a/src/storm/storage/dd/sylvan/InternalSylvanBdd.cpp b/src/storm/storage/dd/sylvan/InternalSylvanBdd.cpp index 7571eb672b..11ef26403f 100644 --- a/src/storm/storage/dd/sylvan/InternalSylvanBdd.cpp +++ b/src/storm/storage/dd/sylvan/InternalSylvanBdd.cpp @@ -176,6 +176,11 @@ InternalBdd InternalBdd::existsAbstractRepresent return InternalBdd(ddManager, this->sylvanBdd.ExistAbstractRepresentative(cube.sylvanBdd)); } +// [rmnt] +InternalBdd InternalBdd::pickOneCube() const { + return InternalBdd(ddManager, this->sylvanBdd.PickOneCube()); +} + InternalBdd InternalBdd::universalAbstract(InternalBdd const& cube) const { return InternalBdd(ddManager, this->sylvanBdd.UnivAbstract(cube.sylvanBdd)); } diff --git a/src/storm/storage/dd/sylvan/InternalSylvanBdd.h b/src/storm/storage/dd/sylvan/InternalSylvanBdd.h index 27733e2b4e..2b1235b445 100644 --- a/src/storm/storage/dd/sylvan/InternalSylvanBdd.h +++ b/src/storm/storage/dd/sylvan/InternalSylvanBdd.h @@ -215,6 +215,14 @@ class InternalBdd { */ InternalBdd existsAbstractRepresentative(InternalBdd const& cube) const; + /*! + * [rmnt] + * Gets a cube that satisfies this Bdd. + * + * @return The BDD representing the cube. + */ + InternalBdd pickOneCube() const; + /*! * Universally abstracts from the given cube. * From ef508f5bd8cf2bbda844ecefb1ca55e789a3a247 Mon Sep 17 00:00:00 2001 From: Ramneet Singh Date: Fri, 14 Jun 2024 13:08:31 +0530 Subject: [PATCH 05/25] Fix Bdd.cpp bug | Add placeholders for Interlave impls --- src/storm/storage/SymbolicMEC.h | 10 ++++++++++ src/storm/storage/SymbolicMEC_stats.h | 13 +++++++++++++ src/storm/storage/dd/Bdd.cpp | 2 +- 3 files changed, 24 insertions(+), 1 deletion(-) diff --git a/src/storm/storage/SymbolicMEC.h b/src/storm/storage/SymbolicMEC.h index 3983ada952..b4b294d596 100644 --- a/src/storm/storage/SymbolicMEC.h +++ b/src/storm/storage/SymbolicMEC.h @@ -231,6 +231,16 @@ std::vector> symbolicMECDecompositionLockstep(storm::dd::Bd return result; } +template +std::vector> symbolicMECDecompositionInterleave(storm::dd::Bdd const & allStates, + storm::dd::Bdd const & transitionsWithActions, + std::set const & metaVariablesRow, + std::set const & metaVariablesColumn, + std::set const & metaVariablesActions, + std::vector> const & metaVariablesRowColumnPairs) { + return std::vector{}; +} + } // namespace symbolicMEC #endif \ No newline at end of file diff --git a/src/storm/storage/SymbolicMEC_stats.h b/src/storm/storage/SymbolicMEC_stats.h index 98afbb4381..b11749b5fa 100644 --- a/src/storm/storage/SymbolicMEC_stats.h +++ b/src/storm/storage/SymbolicMEC_stats.h @@ -257,6 +257,19 @@ std::vector> symbolicMECDecompositionLockstep_stats(storm:: } return result; } + + +template +std::vector> symbolicMECDecompositionInterleave_stats(storm::dd::Bdd const & allStates, + storm::dd::Bdd const & transitionsWithActions, + std::set const & metaVariablesRow, + std::set const & metaVariablesColumn, + std::set const & metaVariablesActions, + std::vector> const & metaVariablesRowColumnPairs, + uint_fast64_t &countSymbolicOps) { + return std::vector{} + } + } // namespace symbolicMEC_stats #endif \ No newline at end of file diff --git a/src/storm/storage/dd/Bdd.cpp b/src/storm/storage/dd/Bdd.cpp index fe1f617ade..1d358b8984 100644 --- a/src/storm/storage/dd/Bdd.cpp +++ b/src/storm/storage/dd/Bdd.cpp @@ -190,7 +190,7 @@ Bdd Bdd::existsAbstractRepresentative(std::set Bdd Bdd::pickOneCube() const { - return Bdd(this->getDdManager(), internalBdd.pickOneCube(), this->getDdManager().getAllMetaVariables()) + return Bdd(this->getDdManager(), internalBdd.pickOneCube(), this->getDdManager().getAllMetaVariables()); // [rmnt] TODO : Is getAllMetaVariables() the right choice? } From 542fcbbade374e2719c20508fbaa7bc48984bfa4 Mon Sep 17 00:00:00 2001 From: Ramneet Singh Date: Fri, 14 Jun 2024 13:42:12 +0530 Subject: [PATCH 06/25] Fix bug in model-handling.h --- src/storm-cli-utilities/model-handling.h | 19 ++++++++++--------- 1 file changed, 10 insertions(+), 9 deletions(-) diff --git a/src/storm-cli-utilities/model-handling.h b/src/storm-cli-utilities/model-handling.h index 7851b43334..e29a8fc221 100644 --- a/src/storm-cli-utilities/model-handling.h +++ b/src/storm-cli-utilities/model-handling.h @@ -513,21 +513,22 @@ std::shared_ptr buildModel(SymbolicInput const& input, } else if (builderType == storm::builder::BuilderType::Explicit) { result = buildModelSparse(input, buildSettings); } + + // THESIS DATA GATHERING [rmnt] - Benchmarking the Symbolic MEC decomposition algorithms. Entry point. + uint64_t DEBUG_THESIS_BENCHMARK = storm::settings::getModule().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((storm::models::ModelBase const &)*result, DEBUG_THESIS_BENCHMARK); + exit(0); + } + } 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."); result = buildModelExplicit(ioSettings, buildSettings); } - // THESIS DATA GATHERING [rmnt] - Benchmarking the Symbolic MEC decomposition algorithms. Entry point. - uint64_t DEBUG_THESIS_BENCHMARK = storm::settings::getModule().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((storm::models::ModelBase const &)*result, DEBUG_THESIS_BENCHMARK); - exit(0); - } - modelBuildingWatch.stop(); if (result) { STORM_PRINT("Time for model construction: " << modelBuildingWatch << ".\n\n"); From db0064157108af0451ee52f235e10cdd672dc045 Mon Sep 17 00:00:00 2001 From: Ramneet Singh Date: Fri, 14 Jun 2024 13:44:58 +0530 Subject: [PATCH 07/25] Add THESIS_DEBUG include to model-handling --- src/storm-cli-utilities/model-handling.h | 2 ++ 1 file changed, 2 insertions(+) diff --git a/src/storm-cli-utilities/model-handling.h b/src/storm-cli-utilities/model-handling.h index e29a8fc221..89d77d4593 100644 --- a/src/storm-cli-utilities/model-handling.h +++ b/src/storm-cli-utilities/model-handling.h @@ -51,6 +51,8 @@ #include "storm/utility/Stopwatch.h" +#include "storm/storage/THESIS_DEBUG.h" + namespace storm { namespace cli { From e1f54bbdf1625708f5e4b690ef17415326bc1ee2 Mon Sep 17 00:00:00 2001 From: Ramneet Singh Date: Fri, 14 Jun 2024 13:49:07 +0530 Subject: [PATCH 08/25] Fix Syntax Bugs --- src/storm/storage/SymbolicMEC_stats.h | 2 +- src/storm/storage/THESIS_DEBUG.h | 2 +- 2 files changed, 2 insertions(+), 2 deletions(-) diff --git a/src/storm/storage/SymbolicMEC_stats.h b/src/storm/storage/SymbolicMEC_stats.h index b11749b5fa..18526c4244 100644 --- a/src/storm/storage/SymbolicMEC_stats.h +++ b/src/storm/storage/SymbolicMEC_stats.h @@ -267,7 +267,7 @@ std::vector> symbolicMECDecompositionInterleave_stats(storm std::set const & metaVariablesActions, std::vector> const & metaVariablesRowColumnPairs, uint_fast64_t &countSymbolicOps) { - return std::vector{} + return std::vector{}; } } // namespace symbolicMEC_stats diff --git a/src/storm/storage/THESIS_DEBUG.h b/src/storm/storage/THESIS_DEBUG.h index 41292b00e3..be9138d1a8 100644 --- a/src/storm/storage/THESIS_DEBUG.h +++ b/src/storm/storage/THESIS_DEBUG.h @@ -88,7 +88,7 @@ BenchmarkResult doSymbolicBenchmark(storm::models::symbolic::NondeterministicMod case MecBenchmarkType::NAIVE: decompositionTimestampStart = std::chrono::high_resolution_clock::now(); mecs = symbolicMEC::symbolicMECDecompositionNaive( - symbolicModel.getReachableStates(), symbolicModel.getTransitionMatrix().toBDD(), + symbolicModel.getReachableStates(), symbolicModel.getTransitionMatrix().toBdd(), symbolicModel.getRowVariables(), symbolicModel.getColumnVariables(), symbolicModel.getNondeterminismVariables(), symbolicModel.getRowColumnMetaVariablePairs() ); From e3811d8b1b4f1e1e29685abc854e6d7dd08717c4 Mon Sep 17 00:00:00 2001 From: Ramneet Singh Date: Fri, 14 Jun 2024 14:31:10 +0530 Subject: [PATCH 09/25] Fix Felix Typing Bug in isTrivialSCCWithoutSelfEdge --- src/storm/storage/SymbolicMEC.h | 23 +++++++++++++---------- src/storm/storage/SymbolicMEC_stats.h | 25 ++++++++++++++----------- 2 files changed, 27 insertions(+), 21 deletions(-) diff --git a/src/storm/storage/SymbolicMEC.h b/src/storm/storage/SymbolicMEC.h index b4b294d596..cac6b6cd8a 100644 --- a/src/storm/storage/SymbolicMEC.h +++ b/src/storm/storage/SymbolicMEC.h @@ -21,14 +21,17 @@ struct StateActionPair { } }; +// [rmnt] Changed type of scc argument because the earlier one was giving a compiler error. +// [rmnt] TODO review this function, seems shady. template -static bool isTrivialSccWithoutSelfEdge(StateActionPair const & scc, +static bool isTrivialSccWithoutSelfEdge(storm::dd::Bdd const & scc, storm::dd::Bdd const & transitionsWithActions, std::vector> const & metaVariablesRowColumnPairs) { - bool isTrivialScc = (1 == scc.states.getNonZeroCount()); - // [rmnt] TODO : Review the noSelfEdge condition. Do you need && scc.states also? - bool noSelfEdge = (transitionsWithActions && scc.actions && scc.states.swapVariables(metaVariablesRowColumnPairs)).isZero(); - return (isTrivialScc && noSelfEdge); + bool isTrivialScc = (1 == scc.getNonZeroCount()); // [rmnt] TODO : Check if this should be counted as a symbolic op + if (! isTrivialScc) + return false; + bool noSelfEdge = (transitionsWithActions && scc && scc.swapVariables(metaVariablesRowColumnPairs)).isZero(); + return noSelfEdge; } @@ -91,7 +94,7 @@ std::vector> symbolicMECDecompositionNaive(storm::dd::Bdd workingCopyTransitionsWithActions(transitionsWithActions); std::vector> result{}; std::stack> mecCandidates{}; - for (const auto& scc : symbolicScc::decomposition(allStates, workingCopyTransitionsWithActions.existsAbstract(metaVariablesActions), + for (const auto& scc : symbolicSCC::decomposition(allStates, workingCopyTransitionsWithActions.existsAbstract(metaVariablesActions), metaVariablesRow, metaVariablesColumn)) { mecCandidates.push(scc); } @@ -109,7 +112,7 @@ std::vector> symbolicMECDecompositionNaive(storm::dd::Bdd attractor = computeRandomAttractor(sccROut, scc, workingCopyTransitionsWithActions, metaVariablesColumn, metaVariablesActions, metaVariablesRowColumnPairs); workingCopyTransitionsWithActions &= !attractor.actions; - for (auto const& subScc : symbolicScc::decomposition( + for (auto const& subScc : symbolicSCC::decomposition( scc && !attractor.states, workingCopyTransitionsWithActions.existsAbstract(metaVariablesActions), metaVariablesRow, metaVariablesColumn)) { mecCandidates.push(subScc); } @@ -182,7 +185,7 @@ std::vector> symbolicMECDecompositionLockstep(storm::dd::Bd storm::dd::Bdd workingCopyTransitionsWithActions(transitionsWithActions); std::vector> result{}; // In paper: "goodC" std::stack mecCandidates{}; // In paper: X - for (const auto & scc : symbolicScc::decomposition(allStates, workingCopyTransitionsWithActions.existsAbstract(metaVariablesActions), metaVariablesRow, metaVariablesColumn)) { + for (const auto & scc : symbolicSCC::decomposition(allStates, workingCopyTransitionsWithActions.existsAbstract(metaVariablesActions), metaVariablesRow, metaVariablesColumn)) { MecCandidate pair = { scc, scc.getDdManager().getBddZero() }; mecCandidates.push(pair); } @@ -201,7 +204,7 @@ std::vector> symbolicMECDecompositionLockstep(storm::dd::Bd if (sccTs.isZero()) { result.template emplace_back(scc); } else if (sccTs.getNonZeroCount() >= sqrt(m)) { - std::vector> subSccs = symbolicScc::decomposition( + std::vector> subSccs = symbolicSCC::decomposition( scc, workingCopyTransitionsWithActions.existsAbstract(metaVariablesActions), metaVariablesRow, metaVariablesColumn); if (subSccs.size() == 1) { result.template emplace_back(scc); @@ -238,7 +241,7 @@ std::vector> symbolicMECDecompositionInterleave(storm::dd:: std::set const & metaVariablesColumn, std::set const & metaVariablesActions, std::vector> const & metaVariablesRowColumnPairs) { - return std::vector{}; + return std::vector< storm::dd::Bdd > {}; } } // namespace symbolicMEC diff --git a/src/storm/storage/SymbolicMEC_stats.h b/src/storm/storage/SymbolicMEC_stats.h index 18526c4244..c35b06e43a 100644 --- a/src/storm/storage/SymbolicMEC_stats.h +++ b/src/storm/storage/SymbolicMEC_stats.h @@ -21,16 +21,19 @@ struct StateActionPair { } }; +// [rmnt] Changed type of scc argument because the earlier one was giving a compiler error. +// [rmnt] TODO review this function, seems shady. template -static bool isTrivialSccWithoutSelfEdge_stats(StateActionPair const & scc, +static bool isTrivialSccWithoutSelfEdge_stats(storm::dd::Bdd const & scc, storm::dd::Bdd const & transitionsWithActions, std::vector> const & metaVariablesRowColumnPairs, uint_fast64_t &countSymbolicOps) { - bool isTrivialScc = (1 == scc.states.getNonZeroCount()); // [rmnt] TODO : Check if this should be counted as a symbolic op + bool isTrivialScc = (1 == scc.getNonZeroCount()); // [rmnt] TODO : Check if this should be counted as a symbolic op countSymbolicOps++; - // [rmnt] TODO : Review the noSelfEdge condition. Do you need && scc.states also? - bool noSelfEdge = (transitionsWithActions && scc.actions && scc.states.swapVariables(metaVariablesRowColumnPairs)).isZero(); - return (isTrivialScc && noSelfEdge); + if (! isTrivialScc) + return false; + bool noSelfEdge = (transitionsWithActions && scc && scc.swapVariables(metaVariablesRowColumnPairs)).isZero(); + return noSelfEdge; } @@ -99,7 +102,7 @@ std::vector> symbolicMECDecompositionNaive_stats(storm::dd: storm::dd::Bdd workingCopyTransitionsWithActions(transitionsWithActions); std::vector> result{}; std::stack> mecCandidates{}; - for (const auto& scc : symbolicScc_stats::decomposition_stats(allStates, workingCopyTransitionsWithActions.existsAbstract(metaVariablesActions), + for (const auto& scc : symbolicSCC_stats::decomposition_stats(allStates, workingCopyTransitionsWithActions.existsAbstract(metaVariablesActions), metaVariablesRow, metaVariablesColumn, countSymbolicOps)) { mecCandidates.push(scc); } @@ -120,7 +123,7 @@ std::vector> symbolicMECDecompositionNaive_stats(storm::dd: metaVariablesColumn, metaVariablesActions, metaVariablesRowColumnPairs, countSymbolicOps); workingCopyTransitionsWithActions &= !attractor.actions; countSymbolicOps++; // [rmnt] For the existsAbstract call in args to scc decomp - for (auto const& subScc : symbolicScc_stats::decomposition_stats( + for (auto const& subScc : symbolicSCC_stats::decomposition_stats( scc && !attractor.states, workingCopyTransitionsWithActions.existsAbstract(metaVariablesActions), metaVariablesRow, metaVariablesColumn, countSymbolicOps)) { mecCandidates.push(subScc); @@ -204,7 +207,7 @@ std::vector> symbolicMECDecompositionLockstep_stats(storm:: std::vector> result{}; // In paper: "goodC" std::stack mecCandidates{}; // In paper: X countSymbolicOps++; // [rmnt] For the exists abstract in the arguments - for (const auto & scc : symbolicScc_stats::decomposition_stats(allStates, workingCopyTransitionsWithActions.existsAbstract(metaVariablesActions), metaVariablesRow, metaVariablesColumn, countSymbolicOps)) { + for (const auto & scc : symbolicSCC_stats::decomposition_stats(allStates, workingCopyTransitionsWithActions.existsAbstract(metaVariablesActions), metaVariablesRow, metaVariablesColumn, countSymbolicOps)) { MecCandidate pair = { scc, scc.getDdManager().getBddZero() }; mecCandidates.push(pair); } @@ -226,7 +229,7 @@ std::vector> symbolicMECDecompositionLockstep_stats(storm:: } else if (sccTs.getNonZeroCount() >= sqrt(m)) { countSymbolicOps++; // [rmnt] for the else if condition countSymbolicOps++; // [rmnt] for the exists below - std::vector> subSccs = symbolicScc_stats::decomposition_stats( + std::vector> subSccs = symbolicSCC_stats::decomposition_stats( scc, workingCopyTransitionsWithActions.existsAbstract(metaVariablesActions), metaVariablesRow, metaVariablesColumn, countSymbolicOps); if (subSccs.size() == 1) { result.template emplace_back(scc); @@ -267,8 +270,8 @@ std::vector> symbolicMECDecompositionInterleave_stats(storm std::set const & metaVariablesActions, std::vector> const & metaVariablesRowColumnPairs, uint_fast64_t &countSymbolicOps) { - return std::vector{}; - } + return std::vector< storm::dd::Bdd > {}; +} } // namespace symbolicMEC_stats From fc6822784952b880773045c588234b5afa91cc3d Mon Sep 17 00:00:00 2001 From: Ramneet Singh Date: Sun, 16 Jun 2024 22:40:31 +0530 Subject: [PATCH 10/25] Add Interleave Algo | Seems to be correct --- src/storm/storage/SymbolicMEC.h | 179 ++++++++++++++++++++++++++++++- src/storm/storage/THESIS_DEBUG.h | 2 +- 2 files changed, 178 insertions(+), 3 deletions(-) diff --git a/src/storm/storage/SymbolicMEC.h b/src/storm/storage/SymbolicMEC.h index cac6b6cd8a..0c97ee1604 100644 --- a/src/storm/storage/SymbolicMEC.h +++ b/src/storm/storage/SymbolicMEC.h @@ -60,10 +60,12 @@ static StateActionPair computeRandomAttractor(storm::dd::Bdd const & && ( ! (actionsCannotIntoCurrent.existsAbstract(metaVariablesActions))); // [rmnt]: All states s such that some (s,a1) in currentSet and all (s,a) pairs in currentSet nextSet.states = (currentSet.states || newVertices) && allStates; + // [rmnt] TODO do the && earlier? // Actions [rmnt] Actions is really state-action pairs. storm::dd::Bdd currentVerticesAsColumn = nextSet.states.swapVariables(metaVariablesRowColumnPairs); - storm::dd::Bdd actionsCanIntoCurrentVertices = (transitionsWithActions && currentVerticesAsColumn).existsAbstract(metaVariablesColumn); + // [rmnt] TODO this can also include actions from states outside allStates. Exclude them? [YES for now] + storm::dd::Bdd actionsCanIntoCurrentVertices = (allStates && transitionsWithActions && currentVerticesAsColumn).existsAbstract(metaVariablesColumn); nextSet.actions = currentSet.actions || actionsCanIntoCurrentVertices; } while (currentSet.states != nextSet.states); return currentSet; @@ -234,6 +236,20 @@ std::vector> symbolicMECDecompositionLockstep(storm::dd::Bd return result; } +template +struct InterleaveDecompTask { + storm::dd::Bdd states; + storm::dd::Bdd startState; + + // Instantiate all copy/move constructors/assignments with the default implementation. + InterleaveDecompTask() = default; + InterleaveDecompTask(InterleaveDecompTask const& other) = default; + InterleaveDecompTask& operator=(InterleaveDecompTask const& other) = default; + InterleaveDecompTask(InterleaveDecompTask&& other) = default; + InterleaveDecompTask& operator=(InterleaveDecompTask&& other) = default; +}; + +// [rmnt] Iterative version of the algorithm in my thesis template std::vector> symbolicMECDecompositionInterleave(storm::dd::Bdd const & allStates, storm::dd::Bdd const & transitionsWithActions, @@ -241,7 +257,166 @@ std::vector> symbolicMECDecompositionInterleave(storm::dd:: std::set const & metaVariablesColumn, std::set const & metaVariablesActions, std::vector> const & metaVariablesRowColumnPairs) { - return std::vector< storm::dd::Bdd > {}; + std::vector< storm::dd::Bdd > result; + if (allStates.isZero()) { return result; } + + storm::dd::Bdd workingCopyTransitionsWithActions(transitionsWithActions); + storm::dd::Bdd transitionsWithoutActions = transitionsWithActions.existsAbstract(metaVariablesActions); + // [rmnt] TODO check if this (exists action first then relational product(exists state)) + // is better or (states and transitions then exists (state, actions)) + + std::stack< InterleaveDecompTask > workStack; + { + InterleaveDecompTask initTask = { allStates, allStates.getDdManager().getBddZero() }; + workStack.emplace(initTask); + } + + while (! workStack.empty()) + { + storm::dd::Bdd sccStartState = allStates.getDdManager().getBddZero(), + newStartState = allStates.getDdManager().getBddZero(), + V2 = allStates.getDdManager().getBddZero(), + V3 = allStates.getDdManager().getBddZero(); + + { // task Scope Start + InterleaveDecompTask task = workStack.top(); + workStack.pop(); + + if (task.startState.isZero()) + { + task.startState = pick(task.states); // [rmnt] TODO try pickv2 or other versions + } + + + { // fwdStartState Scope Start + storm::dd::Bdd fwdStartState = allStates.getDdManager().getBddZero(); + + // Inlined SCC-Fwd-Start function + { + // Forward set computation + storm::dd::Bdd prevLevel = allStates.getDdManager().getBddZero(); + storm::dd::Bdd level = task.startState; + while (! level.isZero()) { + fwdStartState |= level; + prevLevel = level; + level = post(level, task.states && (!fwdStartState), transitionsWithoutActions, metaVariablesRow, metaVariablesColumn); + // [rmnt] TODO do && !fwd in arg or after getting result? + } + + // Pick new start state as any state in the last layer + newStartState = pick(prevLevel); + + // Compute SCC by backward computation + level = task.startState; + while (! level.isZero()) + { + sccStartState |= level; + level = pre(level, task.states && fwdStartState && (!sccStartState), transitionsWithoutActions, + metaVariablesRow, metaVariablesColumn); + // [rmnt] TODO do the &&s in the argument or after getting result? + } + } + + // V1 (reuse sccStartState), V2, V3 are for the recursive call tasks + V2 = fwdStartState && (! sccStartState); + V3 = task.states && (! fwdStartState); + + } // fwdStartState Scope End + + { // ROut1 Scope Start + storm::dd::Bdd ROut1 = ROut( + sccStartState, workingCopyTransitionsWithActions, metaVariablesColumn, + metaVariablesRowColumnPairs + ); + if (ROut1.isZero()) { + if (! isTrivialSccWithoutSelfEdge(sccStartState, workingCopyTransitionsWithActions, metaVariablesRowColumnPairs)) + { result.emplace_back(sccStartState); } + + sccStartState = allStates.getDdManager().getBddZero(); // So that the first recursive call doesn't happen + } + else { + StateActionPair Attr1 = computeRandomAttractor( + ROut1, sccStartState, workingCopyTransitionsWithActions, + metaVariablesColumn, metaVariablesActions, metaVariablesRowColumnPairs + ); + workingCopyTransitionsWithActions &= (! Attr1.actions); + sccStartState &= (! Attr1.states); // For V1, reusing this + } + + } // ROut1 Scope End + + { // ROut3 Scope Start + storm::dd::Bdd ROut3 = ROut( + V3, workingCopyTransitionsWithActions, metaVariablesColumn, + metaVariablesRowColumnPairs + ); + if (! ROut3.isZero()) { + StateActionPair Attr3 = computeRandomAttractor( + ROut3, V3, workingCopyTransitionsWithActions, + metaVariablesColumn, metaVariablesActions, metaVariablesRowColumnPairs + ); + workingCopyTransitionsWithActions &= (! Attr3.actions); + V3 &= (! Attr3.states); // For V3, reusing this + } + + } // ROut3 Scope End + } // task Scope End + + // Get the sizes of each (potential) recursive call. Do them in order from smallest to largest + // So push on stack in order from largest to smallest + uint_fast64_t sizes[3] = { sccStartState.getNonZeroCount(), V2.getNonZeroCount(), V3.getNonZeroCount() }; + uint8_t order[3] = { 1, 2, 3 }; + + // Sort order and sizes based on sizes + { + if (sizes[0] > sizes[1]) { + order[1] = 1; order[0] = 2; + uint_fast64_t temp = sizes[0]; + sizes[0] = sizes[1]; + sizes[1] = temp; + } + if (sizes[1] > sizes[2]) { + uint8_t tempOrder = order[1]; + order[1] = order[2]; + order[2] = tempOrder; + + uint_fast64_t tempSizes = sizes[1]; + sizes[1] = sizes[2]; + sizes[2] = tempSizes; + + if (sizes[0] > sizes[1]) { + uint8_t tempOrder = order[0]; + order[0] = order[1]; + order[1] = tempOrder; + + uint_fast64_t tempSizes = sizes[0]; + sizes[0] = sizes[1]; + sizes[1] = tempSizes; + } + } + } + + for(uint8_t i=0; i<3; i++) { + if ( order[2-i] == 1) { + if ( sizes[2-i] != 0 ) { + InterleaveDecompTask newTask = { sccStartState, allStates.getDdManager().getBddZero() }; + workStack.emplace(newTask); + } + } else if ( order[2-i] == 2 ) { + if ( sizes[2-i] != 0 ) { + InterleaveDecompTask newTask = { V2, newStartState }; + workStack.emplace(newTask); + } + } else { + if ( sizes[2-i] != 0 ) { + InterleaveDecompTask newTask = { V3, allStates.getDdManager().getBddZero() }; + workStack.emplace(newTask); + } + } + } + } + + return result; } } // namespace symbolicMEC diff --git a/src/storm/storage/THESIS_DEBUG.h b/src/storm/storage/THESIS_DEBUG.h index be9138d1a8..7ae49266b1 100644 --- a/src/storm/storage/THESIS_DEBUG.h +++ b/src/storm/storage/THESIS_DEBUG.h @@ -59,7 +59,7 @@ struct BenchmarkResult { void print() { std::string algorithm = benchmarkToString(type); - std::cout << "BENCHMARK MEC DECOMPOSITION (algorithm, time, mecCount[, conversionTime]): " + std::cout << "BENCHMARK MEC DECOMPOSITION (algorithm, time, mecCount): " << algorithm << ", " << decompositionTimeInNanoseconds << ", " << mecCount << "\n"; } From 34444d5370c66ed5fd240434dc99ec6f6f2f204f Mon Sep 17 00:00:00 2001 From: Ramneet-Singh Date: Mon, 17 Jun 2024 11:20:32 +0530 Subject: [PATCH 11/25] Add Interleave Stats Code | Untested --- src/storm/storage/SymbolicMEC_stats.h | 178 ++++++++++++++++++++++++-- 1 file changed, 170 insertions(+), 8 deletions(-) diff --git a/src/storm/storage/SymbolicMEC_stats.h b/src/storm/storage/SymbolicMEC_stats.h index c35b06e43a..0cee7296fd 100644 --- a/src/storm/storage/SymbolicMEC_stats.h +++ b/src/storm/storage/SymbolicMEC_stats.h @@ -261,16 +261,178 @@ std::vector> symbolicMECDecompositionLockstep_stats(storm:: return result; } - +// [rmnt] Iterative version of the algorithm in my thesis template std::vector> symbolicMECDecompositionInterleave_stats(storm::dd::Bdd const & allStates, - storm::dd::Bdd const & transitionsWithActions, - std::set const & metaVariablesRow, - std::set const & metaVariablesColumn, - std::set const & metaVariablesActions, - std::vector> const & metaVariablesRowColumnPairs, - uint_fast64_t &countSymbolicOps) { - return std::vector< storm::dd::Bdd > {}; + storm::dd::Bdd const & transitionsWithActions, + std::set const & metaVariablesRow, + std::set const & metaVariablesColumn, + std::set const & metaVariablesActions, + std::vector> const & metaVariablesRowColumnPairs, + uint_fast64_t &countSymbolicOps) { + std::vector< storm::dd::Bdd > result; + if (allStates.isZero()) { return result; } + + storm::dd::Bdd workingCopyTransitionsWithActions(transitionsWithActions); + storm::dd::Bdd transitionsWithoutActions = transitionsWithActions.existsAbstract(metaVariablesActions); + // [rmnt] TODO check if this (exists action first then relational product(exists state)) + // is better or (states and transitions then exists (state, actions)) + countSymbolicOps++; // [rmnt] For the existsAbstract above + + std::stack< InterleaveDecompTask > workStack; + { + InterleaveDecompTask initTask = { allStates, allStates.getDdManager().getBddZero() }; + workStack.emplace(initTask); + } + + while (! workStack.empty()) + { + storm::dd::Bdd sccStartState = allStates.getDdManager().getBddZero(), + newStartState = allStates.getDdManager().getBddZero(), + V2 = allStates.getDdManager().getBddZero(), + V3 = allStates.getDdManager().getBddZero(); + + { // task Scope Start + InterleaveDecompTask task = workStack.top(); + workStack.pop(); + + if (task.startState.isZero()) + { + task.startState = pick_stats(task.states, countSymbolicOps); // [rmnt] TODO try pickv2 or other versions + } + + + { // fwdStartState Scope Start + storm::dd::Bdd fwdStartState = allStates.getDdManager().getBddZero(); + + // Inlined SCC-Fwd-Start function + { + // Forward set computation + storm::dd::Bdd prevLevel = allStates.getDdManager().getBddZero(); + storm::dd::Bdd level = task.startState; + while (! level.isZero()) { + fwdStartState |= level; + prevLevel = level; + level = post_stats(level, task.states && (!fwdStartState), transitionsWithoutActions, metaVariablesRow, metaVariablesColumn, countSymbolicOps); + // [rmnt] TODO do && !fwd in arg or after getting result? + } + + // Pick new start state as any state in the last layer + newStartState = pick_stats(prevLevel, countSymbolicOps); + + // Compute SCC by backward computation + level = task.startState; + while (! level.isZero()) + { + sccStartState |= level; + level = pre_stats(level, task.states && fwdStartState && (!sccStartState), transitionsWithoutActions, + metaVariablesRow, metaVariablesColumn, countSymbolicOps); + // [rmnt] TODO do the &&s in the argument or after getting result? + } + } + + // V1 (reuse sccStartState), V2, V3 are for the recursive call tasks + V2 = fwdStartState && (! sccStartState); + V3 = task.states && (! fwdStartState); + + } // fwdStartState Scope End + + { // ROut1 Scope Start + storm::dd::Bdd ROut1 = ROut_stats( + sccStartState, workingCopyTransitionsWithActions, metaVariablesColumn, + metaVariablesRowColumnPairs, countSymbolicOps + ); + if (ROut1.isZero()) { + if (! isTrivialSccWithoutSelfEdge_stats(sccStartState, workingCopyTransitionsWithActions, metaVariablesRowColumnPairs, countSymbolicOps)) + { result.emplace_back(sccStartState); } + + sccStartState = allStates.getDdManager().getBddZero(); // So that the first recursive call doesn't happen + } + else { + StateActionPair Attr1 = computeRandomAttractor_stats( + ROut1, sccStartState, workingCopyTransitionsWithActions, + metaVariablesColumn, metaVariablesActions, metaVariablesRowColumnPairs, + countSymbolicOps + ); + workingCopyTransitionsWithActions &= (! Attr1.actions); + sccStartState &= (! Attr1.states); // For V1, reusing this + } + + } // ROut1 Scope End + + { // ROut3 Scope Start + storm::dd::Bdd ROut3 = ROut_stats( + V3, workingCopyTransitionsWithActions, metaVariablesColumn, + metaVariablesRowColumnPairs, countSymbolicOps + ); + if (! ROut3.isZero()) { + StateActionPair Attr3 = computeRandomAttractor_stats( + ROut3, V3, workingCopyTransitionsWithActions, + metaVariablesColumn, metaVariablesActions, metaVariablesRowColumnPairs, + countSymbolicOps + ); + workingCopyTransitionsWithActions &= (! Attr3.actions); + V3 &= (! Attr3.states); // For V3, reusing this + } + + } // ROut3 Scope End + } // task Scope End + + // Get the sizes of each (potential) recursive call. Do them in order from smallest to largest + // So push on stack in order from largest to smallest + uint_fast64_t sizes[3] = { sccStartState.getNonZeroCount(), V2.getNonZeroCount(), V3.getNonZeroCount() }; + uint8_t order[3] = { 1, 2, 3 }; + + // Sort order and sizes based on sizes + { + if (sizes[0] > sizes[1]) { + order[1] = 1; order[0] = 2; + uint_fast64_t temp = sizes[0]; + sizes[0] = sizes[1]; + sizes[1] = temp; + } + if (sizes[1] > sizes[2]) { + uint8_t tempOrder = order[1]; + order[1] = order[2]; + order[2] = tempOrder; + + uint_fast64_t tempSizes = sizes[1]; + sizes[1] = sizes[2]; + sizes[2] = tempSizes; + + if (sizes[0] > sizes[1]) { + uint8_t tempOrder = order[0]; + order[0] = order[1]; + order[1] = tempOrder; + + uint_fast64_t tempSizes = sizes[0]; + sizes[0] = sizes[1]; + sizes[1] = tempSizes; + } + } + } + + for(uint8_t i=0; i<3; i++) { + if ( order[2-i] == 1) { + if ( sizes[2-i] != 0 ) { + InterleaveDecompTask newTask = { sccStartState, allStates.getDdManager().getBddZero() }; + workStack.emplace(newTask); + } + } else if ( order[2-i] == 2 ) { + if ( sizes[2-i] != 0 ) { + InterleaveDecompTask newTask = { V2, newStartState }; + workStack.emplace(newTask); + } + } else { + if ( sizes[2-i] != 0 ) { + InterleaveDecompTask newTask = { V3, allStates.getDdManager().getBddZero() }; + workStack.emplace(newTask); + } + } + } + } + + return result; } } // namespace symbolicMEC_stats From 594e4219e02bb837964062e735c987b8bd67f285 Mon Sep 17 00:00:00 2001 From: Ramneet-Singh Date: Mon, 17 Jun 2024 11:51:58 +0530 Subject: [PATCH 12/25] Run clang-format --- src/storm-cli-utilities/model-handling.h | 2 +- src/storm/storage/SymbolicMEC.h | 279 +++++++------- src/storm/storage/SymbolicMEC_stats.h | 339 ++++++++---------- src/storm/storage/SymbolicOperations.h | 34 +- src/storm/storage/SymbolicOperations_stats.h | 44 +-- src/storm/storage/SymbolicSCCDecomposition.h | 16 +- .../storage/SymbolicSCCDecomposition_stats.h | 30 +- src/storm/storage/THESIS_DEBUG.h | 228 ++++++------ src/storm/storage/dd/Bdd.h | 2 +- src/storm/storage/dd/cudd/InternalCuddBdd.cpp | 2 +- src/storm/storage/dd/cudd/InternalCuddBdd.h | 2 +- .../storage/dd/sylvan/InternalSylvanBdd.h | 2 +- 12 files changed, 465 insertions(+), 515 deletions(-) diff --git a/src/storm-cli-utilities/model-handling.h b/src/storm-cli-utilities/model-handling.h index 89d77d4593..b95bb1b5a3 100644 --- a/src/storm-cli-utilities/model-handling.h +++ b/src/storm-cli-utilities/model-handling.h @@ -521,7 +521,7 @@ std::shared_ptr buildModel(SymbolicInput const& input, 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((storm::models::ModelBase const &)*result, DEBUG_THESIS_BENCHMARK); + doMecBenchmark((storm::models::ModelBase const&)*result, DEBUG_THESIS_BENCHMARK); exit(0); } diff --git a/src/storm/storage/SymbolicMEC.h b/src/storm/storage/SymbolicMEC.h index 0c97ee1604..cbc52bf26f 100644 --- a/src/storm/storage/SymbolicMEC.h +++ b/src/storm/storage/SymbolicMEC.h @@ -3,19 +3,19 @@ #include #include -#include "storm/storage/dd/DdType.h" -#include "storm/storage/dd/Bdd.h" #include "storm/storage/SymbolicSCCDecomposition.h" +#include "storm/storage/dd/Bdd.h" +#include "storm/storage/dd/DdType.h" namespace symbolicMEC { template struct StateActionPair { storm::dd::Bdd states; - storm::dd::Bdd actions; // [rmnt]: Actions is really state-action pairs. + storm::dd::Bdd actions; // [rmnt]: Actions is really state-action pairs. - StateActionPair& operator|=(StateActionPair const & other) { - states |= other.states; + StateActionPair& operator|=(StateActionPair const& other) { + states |= other.states; actions |= other.actions; return *this; } @@ -24,17 +24,15 @@ struct StateActionPair { // [rmnt] Changed type of scc argument because the earlier one was giving a compiler error. // [rmnt] TODO review this function, seems shady. template -static bool isTrivialSccWithoutSelfEdge(storm::dd::Bdd const & scc, - storm::dd::Bdd const & transitionsWithActions, - std::vector> const & metaVariablesRowColumnPairs) { - bool isTrivialScc = (1 == scc.getNonZeroCount()); // [rmnt] TODO : Check if this should be counted as a symbolic op - if (! isTrivialScc) +static bool isTrivialSccWithoutSelfEdge(storm::dd::Bdd const& scc, storm::dd::Bdd const& transitionsWithActions, + std::vector> const& metaVariablesRowColumnPairs) { + bool isTrivialScc = (1 == scc.getNonZeroCount()); // [rmnt] TODO : Check if this should be counted as a symbolic op + if (!isTrivialScc) return false; bool noSelfEdge = (transitionsWithActions && scc && scc.swapVariables(metaVariablesRowColumnPairs)).isZero(); return noSelfEdge; } - /* Given a set of vertices T, the random attractor Attr_R(T) * is a set of vertices consisting of * (1) T, @@ -42,22 +40,21 @@ static bool isTrivialSccWithoutSelfEdge(storm::dd::Bdd const & scc, * (3) player-1 vertices with all outgoing edges in Attr_R(T). */ template -static StateActionPair computeRandomAttractor(storm::dd::Bdd const & actionsToApplyOn, - storm::dd::Bdd const & allStates, - storm::dd::Bdd const & transitionsWithActions, - std::set const & metaVariablesColumn, - std::set const & metaVariablesActions, - std::vector> const & metaVariablesRowColumnPairs) { - StateActionPair nextSet = { .states = allStates.getDdManager().getBddZero(), .actions = actionsToApplyOn }; +static StateActionPair computeRandomAttractor( + storm::dd::Bdd const& actionsToApplyOn, storm::dd::Bdd const& allStates, storm::dd::Bdd const& transitionsWithActions, + std::set const& metaVariablesColumn, std::set const& metaVariablesActions, + std::vector> const& metaVariablesRowColumnPairs) { + StateActionPair nextSet = {.states = allStates.getDdManager().getBddZero(), .actions = actionsToApplyOn}; StateActionPair currentSet; do { currentSet = nextSet; // Vertices - storm::dd::Bdd actionsCannotIntoCurrent = ( transitionsWithActions && ( ! currentSet.actions) - ).existsAbstract(metaVariablesColumn); // [rmnt]: All (s,a) pairs which aren't included in currentSet - storm::dd::Bdd newVertices = currentSet.actions.existsAbstract(metaVariablesActions) - && ( ! (actionsCannotIntoCurrent.existsAbstract(metaVariablesActions))); + storm::dd::Bdd actionsCannotIntoCurrent = + (transitionsWithActions && (!currentSet.actions)) + .existsAbstract(metaVariablesColumn); // [rmnt]: All (s,a) pairs which aren't included in currentSet + storm::dd::Bdd newVertices = + currentSet.actions.existsAbstract(metaVariablesActions) && (!(actionsCannotIntoCurrent.existsAbstract(metaVariablesActions))); // [rmnt]: All states s such that some (s,a1) in currentSet and all (s,a) pairs in currentSet nextSet.states = (currentSet.states || newVertices) && allStates; // [rmnt] TODO do the && earlier? @@ -65,7 +62,8 @@ static StateActionPair computeRandomAttractor(storm::dd::Bdd const & // Actions [rmnt] Actions is really state-action pairs. storm::dd::Bdd currentVerticesAsColumn = nextSet.states.swapVariables(metaVariablesRowColumnPairs); // [rmnt] TODO this can also include actions from states outside allStates. Exclude them? [YES for now] - storm::dd::Bdd actionsCanIntoCurrentVertices = (allStates && transitionsWithActions && currentVerticesAsColumn).existsAbstract(metaVariablesColumn); + storm::dd::Bdd actionsCanIntoCurrentVertices = + (allStates && transitionsWithActions && currentVerticesAsColumn).existsAbstract(metaVariablesColumn); nextSet.actions = currentSet.actions || actionsCanIntoCurrentVertices; } while (currentSet.states != nextSet.states); return currentSet; @@ -74,25 +72,21 @@ static StateActionPair computeRandomAttractor(storm::dd::Bdd const & // For a set of states S, // return all actions which have a non-zero-probability of leaving S. template -static storm::dd::Bdd ROut(storm::dd::Bdd const & sccStates, - storm::dd::Bdd const & transitionsWithActions, - std::set const & metaVariablesColumn, - std::vector> const & metaVariablesRowColumnPairs) { - storm::dd::Bdd transitionsFromSccToOutside = sccStates && transitionsWithActions && ( ! sccStates.swapVariables(metaVariablesRowColumnPairs)); +static storm::dd::Bdd ROut(storm::dd::Bdd const& sccStates, storm::dd::Bdd const& transitionsWithActions, + std::set const& metaVariablesColumn, + std::vector> const& metaVariablesRowColumnPairs) { + storm::dd::Bdd transitionsFromSccToOutside = sccStates && transitionsWithActions && (!sccStates.swapVariables(metaVariablesRowColumnPairs)); storm::dd::Bdd actionsLeavingScc = transitionsFromSccToOutside.existsAbstract(metaVariablesColumn); return actionsLeavingScc; } - // As described in // "Symbolic algorithms for graphs and Markov decision processes with fairness objectives" template -std::vector> symbolicMECDecompositionNaive(storm::dd::Bdd const & allStates, - storm::dd::Bdd const & transitionsWithActions, - std::set const & metaVariablesRow, - std::set const & metaVariablesColumn, - std::set const & metaVariablesActions, - std::vector> const & metaVariablesRowColumnPairs) { +std::vector> symbolicMECDecompositionNaive( + storm::dd::Bdd const& allStates, storm::dd::Bdd const& transitionsWithActions, std::set const& metaVariablesRow, + std::set const& metaVariablesColumn, std::set const& metaVariablesActions, + std::vector> const& metaVariablesRowColumnPairs) { storm::dd::Bdd workingCopyTransitionsWithActions(transitionsWithActions); std::vector> result{}; std::stack> mecCandidates{}; @@ -100,7 +94,7 @@ std::vector> symbolicMECDecompositionNaive(storm::dd::Bdd scc = mecCandidates.top(); mecCandidates.pop(); @@ -112,7 +106,8 @@ std::vector> symbolicMECDecompositionNaive(storm::dd::Bdd attractor = computeRandomAttractor(sccROut, scc, workingCopyTransitionsWithActions, metaVariablesColumn, metaVariablesActions, metaVariablesRowColumnPairs); + StateActionPair attractor = + computeRandomAttractor(sccROut, scc, workingCopyTransitionsWithActions, metaVariablesColumn, metaVariablesActions, metaVariablesRowColumnPairs); workingCopyTransitionsWithActions &= !attractor.actions; for (auto const& subScc : symbolicSCC::decomposition( scc && !attractor.states, workingCopyTransitionsWithActions.existsAbstract(metaVariablesActions), metaVariablesRow, metaVariablesColumn)) { @@ -127,27 +122,26 @@ std::vector> symbolicMECDecompositionNaive(storm::dd::Bdd -storm::dd::Bdd LockStepSearch(storm::dd::Bdd const & states, // S - storm::dd::Bdd const & statesWithRemovedEdges, // T_S - storm::dd::Bdd const & transitionsWithoutActions, - std::set const & metaVariablesRow, - std::set const & metaVariablesColumn) { +storm::dd::Bdd LockStepSearch(storm::dd::Bdd const& states, // S + storm::dd::Bdd const& statesWithRemovedEdges, // T_S + storm::dd::Bdd const& transitionsWithoutActions, std::set const& metaVariablesRow, + std::set const& metaVariablesColumn) { storm::dd::Bdd ts = storm::dd::Bdd(statesWithRemovedEdges); std::unordered_map, storm::dd::Bdd> c{}; - while ( ! ts.isZero()) { + while (!ts.isZero()) { storm::dd::Bdd v = pick(ts); - ts &= ! v; + ts &= !v; c[v] = storm::dd::Bdd(v); } ts = storm::dd::Bdd(statesWithRemovedEdges); while (true) { - for (auto it = c.cbegin(); it != c.cend(); ) { + for (auto it = c.cbegin(); it != c.cend();) { storm::dd::Bdd t = storm::dd::Bdd(it->first); storm::dd::Bdd ct = storm::dd::Bdd(it->second); storm::dd::Bdd ctNew = ct || post(ct, states, transitionsWithoutActions, metaVariablesRow, metaVariablesColumn); - if ((ctNew && ts).getNonZeroCount() > 1) { // [rmnt] there was another state in T_S in the same SCC as t, so we can ignore t. - ts &= ! t; + if ((ctNew && ts).getNonZeroCount() > 1) { // [rmnt] there was another state in T_S in the same SCC as t, so we can ignore t. + ts &= !t; c.erase(it++); } else { if (ctNew == ct) { @@ -164,43 +158,42 @@ storm::dd::Bdd LockStepSearch(storm::dd::Bdd const & states, // S // "Symbolic Algorithms for Graphs and Markov Decision Processes with Fairness Objectives" // Uses a lockstep search template -std::vector> symbolicMECDecompositionLockstep(storm::dd::Bdd const & allStates, - storm::dd::Bdd const & transitionsWithActions, - std::set const & metaVariablesRow, - std::set const & metaVariablesColumn, - std::set const & metaVariablesActions, - std::vector> const & metaVariablesRowColumnPairs) { +std::vector> symbolicMECDecompositionLockstep( + storm::dd::Bdd const& allStates, storm::dd::Bdd const& transitionsWithActions, std::set const& metaVariablesRow, + std::set const& metaVariablesColumn, std::set const& metaVariablesActions, + std::vector> const& metaVariablesRowColumnPairs) { struct MecCandidate { - storm::dd::Bdd states; // In paper: S - storm::dd::Bdd statesWithRemovedEdge; // In Paper: T_s + storm::dd::Bdd states; // In paper: S + storm::dd::Bdd statesWithRemovedEdge; // In Paper: T_s }; // Helper function for better readability - auto hasAtLeastOneEdge = - [metaVariablesActions, metaVariablesRow, metaVariablesColumn, metaVariablesRowColumnPairs] - (storm::dd::Bdd scc, storm::dd::Bdd transitionsWithActions) { + auto hasAtLeastOneEdge = [metaVariablesActions, metaVariablesRow, metaVariablesColumn, metaVariablesRowColumnPairs]( + storm::dd::Bdd scc, storm::dd::Bdd transitionsWithActions) { // Paper suggestion - return ! (post(scc, scc, transitionsWithActions.existsAbstract(metaVariablesActions), metaVariablesRow, metaVariablesColumn)).isZero(); + return !(post(scc, scc, transitionsWithActions.existsAbstract(metaVariablesActions), metaVariablesRow, metaVariablesColumn)).isZero(); }; uint_fast64_t m = (transitionsWithActions.existsAbstract(metaVariablesActions) && allStates).getNonZeroCount(); storm::dd::Bdd workingCopyTransitionsWithActions(transitionsWithActions); - std::vector> result{}; // In paper: "goodC" - std::stack mecCandidates{}; // In paper: X - for (const auto & scc : symbolicSCC::decomposition(allStates, workingCopyTransitionsWithActions.existsAbstract(metaVariablesActions), metaVariablesRow, metaVariablesColumn)) { - MecCandidate pair = { scc, scc.getDdManager().getBddZero() }; + std::vector> result{}; // In paper: "goodC" + std::stack mecCandidates{}; // In paper: X + for (const auto& scc : symbolicSCC::decomposition(allStates, workingCopyTransitionsWithActions.existsAbstract(metaVariablesActions), + metaVariablesRow, metaVariablesColumn)) { + MecCandidate pair = {scc, scc.getDdManager().getBddZero()}; mecCandidates.push(pair); } - while ( ! mecCandidates.empty()) { + while (!mecCandidates.empty()) { MecCandidate currentCandidate = mecCandidates.top(); storm::dd::Bdd scc = currentCandidate.states; storm::dd::Bdd sccTs = currentCandidate.statesWithRemovedEdge; mecCandidates.pop(); storm::dd::Bdd sccROut = ROut(scc, workingCopyTransitionsWithActions, metaVariablesColumn, metaVariablesRowColumnPairs); - StateActionPair randomAttractor = computeRandomAttractor(sccROut, scc, workingCopyTransitionsWithActions, metaVariablesColumn, metaVariablesActions, metaVariablesRowColumnPairs); - scc &= ! randomAttractor.states; - workingCopyTransitionsWithActions &= ! randomAttractor.actions; + StateActionPair randomAttractor = + computeRandomAttractor(sccROut, scc, workingCopyTransitionsWithActions, metaVariablesColumn, metaVariablesActions, metaVariablesRowColumnPairs); + scc &= !randomAttractor.states; + workingCopyTransitionsWithActions &= !randomAttractor.actions; sccTs = (sccTs || randomAttractor.actions.existsAbstract(metaVariablesActions)) && scc; if (hasAtLeastOneEdge(scc, workingCopyTransitionsWithActions)) { if (sccTs.isZero()) { @@ -218,17 +211,17 @@ std::vector> symbolicMECDecompositionLockstep(storm::dd::Bd } } else { // bottomScc is "C" in paper - storm::dd::Bdd bottomScc = LockStepSearch(scc, sccTs, - workingCopyTransitionsWithActions.existsAbstract(metaVariablesActions), - metaVariablesRow, metaVariablesColumn); + storm::dd::Bdd bottomScc = LockStepSearch( + scc, sccTs, workingCopyTransitionsWithActions.existsAbstract(metaVariablesActions), metaVariablesRow, metaVariablesColumn); if (hasAtLeastOneEdge(bottomScc, workingCopyTransitionsWithActions)) { result.template emplace_back(bottomScc); } - storm::dd::Bdd statesLeadingIntoBottomScc = pre(bottomScc, scc, workingCopyTransitionsWithActions.existsAbstract(metaVariablesActions), metaVariablesRow, metaVariablesColumn); - mecCandidates.emplace((MecCandidate) { - scc && ( ! bottomScc), - (scc && ( ! bottomScc)) && (statesLeadingIntoBottomScc || sccTs), + storm::dd::Bdd statesLeadingIntoBottomScc = + pre(bottomScc, scc, workingCopyTransitionsWithActions.existsAbstract(metaVariablesActions), metaVariablesRow, metaVariablesColumn); + mecCandidates.emplace((MecCandidate){ + scc && (!bottomScc), + (scc && (!bottomScc)) && (statesLeadingIntoBottomScc || sccTs), }); } } @@ -251,44 +244,39 @@ struct InterleaveDecompTask { // [rmnt] Iterative version of the algorithm in my thesis template -std::vector> symbolicMECDecompositionInterleave(storm::dd::Bdd const & allStates, - storm::dd::Bdd const & transitionsWithActions, - std::set const & metaVariablesRow, - std::set const & metaVariablesColumn, - std::set const & metaVariablesActions, - std::vector> const & metaVariablesRowColumnPairs) { - std::vector< storm::dd::Bdd > result; - if (allStates.isZero()) { return result; } +std::vector> symbolicMECDecompositionInterleave( + storm::dd::Bdd const& allStates, storm::dd::Bdd const& transitionsWithActions, std::set const& metaVariablesRow, + std::set const& metaVariablesColumn, std::set const& metaVariablesActions, + std::vector> const& metaVariablesRowColumnPairs) { + std::vector> result; + if (allStates.isZero()) { + return result; + } storm::dd::Bdd workingCopyTransitionsWithActions(transitionsWithActions); storm::dd::Bdd transitionsWithoutActions = transitionsWithActions.existsAbstract(metaVariablesActions); // [rmnt] TODO check if this (exists action first then relational product(exists state)) // is better or (states and transitions then exists (state, actions)) - std::stack< InterleaveDecompTask > workStack; + std::stack> workStack; { - InterleaveDecompTask initTask = { allStates, allStates.getDdManager().getBddZero() }; + InterleaveDecompTask initTask = {allStates, allStates.getDdManager().getBddZero()}; workStack.emplace(initTask); } - while (! workStack.empty()) - { - storm::dd::Bdd sccStartState = allStates.getDdManager().getBddZero(), - newStartState = allStates.getDdManager().getBddZero(), - V2 = allStates.getDdManager().getBddZero(), - V3 = allStates.getDdManager().getBddZero(); + while (!workStack.empty()) { + storm::dd::Bdd sccStartState = allStates.getDdManager().getBddZero(), newStartState = allStates.getDdManager().getBddZero(), + V2 = allStates.getDdManager().getBddZero(), V3 = allStates.getDdManager().getBddZero(); - { // task Scope Start + { // task Scope Start InterleaveDecompTask task = workStack.top(); workStack.pop(); - if (task.startState.isZero()) - { - task.startState = pick(task.states); // [rmnt] TODO try pickv2 or other versions + if (task.startState.isZero()) { + task.startState = pick(task.states); // [rmnt] TODO try pickv2 or other versions } - - { // fwdStartState Scope Start + { // fwdStartState Scope Start storm::dd::Bdd fwdStartState = allStates.getDdManager().getBddZero(); // Inlined SCC-Fwd-Start function @@ -296,7 +284,7 @@ std::vector> symbolicMECDecompositionInterleave(storm::dd:: // Forward set computation storm::dd::Bdd prevLevel = allStates.getDdManager().getBddZero(); storm::dd::Bdd level = task.startState; - while (! level.isZero()) { + while (!level.isZero()) { fwdStartState |= level; prevLevel = level; level = post(level, task.states && (!fwdStartState), transitionsWithoutActions, metaVariablesRow, metaVariablesColumn); @@ -304,73 +292,62 @@ std::vector> symbolicMECDecompositionInterleave(storm::dd:: } // Pick new start state as any state in the last layer - newStartState = pick(prevLevel); + newStartState = pick(prevLevel); // Compute SCC by backward computation level = task.startState; - while (! level.isZero()) - { + while (!level.isZero()) { sccStartState |= level; - level = pre(level, task.states && fwdStartState && (!sccStartState), transitionsWithoutActions, - metaVariablesRow, metaVariablesColumn); + level = pre(level, task.states && fwdStartState && (!sccStartState), transitionsWithoutActions, metaVariablesRow, metaVariablesColumn); // [rmnt] TODO do the &&s in the argument or after getting result? } } // V1 (reuse sccStartState), V2, V3 are for the recursive call tasks - V2 = fwdStartState && (! sccStartState); - V3 = task.states && (! fwdStartState); + V2 = fwdStartState && (!sccStartState); + V3 = task.states && (!fwdStartState); - } // fwdStartState Scope End + } // fwdStartState Scope End - { // ROut1 Scope Start - storm::dd::Bdd ROut1 = ROut( - sccStartState, workingCopyTransitionsWithActions, metaVariablesColumn, - metaVariablesRowColumnPairs - ); + { // ROut1 Scope Start + storm::dd::Bdd ROut1 = ROut(sccStartState, workingCopyTransitionsWithActions, metaVariablesColumn, metaVariablesRowColumnPairs); if (ROut1.isZero()) { - if (! isTrivialSccWithoutSelfEdge(sccStartState, workingCopyTransitionsWithActions, metaVariablesRowColumnPairs)) - { result.emplace_back(sccStartState); } - - sccStartState = allStates.getDdManager().getBddZero(); // So that the first recursive call doesn't happen - } - else { - StateActionPair Attr1 = computeRandomAttractor( - ROut1, sccStartState, workingCopyTransitionsWithActions, - metaVariablesColumn, metaVariablesActions, metaVariablesRowColumnPairs - ); - workingCopyTransitionsWithActions &= (! Attr1.actions); - sccStartState &= (! Attr1.states); // For V1, reusing this + if (!isTrivialSccWithoutSelfEdge(sccStartState, workingCopyTransitionsWithActions, metaVariablesRowColumnPairs)) { + result.emplace_back(sccStartState); + } + + sccStartState = allStates.getDdManager().getBddZero(); // So that the first recursive call doesn't happen + } else { + StateActionPair Attr1 = computeRandomAttractor(ROut1, sccStartState, workingCopyTransitionsWithActions, metaVariablesColumn, + metaVariablesActions, metaVariablesRowColumnPairs); + workingCopyTransitionsWithActions &= (!Attr1.actions); + sccStartState &= (!Attr1.states); // For V1, reusing this } - } // ROut1 Scope End - - { // ROut3 Scope Start - storm::dd::Bdd ROut3 = ROut( - V3, workingCopyTransitionsWithActions, metaVariablesColumn, - metaVariablesRowColumnPairs - ); - if (! ROut3.isZero()) { - StateActionPair Attr3 = computeRandomAttractor( - ROut3, V3, workingCopyTransitionsWithActions, - metaVariablesColumn, metaVariablesActions, metaVariablesRowColumnPairs - ); - workingCopyTransitionsWithActions &= (! Attr3.actions); - V3 &= (! Attr3.states); // For V3, reusing this + } // ROut1 Scope End + + { // ROut3 Scope Start + storm::dd::Bdd ROut3 = ROut(V3, workingCopyTransitionsWithActions, metaVariablesColumn, metaVariablesRowColumnPairs); + if (!ROut3.isZero()) { + StateActionPair Attr3 = computeRandomAttractor(ROut3, V3, workingCopyTransitionsWithActions, metaVariablesColumn, + metaVariablesActions, metaVariablesRowColumnPairs); + workingCopyTransitionsWithActions &= (!Attr3.actions); + V3 &= (!Attr3.states); // For V3, reusing this } - } // ROut3 Scope End - } // task Scope End + } // ROut3 Scope End + } // task Scope End // Get the sizes of each (potential) recursive call. Do them in order from smallest to largest // So push on stack in order from largest to smallest - uint_fast64_t sizes[3] = { sccStartState.getNonZeroCount(), V2.getNonZeroCount(), V3.getNonZeroCount() }; - uint8_t order[3] = { 1, 2, 3 }; + uint_fast64_t sizes[3] = {sccStartState.getNonZeroCount(), V2.getNonZeroCount(), V3.getNonZeroCount()}; + uint8_t order[3] = {1, 2, 3}; // Sort order and sizes based on sizes { if (sizes[0] > sizes[1]) { - order[1] = 1; order[0] = 2; + order[1] = 1; + order[0] = 2; uint_fast64_t temp = sizes[0]; sizes[0] = sizes[1]; sizes[1] = temp; @@ -396,20 +373,20 @@ std::vector> symbolicMECDecompositionInterleave(storm::dd:: } } - for(uint8_t i=0; i<3; i++) { - if ( order[2-i] == 1) { - if ( sizes[2-i] != 0 ) { - InterleaveDecompTask newTask = { sccStartState, allStates.getDdManager().getBddZero() }; + for (uint8_t i = 0; i < 3; i++) { + if (order[2 - i] == 1) { + if (sizes[2 - i] != 0) { + InterleaveDecompTask newTask = {sccStartState, allStates.getDdManager().getBddZero()}; workStack.emplace(newTask); } - } else if ( order[2-i] == 2 ) { - if ( sizes[2-i] != 0 ) { - InterleaveDecompTask newTask = { V2, newStartState }; + } else if (order[2 - i] == 2) { + if (sizes[2 - i] != 0) { + InterleaveDecompTask newTask = {V2, newStartState}; workStack.emplace(newTask); } } else { - if ( sizes[2-i] != 0 ) { - InterleaveDecompTask newTask = { V3, allStates.getDdManager().getBddZero() }; + if (sizes[2 - i] != 0) { + InterleaveDecompTask newTask = {V3, allStates.getDdManager().getBddZero()}; workStack.emplace(newTask); } } @@ -419,6 +396,6 @@ std::vector> symbolicMECDecompositionInterleave(storm::dd:: return result; } -} // namespace symbolicMEC +} // namespace symbolicMEC #endif \ No newline at end of file diff --git a/src/storm/storage/SymbolicMEC_stats.h b/src/storm/storage/SymbolicMEC_stats.h index 0cee7296fd..d77fdc1d84 100644 --- a/src/storm/storage/SymbolicMEC_stats.h +++ b/src/storm/storage/SymbolicMEC_stats.h @@ -3,19 +3,19 @@ #include #include -#include "storm/storage/dd/DdType.h" -#include "storm/storage/dd/Bdd.h" #include "storm/storage/SymbolicSCCDecomposition_stats.h" +#include "storm/storage/dd/Bdd.h" +#include "storm/storage/dd/DdType.h" namespace symbolicMEC_stats { template struct StateActionPair { storm::dd::Bdd states; - storm::dd::Bdd actions; // [rmnt]: Actions is really state-action pairs. + storm::dd::Bdd actions; // [rmnt]: Actions is really state-action pairs. - StateActionPair& operator|=(StateActionPair const & other) { - states |= other.states; + StateActionPair &operator|=(StateActionPair const &other) { + states |= other.states; actions |= other.actions; return *this; } @@ -24,19 +24,17 @@ struct StateActionPair { // [rmnt] Changed type of scc argument because the earlier one was giving a compiler error. // [rmnt] TODO review this function, seems shady. template -static bool isTrivialSccWithoutSelfEdge_stats(storm::dd::Bdd const & scc, - storm::dd::Bdd const & transitionsWithActions, - std::vector> const & metaVariablesRowColumnPairs, - uint_fast64_t &countSymbolicOps) { - bool isTrivialScc = (1 == scc.getNonZeroCount()); // [rmnt] TODO : Check if this should be counted as a symbolic op +static bool isTrivialSccWithoutSelfEdge_stats( + storm::dd::Bdd const &scc, storm::dd::Bdd const &transitionsWithActions, + std::vector> const &metaVariablesRowColumnPairs, uint_fast64_t &countSymbolicOps) { + bool isTrivialScc = (1 == scc.getNonZeroCount()); // [rmnt] TODO : Check if this should be counted as a symbolic op countSymbolicOps++; - if (! isTrivialScc) + if (!isTrivialScc) return false; bool noSelfEdge = (transitionsWithActions && scc && scc.swapVariables(metaVariablesRowColumnPairs)).isZero(); return noSelfEdge; } - /* Given a set of vertices T, the random attractor Attr_R(T) * is a set of vertices consisting of * (1) T, @@ -44,24 +42,22 @@ static bool isTrivialSccWithoutSelfEdge_stats(storm::dd::Bdd const & scc, * (3) player-1 vertices with all outgoing edges in Attr_R(T). */ template -static StateActionPair computeRandomAttractor_stats(storm::dd::Bdd const & actionsToApplyOn, - storm::dd::Bdd const & allStates, - storm::dd::Bdd const & transitionsWithActions, - std::set const & metaVariablesColumn, - std::set const & metaVariablesActions, - std::vector> const & metaVariablesRowColumnPairs, - uint_fast64_t &countSymbolicOps) { - StateActionPair nextSet = { .states = allStates.getDdManager().getBddZero(), .actions = actionsToApplyOn }; +static StateActionPair computeRandomAttractor_stats( + storm::dd::Bdd const &actionsToApplyOn, storm::dd::Bdd const &allStates, storm::dd::Bdd const &transitionsWithActions, + std::set const &metaVariablesColumn, std::set const &metaVariablesActions, + std::vector> const &metaVariablesRowColumnPairs, uint_fast64_t &countSymbolicOps) { + StateActionPair nextSet = {.states = allStates.getDdManager().getBddZero(), .actions = actionsToApplyOn}; StateActionPair currentSet; do { currentSet = nextSet; // Vertices - storm::dd::Bdd actionsCannotIntoCurrent = ( transitionsWithActions && ( ! currentSet.actions) - ).existsAbstract(metaVariablesColumn); // [rmnt]: All (s,a) pairs which aren't included in currentSet + storm::dd::Bdd actionsCannotIntoCurrent = + (transitionsWithActions && (!currentSet.actions)) + .existsAbstract(metaVariablesColumn); // [rmnt]: All (s,a) pairs which aren't included in currentSet countSymbolicOps++; - storm::dd::Bdd newVertices = currentSet.actions.existsAbstract(metaVariablesActions) - && ( ! (actionsCannotIntoCurrent.existsAbstract(metaVariablesActions))); + storm::dd::Bdd newVertices = + currentSet.actions.existsAbstract(metaVariablesActions) && (!(actionsCannotIntoCurrent.existsAbstract(metaVariablesActions))); // [rmnt]: All states s such that some (s,a1) in currentSet and all (s,a) pairs in currentSet countSymbolicOps++; nextSet.states = (currentSet.states || newVertices) && allStates; @@ -78,12 +74,11 @@ static StateActionPair computeRandomAttractor_stats(storm::dd::Bdd c // For a set of states S, // return all actions which have a non-zero-probability of leaving S. template -static storm::dd::Bdd ROut_stats(storm::dd::Bdd const & sccStates, - storm::dd::Bdd const & transitionsWithActions, - std::set const & metaVariablesColumn, - std::vector> const & metaVariablesRowColumnPairs, - uint_fast64_t &countSymbolicOps) { - storm::dd::Bdd transitionsFromSccToOutside = sccStates && transitionsWithActions && ( ! sccStates.swapVariables(metaVariablesRowColumnPairs)); +static storm::dd::Bdd ROut_stats(storm::dd::Bdd const &sccStates, storm::dd::Bdd const &transitionsWithActions, + std::set const &metaVariablesColumn, + std::vector> const &metaVariablesRowColumnPairs, + uint_fast64_t &countSymbolicOps) { + storm::dd::Bdd transitionsFromSccToOutside = sccStates && transitionsWithActions && (!sccStates.swapVariables(metaVariablesRowColumnPairs)); storm::dd::Bdd actionsLeavingScc = transitionsFromSccToOutside.existsAbstract(metaVariablesColumn); countSymbolicOps++; return actionsLeavingScc; @@ -92,21 +87,18 @@ static storm::dd::Bdd ROut_stats(storm::dd::Bdd const & sccStates, // As described in // "Symbolic algorithms for graphs and Markov decision processes with fairness objectives" template -std::vector> symbolicMECDecompositionNaive_stats(storm::dd::Bdd const & allStates, - storm::dd::Bdd const & transitionsWithActions, - std::set const & metaVariablesRow, - std::set const & metaVariablesColumn, - std::set const & metaVariablesActions, - std::vector> const & metaVariablesRowColumnPairs, - uint_fast64_t &countSymbolicOps) { +std::vector> symbolicMECDecompositionNaive_stats( + storm::dd::Bdd const &allStates, storm::dd::Bdd const &transitionsWithActions, std::set const &metaVariablesRow, + std::set const &metaVariablesColumn, std::set const &metaVariablesActions, + std::vector> const &metaVariablesRowColumnPairs, uint_fast64_t &countSymbolicOps) { storm::dd::Bdd workingCopyTransitionsWithActions(transitionsWithActions); std::vector> result{}; std::stack> mecCandidates{}; - for (const auto& scc : symbolicSCC_stats::decomposition_stats(allStates, workingCopyTransitionsWithActions.existsAbstract(metaVariablesActions), - metaVariablesRow, metaVariablesColumn, countSymbolicOps)) { + for (const auto &scc : symbolicSCC_stats::decomposition_stats( + allStates, workingCopyTransitionsWithActions.existsAbstract(metaVariablesActions), metaVariablesRow, metaVariablesColumn, countSymbolicOps)) { mecCandidates.push(scc); } - while ( ! mecCandidates.empty()) { + while (!mecCandidates.empty()) { storm::dd::Bdd scc = mecCandidates.top(); mecCandidates.pop(); @@ -114,25 +106,24 @@ std::vector> symbolicMECDecompositionNaive_stats(storm::dd: continue; } - storm::dd::Bdd sccROut = ROut_stats(scc, workingCopyTransitionsWithActions, - metaVariablesColumn, metaVariablesRowColumnPairs, countSymbolicOps); + storm::dd::Bdd sccROut = ROut_stats(scc, workingCopyTransitionsWithActions, metaVariablesColumn, metaVariablesRowColumnPairs, countSymbolicOps); if (sccROut.isZero()) { result.template emplace_back(scc); } else { - StateActionPair attractor = computeRandomAttractor_stats(sccROut, scc, workingCopyTransitionsWithActions, - metaVariablesColumn, metaVariablesActions, metaVariablesRowColumnPairs, countSymbolicOps); + StateActionPair attractor = computeRandomAttractor_stats(sccROut, scc, workingCopyTransitionsWithActions, metaVariablesColumn, + metaVariablesActions, metaVariablesRowColumnPairs, countSymbolicOps); workingCopyTransitionsWithActions &= !attractor.actions; - countSymbolicOps++; // [rmnt] For the existsAbstract call in args to scc decomp - for (auto const& subScc : symbolicSCC_stats::decomposition_stats( - scc && !attractor.states, workingCopyTransitionsWithActions.existsAbstract(metaVariablesActions), - metaVariablesRow, metaVariablesColumn, countSymbolicOps)) { + countSymbolicOps++; // [rmnt] For the existsAbstract call in args to scc decomp + for (auto const &subScc : symbolicSCC_stats::decomposition_stats( + scc && !attractor.states, workingCopyTransitionsWithActions.existsAbstract(metaVariablesActions), metaVariablesRow, metaVariablesColumn, + countSymbolicOps)) { mecCandidates.push(subScc); } } - std::cout << "DEBUG Transition BDD stats: " - << workingCopyTransitionsWithActions.getNonZeroCount() << " Transitions (" << workingCopyTransitionsWithActions.getNodeCount() << " nodes), " - << workingCopyTransitionsWithActions.existsAbstract(metaVariablesActions).getNonZeroCount() << " Transitions (" << workingCopyTransitionsWithActions.existsAbstract(metaVariablesActions).getNodeCount() << " nodes)" - << std::endl; + std::cout << "DEBUG Transition BDD stats: " << workingCopyTransitionsWithActions.getNonZeroCount() << " Transitions (" + << workingCopyTransitionsWithActions.getNodeCount() << " nodes), " + << workingCopyTransitionsWithActions.existsAbstract(metaVariablesActions).getNonZeroCount() << " Transitions (" + << workingCopyTransitionsWithActions.existsAbstract(metaVariablesActions).getNodeCount() << " nodes)" << std::endl; } return result; } @@ -141,28 +132,26 @@ std::vector> symbolicMECDecompositionNaive_stats(storm::dd: // "Symbolic Algorithms for Graphs and Markov Decision Processes with Fairness Objectives" // Slightly simplified we only care about the bottom scc template -storm::dd::Bdd LockStepSearch_stats(storm::dd::Bdd const & states, // S - storm::dd::Bdd const & statesWithRemovedEdges, // T_S - storm::dd::Bdd const & transitionsWithoutActions, - std::set const & metaVariablesRow, - std::set const & metaVariablesColumn, - uint_fast64_t &countSymbolicOps) { +storm::dd::Bdd LockStepSearch_stats(storm::dd::Bdd const &states, // S + storm::dd::Bdd const &statesWithRemovedEdges, // T_S + storm::dd::Bdd const &transitionsWithoutActions, std::set const &metaVariablesRow, + std::set const &metaVariablesColumn, uint_fast64_t &countSymbolicOps) { storm::dd::Bdd ts = storm::dd::Bdd(statesWithRemovedEdges); std::unordered_map, storm::dd::Bdd> c{}; - while ( ! ts.isZero()) { + while (!ts.isZero()) { storm::dd::Bdd v = pick_stats(ts, countSymbolicOps); - ts &= ! v; + ts &= !v; c[v] = storm::dd::Bdd(v); } ts = storm::dd::Bdd(statesWithRemovedEdges); while (true) { - for (auto it = c.cbegin(); it != c.cend(); ) { + for (auto it = c.cbegin(); it != c.cend();) { storm::dd::Bdd t = storm::dd::Bdd(it->first); storm::dd::Bdd ct = storm::dd::Bdd(it->second); storm::dd::Bdd ctNew = ct || post_stats(ct, states, transitionsWithoutActions, metaVariablesRow, metaVariablesColumn, countSymbolicOps); - if ((ctNew && ts).getNonZeroCount() > 1) { // [rmnt] there was another state in T_S in the same SCC as t, so we can ignore t. - ts &= ! t; + if ((ctNew && ts).getNonZeroCount() > 1) { // [rmnt] there was another state in T_S in the same SCC as t, so we can ignore t. + ts &= !t; c.erase(it++); } else { if (ctNew == ct) { @@ -179,81 +168,82 @@ storm::dd::Bdd LockStepSearch_stats(storm::dd::Bdd const & states, / // "Symbolic Algorithms for Graphs and Markov Decision Processes with Fairness Objectives" // Uses a lockstep search template -std::vector> symbolicMECDecompositionLockstep_stats(storm::dd::Bdd const & allStates, - storm::dd::Bdd const & transitionsWithActions, - std::set const & metaVariablesRow, - std::set const & metaVariablesColumn, - std::set const & metaVariablesActions, - std::vector> const & metaVariablesRowColumnPairs, - uint_fast64_t &countSymbolicOps) { +std::vector> symbolicMECDecompositionLockstep_stats( + storm::dd::Bdd const &allStates, storm::dd::Bdd const &transitionsWithActions, std::set const &metaVariablesRow, + std::set const &metaVariablesColumn, std::set const &metaVariablesActions, + std::vector> const &metaVariablesRowColumnPairs, uint_fast64_t &countSymbolicOps) { struct MecCandidate { - storm::dd::Bdd states; // In paper: S - storm::dd::Bdd statesWithRemovedEdge; // In Paper: T_s + storm::dd::Bdd states; // In paper: S + storm::dd::Bdd statesWithRemovedEdge; // In Paper: T_s }; // Helper function for better readability - auto hasAtLeastOneEdge_stats = - [metaVariablesActions, metaVariablesRow, metaVariablesColumn, metaVariablesRowColumnPairs] - (storm::dd::Bdd scc, storm::dd::Bdd transitionsWithActions, uint_fast64_t &countSymbolicOps) { - countSymbolicOps++; // [rmnt] For the exists abstract in the arguments + auto hasAtLeastOneEdge_stats = [metaVariablesActions, metaVariablesRow, metaVariablesColumn, metaVariablesRowColumnPairs]( + storm::dd::Bdd scc, storm::dd::Bdd transitionsWithActions, uint_fast64_t &countSymbolicOps) { + countSymbolicOps++; // [rmnt] For the exists abstract in the arguments // Paper suggestion - return ! (post_stats(scc, scc, transitionsWithActions.existsAbstract(metaVariablesActions), metaVariablesRow, metaVariablesColumn, countSymbolicOps)).isZero(); + return !(post_stats(scc, scc, transitionsWithActions.existsAbstract(metaVariablesActions), metaVariablesRow, metaVariablesColumn, countSymbolicOps)) + .isZero(); }; - countSymbolicOps++; // [rmnt] exists - countSymbolicOps++; // [rmnt] getNonZeroCount + countSymbolicOps++; // [rmnt] exists + countSymbolicOps++; // [rmnt] getNonZeroCount uint_fast64_t m = (transitionsWithActions.existsAbstract(metaVariablesActions) && allStates).getNonZeroCount(); storm::dd::Bdd workingCopyTransitionsWithActions(transitionsWithActions); - std::vector> result{}; // In paper: "goodC" - std::stack mecCandidates{}; // In paper: X - countSymbolicOps++; // [rmnt] For the exists abstract in the arguments - for (const auto & scc : symbolicSCC_stats::decomposition_stats(allStates, workingCopyTransitionsWithActions.existsAbstract(metaVariablesActions), metaVariablesRow, metaVariablesColumn, countSymbolicOps)) { - MecCandidate pair = { scc, scc.getDdManager().getBddZero() }; + std::vector> result{}; // In paper: "goodC" + std::stack mecCandidates{}; // In paper: X + countSymbolicOps++; // [rmnt] For the exists abstract in the arguments + for (const auto &scc : symbolicSCC_stats::decomposition_stats( + allStates, workingCopyTransitionsWithActions.existsAbstract(metaVariablesActions), metaVariablesRow, metaVariablesColumn, countSymbolicOps)) { + MecCandidate pair = {scc, scc.getDdManager().getBddZero()}; mecCandidates.push(pair); } - while ( ! mecCandidates.empty()) { + while (!mecCandidates.empty()) { MecCandidate currentCandidate = mecCandidates.top(); storm::dd::Bdd scc = currentCandidate.states; storm::dd::Bdd sccTs = currentCandidate.statesWithRemovedEdge; mecCandidates.pop(); storm::dd::Bdd sccROut = ROut_stats(scc, workingCopyTransitionsWithActions, metaVariablesColumn, metaVariablesRowColumnPairs, countSymbolicOps); - StateActionPair randomAttractor = computeRandomAttractor_stats(sccROut, scc, workingCopyTransitionsWithActions, metaVariablesColumn, metaVariablesActions, metaVariablesRowColumnPairs, countSymbolicOps); - scc &= ! randomAttractor.states; - workingCopyTransitionsWithActions &= ! randomAttractor.actions; + StateActionPair randomAttractor = computeRandomAttractor_stats(sccROut, scc, workingCopyTransitionsWithActions, metaVariablesColumn, + metaVariablesActions, metaVariablesRowColumnPairs, countSymbolicOps); + scc &= !randomAttractor.states; + workingCopyTransitionsWithActions &= !randomAttractor.actions; countSymbolicOps++; sccTs = (sccTs || randomAttractor.actions.existsAbstract(metaVariablesActions)) && scc; if (hasAtLeastOneEdge_stats(scc, workingCopyTransitionsWithActions, countSymbolicOps)) { if (sccTs.isZero()) { result.template emplace_back(scc); } else if (sccTs.getNonZeroCount() >= sqrt(m)) { - countSymbolicOps++; // [rmnt] for the else if condition - countSymbolicOps++; // [rmnt] for the exists below + countSymbolicOps++; // [rmnt] for the else if condition + countSymbolicOps++; // [rmnt] for the exists below std::vector> subSccs = symbolicSCC_stats::decomposition_stats( scc, workingCopyTransitionsWithActions.existsAbstract(metaVariablesActions), metaVariablesRow, metaVariablesColumn, countSymbolicOps); if (subSccs.size() == 1) { result.template emplace_back(scc); } else { - for (auto const& subScc : subSccs) { + for (auto const &subScc : subSccs) { MecCandidate toProcess = {subScc, scc.getDdManager().getBddZero()}; mecCandidates.push(toProcess); } } } else { - countSymbolicOps++; // [rmnt] for the else if condition + countSymbolicOps++; // [rmnt] for the else if condition // bottomScc is "C" in paper - storm::dd::Bdd bottomScc = LockStepSearch_stats(scc, sccTs, - workingCopyTransitionsWithActions.existsAbstract(metaVariablesActions), - metaVariablesRow, metaVariablesColumn, countSymbolicOps); + storm::dd::Bdd bottomScc = + LockStepSearch_stats(scc, sccTs, workingCopyTransitionsWithActions.existsAbstract(metaVariablesActions), metaVariablesRow, + metaVariablesColumn, countSymbolicOps); if (hasAtLeastOneEdge_stats(bottomScc, workingCopyTransitionsWithActions, countSymbolicOps)) { result.template emplace_back(bottomScc); } - countSymbolicOps++; // [rmnt] for the exists below - storm::dd::Bdd statesLeadingIntoBottomScc = pre_stats(bottomScc, scc, workingCopyTransitionsWithActions.existsAbstract(metaVariablesActions), metaVariablesRow, metaVariablesColumn, countSymbolicOps); - mecCandidates.emplace((MecCandidate) { - scc && ( ! bottomScc), - (scc && ( ! bottomScc)) && (statesLeadingIntoBottomScc || sccTs), + countSymbolicOps++; // [rmnt] for the exists below + storm::dd::Bdd statesLeadingIntoBottomScc = + pre_stats(bottomScc, scc, workingCopyTransitionsWithActions.existsAbstract(metaVariablesActions), metaVariablesRow, metaVariablesColumn, + countSymbolicOps); + mecCandidates.emplace((MecCandidate){ + scc && (!bottomScc), + (scc && (!bottomScc)) && (statesLeadingIntoBottomScc || sccTs), }); } } @@ -263,46 +253,40 @@ std::vector> symbolicMECDecompositionLockstep_stats(storm:: // [rmnt] Iterative version of the algorithm in my thesis template -std::vector> symbolicMECDecompositionInterleave_stats(storm::dd::Bdd const & allStates, - storm::dd::Bdd const & transitionsWithActions, - std::set const & metaVariablesRow, - std::set const & metaVariablesColumn, - std::set const & metaVariablesActions, - std::vector> const & metaVariablesRowColumnPairs, - uint_fast64_t &countSymbolicOps) { - std::vector< storm::dd::Bdd > result; - if (allStates.isZero()) { return result; } +std::vector> symbolicMECDecompositionInterleave_stats( + storm::dd::Bdd const &allStates, storm::dd::Bdd const &transitionsWithActions, std::set const &metaVariablesRow, + std::set const &metaVariablesColumn, std::set const &metaVariablesActions, + std::vector> const &metaVariablesRowColumnPairs, uint_fast64_t &countSymbolicOps) { + std::vector> result; + if (allStates.isZero()) { + return result; + } storm::dd::Bdd workingCopyTransitionsWithActions(transitionsWithActions); storm::dd::Bdd transitionsWithoutActions = transitionsWithActions.existsAbstract(metaVariablesActions); // [rmnt] TODO check if this (exists action first then relational product(exists state)) // is better or (states and transitions then exists (state, actions)) - countSymbolicOps++; // [rmnt] For the existsAbstract above + countSymbolicOps++; // [rmnt] For the existsAbstract above - std::stack< InterleaveDecompTask > workStack; + std::stack> workStack; { - InterleaveDecompTask initTask = { allStates, allStates.getDdManager().getBddZero() }; + InterleaveDecompTask initTask = {allStates, allStates.getDdManager().getBddZero()}; workStack.emplace(initTask); } - while (! workStack.empty()) - { - storm::dd::Bdd sccStartState = allStates.getDdManager().getBddZero(), - newStartState = allStates.getDdManager().getBddZero(), - V2 = allStates.getDdManager().getBddZero(), - V3 = allStates.getDdManager().getBddZero(); + while (!workStack.empty()) { + storm::dd::Bdd sccStartState = allStates.getDdManager().getBddZero(), newStartState = allStates.getDdManager().getBddZero(), + V2 = allStates.getDdManager().getBddZero(), V3 = allStates.getDdManager().getBddZero(); - { // task Scope Start + { // task Scope Start InterleaveDecompTask task = workStack.top(); workStack.pop(); - if (task.startState.isZero()) - { - task.startState = pick_stats(task.states, countSymbolicOps); // [rmnt] TODO try pickv2 or other versions + if (task.startState.isZero()) { + task.startState = pick_stats(task.states, countSymbolicOps); // [rmnt] TODO try pickv2 or other versions } - - { // fwdStartState Scope Start + { // fwdStartState Scope Start storm::dd::Bdd fwdStartState = allStates.getDdManager().getBddZero(); // Inlined SCC-Fwd-Start function @@ -310,83 +294,74 @@ std::vector> symbolicMECDecompositionInterleave_stats(storm // Forward set computation storm::dd::Bdd prevLevel = allStates.getDdManager().getBddZero(); storm::dd::Bdd level = task.startState; - while (! level.isZero()) { + while (!level.isZero()) { fwdStartState |= level; prevLevel = level; - level = post_stats(level, task.states && (!fwdStartState), transitionsWithoutActions, metaVariablesRow, metaVariablesColumn, countSymbolicOps); + level = post_stats(level, task.states && (!fwdStartState), transitionsWithoutActions, metaVariablesRow, metaVariablesColumn, + countSymbolicOps); // [rmnt] TODO do && !fwd in arg or after getting result? } // Pick new start state as any state in the last layer - newStartState = pick_stats(prevLevel, countSymbolicOps); + newStartState = pick_stats(prevLevel, countSymbolicOps); // Compute SCC by backward computation level = task.startState; - while (! level.isZero()) - { + while (!level.isZero()) { sccStartState |= level; - level = pre_stats(level, task.states && fwdStartState && (!sccStartState), transitionsWithoutActions, - metaVariablesRow, metaVariablesColumn, countSymbolicOps); + level = pre_stats(level, task.states && fwdStartState && (!sccStartState), transitionsWithoutActions, metaVariablesRow, + metaVariablesColumn, countSymbolicOps); // [rmnt] TODO do the &&s in the argument or after getting result? } } // V1 (reuse sccStartState), V2, V3 are for the recursive call tasks - V2 = fwdStartState && (! sccStartState); - V3 = task.states && (! fwdStartState); + V2 = fwdStartState && (!sccStartState); + V3 = task.states && (!fwdStartState); - } // fwdStartState Scope End + } // fwdStartState Scope End - { // ROut1 Scope Start - storm::dd::Bdd ROut1 = ROut_stats( - sccStartState, workingCopyTransitionsWithActions, metaVariablesColumn, - metaVariablesRowColumnPairs, countSymbolicOps - ); + { // ROut1 Scope Start + storm::dd::Bdd ROut1 = + ROut_stats(sccStartState, workingCopyTransitionsWithActions, metaVariablesColumn, metaVariablesRowColumnPairs, countSymbolicOps); if (ROut1.isZero()) { - if (! isTrivialSccWithoutSelfEdge_stats(sccStartState, workingCopyTransitionsWithActions, metaVariablesRowColumnPairs, countSymbolicOps)) - { result.emplace_back(sccStartState); } - - sccStartState = allStates.getDdManager().getBddZero(); // So that the first recursive call doesn't happen - } - else { - StateActionPair Attr1 = computeRandomAttractor_stats( - ROut1, sccStartState, workingCopyTransitionsWithActions, - metaVariablesColumn, metaVariablesActions, metaVariablesRowColumnPairs, - countSymbolicOps - ); - workingCopyTransitionsWithActions &= (! Attr1.actions); - sccStartState &= (! Attr1.states); // For V1, reusing this + if (!isTrivialSccWithoutSelfEdge_stats(sccStartState, workingCopyTransitionsWithActions, metaVariablesRowColumnPairs, countSymbolicOps)) { + result.emplace_back(sccStartState); + } + + sccStartState = allStates.getDdManager().getBddZero(); // So that the first recursive call doesn't happen + } else { + StateActionPair Attr1 = computeRandomAttractor_stats(ROut1, sccStartState, workingCopyTransitionsWithActions, metaVariablesColumn, + metaVariablesActions, metaVariablesRowColumnPairs, countSymbolicOps); + workingCopyTransitionsWithActions &= (!Attr1.actions); + sccStartState &= (!Attr1.states); // For V1, reusing this } - } // ROut1 Scope End - - { // ROut3 Scope Start - storm::dd::Bdd ROut3 = ROut_stats( - V3, workingCopyTransitionsWithActions, metaVariablesColumn, - metaVariablesRowColumnPairs, countSymbolicOps - ); - if (! ROut3.isZero()) { - StateActionPair Attr3 = computeRandomAttractor_stats( - ROut3, V3, workingCopyTransitionsWithActions, - metaVariablesColumn, metaVariablesActions, metaVariablesRowColumnPairs, - countSymbolicOps - ); - workingCopyTransitionsWithActions &= (! Attr3.actions); - V3 &= (! Attr3.states); // For V3, reusing this + } // ROut1 Scope End + + { // ROut3 Scope Start + storm::dd::Bdd ROut3 = + ROut_stats(V3, workingCopyTransitionsWithActions, metaVariablesColumn, metaVariablesRowColumnPairs, countSymbolicOps); + if (!ROut3.isZero()) { + StateActionPair Attr3 = computeRandomAttractor_stats(ROut3, V3, workingCopyTransitionsWithActions, metaVariablesColumn, + metaVariablesActions, metaVariablesRowColumnPairs, countSymbolicOps); + workingCopyTransitionsWithActions &= (!Attr3.actions); + V3 &= (!Attr3.states); // For V3, reusing this } - } // ROut3 Scope End - } // task Scope End + } // ROut3 Scope End + } // task Scope End // Get the sizes of each (potential) recursive call. Do them in order from smallest to largest // So push on stack in order from largest to smallest - uint_fast64_t sizes[3] = { sccStartState.getNonZeroCount(), V2.getNonZeroCount(), V3.getNonZeroCount() }; - uint8_t order[3] = { 1, 2, 3 }; + uint_fast64_t sizes[3] = {sccStartState.getNonZeroCount(), V2.getNonZeroCount(), V3.getNonZeroCount()}; + uint8_t order[3] = {1, 2, 3}; // Sort order and sizes based on sizes { if (sizes[0] > sizes[1]) { - order[1] = 1; order[0] = 2; + order[1] = 1; + order[0] = 2; uint_fast64_t temp = sizes[0]; sizes[0] = sizes[1]; sizes[1] = temp; @@ -412,20 +387,20 @@ std::vector> symbolicMECDecompositionInterleave_stats(storm } } - for(uint8_t i=0; i<3; i++) { - if ( order[2-i] == 1) { - if ( sizes[2-i] != 0 ) { - InterleaveDecompTask newTask = { sccStartState, allStates.getDdManager().getBddZero() }; + for (uint8_t i = 0; i < 3; i++) { + if (order[2 - i] == 1) { + if (sizes[2 - i] != 0) { + InterleaveDecompTask newTask = {sccStartState, allStates.getDdManager().getBddZero()}; workStack.emplace(newTask); } - } else if ( order[2-i] == 2 ) { - if ( sizes[2-i] != 0 ) { - InterleaveDecompTask newTask = { V2, newStartState }; + } else if (order[2 - i] == 2) { + if (sizes[2 - i] != 0) { + InterleaveDecompTask newTask = {V2, newStartState}; workStack.emplace(newTask); } } else { - if ( sizes[2-i] != 0 ) { - InterleaveDecompTask newTask = { V3, allStates.getDdManager().getBddZero() }; + if (sizes[2 - i] != 0) { + InterleaveDecompTask newTask = {V3, allStates.getDdManager().getBddZero()}; workStack.emplace(newTask); } } @@ -435,6 +410,6 @@ std::vector> symbolicMECDecompositionInterleave_stats(storm return result; } -} // namespace symbolicMEC_stats +} // namespace symbolicMEC_stats #endif \ No newline at end of file diff --git a/src/storm/storage/SymbolicOperations.h b/src/storm/storage/SymbolicOperations.h index 872111a1d9..3355faa0fa 100644 --- a/src/storm/storage/SymbolicOperations.h +++ b/src/storm/storage/SymbolicOperations.h @@ -6,13 +6,13 @@ #include "storm/storage/expressions/SimpleValuation.h" template -static storm::dd::Bdd pick(storm::dd::Bdd const & states) { - assert (states.getNonZeroCount() > 0); - storm::dd::DdManager const & manager = states.getDdManager(); +static storm::dd::Bdd pick(storm::dd::Bdd const& states) { + assert(states.getNonZeroCount() > 0); + storm::dd::DdManager const& manager = states.getDdManager(); storm::dd::Add add = states.template toAdd(); storm::expressions::SimpleValuation firstNonZeroAssigned = (*add.begin()).first; storm::dd::Bdd result = manager.getBddOne(); - for (auto && variable : add.getContainedMetaVariables()) { + for (auto&& variable : add.getContainedMetaVariables()) { // Get Value to encode int_fast64_t value = 0; { @@ -24,43 +24,39 @@ static storm::dd::Bdd pick(storm::dd::Bdd const & states) { value = firstNonZeroAssigned.getIntegerValue(variable); } else { // How do I even convert this to int_fast64_t for the 'getEncoding'-call? - assert( ! "Unexpected variable type" ); + assert(!"Unexpected variable type"); } } // Copy value encoding of meta variable onto BDD result &= manager.getEncoding(variable, value); } - assert (result.getNonZeroCount() == 1); + assert(result.getNonZeroCount() == 1); return result; } // [rmnt] Adding new pick version to see if it's faster. template -static storm::dd::Bdd pickv2(storm::dd::Bdd const & states) { - assert (! states.isZero()); +static storm::dd::Bdd pickv2(storm::dd::Bdd const& states) { + assert(!states.isZero()); storm::dd::Bdd result = states.existsAbstractRepresentative(states.getContainedMetaVariables()); - assert (result.getNonZeroCount() == 1); + assert(result.getNonZeroCount() == 1); return result; } // NOTE(Felix): Modified from dd.cpp:computeReachableStates template -static storm::dd::Bdd post(storm::dd::Bdd const & statesToApplyPostOn, - storm::dd::Bdd const & allStates, - storm::dd::Bdd const & transitions, - std::set const & metaVariablesRow, - std::set const & metaVariablesColumn) { +static storm::dd::Bdd post(storm::dd::Bdd const& statesToApplyPostOn, storm::dd::Bdd const& allStates, + storm::dd::Bdd const& transitions, std::set const& metaVariablesRow, + std::set const& metaVariablesColumn) { return allStates && statesToApplyPostOn.relationalProduct(transitions, metaVariablesRow, metaVariablesColumn); } // NOTE(Felix): Modified from dd.cpp:computeBackwardsReachableStates template -static storm::dd::Bdd pre(storm::dd::Bdd const & statesToApplyPreOn, - storm::dd::Bdd const & allStates, - storm::dd::Bdd const & transitions, - std::set const & metaVariablesRow, - std::set const & metaVariablesColumn) { +static storm::dd::Bdd pre(storm::dd::Bdd const& statesToApplyPreOn, storm::dd::Bdd const& allStates, storm::dd::Bdd const& transitions, + std::set const& metaVariablesRow, + std::set const& metaVariablesColumn) { return allStates && statesToApplyPreOn.inverseRelationalProduct(transitions, metaVariablesRow, metaVariablesColumn); } diff --git a/src/storm/storage/SymbolicOperations_stats.h b/src/storm/storage/SymbolicOperations_stats.h index 9c31a957a6..4be457a595 100644 --- a/src/storm/storage/SymbolicOperations_stats.h +++ b/src/storm/storage/SymbolicOperations_stats.h @@ -6,14 +6,14 @@ #include "storm/storage/expressions/SimpleValuation.h" template -static storm::dd::Bdd pick_stats(storm::dd::Bdd const & states, uint_fast64_t &countSymbolicOps) { - assert (states.getNonZeroCount() > 0); - countSymbolicOps++; // [rmnt] TODO : Counting each pick as one symbolic op. Ok? - storm::dd::DdManager const & manager = states.getDdManager(); +static storm::dd::Bdd pick_stats(storm::dd::Bdd const &states, uint_fast64_t &countSymbolicOps) { + assert(states.getNonZeroCount() > 0); + countSymbolicOps++; // [rmnt] TODO : Counting each pick as one symbolic op. Ok? + storm::dd::DdManager const &manager = states.getDdManager(); storm::dd::Add add = states.template toAdd(); storm::expressions::SimpleValuation firstNonZeroAssigned = (*add.begin()).first; storm::dd::Bdd result = manager.getBddOne(); - for (auto && variable : add.getContainedMetaVariables()) { + for (auto &&variable : add.getContainedMetaVariables()) { // Get Value to encode int_fast64_t value = 0; { @@ -25,48 +25,42 @@ static storm::dd::Bdd pick_stats(storm::dd::Bdd const & states, uint value = firstNonZeroAssigned.getIntegerValue(variable); } else { // How do I even convert this to int_fast64_t for the 'getEncoding'-call? - assert( ! "Unexpected variable type" ); + assert(!"Unexpected variable type"); } } // Copy value encoding of meta variable onto BDD result &= manager.getEncoding(variable, value); } - assert (result.getNonZeroCount() == 1); + assert(result.getNonZeroCount() == 1); return result; } // [rmnt] Adding new pick version to see if it's faster. template -static storm::dd::Bdd pickv2_stats(storm::dd::Bdd const & states, uint_fast64_t &countSymbolicOps) { - assert (! states.isZero()); - countSymbolicOps++; // [rmnt] TODO : Counting each pick as one symbolic op. Ok? +static storm::dd::Bdd pickv2_stats(storm::dd::Bdd const &states, uint_fast64_t &countSymbolicOps) { + assert(!states.isZero()); + countSymbolicOps++; // [rmnt] TODO : Counting each pick as one symbolic op. Ok? storm::dd::Bdd result = states.existsAbstractRepresentative(states.getContainedMetaVariables()); - assert (result.getNonZeroCount() == 1); + assert(result.getNonZeroCount() == 1); return result; } // NOTE(Felix): Modified from dd.cpp:computeReachableStates template -static storm::dd::Bdd post_stats(storm::dd::Bdd const & statesToApplyPostOn, - storm::dd::Bdd const & allStates, - storm::dd::Bdd const & transitions, - std::set const & metaVariablesRow, - std::set const & metaVariablesColumn, - uint_fast64_t &countSymbolicOps) { - countSymbolicOps++; // [rmnt] TODO : Counting each post as one symbolic op. Ok? +static storm::dd::Bdd post_stats(storm::dd::Bdd const &statesToApplyPostOn, storm::dd::Bdd const &allStates, + storm::dd::Bdd const &transitions, std::set const &metaVariablesRow, + std::set const &metaVariablesColumn, uint_fast64_t &countSymbolicOps) { + countSymbolicOps++; // [rmnt] TODO : Counting each post as one symbolic op. Ok? return allStates && statesToApplyPostOn.relationalProduct(transitions, metaVariablesRow, metaVariablesColumn); } // NOTE(Felix): Modified from dd.cpp:computeBackwardsReachableStates template -static storm::dd::Bdd pre_stats(storm::dd::Bdd const & statesToApplyPreOn, - storm::dd::Bdd const & allStates, - storm::dd::Bdd const & transitions, - std::set const & metaVariablesRow, - std::set const & metaVariablesColumn, - uint_fast64_t &countSymbolicOps) { - countSymbolicOps++; // [rmnt] TODO : Counting each pre as one symbolic op. Ok? +static storm::dd::Bdd pre_stats(storm::dd::Bdd const &statesToApplyPreOn, storm::dd::Bdd const &allStates, + storm::dd::Bdd const &transitions, std::set const &metaVariablesRow, + std::set const &metaVariablesColumn, uint_fast64_t &countSymbolicOps) { + countSymbolicOps++; // [rmnt] TODO : Counting each pre as one symbolic op. Ok? return allStates && statesToApplyPreOn.inverseRelationalProduct(transitions, metaVariablesRow, metaVariablesColumn); } diff --git a/src/storm/storage/SymbolicSCCDecomposition.h b/src/storm/storage/SymbolicSCCDecomposition.h index ef758d5bd8..54c246ffb6 100644 --- a/src/storm/storage/SymbolicSCCDecomposition.h +++ b/src/storm/storage/SymbolicSCCDecomposition.h @@ -22,7 +22,9 @@ static std::vector> decomposition(storm::dd::Bdd cons std::set const& metaVariablesRow, std::set const& metaVariablesColumn) { std::vector> result = {}; - if (allStates.isZero()) { return result; } + if (allStates.isZero()) { + return result; + } std::stack> workQueue; { TaskEntry initialTask = {allStates, allStates.getDdManager().getBddZero(), allStates.getDdManager().getBddZero()}; @@ -33,7 +35,7 @@ static std::vector> decomposition(storm::dd::Bdd cons while (!workQueue.empty()) { TaskEntry currentTask = workQueue.top(); workQueue.pop(); - assert( ! currentTask.states.isZero()); + assert(!currentTask.states.isZero()); // "Determine the node for which the scc is computed" if (currentTask.node.isZero() && currentTask.s.isZero()) { // Modified to allow for specification of a starting vertex @@ -92,7 +94,9 @@ static std::vector> decomposition(storm::dd::Bdd cons sToCheck, sToCheck && pre(scc && currentTask.s, currentTask.states, transitions, metaVariablesRow, metaVariablesColumn), }; - if ( ! newTask.states.isZero()) { workQueue.push(newTask); } + if (!newTask.states.isZero()) { + workQueue.push(newTask); + } } // "Second recursive call : Computation of the scc's in FW \ SCC" @@ -102,12 +106,14 @@ static std::vector> decomposition(storm::dd::Bdd cons newS && (!scc), newNode && (!scc), }; - if ( ! newTask.states.isZero()) { workQueue.push(newTask); } + if (!newTask.states.isZero()) { + workQueue.push(newTask); + } } } return result; } -} // namespace symbolicSCC +} // namespace symbolicSCC #endif diff --git a/src/storm/storage/SymbolicSCCDecomposition_stats.h b/src/storm/storage/SymbolicSCCDecomposition_stats.h index 57801b8f89..e8e7283a51 100644 --- a/src/storm/storage/SymbolicSCCDecomposition_stats.h +++ b/src/storm/storage/SymbolicSCCDecomposition_stats.h @@ -19,11 +19,13 @@ struct TaskEntry { * (Gentilini, Piazza, Policriti) */ template static std::vector> decomposition_stats(storm::dd::Bdd const& allStates, storm::dd::Bdd const& transitions, - std::set const& metaVariablesRow, - std::set const& metaVariablesColumn, - uint_fast64_t &countSymbolicOps) { + std::set const& metaVariablesRow, + std::set const& metaVariablesColumn, + uint_fast64_t& countSymbolicOps) { std::vector> result = {}; - if (allStates.isZero()) { return result; } + if (allStates.isZero()) { + return result; + } std::stack> workQueue; { TaskEntry initialTask = {allStates, allStates.getDdManager().getBddZero(), allStates.getDdManager().getBddZero()}; @@ -34,7 +36,7 @@ static std::vector> decomposition_stats(storm::dd::Bdd currentTask = workQueue.top(); workQueue.pop(); - assert( ! currentTask.states.isZero()); + assert(!currentTask.states.isZero()); // "Determine the node for which the scc is computed" if (currentTask.node.isZero() && currentTask.s.isZero()) { // Modified to allow for specification of a starting vertex @@ -61,11 +63,12 @@ static std::vector> decomposition_stats(storm::dd::Bdd(level, countSymbolicOps); // TODO: Better Name - newS = storm::dd::Bdd(newNode); // TODO: Better name for this variable + newS = storm::dd::Bdd(newNode); // TODO: Better name for this variable while (!stack.empty()) { level = stack.top(); stack.pop(); - storm::dd::Bdd toPickFrom = level && pre_stats(newS, currentTask.states, transitions, metaVariablesRow, metaVariablesColumn, countSymbolicOps); + storm::dd::Bdd toPickFrom = + level && pre_stats(newS, currentTask.states, transitions, metaVariablesRow, metaVariablesColumn, countSymbolicOps); newS |= pick_stats(toPickFrom, countSymbolicOps); } } @@ -75,7 +78,8 @@ static std::vector> decomposition_stats(storm::dd::Bdd updatedScc = fw && pre_stats(scc, currentTask.states, transitions, metaVariablesRow, metaVariablesColumn, countSymbolicOps); + storm::dd::Bdd updatedScc = + fw && pre_stats(scc, currentTask.states, transitions, metaVariablesRow, metaVariablesColumn, countSymbolicOps); storm::dd::Bdd addedStates = updatedScc && (!scc); scc |= updatedScc; changed = (!addedStates.isZero()); @@ -93,7 +97,9 @@ static std::vector> decomposition_stats(storm::dd::Bdd> decomposition_stats(storm::dd::Bdd -enum class MecBenchmarkType { - NAIVE, - NAIVE_STATS, - LOCKSTEP, - LOCKSTEP_STATS, - INTERLEAVE, - INTERLEAVE_STATS -}; - -MecBenchmarkType debugIntToBenchmarkType(uint64_t forcedMecAlgorithm) -{ - switch(forcedMecAlgorithm) { - case 1 : return MecBenchmarkType::NAIVE; - case 2 : return MecBenchmarkType::NAIVE_STATS; - case 3 : return MecBenchmarkType::LOCKSTEP; - case 4 : return MecBenchmarkType::LOCKSTEP_STATS; - case 5 : return MecBenchmarkType::INTERLEAVE; - case 6 : return MecBenchmarkType::INTERLEAVE_STATS; - default: STORM_LOG_ASSERT(false, "Unexpected symbolic benchmark int"); +enum class MecBenchmarkType { NAIVE, NAIVE_STATS, LOCKSTEP, LOCKSTEP_STATS, INTERLEAVE, INTERLEAVE_STATS }; + +MecBenchmarkType debugIntToBenchmarkType(uint64_t forcedMecAlgorithm) { + switch (forcedMecAlgorithm) { + case 1: + return MecBenchmarkType::NAIVE; + case 2: + return MecBenchmarkType::NAIVE_STATS; + case 3: + return MecBenchmarkType::LOCKSTEP; + case 4: + return MecBenchmarkType::LOCKSTEP_STATS; + case 5: + return MecBenchmarkType::INTERLEAVE; + case 6: + return MecBenchmarkType::INTERLEAVE_STATS; + default: + STORM_LOG_ASSERT(false, "Unexpected symbolic benchmark int"); } STORM_LOG_ASSERT(false, "Unreachable"); } -std::string benchmarkToString(const MecBenchmarkType type) -{ - switch(type) { - case MecBenchmarkType::NAIVE : return "NAIVE"; - case MecBenchmarkType::NAIVE_STATS : return "NAIVE-STATS"; - case MecBenchmarkType::LOCKSTEP : return "LOCKSTEP"; - case MecBenchmarkType::LOCKSTEP_STATS : return "LOCKSTEP-STATS"; - case MecBenchmarkType::INTERLEAVE : return "INTERLEAVE"; - case MecBenchmarkType::INTERLEAVE_STATS : return "INTERLEAVE-STATS"; +std::string benchmarkToString(const MecBenchmarkType type) { + switch (type) { + case MecBenchmarkType::NAIVE: + return "NAIVE"; + case MecBenchmarkType::NAIVE_STATS: + return "NAIVE-STATS"; + case MecBenchmarkType::LOCKSTEP: + return "LOCKSTEP"; + case MecBenchmarkType::LOCKSTEP_STATS: + return "LOCKSTEP-STATS"; + case MecBenchmarkType::INTERLEAVE: + return "INTERLEAVE"; + case MecBenchmarkType::INTERLEAVE_STATS: + return "INTERLEAVE-STATS"; } } @@ -59,9 +63,8 @@ struct BenchmarkResult { void print() { std::string algorithm = benchmarkToString(type); - std::cout << "BENCHMARK MEC DECOMPOSITION (algorithm, time, mecCount): " - << algorithm << ", " << decompositionTimeInNanoseconds << ", " - << mecCount << "\n"; + std::cout << "BENCHMARK MEC DECOMPOSITION (algorithm, time, mecCount): " << algorithm << ", " << decompositionTimeInNanoseconds << ", " << mecCount + << "\n"; } }; @@ -75,77 +78,71 @@ uint_fast64_t getDdVariablesCount(storm::dd::DdManager& manager, std::se } template -BenchmarkResult doSymbolicBenchmark(storm::models::symbolic::NondeterministicModel const& symbolicModel, - MecBenchmarkType type) { - auto & manager = symbolicModel.getManager(); +BenchmarkResult doSymbolicBenchmark(storm::models::symbolic::NondeterministicModel const& symbolicModel, MecBenchmarkType type) { + auto& manager = symbolicModel.getManager(); std::vector> mecs; std::chrono::high_resolution_clock::time_point decompositionTimestampStart; std::chrono::high_resolution_clock::time_point decompositionTimestampEnd; uint_fast64_t countSymbolicOps = 0; - switch (type) - { - case MecBenchmarkType::NAIVE: - decompositionTimestampStart = std::chrono::high_resolution_clock::now(); - mecs = symbolicMEC::symbolicMECDecompositionNaive( - symbolicModel.getReachableStates(), symbolicModel.getTransitionMatrix().toBdd(), - symbolicModel.getRowVariables(), symbolicModel.getColumnVariables(), symbolicModel.getNondeterminismVariables(), - symbolicModel.getRowColumnMetaVariablePairs() - ); - decompositionTimestampEnd = std::chrono::high_resolution_clock::now(); - break; - - case MecBenchmarkType::NAIVE_STATS: - decompositionTimestampStart = std::chrono::high_resolution_clock::now(); - mecs = symbolicMEC_stats::symbolicMECDecompositionNaive_stats( - symbolicModel.getReachableStates(), symbolicModel.getTransitionMatrix().toBdd(), - symbolicModel.getRowVariables(), symbolicModel.getColumnVariables(), symbolicModel.getNondeterminismVariables(), - symbolicModel.getRowColumnMetaVariablePairs(), countSymbolicOps); - decompositionTimestampEnd = std::chrono::high_resolution_clock::now(); - std::cout << "DEBUG SYMBOLIC OPS " << countSymbolicOps << std::endl; - break; - - case MecBenchmarkType::LOCKSTEP: - decompositionTimestampStart = std::chrono::high_resolution_clock::now(); - mecs = symbolicMEC::symbolicMECDecompositionLockstep( - symbolicModel.getReachableStates(), symbolicModel.getTransitionMatrix().toBdd(), - symbolicModel.getRowVariables(), symbolicModel.getColumnVariables(), symbolicModel.getNondeterminismVariables(), - symbolicModel.getRowColumnMetaVariablePairs()); - decompositionTimestampEnd = std::chrono::high_resolution_clock::now(); - break; - - case MecBenchmarkType::LOCKSTEP_STATS: - decompositionTimestampStart = std::chrono::high_resolution_clock::now(); - mecs = symbolicMEC_stats::symbolicMECDecompositionLockstep_stats( - symbolicModel.getReachableStates(), symbolicModel.getTransitionMatrix().toBdd(), - symbolicModel.getRowVariables(), symbolicModel.getColumnVariables(), symbolicModel.getNondeterminismVariables(), - symbolicModel.getRowColumnMetaVariablePairs(), countSymbolicOps); - decompositionTimestampEnd = std::chrono::high_resolution_clock::now(); - std::cout << "DEBUG SYMBOLIC OPS " << countSymbolicOps << std::endl; - break; - - case MecBenchmarkType::INTERLEAVE: - decompositionTimestampStart = std::chrono::high_resolution_clock::now(); - mecs = symbolicMEC::symbolicMECDecompositionInterleave( - symbolicModel.getReachableStates(), symbolicModel.getTransitionMatrix().toBdd(), - symbolicModel.getRowVariables(), symbolicModel.getColumnVariables(), symbolicModel.getNondeterminismVariables(), - symbolicModel.getRowColumnMetaVariablePairs()); - decompositionTimestampEnd = std::chrono::high_resolution_clock::now(); - break; - - case MecBenchmarkType::INTERLEAVE_STATS: - decompositionTimestampStart = std::chrono::high_resolution_clock::now(); - mecs = symbolicMEC_stats::symbolicMECDecompositionInterleave_stats( - symbolicModel.getReachableStates(), symbolicModel.getTransitionMatrix().toBdd(), - symbolicModel.getRowVariables(), symbolicModel.getColumnVariables(), symbolicModel.getNondeterminismVariables(), - symbolicModel.getRowColumnMetaVariablePairs(), countSymbolicOps); - std::cout << "DEBUG SYMBOLIC OPS " << countSymbolicOps << std::endl; - decompositionTimestampEnd = std::chrono::high_resolution_clock::now(); - break; - - default: - STORM_LOG_ASSERT(false, "Unexpected symbolic benchmark type"); - break; + switch (type) { + case MecBenchmarkType::NAIVE: + decompositionTimestampStart = std::chrono::high_resolution_clock::now(); + mecs = symbolicMEC::symbolicMECDecompositionNaive( + symbolicModel.getReachableStates(), symbolicModel.getTransitionMatrix().toBdd(), symbolicModel.getRowVariables(), + symbolicModel.getColumnVariables(), symbolicModel.getNondeterminismVariables(), symbolicModel.getRowColumnMetaVariablePairs()); + decompositionTimestampEnd = std::chrono::high_resolution_clock::now(); + break; + + case MecBenchmarkType::NAIVE_STATS: + decompositionTimestampStart = std::chrono::high_resolution_clock::now(); + mecs = symbolicMEC_stats::symbolicMECDecompositionNaive_stats( + symbolicModel.getReachableStates(), symbolicModel.getTransitionMatrix().toBdd(), symbolicModel.getRowVariables(), + symbolicModel.getColumnVariables(), symbolicModel.getNondeterminismVariables(), symbolicModel.getRowColumnMetaVariablePairs(), + countSymbolicOps); + decompositionTimestampEnd = std::chrono::high_resolution_clock::now(); + std::cout << "DEBUG SYMBOLIC OPS " << countSymbolicOps << std::endl; + break; + + case MecBenchmarkType::LOCKSTEP: + decompositionTimestampStart = std::chrono::high_resolution_clock::now(); + mecs = symbolicMEC::symbolicMECDecompositionLockstep( + symbolicModel.getReachableStates(), symbolicModel.getTransitionMatrix().toBdd(), symbolicModel.getRowVariables(), + symbolicModel.getColumnVariables(), symbolicModel.getNondeterminismVariables(), symbolicModel.getRowColumnMetaVariablePairs()); + decompositionTimestampEnd = std::chrono::high_resolution_clock::now(); + break; + + case MecBenchmarkType::LOCKSTEP_STATS: + decompositionTimestampStart = std::chrono::high_resolution_clock::now(); + mecs = symbolicMEC_stats::symbolicMECDecompositionLockstep_stats( + symbolicModel.getReachableStates(), symbolicModel.getTransitionMatrix().toBdd(), symbolicModel.getRowVariables(), + symbolicModel.getColumnVariables(), symbolicModel.getNondeterminismVariables(), symbolicModel.getRowColumnMetaVariablePairs(), + countSymbolicOps); + decompositionTimestampEnd = std::chrono::high_resolution_clock::now(); + std::cout << "DEBUG SYMBOLIC OPS " << countSymbolicOps << std::endl; + break; + + case MecBenchmarkType::INTERLEAVE: + decompositionTimestampStart = std::chrono::high_resolution_clock::now(); + mecs = symbolicMEC::symbolicMECDecompositionInterleave( + symbolicModel.getReachableStates(), symbolicModel.getTransitionMatrix().toBdd(), symbolicModel.getRowVariables(), + symbolicModel.getColumnVariables(), symbolicModel.getNondeterminismVariables(), symbolicModel.getRowColumnMetaVariablePairs()); + decompositionTimestampEnd = std::chrono::high_resolution_clock::now(); + break; + + case MecBenchmarkType::INTERLEAVE_STATS: + decompositionTimestampStart = std::chrono::high_resolution_clock::now(); + mecs = symbolicMEC_stats::symbolicMECDecompositionInterleave_stats( + symbolicModel.getReachableStates(), symbolicModel.getTransitionMatrix().toBdd(), symbolicModel.getRowVariables(), + symbolicModel.getColumnVariables(), symbolicModel.getNondeterminismVariables(), symbolicModel.getRowColumnMetaVariablePairs(), + countSymbolicOps); + std::cout << "DEBUG SYMBOLIC OPS " << countSymbolicOps << std::endl; + decompositionTimestampEnd = std::chrono::high_resolution_clock::now(); + break; + + default: + STORM_LOG_ASSERT(false, "Unexpected symbolic benchmark type"); + break; } // Output Model stats @@ -153,29 +150,26 @@ BenchmarkResult doSymbolicBenchmark(storm::models::symbolic::NondeterministicMod uint_fast64_t ddColumnVariableCount = getDdVariablesCount(manager, symbolicModel.getColumnVariables()); uint_fast64_t ddNondeterminismCount = getDdVariablesCount(manager, symbolicModel.getNondeterminismVariables()); std::cout << "Symbolic model stats: " << std::endl - << "Type: " << symbolicModel.getType() << std::endl - << "States: " << symbolicModel.getNumberOfStates() << " (" << symbolicModel.getReachableStates().getNodeCount() << " nodes)" - << std::endl - << "Transitions: " << symbolicModel.getNumberOfTransitions() << " (" << symbolicModel.getTransitionMatrix().toBdd().getNodeCount() - << " nodes)" << std::endl - << "Choices: " << symbolicModel.getNumberOfChoices() << std::endl - << "Variables Total: " - << (symbolicModel.getRowVariables().size() + symbolicModel.getColumnVariables().size() + - symbolicModel.getNondeterminismVariables().size()) - << " (" << (ddRowVariableCount + ddColumnVariableCount + ddNondeterminismCount) << " DD variables)" << std::endl - << "Variables Row: " << symbolicModel.getRowVariables().size() << " (" << ddRowVariableCount << " DD variables)" << std::endl - << "Variables Column: " << symbolicModel.getColumnVariables().size() << " (" << ddColumnVariableCount << " DD variables)" << std::endl - << "Variables Nondeterminism: " << symbolicModel.getNondeterminismVariables().size() << " (" << ddNondeterminismCount - << " DD variables)" << std::endl - << std::endl; + << "Type: " << symbolicModel.getType() << std::endl + << "States: " << symbolicModel.getNumberOfStates() << " (" << symbolicModel.getReachableStates().getNodeCount() << " nodes)" << std::endl + << "Transitions: " << symbolicModel.getNumberOfTransitions() << " (" << symbolicModel.getTransitionMatrix().toBdd().getNodeCount() << " nodes)" + << std::endl + << "Choices: " << symbolicModel.getNumberOfChoices() << std::endl + << "Variables Total: " + << (symbolicModel.getRowVariables().size() + symbolicModel.getColumnVariables().size() + symbolicModel.getNondeterminismVariables().size()) + << " (" << (ddRowVariableCount + ddColumnVariableCount + ddNondeterminismCount) << " DD variables)" << std::endl + << "Variables Row: " << symbolicModel.getRowVariables().size() << " (" << ddRowVariableCount << " DD variables)" << std::endl + << "Variables Column: " << symbolicModel.getColumnVariables().size() << " (" << ddColumnVariableCount << " DD variables)" << std::endl + << "Variables Nondeterminism: " << symbolicModel.getNondeterminismVariables().size() << " (" << ddNondeterminismCount << " DD variables)" + << std::endl + << std::endl; uint_fast64_t decompositionTimeInNanoseconds = (decompositionTimestampEnd - decompositionTimestampStart).count(); return BenchmarkResult(type, mecs.size(), decompositionTimeInNanoseconds); } template -void doMecBenchmark(storm::models::ModelBase const& model, - uint64_t forcedMecAlgorithm) { +void doMecBenchmark(storm::models::ModelBase const& model, uint64_t forcedMecAlgorithm) { assert(forcedMecAlgorithm > 0); MecBenchmarkType type = debugIntToBenchmarkType(forcedMecAlgorithm); BenchmarkResult benchmark = doSymbolicBenchmark((storm::models::symbolic::NondeterministicModel&)model, type); diff --git a/src/storm/storage/dd/Bdd.h b/src/storm/storage/dd/Bdd.h index b9f82992a9..a620842dba 100644 --- a/src/storm/storage/dd/Bdd.h +++ b/src/storm/storage/dd/Bdd.h @@ -212,7 +212,7 @@ class Bdd : public Dd { * Gets a cube that satisfies this Bdd. * * @return The BDD representing the cube. - */ + */ Bdd pickOneCube() const; /*! diff --git a/src/storm/storage/dd/cudd/InternalCuddBdd.cpp b/src/storm/storage/dd/cudd/InternalCuddBdd.cpp index d0a1750320..a5f118d487 100644 --- a/src/storm/storage/dd/cudd/InternalCuddBdd.cpp +++ b/src/storm/storage/dd/cudd/InternalCuddBdd.cpp @@ -134,7 +134,7 @@ InternalBdd InternalBdd::pickOneCube() const { std::vector varBdds; // [rmnt] TODO : Does the order of pushing vars matter to perfornance? // [rmnt] See the implementation of Cudd_Support() in cuddUtil.c where this is done in reverse order - for(int index = 0; index < numVars; ++index) { + for (int index = 0; index < numVars; ++index) { varBdds.push_back(ddManager->getCuddManager().bddVar(index)); } return InternalBdd(ddManager, this->getCuddBdd().PickOneMinterm(varBdds)); diff --git a/src/storm/storage/dd/cudd/InternalCuddBdd.h b/src/storm/storage/dd/cudd/InternalCuddBdd.h index 38266a0033..99cd234ed9 100644 --- a/src/storm/storage/dd/cudd/InternalCuddBdd.h +++ b/src/storm/storage/dd/cudd/InternalCuddBdd.h @@ -229,7 +229,7 @@ class InternalBdd { * Gets a cube that satisfies this Bdd. * * @return The BDD representing the cube. - */ + */ InternalBdd pickOneCube() const; /*! diff --git a/src/storm/storage/dd/sylvan/InternalSylvanBdd.h b/src/storm/storage/dd/sylvan/InternalSylvanBdd.h index 2b1235b445..8298012bab 100644 --- a/src/storm/storage/dd/sylvan/InternalSylvanBdd.h +++ b/src/storm/storage/dd/sylvan/InternalSylvanBdd.h @@ -220,7 +220,7 @@ class InternalBdd { * Gets a cube that satisfies this Bdd. * * @return The BDD representing the cube. - */ + */ InternalBdd pickOneCube() const; /*! From 8d4a4479f8057593cb9bb25869aec4ebf5a935a8 Mon Sep 17 00:00:00 2001 From: Ramneet-Singh Date: Mon, 17 Jun 2024 14:29:04 +0530 Subject: [PATCH 13/25] Change Symbolic Ops Benchmark Output --- src/storm/storage/THESIS_DEBUG.h | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/src/storm/storage/THESIS_DEBUG.h b/src/storm/storage/THESIS_DEBUG.h index 88001a14ca..7ec230030a 100644 --- a/src/storm/storage/THESIS_DEBUG.h +++ b/src/storm/storage/THESIS_DEBUG.h @@ -101,7 +101,7 @@ BenchmarkResult doSymbolicBenchmark(storm::models::symbolic::NondeterministicMod symbolicModel.getColumnVariables(), symbolicModel.getNondeterminismVariables(), symbolicModel.getRowColumnMetaVariablePairs(), countSymbolicOps); decompositionTimestampEnd = std::chrono::high_resolution_clock::now(); - std::cout << "DEBUG SYMBOLIC OPS " << countSymbolicOps << std::endl; + std::cout << "BENCHMARK SYMBOLIC OPS (count): " << countSymbolicOps << std::endl; break; case MecBenchmarkType::LOCKSTEP: @@ -119,7 +119,7 @@ BenchmarkResult doSymbolicBenchmark(storm::models::symbolic::NondeterministicMod symbolicModel.getColumnVariables(), symbolicModel.getNondeterminismVariables(), symbolicModel.getRowColumnMetaVariablePairs(), countSymbolicOps); decompositionTimestampEnd = std::chrono::high_resolution_clock::now(); - std::cout << "DEBUG SYMBOLIC OPS " << countSymbolicOps << std::endl; + std::cout << "BENCHMARK SYMBOLIC OPS (count): " << countSymbolicOps << std::endl; break; case MecBenchmarkType::INTERLEAVE: @@ -136,8 +136,8 @@ BenchmarkResult doSymbolicBenchmark(storm::models::symbolic::NondeterministicMod symbolicModel.getReachableStates(), symbolicModel.getTransitionMatrix().toBdd(), symbolicModel.getRowVariables(), symbolicModel.getColumnVariables(), symbolicModel.getNondeterminismVariables(), symbolicModel.getRowColumnMetaVariablePairs(), countSymbolicOps); - std::cout << "DEBUG SYMBOLIC OPS " << countSymbolicOps << std::endl; decompositionTimestampEnd = std::chrono::high_resolution_clock::now(); + std::cout << "BENCHMARK SYMBOLIC OPS (count): " << countSymbolicOps << std::endl; break; default: From 21a8daa1bb69dd068ec9211e25dd49382631c639 Mon Sep 17 00:00:00 2001 From: Ramneet-Singh Date: Mon, 17 Jun 2024 15:00:31 +0530 Subject: [PATCH 14/25] Fix Interleave Stats Bug --- src/storm/storage/SymbolicMEC_stats.h | 13 +++++++++++++ 1 file changed, 13 insertions(+) diff --git a/src/storm/storage/SymbolicMEC_stats.h b/src/storm/storage/SymbolicMEC_stats.h index d77fdc1d84..8802a79d32 100644 --- a/src/storm/storage/SymbolicMEC_stats.h +++ b/src/storm/storage/SymbolicMEC_stats.h @@ -251,6 +251,19 @@ std::vector> symbolicMECDecompositionLockstep_stats( return result; } +template +struct InterleaveDecompTask { + storm::dd::Bdd states; + storm::dd::Bdd startState; + + // Instantiate all copy/move constructors/assignments with the default implementation. + InterleaveDecompTask() = default; + InterleaveDecompTask(InterleaveDecompTask const& other) = default; + InterleaveDecompTask& operator=(InterleaveDecompTask const& other) = default; + InterleaveDecompTask(InterleaveDecompTask&& other) = default; + InterleaveDecompTask& operator=(InterleaveDecompTask&& other) = default; +}; + // [rmnt] Iterative version of the algorithm in my thesis template std::vector> symbolicMECDecompositionInterleave_stats( From 38668b342ba624e5c678251298c932ebcb3ca2cd Mon Sep 17 00:00:00 2001 From: Ramneet-Singh Date: Mon, 17 Jun 2024 15:08:51 +0530 Subject: [PATCH 15/25] Remove Printing Transition BDD Stats --- src/storm/storage/SymbolicMEC_stats.h | 4 ---- 1 file changed, 4 deletions(-) diff --git a/src/storm/storage/SymbolicMEC_stats.h b/src/storm/storage/SymbolicMEC_stats.h index 8802a79d32..fc389ab2ad 100644 --- a/src/storm/storage/SymbolicMEC_stats.h +++ b/src/storm/storage/SymbolicMEC_stats.h @@ -120,10 +120,6 @@ std::vector> symbolicMECDecompositionNaive_stats( mecCandidates.push(subScc); } } - std::cout << "DEBUG Transition BDD stats: " << workingCopyTransitionsWithActions.getNonZeroCount() << " Transitions (" - << workingCopyTransitionsWithActions.getNodeCount() << " nodes), " - << workingCopyTransitionsWithActions.existsAbstract(metaVariablesActions).getNonZeroCount() << " Transitions (" - << workingCopyTransitionsWithActions.existsAbstract(metaVariablesActions).getNodeCount() << " nodes)" << std::endl; } return result; } From 55978e9e9a73b026029d99f8509f094c11551494 Mon Sep 17 00:00:00 2001 From: Ramneet Singh Date: Mon, 17 Jun 2024 16:03:27 +0530 Subject: [PATCH 16/25] Potential Bug Fix --- src/storm/storage/SymbolicMEC.h | 9 +++++---- src/storm/storage/SymbolicMEC_stats.h | 11 ++++++----- 2 files changed, 11 insertions(+), 9 deletions(-) diff --git a/src/storm/storage/SymbolicMEC.h b/src/storm/storage/SymbolicMEC.h index cbc52bf26f..21ae9e3962 100644 --- a/src/storm/storage/SymbolicMEC.h +++ b/src/storm/storage/SymbolicMEC.h @@ -254,9 +254,6 @@ std::vector> symbolicMECDecompositionInterleave( } storm::dd::Bdd workingCopyTransitionsWithActions(transitionsWithActions); - storm::dd::Bdd transitionsWithoutActions = transitionsWithActions.existsAbstract(metaVariablesActions); - // [rmnt] TODO check if this (exists action first then relational product(exists state)) - // is better or (states and transitions then exists (state, actions)) std::stack> workStack; { @@ -281,6 +278,10 @@ std::vector> symbolicMECDecompositionInterleave( // Inlined SCC-Fwd-Start function { + storm::dd::Bdd transitionsWithoutActions = transitionsWithActions.existsAbstract(metaVariablesActions); + // [rmnt] TODO check if this (exists action first then relational product(exists state)) + // is better or (states and transitions then exists (state, actions)) + // Forward set computation storm::dd::Bdd prevLevel = allStates.getDdManager().getBddZero(); storm::dd::Bdd level = task.startState; @@ -398,4 +399,4 @@ std::vector> symbolicMECDecompositionInterleave( } // namespace symbolicMEC -#endif \ No newline at end of file +#endif diff --git a/src/storm/storage/SymbolicMEC_stats.h b/src/storm/storage/SymbolicMEC_stats.h index fc389ab2ad..b6622517a5 100644 --- a/src/storm/storage/SymbolicMEC_stats.h +++ b/src/storm/storage/SymbolicMEC_stats.h @@ -272,10 +272,6 @@ std::vector> symbolicMECDecompositionInterleave_stats( } storm::dd::Bdd workingCopyTransitionsWithActions(transitionsWithActions); - storm::dd::Bdd transitionsWithoutActions = transitionsWithActions.existsAbstract(metaVariablesActions); - // [rmnt] TODO check if this (exists action first then relational product(exists state)) - // is better or (states and transitions then exists (state, actions)) - countSymbolicOps++; // [rmnt] For the existsAbstract above std::stack> workStack; { @@ -300,6 +296,11 @@ std::vector> symbolicMECDecompositionInterleave_stats( // Inlined SCC-Fwd-Start function { + storm::dd::Bdd transitionsWithoutActions = transitionsWithActions.existsAbstract(metaVariablesActions); + // [rmnt] TODO check if this (exists action first then relational product(exists state)) + // is better or (states and transitions then exists (state, actions)) + countSymbolicOps++; // [rmnt] For the existsAbstract above + // Forward set computation storm::dd::Bdd prevLevel = allStates.getDdManager().getBddZero(); storm::dd::Bdd level = task.startState; @@ -421,4 +422,4 @@ std::vector> symbolicMECDecompositionInterleave_stats( } // namespace symbolicMEC_stats -#endif \ No newline at end of file +#endif From 8dbb0584f0f1e296d29755b616d211e698e9b574 Mon Sep 17 00:00:00 2001 From: Ramneet Singh Date: Mon, 17 Jun 2024 17:00:33 +0530 Subject: [PATCH 17/25] Potential Bug Fix --- src/storm/storage/SymbolicMEC.h | 4 ++-- src/storm/storage/SymbolicMEC_stats.h | 4 ++-- 2 files changed, 4 insertions(+), 4 deletions(-) diff --git a/src/storm/storage/SymbolicMEC.h b/src/storm/storage/SymbolicMEC.h index 21ae9e3962..47345c5eeb 100644 --- a/src/storm/storage/SymbolicMEC.h +++ b/src/storm/storage/SymbolicMEC.h @@ -278,7 +278,7 @@ std::vector> symbolicMECDecompositionInterleave( // Inlined SCC-Fwd-Start function { - storm::dd::Bdd transitionsWithoutActions = transitionsWithActions.existsAbstract(metaVariablesActions); + storm::dd::Bdd transitionsWithoutActions = workingCopyTransitionsWithActions.existsAbstract(metaVariablesActions); // [rmnt] TODO check if this (exists action first then relational product(exists state)) // is better or (states and transitions then exists (state, actions)) @@ -382,7 +382,7 @@ std::vector> symbolicMECDecompositionInterleave( } } else if (order[2 - i] == 2) { if (sizes[2 - i] != 0) { - InterleaveDecompTask newTask = {V2, newStartState}; + InterleaveDecompTask newTask = {V2, newStartState && V2}; workStack.emplace(newTask); } } else { diff --git a/src/storm/storage/SymbolicMEC_stats.h b/src/storm/storage/SymbolicMEC_stats.h index b6622517a5..119a94d4f8 100644 --- a/src/storm/storage/SymbolicMEC_stats.h +++ b/src/storm/storage/SymbolicMEC_stats.h @@ -296,7 +296,7 @@ std::vector> symbolicMECDecompositionInterleave_stats( // Inlined SCC-Fwd-Start function { - storm::dd::Bdd transitionsWithoutActions = transitionsWithActions.existsAbstract(metaVariablesActions); + storm::dd::Bdd transitionsWithoutActions = workingCopyTransitionsWithActions.existsAbstract(metaVariablesActions); // [rmnt] TODO check if this (exists action first then relational product(exists state)) // is better or (states and transitions then exists (state, actions)) countSymbolicOps++; // [rmnt] For the existsAbstract above @@ -405,7 +405,7 @@ std::vector> symbolicMECDecompositionInterleave_stats( } } else if (order[2 - i] == 2) { if (sizes[2 - i] != 0) { - InterleaveDecompTask newTask = {V2, newStartState}; + InterleaveDecompTask newTask = {V2, newStartState && V2}; workStack.emplace(newTask); } } else { From d06835b5977d1c3765c636904ff48c6ba7fc16d6 Mon Sep 17 00:00:00 2001 From: Ramneet-Singh Date: Wed, 26 Jun 2024 01:02:08 +0530 Subject: [PATCH 18/25] Add Acknowledgment to Felix --- README.md | 1 + 1 file changed, 1 insertion(+) diff --git a/README.md b/README.md index 197c49084b..6a7d9ddd9c 100644 --- a/README.md +++ b/README.md @@ -5,6 +5,7 @@ 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". Most of the code (except the new algorithm added -- `INTERLEAVE`) 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. Usage ----------------------------- From 433363caedadcaa8b8331cff5d5fba66a13eeea8 Mon Sep 17 00:00:00 2001 From: Ramneet Singh <63390014+Ramneet-Singh@users.noreply.github.com> Date: Thu, 18 Jul 2024 19:31:26 +0530 Subject: [PATCH 19/25] Update README.md --- README.md | 4 +++- 1 file changed, 3 insertions(+), 1 deletion(-) diff --git a/README.md b/README.md index 6a7d9ddd9c..920123199f 100644 --- a/README.md +++ b/README.md @@ -5,7 +5,9 @@ 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". Most of the code (except the new algorithm added -- `INTERLEAVE`) 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. +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`) 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. The files `src/storm/storage/SymbolicMEC.h` and `src/storm/storage/SymbolicMEC_stats.h` contain the algorithm implementations, the files `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), the files `src/storm/storage/SymbolicSCCDecomposition.h` and `src/storm/storage/SymbolicSCCDecomposition_stats.h` contain symbolic SCC decomposition algorithm implementations, and the file `src/storm/storage/THESIS_DEBUG.h` contains miscellaneous definitions of the algorithms we benchmarked. + +To run any of the symbolic MEC decomposition algorithms, call the `storm` binary as usual, adding the argument `--benchmarkForceMECDecompositionAlgorithm ` with `n = 1,2,3` for `NAIVE, LOCKSTEP, INTERLEAVE`. Using `n = 4,5,6` also counts and outputs the number of symbolic operations performed by the `NAIVE, LOCKSTEP, INTERLEAVE` algorithms. Usual Stork GitHub README is below. Usage ----------------------------- From 3b3834a901ad054f929bdba7273184469e33a04e Mon Sep 17 00:00:00 2001 From: Ramneet Singh <63390014+Ramneet-Singh@users.noreply.github.com> Date: Thu, 18 Jul 2024 19:34:22 +0530 Subject: [PATCH 20/25] Change Stork to Storm --- README.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/README.md b/README.md index 920123199f..96796c194d 100644 --- a/README.md +++ b/README.md @@ -7,7 +7,7 @@ Storm - A Modern Probabilistic Model Checker 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`) 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. The files `src/storm/storage/SymbolicMEC.h` and `src/storm/storage/SymbolicMEC_stats.h` contain the algorithm implementations, the files `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), the files `src/storm/storage/SymbolicSCCDecomposition.h` and `src/storm/storage/SymbolicSCCDecomposition_stats.h` contain symbolic SCC decomposition algorithm implementations, and the file `src/storm/storage/THESIS_DEBUG.h` contains miscellaneous definitions of the algorithms we benchmarked. -To run any of the symbolic MEC decomposition algorithms, call the `storm` binary as usual, adding the argument `--benchmarkForceMECDecompositionAlgorithm ` with `n = 1,2,3` for `NAIVE, LOCKSTEP, INTERLEAVE`. Using `n = 4,5,6` also counts and outputs the number of symbolic operations performed by the `NAIVE, LOCKSTEP, INTERLEAVE` algorithms. Usual Stork GitHub README is below. +To run any of the symbolic MEC decomposition algorithms, call the `storm` binary as usual, adding the argument `--benchmarkForceMECDecompositionAlgorithm ` with `n = 1,2,3` for `NAIVE, LOCKSTEP, INTERLEAVE`. Using `n = 4,5,6` also counts and outputs the number of symbolic operations performed by the `NAIVE, LOCKSTEP, INTERLEAVE` algorithms. Usual Storm GitHub README is below. Usage ----------------------------- From f448b00ce9bef3911536cb70aed7b7f64d131bf4 Mon Sep 17 00:00:00 2001 From: Ramneet Singh <63390014+Ramneet-Singh@users.noreply.github.com> Date: Sun, 15 Sep 2024 17:55:10 +0530 Subject: [PATCH 21/25] Update README.md --- README.md | 7 ++++++- 1 file changed, 6 insertions(+), 1 deletion(-) diff --git a/README.md b/README.md index 96796c194d..26de903acb 100644 --- a/README.md +++ b/README.md @@ -5,7 +5,12 @@ 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`) 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. The files `src/storm/storage/SymbolicMEC.h` and `src/storm/storage/SymbolicMEC_stats.h` contain the algorithm implementations, the files `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), the files `src/storm/storage/SymbolicSCCDecomposition.h` and `src/storm/storage/SymbolicSCCDecomposition_stats.h` contain symbolic SCC decomposition algorithm implementations, and the file `src/storm/storage/THESIS_DEBUG.h` contains miscellaneous definitions of the algorithms we benchmarked. +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) +- `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 of the algorithms we benchmarked. To run any of the symbolic MEC decomposition algorithms, call the `storm` binary as usual, adding the argument `--benchmarkForceMECDecompositionAlgorithm ` with `n = 1,2,3` for `NAIVE, LOCKSTEP, INTERLEAVE`. Using `n = 4,5,6` also counts and outputs the number of symbolic operations performed by the `NAIVE, LOCKSTEP, INTERLEAVE` algorithms. Usual Storm GitHub README is below. From 00e1604281f1e5c7207631f9423c33881333d584 Mon Sep 17 00:00:00 2001 From: Ramneet Singh <63390014+Ramneet-Singh@users.noreply.github.com> Date: Sun, 15 Sep 2024 17:57:23 +0530 Subject: [PATCH 22/25] Update README.md --- README.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/README.md b/README.md index 26de903acb..55bf168b6a 100644 --- a/README.md +++ b/README.md @@ -7,7 +7,7 @@ Storm - A Modern Probabilistic Model Checker 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) +- `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 of the algorithms we benchmarked. From c36b96a2f30b736c99c295c4e74e5a9c6f1335ec Mon Sep 17 00:00:00 2001 From: Ramneet Singh <63390014+Ramneet-Singh@users.noreply.github.com> Date: Sun, 15 Sep 2024 17:57:53 +0530 Subject: [PATCH 23/25] Update README.md --- README.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/README.md b/README.md index 55bf168b6a..339a890ecf 100644 --- a/README.md +++ b/README.md @@ -10,7 +10,7 @@ This is a custom fork of Storm for my Bachelor and Master Thesis at IIT Delhi, t - `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 of the algorithms we benchmarked. +- `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 ` with `n = 1,2,3` for `NAIVE, LOCKSTEP, INTERLEAVE`. Using `n = 4,5,6` also counts and outputs the number of symbolic operations performed by the `NAIVE, LOCKSTEP, INTERLEAVE` algorithms. Usual Storm GitHub README is below. From 631990a23fe58812f22920f95f91dbb7ab931bb3 Mon Sep 17 00:00:00 2001 From: Ramneet Singh Date: Wed, 9 Apr 2025 14:09:42 +0000 Subject: [PATCH 24/25] Fix typo in README --- README.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/README.md b/README.md index 339a890ecf..5fd50dfd3c 100644 --- a/README.md +++ b/README.md @@ -12,7 +12,7 @@ This is a custom fork of Storm for my Bachelor and Master Thesis at IIT Delhi, t - `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 ` with `n = 1,2,3` for `NAIVE, LOCKSTEP, INTERLEAVE`. Using `n = 4,5,6` also counts and outputs the number of symbolic operations performed by the `NAIVE, LOCKSTEP, INTERLEAVE` algorithms. Usual Storm GitHub README is below. +To run any of the symbolic MEC decomposition algorithms, call the `storm` binary as usual, adding the argument `--benchmarkForceMECDecompositionAlgorithm ` 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 ----------------------------- From ad935400f1aba8e2e2db639976188dd6db92778a Mon Sep 17 00:00:00 2001 From: Ramneet Singh Date: Wed, 9 Apr 2025 17:08:51 +0000 Subject: [PATCH 25/25] Change early exit so peak memory stats are also printed --- src/storm-cli-utilities/model-handling.h | 37 +++++++++++++++++------- 1 file changed, 27 insertions(+), 10 deletions(-) diff --git a/src/storm-cli-utilities/model-handling.h b/src/storm-cli-utilities/model-handling.h index b95bb1b5a3..dffd2e7942 100644 --- a/src/storm-cli-utilities/model-handling.h +++ b/src/storm-cli-utilities/model-handling.h @@ -516,15 +516,6 @@ std::shared_ptr buildModel(SymbolicInput const& input, result = buildModelSparse(input, buildSettings); } - // THESIS DATA GATHERING [rmnt] - Benchmarking the Symbolic MEC decomposition algorithms. Entry point. - uint64_t DEBUG_THESIS_BENCHMARK = storm::settings::getModule().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((storm::models::ModelBase const&)*result, DEBUG_THESIS_BENCHMARK); - exit(0); - } - } 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."); @@ -1292,6 +1283,17 @@ std::shared_ptr buildPreprocessModelWithValueTypeAndDd std::shared_ptr model; if (!buildSettings.isNoBuildModelSet()) { model = buildModel(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().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((storm::models::ModelBase const&)*model, DEBUG_THESIS_BENCHMARK); + return model; + } + } if (model) { @@ -1300,6 +1302,7 @@ std::shared_ptr buildPreprocessModelWithValueTypeAndDd STORM_LOG_THROW(model || input.properties.empty(), storm::exceptions::InvalidSettingsException, "No input model."); + if (model) { auto preprocessingResult = preprocessModel(model, input, mpi); if (preprocessingResult.second) { @@ -1313,6 +1316,13 @@ std::shared_ptr buildPreprocessModelWithValueTypeAndDd template std::shared_ptr buildPreprocessExportModelWithValueTypeAndDdlib(SymbolicInput const& input, ModelProcessingInformation const& mpi) { auto model = buildPreprocessModelWithValueTypeAndDdlib(input, mpi); + + // THESIS DATA GATHERING [rmnt] - Benchmarking the Symbolic MEC decomposition algorithms. Early exit. + uint64_t DEBUG_THESIS_BENCHMARK = storm::settings::getModule().forceMECDecompositionAlgorithm(); + if (DEBUG_THESIS_BENCHMARK != 0) { + return model; + } + if (model) { exportModel(model, input); } @@ -1333,6 +1343,13 @@ void processInputWithValueTypeAndDdlib(SymbolicInput const& input, ModelProcessi } else { std::shared_ptr model = buildPreprocessExportModelWithValueTypeAndDdlib(input, mpi); + + // THESIS DATA GATHERING [rmnt] - Benchmarking the Symbolic MEC decomposition algorithms. Early exit. + uint64_t DEBUG_THESIS_BENCHMARK = storm::settings::getModule().forceMECDecompositionAlgorithm(); + if (DEBUG_THESIS_BENCHMARK != 0) { + return; + } + if (model) { if (counterexampleSettings.isCounterexampleSet()) { generateCounterexamples(model, input); @@ -1370,4 +1387,4 @@ void processInputWithValueType(SymbolicInput const& input, ModelProcessingInform } // namespace cli } // namespace storm -#endif \ No newline at end of file +#endif