optimize the execution of the model checker. 

Give to eat to the simulator, just the external events that are in the
field event of each state.
Added better printing when an error is found.