17 May
2019
17 May
'19
9:02 p.m.
On Fri, May 17, 2019 at 5:16 PM Victor Khomenko
<victor.khomenko(a)newcastle.ac.uk> wrote:
Hi Alexandre,
I've just tried to use the development version at https://spot-dev.lrde.epita.fr/app/
and fed it the following formula (which is ugly but simple, just {SERE} |-> bool), and
it died of "500 Internal Server Error".
{(((((((!"a")##1(!"b"))##0("c" <->
"d"))##0("e" xor "f"))##0(((((("g" &
"h") xor "i") <-> "j") | "k") &
"l") | "m"))##0(("n" & "o") | (!"n"
& "p")))##0("q" -> ("r" <->
"s")))##[0:1]"t"} |-> "u"
Hi Victor,
Thanks for this report.
I checked from the command-line, and ltl2tgba has no trouble
translating this formula or its negation to to a 4 state DBA.
One issue is that when converting this automaton to GraphViz, one of
the edge labels is over 42000-character long (!), and apparently
GraphViz has a 16k limit.
It dies with:
Error: foo.dot: syntax error in line 13 scanning a HTML string
(missing '>'? bad nesting? longer than 16384?)
You learn every day... I guess it makes no sense to display such huge
labels anyway and that Spot replace those by "(label too long)".
This issue is causing the error in the "TRANSLATE" tab.
However the "STUDY" tab has two different issues with this formula.
1. it fails to display the "circular progress" animation while waiting
2. it actually times outs in the function that decides if an automaton
is a liveness property because of the size of 2^AP.
I have two ideas to improve that.
--
Alexandre Duret-Lutz