310N/Alogic CspCASL

310N/Aspec tcs3 =

310N/Adata sorts S, T

310N/A ops f: S ->? T

310N/A . forall x: S . not def f(x);

310N/Aprocess

310N/A tcs3: S, T

310N/A tcs3 = [] x:S -> f(x) -> SKIP [| T |] [] y : T -> (if def y then SKIP else STOP)

310N/A