counter-examples

[davidebasile]

for an empty synthesis, it is useful to provide a trace leading to a forbidden state that cannot be blocked.
For a non-empty synthesis, it is useful to visualize the "cut" performed by the synthesis, which was called the set of liable transitions.