Hello Prof. Alexandre Duret-Lutz Is it possible to do a straightforward intersection between 2 automatas and check if the intersection has an accepting state? Regards, Phillip
Hello, I think I found the way: aut1.intersecting_run(aut2).aut.is_empty() Regards, Philipp On Mon, 23 Nov 2020 at 08:55, Philip Schwartz <pschwartz090@gmail.com> wrote:
Hello Prof. Alexandre Duret-Lutz
Is it possible to do a straightforward intersection between 2 automatas and check if the intersection has an accepting state?
Regards, Phillip
On Mon, Nov 23, 2020 at 7:55 AM Philip Schwartz <pschwartz090@gmail.com> wrote:
Hello Prof. Alexandre Duret-Lutz
Is it possible to do a straightforward intersection between 2 automatas and check if the intersection has an accepting state?
if aut1.intersects(aut2): ... -- Alexandre Duret-Lutz
Thank you very much. Can I transfer this word to an automata - "!p2; p1 & p2; !p1 & !p2; cycle{p1 & !p2}" using spot translate? Regards, Phillipp On Mon, 23 Nov 2020 at 10:31, Alexandre Duret-Lutz <adl@lrde.epita.fr> wrote:
On Mon, Nov 23, 2020 at 7:55 AM Philip Schwartz <pschwartz090@gmail.com> wrote:
Hello Prof. Alexandre Duret-Lutz
Is it possible to do a straightforward intersection between 2 automatas
and check if the intersection has an accepting state?
if aut1.intersects(aut2): ...
-- Alexandre Duret-Lutz
Hello, I think I figured it out, just using LTL syntax - "!p2 & X(p1 & p2) & XX(!p1 & !p2) & XXX{p1 & p2}" Regards, Phillipp On Mon, 23 Nov 2020 at 11:14, Philip Schwartz <pschwartz090@gmail.com> wrote:
Thank you very much.
Can I transfer this word to an automata - "!p2; p1 & p2; !p1 & !p2; cycle{p1 & !p2}" using spot translate?
Regards, Phillipp
On Mon, 23 Nov 2020 at 10:31, Alexandre Duret-Lutz <adl@lrde.epita.fr> wrote:
On Mon, Nov 23, 2020 at 7:55 AM Philip Schwartz <pschwartz090@gmail.com> wrote:
Hello Prof. Alexandre Duret-Lutz
Is it possible to do a straightforward intersection between 2 automatas
and check if the intersection has an accepting state?
if aut1.intersects(aut2): ...
-- Alexandre Duret-Lutz
On Mon, 23 Nov 2020 at 11:14, Philip Schwartz <pschwartz090@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@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)".
participants (2)
-
Alexandre Duret-Lutz -
Philip Schwartz