Computation of the simulation according to the algorithm in the
lecture notes (note the definition of simulation and the algorithm
for computing it must be written on the exam solution, also all
tuple deletions must be briefly justified).


R_0

(t1,s1q1)
%removed (t1,s1q2) - t1 final, s2q1 not final
%removed (t1,s2q1) - t1 final, s2q1 not final
%removed (t1,s2q2) - t1 final, s2q2 not final

(t2,s1q1)
(t2,s1q2)
(t2,s2q1)
(t2,s2q2)

(t3,s1q1)
(t3,s1q2)
(t3,s2q1)
(t3,s2q2)

(t4,s1q1)
(t4,s1q2)
(t4,s2q1)
(t4,s2q2)


R_1

(t1,s1q1)
%removed (t1,s1q2) 
%removed (t1,s2q1)
%removed (t1,s2q2)

(t2,s1q1)
(t2,s1q2) 
(t2,s2q1) 
(t2,s2q2) 


(t3,s1q1)
(t3,s1q2) 
remove (t3,s2q1) t3 can do a s2q1 cannot
(t3,s2q2) 

(t4,s1q1)
(t4,s1q2)
(t4,s2q1) 
remove (t4,s2q2) - t2 can do b going to t3, s2q2 can do c with 2  going to s2q1 
                               but (t3,s2q1) not in R_0 (s2q1 is not Final)

R_2

(t1,s1q1)
%removed (t1,s1q2) 
%removed (t1,s2q1)
%removed (t1,s2q2)

(t2,s1q1)
(t2,s1q2) 
(t2,s2q1) 
remove (t2,s2q2) - t2 can do c going to t3, s2q2 can do c with 2  going to s2q1 
                               but (t3,s2q1) not in R_1

(t3,s1q1)
(t3,s1q2) 
%removed (t3,s2q1) 
(t3,s2q2) 

(t4,s1q1)
(t4,s1q2)
(t4,s2q1)
%removed (t4,s2q2)

R_3

(t1,s1q1)
%removed (t1,s1q2) 
%removed (t1,s2q1)
%removed (t1,s2q2)

(t2,s1q1)
(t2,s1q2) 
(t2,s2q1) 
%remove (t2,s2q2)

(t3,s1q1)
(t3,s1q2) 
%removed (t3,s2q1) 
(t3,s2q2) 

(t4,s1q1)
(t4,s1q2)
(t4,s2q1)
%removed (t4,s2q2)

At R_3 we cannot eliminate any tuple from the relation: i.e, R_3 is the
result of the algorithm (the greatest simulation relation).



Now, on the basis of the greatest simulation relation, we can
compute the output function of the orchestrator generator - see
lecture notes (note such output function must be written on the exam
solution):

W(t1,s1q1,a) = {1}

W(t2,s1q1,b) = {2}
W(t2,s1q1,c) = {2}
W(t2,s1q2,b) = {2}
W(t2,s1q2,c) = {2}
W(t2,s2q1,b) = {1,2}
W(t2,s2q1,c) = {2}

W(t3,s1q1,a) = {1}
W(t3,s1q2,a) = {2}
W(t3,s2q2,a) = {2}

W(t4,s1q1,b) = {2}
W(t4,s1q2,b) = {2}
W(t4,s2q1,b) = {1}

Any choice of the index, at each point in time, according to the above
function guarantees a composition.