ltlgrind

This tool lists formulas that are similar to but simpler than a given formula by applying simple mutations to it, like removing operands or formulas that are similar to but simpler than a given formula by applying simple mutations to it, like removing operands or operators. This is meant to be used with ltlcross to simplify a formula that caused a problem before trying to debug it (see also ltlcross --grind=FILENAME).

Here is a list of the different kinds of mutations that can be applied:

--ap-to-const          atomic propositions are replaced with true/false
--remove-multop-operands   remove one operand from multops
--remove-one-ap        all occurrences of an atomic proposition are
                       replaced with another atomic proposition used in
                       the formula
--remove-ops           replace unary/binary operators with one of their
                       operands
--rewrite-ops          rewrite operators that have a semantically simpler
                       form: a U b becomes a W b, etc.
--simplify-bounds      on a bounded unary operator, decrement one of the
                       bounds, or set min to 0 or max to unbounded
--split-ops            when an operator can be expressed as a
                       conjunction/disjunction using simpler operators,
                       each term of the conjunction/disjunction is a
                       mutation. e.g. a <-> b can be written as ((a & b)
                       | (!a & !b)) or as ((a -> b) & (b -> a)) so those
                       four terms can be a mutation of a <-> b

By default, all rules are applied. But if one or more rules are specified, only those will be applied.

ltlgrind -f 'a U G(b <-> c)' --split-ops --rewrite-ops --remove-ops

a
G(b <-> c)
a W G(b <-> c)
a U (b <-> c)
a U Gb
a U Gc
a U G(b -> c)
a U G(c -> b)
a U G(b & c)
a U G(!b & !c)

The idea behind this tool is that when a bogus algorithm is found with ltlcross, you probably want to debug it using a smaller formula than the one found by ltlcross. So you would give the formula found by ltlcross as an argument to ltlgrind and then use the resulting mutations as a new input for ltlcross. It might report an error on one of the mutation, which is guaranteed to be simpler than the initial formula. The process can then be repeated until no error is reported by ltlcross.

Since the whole process can become quite tedious, it can be done automatically by calling ltlcross with the --grind=FILENAME argument.