bayermoore.tla

----------------------------- MODULE bayermoore -----------------------------
EXTENDS Integers, Sequences,Naturals, TLC
CONSTANTS Character, text, pattern
ASSUME text \in Seq(Character)
ASSUME pattern \in Seq(Character)
Max(x,y) == IF x < y THEN y ELSE x
struct == [a |-> 97, b |-> 98, c |-> 99]
(*--algorithm bayermoore

variables
           i,m,l,n,j,k,p,skips,x,y,
           flag = [g \in 0..256 |-> -1];

begin
 i := 1;          

 while i < Len(pattern) do
  p := struct[pattern[i]];
  flag[p] := 1;
  i := i + 1;
 end while;
 
 
i := 1;          
m := Len(pattern);
n := Len(text); 
k := n - m;
 while i <= k do
  skips := 0;
     j := m - 1;
     while j >= 0 do
            x := struct[pattern[j+1]];
            y := struct[text[i + j]];
            \* print ( "x " \o ToString(x) \o "y " \o ToString(y) );
            print ( "i " \o ToString(i) \o " j " \o ToString(j));
        if x # y then
            skips := Max(1,j - flag[y]);
            j := -1;
        end if;
        j :=  j - 1;
     end while;
  i := i + skips;  
  print ("i - " \o ToString(i)); 
 end while;
 end algorithm; *)