search

UoY-RoboStar / robocert-textual

Textual plugin and CSP generator for RoboCert
Eclipse Public License 2.0
2 stars 0 forks source link

Invalid arities in generated CSP code #138

Open twright opened 1 year ago

twright commented 1 year ago

I have ran into an issue where after making some changes to the RAD RoboChart model, the RoboCert specification generates invalid CSP code. Specifically, I observed the following error message in FDR:

/home/thomaswright/Documents/Research/RoboTool/workspace/RAD Controller/csp-gen/timed/robocert/pkg/specification.csp:32:14-35:
    Couldn't match expected type (a, b, c, d, e, f) -> g
            with actual type (h, i, j, k, l, m, n) -> Proc
    In the expression: RobotAssistedDressing::O__
    In the expression:…
    In a pattern binding:…
    Relevant variable types:
        RobotAssistedDressing::O__ :: (o, p, q, r, s, t, u) -> Proc
        RAD::id__ :: Int
        RAD::const_radcontrol_CDressingControl_Kp :: Int
        RAD::const_radcontrol_CDressingControl_Ki :: Int
        RAD::const_radcontrol_CDressingControl_Kd :: Int
        RAD::const_radcontrol_CDressingControl_step :: Int
        RAD::const_movement_MovementControl_EPSILON :: Int

This may be due to some bug in the model I have missed, but this is not caught by the validation in the RoboChart textual editor or the CSP generator.

This bug is triggered on the following branch of the RAD model repository: https://github.com/hlsa/Verifiability-Node/tree/robocert-type-bug/Models/RAD

twright commented 1 year ago

On further investigation, it seems like this bug is another case where the CSP generator stops working without emitting any error messages. However, in this case an out of date specification.csp file is left behind, causing the above type error due to mismatches between the specification CSP and the model CSP.

MattWindsor91 commented 1 year ago

Hmm, has Eclipse not output anything in stderr? I'm unsure where any stderr emitted by Eclipse plugins is directed under usual conditions.

I'll try running the plugin in debug mode at some point soon to see if I can get some error output out of it.

Failing that, I might just remove the bit of code that's making it catch errors and make it just loudly throw them. Or, at least, remove the generated files.