Solver Error in Realizability Checking

[abakst]

Hi all,

I'm experimenting with FRET, and running into trouble using the realizability checker. When I try to run the checker on a component, I only see "SOLVER ERROR," but no other output to help me diagnose the problem.

I think I've installed all the dependencies, but it's possible something is misconfigured.

Do you have any ideas for what I might try to narrow down the problem? That could be additional flags, debug print statements, etc.

[abakst]

I've discovered that some of the components are in fact checkable (the solver appears to run successfully).

[andreaskatis]

Hello Alexander,

The SOLVER ERROR message is not related to installation issues, but to problems with the input file to JKind. This can happen due to a misconfiguration in Variable Mapping or some, unknown yet to us, bug.

One way we can help is if you can provide us with an example set of requirements that causes this issue, along with the variable mapping table for the system component.

We are also planning in the future to provide an option in the GUI to retain files that were generated for JKind, for debugging purposes. If the previous suggestion is not an option, the next best that you can try and do is to try and run the realizability check from the command line.

To do so, try to start FRET in developer mode using npm run dev instead of npm start and run the analysis as normal.
After you get the error, you can find the JKind input under Documents/fret-analysis. It should be named name_of_component.lus. If you are under the compositional mode, then the name will be name_of_component_ccX.lus, where X will be the index value of the corresponding connected component from the GUI. You can then try and run JKind from the command line using jrealizability -fixpoint name_of_component.lus and observe the exact error message.

If you can share with us this error message, I will be glad to point out what may have gone wrong in your case.

[abakst]

Aha! Thank you. It looks like it was a parse error:

Parse error line 85:64 no viable alternative at input '->'
Actuate_Device_0 = (H((( ( Set_Actuate_0 or Manual_Actuate_0 ) <-> Actuate_0 ))));

I'm not so familiar with Lustre, but is it the case that there is no builtin if-and-only-if? Of course I can rewrite the requirement, so I'm just curious.

[andreaskatis]

Right, it seems that <-> is not properly translated for Lustre. Thank you for bringing this up, as it does seem to be a bug.

For now, you can use the equality symbol = for such cases at the FRETish level.

Thank you for using FRET! We will be more than glad to answer questions or assist with future issues.