const int k; // step bound used in properties

// the probability the robot reaches a goal1 state is at least 0.2
P>=1[ F "goal2" ]
// the probability the robot never visits a hazard state is at most 0.1
P<=0.1[ G !"hazard" ]
// what is the probability that the robot reaches a state labelled with either goal1 or goal2, while avoiding hazard-labelled states, during the first k steps of operation?
P=?[ !"hazard" U<=k ("goal1" | "goal2") ]
//the expected number of times the robot visits a hazard labelled state during the first k steps is at most 4.5 
R{"r1"}<=4.5 [ C<=k ] 
// what is the expected number of steps required by the robot before reaching a state labelled goal1 or goal2?
R{"r2"}=? [ F ("goal1" | "goal2") ]