[RFC PATCH 1/4] rv/tlob: Add tlob model DOT file

[wen.yang@linux.dev]

From: Wen Yang <wen.yang@linux.dev>

Add the Graphviz DOT specification for the tlob (task latency over
budget) deterministic automaton.

The model has three states: unmonitored, on_cpu, and off_cpu.
trace_start transitions from unmonitored to on_cpu; switch_out and
switch_in cycle between on_cpu and off_cpu; trace_stop and
budget_expired return to unmonitored from either active state.
unmonitored is the sole accepting state.

switch_in, switch_out, and sched_wakeup self-loop in unmonitored;
sched_wakeup self-loops in on_cpu; switch_out and sched_wakeup
self-loop in off_cpu.

Signed-off-by: Wen Yang <wen.yang@linux.dev>
---
 MAINTAINERS                        |  3 +++
 tools/verification/models/tlob.dot | 25 +++++++++++++++++++++++++
 2 files changed, 28 insertions(+)
 create mode 100644 tools/verification/models/tlob.dot

diff --git a/MAINTAINERS b/MAINTAINERS
index 9fbb619c6..c2c56236c 100644
--- a/MAINTAINERS
+++ b/MAINTAINERS
@@ -23242,7 +23242,10 @@ S:	Maintained
 F:	Documentation/trace/rv/
 F:	include/linux/rv.h
 F:	include/rv/
+F:	include/uapi/linux/rv.h
 F:	kernel/trace/rv/
+F:	samples/rv/
+F:	tools/testing/selftests/rv/
 F:	tools/testing/selftests/verification/
 F:	tools/verification/
 
diff --git a/tools/verification/models/tlob.dot b/tools/verification/models/tlob.dot
new file mode 100644
index 000000000..df34a14b8
--- /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_unmonitored"};
+	{node [shape = ellipse] "unmonitored"};
+	{node [shape = plaintext] "unmonitored"};
+	{node [shape = plaintext] "on_cpu"};
+	{node [shape = plaintext] "off_cpu"};
+	"__init_unmonitored" -> "unmonitored";
+	"unmonitored" [label = "unmonitored", color = green3];
+	"unmonitored" -> "on_cpu" [ label = "trace_start" ];
+	"unmonitored" -> "unmonitored" [ label = "switch_in\nswitch_out\nsched_wakeup" ];
+	"on_cpu" [label = "on_cpu"];
+	"on_cpu" -> "off_cpu" [ label = "switch_out" ];
+	"on_cpu" -> "unmonitored" [ label = "trace_stop\nbudget_expired" ];
+	"on_cpu" -> "on_cpu" [ label = "sched_wakeup" ];
+	"off_cpu" [label = "off_cpu"];
+	"off_cpu" -> "on_cpu" [ label = "switch_in" ];
+	"off_cpu" -> "unmonitored" [ label = "trace_stop\nbudget_expired" ];
+	"off_cpu" -> "off_cpu" [ label = "switch_out\nsched_wakeup" ];
+	{ rank = min ;
+		"__init_unmonitored";
+		"unmonitored";
+	}
+}
-- 
2.43.0