Skip to content

Instantly share code, notes, and snippets.

@mohanr
Created December 22, 2022 05:06
Show Gist options
  • Save mohanr/41c55a5a98ae7397aa34085994d631f7 to your computer and use it in GitHub Desktop.
Save mohanr/41c55a5a98ae7397aa34085994d631f7 to your computer and use it in GitHub Desktop.
\* 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
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment