Translate Quint generate
#2916
Translate Quint generate
#2916
Conversation
|
Hey @bugarela, is there any chance I would be able to get a review? It would be great if I could call Apalache from quint without relying on a fork |
|
@konnov Ah, sorry, I missed this one. So is this why the PR on the Quint side has a failing test? I saw that PR and thought it was still WIP due to the failing test. I'll take a look at both of them still this week! |
I guess, Quint is failing as it is picking up the older version of Apalache. |
| val elemType = typeConv.convert(types(id).typ) | ||
| val boundIntConst = intFromExpr(bound) | ||
| if (boundIntConst.isEmpty) { | ||
| throw new QuintIRParseError(s"nondet $name = generate($bound) ... expects an integer constant") |
There was a problem hiding this comment.
There is a nested expression under nondet
There was a problem hiding this comment.
Yeah, but it's not relevant for the error here, so at best it will confuse.
Also, afaiu there's a second parameter to generate()? So ellipses inside the parentheses make more sense to me.
This PR adds translation of Quint
generateintroduced in informalsystems/quint#1455 intoApalache!Gen../unreleased/for any new functionality