// max probability of reaching the error state
Pmax
=? [
F
(
error
=
1
) ]