Merge pull request #1442 from informalsystems/gabriela/all-lists-up-to

Introduce `allListsUpTo`

CHANGELOG.md

@@ -11,6 +11,7 @@ and this project adheres to [Semantic Versioning](https://semver.org/spec/v2.0.0
 
 - Added an experimental `--mbt` flag to produce metadata that is useful for
   Model-Based Testing (#1441).
+- Added the `allListsUpTo`, a limited but computable version of `allLists` (#1442)
 
 ### Changed
 

doc/builtin.md

@@ -242,7 +242,7 @@ assert(Set(Set(1, 2), Set(3, 4)).flatten() == Set(1, 2, 3, 4))
 `s.allLists()` is the set of all lists containing elements in `s`.
 This is an infinite set unless `s` is the empty set.
 
-Like other inifite sets, this is not supported in the simulator.
+Like other inifite sets, this is not supported in any execution/verification form.
 
 ### Examples
 
@@ -251,6 +251,15 @@ assert(Set(1, 2).allLists().contains([]))
 assert(Set(1, 2).allLists().contains([1, 1, 1, 1, 2, 1]))
 ```
 
+## `pure def allListsUpTo: (Set[a], int) => Set[List[a]]`
+
+`s.allListsUpTo(l)` is the set of all lists of elements in `s` with length <= `l`
+
+```
+assert(Set(1, 2).allListsUpTo(1) == Set([], [1], [2]))
+assert(Set(1).allListsUpTo(2) == Set([], [1], [1, 1]))
+```
+
 ## `pure def chooseSome: (Set[a]) => a`
 
 `s.chooseSome()` is, deterministically, one element of `s`.

doc/lang.md

@@ -1191,9 +1191,12 @@ powerset(S)
 // UNION S
 S.flatten()
 flatten(S)
-// Seq(S): the set of all lists of elements in S
+// Seq(S): the set of all lists of elements in S.
+// Cannot be used in simulation or verification. See `allListsUpTo`
 S.allLists()
 allLists(S)
+// Limited version:
+S.allListsUpTo(2)
 // CHOOSE x \in S: TRUE
 // The operator name is deliberately made long, so it would not be the user's default choice.
 S.chooseSome()

quint/src/builtin.qnt

@@ -218,7 +218,7 @@ module builtin {
   /// `s.allLists()` is the set of all lists containing elements in `s`.
   /// This is an infinite set unless `s` is the empty set.
   ///
-  /// Like other inifite sets, this is not supported in the simulator.
+  /// Like other inifite sets, this is not supported in any execution/verification form.
   ///
   /// ### Examples
   ///
@@ -228,6 +228,14 @@ module builtin {
   /// ```
   pure def allLists(s): (Set[a]) => Set[List[a]]
 
+  /// `s.allListsUpTo(l)` is the set of all lists of elements in `s` with length <= `l`
+  ///
+  /// ```
+  /// assert(Set(1, 2).allListsUpTo(1) == Set([], [1], [2]))
+  /// assert(Set(1).allListsUpTo(2) == Set([], [1], [1, 1]))
+  /// ```
+  pure def allListsUpTo(s: Set[a], max_length: int): Set[List[a]]
+
   /// `s.chooseSome()` is, deterministically, one element of `s`.
   ///
   /// ### Examples

quint/src/effects/builtinSignatures.ts

@@ -143,6 +143,7 @@ export const setOperators = [
   { name: 'powerset', effect: standardPropagation(1) },
   { name: 'flatten', effect: standardPropagation(1) },
   { name: 'allLists', effect: standardPropagation(1) },
+  { name: 'allListsUpTo', effect: standardPropagation(2) },
   { name: 'chooseSome', effect: standardPropagation(1) },
   { name: 'oneOf', effect: standardPropagation(1) },
   { name: 'isFinite', effect: standardPropagation(1) },

quint/src/ir/quintIr.ts

@@ -132,6 +132,7 @@ export const builtinOpCodes = [
   'actionAll',
   'actionAny',
   'allLists',
+  'allListsUpTo',
   'always',
   'and',
   'append',

quint/src/names/base.ts

@@ -172,6 +172,7 @@ export const builtinNames = [
   'powerset',
   'flatten',
   'allLists',
+  'allListsUpTo',
   'chooseSome',
   'oneOf',
   'isFinite',

quint/src/runtime/impl/compilerImpl.ts

@@ -40,7 +40,7 @@ import { prettyQuintEx, terminalWidth } from '../../graphics'
 import { format } from '../../prettierimp'
 import { unreachable } from '../../util'
 import { zerog } from '../../idGenerator'
-import { chunk } from 'lodash'
+import { chunk, times } from 'lodash'
 
 // Internal names in the compiler, which have special treatment.
 // For some reason, if we replace 'q::input' with inputDefName, everything breaks.
@@ -982,6 +982,25 @@ export class CompilerVisitor implements IRVisitor {
           })
           break
 
+        case 'allListsUpTo':
+          this.applyFun(app.id, 2, (set: RuntimeValue, max_length: RuntimeValue) => {
+            let lists: Set<RuntimeValue[]> = Set([[]])
+            let last_lists: Set<RuntimeValue[]> = Set([[]])
+            times(Number(max_length.toInt())).forEach(_length => {
+              // Generate all lists of length `length` from the set
+              const new_lists: Set<RuntimeValue[]> = set.toSet().flatMap(value => {
+                // for each value in the set, append it to all lists of length `length - 1`
+                return last_lists.map(list => list.concat(value))
+              })
+
+              lists = lists.merge(new_lists)
+              last_lists = new_lists
+            })
+
+            return just(rv.mkSet(lists.map(list => rv.mkList(list)).toOrderedSet()))
+          })
+          break
+
         // standard unary operators that are not handled by REPL
         case 'allLists':
         case 'chooseSome':

quint/src/types/builtinSignatures.ts

@@ -59,6 +59,7 @@ const setOperators = [
   { name: 'powerset', type: '(Set[a]) => Set[Set[a]]' },
   { name: 'flatten', type: '(Set[Set[a]]) => Set[a]' },
   { name: 'allLists', type: '(Set[a]) => Set[List[a]]' },
+  { name: 'allListsUpTo', type: '(Set[a], int) => Set[List[a]]' },
   { name: 'chooseSome', type: '(Set[a]) => a' },
   { name: 'oneOf', type: '(Set[a]) => a' },
   { name: 'isFinite', type: '(Set[a]) => bool' },

quint/test/runtime/compile.test.ts

@@ -853,6 +853,16 @@ describe('compiling specs to runtime values', () => {
       assertResultAsString('[].select(e => e % 2 == 0)', 'List()')
       assertResultAsString('[4, 5, 6].select(e => e % 2 == 0)', 'List(4, 6)')
     })
+
+    it('allListsUpTo', () => {
+      assertResultAsString(
+        'Set(1, 2, 3).allListsUpTo(2)',
+        'Set(List(), List(1, 1), List(1, 2), List(1, 3), List(1), List(2, 1), List(2, 2), List(2, 3), List(2), List(3, 1), List(3, 2), List(3, 3), List(3))'
+      )
+      assertResultAsString('Set(1).allListsUpTo(3)', 'Set(List(), List(1, 1, 1), List(1, 1), List(1))')
+      assertResultAsString('Set().allListsUpTo(3)', 'Set(List())')
+      assertResultAsString('Set(1).allListsUpTo(0)', 'Set(List())')
+    })
   })
 
   describe('compile over records', () => {

quint/testFixture/SuperSpec.qnt

@@ -197,6 +197,9 @@ module withConsts {
   val subseteq_empty = Set().subseteq(Set())
   val powersets = Set(1).in(powerset(Set(1,2,3)))
 
+  // Builting list operators
+  val lists = Set(1, 2).allListsUpTo(3)
+
   // a named assumption
   assume positive = N > 0
   // an anonymous assumption