Re: [PATCH v10 17/19] rv: Add rtapp_sleep monitor

[Gabriele Monaco <gmonaco@redhat.com>]

On Tue, 2025-07-08 at 09:50 +0200, Nam Cao wrote:
> On Wed, Jul 02, 2025 at 08:29:28AM +0200, Gabriele Monaco wrote:
> > That's a good point, at the moment the DA monitors have a comment
> > in
> > the /completely/ generated files (the automata header), the others
> > where just a skeleton is prepared have some hints that we removed
> > while
> > filling the monitor.
> > 
> > I'd say for now it's good to just add a comment in the LTL header
> > (like
> > Dot2k:fill_model_h_header), then we can adapt all generated files
> > (whether fully or not) to have also the actual command that
> > generated
> > them starting from the model file.
> > Or did you have something different in mind, Nam?
> 
> Yes, I think the same.
> 
> An easy way to do it is just dump out sys.argv. But one thing I'm
> unsure
> about: I prefer to execute the command from tools/verification, and
> the
> command I use would not work for people running from root directory.
> I
> would like the printed command to always appear as if it is executed
> from
> root directory. However, I see no elegant way to do it - will need to
> think
> some more.
> 

Mmh, that's something I didn't think about, but perhaps we shouldn't be
too picky and think users would just copy-paste the command provided
and expect it to work.

By the way, the sys.argv could be a great start, but depending on the
workflow, one may not even keep the model in the location where it
would be committed during generation (I usually don't, mostly out of
laziness).

Anyway, although I'd prefer running the command from the repo root,
just for sake of compactness we could include the command as run from
tools/verification, but I'm fine either ways. I think by adding proper
documentation, the reader can easily figure that out.
We could edit sys.argv before printing to make sure the model is where
we expect it to be, and perhaps strip/add some arguments (e.g. if we
want the -a or not), just to keep it always consistent and predictable.

As long as the command written to the files is consistent and clear to
understand, I wouldn't mind too much.

Thanks,
Gabriele