| Message ID | af31461eae544f9aea6fb3e1c16a0bd24574ef56.1744785335.git.namcao@linutronix.de (mailing list archive) |
|---|---|
| State | New |
| Headers | show |
| Series | RV: Linear temporal logic monitors for RT application | expand |
On Wed, 2025-04-16 at 08:51 +0200, Nam Cao wrote: > 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 dot2/dot2k monitor -c da -s wip.dot -t per_cpu Some more things changed here: python3 rvgen monitor -c da -s wip.dot -t per_cpu For the rest, all changes in the scripts (11-12/22) look good to me. Reviewed-by: Gabriele Monaco <gmonaco@redhat.com> Thanks, Gabriele > > Signed-off-by: Nam Cao <namcao@linutronix.de> > --- > tools/verification/{dot2 => rvgen}/Makefile | 10 +++++----- > .../{dot2/dot2k => rvgen/__main__.py} | 18 +++++++++++++--- > -- > tools/verification/{dot2 => rvgen}/dot2c | 2 +- > .../{dot2 => rvgen}/dot2k_templates/Kconfig | 0 > .../dot2k_templates/Kconfig_container | 0 > .../{dot2 => rvgen}/dot2k_templates/main.c | 0 > .../dot2k_templates/main_container.c | 0 > .../dot2k_templates/main_container.h | 0 > .../{dot2 => rvgen}/dot2k_templates/trace.h | 0 > .../{dot2 => rvgen/rvgen}/automata.py | 0 > .../{dot2 => rvgen/rvgen}/dot2c.py | 2 +- > .../{dot2 => rvgen/rvgen}/dot2k.py | 10 +++++----- > 12 files changed, 25 insertions(+), 17 deletions(-) > rename tools/verification/{dot2 => rvgen}/Makefile (55%) > rename tools/verification/{dot2/dot2k => rvgen/__main__.py} (72%) > rename tools/verification/{dot2 => rvgen}/dot2c (97%) > rename tools/verification/{dot2 => rvgen}/dot2k_templates/Kconfig > (100%) > rename tools/verification/{dot2 => > rvgen}/dot2k_templates/Kconfig_container (100%) > rename tools/verification/{dot2 => rvgen}/dot2k_templates/main.c > (100%) > rename tools/verification/{dot2 => > rvgen}/dot2k_templates/main_container.c (100%) > rename tools/verification/{dot2 => > rvgen}/dot2k_templates/main_container.h (100%) > rename tools/verification/{dot2 => rvgen}/dot2k_templates/trace.h > (100%) > rename tools/verification/{dot2 => rvgen/rvgen}/automata.py (100%) > rename tools/verification/{dot2 => rvgen/rvgen}/dot2c.py (99%) > rename tools/verification/{dot2 => rvgen/rvgen}/dot2k.py (98%) > > diff --git a/tools/verification/dot2/Makefile > b/tools/verification/rvgen/Makefile > similarity index 55% > rename from tools/verification/dot2/Makefile > rename to tools/verification/rvgen/Makefile > index 021beb07a521..cea9c21c3bce 100644 > --- a/tools/verification/dot2/Makefile > +++ b/tools/verification/rvgen/Makefile > @@ -3,7 +3,7 @@ INSTALL=install > prefix ?= /usr > bindir ?= $(prefix)/bin > mandir ?= $(prefix)/share/man > -miscdir ?= $(prefix)/share/dot2 > +miscdir ?= $(prefix)/share/rvgen > srcdir ?= $(prefix)/src > > PYLIB ?= $(shell python3 -c 'import sysconfig; print > (sysconfig.get_path("purelib"))') > @@ -16,11 +16,11 @@ clean: > > .PHONY: install > install: > - $(INSTALL) automata.py -D -m 644 > $(DESTDIR)$(PYLIB)/dot2/automata.py > - $(INSTALL) dot2c.py -D -m 644 > $(DESTDIR)$(PYLIB)/dot2/dot2c.py > + $(INSTALL) rvgen/automata.py -D -m 644 > $(DESTDIR)$(PYLIB)/rvgen/automata.py > + $(INSTALL) rvgen/dot2c.py -D -m 644 > $(DESTDIR)$(PYLIB)/rvgen/dot2c.py > $(INSTALL) dot2c -D -m 755 $(DESTDIR)$(bindir)/ > - $(INSTALL) dot2k.py -D -m 644 > $(DESTDIR)$(PYLIB)/dot2/dot2k.py > - $(INSTALL) dot2k -D -m 755 $(DESTDIR)$(bindir)/ > + $(INSTALL) rvgen/dot2k.py -D -m 644 > $(DESTDIR)$(PYLIB)/rvgen/dot2k.py > + $(INSTALL) __main__.py -D -m 755 $(DESTDIR)$(bindir)/rvgen > > mkdir -p ${miscdir}/ > cp -rp dot2k_templates $(DESTDIR)$(miscdir)/ > diff --git a/tools/verification/dot2/dot2k > b/tools/verification/rvgen/__main__.py > similarity index 72% > rename from tools/verification/dot2/dot2k > rename to tools/verification/rvgen/__main__.py > index 133fb17d9d47..994d320ad2d1 100644 > --- a/tools/verification/dot2/dot2k > +++ b/tools/verification/rvgen/__main__.py > @@ -9,11 +9,11 @@ > # Documentation/trace/rv/da_monitor_synthesis.rst > > if __name__ == '__main__': > - from dot2.dot2k import dot2k > + from rvgen.dot2k import dot2k > import argparse > import sys > > - parser = argparse.ArgumentParser(description='transform .dot > file into kernel rv monitor') > + parser = argparse.ArgumentParser(description='Generate kernel rv > monitor') > parser.add_argument("-D", "--description", dest="description", > required=False) > parser.add_argument("-a", "--auto_patch", dest="auto_patch", > action="store_true", required=False, > @@ -25,7 +25,9 @@ if __name__ == '__main__': > monitor_parser.add_argument('-n', "--model_name", > dest="model_name") > monitor_parser.add_argument("-p", "--parent", dest="parent", > required=False, help="Create a > monitor nested to parent") > - monitor_parser.add_argument('-d', "--dot", dest="dot_file") > + monitor_parser.add_argument('-c', "--class", > dest="monitor_class", > + help="Monitor class, either \"da\" > or \"ltl\"") > + monitor_parser.add_argument('-s', "--spec", dest="spec", > help="Monitor specification file") > monitor_parser.add_argument('-t', "--monitor_type", > dest="monitor_type", > help=f"Available options: {', > '.join(dot2k.monitor_types.keys())}") > > @@ -36,8 +38,14 @@ if __name__ == '__main__': > > try: > if params.subcmd == "monitor": > - print("Opening and parsing the dot file %s" % > params.dot_file) > - monitor = dot2k(params.dot_file, params.monitor_type, > vars(params)) > + print("Opening and parsing the specification file %s" % > params.spec) > + if params.monitor_class == "da": > + monitor = dot2k(params.spec, params.monitor_type, > vars(params)) > + elif params.monitor_class == "ltl": > + raise NotImplementedError > + else: > + print("Unknown monitor class:", > params.monitor_class) > + sys.exit(1) > else: > monitor = dot2k(None, None, vars(params)) > except Exception as e: > diff --git a/tools/verification/dot2/dot2c > b/tools/verification/rvgen/dot2c > similarity index 97% > rename from tools/verification/dot2/dot2c > rename to tools/verification/rvgen/dot2c > index 3fe89ab88b65..bf0c67c5b66c 100644 > --- a/tools/verification/dot2/dot2c > +++ b/tools/verification/rvgen/dot2c > @@ -14,7 +14,7 @@ > # Documentation/trace/rv/deterministic_automata.rst > > if __name__ == '__main__': > - from dot2 import dot2c > + from rvgen import dot2c > import argparse > import sys > > diff --git a/tools/verification/dot2/dot2k_templates/Kconfig > b/tools/verification/rvgen/dot2k_templates/Kconfig > similarity index 100% > rename from tools/verification/dot2/dot2k_templates/Kconfig > rename to tools/verification/rvgen/dot2k_templates/Kconfig > diff --git > a/tools/verification/dot2/dot2k_templates/Kconfig_container > b/tools/verification/rvgen/dot2k_templates/Kconfig_container > similarity index 100% > rename from tools/verification/dot2/dot2k_templates/Kconfig_container > rename to tools/verification/rvgen/dot2k_templates/Kconfig_container > diff --git a/tools/verification/dot2/dot2k_templates/main.c > b/tools/verification/rvgen/dot2k_templates/main.c > similarity index 100% > rename from tools/verification/dot2/dot2k_templates/main.c > rename to tools/verification/rvgen/dot2k_templates/main.c > diff --git a/tools/verification/dot2/dot2k_templates/main_container.c > b/tools/verification/rvgen/dot2k_templates/main_container.c > similarity index 100% > rename from tools/verification/dot2/dot2k_templates/main_container.c > rename to tools/verification/rvgen/dot2k_templates/main_container.c > diff --git a/tools/verification/dot2/dot2k_templates/main_container.h > b/tools/verification/rvgen/dot2k_templates/main_container.h > similarity index 100% > rename from tools/verification/dot2/dot2k_templates/main_container.h > rename to tools/verification/rvgen/dot2k_templates/main_container.h > diff --git a/tools/verification/dot2/dot2k_templates/trace.h > b/tools/verification/rvgen/dot2k_templates/trace.h > similarity index 100% > rename from tools/verification/dot2/dot2k_templates/trace.h > rename to tools/verification/rvgen/dot2k_templates/trace.h > diff --git a/tools/verification/dot2/automata.py > b/tools/verification/rvgen/rvgen/automata.py > similarity index 100% > rename from tools/verification/dot2/automata.py > rename to tools/verification/rvgen/rvgen/automata.py > diff --git a/tools/verification/dot2/dot2c.py > b/tools/verification/rvgen/rvgen/dot2c.py > similarity index 99% > rename from tools/verification/dot2/dot2c.py > rename to tools/verification/rvgen/rvgen/dot2c.py > index fa2816ac7b61..6009caf568d9 100644 > --- a/tools/verification/dot2/dot2c.py > +++ b/tools/verification/rvgen/rvgen/dot2c.py > @@ -13,7 +13,7 @@ > # For further information, see: > # Documentation/trace/rv/deterministic_automata.rst > > -from dot2.automata import Automata > +from .automata import Automata > > class Dot2c(Automata): > enum_suffix = "" > diff --git a/tools/verification/dot2/dot2k.py > b/tools/verification/rvgen/rvgen/dot2k.py > similarity index 98% > rename from tools/verification/dot2/dot2k.py > rename to tools/verification/rvgen/rvgen/dot2k.py > index 9ec99e297012..e29462413194 100644 > --- a/tools/verification/dot2/dot2k.py > +++ b/tools/verification/rvgen/rvgen/dot2k.py > @@ -8,13 +8,13 @@ > # For further information, see: > # Documentation/trace/rv/da_monitor_synthesis.rst > > -from dot2.dot2c import Dot2c > +from .dot2c import Dot2c > import platform > import os > > class dot2k(Dot2c): > monitor_types = { "global" : 1, "per_cpu" : 2, "per_task" : 3 } > - monitor_templates_dir = "dot2/dot2k_templates/" > + monitor_templates_dir = "rvgen/dot2k_templates/" > rv_dir = "kernel/trace/rv" > monitor_type = "per_cpu" > > @@ -60,14 +60,14 @@ class dot2k(Dot2c): > if platform.system() != "Linux": > raise OSError("I can only run on Linux.") > > - kernel_path = > "/lib/modules/%s/build/tools/verification/dot2/dot2k_templates/" % > (platform.release()) > + kernel_path = > "/lib/modules/%s/build/tools/verification/rvgen/dot2k_templates/" % > (platform.release()) > > if os.path.exists(kernel_path): > self.monitor_templates_dir = kernel_path > return > > - if os.path.exists("/usr/share/dot2/dot2k_templates/"): > - self.monitor_templates_dir = > "/usr/share/dot2/dot2k_templates/" > + if os.path.exists("/usr/share/rvgen/dot2k_templates/"): > + self.monitor_templates_dir = > "/usr/share/rvgen/dot2k_templates/" > return > > raise FileNotFoundError("Could not find the template > directory, do you have the kernel source installed?")
diff --git a/tools/verification/dot2/Makefile b/tools/verification/rvgen/Makefile similarity index 55% rename from tools/verification/dot2/Makefile rename to tools/verification/rvgen/Makefile index 021beb07a521..cea9c21c3bce 100644 --- a/tools/verification/dot2/Makefile +++ b/tools/verification/rvgen/Makefile @@ -3,7 +3,7 @@ INSTALL=install prefix ?= /usr bindir ?= $(prefix)/bin mandir ?= $(prefix)/share/man -miscdir ?= $(prefix)/share/dot2 +miscdir ?= $(prefix)/share/rvgen srcdir ?= $(prefix)/src PYLIB ?= $(shell python3 -c 'import sysconfig; print (sysconfig.get_path("purelib"))') @@ -16,11 +16,11 @@ clean: .PHONY: install install: - $(INSTALL) automata.py -D -m 644 $(DESTDIR)$(PYLIB)/dot2/automata.py - $(INSTALL) dot2c.py -D -m 644 $(DESTDIR)$(PYLIB)/dot2/dot2c.py + $(INSTALL) rvgen/automata.py -D -m 644 $(DESTDIR)$(PYLIB)/rvgen/automata.py + $(INSTALL) rvgen/dot2c.py -D -m 644 $(DESTDIR)$(PYLIB)/rvgen/dot2c.py $(INSTALL) dot2c -D -m 755 $(DESTDIR)$(bindir)/ - $(INSTALL) dot2k.py -D -m 644 $(DESTDIR)$(PYLIB)/dot2/dot2k.py - $(INSTALL) dot2k -D -m 755 $(DESTDIR)$(bindir)/ + $(INSTALL) rvgen/dot2k.py -D -m 644 $(DESTDIR)$(PYLIB)/rvgen/dot2k.py + $(INSTALL) __main__.py -D -m 755 $(DESTDIR)$(bindir)/rvgen mkdir -p ${miscdir}/ cp -rp dot2k_templates $(DESTDIR)$(miscdir)/ diff --git a/tools/verification/dot2/dot2k b/tools/verification/rvgen/__main__.py similarity index 72% rename from tools/verification/dot2/dot2k rename to tools/verification/rvgen/__main__.py index 133fb17d9d47..994d320ad2d1 100644 --- a/tools/verification/dot2/dot2k +++ b/tools/verification/rvgen/__main__.py @@ -9,11 +9,11 @@ # Documentation/trace/rv/da_monitor_synthesis.rst if __name__ == '__main__': - from dot2.dot2k import dot2k + from rvgen.dot2k import dot2k import argparse import sys - parser = argparse.ArgumentParser(description='transform .dot file into kernel rv monitor') + parser = argparse.ArgumentParser(description='Generate kernel rv monitor') parser.add_argument("-D", "--description", dest="description", required=False) parser.add_argument("-a", "--auto_patch", dest="auto_patch", action="store_true", required=False, @@ -25,7 +25,9 @@ if __name__ == '__main__': monitor_parser.add_argument('-n', "--model_name", dest="model_name") monitor_parser.add_argument("-p", "--parent", dest="parent", required=False, help="Create a monitor nested to parent") - monitor_parser.add_argument('-d', "--dot", dest="dot_file") + monitor_parser.add_argument('-c', "--class", dest="monitor_class", + help="Monitor class, either \"da\" or \"ltl\"") + monitor_parser.add_argument('-s', "--spec", dest="spec", help="Monitor specification file") monitor_parser.add_argument('-t', "--monitor_type", dest="monitor_type", help=f"Available options: {', '.join(dot2k.monitor_types.keys())}") @@ -36,8 +38,14 @@ if __name__ == '__main__': try: if params.subcmd == "monitor": - print("Opening and parsing the dot file %s" % params.dot_file) - monitor = dot2k(params.dot_file, params.monitor_type, vars(params)) + print("Opening and parsing the specification file %s" % params.spec) + if params.monitor_class == "da": + monitor = dot2k(params.spec, params.monitor_type, vars(params)) + elif params.monitor_class == "ltl": + raise NotImplementedError + else: + print("Unknown monitor class:", params.monitor_class) + sys.exit(1) else: monitor = dot2k(None, None, vars(params)) except Exception as e: diff --git a/tools/verification/dot2/dot2c b/tools/verification/rvgen/dot2c similarity index 97% rename from tools/verification/dot2/dot2c rename to tools/verification/rvgen/dot2c index 3fe89ab88b65..bf0c67c5b66c 100644 --- a/tools/verification/dot2/dot2c +++ b/tools/verification/rvgen/dot2c @@ -14,7 +14,7 @@ # Documentation/trace/rv/deterministic_automata.rst if __name__ == '__main__': - from dot2 import dot2c + from rvgen import dot2c import argparse import sys diff --git a/tools/verification/dot2/dot2k_templates/Kconfig b/tools/verification/rvgen/dot2k_templates/Kconfig similarity index 100% rename from tools/verification/dot2/dot2k_templates/Kconfig rename to tools/verification/rvgen/dot2k_templates/Kconfig diff --git a/tools/verification/dot2/dot2k_templates/Kconfig_container b/tools/verification/rvgen/dot2k_templates/Kconfig_container similarity index 100% rename from tools/verification/dot2/dot2k_templates/Kconfig_container rename to tools/verification/rvgen/dot2k_templates/Kconfig_container diff --git a/tools/verification/dot2/dot2k_templates/main.c b/tools/verification/rvgen/dot2k_templates/main.c similarity index 100% rename from tools/verification/dot2/dot2k_templates/main.c rename to tools/verification/rvgen/dot2k_templates/main.c diff --git a/tools/verification/dot2/dot2k_templates/main_container.c b/tools/verification/rvgen/dot2k_templates/main_container.c similarity index 100% rename from tools/verification/dot2/dot2k_templates/main_container.c rename to tools/verification/rvgen/dot2k_templates/main_container.c diff --git a/tools/verification/dot2/dot2k_templates/main_container.h b/tools/verification/rvgen/dot2k_templates/main_container.h similarity index 100% rename from tools/verification/dot2/dot2k_templates/main_container.h rename to tools/verification/rvgen/dot2k_templates/main_container.h diff --git a/tools/verification/dot2/dot2k_templates/trace.h b/tools/verification/rvgen/dot2k_templates/trace.h similarity index 100% rename from tools/verification/dot2/dot2k_templates/trace.h rename to tools/verification/rvgen/dot2k_templates/trace.h diff --git a/tools/verification/dot2/automata.py b/tools/verification/rvgen/rvgen/automata.py similarity index 100% rename from tools/verification/dot2/automata.py rename to tools/verification/rvgen/rvgen/automata.py diff --git a/tools/verification/dot2/dot2c.py b/tools/verification/rvgen/rvgen/dot2c.py similarity index 99% rename from tools/verification/dot2/dot2c.py rename to tools/verification/rvgen/rvgen/dot2c.py index fa2816ac7b61..6009caf568d9 100644 --- a/tools/verification/dot2/dot2c.py +++ b/tools/verification/rvgen/rvgen/dot2c.py @@ -13,7 +13,7 @@ # For further information, see: # Documentation/trace/rv/deterministic_automata.rst -from dot2.automata import Automata +from .automata import Automata class Dot2c(Automata): enum_suffix = "" diff --git a/tools/verification/dot2/dot2k.py b/tools/verification/rvgen/rvgen/dot2k.py similarity index 98% rename from tools/verification/dot2/dot2k.py rename to tools/verification/rvgen/rvgen/dot2k.py index 9ec99e297012..e29462413194 100644 --- a/tools/verification/dot2/dot2k.py +++ b/tools/verification/rvgen/rvgen/dot2k.py @@ -8,13 +8,13 @@ # For further information, see: # Documentation/trace/rv/da_monitor_synthesis.rst -from dot2.dot2c import Dot2c +from .dot2c import Dot2c import platform import os class dot2k(Dot2c): monitor_types = { "global" : 1, "per_cpu" : 2, "per_task" : 3 } - monitor_templates_dir = "dot2/dot2k_templates/" + monitor_templates_dir = "rvgen/dot2k_templates/" rv_dir = "kernel/trace/rv" monitor_type = "per_cpu" @@ -60,14 +60,14 @@ class dot2k(Dot2c): if platform.system() != "Linux": raise OSError("I can only run on Linux.") - kernel_path = "/lib/modules/%s/build/tools/verification/dot2/dot2k_templates/" % (platform.release()) + kernel_path = "/lib/modules/%s/build/tools/verification/rvgen/dot2k_templates/" % (platform.release()) if os.path.exists(kernel_path): self.monitor_templates_dir = kernel_path return - if os.path.exists("/usr/share/dot2/dot2k_templates/"): - self.monitor_templates_dir = "/usr/share/dot2/dot2k_templates/" + if os.path.exists("/usr/share/rvgen/dot2k_templates/"): + self.monitor_templates_dir = "/usr/share/rvgen/dot2k_templates/" return raise FileNotFoundError("Could not find the template directory, do you have the kernel source installed?")
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 dot2/dot2k monitor -c da -s wip.dot -t per_cpu Signed-off-by: Nam Cao <namcao@linutronix.de> --- tools/verification/{dot2 => rvgen}/Makefile | 10 +++++----- .../{dot2/dot2k => rvgen/__main__.py} | 18 +++++++++++++----- tools/verification/{dot2 => rvgen}/dot2c | 2 +- .../{dot2 => rvgen}/dot2k_templates/Kconfig | 0 .../dot2k_templates/Kconfig_container | 0 .../{dot2 => rvgen}/dot2k_templates/main.c | 0 .../dot2k_templates/main_container.c | 0 .../dot2k_templates/main_container.h | 0 .../{dot2 => rvgen}/dot2k_templates/trace.h | 0 .../{dot2 => rvgen/rvgen}/automata.py | 0 .../{dot2 => rvgen/rvgen}/dot2c.py | 2 +- .../{dot2 => rvgen/rvgen}/dot2k.py | 10 +++++----- 12 files changed, 25 insertions(+), 17 deletions(-) rename tools/verification/{dot2 => rvgen}/Makefile (55%) rename tools/verification/{dot2/dot2k => rvgen/__main__.py} (72%) rename tools/verification/{dot2 => rvgen}/dot2c (97%) rename tools/verification/{dot2 => rvgen}/dot2k_templates/Kconfig (100%) rename tools/verification/{dot2 => rvgen}/dot2k_templates/Kconfig_container (100%) rename tools/verification/{dot2 => rvgen}/dot2k_templates/main.c (100%) rename tools/verification/{dot2 => rvgen}/dot2k_templates/main_container.c (100%) rename tools/verification/{dot2 => rvgen}/dot2k_templates/main_container.h (100%) rename tools/verification/{dot2 => rvgen}/dot2k_templates/trace.h (100%) rename tools/verification/{dot2 => rvgen/rvgen}/automata.py (100%) rename tools/verification/{dot2 => rvgen/rvgen}/dot2c.py (99%) rename tools/verification/{dot2 => rvgen/rvgen}/dot2k.py (98%)