1digraph state_automaton { 2 {node [shape = circle] "state_b"}; 3 {node [shape = plaintext, style=invis, label=""] "__init_state_a"}; 4 {node [shape = doublecircle] "state_a"}; 5 {node [shape = circle] "state_a"}; 6 "__init_state_a" -> "state_a"; 7 "state_a" [label = "state_a;clk < 1"]; 8 "state_a" -> "state_a" [ label = "event_2;reset(clk)" ]; 9 "state_a" -> "state_b" [ label = "event_1;wrong_constraint" ]; 10 "state_b" [label = "state_b"]; 11 "state_b" -> "state_a" [ label = "event_2" ]; 12 { rank = min ; 13 "__init_state_a"; 14 "state_a"; 15 } 16} 17