Realisability Checker Uncaught Exception

[mluckcuck]

I've just tried out the Realisbility Checker on my laptop and had an Uncaught Exception from FRET, not sure what's happened.

I'm running Ubuntu 22.04.5, Node version 20.18.1, and I've got z3 and kind2 (downloaded today), and I tried pulling FRET and it's already up to date.

As you can see form the screenshot, I made a very simple requirements set to try this one, because it did the same thing on a set I already had.

Any ideas what's happened here?

Thanks,
Matt

[mluckcuck]

The screenshot above was from trying in Monolithic mode, it does the same thing in Compositional mode.

Attached is the (simple) requirements and variable mappings.

fretRequirementsVariables.json

[anmavrid]

Thanks, Matt. @andreaskatis is looking into this.

[andreaskatis]

Hi @mluckcuck ,

This issue is related to a bug in Kind2's v2.2.0 release. There are two alternatives to fix it:

1. Downgrade to the previous release of Kind 2, v2.1.1: https://github.com/kind2-mc/kind2/releases/tag/v2.1.1
2. Build Kind 2 from source using the develop branch, which contains a fix.

Please let us know if either of the above works or not.

A couple more notes following from your example and setup:

1. Both requirements are unrealizable. This is because you are trying to enforce the satisfaction of constraints over input variables. Typically, requirements that express expectations over inputs are meant to be declared as assumptions. In order to have the realizability checking analysis consider them as assumptions, you currently need to add the string assumption to the corresponding requirement ID (e.g., change REQ1 to REQ1_assumption).
2. Your version of Node is more recent than the range of versions that we currently know that we support ( v16.16.x - v20.13.1 ). Just pointing it out in case you run into issues that may be related to it, as I do not think that we have tested v20.18.1 (I haven't).

Best Regards,

Andreas

[mluckcuck]

Thanks @andreaskatis (and @anmavrid ) for such a quick reply!

I'll try downgrading Kind2. But I've got the same version on my desktop machine (also Ubuntu 22.04.5 but, oddly, running FRET using Node version 12.22.9!) and a similar set of requirements works ok.

Perhaps it's related to your first note.
I'm actually quite confused by the interaction between the realisability checker and the input/output variables in the variable mapping tab. So for the requirements set I've got here, I had just set them all to Input.
The set on my desktop machine are a mix of inputs and outputs (in a way that seemed sensible to me) so maybe that is why it runs ok and doesn't cause the same exception.

I will go and try downgrading Kind2 and tweaking the variable types on my desktop and let you know.

[mluckcuck]

OK...

On my laptop, swapping to Node version 20.13.1 and then down to version 12.22.9 still cause the same error (with Kind2 unchanged). On my desktop, if I swap the four boolean variables to all be inputs (again, with the same version of Kind2) it does not throw this exception. (At least, I don't get the dialogue box warning me of the uncaught exception, and there is a nice green tick.)

Unfortunately, on my laptop after downgrading to Kind2 version 2.1.1 (and using Node 20.12.1) it still throws the exception.
Again, on my desktop it's still fine.

Please let me know if you need some more information from me about these two setups.

[andreaskatis]

Hi Matt,

Thank you for all the information so far. I would suggest that we focus on issues that come up while only using v2.1.1 or the develop branch for the time being. Kind2's v2.2.0 has a couple of issues which can make things more confusing. One of these is the fact that the JSON output had a change (now reverted on develop) that can lead to wrong results being reported (the "nice green tick" in your comments suggests this, as the specific example is unrealizable). I will talk to the Kind 2 devs about this, to see if there is a more elegant solution to provide, other than asking people to use a different version of the tool.

So far, I have been unable to replicate the unhandled exception error while running 2.1.1, using Node 20.13.1. The example is declared unrealizable (which is the correct result) and the diagnosis completes successfully. This is true for both the compositional and monolithic analysis options.

When you changed versions, did you make sure that the new version is what FRET has access to? This would normally mean that you'd need to update the path to the Kind 2 binary in your PATH environment variable.

Best Regards,

Andreas