| Commit message (Collapse) | Author | Age | Files | Lines |
|---|
| |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
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 <[email protected]>
Cc: Mathieu Desnoyers <[email protected]>
Link: https://lore.kernel.org/dea18f7a44374e4db8df5c7e785604bc3062ffc9.1751634289.git.namcao@linutronix.de
Reviewed-by: Gabriele Monaco <[email protected]>
Signed-off-by: Nam Cao <[email protected]>
Signed-off-by: Steven Rostedt (Google) <[email protected]>
|
| |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
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 <[email protected]>
Cc: Thomas Gleixner <[email protected]>
Cc: John Kacur <[email protected]>
Link: https://lore.kernel.org/[email protected]
Signed-off-by: Gabriele Monaco <[email protected]>
Signed-off-by: Steven Rostedt (Google) <[email protected]>
|
| |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
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 <[email protected]>
Cc: Thomas Gleixner <[email protected]>
Cc: John Kacur <[email protected]>
Link: https://lore.kernel.org/[email protected]
Signed-off-by: Gabriele Monaco <[email protected]>
Signed-off-by: Steven Rostedt (Google) <[email protected]>
|
| |
|
|
|
|
|
|
|
|
|
|
|
|
| |
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/[email protected]
Signed-off-by: Gabriele Monaco <[email protected]>
Signed-off-by: Steven Rostedt (Google) <[email protected]>
|
| |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
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 <[email protected]>
Cc: Guenter Roeck <[email protected]>
Cc: Jonathan Corbet <[email protected]>
Cc: Ingo Molnar <[email protected]>
Cc: Thomas Gleixner <[email protected]>
Cc: Peter Zijlstra <[email protected]>
Cc: Will Deacon <[email protected]>
Cc: Catalin Marinas <[email protected]>
Cc: Marco Elver <[email protected]>
Cc: Dmitry Vyukov <[email protected]>
Cc: "Paul E. McKenney" <[email protected]>
Cc: Shuah Khan <[email protected]>
Cc: Gabriele Paoloni <[email protected]>
Cc: Juri Lelli <[email protected]>
Cc: Clark Williams <[email protected]>
Cc: Tao Zhou <[email protected]>
Cc: Randy Dunlap <[email protected]>
Cc: [email protected]
Cc: [email protected]
Cc: [email protected]
Signed-off-by: Daniel Bristot de Oliveira <[email protected]>
Signed-off-by: Steven Rostedt (Google) <[email protected]>
|
|
|
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 <[email protected]>
Cc: Guenter Roeck <[email protected]>
Cc: Jonathan Corbet <[email protected]>
Cc: Ingo Molnar <[email protected]>
Cc: Thomas Gleixner <[email protected]>
Cc: Peter Zijlstra <[email protected]>
Cc: Will Deacon <[email protected]>
Cc: Catalin Marinas <[email protected]>
Cc: Marco Elver <[email protected]>
Cc: Dmitry Vyukov <[email protected]>
Cc: "Paul E. McKenney" <[email protected]>
Cc: Shuah Khan <[email protected]>
Cc: Gabriele Paoloni <[email protected]>
Cc: Juri Lelli <[email protected]>
Cc: Clark Williams <[email protected]>
Cc: Tao Zhou <[email protected]>
Cc: Randy Dunlap <[email protected]>
Cc: [email protected]
Cc: [email protected]
Cc: [email protected]
Signed-off-by: Daniel Bristot de Oliveira <[email protected]>
Signed-off-by: Steven Rostedt (Google) <[email protected]>
|
