rewrite LTL/PSL formulas using some pattern matching rule
We would like to have a function that takes a formula f
, a rewriting rule r
, and return the formula f'
after applying the rewriting rule r
.
I'm thinking about something like:
formula rewrite(formula f, const char* rule);
So for instance
formula f1 = spot::parse_formula("FX(a & b)|Gb");
formula f2 = rewrite(f1, "FX(f) = XF(f)");
std::cout << f2 << '\n';
would print XF(a & b) | Gb
.
The main objective is to design a language to represent a rule
. It should ideally be able to represent most of the rewriting rules of section 5.4 of tl.pdf
, including the specification of constraints on subformulas (like, "this subformula should be purely eventual") or between subformulas ("this subformula should imply that other subformula"). Once we have that language, we would like be able to parse it and execute it. It might make sense to expose these two steps in the API (just like we have regcomp()
and regexec()
in POSIX) instead of just rewrite()
as above, so that we can apply the same rule to several formulas without parsing it each time.
For reference, all rules of sections 5.4 are currently hard-coded in spot/tl/simplify.cc
. This is the largest file in Spot and it has become a pain to maintain by hand. There are also some quick examples of how to manipulate formula
objects
in tut01 and tut03.