Two bugs in Timed Rebeca is fixed (the model checking result is changed for Probabilistic Timed Rebeca extension as it uses Timed Rebeca state space generation engine)