]> git.ipfire.org Git - thirdparty/linux.git/commit
verification/rvgen: Add support for Hybrid Automata
authorGabriele Monaco <gmonaco@redhat.com>
Mon, 30 Mar 2026 11:10:02 +0000 (13:10 +0200)
committerGabriele Monaco <gmonaco@redhat.com>
Tue, 31 Mar 2026 14:47:16 +0000 (16:47 +0200)
commita82adadb16894852fc8bc5a681f2070bea33b6b6
tree0d938ab6d3e3ac4a2b56584fedd9c20452f5338d
parentc707b1da1043f89e3368835c77a1f8a14a4a8843
verification/rvgen: Add support for Hybrid Automata

Add the possibility to parse dot files as hybrid automata and generate
the necessary code from rvgen.

Hybrid automata are very similar to deterministic ones and most
functionality is shared, the dot files include also constraints together
with event names (separated by ;) and state names (separated by \n).

The tool can now generate the appropriate code to validate constraints
at runtime according to the dot specification.

Reviewed-by: Nam Cao <namcao@linutronix.de>
Link: https://lore.kernel.org/r/20260330111010.153663-5-gmonaco@redhat.com
Signed-off-by: Gabriele Monaco <gmonaco@redhat.com>
tools/verification/rvgen/__main__.py
tools/verification/rvgen/rvgen/automata.py
tools/verification/rvgen/rvgen/dot2c.py
tools/verification/rvgen/rvgen/dot2k.py
tools/verification/rvgen/rvgen/generator.py
tools/verification/rvgen/rvgen/templates/dot2k/main.c
tools/verification/rvgen/rvgen/templates/dot2k/trace_hybrid.h [new file with mode: 0644]