// Reachability
<<robot>> Pmax=? [ F "goal1" ]