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