{
 ch_m(empty), ch_w(empty), m, w.
 
 m :- m(s1).
 m(s1), ch_w(empty)  :- m(s2), ch_w(ini).
 m(s2), ch_m(ack)    :- m(s3), ch_m(empty).
 m(s3), timeout      :- m(s4).
 m(s4), ch_w(empty)  :- m(se), ch_w(shutup).
 m(s4), ch_w(empty)  :- m(s7), ch_w(dreq).
 m(s7), ch_m(data)   :- m(s8), ch_m(empty).
 m(s8), ch_w(empty)  :- m(s8), ch_w(data).
 m(s8), ch_w(empty)  :- m(se), ch_w(shutup).
 m(se), ch_m(shutup) :- m(sf), ch_m(empty).
 m(sf), ch_w(empty)  :- m(sg), ch_w(quiet).
 m(sg), ch_m(dead)   :- mEnd.
 
 w :- w(s1).
 w(s1), ch_w(ini)    :- w(s2), ch_w(empty).
 w(s2), ch_m(empty)  :- w(s3), ch_m(ack).
 w(s3), ch_w(dreq)   :- w(s5), ch_w(empty).
 w(s5), ch_m(empty)  :- w(s3), ch_m(data).
 w(s3), ch_w(data)   :- w(s3), ch_w(empty).
 w(s3), ch_w(shutup) :- w(s9), ch_w(empty).
 w(s9), ch_m(empty)  :- w(sc), ch_m(shutup).
 w(sc), ch_w(quiet)  :- w(sd), ch_w(empty).
 w(sd), ch_m(empty)  :- wEnd,  ch_m(dead).
}.
{$p,@p}/ :- \+($p=(mEnd,wEnd,$q)) | {timeout,$p,@p}.