-
Alexandre Duret-Lutz authored
star_normal_form() used to be called under bounded repetitions like [*0..4], but some of these rewritings are only correct for [*0..]. For instance (a*|1)[*] can be rewritten to 1[*] but (a*|1)[*0..1] cannot be rewritten to 1[*0..1] it would be correct to rewrite the latter as (a[+]|1)[*0..1], canceling the empty word in a*. Also (a*;b*)[*] can be rewritten to (a|b)[*] but (a*;b*)[*0..1] cannot be rewritten to (a|b)[*0..1] and it cannot either be rewritten to (a[+]|b[+])[*0..1]. This patch introduces a new function to implement rewritings under bounded repetition. * src/ltlvisit/snf.hh, src/ltlvisit/snf.cc (star_normal_form_unbounded): New function. * src/ltlvisit/simplify.cc: Use it. * src/ltltest/reduccmp.test: Add tests. * doc/tl/tl.tex: Document the rewritings implemented.
05ed3def