// the probability of eventually reaching state 16, corresponding to the successful completetion of the workflow
P>0.8[F(s=16)]
filter(forall,P<=0.035[F(s=13)],s=1)
// the probability of eventually reaching state 16, corresponding to the successful completetion of the workflow
P=?[F(s=16)]
// This gives the maximum value, starting from any state satisfying s=1, of the probability of reaching the express service "fail" state 13
//filter(max,P=?[F(s=13)],s=1)
P<0.06[F s=5]
//P=?[F s=5]