search

symphonytool / symphony

The Symphony IDE
5 stars 4 forks source link

Model checker finds deadlock but cannot show counter example #240

Closed pglvdm closed 10 years ago

pglvdm commented 10 years ago

For the BitRegister_MC the model checker finds a deadlock but when you double-click it to see the counter example it gives an error with the message: "Cannot run program "dot": CreateProcess error=2, The system cannot find the file specified. In addition a number of reports are listed in the error log.

adalbertocajueiro commented 10 years ago

That is because the model checker uses a program called (dot), which is included in GraphViz package to build the graph. The program GraphViz is one of the required software to make the model checker feature work. This is pointed out in installation instructions on symphony's documentation. To correct the problem, please install the graphviz software and check is the program "dot" is present in your PATH environment variable.

pglvdm commented 10 years ago

That is correct. I now also has it working. However, it would be beneficial if you would be able to catch the error to explain to the user that access to GraphViz is not there so the user need to install that.

joey-coleman commented 10 years ago

This properly needs a good explanation of what's wrong, not just the generic reference to the missing dot.exe

adalbertocajueiro commented 10 years ago

Updated plugin classes to provide detailed information about installation on auxiliary softwares: FORMULA and GraphViz (that includes dot.exe).