Merge branch 'main' into th/vsc-complete

.github/workflows/main.yml

@@ -31,18 +31,21 @@ jobs:
 
   quint-vscode-linting:
     runs-on: ubuntu-latest
-    defaults:
-      run:
-        working-directory: ./vscode/quint-vscode
     strategy:
       fail-fast: false
     steps:
       - uses: actions/checkout@v2
       - uses: actions/setup-node@v2
         with:
           node-version: "18"
-      - run: npm install
-      - run: npm run format-check || (echo "Run 'npm run format'" && exit 1)
+      - name: Install quint deps
+        run: cd ./quint && npm install
+      - name: Install yalc
+        run: npm i yalc -g
+      - name: Compile quint vscode plugin
+        run: make local
+      - name: Run formatting for the plugin
+        run: cd ./vscode/quint-vscode && npm run format-check || (echo "Run 'npm run format'" && exit 1)
 
   quint-unit-tests:
     runs-on: ${{ matrix.operating-system }}

CHANGELOG.md

@@ -13,9 +13,19 @@ and this project adheres to [Semantic Versioning](https://semver.org/spec/v2.0.0
   through Apalache (#1154)
 
 ### Changed
+
+- Introduce frames on actions in the verbose output. The verbose output has changed! (#1158)
+- The ITF traces always serialize integers as `{ '#bigint': 'num }`  (#1165)
+
 ### Deprecated
 ### Removed
 ### Fixed
+
+- Fixed a problem where an error was thrown when a name from an importing module
+  shadowed a nested name from the imported module (#802)
+- Fixed a problem where tests were ignored if they are not defined directly in
+  the main module - that is, they were imported (#1161)
+
 ### Security
 
 ## v0.14.2 -- 2023-09-06

quint/io-cli-tests.md

@@ -298,6 +298,34 @@ exit $exit_code
       HOME/failingTestCounters.qnt
 ```
 
+### Tests are found even if they are imported in the main module
+
+<!-- !test exit 0 -->
+<!-- !test in tests are found -->
+```
+output=$(quint test --max-samples=10 --main TendermintModels ../examples/cosmos/tendermint/TendermintModels.qnt)
+exit_code=$?
+echo "$output" | sed -e 's/([0-9]*ms)/(duration)/g'
+exit $exit_code
+```
+
+<!-- !test out tests are found -->
+```
+
+  TendermintModels
+    ok TendermintModels::n4_f1::decisionTest passed 10 test(s)
+    ok TendermintModels::n4_f1::noProposeTwiceTest passed 10 test(s)
+    ok TendermintModels::n4_f1::timeoutProposeTest passed 10 test(s)
+    ok TendermintModels::n4_f2::decisionTest passed 10 test(s)
+    ok TendermintModels::n4_f2::noProposeTwiceTest passed 10 test(s)
+    ok TendermintModels::n4_f2::timeoutProposeTest passed 10 test(s)
+    ok TendermintModels::n5_f2::decisionTest passed 10 test(s)
+    ok TendermintModels::n5_f2::noProposeTwiceTest passed 10 test(s)
+    ok TendermintModels::n5_f2::timeoutProposeTest passed 10 test(s)
+
+  9 passing (duration)
+```
+
 ### test counters produces no execution
 
 `test` should handle the special case of when an execution has not been
@@ -325,7 +353,10 @@ exit $exit_code
       45:          assert(n == 0),
 
 [Frame 0]
-init() => true
+init => true
+
+[Frame 1]
+_ => none
 
     Use --seed=0x1 --match=failingTest to repeat.
 ```
@@ -496,9 +527,9 @@ exit $exit_code
 An example execution:
 
 [Frame 0]
-q::initAndInvariant() => true
-├─ q::init() => true
-│  └─ init() => true
+q::initAndInvariant => true
+├─ q::init => true
+│  └─ init => true
 └─ isUInt(0) => true
 
 [State 0]
@@ -509,9 +540,9 @@ q::initAndInvariant() => true
 }
 
 [Frame 1]
-q::stepAndInvariant() => true
-├─ q::step() => true
-│  └─ step() => true
+q::stepAndInvariant => true
+├─ q::step => true
+│  └─ step => true
 │     └─ mint(
 │          "bob",
 │          "null",
@@ -541,9 +572,9 @@ q::stepAndInvariant() => true
 }
 
 [Frame 2]
-q::stepAndInvariant() => true
-├─ q::step() => true
-│  └─ step() => true
+q::stepAndInvariant => true
+├─ q::step => true
+│  └─ step => true
 │     └─ send(
 │          "null",
 │          "charlie",
@@ -578,9 +609,9 @@ q::stepAndInvariant() => true
 }
 
 [Frame 3]
-q::stepAndInvariant() => true
-├─ q::step() => true
-│  └─ step() => true
+q::stepAndInvariant => true
+├─ q::step => true
+│  └─ step => true
 │     └─ mint(
 │          "bob",
 │          "bob",
@@ -632,7 +663,9 @@ rm out-itf-example.itf.json
 ```
 [
   "alice",
-  0
+  {
+    "#bigint": "0"
+  }
 ]
 ```
 
@@ -665,27 +698,66 @@ exit $exit_code
 [
   [
     "alice",
-    0
+    {
+      "#bigint": "0"
+    }
   ],
   [
     "bob",
-    0
+    {
+      "#bigint": "0"
+    }
   ],
   [
     "charlie",
-    0
+    {
+      "#bigint": "0"
+    }
   ],
   [
     "eve",
-    0
+    {
+      "#bigint": "0"
+    }
   ],
   [
     "null",
-    0
+    {
+      "#bigint": "0"
+    }
   ]
 ]
 ```
 
+### Test does not skip assignments (#1133)
+
+See: https://github.com/informalsystems/quint/issues/1133
+
+FIXME: fix the traces found by the simulator once #1133 is resolved.
+
+<!-- !test in test1133 -->
+```
+output=$(quint test --match='(t1|t2)' --output='out_{#}_{}.itf.json' \
+  ./testFixture/simulator/lastActionInRun.qnt)
+exit_code=$?
+echo "BEGIN"
+# This test should have 3 states (FIXME: it does not!)
+cat out_0_t1.itf.json | jq '.states' | grep "s" | wc -l | grep 3
+rm out_0_t1.itf.json
+# This test should have 4 states (FIXME: it does not!)
+cat out_1_t2.itf.json | jq '.states' | grep "s" | wc -l | grep 4
+rm out_1_t2.itf.json
+echo "END"
+exit $exit_code
+```
+
+<!-- !test out test1133 -->
+```
+BEGIN
+END
+```
+FIX THE TEST ABOVE: it should have 3 and 4
+
 ### OK REPL tutorial
 
 The REPL tutorial is reproducible in REPL.
@@ -722,7 +794,7 @@ exit $exit_code
       176:     run mintTwiceThenSendError = {
 
 [Frame 0]
-init() => true
+init => true
 
 [Frame 1]
 mint(

quint/src/cliCommands.ts

@@ -26,9 +26,9 @@ import {
 
 import { Either, left, right } from '@sweet-monads/either'
 import { EffectScheme } from './effects/base'
-import { LookupTable } from './names/base'
+import { LookupTable, UnusedDefinitions } from './names/base'
 import { ReplOptions, quintRepl } from './repl'
-import { OpQualifier, QuintEx, QuintModule } from './ir/quintIr'
+import { OpQualifier, QuintEx, QuintModule, QuintOpDef, qualifier } from './ir/quintIr'
 import { TypeScheme } from './types/base'
 import lineColumn from 'line-column'
 import { formatError } from './errorReporter'
@@ -55,6 +55,7 @@ interface OutputStage {
   // the modules and the lookup table produced by 'parse'
   modules?: QuintModule[]
   table?: LookupTable
+  unusedDefinitions?: UnusedDefinitions
   // the tables produced by 'typecheck'
   types?: Map<bigint, TypeScheme>
   effects?: Map<bigint, EffectScheme>
@@ -80,6 +81,7 @@ const pickOutputStage = ({
   warnings,
   modules,
   table,
+  unusedDefinitions,
   types,
   effects,
   errors,
@@ -95,6 +97,7 @@ const pickOutputStage = ({
     warnings,
     modules,
     table,
+    unusedDefinitions,
     types,
     effects,
     errors,
@@ -121,6 +124,7 @@ interface ParsedStage extends LoadedStage {
   modules: QuintModule[]
   sourceMap: Map<bigint, Loc>
   table: LookupTable
+  unusedDefinitions: UnusedDefinitions
   idGen: IdGenerator
 }
 
@@ -331,6 +335,37 @@ export async function runTests(prev: TypecheckedStage): Promise<CLIProcedure<Tes
       }
     },
   }
+
+  // Find tests that are not used in the main module. We need to add references to them in the main module so flattening
+  // doesn't drop the definitions.
+  const unusedTests = [...testing.unusedDefinitions(mainName)].filter(
+    d => d.kind === 'def' && options.testMatch(d.name)
+  )
+
+  // Define name expressions referencing each test that is not referenced elsewhere, adding the references to the lookup
+  // table
+  const args: QuintEx[] = unusedTests.map(defToAdd => {
+    const id = testing.idGen.nextId()
+    testing.table.set(id, defToAdd)
+    const namespace = defToAdd.importedFrom ? qualifier(defToAdd.importedFrom) : undefined
+    const name = namespace ? [namespace, defToAdd.name].join('::') : defToAdd.name
+
+    return { kind: 'name', id, name }
+  })
+
+  // Wrap all expressions in a single declaration
+  const testDeclaration: QuintOpDef = {
+    id: testing.idGen.nextId(),
+    name: 'q::unitTests',
+    kind: 'def',
+    qualifier: 'run',
+    expr: { kind: 'app', opcode: 'actionAll', args, id: testing.idGen.nextId() },
+  }
+
+  // Add the declaration to the main module
+  const main = testing.modules.find(m => m.name === mainName)
+  main?.declarations.push(testDeclaration)
+
   const analysisOutput = { types: testing.types, effects: testing.effects, modes: testing.modes }
   const { flattenedModules, flattenedTable, flattenedAnalysis } = flattenModules(
     testing.modules,

quint/src/flattening/fullFlattener.ts

@@ -22,6 +22,7 @@ import { AnalysisOutput } from '../quintAnalyzer'
 import { inlineTypeAliases } from '../types/aliasInliner'
 import { flattenModule } from './flattener'
 import { flattenInstances } from './instanceFlattener'
+import { unshadowNames } from '../names/unshadower'
 
 /**
  * Flatten an array of modules, replacing instances, imports and exports with
@@ -45,8 +46,11 @@ export function flattenModules(
   // FIXME: use copies of parameters so the original objects are not mutated.
   // This is not a problem atm, but might be in the future.
 
+  // Use unique names when there is shadowing
+  const modulesWithUniqueNames = modules.map(m => unshadowNames(m, table))
+
   // Inline type aliases
-  const inlined = inlineTypeAliases(modules, table, analysisOutput)
+  const inlined = inlineTypeAliases(modulesWithUniqueNames, table, analysisOutput)
 
   const modulesByName = new Map(inlined.modules.map(m => [m.name, m]))
 

quint/src/graphics.ts

@@ -267,7 +267,8 @@ export function printExecutionFrameRec(box: ConsoleBox, frame: ExecutionFrame, i
   box.out(treeArt)
 
   // format the call with its arguments and place it right after the tree art
-  const argsDoc = group(textify(['(', nest('  ', [linebreak, group(args)]), linebreak, ')']))
+  let argsDoc =
+    frame.args.length === 0 ? text('') : group(textify(['(', nest('  ', [linebreak, group(args)]), linebreak, ')']))
   // draw proper branches in the indentation
   const indentTreeArt = isLast.map(il => (il ? '   ' : '│  ')).join('')
   // pretty print the arguments and the result

quint/src/itf.ts

@@ -71,9 +71,6 @@ function isUnserializable(v: ItfValue): v is ItfUnserializable {
   return (v as ItfUnserializable)['#unserializable'] !== undefined
 }
 
-const minJsInt: bigint = BigInt(Number.MIN_SAFE_INTEGER)
-const maxJsInt: bigint = BigInt(Number.MAX_SAFE_INTEGER)
-
 /**
  * Convert a list of Quint expressions into an object that matches the JSON
  * representation of the ITF trace. This function does not add metadata
@@ -87,13 +84,8 @@ export function toItf(vars: string[], states: QuintEx[]): Either<string, ItfTrac
   const exprToItf = (ex: QuintEx): Either<string, ItfValue> => {
     switch (ex.kind) {
       case 'int':
-        if (ex.value >= minJsInt && ex.value <= maxJsInt) {
-          // We can represent safely as a JS number
-          return right(Number(ex.value))
-        } else {
-          // convert to a special structure, when saving to JSON
-          return right({ '#bigint': `${ex.value}` })
-        }
+        // convert to a special structure, when saving to JSON
+        return right({ '#bigint': `${ex.value}` })
 
       case 'str':
       case 'bool':
@@ -189,12 +181,16 @@ export function ofItf(itf: ItfTrace): QuintEx[] {
       return { id, kind: 'bool', value }
     } else if (typeof value === 'string') {
       return { id, kind: 'str', value }
+    } else if (isBigint(value)) {
+      // this is the standard way of encoding an integer in ITF.
+      return { id, kind: 'int', value: BigInt(value['#bigint']) }
     } else if (typeof value === 'number') {
+      // We never encode an integer as a JS number,
+      // but we consume it for backwards compatibility with older ITF traces.
+      // See: https://apalache.informal.systems/docs/adr/015adr-trace.html
       return { id, kind: 'int', value: BigInt(value) }
     } else if (Array.isArray(value)) {
       return { id, kind: 'app', opcode: 'List', args: value.map(ofItfValue) }
-    } else if (isBigint(value)) {
-      return { id, kind: 'int', value: BigInt(value['#bigint']) }
     } else if (isTup(value)) {
       return { id, kind: 'app', opcode: 'Tup', args: value['#tup'].map(ofItfValue) }
     } else if (isSet(value)) {