Variable mapping

[anaisac]

Hello everyone :)

Currently I've putting most of my variables with variable type= Input and data type = boolean.
But I was seeing in this document (page 57) that has a small explanation for the different on selecting Input/Output/Internal. And I've found no information for the Function and Mode types.
I would like to understand more what is each type and confirm what is most adequate selection for my system.

Can someone explain this a bit further or reference me to a document where this is explained?

Thank you,
Anaísa Carvalho

[anaisac]

Another question I have is:
We have 2 export languages: CoPilot and CoCoSim.
But where does this selection leads to?

Currently, if I have CoPilot select, all my components are able to be exported. And in the CoCoSim selection currently I can only export 2 components because it were the ones I've mapped.
However when I go to the Realizability Analysis, I can only "work" with the components It shows in CoCoSim.
Is this because Realizability analysis per default using CoCoSim to proceed, or because I haven't mapped the rest of the components?

I'm trying to understand what the selection of CoCoSim and CoPilot is actually used. I feel that something is not connecting, but is probably just lack of knowledge on my part. Any ideas?

[andreaskatis]

Hi @anaisac ,

Functions and Modes are not supported for realizability checking at the moment, only Input, Output and Internals are meant to be used. If you want to learn more about these two data types, you can read our recent responses on them below:

#126 (comment)

#127 (comment)

Regarding what components are available for realizability checking analysis, only the ones with complete variable information can be considered. "Complete'' means that every variable in your component must have a variable type, a data type and in the case of Internal variables, an assignment expression compatible with Lustre syntax must be given. We only support a subset of possible Lustre expressions (you can see the exact grammar here: https://github.com/NASA-SW-VnV/fret/blob/master/fret-electron/support/LustreExpressionsParser/LustreExpressions.g4 ).

The differentation between CoCoSpec and Copilot should only come to consideration if your intent is to export the requirements into a file that can be used with external tools that support CoCoSpec specifications ([CoCoSim](https://github.com/NASA-SW-VnV/cocosim , Kind 2) or Copilot , respectively.

Best,

Andreas