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. Best regards, Nam
