(* complete the following definitions *)
(* implementation *)
agent A(a,b,c,d) = 
agent B(a,b,c,d) = 
agent C(a,b,c,d) = 
agent D(a,b,c,d) = 
agent S(a0,a1,b0,b1) = 

(* specification *)
agent Scheduler(a0,a1,b0,b1) = Sched1(a0,a1,b0,b1)
agent Sched1(a0,a1,b0,b1) = (a1.Sched01(a0,a1,b0,b1))
agent Sched11(a0,a1,b0,b1) = (b1.Sched1(a0,a1,b0,b1))
agent Sched10(a0,a1,b0,b1) = (b0.Sched1(a0,a1,b0,b1) + a1.Sched001(a0,a1,b0,b1))
agent Sched101(a0,a1,b0,b1) = (b0.Sched11(a0,a1,b0,b1) + b1.Sched10(a0,a1,b0,b1))
agent Sched0(a0,a1,b0,b1) = 
agent Sched01(a0,a1,b0,b1) = 
agent Sched00(a0,a1,b0,b1) = 
agent Sched001(a0,a1,b0,b1) = 

(* check if this implementation and the specification are weakly bisimilar *)
(* hint: use the command weqd *)


(* if they are not bisimilar, try to find why by using the command step *)
(* to explore the reduction graph of the processes *)