[Spot] Acceptance check in Spot

Alexandre Duret-Lutz adl at lrde.epita.fr
Tue Sep 29 18:00:57 CEST 2015


On Tue, Sep 29, 2015 at 5:09 PM, Matthias Heizmann
<heizmann at informatik.uni-freiburg.de> wrote:
> Hi Spot developers,
>
> I just extended our automata library
> https://ultimate.informatik.uni-freiburg.de/?ui=int&tool=automata_script_interpreter&task=automataScript&sample=1954831617
> with support to  write Büchi automata in the HOA format.

Sweet!

> Now, I just wanted to check a few results without implementing
> support to read HOA files.
> Syntactically my files seem to be correct, (example attached, file
> is read by Spot), but I also wanted to do some semantic check,
> e.g., test if a certain word is accepted.

>From a semantic point of view, I suspect that you may have a problem
because the HOA format assumes that the alphabet is 2^AP (i.e., each
letter is an assignment of all atomic propositions), not AP.
So the automaton you attached also accepts an infinite word where each
letter is a&b, which somehow contradicts the name of the file.

> Spot provides quite a number of sophisticated operations but I did not
> find something "simple" like an acceptance check.
> Have I overlooked it or is it not documented?
> For my purpose it is sufficient if it works on the "usual" Büchi automata.

You did not overlook anything: Spot does not export such a feature.
I'll add that to the todo list.

Currently, you can still check acceptance of a word by representing
this word as an automaton, and testing the interstection of the two
automata using autfilt's --intersect option.

If you can write your word as an LTL or PSL formula, is it even
easier than writing an automaton.
E.g. testing the word  a&!b ; b&!a ; followed by a cycle of just a&b

% ltl2tgba -f "(a & !b) & X(b & !a) & XXG(a & b)" -H |
    autfilt -q --intersect FinitelyManyAWithSink.hoa - &&
     echo accepted || echo non-accepted
accepted


I guess you could restrict the FinitelyManyAWithSink.hoa
to disallow a and b to be accepted at the same time.
autfilt --exclusive-ap can be handy for that:

% autfilt --exclusive-ap=a,b FinitelyManyAWithSink.hoa -H > F2.hoa

Now you can evaluate words (via LTL) as if the alphabet was AP:

% ltl2tgba -f "a & X(b) & XXG(b)" -H |
    autfilt -q --intersect F2.hoa - && echo accepted || echo non-accepted
accepted

% ltl2tgba -f "a & X(b) & XXG(a)" -H |
    autfilt -q --intersect F2.hoa - && echo accepted || echo non-accepted
non-accepted


(Note that --intersect is a filter.  Without the -q option it returns the
automata that interesect the reference automaton.  If you want to
compute the product of two automata to check the intersection
by yourself, use --product instead.)

HTH
-- 
Alexandre Duret-Lutz


More information about the Spot mailing list