A sample of the simulation equivalence test.
The test reports that the current automaton (which equals <> p)
can simulate the target automaton (which equals <>[]p).
But this is not true in the other direction.
You have to choose a target automaton after the function is triggered. This function checks if the initial state of the current automaton can be simulated by the initial state of the target automaton, and vice versa.