24 Nov
2020
24 Nov
'20
11:51 a.m.
On Mon, 23 Nov 2020 at 11:14, Philip Schwartz
<pschwartz090(a)gmail.com> wrote:
> Can I transfer this word to an automata - "!p2; p1 & p2; !p1 & !p2;
cycle{p1 & !p2}" using spot translate?
Use parse_word() and then convert the result to an automaton using
as_automaton().
See bottom of https://spot-dev.lrde.epita.fr/ipynb/word.html
On Mon, Nov 23, 2020 at 4:41 PM Philip Schwartz <pschwartz090(a)gmail.com> wrote:
I think I figured it out, just using LTL syntax -
"!p2 & X(p1 & p2) & XX(!p1 & !p2) & XXX{p1 & p2}"
Not really. The above LTL formula only constraints the 4 first step of
the words it matches.
As if you had used the word "!p2; p1 & p2; !p1 & !p2; p1 & p2;
cycle{true}".
The word "!p2; p1 & p2; !p1 & !p2; cycle{p1 & !p2}" mentioned
earlier could be
written using LTL as "!p2 & X(p1 & p2) & XX(!p1 & !p2) & XXXG(p1
& !p2)".
Or using PSL as "{!p2; p1 & p2; !p1 & !p2}<>=>G(p1 &
!p2)".