Bubblesort Algorithm

BubbleSort.tla

---- MODULE BubbleSort ----
EXTENDS Integers, TLC, Sequences, FiniteSets

Counter(seq) == 
  LET
   Range == {seq[x] : x \in DOMAIN seq}
   CountOf(x) == Cardinality({i \in 1..Len(seq): seq[i] = x})
  IN
    [val \in Range |-> CountOf(val)]

IsSorted(seq) ==
  \A i, j \in 1..Len(seq):
    i < j => seq[i] <= seq[j]

(*--fair algorithm sort
(* github highlighting is borked, unbork it *)
variables 
  input \in [1..4 -> 1..4]; 
  i = 1;
  is_sorted = FALSE;

define
  Correct == <>[](IsSorted(input))
  SameInput == [][UNCHANGED Counter(input)]_input
end define;

begin
  while ~is_sorted do
    is_sorted := TRUE;
    i := 1;
    while i <= Len(input)-1 do \* -1 b/c we do input[i + 1]
      if input[i] > input[i + 1] then
        is_sorted := FALSE;
        input[i] := input[i+1] || input[i+1] := input[i];
        end if;
      i := i + 1;
    end while;
  end while;
  \* input[1] := 0;
end algorithm;*)

====