diff options
Diffstat (limited to 'tools/verification/models/sched/tss.dot')
| -rw-r--r-- | tools/verification/models/sched/tss.dot | 18 |
1 files changed, 18 insertions, 0 deletions
diff --git a/tools/verification/models/sched/tss.dot b/tools/verification/models/sched/tss.dot new file mode 100644 index 000000000000..7dfa1d9121bb --- /dev/null +++ b/tools/verification/models/sched/tss.dot @@ -0,0 +1,18 @@ +digraph state_automaton { + center = true; + size = "7,11"; + {node [shape = plaintext] "sched"}; + {node [shape = plaintext, style=invis, label=""] "__init_thread"}; + {node [shape = ellipse] "thread"}; + {node [shape = plaintext] "thread"}; + "__init_thread" -> "thread"; + "sched" [label = "sched"]; + "sched" -> "sched" [ label = "sched_switch" ]; + "sched" -> "thread" [ label = "schedule_exit" ]; + "thread" [label = "thread", color = green3]; + "thread" -> "sched" [ label = "schedule_entry" ]; + { rank = min ; + "__init_thread"; + "thread"; + } +} |