hoa: output highlighted states and edges in v1.1
* spot/twaalgos/hoa.cc: Here. * doc/org/hoa.org, NEWS: Document that. * tests/core/readsave.test: Test it.
This commit is contained in:
Alexandre Duret-Lutz
parent
bbc3afe1cf
commit
e17a617bc2
4 changed files with 181 additions and 12 deletions
7
NEWS
7
NEWS
|
|
@ -54,6 +54,13 @@ New in spot 2.0.3a (not yet released)
|
||||||
is still the default, but we plan to default to version 1.1 in the
|
is still the default, but we plan to default to version 1.1 in the
|
||||||
future.
|
future.
|
||||||
|
|
||||||
|
* The "highlight-states" and "highlight-edges" named properties,
|
||||||
|
which were introduced in 1.99.8, will now be output using
|
||||||
|
"spot.highlight.edges:" and "spot.highlight.states:" headers if
|
||||||
|
version 1.1 of the HOA format is selected. The automaton parser
|
||||||
|
was secretly able of reading that since 1.99.8, but that is now
|
||||||
|
documented at https://spot.lrde.epita.fr/hoa.html#extensions
|
||||||
|
|
||||||
* is_deterministic(), is_terminal(), is_weak(), and
|
* is_deterministic(), is_terminal(), is_weak(), and
|
||||||
is_inherently_weak(), count_nondet_states() will update the
|
is_inherently_weak(), count_nondet_states() will update the
|
||||||
corresponding properties of the automaton as a side-effect of
|
corresponding properties of the automaton as a side-effect of
|
||||||
|
|
|
||||||
156
doc/org/hoa.org
156
doc/org/hoa.org
|
|
@ -191,10 +191,6 @@ State: 2
|
||||||
[0] 2 {1}
|
[0] 2 {1}
|
||||||
#+END_SRC
|
#+END_SRC
|
||||||
|
|
||||||
#+BEGIN_SRC sh :results silent :exports results
|
|
||||||
rm -f stvstracc.hoa
|
|
||||||
#+END_SRC
|
|
||||||
|
|
||||||
Even if an input HOA file uses only state-based acceptance, Spot
|
Even if an input HOA file uses only state-based acceptance, Spot
|
||||||
internally stores it using transition-based acceptance. However in
|
internally stores it using transition-based acceptance. However in
|
||||||
that case the TωA will have a property flag indicating that it actually
|
that case the TωA will have a property flag indicating that it actually
|
||||||
|
|
@ -303,10 +299,6 @@ State: 2
|
||||||
--END--
|
--END--
|
||||||
#+END_SRC
|
#+END_SRC
|
||||||
|
|
||||||
#+BEGIN_SRC sh :results silent :exports results
|
|
||||||
rm sba.hoa
|
|
||||||
#+END_SRC
|
|
||||||
|
|
||||||
By default, the output uses either state-based acceptance, or
|
By default, the output uses either state-based acceptance, or
|
||||||
transition-based acceptance. However there is no restriction in the
|
transition-based acceptance. However there is no restriction in the
|
||||||
format to prevents mixing the two: if you use =-Hm=, the decision of
|
format to prevents mixing the two: if you use =-Hm=, the decision of
|
||||||
|
|
@ -585,10 +577,6 @@ State: 2
|
||||||
[!1] 1
|
[!1] 1
|
||||||
#+END_SRC
|
#+END_SRC
|
||||||
|
|
||||||
#+BEGIN_SRC sh :results silent :exports results
|
|
||||||
rm -f stvstrlab.hoa
|
|
||||||
#+END_SRC
|
|
||||||
|
|
||||||
The HOA printer has an option to output automata using state-based
|
The HOA printer has an option to output automata using state-based
|
||||||
labels whenever that is possible. The option is named =k= (i.e., use
|
labels whenever that is possible. The option is named =k= (i.e., use
|
||||||
=-Hk= with command-line tools) because it is useful when the HOA file
|
=-Hk= with command-line tools) because it is useful when the HOA file
|
||||||
|
|
@ -969,3 +957,147 @@ Command-line tools with a HOA output all have a =--check= option that
|
||||||
can be used to request additional checks such as testing whether the
|
can be used to request additional checks such as testing whether the
|
||||||
automaton is stutter-invariant, unambiguous, (inherently) weak, and
|
automaton is stutter-invariant, unambiguous, (inherently) weak, and
|
||||||
terminal.
|
terminal.
|
||||||
|
* Extensions
|
||||||
|
:PROPERTIES:
|
||||||
|
:CUSTOM_ID: extensions
|
||||||
|
:END:
|
||||||
|
|
||||||
|
Spot supports two additional headers that are not part of the standard
|
||||||
|
HOA format. These are =spot.highlight.states= and
|
||||||
|
=spot.highlight.edges=. These are used to decorate states and edges
|
||||||
|
with colors.
|
||||||
|
|
||||||
|
#+NAME: decorate
|
||||||
|
#+BEGIN_SRC sh :results verbatim :exports code
|
||||||
|
cat >decorate.hoa <<EOF
|
||||||
|
HOA: v1.1
|
||||||
|
States: 3
|
||||||
|
Start: 1
|
||||||
|
AP: 2 "a" "b"
|
||||||
|
Acceptance: 0 t
|
||||||
|
spot.highlight.states: 1 0 2 3
|
||||||
|
spot.highlight.edges: 1 1 2 2
|
||||||
|
--BODY--
|
||||||
|
State: 0
|
||||||
|
[t] 0 /* edge #1 */
|
||||||
|
State: 1
|
||||||
|
[t] 2 /* edge #2 */
|
||||||
|
State: 2
|
||||||
|
[1] 0 /* edge #3 */
|
||||||
|
[0&!1] 2 /* edge #4 */
|
||||||
|
--END--
|
||||||
|
EOF
|
||||||
|
|
||||||
|
autfilt decorate.hoa -d'.#'
|
||||||
|
#+END_SRC
|
||||||
|
|
||||||
|
#+RESULTS: decorate
|
||||||
|
#+begin_example
|
||||||
|
digraph G {
|
||||||
|
rankdir=LR
|
||||||
|
node [shape="circle"]
|
||||||
|
node [style="filled", fillcolor="#ffffa0"]
|
||||||
|
fontname="Lato"
|
||||||
|
node [fontname="Lato"]
|
||||||
|
edge [fontname="Lato"]
|
||||||
|
edge[arrowhead=vee, arrowsize=.7]
|
||||||
|
I [label="", style=invis, width=0]
|
||||||
|
I -> 1
|
||||||
|
0 [label=<0>]
|
||||||
|
0 -> 0 [label=<1>, taillabel="#1", style=bold, color="#F17CB0"]
|
||||||
|
1 [label=<1>, style="bold,filled", color="#5DA5DA"]
|
||||||
|
1 -> 2 [label=<1>, taillabel="#2", style=bold, color="#FAA43A"]
|
||||||
|
2 [label=<2>, style="bold,filled", color="#B276B2"]
|
||||||
|
2 -> 0 [label=<b>, taillabel="#3"]
|
||||||
|
2 -> 2 [label=<a & !b>, taillabel="#4"]
|
||||||
|
}
|
||||||
|
#+end_example
|
||||||
|
|
||||||
|
#+BEGIN_SRC dot :file decorate.png :cmdline -Tpng :var txt=decorate :exports results
|
||||||
|
$txt
|
||||||
|
#+END_SRC
|
||||||
|
|
||||||
|
#+RESULTS:
|
||||||
|
[[file:decorate.png]]
|
||||||
|
|
||||||
|
|
||||||
|
On the above example, we call =autfilt= with option =-d#= to display
|
||||||
|
edges numbers, which helps identifying the edges to highlight. The
|
||||||
|
headers ~spot.highlight.states:~ and ~spot.highlight.edges:~ gives a
|
||||||
|
list of alternating state/edges numbers and color numbers.
|
||||||
|
|
||||||
|
So in the above file,
|
||||||
|
#+BEGIN_SRC sh :results verbatim :exports results :wrap SRC hoa
|
||||||
|
grep spot.highlight decorate.hoa
|
||||||
|
#+END_SRC
|
||||||
|
#+RESULTS:
|
||||||
|
#+BEGIN_SRC hoa
|
||||||
|
spot.highlight.states: 1 0 2 3
|
||||||
|
spot.highlight.edges: 1 1 2 2
|
||||||
|
#+END_SRC
|
||||||
|
specifies that states =#1= should have color =0=, state =#2= should have
|
||||||
|
color =3=, edge =#1= should have color =1=, and edge =#2= should have
|
||||||
|
color =2=.
|
||||||
|
|
||||||
|
State numbers obviously correspond to the state numbers used in the
|
||||||
|
HOA file, and are 0-based. Edge numbers are 1-based (because that is
|
||||||
|
how they are actually stored in Spot), and numbered in the order they
|
||||||
|
appear in the HOA file.
|
||||||
|
|
||||||
|
The color palette is currently the same that is used for coloring
|
||||||
|
acceptance sets. This might change in the future.
|
||||||
|
|
||||||
|
The automaton parser will not complain if these headers are used in
|
||||||
|
the =HOA: v1= file, even if =v1= disallows dots in header names.
|
||||||
|
However the automaton printer is more rigorous and will only output
|
||||||
|
these lines when version 1.1 is selected.
|
||||||
|
|
||||||
|
Compare:
|
||||||
|
|
||||||
|
#+BEGIN_SRC sh :results verbatim :exports both :wrap SRC hoa
|
||||||
|
autfilt -H1 decorate.hoa; echo
|
||||||
|
autfilt -H1.1 decorate.hoa
|
||||||
|
#+END_SRC
|
||||||
|
#+RESULTS:
|
||||||
|
#+BEGIN_SRC hoa
|
||||||
|
HOA: v1
|
||||||
|
States: 3
|
||||||
|
Start: 1
|
||||||
|
AP: 2 "a" "b"
|
||||||
|
acc-name: all
|
||||||
|
Acceptance: 0 t
|
||||||
|
properties: trans-labels explicit-labels state-acc deterministic
|
||||||
|
--BODY--
|
||||||
|
State: 0
|
||||||
|
[t] 0
|
||||||
|
State: 1
|
||||||
|
[t] 2
|
||||||
|
State: 2
|
||||||
|
[1] 0
|
||||||
|
[0&!1] 2
|
||||||
|
--END--
|
||||||
|
|
||||||
|
HOA: v1.1
|
||||||
|
States: 3
|
||||||
|
Start: 1
|
||||||
|
AP: 2 "a" "b"
|
||||||
|
acc-name: all
|
||||||
|
Acceptance: 0 t
|
||||||
|
properties: trans-labels explicit-labels state-acc !complete
|
||||||
|
properties: deterministic
|
||||||
|
spot.highlight.states: 1 0 2 3
|
||||||
|
spot.highlight.edges: 1 1 2 2
|
||||||
|
--BODY--
|
||||||
|
State: 0
|
||||||
|
[t] 0
|
||||||
|
State: 1
|
||||||
|
[t] 2
|
||||||
|
State: 2
|
||||||
|
[1] 0
|
||||||
|
[0&!1] 2
|
||||||
|
--END--
|
||||||
|
#+END_SRC
|
||||||
|
|
||||||
|
#+BEGIN_SRC sh :results silent :exports results
|
||||||
|
rm -f stvstracc.hoa sba.hoa stvstrlab.hoa decorate.hoa
|
||||||
|
#+END_SRC
|
||||||
|
|
|
||||||
|
|
@ -493,6 +493,28 @@ namespace spot
|
||||||
prop(" !inherently-weak");
|
prop(" !inherently-weak");
|
||||||
os << nl;
|
os << nl;
|
||||||
|
|
||||||
|
// highlighted states and edges are only output in the 1.1 format,
|
||||||
|
// because we use a dot in the header name.
|
||||||
|
if (v1_1)
|
||||||
|
{
|
||||||
|
if (auto hstates = aut->get_named_prop
|
||||||
|
<std::map<unsigned, unsigned>>("highlight-states"))
|
||||||
|
{
|
||||||
|
os << "spot.highlight.states:";
|
||||||
|
for (auto& p: *hstates)
|
||||||
|
os << ' ' << p.first << ' ' << p.second;
|
||||||
|
os << nl;
|
||||||
|
}
|
||||||
|
if (auto hedges = aut->get_named_prop
|
||||||
|
<std::map<unsigned, unsigned>>("highlight-edges"))
|
||||||
|
{
|
||||||
|
os << "spot.highlight.edges:";
|
||||||
|
for (auto& p: *hedges)
|
||||||
|
os << ' ' << p.first << ' ' << p.second;
|
||||||
|
os << nl;
|
||||||
|
}
|
||||||
|
}
|
||||||
|
|
||||||
// If we want to output implicit labels, we have to
|
// If we want to output implicit labels, we have to
|
||||||
// fill a vector with all destinations in order.
|
// fill a vector with all destinations in order.
|
||||||
std::vector<unsigned> out;
|
std::vector<unsigned> out;
|
||||||
|
|
|
||||||
|
|
@ -1014,4 +1014,12 @@ digraph G {
|
||||||
EOF
|
EOF
|
||||||
diff output9 expected9
|
diff output9 expected9
|
||||||
|
|
||||||
|
# spot.hightlight.edges and spot.hightlight.states are not valid HOA
|
||||||
|
# v1 output, so they should only but output for HOA 1.1
|
||||||
|
autfilt input9 -H1 | autfilt -H1 | grep highlight && exit 1
|
||||||
|
autfilt input9 -H1 | autfilt -H1.1 | grep highlight && exit 1
|
||||||
|
autfilt -H1.1 input9 | autfilt -H1.1 | grep highlight
|
||||||
|
autfilt -H1.1 input9 | autfilt -d > output9b
|
||||||
|
diff output9 output9b
|
||||||
|
|
||||||
test 2 = `ltl2tgba 'GFa' 'a U b' 'a U b U c'| autfilt --ap=2..3 --count`
|
test 2 = `ltl2tgba 'GFa' 'a U b' 'a U b U c'| autfilt --ap=2..3 --count`
|
||||||
|
|
|
||||||
Loading…
Add table
Add a link
Reference in a new issue