xref: /linux/tools/verification/rvgen/tests/specs/test_ha.dot (revision 55ee4b931a7ffedc886175d265dd6e6d08fd4151)
1digraph state_automaton {
2	center = true;
3	size = "7,11";
4	{node [shape = circle] "S1"};
5	{node [shape = plaintext, style=invis, label=""] "__init_S0"};
6	{node [shape = doublecircle] "S0"};
7	{node [shape = circle] "S0"};
8	{node [shape = circle] "S2"};
9	{node [shape = circle] "S3"};
10	"__init_S0" -> "S0";
11	"S0" [label = "S0\nclk < bar_ns()", color = green3];
12	"S1" [label = "S1"];
13	"S2" [label = "S2\nclk < BAR_NS()"];
14	"S3" [label = "S3"];
15	"S1" -> "S0" [ label = "event0;reset(clk)" ];
16	"S0" -> "S1" [ label = "event1;reset(clk)" ];
17	"S0" -> "S0" [ label = "event0;reset(clk)" ];
18	"S1" -> "S2" [ label = "event2;env1 == 0;reset(clk)" ];
19	"S2" -> "S3" [ label = "event2" ];
20	"S2" -> "S2" [ label = "event1;clk < foo_ns" ];
21	"S3" -> "S0" [ label = "event0;clk < FOO_NS && env2 == 0" ];
22	"S3" -> "S1" [ label = "event1;clk < 5us && env1 == 1;reset(clk)" ];
23	{ rank = min ;
24		"__init_S0";
25		"S0";
26	}
27}
28