text: #include "storm/storage/memorystructure/NondeterministicMemoryStructure.h"
  #include "storm/storage/memorystructure/NondeterministicMemoryStructureBuilder.h"
  
  #include "storm/utility/macros.h"
  #include "storm/exceptions/InvalidArgumentException.h"
  
  namespace storm {
      namespace storage {
          
          std::string toString(NondeterministicMemoryStructurePattern const& pattern) {
              switch (pattern) {
                  case NondeterministicMemoryStructurePattern::Trivial:
                      return "trivial";
                  case NondeterministicMemoryStructurePattern::FixedCounter:
                      return "fixedcounter";
                  case NondeterministicMemoryStructurePattern::SelectiveCounter:
                      return "selectivecounter";
                  case NondeterministicMemoryStructurePattern::FixedRing:
                      return "fixedring";
                  case NondeterministicMemoryStructurePattern::SelectiveRing:
                      return "ring";
                  case NondeterministicMemoryStructurePattern::SettableBits:
                      return "settablebits";
                  case NondeterministicMemoryStructurePattern::Full:
                      return "full";
              }
              return "unknown";
          }
  
          NondeterministicMemoryStructure NondeterministicMemoryStructureBuilder::build(NondeterministicMemoryStructurePattern pattern, uint64_t numStates) const {
              switch (pattern) {
                  case NondeterministicMemoryStructurePattern::Trivial:
                      STORM_LOG_ERROR_COND(numStates == 1, "Invoked building trivial nondeterministic memory structure with " << numStates << " states. However, trivial  nondeterministic memory structure always has one state.");
                      return buildTrivialMemory();
                  case NondeterministicMemoryStructurePattern::FixedCounter:
                      return buildFixedCountingMemory(numStates);
                  case NondeterministicMemoryStructurePattern::SelectiveCounter:
                      return buildSelectiveCountingMemory(numStates);
                  case NondeterministicMemoryStructurePattern::FixedRing:
                      return buildFixedRingMemory(numStates);
                  case NondeterministicMemoryStructurePattern::SelectiveRing:
                      return buildSelectiveRingMemory(numStates);
                  case NondeterministicMemoryStructurePattern::SettableBits:
                      return buildSettableBitsMemory(numStates);
                  case NondeterministicMemoryStructurePattern::Full:
                      return buildFullyConnectedMemory(numStates);
              }
          }
          
          NondeterministicMemoryStructure NondeterministicMemoryStructureBuilder::buildTrivialMemory() const {
              return buildFullyConnectedMemory(1);
          }
          
          NondeterministicMemoryStructure NondeterministicMemoryStructureBuilder::buildFixedCountingMemory(uint64_t numStates) const {
              std::vector<storm::storage::BitVector> transitions(numStates, storm::storage::BitVector(numStates, false));
              for (uint64_t state = 0; state < numStates; ++state) {
                  transitions[state].set(std::min(state + 1, numStates - 1));
              }
              return NondeterministicMemoryStructure(transitions, 0);
          }
          
          NondeterministicMemoryStructure NondeterministicMemoryStructureBuilder::buildSelectiveCountingMemory(uint64_t numStates) const {
              std::vector<storm::storage::BitVector> transitions(numStates, storm::storage::BitVector(numStates, false));
              for (uint64_t state = 0; state < numStates; ++state) {
                  transitions[state].set(state);
                  transitions[state].set(std::min(state + 1, numStates - 1));
              }
              return NondeterministicMemoryStructure(transitions, 0);
          }
          
          NondeterministicMemoryStructure NondeterministicMemoryStructureBuilder::buildFixedRingMemory(uint64_t numStates) const {
              std::vector<storm::storage::BitVector> transitions(numStates, storm::storage::BitVector(numStates, false));
              for (uint64_t state = 0; state < numStates; ++state) {
                  transitions[state].set((state + 1) % numStates);
              }
              return NondeterministicMemoryStructure(transitions, 0);
          }
          
          NondeterministicMemoryStructure NondeterministicMemoryStructureBuilder::buildSelectiveRingMemory(uint64_t numStates) const {
              std::vector<storm::storage::BitVector> transitions(numStates, storm::storage::BitVector(numStates, false));
              for (uint64_t state = 0; state < numStates; ++state) {
                  transitions[state].set(state);
                  transitions[state].set((state + 1) % numStates);
              }
              return NondeterministicMemoryStructure(transitions, 0);
          }
          
          NondeterministicMemoryStructure NondeterministicMemoryStructureBuilder::buildSettableBitsMemory(uint64_t numStates) const {
              // compute the number of bits, i.e., floor(log(numStates))
              uint64_t numBits = 0;
              uint64_t actualNumStates = 1;
              while (actualNumStates * 2 <= numStates) {
                  actualNumStates *= 2;
                  ++numBits;
              }
              
              STORM_LOG_WARN_COND(actualNumStates == numStates, "The number of memory states for the settable bits pattern has to be a power of 2. Shrinking the number of memory states to " << actualNumStates << ".");
              
              std::vector<storm::storage::BitVector> transitions(actualNumStates, storm::storage::BitVector(actualNumStates, false));
              for (uint64_t state = 0; state < actualNumStates; ++state) {
                  transitions[state].set(state);
                  for (uint64_t bit = 0; bit < numBits; ++bit) {
                      uint64_t bitMask = 1u << bit;
                      transitions[state].set(state | bitMask);
                  }
              }
              return NondeterministicMemoryStructure(transitions, 0);
          }
          
          NondeterministicMemoryStructure NondeterministicMemoryStructureBuilder::buildFullyConnectedMemory(uint64_t numStates) const {
              std::vector<storm::storage::BitVector> transitions(numStates, storm::storage::BitVector(numStates, true));
              return NondeterministicMemoryStructure(transitions, 0);
          }
      }
  }