Lower and upper bound not including the correct probability

[zgzn]

The probability bound generated by STAMINA does not include the correct probability for the cluster model with the qos1 property (http://qcomp.org/competition/2020/benchmarks.html). See attached log for results.
qcomp2020_cluster_qos1_result.txt

[RileyLRoberts]

@zgzn Zhen, I took a look at this example, and we get the wrong answer with STAMINA 2.0, in fact, even more wrong then before. Less states are generated in STAMINA 2.0, so my theory is that our method of determining Pmin and Pmax is wrong for this type of property. I'm not familiar with this type of property, can you explain the meaning? Here is the property: "qos1": P=? [ F<=2000 !"minimum" ];