//The computation will eventually halt.
ltl: eventually output.halt>0;
ctl: eventually output.halt>0;
//The computation will eventually halt with either a `yes' or `no' result.
ltl: output.halt = 0 until (output.halt > 0 and (output.yes > 0 or output.no > 0));
ctl: output.halt = 0 until (output.halt > 0 and (output.yes > 0 or output.no > 0));
//A `yes' result is eventually observed within `no' more than three steps.
ltl: eventually (output.yes > 0 and output.step <= 3);
ctl: eventually (output.yes > 0 and output.step <= 3);