Thread (29 messages) 29 messages, 4 authors, 2025-07-08

Re: [PATCH v9 12/22] verification/rvgen: Restructure the classes to prepare for LTL inclusion

From: Gabriele Monaco <gmonaco@redhat.com>
Date: 2025-05-27 09:32:42
Also in: lkml


On Tue, 2025-05-27 at 11:27 +0200, Nam Cao wrote:
On Tue, May 27, 2025 at 11:15:21AM +0200, Gabriele Monaco wrote:
quoted

On Mon, 2025-05-19 at 12:27 +0200, Nam Cao wrote:
quoted
Both container generation and DA monitor generation is
implemented in
the
class dot2k. That requires some ugly "if is_container ... else
...".
If
linear temporal logic support is added at the current state, the
"if
else"
chain is longer and uglier.

Furthermore, container generation is irrevelant to .dot files. It
is
therefore illogical to be implemented in class "dot2k".

Clean it up, restructure the dot2k class into the following class
hierarchy:

         (RVGenerator)
              /\
             /  \
            /    \
           /      \
          /        \
    (Container)  (Monitor)
                    /\
                   /  \
                  /    \
                 /      \
              (dot2k)  [ltl2k] <- intended

This allows a simple and clean integration of LTL.

Reviewed-by: Gabriele Monaco <gmonaco@redhat.com>
Signed-off-by: Nam Cao <redacted>
---
Steve,

since this series is quite /meaty/ and it seems the later parts
require
a bit more discussion about tracepoints, could we start merging
until
here (1-12/22)?
I'd be tempted merging also 13 (actual LTL introduction) but
perhaps
keeping it together with the LTL monitors is cleaner.
The x86 patches have been merged through tip tree. My plan is sending
the
next version without the merged x86 patches, and without the arm64
patch -
it can be sent separately. Then the whole series can be applied.

I will do it after the merge window.
Alright, sounds good too.
Sorry for being pushy but I'm have a couple of other series kinda based
on this one and I'm getting a bit crazy maintaining all that ;)

Cheers,
Gabriele
Best regards,
Nam
  
Keyboard shortcuts
hback out one level
jnext message in thread
kprevious message in thread
ldrill in
Escclose help / fold thread tree
?toggle this help