15 May
15 May
7:32 p.m.
Hi David,
The following one might be helpful.
http://ltlf2dfa.diag.uniroma1.it/
Best,
Shufang
On Sat, May 14, 2022 at 11:16 PM David Lidell <lidelld(a)chalmers.se> wrote:
Hi!
I am a PhD student from the University of Gothenburg, and I am currently
working a lot with LTL extended with the past operators Y and S. Spot is a
fantastic tool, but it unfortunately doesn't support these operators.
I'm wondering whether there have been any discussions on extending Spot to
support them, and if the developers have any idea of how difficult that
would be?
Thanks!
_______________________________________________
Spot mailing list -- spot(a)lrde.epita.fr
To unsubscribe send an email to spot-leave(a)lrde.epita.fr
10:14 a.m.
David Lidell <lidelld(a)chalmers.se> writes:
I'm wondering whether there have been any
discussions on extending
Spot to support them, and if the developers have any idea of how
difficult that would be?
Yes, supporting the past would be helpful. The main issue would be
to be able to translate those into automata. I'm not very familiar
with translation of past operators; but unless there are tricks that
can be use to translate the past and the future separately, I don't
think our current translations would be easy to extend.
996
days inactive
1001
days old
4 comments
3 participants
participants (3)
-
Alexandre Duret-Lutz -
David Lidell -
Shufang Zhu