Legality check
Add to the check menu the possibility of checking if one process is legal with respect to another process.
When the composite process selected in the pull down menu is the composition of exactly two other processes, a new window should appear. Assuming ||C = (A || B), the window should allow me to select if I want to check if A is legal with respect to B or the other way round.
Assuming I select to check if A is legal with respect to B:
It should also allow me to select a predefined set of actions (defined with syntax like “set S = {a, b}”) as the set of controlled actions of A. Upon selecting and pressing the check button, it should let me know if in the composition C there is a state in which the current state of B there is an action act not in S that is not in the current state of A.
If this is the case, a trace in the composition to that state should be shown and the action act reported.