Skip to content
  • Alexandre Duret-Lutz's avatar
    simplifier: new PSL simplifications · abff7eba
    Alexandre Duret-Lutz authored
    {e[*0..j]}<>->f = {e[*1..j]}<>->f
    {e[*0..j]}[]->f = {e[*1..j]}[]->f
    
    Fixes #81.
    
    This required a small change to the bounded-star-normal-form to prevent
    infinite recursion.
    
    * spot/tl/simplify.cc: Implement these rules.
    * doc/tl/tl.tex, NEWS: Document them.
    * tests/core/reduccmp.test: Add tests, and adjust others.
    * tests/core/unambig.test: Replace formula that used to generated an
    ambiguous automaton, but now generates a deterministic one.
    abff7eba