Add member transition matrix to bisimulation

src/storm-gamebased-ar/modelchecker/abstraction/BisimulationAbstractionRefinementModelChecker.cpp

@@ -7,7 +7,7 @@
 
 #include "storm-gamebased-ar/abstraction/SymbolicStateSet.h"
 
-#include "storm/storage/dd/BisimulationDecomposition.h"
+#include "storm/storage/dd/bisimulation/BisimulationDecomposition.h"
 
 #include "storm/modelchecker/propositional/SymbolicPropositionalModelChecker.h"
 #include "storm/modelchecker/results/SymbolicQualitativeCheckResult.h"

src/storm/api/bisimulation.h

@@ -1,16 +1,13 @@
 #pragma once
 
+#include "storm/exceptions/NotSupportedException.h"
 #include "storm/models/sparse/Ctmc.h"
 #include "storm/models/sparse/Dtmc.h"
 #include "storm/models/sparse/Mdp.h"
-
 #include "storm/storage/bisimulation/DeterministicModelBisimulationDecomposition.h"
 #include "storm/storage/bisimulation/NondeterministicModelBisimulationDecomposition.h"
-
-#include "storm/storage/dd/BisimulationDecomposition.h"
 #include "storm/storage/dd/DdType.h"
-
-#include "storm/exceptions/NotSupportedException.h"
+#include "storm/storage/dd/bisimulation/BisimulationDecomposition.h"
 #include "storm/utility/macros.h"
 
 namespace storm {

src/storm/storage/bisimulation/BisimulationDecomposition.cpp

@@ -6,23 +6,16 @@
 #include "storm/exceptions/AbortException.h"
 #include "storm/exceptions/IllegalFunctionCallException.h"
 #include "storm/exceptions/InvalidOptionException.h"
-
 #include "storm/logic/FormulaInformation.h"
 #include "storm/logic/FragmentSpecification.h"
-
+#include "storm/modelchecker/propositional/SparsePropositionalModelChecker.h"
+#include "storm/modelchecker/results/ExplicitQualitativeCheckResult.h"
 #include "storm/models/sparse/Ctmc.h"
 #include "storm/models/sparse/Dtmc.h"
 #include "storm/models/sparse/Mdp.h"
-#include "storm/models/sparse/StandardRewardModel.h"
-
-#include "storm/modelchecker/propositional/SparsePropositionalModelChecker.h"
-#include "storm/modelchecker/results/ExplicitQualitativeCheckResult.h"
-
 #include "storm/settings/SettingsManager.h"
 #include "storm/settings/modules/CoreSettings.h"
-
 #include "storm/storage/bisimulation/DeterministicBlockData.h"
-
 #include "storm/utility/SignalHandler.h"
 #include "storm/utility/macros.h"
 
@@ -71,8 +64,8 @@ template<typename ModelType, typename BlockDataType>
 void BisimulationDecomposition<ModelType, BlockDataType>::Options::preserveFormula(storm::logic::Formula const& formula) {
     // Disable the measure driven initial partition.
     measureDrivenInitialPartition = false;
-    phiStates = boost::none;
-    psiStates = boost::none;
+    phiStates.reset();
+    psiStates.reset();
 
     // Retrieve information about formula.
     storm::logic::FormulaInformation info = formula.info();
@@ -163,7 +156,7 @@ void BisimulationDecomposition<ModelType, BlockDataType>::Options::checkAndSetMe
         phiStates = phiStatesCheckResult->asExplicitQualitativeCheckResult().getTruthValuesVector();
         psiStates = psiStatesCheckResult->asExplicitQualitativeCheckResult().getTruthValuesVector();
     } else {
-        optimalityType = boost::none;
+        optimalityType.reset();
     }
 }
 
@@ -181,7 +174,7 @@ void BisimulationDecomposition<ModelType, BlockDataType>::Options::addToRespecte
     if (!respectedAtomicPropositions) {
         respectedAtomicPropositions = labelsToRespect;
     } else {
-        respectedAtomicPropositions.get().insert(labelsToRespect.begin(), labelsToRespect.end());
+        respectedAtomicPropositions.value().insert(labelsToRespect.begin(), labelsToRespect.end());
     }
 }
 
