MODULE one-bit-chan(input)
VAR
   output : boolean;
ASSIGN
   next(output) := {input,output};
FAIRNESS running
FAIRNESS (input=0 -> AF output=0) & (input=1 -> AF output=1)

MODULE two-bit-chan(input1,input2)
VAR
   forget : boolean;
   output1 : boolean;
   output2 : boolean;
ASSIGN
   next(output1) := case
                      forget : output1;
                      1:       input1;
                    esac;
   next(output2) := case
                      forget : output2;
                      1:       input2;
                    esac;
FAIRNESS running
FAIRNESS !forget