BD Model Checking verds -ck 3 me005.vvm VERSION: verds 1.30 - AUG 2010 FILE: me005.vvm PROPERTY: AG((!(p0.a=1)|AF(p0.a=2))& (!(p1.a=1)|AF(p1.a=2))) CONCLUSION: FALSE (time=0) Remark: Needs an additional fairness constraint: a!=s2 for the 2 processes
{}