Re: [PATCH v6 3/9] rv: Add tlob model DOT file

[sashiko-bot@kernel.org]

Thank you for your contribution! Sashiko AI review found 1 potential issue(s) to consider:
- [Medium] The implemented DOT model contradicts explicit claims made in the commit message regarding states, transitions, and invariants.
--

--- Patch [3]: [PATCH v6 3/9] rv: Add tlob model DOT file ---
commit 8a3ea61817d2834335f8a9230c5ffaf2a08353b7
Author: Wen Yang <wen.yang@linux.dev>

rv: Add tlob model DOT file

This commit adds the Graphviz DOT specification of the tlob hybrid
automaton to the kernel's verification models.

> 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.

[Severity: Medium]
Does this description accurately reflect the implemented model?

The text mentions three states, five transitions, and an invariant active
in all states. However, the included DOT file defines a fourth "stopped"
state, two additional transitions ("stop" and "start"), and omits the
invariant from the "stopped" state:

tools/verification/models/tlob.dot:
	"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)" ];

Could the commit message be updated to match the actual automaton
implemented in the code?

-- 
Sashiko AI review · https://sashiko.dev/#/patchset/cover.1787243842.git.wen.yang@linux.dev?part=3