xref: /linux/tools/verification/rvgen/tests/specs/test_invalid_ha.dot (revision 55ee4b931a7ffedc886175d265dd6e6d08fd4151)
1*655d4809SGabriele Monacodigraph state_automaton {
2*655d4809SGabriele Monaco	{node [shape = circle] "state_b"};
3*655d4809SGabriele Monaco	{node [shape = plaintext, style=invis, label=""] "__init_state_a"};
4*655d4809SGabriele Monaco	{node [shape = doublecircle] "state_a"};
5*655d4809SGabriele Monaco	{node [shape = circle] "state_a"};
6*655d4809SGabriele Monaco	"__init_state_a" -> "state_a";
7*655d4809SGabriele Monaco	"state_a" [label = "state_a;clk < 1"];
8*655d4809SGabriele Monaco	"state_a" -> "state_a" [ label = "event_2;reset(clk)" ];
9*655d4809SGabriele Monaco	"state_a" -> "state_b" [ label = "event_1;wrong_constraint" ];
10*655d4809SGabriele Monaco	"state_b" [label = "state_b"];
11*655d4809SGabriele Monaco	"state_b" -> "state_a" [ label = "event_2" ];
12*655d4809SGabriele Monaco	{ rank = min ;
13*655d4809SGabriele Monaco		"__init_state_a";
14*655d4809SGabriele Monaco		"state_a";
15*655d4809SGabriele Monaco	}
16*655d4809SGabriele Monaco}
17