• Alexandre Duret-Lutz's avatar
    Add LTL reductions for strong release. · f003c3d1
    Alexandre Duret-Lutz authored
    * src/ltlvisit/basicreduce.cc: Perform the following reductions.
    a R (b & F(a)) = a M b
    a M (b & F(a)) = a M b
    a R Fa = Fa
    a M Fa = Fa
    a R b & Fa = a M b
    a R b & a M c = a M (b & c)
    a M b & a M c = a M (b & c)
    * src/ltltest/reduccmp.test: More tests.
    f003c3d1
basicreduce.cc 18.5 KB