const int k;
const double p;

// Reachability
Pmax=? [ F "goal1" ]

// Bounded reachability
Pmax=? [ F<=k "goal2" ]

// Half an LTL formula
Pmax=? [ G !"hazard" ]

// A simple LTL formula
Pmax=? [ G F "goal1" ]

// Another LTL formula
Pmax=? [ (G !"hazard")&(G F "goal1") ]

// Check can reach goal2 with prob 1
Pmax=? [ F "goal2" ]

// Rewards: best exp time to reach goal2
R{"time"}min=? [ F "goal2" ]

// Pareto
multi(Pmax=? [ G !"hazard" ], Pmax=? [ G F "goal1" ])

// Pareto (swap axes)
multi(Pmax=? [ G F "goal1" ], Pmax=? [ G !"hazard" ])

// Approximate Pareto with numerical
multi(Pmax=? [ G F "goal1" ], P>=p [ G !"hazard" ])

// Approximate Pareto with numerical (swap axes)
multi(Pmax=? [ G !"hazard" ], P>=p [ G F "goal1" ])