kernel/git/stable/linux.git/tools/verification/dot2/automata.py, branch master

verification/dot2k: Prepare the frontend for LTL inclusion

2025-07-24T14:42:46+00:00

The dot2k tool has some code that can be reused for linear temporal logic monitor. Prepare its frontend for LTL inclusion: 1. Rename to be generic: rvgen 2. Replace the parameter --dot with 2 parameters: --class: to specific the monitor class, can be 'da' or 'ltl' --spec: the monitor specification file, .dot file for DA, and .ltl file for LTL The old command: python3 dot2/dot2k monitor -d wip.dot -t per_cpu is equivalent to the new commands: python3 rvgen monitor -c da -s wip.dot -t per_cpu Cc: Masami Hiramatsu Cc: Mathieu Desnoyers Link: https://lore.kernel.org/dea18f7a44374e4db8df5c7e785604bc3062ffc9.1751634289.git.namcao@linutronix.de Reviewed-by: Gabriele Monaco Signed-off-by: Nam Cao Signed-off-by: Steven Rostedt (Google)

verification/dot2k: Implement event type detection

2024-12-27T19:41:01+00:00

Currently dot2k treats all events equally and registers them with a general da_handle_event. This is however just part of the work because some events are necessary to understand when the monitor is entering the initial state. Specifically, the da_handle_start_event takes care of setting the monitor in the initial state and da_handle_start_run_event also registers the current event in the newly enabled monitor. da_handle_start_event can be used on events that only lead to the initial state (as it is currently done in the example monitors), while da_handle_start_run_event could be used on events that are only valid from the initial one. Failing to set at least one of those functions to handle events makes the monitor useless, since it will never be activated. This patch adapts dot2k to parse the events that surely lead to the initial state and set da_handle_start_event for those, if no such event is found but some events are only valid in the initial event, we instead set da_handle_start_run_event (it isn't necessary to set both). We still add a comment to warn the user to make sure this change is matching the model definition. Cc: Juri Lelli Cc: Thomas Gleixner Cc: John Kacur Link: https://lore.kernel.org/20241227144752.362911-9-gmonaco@redhat.com Signed-off-by: Gabriele Monaco Signed-off-by: Steven Rostedt (Google)

verification/dot2k: Add support for name and description options

2024-12-27T19:19:34+00:00

The dot2k command includes options to set a model name with -n and a description with -D, however those are not used in practice. This patch allows to specify a custom model name (by default the name of the dot file without extension) and a description which overrides the one in the C file. Cc: Juri Lelli Cc: Thomas Gleixner Cc: John Kacur Link: https://lore.kernel.org/20241227144752.362911-5-gmonaco@redhat.com Signed-off-by: Gabriele Monaco Signed-off-by: Steven Rostedt (Google)

verification/dot2: Improve dot parser robustness

2024-11-19T13:57:13+00:00

This patch makes the dot parser used by dot2c and dot2k slightly more robust, namely: * allows parsing files with the gv extension (GraphViz) * correctly parses edges with any indentation * used to work only with a single character (e.g. '\t') Additionally it fixes a couple of warnings reported by pylint such as wrong indentation and comparison to False instead of `not ...` Link: https://lore.kernel.org/20241017064238.41394-2-gmonaco@redhat.com Signed-off-by: Gabriele Monaco Signed-off-by: Steven Rostedt (Google)

Documentation/rv: Add deterministic automaton documentation

2022-07-30T18:01:29+00:00

Add documentation about deterministic automaton and its possible representations (formal, graphic, .dot and C). Link: https://lkml.kernel.org/r/387edaed87630bd5eb37c4275045dfd229700aa6.1659052063.git.bristot@kernel.org Cc: Wim Van Sebroeck Cc: Guenter Roeck Cc: Jonathan Corbet Cc: Ingo Molnar Cc: Thomas Gleixner Cc: Peter Zijlstra Cc: Will Deacon Cc: Catalin Marinas Cc: Marco Elver Cc: Dmitry Vyukov Cc: "Paul E. McKenney" Cc: Shuah Khan Cc: Gabriele Paoloni Cc: Juri Lelli Cc: Clark Williams Cc: Tao Zhou Cc: Randy Dunlap Cc: linux-doc@vger.kernel.org Cc: linux-kernel@vger.kernel.org Cc: linux-trace-devel@vger.kernel.org Signed-off-by: Daniel Bristot de Oliveira Signed-off-by: Steven Rostedt (Google)

tools/rv: Add dot2c

2022-07-30T18:01:29+00:00

dot2c is a tool that transforms an automata in the graphiviz .dot file into an C representation of the automata. usage: dot2c [-h] dot_file dot2c: converts a .dot file into a C structure positional arguments: dot_file The dot file to be converted optional arguments: -h, --help show this help message and exit Link: https://lkml.kernel.org/r/b26204ba9509c80bcda31b76cdea31ddb188cd24.1659052063.git.bristot@kernel.org Cc: Wim Van Sebroeck Cc: Guenter Roeck Cc: Jonathan Corbet Cc: Ingo Molnar Cc: Thomas Gleixner Cc: Peter Zijlstra Cc: Will Deacon Cc: Catalin Marinas Cc: Marco Elver Cc: Dmitry Vyukov Cc: "Paul E. McKenney" Cc: Shuah Khan Cc: Gabriele Paoloni Cc: Juri Lelli Cc: Clark Williams Cc: Tao Zhou Cc: Randy Dunlap Cc: linux-doc@vger.kernel.org Cc: linux-kernel@vger.kernel.org Cc: linux-trace-devel@vger.kernel.org Signed-off-by: Daniel Bristot de Oliveira Signed-off-by: Steven Rostedt (Google)