C.tla

               See Specifying Systems section 6.6 on page 73.

--------------------------------- MODULE C ----------------------------------
EXTENDS Integers

S ==
    {"c","a","c","f"}

VARIABLE 
    \* @type: Str;
    x

-----------------------------------------------------------------------------

InitC ==
    x = CHOOSE n \in S: TRUE

NextC ==
    x' = CHOOSE n \in {"a","c","f","f","c","a"}: n \in S

SpecC == InitC /\ [][NextC]_x

-----------------------------------------------------------------------------

InitE ==
    x \in S

NextE ==
    x' \in {"a","c","f","f","c","a"}

SpecE == InitE /\ [][NextE]_x

-----------------------------------------------------------------------------

\* TLC
InvT ==
    [][x = x']_x

\* Apalache
InvA ==
    x = x'

=============================================================================