Commit b6c62aa7 authored by Nam Cao's avatar Nam Cao Committed by Steven Rostedt (Google)
Browse files

verification/dot2k: Prepare the frontend for LTL inclusion 

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 <mhiramat@kernel.org>
Cc: Mathieu Desnoyers <mathieu.desnoyers@efficios.com>
Link: https://lore.kernel.org/dea18f7a44374e4db8df5c7e785604bc3062ffc9.1751634289.git.namcao@linutronix.de


Reviewed-by: default avatarGabriele Monaco <gmonaco@redhat.com>
Signed-off-by: default avatarNam Cao <namcao@linutronix.de>
Signed-off-by: default avatarSteven Rostedt (Google) <rostedt@goodmis.org>
parent 5270a0e3

tools/verification/dot2/Makefile→tools/verification/rvgen/Makefile

+5 −5
Original line number Diff line number Diff line
@@ -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)/

tools/verification/dot2/dot2k→tools/verification/rvgen/__main__.py

+13 −5
Original line number Diff line number Diff line
@@ -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:

tools/verification/dot2/dot2c→tools/verification/rvgen/dot2c

+1 −1
Original line number Diff line number Diff line
@@ -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