printer of kripke_graph
Our printer_dot()
really support only twa_graph
automata, but is able to handle any subclass of twa
by first copying in into a twa_graph
and naming states are they are discovered.
For instance, note how states s0, s1, s2 (which are stored at index 0, 1, 2) get renumbered to 0, 2, 1 in the following output, as a consequence of the copy from kripke_graph to twa_graph.
import spot
spot.setup()
from buddy import bddtrue
k = spot.make_kripke_graph(spot._bdd_dict)
s0 = k.new_state(bddtrue);
s1 = k.new_state(bddtrue);
s2 = k.new_state(bddtrue);
k.set_state_names(["s0", "s1", "s2"])
k.set_init_state(s0);
k.new_edge(s0, s2);
k.new_edge(s2, s1);
k.new_edge(s1, s0);
print(k.to_str('dot'))
digraph "" {
rankdir=LR
label=<t<br/>[all]>
labelloc="t"
node [shape="box",style="rounded",width="0.5"]
node [style="filled,rounded", fillcolor="#ffffaa"]
fontname="Lato"
node [fontname="Lato"]
edge [fontname="Lato"]
size="10.13,5" edge[arrowhead=vee, arrowsize=.7]
I [label="", style=invis, width=0]
I -> 0
0 [label=<s0<br/>1>]
0 -> 1 [label=<>]
1 [label=<s2<br/>1>]
1 -> 2 [label=<>]
2 [label=<s1<br/>1>]
2 -> 0 [label=<>]
}
This was unexpected by Edmond Irani Liu (private email from May 9). In the interest of least surprize, maybe we could try preserve the order of states when creating a twa_graph
from a kripke_graph
.