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

[sashiko-bot@kernel.org]

Thank you for your contribution! Sashiko AI review found 2 potential issue(s) to consider:
- [High] The 'running' node is defined twice with conflicting shapes, incorrectly designating it as the final state instead of 'stopped'.
- [Medium] The commit message significantly contradicts the implemented DOT model's states, transitions, and invariants.
--

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

rv: Add tlob model DOT file

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]
This isn't a bug, but does this description accurately reflect the
implemented model?

The DOT file defines four states (running, waiting, sleeping, stopped), six
transitions, and the clock invariant is intentionally absent from the
"stopped" state.

> diff --git a/tools/verification/models/tlob.dot b/tools/verification/models/tlob.dot
> new file mode 100644
> index 0000000000000..7f6f09c3d7cf0
> --- /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"};

[Severity: High]
Is it intentional to define the "running" node twice with conflicting shapes?

Because tools/verification/rvgen/rvgen/automata.py prioritizes the first
definition ("ellipse") over the second ("plaintext") when merging attributes,
this improperly designates "running" as the final accepting state instead of
"stopped".

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