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 <[email protected]> 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/[email protected]?part=3
