const int k; // step bound in formula

// 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?
Pmax=?[ !"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{"moves"}min=? [ F ("goal1" | "goal2") ]
// minimum probability the robot can reach a goal2 state
Pmin=? [ F "goal2" ]
// minimum probability the robot can reach a goal2 state
Pmax=? [ F "goal2" ]
// minimum probability the robot can reach a goal1 state within k steps
Pmin=? [ F<=k "goal2" ]
// maximum probability the robot can reach a goal2 state within k steps
Pmax=? [ F<=k "goal2" ]
// maximum probability the robot never reaches a hazard state
Pmax=? [ G !"hazard" ]
// maximum probability a goal1 state is reached infinitely often
Pmax=? [ G F "goal1" ]
// maximum probability the robot never reaches a hazard state and reaches a goal1 state infinitely often
Pmax=? [ (G !"hazard")&(G F "goal1") ]

// (multi-objective query) pareto curve construction
multi(Pmax=? [ G !"hazard" ], Pmax=? [ G F "goal1" ])