// to check properties need to use the digital clocks engine
const int T; // time bound in properties

// minimum expected time to reach goal2
R{"time"}min=? [ F "goal2" ]
// maximum expected time to reach goal2
R{"time"}max=? [ F "goal2" ]
// maximum probability of reaching a goal1 state by time T
Pmax=?[ F<=T "goal1" ]
// maximum probability of reaching a goal2 state by time T
Pmax=?[ F<=T "goal2" ]