Formal Definition for Watcher

The Watcher index cell is described by ic = (X,Y,S,so,A,tmax,f,g) where:

X is {m1, m2}

Y is {m0, m3}

S is {s0, s1}

so in S is the initial state.

A is {a1, a5}.

f and g functions can be derived from the transition diagram.