SLAM.LoopClosure.RGBDKeyframes.ValidHeader

Parameters, inputs, outputs, defaults and equations from the source file.

function ValidHeader
    input Catalog state;
    output Boolean valid;
  protected
    Integer expectedOccupied;
    Integer actualOccupied;
    Integer olderSlot;
    Integer newestSlot;
    Boolean identityValid;
  algorithm
    expectedOccupied := 0; actualOccupied := 0;
    olderSlot := 1; newestSlot := 1; identityValid := false;
    valid := state.generation >= 1 and state.generation <= identifierLimit
      and state.vocabularyVersion >= 1 and state.vocabularyVersion <= identifierLimit
      and state.nextId >= 1 and state.nextId <= identifierLimit
      and state.nextSlot >= 1 and state.nextSlot <= keyframeCapacity
      and state.lastEpoch >= -1 and state.lastEpoch <= identifierLimit
      and state.lastTime >= 0 and state.lastTime <= 1e9;
    // Certify Integer domains before subtraction or computing array indices.
    if valid then
      valid := state.nextSlot == mod(state.nextId-1,keyframeCapacity)+1;
      expectedOccupied := min(state.nextId-1,keyframeCapacity);
      for slot in 1:keyframeCapacity loop
        if state.occupied[slot] then
          actualOccupied := actualOccupied+1;
          identityValid := state.ids[slot] >= max(1,state.nextId-keyframeCapacity)
            and state.ids[slot] < state.nextId;
          valid := valid and identityValid
            and state.generations[slot] == state.generation
            and state.vocabularyVersions[slot] == state.vocabularyVersion
            and state.epochs[slot] >= 0 and state.epochs[slot] <= state.lastEpoch
            and state.imageTimes[slot] >= 0 and state.imageTimes[slot] <= state.lastTime;
          if identityValid then
            valid := valid and mod(state.ids[slot]-1,keyframeCapacity)+1 == slot;
            if state.ids[slot] > max(1,state.nextId-keyframeCapacity) then
              olderSlot := mod(state.ids[slot]-2,keyframeCapacity)+1;
              valid := valid and state.occupied[olderSlot]
                and state.ids[olderSlot] == state.ids[slot]-1
                and state.epochs[olderSlot] < state.epochs[slot]
                and state.imageTimes[olderSlot] < state.imageTimes[slot];
            end if;
          end if;
        end if;
      end for;
      valid := valid and actualOccupied == expectedOccupied
        and ((state.nextId == 1 and state.lastEpoch == -1 and state.lastTime == 0)
          or (state.nextId > 1 and state.lastEpoch >= 0));
      if state.nextId > 1 then
        newestSlot := mod(state.nextId-2,keyframeCapacity)+1;
        valid := valid and state.occupied[newestSlot]
          and state.ids[newestSlot] == state.nextId-1
          and state.epochs[newestSlot] == state.lastEpoch
          and state.imageTimes[newestSlot] == state.lastTime;
      end if;
    end if;
  end ValidHeader;