Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Invalid arities in generated CSP code #138

Open
twright opened this issue Nov 30, 2022 · 2 comments
Open

Invalid arities in generated CSP code #138

twright opened this issue Nov 30, 2022 · 2 comments

Comments

@twright
Copy link

twright commented Nov 30, 2022

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
Copy link
Author

twright commented Dec 1, 2022

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
Copy link
Collaborator

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.

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Projects
None yet
Development

No branches or pull requests

2 participants