Model gives different results in GUI/console

[hallba]

Activator-Inhibitor_Oscillations.zip

Tested in GUI with stability analysis and LTL, gives an oscillation

Tested in console gives a fixpoint (i.e. stability) using VMCAI ('C:\Program Files (x86)\BMA\BioCheckConsole.exe' -engine VMCAI -model .\Activator-Inhibitor_Oscillations.json -log).

Oscillations using LTL in console ('C:\Program Files (x86)\BMA\BioCheckConsole.exe' -engine CAV -model .\Activator-Inhibitor_Oscillations.json -log -formula "(Eventually (Oscillation))" -path 10)

[Rachel-Alcraft]

I don't understand this well enough to know what I should see to compare them. I should be comparing the 2nd console inputs to the GUI? The outputs are so different - what would the console show if it was the same as the GUI, or vice versa?

[Rachel-Alcraft]

The problem was that the console uses a fixed version of Microsoft.Z3.dll and the companion libz3.dll - 4.8.4, but the backend uses nuget and was on version 4.11.2.

The prolem only appeared in 4.8.4 so an upgrade to 4.11.2 fixes the problem. The new release will have the same z3 version for console and backend - 4.11.2.

Note for future - the z3 dlls are taken from different places for the standalone console and for the backend, the console copies the dll in from the ext/z3 directory. The backend uses nuget.

In future any nuget version changes mean that the dlls need to be updated in the ext directory. I have updated that directory to include version history and a text file with version comments.