Add generate operator

[konnov]

Hello !

I would like to add an experimental contribution, namely, the operator generate that mirrors Apalache!Gen. This operator should unlock the feature of Apalache that is sometimes used to reason about inductive invariants. This PR:

• adds the operator generate
• adds an error for generate in the simulator, as it is not clear to me how one would implement that in the simulator
• prepares the ground for translation in Apalache, see Translate Quint generate apalache-mc/apalache#2916
• Tests added for any new code
• Entries added to the respective CHANGELOG.md for any new functionality

[netlify]

❌ Deploy Preview for quint-docs failed. Why did it fail? →

Name	Link
🔨 Latest commit	4df3ae5
🔍 Latest deploy log	https://app.netlify.com/sites/quint-docs/deploys/667da4508e7f2d00083bd613

[bugarela]

Hi! Thanks Igor, I'll take a look when I can.

Please ignore the Netlify bot, I'm still not done setting it up

[bugarela]

Hey @konnov, I finally took a look at these and I feel like I need more context here. I don't think the name "generate" is very informative, and maybe we should have something more tuned to the particular use case where it is necessary.

A couple of months ago, I introduced an operator called allListsUpTo #1442 (that only works on the simulator). Do you think that we can approach this by adding an allSetsUpTo and mapping those into Apalache!Gen calls on the Apalache side? Or did I misunderstood this and it should do something completely different?

[konnov]

Hey @konnov, I finally took a look at these and I feel like I need more context here. I don't think the name "generate" is very informative, and maybe we should have something more tuned to the particular use case where it is necessary.

A couple of months ago, I introduced an operator called allListsUpTo #1442 (that only works on the simulator). Do you think that we can approach this by adding an allSetsUpTo and mapping those into Apalache!Gen calls on the Apalache side? Or did I misunderstood this and it should do something completely different?

Hey @bugarela, yeah, I can see how generate could be confusing. However, it's kind of similar to the generators in property-based testing. It simply generates a value of the proper type (given by the example) that has up to a given number of elements, in case it is a non-scalar type such as a set or a list. The difference from PBT is that generation does not happen at random, but is done by the solver. I can see how using a set instead of a single element could be easier to understand for the people who know TLA+. However, the way generate works now is more in line with oneOf, which could be also expressed as a quantifier over a set

[bugarela]

Ok, so that makes me even more in favor of having the current:

nondet a = Int.allListsUpTo(10).oneOf()

and, in addition, the Set version:

nondet a = Int.allSetsUpTo(10).oneOf()

I'm using the infinite set Int in these examples because iiuc that's the behavior of Apalache!Gen. Could we also use Apalache!Gen for a bounded set like Set(1,2,3).allListsUpTo(10).oneOf()? If not, is it feasible to use a filter, like the equivalent of Int.allSetsUpTo(10).filter(s => s.in(Set(1,2,3))).oneOf()? We could take care of that during the conversion to Apalache IR

[konnov]

Well, this would definitely play nice for the set of all integers, as it is a built-in set. Imagine you would like to generate a set of structures, e.g., of the shape { x: Set[int], y: int -> bool }. Now, if you would like to pass a set, you are basically replacing the type with the set. It's very much what TLA+ people are doing when they are writing TypeOK. However, this approach does not play well with Apalache, as it sometimes starts to unfold the sets. This is exactly what we are trying to avoid with Apalache!Gen.

[bugarela]

I have to thoughts here:

1. The most natural way for a non TLA+ expert to write this would probably be

nondet size = 0.to(10).oneOf()
0.to(size).map(_ =>
  nondet x = Int.oneOf()
  nondet y = setOfMaps(Int, Bool).oneOf()
  { x: x, y: y }
)

Of course, this doesn't work. But I'd like to try and get closer to this intuition than introducing a magical generate operator. Even if that means adding a keyword.

2. We shouldn't require users to write a dummy value like { x: Set(0), y: Map(0 -> false) }. I'd rather require a type annotation, since Quint is a typed language.

[konnov]

I have to thoughts here:

1. The most natural way for a non TLA+ expert to write this would probably be

nondet size = 0.to(10).oneOf()
0.to(size).map(_ =>
  nondet x = Int.oneOf()
  nondet y = setOfMaps(Int, Bool).oneOf()
  { x: x, y: y }
)

This looks really complicated. I agree that this is similar to how one would do it in a property-based framework, since most of them are functional. However, we don't have to do complicated things just because someone did them in the past. Thinking about with a fresh head, I would say that the most natural way for a non-TLA+ person to write this would be something like:

fresh a: { x: Set[int], y: int -> bool } up to 10

I am kind of making up keywords here. The point is that we essentially have to declare a fresh variable and limit its scope.

Of course, this doesn't work. But I'd like to try and get closer to this intuition than introducing a magical generate operator. Even if that means adding a keyword.

2. We shouldn't require users to write a dummy value like { x: Set(0), y: Map(0 -> false) }. I'd rather require a type annotation, since Quint is a typed language.

Yes, this would be great. As an alternative, we could have this form:

nondet a: { x: Set[int], y: int -> bool } = generate(10)

[konnov]

bumped the version of apalache to 0.45.3

[konnov]

Hey @bugarela! Any thoughts on this feature? I really need something like to work on an inductive invariant, see example.

[bugarela]

Hi! I guess we agreed on a solution at the end of the last discussion. However, I'm having trouble picturing the use case for this and therefore assessing the priority here, as this doesn't seem trivial to implement.

IIRC, we talked over zoom and you said you'd try to come up with an example to demonstrate where you need this. Are you still willing to do this? We could also jump into a call sometime, whatever works best.

[konnov]

Hi! I guess we agreed on a solution at the end of the last discussion. However, I'm having trouble picturing the use case for this and therefore assessing the priority here, as this doesn't seem trivial to implement.

IIRC, we talked over zoom and you said you'd try to come up with an example to demonstrate where you need this. Are you still willing to do this? We could also jump into a call sometime, whatever works best.

There is a link to the WIP example in my reply. Sure, happy to jump on a call!

[konnov]

@bugarela I have just described the need for value generators in detail in Apalache: apalache-mc/apalache#3014

I agree that what we currently have in Apalache is a hack, though it's hard to tell how long it would take to implement a better version (proposed there).