ratexp_trad_visitor handling of one_star
[*]
a.k.a. one_star()
is the PSL equivalent of Σ*. Maybe next_to_concat()
could encode this as bddtrue
? This would allow formula like (α∧β)∨(¬α∧[*])
to be simplified as β∨(¬α∧[*])
. I'm just a bit afraid that several places that expect a next variable will have to be adjusted to interpret bddtrue
as [*]
.