bugfix: infinite loop in the executeAll
bugfix: If there is no proof model in the simulator, the simulation will
still work
we can now choose the initialization value of the CTL