Here you can ask questions and find or give answers to organizational, academic and other questions about studying computer science.

1.1k questions

1.2k answers


546 users

0 votes

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?

in * TF "Emb. Sys. and Rob." by (150 points)

1 Answer

0 votes
Best answer

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;

by (166k points)
selected by
Imprint | Privacy Policy