Product of two Kripke Structures

Question

I am trying to compute the product of two Kripke structures of the following form:

K1: vars a,c,d;

init 0,1;

labels 0:; 1:a,c,d; 2:a;

transitions 0->1; 0->2; 1->2; 2->0; 2->2;

and

K2: vars b,c,d;

init 2;

labels 0:c,d; 1:b,c,d; 2:;

transitions 0->1; 0->2; 1->2; 2->0; 2->2;

i tried with both hand and tool to solve the product and this is the resultant Kripse Structure I get (after eliminating the unreachable state and its edges):

K1*K2= vars a,c,d;

init 0;

labels 0:; 1:a,c,d; 2:a,;

transitions 0->1; 0->2; 1->2; 2->0; 2->2;

But the Solution is not getting accepted by the exercise automated checker. Am i doing something wrong here?

Please help!

Answer 1

If K1 is defined on variables a,c,d and K2 is defined on variables b,c,d, then their product is defined on variables a,b,c,d .

Comments

Thank you KS. adding b to the list of variables worked.
I had removed the variable "b" as it was belonging to the unreachable state SQ2.

---

Yes, I have seen what you thought. But even though there is no state left which carries variable b, it is still known by the product and the states of the product state that b is false there. Not mentioned means false and not that it does not exist. It's a common mistake, I know.