xref: /linux/tools/verification/models/sched/sssw.dot (revision 4ff261e725d7376c12e745fdbe8a33cd6dbd5a83)
1*e8440a88SGabriele Monacodigraph state_automaton {
2*e8440a88SGabriele Monaco	center = true;
3*e8440a88SGabriele Monaco	size = "7,11";
4*e8440a88SGabriele Monaco	{node [shape = plaintext, style=invis, label=""] "__init_runnable"};
5*e8440a88SGabriele Monaco	{node [shape = doublecircle] "runnable"};
6*e8440a88SGabriele Monaco	{node [shape = circle] "runnable"};
7*e8440a88SGabriele Monaco	{node [shape = circle] "signal_wakeup"};
8*e8440a88SGabriele Monaco	{node [shape = circle] "sleepable"};
9*e8440a88SGabriele Monaco	{node [shape = circle] "sleeping"};
10*e8440a88SGabriele Monaco	"__init_runnable" -> "runnable";
11*e8440a88SGabriele Monaco	"runnable" [label = "runnable", color = green3];
12*e8440a88SGabriele Monaco	"runnable" -> "runnable" [ label = "sched_set_state_runnable\nsched_wakeup\nsched_switch_in\nsched_switch_yield\nsched_switch_preempt\nsignal_deliver" ];
13*e8440a88SGabriele Monaco	"runnable" -> "sleepable" [ label = "sched_set_state_sleepable" ];
14*e8440a88SGabriele Monaco	"runnable" -> "sleeping" [ label = "sched_switch_blocking" ];
15*e8440a88SGabriele Monaco	"signal_wakeup" [label = "signal_wakeup"];
16*e8440a88SGabriele Monaco	"signal_wakeup" -> "runnable" [ label = "signal_deliver" ];
17*e8440a88SGabriele Monaco	"signal_wakeup" -> "signal_wakeup" [ label = "sched_switch_in\nsched_switch_preempt\nsched_switch_yield\nsched_wakeup" ];
18*e8440a88SGabriele Monaco	"signal_wakeup" -> "sleepable" [ label = "sched_set_state_sleepable" ];
19*e8440a88SGabriele Monaco	"sleepable" [label = "sleepable"];
20*e8440a88SGabriele Monaco	"sleepable" -> "runnable" [ label = "sched_set_state_runnable\nsched_wakeup" ];
21*e8440a88SGabriele Monaco	"sleepable" -> "signal_wakeup" [ label = "sched_switch_yield" ];
22*e8440a88SGabriele Monaco	"sleepable" -> "sleepable" [ label = "sched_set_state_sleepable\nsched_switch_in\nsched_switch_preempt\nsignal_deliver" ];
23*e8440a88SGabriele Monaco	"sleepable" -> "sleeping" [ label = "sched_switch_suspend\nsched_switch_blocking" ];
24*e8440a88SGabriele Monaco	"sleeping" [label = "sleeping"];
25*e8440a88SGabriele Monaco	"sleeping" -> "runnable" [ label = "sched_wakeup" ];
26*e8440a88SGabriele Monaco	{ rank = min ;
27*e8440a88SGabriele Monaco		"__init_runnable";
28*e8440a88SGabriele Monaco		"runnable";
29*e8440a88SGabriele Monaco	}
30*e8440a88SGabriele Monaco}
31