18 Oct
2014
18 Oct
'14
1:47 a.m.
Hi Dennis,
On Sat, Oct 18, 2014 at 1:07 AM, Dennis Park <emaildpark(a)gmail.com> wrote:
More specifically, I would like to take an ltl
formula
spot::ltl::formula* f
and propagate all negations in f so that negations only occur before atomic
propositions. Does the Spot library support such a functionality?
Sure, you can even do it from the command line.
% ltlfilt --nnf -f '!G(a -> b)'
F(a & !b)
If so, where in the documentation could I find
information on it (I
tried to look for something like it in the documentation but had
trouble finding anything).
When you know it's called "negative normal form", it's easier to find
:-)
But without this, you can start from
http://spot.lip6.fr/refdoc/spot-latest/modules.html then click on
"rewriting LTL formulae", and explore what is available (the same
pages are included in doc/spot.html/ inside the tarball in case you
work off line).
There are basically two interfaces you may want to use, either the
spot::ltl::negative_normal_form() function, or the
spot::ltl::ltl_simplifier::negative_normal_form() method. The latter
uses a cache to speed up the rewriting of (sub)formulae that have
already been seen previously, so this is better if you have multiple
formulae to process. The former function is just a wrapper around the
latter: it creates a temporary spot::ltl::ltl_simplifier object just
for a one-shot usage.
Regarding the documentation, I should point that most of the existing
transformations applicable to LTL/PSL formulae (including negative
normal form) are documented in the file doc/tl/tl.pdf included in the
tarball. This document is mostly concerned about detailing what
rewriting rules are actually used, but it also points to the function
names implementing them.
--
Alexandre Duret-Lutz