Using BDD-based Bounded Model Checking
Formula ((EF(E< proc0.allowed >X(proc0.in)) AND EF(E< proc1.allowed >X(proc1.in))) AND EF(E< proc2.allowed >X(proc2.in))) holds
Using BDD-based Bounded Model Checking
Formula EF(((proc0.approach AND proc1.approach) AND proc2.approach)) holds
Using BDD-based Bounded Model Checking
Formula AG((proc0.in IMPLIES K[proc0]((~proc1.in AND ~proc2.in)))) holds
Using BDD-based Bounded Model Checking
Formula AG((proc0.in IMPLIES C[proc0 proc1 proc2]((~proc1.in AND ~proc2.in)))) holds
