Skip to content
  • Alexandre Duret-Lutz's avatar
    More simplifications rules for M. · 1a912089
    Alexandre Duret-Lutz authored
    * src/ltlvisit/reduce.cc (reduce_visitor): Add the following
    implication rewriting rules:
    a M (b M c) = a M c if a implies b.
    a M (b R c) = a M c if a implies b.
    a R (b R c) = a R c if a implies b.
    a R (b M c) = b M c if b implies a.
    a M (b M c) = b M c if b implies a.
    The latter rule was fixed from an incorrectly copied&pasted
    rule for a M (b R c) = b R c if b implies a (this is wrong).
    * src/ltltest/reduccmp.test: Add more tests.
    1a912089