Currently the automata parser assumes event strings don't have any
space, this stands true for event names, but can be a wrong assumption
if we want to store other information in the event strings (e.g.
constraints for hybrid automata).

Adapt the parser logic to allow spaces in the event strings.

Signed-off-by: Gabriele Monaco <gmonaco@redhat.com>
---
 tools/verification/rvgen/rvgen/automata.py | 9 ++++-----
 1 file changed, 4 insertions(+), 5 deletions(-)

diff --git a/tools/verification/rvgen/rvgen/automata.py b/tools/verification/rvgen/rvgen/automata.py
index 76d7a3cfaec6..c637cf4ee749 100644
--- a/tools/verification/rvgen/rvgen/automata.py
+++ b/tools/verification/rvgen/rvgen/automata.py
@@ -127,14 +127,13 @@ class Automata:
             #  ------------ event is here ------------^^^^^
             if self.__dot_lines[cursor].split()[1] == "->":
                 line = self.__dot_lines[cursor].split()
-                event = line[-2].replace('"','')
+                event = "".join(line[line.index("label")+2:-1]).replace('"','')
 
                 # when a transition has more than one lables, they are like this
                 # "local_irq_enable\nhw_local_irq_enable_n"
                 # so split them.
 
-                event = event.replace("\\n", " ")
-                for i in event.split():
+                for i in event.split("\\n"):
                     events.append(i)
             cursor += 1
 
@@ -167,8 +166,8 @@ class Automata:
                 line = self.__dot_lines[cursor].split()
                 origin_state = line[0].replace('"','').replace(',','_')
                 dest_state = line[2].replace('"','').replace(',','_')
-                possible_events = line[-2].replace('"','').replace("\\n", " ")
-                for event in possible_events.split():
+                possible_events = "".join(line[line.index("label")+2:-1]).replace('"','')
+                for event in possible_events.split("\\n"):
                     matrix[states_dict[origin_state]][events_dict[event]] = dest_state
             cursor += 1
 
-- 
2.50.1

On Thu, Aug 14, 2025 at 05:08:01PM +0200, Gabriele Monaco wrote:
> Currently the automata parser assumes event strings don't have any
> space, this stands true for event names, but can be a wrong assumption
> if we want to store other information in the event strings (e.g.
> constraints for hybrid automata).
> 
> Adapt the parser logic to allow spaces in the event strings.

The current parser does have a few problems. Not all valid .dot files are
accepted.

I have a patch buried somewhere which removes the custom parser and instead
uses a library. But then it adds a new dependency, so I'm not sure if it is
worth..

Nam

On Thu, 2025-08-21 at 14:22 +0200, Nam Cao wrote:
> On Thu, Aug 14, 2025 at 05:08:01PM +0200, Gabriele Monaco wrote:
> > Currently the automata parser assumes event strings don't have any
> > space, this stands true for event names, but can be a wrong
> > assumption
> > if we want to store other information in the event strings (e.g.
> > constraints for hybrid automata).
> > 
> > Adapt the parser logic to allow spaces in the event strings.
> 
> The current parser does have a few problems. Not all valid .dot files
> are accepted.
> 
> I have a patch buried somewhere which removes the custom parser and
> instead uses a library. But then it adds a new dependency, so I'm not
> sure if it is worth..

Yeah it isn't really robust, I tried to improve it a bit but sure
something is still failing it.
We don't need full dot capabilities, but just extract some keywords,
I'd avoid pulling in a dependency for that.

I'm imagining users would either generate graphs from the
Waters/Supremica tool [1] or copy/edit existing ones, so I'm not sure
they can go that far.
Still that's hacky because some things are just lightly implied by the
code (e.g. initial/final states, edges labels, etc.), so one day we
should at the very least say what DOT is valid and what not.

Do you have specific examples of what doesn't work?

Thanks,
Gabriele

[1] - https://github.com/robimalik/Waters/releases

On Thu, Aug 21, 2025 at 03:22:23PM +0200, Gabriele Monaco wrote:
> On Thu, 2025-08-21 at 14:22 +0200, Nam Cao wrote:
> > On Thu, Aug 14, 2025 at 05:08:01PM +0200, Gabriele Monaco wrote:
> > > Currently the automata parser assumes event strings don't have any
> > > space, this stands true for event names, but can be a wrong
> > > assumption
> > > if we want to store other information in the event strings (e.g.
> > > constraints for hybrid automata).
> > > 
> > > Adapt the parser logic to allow spaces in the event strings.
> > 
> > The current parser does have a few problems. Not all valid .dot files
> > are accepted.
> > 
> > I have a patch buried somewhere which removes the custom parser and
> > instead uses a library. But then it adds a new dependency, so I'm not
> > sure if it is worth..
> 
> Yeah it isn't really robust, I tried to improve it a bit but sure
> something is still failing it.
> We don't need full dot capabilities, but just extract some keywords,
> I'd avoid pulling in a dependency for that.
> 
> I'm imagining users would either generate graphs from the
> Waters/Supremica tool [1] or copy/edit existing ones, so I'm not sure
> they can go that far.

When I tried out the DA monitor, I edited the .dot files directly.

> Still that's hacky because some things are just lightly implied by the
> code (e.g. initial/final states, edges labels, etc.), so one day we
> should at the very least say what DOT is valid and what not.

We could also rewrite the parser using ply with a well-defined grammar and
tokenizer, like how the LTL parser is implemented. Doing it this way would
be easier to validate as well, because the grammar would be mostly
copy-pasted from the specification.

> Do you have specific examples of what doesn't work?

Two things that I can remember:

  - breaking long lines

  - C-style and C++-style comments

Not really relevant if you do not edit the .dot files directly like I did.
But these things are valid according to https://graphviz.org/doc/info/lang.html

Nam

2025-08-21T15:15:36Z Nam Cao <namcao@linutronix.de>:
> We could also rewrite the parser using ply with a well-defined grammar and
> tokenizer, like how the LTL parser is implemented. Doing it this way would
> be easier to validate as well, because the grammar would be mostly
> copy-pasted from the specification.

Good idea, I can look into that and see how hard it's going to be (I'm not familiar with ply, but I see it's well documented).

>> Do you have specific examples of what doesn't work?
>
> Two things that I can remember:
>
>   - breaking long lines
>
>   - C-style and C++-style comments
>

Yeah those could break some assumptions (and they shouldn't), especially the line breaks.. And supporting it in the current parser may make it just uglier..

Thanks,
Gabriele