From e17a617bc2bfce15767ab31daf0ef227adbd992b Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Fri, 15 Jul 2016 20:03:12 +0200 Subject: [PATCH] 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. --- NEWS | 7 ++ doc/org/hoa.org | 156 ++++++++++++++++++++++++++++++++++++--- spot/twaalgos/hoa.cc | 22 ++++++ tests/core/readsave.test | 8 ++ 4 files changed, 181 insertions(+), 12 deletions(-) diff --git a/NEWS b/NEWS index 40770e934..2f0b897bd 100644 --- a/NEWS +++ b/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 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_inherently_weak(), count_nondet_states() will update the corresponding properties of the automaton as a side-effect of diff --git a/doc/org/hoa.org b/doc/org/hoa.org index 71a3c2267..8c5691333 100644 --- a/doc/org/hoa.org +++ b/doc/org/hoa.org @@ -191,10 +191,6 @@ State: 2 [0] 2 {1} #+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 internally stores it using transition-based acceptance. However in that case the TωA will have a property flag indicating that it actually @@ -303,10 +299,6 @@ State: 2 --END-- #+END_SRC -#+BEGIN_SRC sh :results silent :exports results -rm sba.hoa -#+END_SRC - By default, the output uses either state-based acceptance, or transition-based acceptance. However there is no restriction in the format to prevents mixing the two: if you use =-Hm=, the decision of @@ -585,10 +577,6 @@ State: 2 [!1] 1 #+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 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 @@ -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 automaton is stutter-invariant, unambiguous, (inherently) weak, and 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 < 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=, taillabel="#3"] + 2 -> 2 [label=, 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 diff --git a/spot/twaalgos/hoa.cc b/spot/twaalgos/hoa.cc index 590b2bfc0..ee5d0fe28 100644 --- a/spot/twaalgos/hoa.cc +++ b/spot/twaalgos/hoa.cc @@ -493,6 +493,28 @@ namespace spot prop(" !inherently-weak"); 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 + >("highlight-states")) + { + os << "spot.highlight.states:"; + for (auto& p: *hstates) + os << ' ' << p.first << ' ' << p.second; + os << nl; + } + if (auto hedges = aut->get_named_prop + >("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 // fill a vector with all destinations in order. std::vector out; diff --git a/tests/core/readsave.test b/tests/core/readsave.test index 2e5cd032d..5cac65162 100755 --- a/tests/core/readsave.test +++ b/tests/core/readsave.test @@ -1014,4 +1014,12 @@ digraph G { EOF 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`