@@ -347,7 +340,7 @@ template<typename ModelType, typename BlockDataType>
 void BisimulationDecomposition<ModelType, BlockDataType>::initializeLabelBasedPartition() {
     partition = storm::storage::bisimulation::Partition<BlockDataType>(model.getNumberOfStates());
 
-    for (auto const& label : options.respectedAtomicPropositions.get()) {
+    for (auto const& label : options.respectedAtomicPropositions.value()) {
         if (label == "init") {
             continue;
         }
@@ -365,14 +358,14 @@ template<typename ModelType, typename BlockDataType>
 void BisimulationDecomposition<ModelType, BlockDataType>::initializeMeasureDrivenPartition() {
     std::pair<storm::storage::BitVector, storm::storage::BitVector> statesWithProbability01 = this->getStatesWithProbability01();
 
-    boost::optional<storm::storage::sparse::state_type> representativePsiState;
-    if (!options.psiStates.get().empty()) {
-        representativePsiState = *options.psiStates.get().begin();
+    std::optional<storm::storage::sparse::state_type> representativePsiState;
+    if (!options.psiStates.value().empty()) {
+        representativePsiState = *options.psiStates.value().begin();
     }
 
     partition = storm::storage::bisimulation::Partition<BlockDataType>(
         model.getNumberOfStates(), statesWithProbability01.first,
-        options.getBounded() || options.getKeepRewards() ? options.psiStates.get() : statesWithProbability01.second, representativePsiState);
+        options.getBounded() || options.getKeepRewards() ? options.psiStates.value() : statesWithProbability01.second, representativePsiState);
 
     // If the model has state rewards, we need to consider them, because otherwise reward properties are not
     // preserved.
@@ -404,14 +397,12 @@ template class BisimulationDecomposition<storm::models::sparse::Dtmc<double>, bi
 template class BisimulationDecomposition<storm::models::sparse::Ctmc<double>, bisimulation::DeterministicBlockData>;
 template class BisimulationDecomposition<storm::models::sparse::Mdp<double>, bisimulation::DeterministicBlockData>;
 
-#ifdef STORM_HAVE_CARL
 template class BisimulationDecomposition<storm::models::sparse::Dtmc<storm::RationalNumber>, bisimulation::DeterministicBlockData>;
 template class BisimulationDecomposition<storm::models::sparse::Ctmc<storm::RationalNumber>, bisimulation::DeterministicBlockData>;
 template class BisimulationDecomposition<storm::models::sparse::Mdp<storm::RationalNumber>, bisimulation::DeterministicBlockData>;
 
 template class BisimulationDecomposition<storm::models::sparse::Dtmc<storm::RationalFunction>, bisimulation::DeterministicBlockData>;
 template class BisimulationDecomposition<storm::models::sparse::Ctmc<storm::RationalFunction>, bisimulation::DeterministicBlockData>;
 template class BisimulationDecomposition<storm::models::sparse::Mdp<storm::RationalFunction>, bisimulation::DeterministicBlockData>;
-#endif
 }  // namespace storage
 }  // namespace storm

src/storm/storage/bisimulation/BisimulationDecomposition.h

@@ -1,19 +1,14 @@
-#ifndef STORM_STORAGE_BISIMULATIONDECOMPOSITION_H_
-#define STORM_STORAGE_BISIMULATIONDECOMPOSITION_H_
+#pragma once
 
+#include "storm/logic/Formulas.h"
 #include "storm/settings/SettingsManager.h"
 #include "storm/settings/modules/BisimulationSettings.h"
 #include "storm/solver/OptimizationDirection.h"
 #include "storm/storage/Decomposition.h"
 #include "storm/storage/StateBlock.h"
 #include "storm/storage/bisimulation/BisimulationType.h"
 #include "storm/storage/bisimulation/Partition.h"
-#include "storm/storage/sparse/StateType.h"
-
-#include "storm/logic/Formulas.h"
-
 #include "storm/utility/ConstantsComparator.h"
-#include "storm/utility/constants.h"
 
 namespace storm {
 namespace logic {
@@ -56,7 +51,7 @@ class BisimulationDecomposition : public Decomposition<StateBlock> {
          * Creates an object representing the options necessary to obtain the quotient while still preserving
          * the given formula.
          *
-         * @param The model for which the quotient model shall be computed. This needs to be given in order to
+         * @param model The model for which the quotient model shall be computed. This needs to be given in order to
          * derive a suitable initial partition.
          * @param formula The formula that is to be preserved.
          */
@@ -66,7 +61,7 @@ class BisimulationDecomposition : public Decomposition<StateBlock> {
          * Creates an object representing the options necessary to obtain the smallest quotient while still
          * preserving the given formulas.
          *
-         * @param The model for which the quotient model shall be computed. This needs to be given in order to
+         * @param model The model for which the quotient model shall be computed. This needs to be given in order to
          * derive a suitable initial partition.
          * @param formulas The formulas that need to be preserved.
          */
@@ -120,27 +115,27 @@ class BisimulationDecomposition : public Decomposition<StateBlock> {
 
         OptimizationDirection getOptimizationDirection() const {
             STORM_LOG_ASSERT(optimalityType, "Optimality type not set.");
-            return optimalityType.get();
+            return optimalityType.value();
         }
 
         // A flag that indicates whether a measure driven initial partition is to be used. If this flag is set
         // to true, the two optional pairs phiStatesAndLabel and psiStatesAndLabel must be set. Then, the
         // measure driven initial partition wrt. to the states phi and psi is taken.
         bool measureDrivenInitialPartition;
-        boost::optional<storm::storage::BitVector> phiStates;
-        boost::optional<storm::storage::BitVector> psiStates;
+        std::optional<storm::storage::BitVector> phiStates;
+        std::optional<storm::storage::BitVector> psiStates;
 
         /// An optional set of strings that indicate which of the atomic propositions of the model are to be
         /// respected and which may be ignored. If not given, all atomic propositions of the model are respected.
-        boost::optional<std::set<std::string>> respectedAtomicPropositions;
+        std::optional<std::set<std::string>> respectedAtomicPropositions;
 
         /// A flag that governs whether the quotient model is actually built or only the decomposition is computed.
         bool buildQuotient;
 
        private:
-        boost::optional<OptimizationDirection> optimalityType;
+        std::optional<OptimizationDirection> optimalityType;
 
-        /// A flag that indicates whether or not the state-rewards of the model are to be respected (and should
+        /// A flag that indicates whether the state-rewards of the model are to be respected (and should
         /// be kept in the quotient model, if one is built).
         bool keepRewards;
 
@@ -184,7 +179,7 @@ class BisimulationDecomposition : public Decomposition<StateBlock> {
     };
 
     /*!
-     * Decomposes the given model into equivalance classes of a bisimulation.
+     * Decomposes the given model into equivalence classes of a bisimulation.
      *
      * @param model The model to decompose.
      * @param options The options to use during for the decomposition.
@@ -208,10 +203,10 @@ class BisimulationDecomposition : public Decomposition<StateBlock> {
 
    protected:
     /*!
-     * Decomposes the given model into equivalance classes of a bisimulation.
+     * Decomposes the given model into equivalence classes of a bisimulation.
      *
      * @param model The model to decompose.
-     * @param backwardTransition The backward transitions of the model.
+     * @param backwardTransitions The backward transitions of the model.
      * @param options The options to use during for the decomposition.
      */
     BisimulationDecomposition(ModelType const& model, storm::storage::SparseMatrix<ValueType> const& backwardTransitions, Options const& options);
@@ -231,11 +226,10 @@ class BisimulationDecomposition : public Decomposition<StateBlock> {
      * @param splitterVector The vector into which to insert the newly discovered potential splitters.
      */
     virtual void refinePartitionBasedOnSplitter(bisimulation::Block<BlockDataType>& splitter,
-                                                std::vector<bisimulation::Block<BlockDataType>*>& splitterQueue) = 0;
+                                                std::vector<bisimulation::Block<BlockDataType>*>& splitterVector) = 0;
 
     /*!
-     * Builds the quotient model based on the previously computed equivalence classes (stored in the blocks
-     * of the decomposition.
+     * Builds the quotient model based on the previously computed equivalence classes (stored in the blocks of the decomposition).
      */
     virtual void buildQuotient() = 0;
 
@@ -297,10 +291,8 @@ class BisimulationDecomposition : public Decomposition<StateBlock> {
     // A comparator used for comparing the distances of constants.
     storm::utility::ConstantsComparator<ValueType> comparator;
 
-    // The quotient, if it was build. Otherwhise a null pointer.
+    // The quotient, if it was build. Otherwise a null pointer.
     std::shared_ptr<ModelType> quotient;
 };
 }  // namespace storage
 }  // namespace storm
-
-#endif /* STORM_STORAGE_BISIMULATIONDECOMPOSITION_H_ */

src/storm/storage/bisimulation/Block.cpp

@@ -1,11 +1,9 @@
 #include "storm/storage/bisimulation/Block.h"
 
-#include <iomanip>
 #include <iostream>
 
 #include "storm/storage/bisimulation/DeterministicBlockData.h"
 #include "storm/storage/bisimulation/Partition.h"
-
 #include "storm/utility/macros.h"
 
 namespace storm {

src/storm/storage/bisimulation/Block.h

@@ -1,8 +1,4 @@
-#ifndef STORM_STORAGE_BISIMULATION_BLOCK_H_
-#define STORM_STORAGE_BISIMULATION_BLOCK_H_
-
-#include <boost/optional.hpp>
-#include <list>
+#pragma once
 
 #include "storm/storage/sparse/StateType.h"
 
@@ -105,5 +101,3 @@ class Block {
 }  // namespace bisimulation
 }  // namespace storage
 }  // namespace storm
-
-#endif /* STORM_STORAGE_BISIMULATION_BLOCK_H_ */

src/storm/storage/bisimulation/DeterministicBlockData.cpp

@@ -89,8 +89,8 @@ bool DeterministicBlockData::hasRepresentativeState() const {
 }
 
 storm::storage::sparse::state_type DeterministicBlockData::representativeState() const {
-    STORM_LOG_THROW(valRepresentativeState, storm::exceptions::InvalidOperationException, "Unable to retrieve representative state for block.");
-    return valRepresentativeState.get();
+    STORM_LOG_THROW(hasRepresentativeState(), storm::exceptions::InvalidOperationException, "Unable to retrieve representative state for block.");
+    return valRepresentativeState.value();
 }
 
 bool DeterministicBlockData::needsRefinement() const {

src/storm/storage/bisimulation/DeterministicBlockData.h

@@ -1,7 +1,4 @@
-#ifndef STORM_STORAGE_BISIMULATION_DETERMINISTICBLOCKDATA_H_
-#define STORM_STORAGE_BISIMULATION_DETERMINISTICBLOCKDATA_H_
-
-#include <cstdint>
+#pragma once
 
 #include "storm/storage/bisimulation/Block.h"
 
@@ -43,7 +40,7 @@ class DeterministicBlockData {
     // Marks the block as needing refinement (or not).
     void setNeedsRefinement(bool value = true);
 
-    // Sets whether or not the block is to be interpreted as absorbing.
+    // Sets whether the block is to be interpreted as absorbing.
     void setAbsorbing(bool absorbing);
 
     // Retrieves whether the block is to be interpreted as absorbing.
@@ -77,20 +74,18 @@ class DeterministicBlockData {
     uint_fast64_t valMarker2;
 
     // Some bits to store flags: splitter flag, refinement flag, absorbing flag.
-    static const uint64_t SPLITTER_FLAG = 1ull;
-    static const uint64_t REFINEMENT_FLAG = 1ull << 1;
-    static const uint64_t ABSORBING_FLAG = 1ull << 2;
-    static const uint64_t REWARD_FLAG = 1ull << 3;
+    static constexpr uint64_t SPLITTER_FLAG = 1ull;
+    static constexpr uint64_t REFINEMENT_FLAG = 1ull << 1;
+    static constexpr uint64_t ABSORBING_FLAG = 1ull << 2;
+    static constexpr uint64_t REWARD_FLAG = 1ull << 3;
     uint8_t flags;
 
     // An optional representative state for the block. If this is set, this state is used to derive the
     // atomic propositions of the meta state in the quotient model.
-    boost::optional<storm::storage::sparse::state_type> valRepresentativeState;
+    std::optional<storm::storage::sparse::state_type> valRepresentativeState;
 };
 
 std::ostream& operator<<(std::ostream& out, DeterministicBlockData const& data);
 }  // namespace bisimulation
 }  // namespace storage
 }  // namespace storm
-
-#endif /* STORM_STORAGE_BISIMULATION_DETERMINISTICBLOCKDATA_H_ */