alarsyo/spot
1
0
Fork 0
Code Issues Pull requests Projects Releases Wiki Activity

dot: fix #392

Browse source 
* spot/twaalgos/dot.cc: Add tooltips to "..." states and edges.
* tests/core/readsave.test: Test this.
* tests/python/highlighting.ipynb: Adjust.
This commit is contained in:
Alexandre Duret-Lutz 2020-04-29 10:48:05 +02:00
parent 6706042019
commit 3ea63e9a75
3 changed files with 1009 additions and 991 deletions
Download patch file Download diff file Expand all files Collapse all files

9
spot/twaalgos/dot.cc
View file

@ -1,5 +1,5 @@
// -*- coding: utf-8 -*- // -*- coding: utf-8 -*-
// Copyright (C) 2011, 2012, 2014-2019 Laboratoire de Recherche // Copyright (C) 2011, 2012, 2014-2020 Laboratoire de Recherche
// et Développement de l'Epita (LRDE). // et Développement de l'Epita (LRDE).
// Copyright (C) 2003, 2004 Laboratoire d'Informatique de Paris 6 (LIP6), // Copyright (C) 2003, 2004 Laboratoire d'Informatique de Paris 6 (LIP6),
// département Systèmes Répartis Coopératifs (SRC), Université Pierre // département Systèmes Répartis Coopératifs (SRC), Université Pierre
@ -739,8 +739,11 @@ namespace spot
} }
os_ << "]\n"; os_ << "]\n";
if (incomplete_ && incomplete_->find(s) != incomplete_->end()) if (incomplete_ && incomplete_->find(s) != incomplete_->end())
os_ << " u" << s << " [label=\"...\", shape=none, width=0, height=0" os_ << " u" << s << (" [label=\"...\", shape=none, "
"]\n " << s << " -> u" << s << " [style=dashed]\n"; "width=0, height=0, "
"tooltip=\"hidden successors\"]\n ")
<< s << " -> u" << s << (" [style=dashed, "
"tooltip=\"hidden successors\"]\n");
} }
void void

7
tests/core/readsave.test
View file

@ -1,6 +1,6 @@
#!/bin/sh #!/bin/sh
# -*- coding: utf-8 -*- # -*- coding: utf-8 -*-
# Copyright (C) 2009, 2010, 2012, 2014-2019 Laboratoire de # Copyright (C) 2009, 2010, 2012, 2014-2020 Laboratoire de
# Recherche et Développement de l'Epita (LRDE). # Recherche et Développement de l'Epita (LRDE).
# Copyright (C) 2003, 2004 Laboratoire d'Informatique de Paris 6 (LIP6), # Copyright (C) 2003, 2004 Laboratoire d'Informatique de Paris 6 (LIP6),
# département Systèmes Répartis Coopératifs (SRC), Université Pierre # département Systèmes Répartis Coopératifs (SRC), Université Pierre
@ -571,7 +571,7 @@ digraph "" {
node [shape="circle"] node [shape="circle"]
I [label="", style=invis, width=0] I [label="", style=invis, width=0]
0 [label="6", peripheries=2] 0 [label="6", peripheries=2]
u0 [label="...", shape=none, width=0, height=0] u0 [label="...", shape=none, width=0, height=0, tooltip="hidden successors"]
1 [label="0", peripheries=2] 1 [label="0", peripheries=2]
2 [label="1", peripheries=2] 2 [label="1", peripheries=2]
3 [label="2", peripheries=2] 3 [label="2", peripheries=2]
@ -1105,6 +1105,9 @@ digraph "a U b" {
EOF EOF
diff out expected diff out expected
# Issue #392.
test 2 = `genltl --rv-counter-carry-linear=7|ltl2tgba -d'<10' |grep -c hidden`
f="{{!a;!b}:{{c <-> d} && {e xor f} && {m | {l && {k | {j <-> {i xor {g && h}" f="{{!a;!b}:{{c <-> d} && {e xor f} && {m | {l && {k | {j <-> {i xor {g && h}"
f="$f}}}}} && {{n && o} | {!n && p}} && {q -> {r <-> s}}}:{[*0..1];t}}[]-> u" f="$f}}}}} && {{n && o} | {!n && p}} && {q -> {r <-> s}}}:{[*0..1];t}}[]-> u"
ltl2tgba -f "$f" --dot=bar > out.dot ltl2tgba -f "$f" --dot=bar > out.dot

1984
tests/python/highlighting.ipynb
View file

File diff suppressed because it is too large Load diff