Commit 745fda1a authored by Alexandre Duret-Lutz's avatar Alexandre Duret-Lutz

print_hoa: add option "k"

* src/twaalgos/hoa.cc, src/twaalgos/hoa.hh: Implement it.
* NEWS, doc/org/hoa.org, src/bin/common_aoutput.cc: Document it.
* src/tests/readsave.test: Test it.
parent a825fa91
......@@ -48,6 +48,10 @@ New in spot 1.99.5a (not yet released)
automata already tagged as "deterministic", and "inherently-weak"
or "weak" even for automata tagged "weak" or "terminal".
* The HOA printer has a new option "k" (use "-Hk" from the command
line) to output automata using state labels whenever possible.
This is useful to print Kripke structures.
* The dot output will display pair of states when displaying an
automaton built as an explicit product. This works in IPython
with spot.product() or spot.product_or() and in the shell with
......
......@@ -510,6 +510,79 @@ Acceptance: 6 (Fin(0)|Fin(1)) | (Fin(2) & Fin(3) & (Inf(4)&Inf(5)))
Here =Fin(0)|Fin(1)= is actually a single internal term =Fin({0,1})=,
and likewise for =Inf(4)&Inf(5)=.
** State-based vs. transition-based labels
State labels are handled in the same way as state-based acceptance:
Spot store labels on transitions internally, so if an input automaton
has state labels, those are pushed to all outgoing transitions.
For instance an automaton declared in some HOA file with this body:
#+BEGIN_SRC sh :results silent :exports results
cat >stvstrlab.hoa <<EOF
HOA: v1
States: 3
Start: 0
AP: 2 "p0" "p1"
Acceptance: 1 Inf(1)
--BODY--
State: [0&1] 0
0 1 2
State: [!0&1] 1 {0}
0 1
State: [!1] 2
2 1
--END--
EOF
#+END_SRC
#+RESULTS:
#+BEGIN_SRC sh :results verbatim :exports results :wrap SRC hoa
sed -n '/--BODY/,/--END/p' stvstrlab.hoa | grep -v -- --
#+END_SRC
#+RESULTS:
#+BEGIN_SRC hoa
State: [0&1] 0
0 1 2
State: [!0&1] 1 {0}
0 1
State: [!1] 2
2 1
#+END_SRC
will always be stored as an automaton with the following transition
structure
#+BEGIN_SRC sh :results verbatim :exports results :wrap SRC hoa
autfilt -Ht stvstrlab.hoa | sed -n '/--BODY/,/--END/p' | grep -v -- --
#+END_SRC
#+RESULTS:
#+BEGIN_SRC hoa
State: 0
[0&1] 0
[0&1] 1
[0&1] 2
State: 1
[!0&1] 0 {0}
[!0&1] 1 {0}
State: 2
[!1] 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
is used to describe a Kripke structure.
** Property bits
The =HOA= format supports a number of optional =property:= tokens.
......@@ -577,24 +650,24 @@ particular:
to detect deterministic automata that have been output by algorithms
that do not try to output deterministic automata.
| property | parser | stored | printer | notes |
|---------------------+---------+--------+---------------------------------------------+--------------------------------------------------------|
| =state-labels= | checked | no | never | state labels are always converted to transition labels |
| =trans-labels= | checked | no | always, unless =-Hi= | |
| =implicit-labels= | checked | no | if =-Hi= | =-Hi= only works for deterministic automata |
| =explicit-labels= | checked | no | always, unless =-Hi= | |
| =state-acc= | checked | yes | re-checked, unless =-Ht= or =-Hm= | |
| =trans-acc= | checked | no | if not =state-acc= and not =-Hm= | |
| =no-univ-branch= | ignored | no | only if =-Hv= | |
| =deterministic= | checked | yes | re-checked | |
| =complete= | checked | no | re-checked | |
| =unambiguous= | trusted | yes | as stored if (=-Hv= or not =deterministic=) | can be re-checked with =--check=unambiguous= |
| =stutter-invariant= | trusted | yes | as stored | can be re-checked with =--check=stuttering= |
| =stutter-sensitive= | trusted | yes | as stored | can be re-checked with =--check=stuttering= |
| =terminal= | trusted | yes | as stored | can be re-checked with =--check=strength= |
| =weak= | trusted | yes | as stored if (=-Hv= or not =terminal=) | can be re-checked with =--check=strength= |
| =inherently-weak= | trusted | yes | as stored if (=-Hv= or not =weak=) | |
| =colored= | ignored | no | checked | |
| property | parser | stored | printer | notes |
|---------------------+---------+--------+---------------------------------------------+------------------------------------------------------------------|
| =state-labels= | checked | no | re-rechecked if =-Hk= | state labels are converted to transition labels when reading TωA |
| =trans-labels= | checked | no | always, unless =-Hi= or =-Hk= | |
| =implicit-labels= | checked | no | if =-Hi= | =-Hi= only works for deterministic automata |
| =explicit-labels= | checked | no | always, unless =-Hi= | |
| =state-acc= | checked | yes | re-checked, unless =-Ht= or =-Hm= | |
| =trans-acc= | checked | no | if not =state-acc= and not =-Hm= | |
| =no-univ-branch= | ignored | no | only if =-Hv= | |
| =deterministic= | checked | yes | re-checked | |
| =complete= | checked | no | re-checked | |
| =unambiguous= | trusted | yes | as stored if (=-Hv= or not =deterministic=) | can be re-checked with =--check=unambiguous= |
| =stutter-invariant= | trusted | yes | as stored | can be re-checked with =--check=stuttering= |
| =stutter-sensitive= | trusted | yes | as stored | can be re-checked with =--check=stuttering= |
| =terminal= | trusted | yes | as stored | can be re-checked with =--check=strength= |
| =weak= | trusted | yes | as stored if (=-Hv= or not =terminal=) | can be re-checked with =--check=strength= |
| =inherently-weak= | trusted | yes | as stored if (=-Hv= or not =weak=) | |
| =colored= | ignored | no | checked | |
** Named properties
......
......@@ -104,6 +104,7 @@ static const argp_option options[] =
"(s) prefer state-based acceptance when possible [default], "
"(t) force transition-based acceptance, "
"(m) mix state and transition-based acceptance, "
"(k) use state labels when possible, "
"(l) single-line output, "
"(v) verbose properties", 0 },
{ "lbtt", OPT_LBTT, "t", OPTION_ARG_OPTIONAL,
......
......@@ -633,7 +633,27 @@ EOF
diff output2 expect2
$autfilt -Hk expect2 >output2b
cat >expect2b <<EOF
HOA: v1
States: 3
Start: 0
AP: 2 "p0" "p1"
acc-name: all
Acceptance: 0 t
properties: state-labels explicit-labels state-acc deterministic
--BODY--
State: [!0&!1] 0
1
State: [0&1] 1
2
State: [!0&!1] 2
0
--END--
EOF
diff output2b expect2b
# Check the difference between --remove-unreach and --remove-dead
cat >input <<EOF
......@@ -700,8 +720,8 @@ EOF
diff output3 expect3
$autfilt -Hk input 2>stderr && exit 1
grep 'print_hoa.*k' stderr
$autfilt -Hz input 2>stderr && exit 1
grep 'print_hoa.*z' stderr
cat >input4 <<EOF
HOA: v1
......@@ -773,3 +793,47 @@ State: 2 {0}
--END--
EOF
diff output5 expect5
cat >input6 <<EOF
HOA: v1
States: 3
Start: 1
AP: 2 "a" "b"
acc-name: Buchi
Acceptance: 1 Inf(0)
properties: no-univ-branch trans-labels explicit-labels state-acc
--BODY--
State: 0
[1] 2
[1] 1
[1] 1
State: 1
[0] 0
[0] 1
State: 2 {0}
[0] 2
[0] 0
[0] 1
--END--
EOF
run 0 $autfilt -Hk input6 >output6
cat >expect6 <<EOF
HOA: v1
States: 3
Start: 1
AP: 2 "a" "b"
acc-name: Buchi
Acceptance: 1 Inf(0)
properties: state-labels explicit-labels state-acc
--BODY--
State: [1] 0
2 1 1
State: [0] 1
0 1
State: [0] 2 {0}
2 0 1
--END--
EOF
diff output6 expect6
......@@ -52,6 +52,7 @@ namespace spot
bool is_deterministic;
bool is_colored;
bool use_implicit_labels;
bool use_state_labels = true;
bdd all_ap;
// Label support: the set of all conditions occurring in the
......@@ -59,10 +60,12 @@ namespace spot
typedef std::map<bdd, std::string, bdd_less_than> sup_map;
sup_map sup;
metadata(const const_twa_graph_ptr& aut, bool implicit)
metadata(const const_twa_graph_ptr& aut, bool implicit,
bool state_labels)
{
check_det_and_comp(aut);
use_implicit_labels = implicit && is_deterministic && is_complete;
use_state_labels &= state_labels;
number_all_ap();
}
......@@ -106,8 +109,13 @@ namespace spot
bool notfirst = false;
acc_cond::mark_t prev = 0U;
bool has_succ = false;
bdd lastcond = bddfalse;
for (auto& t: aut->out(src))
{
if (has_succ)
use_state_labels &= lastcond == t.cond;
else
lastcond = t.cond;
if (complete)
sum |= t.cond;
if (deterministic)
......@@ -244,6 +252,7 @@ namespace spot
hoa_acceptance acceptance = Hoa_Acceptance_States;
bool implicit_labels = false;
bool verbose = false;
bool state_labels = false;
if (opt)
while (*opt)
......@@ -253,6 +262,9 @@ namespace spot
case 'i':
implicit_labels = true;
break;
case 'k':
state_labels = true;
break;
case 'l':
newline = false;
break;
......@@ -278,7 +290,7 @@ namespace spot
// automata, so it has to be done first.
unsigned init = aut->get_init_state_number();
metadata md(aut, implicit_labels);
metadata md(aut, implicit_labels, state_labels);
if (acceptance == Hoa_Acceptance_States && !md.has_state_acc)
acceptance = Hoa_Acceptance_Transitions;
......@@ -399,8 +411,11 @@ namespace spot
if (verbose)
prop(" no-univ-branch");
implicit_labels = md.use_implicit_labels;
state_labels = md.use_state_labels;
if (implicit_labels)
prop(" implicit-labels");
else if (state_labels)
prop(" state-labels explicit-labels");
else
prop(" trans-labels explicit-labels");
if (acceptance == Hoa_Acceptance_States)
......@@ -453,7 +468,20 @@ namespace spot
this_acc = (md.common_acc[i] ?
Hoa_Acceptance_States : Hoa_Acceptance_Transitions);
os << "State: " << i;
os << "State: ";
if (state_labels)
{
bool output = false;
for (auto& t: aut->out(i))
{
os << '[' << md.sup[t.cond] << "] ";
output = true;
break;
}
if (!output)
os << "[f] ";
}
os << i;
if (sn && i < sn->size() && !(*sn)[i].empty())
os << " \"" << (*sn)[i] << '"';
if (this_acc == Hoa_Acceptance_States)
......@@ -468,8 +496,9 @@ namespace spot
}
os << nl;
if (!implicit_labels)
if (!implicit_labels && !state_labels)
{
for (auto& t: aut->out(i))
{
os << '[' << md.sup[t.cond] << "] " << t.dst;
......@@ -478,6 +507,24 @@ namespace spot
os << nl;
}
}
else if (state_labels)
{
unsigned n = 0;
for (auto& t: aut->out(i))
{
os << t.dst;
if (this_acc == Hoa_Acceptance_Transitions)
{
md.emit_acc(os, aut, t.acc);
os << nl;
}
else
{
++n;
os << (((n & 15) && t.next_succ) ? ' ' : nl);
}
}
}
else
{
for (auto& t: aut->out(i))
......
......@@ -32,7 +32,8 @@ namespace spot
/// \param g The automaton to output.
/// \param opt a set of characters each corresponding to a possible
/// option: (i) implicit labels for complete and
/// deterministic automata, (s) state-based acceptance, (t)
/// deterministic automata, (k) state labels when possible,
/// (s) state-based acceptance when possible, (t)
/// transition-based acceptance, (m) mixed acceptance, (l)
/// single-line output, (v) verbose properties.
SPOT_API std::ostream&
......
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment