Skip to content
  • Alexandre Duret-Lutz's avatar
    Add LTL reductions for weak until. · 80ceca59
    Alexandre Duret-Lutz authored
    * src/ltlvisit/basicreduce.cc: Perform the following reductions.
    a U (b | Ga) = a W b
    a W (b | Ga) = a W b
    a U b | Ga = a W b
    a U b | a W c = a W (b | c)
    a W b | a W c = a W (b | c)
    a U Ga = Ga
    a W Ga = Ga
    * src/ltltest/reduccmp.test: More tests.
    80ceca59