bayermoore_translation.tla

\* BEGIN TRANSLATION (chksum(pcal) = "e913b13a" /\ chksum(tla) = "2d410eef")
CONSTANT defaultInitValue
VARIABLES i, m, l, n, j, k, p, skips, x, y, flag, pc

vars == << i, m, l, n, j, k, p, skips, x, y, flag, pc >>

Init == (* Global variables *)
        /\ i = defaultInitValue
        /\ m = defaultInitValue
        /\ l = defaultInitValue
        /\ n = defaultInitValue
        /\ j = defaultInitValue
        /\ k = defaultInitValue
        /\ p = defaultInitValue
        /\ skips = defaultInitValue
        /\ x = defaultInitValue
        /\ y = defaultInitValue
        /\ flag = [g \in 0..256 |-> -1]
        /\ pc = "Lbl_1"

Lbl_1 == /\ pc = "Lbl_1"
         /\ i' = 1
         /\ pc' = "Lbl_2"
         /\ UNCHANGED << m, l, n, j, k, p, skips, x, y, flag >>

Lbl_2 == /\ pc = "Lbl_2"
         /\ IF i < Len(pattern)
               THEN /\ p' = struct[pattern[i]]
                    /\ flag' = [flag EXCEPT ![p'] = 1]
                    /\ i' = i + 1
                    /\ pc' = "Lbl_2"
                    /\ UNCHANGED << m, n, k >>
               ELSE /\ i' = 1
                    /\ m' = Len(pattern)
                    /\ n' = Len(text)
                    /\ k' = n' - m'
                    /\ pc' = "Lbl_3"
                    /\ UNCHANGED << p, flag >>
         /\ UNCHANGED << l, j, skips, x, y >>

Lbl_3 == /\ pc = "Lbl_3"
         /\ IF i <= k
               THEN /\ skips' = 0
                    /\ j' = m - 1
                    /\ pc' = "Lbl_4"
               ELSE /\ pc' = "Done"
                    /\ UNCHANGED << j, skips >>
         /\ UNCHANGED << i, m, l, n, k, p, x, y, flag >>

Lbl_4 == /\ pc = "Lbl_4"
         /\ IF j >= 0
               THEN /\ x' = struct[pattern[j+1]]
                    /\ y' = struct[text[i + j]]
                    /\ PrintT(( "i " \o ToString(i) \o " j " \o ToString(j)))
                    /\ IF x' # y'
                          THEN /\ skips' = Max(1,j - flag[y'])
                               /\ j' = -1
                          ELSE /\ TRUE
                               /\ UNCHANGED << j, skips >>
                    /\ pc' = "Lbl_5"
                    /\ i' = i
               ELSE /\ i' = i + skips
                    /\ PrintT(("i - " \o ToString(i')))
                    /\ pc' = "Lbl_3"
                    /\ UNCHANGED << j, skips, x, y >>
         /\ UNCHANGED << m, l, n, k, p, flag >>

Lbl_5 == /\ pc = "Lbl_5"
         /\ j' = j - 1
         /\ pc' = "Lbl_4"
         /\ UNCHANGED << i, m, l, n, k, p, skips, x, y, flag >>

(* Allow infinite stuttering to prevent deadlock on termination. *)
Terminating == pc = "Done" /\ UNCHANGED vars

Next == Lbl_1 \/ Lbl_2 \/ Lbl_3 \/ Lbl_4 \/ Lbl_5
           \/ Terminating

Spec == Init /\ [][Next]_vars

Termination == <>(pc = "Done")

\* END TRANSLATION