[PATCH v7 10/14] rv: Add tlob model DOT file

[wen . yang]

From: Wen Yang <wen.yang@xxxxxxxxx>

Add the Graphviz DOT specification of the tlob hybrid automaton to
tools/verification/models/.

The model has four states (stopped, running, waiting, sleeping) and six
events (start, stop, sleep, preempt, wakeup, switch_in).  A single clock
invariant, clk_elapsed < BUDGET_NS(), holds in running, waiting and
sleeping; stopped has no invariant, hence no timer.

wakeup is a self-loop on running and waiting: a task that is already
queued can still be the target of a traced wakeup, either by waking
itself or through ttwu_runnable() while preempted, and neither case ends
the budget window.  stopped takes every scheduler event as a self-loop,
so a task keeps going through the scheduler between windows.

Suggested-by: Gabriele Monaco <gmonaco@xxxxxxxxxx>
Signed-off-by: Wen Yang <wen.yang@xxxxxxxxx>
---
 tools/verification/models/tlob.dot | 27 +++++++++++++++++++++++++++
 1 file changed, 27 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..021a4d823548
--- /dev/null
+++ b/tools/verification/models/tlob.dot
@@ -0,0 +1,27 @@
+digraph state_automaton {
+	center = true;
+	size = "7,11";
+	{node [shape = plaintext, style=invis, label=""] "__init_stopped"};
+	{node [shape = plaintext] "running"};
+	{node [shape = plaintext] "waiting"};
+	{node [shape = plaintext] "sleeping"};
+	{node [shape = ellipse] "stopped"};
+	"__init_stopped" -> "stopped";
+	"running"  [label = "running\nclk_elapsed <= BUDGET_NS()"];
+	"waiting"  [label = "waiting\nclk_elapsed <= BUDGET_NS()"];
+	"sleeping" [label = "sleeping\nclk_elapsed <= BUDGET_NS()"];
+	"stopped"  [label = "stopped", color = green3];
+	"running"  -> "sleeping" [ label = "sleep" ];
+	"running"  -> "waiting"  [ label = "preempt" ];
+	"running"  -> "running"  [ label = "wakeup" ];
+	"waiting"  -> "running"  [ label = "switch_in" ];
+	"waiting"  -> "waiting"  [ label = "wakeup" ];
+	"sleeping" -> "waiting"  [ label = "wakeup" ];
+	"running"  -> "stopped"  [ label = "stop" ];
+	"stopped"  -> "running"  [ label = "start;reset(clk_elapsed)" ];
+	"stopped"  -> "stopped"  [ label = "preempt\nsleep\nswitch_in\nwakeup" ];
+	{ rank = min ;
+		"__init_stopped";
+		"stopped";
+	}
+}
-- 
2.25.1