]> git.ipfire.org Git - thirdparty/kernel/stable.git/commit
projects / thirdparty / kernel / stable.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: cce86e0) | patch
verification/rvgen: Add support for linear temporal logic
authorNam Cao <namcao@linutronix.de>
Fri, 4 Jul 2025 13:20:06 +0000 (15:20 +0200)
committerSteven Rostedt (Google) <rostedt@goodmis.org>
Thu, 24 Jul 2025 14:42:47 +0000 (10:42 -0400)
commit97ffa4ce6ab329bf601f1362bb2e181636fcc3a0
tree3e8de2282f69e2238fb774813f6d73aca2db8de5tree
parentcce86e03a27fdce11684c85ee33c528124904d8dcommit | diff
verification/rvgen: Add support for linear temporal logic

Add support for generating RV monitors from linear temporal logic, similar
to the generation of deterministic automaton monitors.

Cc: Masami Hiramatsu <mhiramat@kernel.org>
Cc: Mathieu Desnoyers <mathieu.desnoyers@efficios.com>
Cc: Gabriele Monaco <gmonaco@redhat.com>
Link: https://lore.kernel.org/f3c63b363ff9c5af3302ba2b5d92a26a98700eaf.1751634289.git.namcao@linutronix.de
Signed-off-by: Nam Cao <namcao@linutronix.de>
Signed-off-by: Steven Rostedt (Google) <rostedt@goodmis.org>
tools/verification/rvgen/.gitignore [new file with mode: 0644] blob
tools/verification/rvgen/Makefile diff | blob | blame | history
tools/verification/rvgen/__main__.py diff | blob | blame | history
tools/verification/rvgen/rvgen/ltl2ba.py [new file with mode: 0644] blob
tools/verification/rvgen/rvgen/ltl2k.py [new file with mode: 0644] blob
tools/verification/rvgen/rvgen/templates/ltl2k/main.c [new file with mode: 0644] blob
tools/verification/rvgen/rvgen/templates/ltl2k/trace.h [new file with mode: 0644] blob
Mirror https://git.kernel.org/pub/scm/linux/kernel/git/stable/linux.git