I have this finite-state process with the corresponding labeled transition system:
The FSP is:
MAKER = (kochen -> fertig -> MAKER).
USER = (fertig -> essen -> USER).
||MAKER_USER = (USER||MAKER).
Why is essen
possible after the second kochen
? USER
needs to have fertig
in order to able to essen
right?