From: Wen Yang <[email protected]> Add the Graphviz DOT specification of the tlob hybrid automaton to tools/verification/models/. The model has three states (running, waiting, sleeping), five transitions (switch_in, preempt, wakeup, sleep), and a single clock invariant clk_elapsed < BUDGET_NS() active in all states.
Suggested-by: Gabriele Monaco <[email protected]> Signed-off-by: Wen Yang <[email protected]> --- tools/verification/models/tlob.dot | 25 +++++++++++++++++++++++++ 1 file changed, 25 insertions(+) create mode 100644 tools/verification/models/tlob.dot diff --git a/tools/verification/models/tlob.dot b/tools/verification/models/tlob.dot new file mode 100644 index 000000000000..7f6f09c3d7cf --- /dev/null +++ b/tools/verification/models/tlob.dot @@ -0,0 +1,25 @@ +digraph state_automaton { + center = true; + size = "7,11"; + {node [shape = plaintext, style=invis, label=""] "__init_stopped"}; + {node [shape = ellipse] "running"}; + {node [shape = plaintext] "running"}; + {node [shape = plaintext] "waiting"}; + {node [shape = plaintext] "sleeping"}; + {node [shape = plaintext] "stopped"}; + "__init_stopped" -> "stopped"; + "running" [label = "running\nclk_elapsed < BUDGET_NS()", color = green3]; + "waiting" [label = "waiting\nclk_elapsed < BUDGET_NS()"]; + "sleeping" [label = "sleeping\nclk_elapsed < BUDGET_NS()"]; + "stopped" [label = "stopped"]; + "running" -> "sleeping" [ label = "sleep" ]; + "running" -> "waiting" [ label = "preempt" ]; + "waiting" -> "running" [ label = "switch_in" ]; + "sleeping" -> "waiting" [ label = "wakeup" ]; + "running" -> "stopped" [ label = "stop" ]; + "stopped" -> "running" [ label = "start;reset(clk_elapsed)" ]; + { rank = min ; + "__init_stopped"; + "stopped"; + } +} -- 2.25.1
