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)