logic CspCASL

spec tcs3 =

data sorts S, T

ops f: S ->? T

. forall x: S . not def f(x);

process

tcs3: S, T

tcs3 = [] x@S -> f(x) -> SKIP [| T |] [] y @ T -> (if def y then SKIP else STOP)