initial state pairs in greatest simulation relation - difference between teaching tool and exercise

Question

The teaching tool does not consider {S2,Q3} as an initial state pair, while the exercise does (also K1<=K2). 

Why is that the case?

Answer 1

It does when I tried; maybe you missed the right specification of the variables of the Kripke structures. Here is my input:

for K1 

vars a;
init 0;
labels 0:; 1:; 2:a;
transitions 0->1; 1->1; 1->2; 2->0;

for K2

vars a,b;
init 0,2,3;
labels 0:; 1:; 2:a; 3:a,b;
transitions 0->1; 1->1; 1->2; 1->3; 2->0; 2->1; 3->0;