summaryrefslogtreecommitdiff
path: root/tools/verification/models/sched/snep.dot
diff options
context:
space:
mode:
Diffstat (limited to 'tools/verification/models/sched/snep.dot')
-rw-r--r--tools/verification/models/sched/snep.dot18
1 files changed, 18 insertions, 0 deletions
diff --git a/tools/verification/models/sched/snep.dot b/tools/verification/models/sched/snep.dot
new file mode 100644
index 000000000000..fe1300e93f21
--- /dev/null
+++ b/tools/verification/models/sched/snep.dot
@@ -0,0 +1,18 @@
+digraph state_automaton {
+ center = true;
+ size = "7,11";
+ {node [shape = plaintext, style=invis, label=""] "__init_non_scheduling_context"};
+ {node [shape = ellipse] "non_scheduling_context"};
+ {node [shape = plaintext] "non_scheduling_context"};
+ {node [shape = plaintext] "scheduling_contex"};
+ "__init_non_scheduling_context" -> "non_scheduling_context";
+ "non_scheduling_context" [label = "non_scheduling_context", color = green3];
+ "non_scheduling_context" -> "non_scheduling_context" [ label = "preempt_disable\npreempt_enable" ];
+ "non_scheduling_context" -> "scheduling_contex" [ label = "schedule_entry" ];
+ "scheduling_contex" [label = "scheduling_contex"];
+ "scheduling_contex" -> "non_scheduling_context" [ label = "schedule_exit" ];
+ { rank = min ;
+ "__init_non_scheduling_context";
+ "non_scheduling_context";
+ }
+}