Unsuccessful installation of NuSMV path and the use of realizity use

[baobao1225]

Hello , I am having problems with fret usage. I have installed the binaries of the NuSMV file in the environment variable, but in unbuntu 64-bit, FRET does not find NuSMV, causing SIMULATE to be unusable. I used the same method to be able to use under Windows installation.

Another problem is that when I use the Realizity function, related dependencies have been installed normally, but when I check, solver error occurs, I do not know how to solve it

[matt-knudson]

Hi!
Unfortunately, both of the leads on the FRET project are out of the office. I have successfully implemented FRET on an Ubuntu64 platform, but I am not sure of the problems you are experiencing. I am happy to help as much as I can, but we should probably wait until the lead comes back. I'm sorry you are having trouble!

[andreaskatis]

Hello!

Thank you very much for trying out FRET!

I have installed the binaries of the NuSMV file in the environment variable, but in unbuntu 64-bit, FRET does not find NuSMV, causing SIMULATE to be unusable.

I suspect that this is related to how FRET checks whether NuSMV has been installed. It does so by seeing whether nusmv is available as a command in your system. Our installation instructions for NuSMV lack a step that ensures this is true, by creating a symbolic link called nusmv to the NuSMV binary, and adding the directory that the link resides in to PATH. Please try the following and let us know:

1. Ensure that nusmv is not a command in your system. Try calling it from the terminal and see what it returns
2. If nusmv is indeed not a command, you need to create a symbolic link called nusmv, pointing to the NuSMV binary. The most straightforward way to do this is to go under the directory where your NuSMV binary is, then create the symbolic link using the following command: ln -s /full/path/to/NuSMV/binary nusmv
3. Make sure that the directories where the NuSMV binary and the symbolic link reside in, are in your PATH.
4. Try and run nusmv from the command line, in an arbitrary directory in your system, and ensure that it does call NuSMV (should print the same output as if you were to run the NuSMV binary directly).
5. Open FRET and see if the problem is fixed (the SIMULATE button should become available for a valid FRETish requirement).

Another problem is that when I use the Realizability function, related dependencies have been installed normally, but when I check, solver error occurs, I do not know how to solve it.

This is the default behavior when something goes wrong in the underlying solvers that the realizability check utilizes. To be able to further assist you on this, we need an example. Before submitting an example, please make sure that you have removed any sensitive information from your requirements (including project and component names). The steps are the following:

1. Try to minimize the number of requirements that expose this behavior (perhaps by creating a new FRET project where you liberally add and delete requirements from the original project).
2. Run FRET using npm run dev, instead of npm start
3. Attempt to perform the realizability check on your example, then wait for the "SOLVER ERROR" result.
4. In your system, navigate under /Documents/fret-analysis
5. Add ALL the files whose name is prefixed by the FRET System Component that you tried realizability on in a .zip folder
6. Attach the .zip folder in a new post in this thread.

[baobao1225]

Thank for your answer! I write a simple requirement,but the solver error still occurs
RESULT.zip

[andreaskatis]

Glad to help! Did you mean to close the issue? Did you get the SIMULATE button to work?

As for realizability checking, the issue is the name of the requirement. As it currently stands, JKind, the tool that is used for realizability under the hood does not accept plain numbers as identifiers. Try to rename your requirement by adding at least one letter, or the symbol "_". This should fix the problem.

[andreaskatis]

Reopening this until both issues are properly addressed on our end.

[baobao1225]

Thank you a lot! I solve all the question.

[andreaskatis]

Glad to help, please let us know if you have any further issues.

I will re-open this issue though, as it helps us towards tracking current issues that can be fixed or improved with future versions of FRET. We will close it some time in the future, with a commit that better addresses these issues.

[anmavrid]

Internal JIRA issues for further improvement are created. Closing this issue.