• Alexandre Duret-Lutz's avatar
    simplifier: new LTL simplifications · d5b2de7f
    Alexandre Duret-Lutz authored
    if e is pure eventuality and g => e, then e U g = Fg
    if u is purely universal and u => g, then u R g = Gg
    
    Fixes #93.
    
    * doc/tl/tl.tex, NEWS: Document the rules.
    * spot/tl/simplify.cc: Implement them.
    * tests/core/reduccmp.test: Test them.
    * tests/core/det.test: Adjust.
    d5b2de7f
det.test 5.69 KB