• Alexandre Duret-Lutz's avatar
    snf: Fix the handling of bounded repetition. · 05ed3def
    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
snf.hh 1.97 KB