xref: /linux/tools/verification/models/sched/nrp.dot (revision 4ff261e725d7376c12e745fdbe8a33cd6dbd5a83)
1*e8440a88SGabriele Monacodigraph state_automaton {
2*e8440a88SGabriele Monaco	center = true;
3*e8440a88SGabriele Monaco	size = "7,11";
4*e8440a88SGabriele Monaco	{node [shape = doublecircle] "any_thread_running"};
5*e8440a88SGabriele Monaco	{node [shape = circle] "any_thread_running"};
6*e8440a88SGabriele Monaco	{node [shape = circle] "nested_preempt"};
7*e8440a88SGabriele Monaco	{node [shape = plaintext, style=invis, label=""] "__init_preempt_irq"};
8*e8440a88SGabriele Monaco	{node [shape = circle] "preempt_irq"};
9*e8440a88SGabriele Monaco	{node [shape = circle] "rescheduling"};
10*e8440a88SGabriele Monaco	"__init_preempt_irq" -> "preempt_irq";
11*e8440a88SGabriele Monaco	"any_thread_running" [label = "any_thread_running", color = green3];
12*e8440a88SGabriele Monaco	"any_thread_running" -> "any_thread_running" [ label = "schedule_entry\nirq_entry" ];
13*e8440a88SGabriele Monaco	"any_thread_running" -> "rescheduling" [ label = "sched_need_resched" ];
14*e8440a88SGabriele Monaco	"nested_preempt" [label = "nested_preempt"];
15*e8440a88SGabriele Monaco	"nested_preempt" -> "any_thread_running" [ label = "schedule_entry_preempt\nschedule_entry" ];
16*e8440a88SGabriele Monaco	"nested_preempt" -> "nested_preempt" [ label = "irq_entry" ];
17*e8440a88SGabriele Monaco	"nested_preempt" -> "preempt_irq" [ label = "sched_need_resched" ];
18*e8440a88SGabriele Monaco	"preempt_irq" [label = "preempt_irq"];
19*e8440a88SGabriele Monaco	"preempt_irq" -> "nested_preempt" [ label = "schedule_entry_preempt\nschedule_entry" ];
20*e8440a88SGabriele Monaco	"preempt_irq" -> "preempt_irq" [ label = "irq_entry\nsched_need_resched" ];
21*e8440a88SGabriele Monaco	"rescheduling" [label = "rescheduling"];
22*e8440a88SGabriele Monaco	"rescheduling" -> "any_thread_running" [ label = "schedule_entry_preempt\nschedule_entry" ];
23*e8440a88SGabriele Monaco	"rescheduling" -> "preempt_irq" [ label = "irq_entry" ];
24*e8440a88SGabriele Monaco	"rescheduling" -> "rescheduling" [ label = "sched_need_resched" ];
25*e8440a88SGabriele Monaco	{ rank = min ;
26*e8440a88SGabriele Monaco		"__init_preempt_irq";
27*e8440a88SGabriele Monaco		"preempt_irq";
28*e8440a88SGabriele Monaco	}
29*e8440a88SGabriele Monaco}
30