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/README.md b/README.md index 197c49084b..5fd50dfd3c 100644 --- a/README.md +++ b/README.md @@ -5,6 +5,14 @@ Storm - A Modern Probabilistic Model Checker [![GitHub release](https://img.shields.io/github/release/moves-rwth/storm.svg)](https://github.com/moves-rwth/storm/releases/) [![DOI](https://zenodo.org/badge/DOI/10.5281/zenodo.1181896.svg)](https://doi.org/10.5281/zenodo.1181896) +This is a custom fork of Storm for my Bachelor and Master Thesis at IIT Delhi, titled, "`INTERLEAVE` : An Empirically Faster Symbolic Algorithm for Maximal End Component Decomposition of MDPs" and advised by Suguman Bansal (Georgia Tech) and Subodh Sharma (IIT Delhi). Most of the code (except the new algorithm added -- `INTERLEAVE` and minor bug fixes) has been adapted from [the code for Felix Faber's Bachelor Thesis at RWTH Aachen](https://doi.org/10.5281/zenodo.8311805). I am grateful to Felix for writing an excellent thesis, and for writing code that was easy to understand and extend. Below is a brief description of the relevant files. + +- `src/storm/storage/SymbolicMEC.h` and `src/storm/storage/SymbolicMEC_stats.h` contain the algorithm implementations (the `_stats` files additionally count the number of transition BDD operations). The functions `symbolicMECDecompositionInterleave` and `symbolicMECDecompositionInterleave_stats` implement our `INTERLEAVE` algorithm. +- `src/storm/storage/SymbolicOperations.h` and `src/storm/storage/SymbolicOperations_stats.h` contain the implementations of symbolic operations (including a new implementation of `pick` which I tried out and added support for to the `src/storm/storage/dd`, `src/storm/storage/dd/cudd` and `src/storm/storage/dd/sylvan` folders) +- `src/storm/storage/SymbolicSCCDecomposition.h` and `src/storm/storage/SymbolicSCCDecomposition_stats.h` contain symbolic SCC decomposition algorithm implementations +- `src/storm/storage/THESIS_DEBUG.h` contains miscellaneous definitions for the algorithms we benchmarked. + +To run any of the symbolic MEC decomposition algorithms, call the `storm` binary as usual, adding the argument `--benchmarkForceMECDecompositionAlgorithm ` 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 ----------------------------- diff --git a/src/storm-cli-utilities/model-handling.h b/src/storm-cli-utilities/model-handling.h index af1a5e6b55..dffd2e7942 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" @@ -50,6 +51,8 @@ #include "storm/utility/Stopwatch.h" +#include "storm/storage/THESIS_DEBUG.h" + namespace storm { namespace cli { @@ -512,6 +515,7 @@ std::shared_ptr buildModel(SymbolicInput const& input, } else if (builderType == storm::builder::BuilderType::Explicit) { result = buildModelSparse(input, buildSettings); } + } else if (ioSettings.isExplicitSet() || ioSettings.isExplicitDRNSet() || ioSettings.isExplicitIMCASet()) { STORM_LOG_THROW(mpi.engine == storm::utility::Engine::Sparse, storm::exceptions::InvalidSettingsException, "Can only use sparse engine with explicit input."); @@ -1279,6 +1283,17 @@ std::shared_ptr 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) { @@ -1287,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) { @@ -1300,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); } @@ -1320,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); @@ -1356,3 +1386,5 @@ void processInputWithValueType(SymbolicInput const& input, ModelProcessingInform } } // namespace cli } // namespace storm + +#endif 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 diff --git a/src/storm/storage/SymbolicMEC.h b/src/storm/storage/SymbolicMEC.h new file mode 100644 index 0000000000..47345c5eeb --- /dev/null +++ b/src/storm/storage/SymbolicMEC.h @@ -0,0 +1,402 @@ +#ifndef STORM_STORAGE_SYMBOLICMEC_H +#define STORM_STORAGE_SYMBOLICMEC_H + +#include +#include +#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. + + StateActionPair& operator|=(StateActionPair const& other) { + states |= other.states; + actions |= other.actions; + return *this; + } +}; + +// [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) + 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, + * (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; + // [rmnt] TODO do the && earlier? + + // 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); + 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; +} + +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, 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); + + std::stack> 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 + { + 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)) + + // 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 && V2}; + workStack.emplace(newTask); + } + } else { + if (sizes[2 - i] != 0) { + InterleaveDecompTask newTask = {V3, allStates.getDdManager().getBddZero()}; + workStack.emplace(newTask); + } + } + } + } + + return result; +} + +} // namespace symbolicMEC + +#endif diff --git a/src/storm/storage/SymbolicMEC_stats.h b/src/storm/storage/SymbolicMEC_stats.h new file mode 100644 index 0000000000..119a94d4f8 --- /dev/null +++ b/src/storm/storage/SymbolicMEC_stats.h @@ -0,0 +1,425 @@ +#ifndef STORM_STORAGE_SYMBOLICMEC_STATS_H +#define STORM_STORAGE_SYMBOLICMEC_STATS_H + +#include +#include +#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. + + StateActionPair &operator|=(StateActionPair const &other) { + states |= other.states; + actions |= other.actions; + return *this; + } +}; + +// [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 + countSymbolicOps++; + 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, + * (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); + } + } + } + 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; +} + +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( + 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); + + std::stack> 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 + { + 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 + + // 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 && V2}; + workStack.emplace(newTask); + } + } else { + if (sizes[2 - i] != 0) { + InterleaveDecompTask newTask = {V3, allStates.getDdManager().getBddZero()}; + workStack.emplace(newTask); + } + } + } + } + + return result; +} + +} // namespace symbolicMEC_stats + +#endif diff --git a/src/storm/storage/SymbolicOperations.h b/src/storm/storage/SymbolicOperations.h new file mode 100644 index 0000000000..3355faa0fa --- /dev/null +++ b/src/storm/storage/SymbolicOperations.h @@ -0,0 +1,63 @@ +#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..4be457a595 --- /dev/null +++ b/src/storm/storage/SymbolicOperations_stats.h @@ -0,0 +1,67 @@ +#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..54c246ffb6 --- /dev/null +++ b/src/storm/storage/SymbolicSCCDecomposition.h @@ -0,0 +1,119 @@ +#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..e8e7283a51 --- /dev/null +++ b/src/storm/storage/SymbolicSCCDecomposition_stats.h @@ -0,0 +1,122 @@ +#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 new file mode 100644 index 0000000000..7ec230030a --- /dev/null +++ b/src/storm/storage/THESIS_DEBUG.h @@ -0,0 +1,179 @@ +#ifndef STORM_STORAGE_THESIS_DEBUG_H +#define STORM_STORAGE_THESIS_DEBUG_H + +#include "storm/models/Model.h" +#include "storm/models/symbolic/NondeterministicModel.h" +#include "storm/storage/SymbolicMEC.h" +#include "storm/storage/SymbolicMEC_stats.h" +#include "storm/storage/dd/DdType.h" +#include "storm/utility/Stopwatch.h" +#include "storm/utility/macros.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): " << 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; + 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 << "BENCHMARK SYMBOLIC OPS (count): " << 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 << "BENCHMARK SYMBOLIC OPS (count): " << 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); + decompositionTimestampEnd = std::chrono::high_resolution_clock::now(); + std::cout << "BENCHMARK SYMBOLIC OPS (count): " << countSymbolicOps << std::endl; + 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 diff --git a/src/storm/storage/dd/Bdd.cpp b/src/storm/storage/dd/Bdd.cpp index ea56ce91d4..1d358b8984 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..a620842dba 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..a5f118d487 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..99cd234ed9 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..8298012bab 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. * 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)