Commit a889dd7d authored by Alexandre Duret-Lutz's avatar Alexandre Duret-Lutz
Browse files


parent 25e6cca4
......@@ -73,7 +73,7 @@ namespace spot
fact_.add_relation(bdd_apply(now, x | next, bddop_biimp));
`x | next', doesn't actually encode the fact that x
should be fulfilled at eventually. We ensure
should be fulfilled eventually. We ensure
this by creating a new generalized Bchi accepting set,
Acc[x], and leave any transition going to NEXT without
checking X out of this set. Such accepting conditions
Supports Markdown
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment