CSP generation stops working without visible error messages

UoY-RoboStar / robocert-textual

Textual plugin and CSP generator for RoboCert

Eclipse Public License 2.0

2 stars 0 forks source link

CSP generation stops working without visible error messages #137

Closed twright closed 1 year ago

twright commented 1 year ago

In some cases the CSP file associated to specifications stop being generated without any visible error messages (sorry if this makes things hard to debug). In this case pressing the CSP button generates CSP for the RoboChart modules and creates timed/RoboCert but the pkg folder is empty.

I have created a branch of the RAD model which triggers this bug here: https://github.com/hlsa/Verifiability-Node/tree/csp-gen-bug/Models/RAD/RAD%20Controller

This happens with RoboCert Textual Editor version 0.2.0.202211101052.

twright commented 1 year ago

On further investigation it seems like this bug is being triggered by the message set MMovementOrGrip: if the final element of the set is movementWasAllowed(any) then generation silently fails, whether if it is (correctly) movementWasAllowed then it succeeds.

MattWindsor91 commented 1 year ago

Hmm, this is bad. There should be (and I'm sure I remember there being) a validation to make sure that parameter sets agreed in number and type, but this result makes me think that there isn't.

As for generation silently failing, that's strange too. It used to be that exceptions in the generator noisily crashed the Eclipse plugin. I think at some point I added SafeRunner in and this has made the exceptions get silently hidden. I'll look into this further, also.

MattWindsor91 commented 1 year ago

Ok, so both issues should now be resolved:

The generator will loudly emit a backtrace to stderr when it goes wrong (it should probably go through more official Eclipse channels, but this is close to what RoboChart does);
The validator now actively enforces the well-formedness conditions that require argument and parameter lists to agree on size and type. This will catch both the issue that caused the crash and also seems to catch a few missing (any)s in the example given.

I've also changed the syntax for wait because I messed it up in my last syntax sweep. The syntax is wait (X units on Y).

twright commented 1 year ago

Thank you very much for this; I have updated and can confirm that the validator (and the fixed version of this specification) are now working as expected.