Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

quint verify fails with error 13 on a relatively small spec #1464

Open
konnov opened this issue Jul 23, 2024 · 1 comment
Open

quint verify fails with error 13 on a relatively small spec #1464

konnov opened this issue Jul 23, 2024 · 1 comment

Comments

@konnov
Copy link
Contributor

konnov commented Jul 23, 2024

I have a MWE t.qnt (see below). Quint fails on it like this:

$ quint verify --invariant=inv t.qnt
13:57:49.505 [main] INFO at.forsyte.apalache.tla.tooling.opt.ServerCmd -- Loading configuration
# Usage statistics is OFF. We care about your privacy.
# If you want to help our project, consider enabling statistics with config --enable-stats=true.

Output directory: /Users/igor/Downloads/_apalache-out/server/2024-07-23T13-57-49_7159912221971505750
# APALACHE version: 0.44.11 | build: 5dee24e                      I@13:57:49.677
Starting server on port 8822...                                   I@13:57:49.681
The Apalache server is running on port 8822. Press Ctrl-C to stop.
PASS #0: SanyParser                                               I@13:57:50.450
quint verify <input>

Verify a Quint specification via Apalache

Options:
[...]

Error: 13 INTERNAL: 
    at callErrorFromStatus (/Users/igor/devl/quint/quint/node_modules/@grpc/grpc-js/build/src/call.js:31:19)
    at Object.onReceiveStatus (/Users/igor/devl/quint/quint/node_modules/@grpc/grpc-js/build/src/client.js:192:76)
    at Object.onReceiveStatus (/Users/igor/devl/quint/quint/node_modules/@grpc/grpc-js/build/src/client-interceptors.js:360:141)
    at Object.onReceiveStatus (/Users/igor/devl/quint/quint/node_modules/@grpc/grpc-js/build/src/client-interceptors.js:323:181)
    at /Users/igor/devl/quint/quint/node_modules/@grpc/grpc-js/build/src/resolving-call.js:99:78
    at process.processTicksAndRejections (node:internal/process/task_queues:77:11)
for call at
    at ServiceClientImpl.makeUnaryRequest (/Users/igor/devl/quint/quint/node_modules/@grpc/grpc-js/build/src/client.js:160:32)
    at ServiceClientImpl.run (/Users/igor/devl/quint/quint/node_modules/@grpc/grpc-js/build/src/make-client.js:105:19)
    at Object.<anonymous> (/Users/igor/devl/quint/quint/dist/src/apalache.js:219:55)
    at node:internal/util:360:7
    at new Promise (<anonymous>)
    at Object.run (node:internal/util:346:12)
    at Object.check (/Users/igor/devl/quint/quint/dist/src/apalache.js:147:28)
    at /Users/igor/devl/quint/quint/dist/src/quintVerifier.js:32:53
    at EitherConstructor.asyncChain (/Users/igor/devl/quint/quint/node_modules/@sweet-monads/either/cjs/index.js:125:16)
    at verify (/Users/igor/devl/quint/quint/dist/src/quintVerifier.js:32:29) {
  code: 13,
  details: '',
  metadata: Metadata { internalRepr: Map(0) {}, options: {} }
}

The spec is actually relatively small:

module t {
  var ms: Set[str]

  action init = {
    nondet ms0 = LARGE_SET.oneOf()
    ms' = ms0
  }

  action step = {
    nondet ms0 = LARGE_SET.oneOf()
    ms' = ms0
  }

  val inv = {
    ms.size() >= 9
  }

  pure val LARGE_SET: Set[Set[str]] =
    Set(
      Set("aa1", "aa10", "aa11", "aa12", "aa2", "aa3", "aa4", "aa5", "aa6", "aa7", "aa8", "aa9"),
      Set("aa1", "aa10", "aa11", "aa12", "aa2", "aa3", "aa4", "aa5", "aa6", "aa7", "aa8"),
      Set("aa1", "aa10", "aa11", "aa12", "aa2", "aa3", "aa4", "aa5", "aa6", "aa7", "aa9"),
      Set("aa1", "aa10", "aa11", "aa12", "aa2", "aa3", "aa4", "aa5", "aa6", "aa7"),
      Set("aa1", "aa10", "aa11", "aa12", "aa2", "aa3", "aa4", "aa5", "aa6", "aa8", "aa9"),
      Set("aa1", "aa10", "aa11", "aa12", "aa2", "aa3", "aa4", "aa5", "aa6", "aa8"),
      Set("aa1", "aa10", "aa11", "aa12", "aa2", "aa3", "aa4", "aa5", "aa6", "aa9"),
      Set("aa1", "aa10", "aa11", "aa12", "aa2", "aa3", "aa4", "aa5", "aa6"),
      Set("aa1", "aa10", "aa11", "aa12", "aa2", "aa3", "aa4", "aa5", "aa7", "aa8", "aa9"),
      Set("aa1", "aa10", "aa11", "aa12", "aa2", "aa3", "aa4", "aa5", "aa7", "aa8"),
      Set("aa1", "aa10", "aa11", "aa12", "aa2", "aa3", "aa4", "aa5", "aa7", "aa9"),
      Set("aa1", "aa10", "aa11", "aa12", "aa2", "aa3", "aa4", "aa5", "aa7"),
      Set("aa1", "aa10", "aa11", "aa12", "aa2", "aa3", "aa4", "aa5", "aa8", "aa9"),
      Set("aa1", "aa10", "aa11", "aa12", "aa2", "aa3", "aa4", "aa5", "aa8"),
      Set("aa1", "aa10", "aa11", "aa12", "aa2", "aa3", "aa4", "aa5", "aa9"),
      Set("aa1", "aa10", "aa11", "aa12", "aa2", "aa3", "aa4", "aa6", "aa7", "aa8", "aa9"),
      Set("aa1", "aa10", "aa11", "aa12", "aa2", "aa3", "aa4", "aa6", "aa7", "aa8"),
      Set("aa1", "aa10", "aa11", "aa12", "aa2", "aa3", "aa4", "aa6", "aa7", "aa9"),
      Set("aa1", "aa10", "aa11", "aa12", "aa2", "aa3", "aa4", "aa6", "aa7"),
      Set("aa1", "aa10", "aa11", "aa12", "aa2", "aa3", "aa4", "aa6", "aa8", "aa9"),
      Set("aa1", "aa10", "aa11", "aa12", "aa2", "aa3", "aa4", "aa6", "aa8"),
      Set("aa1", "aa10", "aa11", "aa12", "aa2", "aa3", "aa4", "aa6", "aa9"),
      Set("aa1", "aa10", "aa11", "aa12", "aa2", "aa3", "aa4", "aa7", "aa8", "aa9"),
      Set("aa1", "aa10", "aa11", "aa12", "aa2", "aa3", "aa4", "aa7", "aa8"),
      Set("aa1", "aa10", "aa11", "aa12", "aa2", "aa3", "aa4", "aa7", "aa9"),
      Set("aa1", "aa10", "aa11", "aa12", "aa2", "aa3", "aa4", "aa8", "aa9"),
      Set("aa1", "aa10", "aa11", "aa12", "aa2", "aa3", "aa5", "aa6", "aa7", "aa8", "aa9"),
      Set("aa1", "aa10", "aa11", "aa12", "aa2", "aa3", "aa5", "aa6", "aa7", "aa8"),
      Set("aa1", "aa10", "aa11", "aa12", "aa2", "aa3", "aa5", "aa6", "aa7", "aa9"),
      Set("aa1", "aa10", "aa11", "aa12", "aa2", "aa3", "aa5", "aa6", "aa7"),
      Set("aa1", "aa10", "aa11", "aa12", "aa2", "aa3", "aa5", "aa6", "aa8", "aa9"),
      Set("aa1", "aa10", "aa11", "aa12", "aa2", "aa3", "aa5", "aa6", "aa8"),
      Set("aa1", "aa10", "aa11", "aa12", "aa2", "aa3", "aa5", "aa6", "aa9"),
      Set("aa1", "aa10", "aa11", "aa12", "aa2", "aa3", "aa5", "aa7", "aa8", "aa9"),
      Set("aa1", "aa10", "aa11", "aa12", "aa2", "aa3", "aa5", "aa7", "aa8"),
      Set("aa1", "aa10", "aa11", "aa12", "aa2", "aa3", "aa5", "aa7", "aa9"),
      Set("aa1", "aa10", "aa11", "aa12", "aa2", "aa3", "aa5", "aa8", "aa9"),
      Set("aa1", "aa10", "aa11", "aa12", "aa2", "aa3", "aa6", "aa7", "aa8", "aa9"),
      Set("aa1", "aa10", "aa11", "aa12", "aa2", "aa3", "aa6", "aa7", "aa8"),
      Set("aa1", "aa10", "aa11", "aa12", "aa2", "aa3", "aa6", "aa7", "aa9"),
      Set("aa1", "aa10", "aa11", "aa12", "aa2", "aa3", "aa6", "aa8", "aa9"),
      Set("aa1", "aa10", "aa11", "aa12", "aa2", "aa3", "aa7", "aa8", "aa9"),
      Set("aa1", "aa10", "aa11", "aa12", "aa2", "aa4", "aa5", "aa6", "aa7", "aa8", "aa9"),
      Set("aa1", "aa10", "aa11", "aa12", "aa2", "aa4", "aa5", "aa6", "aa7", "aa8"),
      Set("aa1", "aa10", "aa11", "aa12", "aa2", "aa4", "aa5", "aa6", "aa7", "aa9"),
      Set("aa1", "aa10", "aa11", "aa12", "aa2", "aa4", "aa5", "aa6", "aa7"),
      Set("aa1", "aa10", "aa11", "aa12", "aa2", "aa4", "aa5", "aa6", "aa8", "aa9"),
      Set("aa1", "aa10", "aa11", "aa12", "aa2", "aa4", "aa5", "aa6", "aa8"),
      Set("aa1", "aa10", "aa11", "aa12", "aa2", "aa4", "aa5", "aa6", "aa9"),
      Set("aa1", "aa10", "aa11", "aa12", "aa2", "aa4", "aa5", "aa7", "aa8", "aa9"),
      Set("aa1", "aa10", "aa11", "aa12", "aa2", "aa4", "aa5", "aa7", "aa8"),
      Set("aa1", "aa10", "aa11", "aa12", "aa2", "aa4", "aa5", "aa7", "aa9"),
      Set("aa1", "aa10", "aa11", "aa12", "aa2", "aa4", "aa5", "aa8", "aa9"),
      Set("aa1", "aa10", "aa11", "aa12", "aa2", "aa4", "aa6", "aa7", "aa8", "aa9"),
      Set("aa1", "aa10", "aa11", "aa12", "aa2", "aa4", "aa6", "aa7", "aa8"),
      Set("aa1", "aa10", "aa11", "aa12", "aa2", "aa4", "aa6", "aa7", "aa9"),
      Set("aa1", "aa10", "aa11", "aa12", "aa2", "aa4", "aa6", "aa8", "aa9"),
      Set("aa1", "aa10", "aa11", "aa12", "aa2", "aa4", "aa7", "aa8", "aa9"),
      Set("aa1", "aa10", "aa11", "aa12", "aa2", "aa5", "aa6", "aa7", "aa8", "aa9"),
      Set("aa1", "aa10", "aa11", "aa12", "aa2", "aa5", "aa6", "aa7", "aa8"),
      Set("aa1", "aa10", "aa11", "aa12", "aa2", "aa5", "aa6", "aa7", "aa9"),
      Set("aa1", "aa10", "aa11", "aa12", "aa2", "aa5", "aa6", "aa8", "aa9"),
      Set("aa1", "aa10", "aa11", "aa12", "aa2", "aa5", "aa7", "aa8", "aa9"),
      Set("aa1", "aa10", "aa11", "aa12", "aa2", "aa6", "aa7", "aa8", "aa9"),
      Set("aa1", "aa10", "aa11", "aa12", "aa3", "aa4", "aa5", "aa6", "aa7", "aa8", "aa9"),
      Set("aa1", "aa10", "aa11", "aa12", "aa3", "aa4", "aa5", "aa6", "aa7", "aa8"),
      Set("aa1", "aa10", "aa11", "aa12", "aa3", "aa4", "aa5", "aa6", "aa7", "aa9"),
      Set("aa1", "aa10", "aa11", "aa12", "aa3", "aa4", "aa5", "aa6", "aa7"),
      Set("aa1", "aa10", "aa11", "aa12", "aa3", "aa4", "aa5", "aa6", "aa8", "aa9"),
      Set("aa1", "aa10", "aa11", "aa12", "aa3", "aa4", "aa5", "aa6", "aa8"),
      Set("aa1", "aa10", "aa11", "aa12", "aa3", "aa4", "aa5", "aa6", "aa9"),
      Set("aa1", "aa10", "aa11", "aa12", "aa3", "aa4", "aa5", "aa7", "aa8", "aa9"),
      Set("aa1", "aa10", "aa11", "aa12", "aa3", "aa4", "aa5", "aa7", "aa8"),
      Set("aa1", "aa10", "aa11", "aa12", "aa3", "aa4", "aa5", "aa7", "aa9"),
      Set("aa1", "aa10", "aa11", "aa12", "aa3", "aa4", "aa5", "aa8", "aa9"),
      Set("aa1", "aa10", "aa11", "aa12", "aa3", "aa4", "aa6", "aa7", "aa8", "aa9"),
      Set("aa1", "aa10", "aa11", "aa12", "aa3", "aa4", "aa6", "aa7", "aa8"),
      Set("aa1", "aa10", "aa11", "aa12", "aa3", "aa4", "aa6", "aa7", "aa9"),
      Set("aa1", "aa10", "aa11", "aa12", "aa3", "aa4", "aa6", "aa8", "aa9"),
      Set("aa1", "aa10", "aa11", "aa12", "aa3", "aa4", "aa7", "aa8", "aa9"),
      Set("aa1", "aa10", "aa11", "aa12", "aa3", "aa5", "aa6", "aa7", "aa8", "aa9"),
      Set("aa1", "aa10", "aa11", "aa12", "aa3", "aa5", "aa6", "aa7", "aa8"),
      Set("aa1", "aa10", "aa11", "aa12", "aa3", "aa5", "aa6", "aa7", "aa9"),
      Set("aa1", "aa10", "aa11", "aa12", "aa3", "aa5", "aa6", "aa8", "aa9"),
      Set("aa1", "aa10", "aa11", "aa12", "aa3", "aa5", "aa7", "aa8", "aa9"),
      Set("aa1", "aa10", "aa11", "aa12", "aa3", "aa6", "aa7", "aa8", "aa9"),
      Set("aa1", "aa10", "aa11", "aa12", "aa4", "aa5", "aa6", "aa7", "aa8", "aa9"),
      Set("aa1", "aa10", "aa11", "aa12", "aa4", "aa5", "aa6", "aa7", "aa8"),
      Set("aa1", "aa10", "aa11", "aa12", "aa4", "aa5", "aa6", "aa7", "aa9"),
      Set("aa1", "aa10", "aa11", "aa12", "aa4", "aa5", "aa6", "aa8", "aa9"),
      Set("aa1", "aa10", "aa11", "aa12", "aa4", "aa5", "aa7", "aa8", "aa9"),
      Set("aa1", "aa10", "aa11", "aa12", "aa4", "aa6", "aa7", "aa8", "aa9"),
      Set("aa1", "aa10", "aa11", "aa12", "aa5", "aa6", "aa7", "aa8", "aa9"),
      Set("aa1", "aa10", "aa11", "aa2", "aa3", "aa4", "aa5", "aa6", "aa7", "aa8", "aa9"),
      Set("aa1", "aa10", "aa11", "aa2", "aa3", "aa4", "aa5", "aa6", "aa7", "aa8"),
      Set("aa1", "aa10", "aa11", "aa2", "aa3", "aa4", "aa5", "aa6", "aa7", "aa9"),
      Set("aa1", "aa10", "aa11", "aa2", "aa3", "aa4", "aa5", "aa6", "aa7"),
      Set("aa1", "aa10", "aa11", "aa2", "aa3", "aa4", "aa5", "aa6", "aa8", "aa9"),
      Set("aa1", "aa10", "aa11", "aa2", "aa3", "aa4", "aa5", "aa6", "aa8"),
      Set("aa1", "aa10", "aa11", "aa2", "aa3", "aa4", "aa5", "aa6", "aa9"),
      Set("aa1", "aa10", "aa11", "aa2", "aa3", "aa4", "aa5", "aa7", "aa8", "aa9"),
      Set("aa1", "aa10", "aa11", "aa2", "aa3", "aa4", "aa5", "aa7", "aa8"),
      Set("aa1", "aa10", "aa11", "aa2", "aa3", "aa4", "aa5", "aa7", "aa9"),
      Set("aa1", "aa10", "aa11", "aa2", "aa3", "aa4", "aa5", "aa8", "aa9"),
      Set("aa1", "aa10", "aa11", "aa2", "aa3", "aa4", "aa6", "aa7", "aa8", "aa9"),
      Set("aa1", "aa10", "aa11", "aa2", "aa3", "aa4", "aa6", "aa7", "aa8"),
      Set("aa1", "aa10", "aa11", "aa2", "aa3", "aa4", "aa6", "aa7", "aa9"),
      Set("aa1", "aa10", "aa11", "aa2", "aa3", "aa4", "aa6", "aa8", "aa9"),
      Set("aa1", "aa10", "aa11", "aa2", "aa3", "aa4", "aa7", "aa8", "aa9"),
      Set("aa1", "aa10", "aa11", "aa2", "aa3", "aa5", "aa6", "aa7", "aa8", "aa9"),
      Set("aa1", "aa10", "aa11", "aa2", "aa3", "aa5", "aa6", "aa7", "aa8"),
      Set("aa1", "aa10", "aa11", "aa2", "aa3", "aa5", "aa6", "aa7", "aa9"),
      Set("aa1", "aa10", "aa11", "aa2", "aa3", "aa5", "aa6", "aa8", "aa9"),
      Set("aa1", "aa10", "aa11", "aa2", "aa3", "aa5", "aa7", "aa8", "aa9"),
      Set("aa1", "aa10", "aa11", "aa2", "aa3", "aa6", "aa7", "aa8", "aa9"),
      Set("aa1", "aa10", "aa11", "aa2", "aa4", "aa5", "aa6", "aa7", "aa8", "aa9"),
      Set("aa1", "aa10", "aa11", "aa2", "aa4", "aa5", "aa6", "aa7", "aa8"),
      Set("aa1", "aa10", "aa11", "aa2", "aa4", "aa5", "aa6", "aa7", "aa9"),
      Set("aa1", "aa10", "aa11", "aa2", "aa4", "aa5", "aa6", "aa8", "aa9"),
      Set("aa1", "aa10", "aa11", "aa2", "aa4", "aa5", "aa7", "aa8", "aa9"),
      Set("aa1", "aa10", "aa11", "aa2", "aa4", "aa6", "aa7", "aa8", "aa9"),
      Set("aa1", "aa10", "aa11", "aa2", "aa5", "aa6", "aa7", "aa8", "aa9"),
      Set("aa1", "aa10", "aa11", "aa3", "aa4", "aa5", "aa6", "aa7", "aa8", "aa9"),
      Set("aa1", "aa10", "aa11", "aa3", "aa4", "aa5", "aa6", "aa7", "aa8"),
      Set("aa1", "aa10", "aa11", "aa3", "aa4", "aa5", "aa6", "aa7", "aa9"),
      Set("aa1", "aa10", "aa11", "aa3", "aa4", "aa5", "aa6", "aa8", "aa9"),
      Set("aa1", "aa10", "aa11", "aa3", "aa4", "aa5", "aa7", "aa8", "aa9"),
      Set("aa1", "aa10", "aa11", "aa3", "aa4", "aa6", "aa7", "aa8", "aa9"),
      Set("aa1", "aa10", "aa11", "aa3", "aa5", "aa6", "aa7", "aa8", "aa9"),
      Set("aa1", "aa10", "aa11", "aa4", "aa5", "aa6", "aa7", "aa8", "aa9"),
      Set("aa1", "aa10", "aa12", "aa2", "aa3", "aa4", "aa5", "aa6", "aa7", "aa8", "aa9"),
      Set("aa1", "aa10", "aa12", "aa2", "aa3", "aa4", "aa5", "aa6", "aa7", "aa8"),
      Set("aa1", "aa10", "aa12", "aa2", "aa3", "aa4", "aa5", "aa6", "aa7", "aa9"),
      Set("aa1", "aa10", "aa12", "aa2", "aa3", "aa4", "aa5", "aa6", "aa7"),
      Set("aa1", "aa10", "aa12", "aa2", "aa3", "aa4", "aa5", "aa6", "aa8", "aa9"),
      Set("aa1", "aa10", "aa12", "aa2", "aa3", "aa4", "aa5", "aa6", "aa8"),
      Set("aa1", "aa10", "aa12", "aa2", "aa3", "aa4", "aa5", "aa6", "aa9"),
      Set("aa1", "aa10", "aa12", "aa2", "aa3", "aa4", "aa5", "aa7", "aa8", "aa9"),
      Set("aa1", "aa10", "aa12", "aa2", "aa3", "aa4", "aa5", "aa7", "aa8"),
      Set("aa1", "aa10", "aa12", "aa2", "aa3", "aa4", "aa5", "aa7", "aa9"),
      Set("aa1", "aa10", "aa12", "aa2", "aa3", "aa4", "aa5", "aa8", "aa9"),
      Set("aa1", "aa10", "aa12", "aa2", "aa3", "aa4", "aa6", "aa7", "aa8", "aa9"),
      Set("aa1", "aa10", "aa12", "aa2", "aa3", "aa4", "aa6", "aa7", "aa8"),
      Set("aa1", "aa10", "aa12", "aa2", "aa3", "aa4", "aa6", "aa7", "aa9"),
      Set("aa1", "aa10", "aa12", "aa2", "aa3", "aa4", "aa6", "aa8", "aa9"),
      Set("aa1", "aa10", "aa12", "aa2", "aa3", "aa4", "aa7", "aa8", "aa9"),
      Set("aa1", "aa10", "aa12", "aa2", "aa3", "aa5", "aa6", "aa7", "aa8", "aa9"),
      Set("aa1", "aa10", "aa12", "aa2", "aa3", "aa5", "aa6", "aa7", "aa8"),
      Set("aa1", "aa10", "aa12", "aa2", "aa3", "aa5", "aa6", "aa7", "aa9"),
      Set("aa1", "aa10", "aa12", "aa2", "aa3", "aa5", "aa6", "aa8", "aa9"),
      Set("aa1", "aa10", "aa12", "aa2", "aa3", "aa5", "aa7", "aa8", "aa9"),
      Set("aa1", "aa10", "aa12", "aa2", "aa3", "aa6", "aa7", "aa8", "aa9"),
      Set("aa1", "aa10", "aa12", "aa2", "aa4", "aa5", "aa6", "aa7", "aa8", "aa9"),
      Set("aa1", "aa10", "aa12", "aa2", "aa4", "aa5", "aa6", "aa7", "aa8"),
      Set("aa1", "aa10", "aa12", "aa2", "aa4", "aa5", "aa6", "aa7", "aa9"),
      Set("aa1", "aa10", "aa12", "aa2", "aa4", "aa5", "aa6", "aa8", "aa9"),
      Set("aa1", "aa10", "aa12", "aa2", "aa4", "aa5", "aa7", "aa8", "aa9"),
      Set("aa1", "aa10", "aa12", "aa2", "aa4", "aa6", "aa7", "aa8", "aa9"),
      Set("aa1", "aa10", "aa12", "aa2", "aa5", "aa6", "aa7", "aa8", "aa9"),
      Set("aa1", "aa10", "aa12", "aa3", "aa4", "aa5", "aa6", "aa7", "aa8", "aa9"),
      Set("aa1", "aa10", "aa12", "aa3", "aa4", "aa5", "aa6", "aa7", "aa8"),
      Set("aa1", "aa10", "aa12", "aa3", "aa4", "aa5", "aa6", "aa7", "aa9"),
      Set("aa1", "aa10", "aa12", "aa3", "aa4", "aa5", "aa6", "aa8", "aa9"),
      Set("aa1", "aa10", "aa12", "aa3", "aa4", "aa5", "aa7", "aa8", "aa9"),
      Set("aa1", "aa10", "aa12", "aa3", "aa4", "aa6", "aa7", "aa8", "aa9"),
      Set("aa1", "aa10", "aa12", "aa3", "aa5", "aa6", "aa7", "aa8", "aa9"),
      Set("aa1", "aa10", "aa12", "aa4", "aa5", "aa6", "aa7", "aa8", "aa9"),
      Set("aa1", "aa10", "aa2", "aa3", "aa4", "aa5", "aa6", "aa7", "aa8", "aa9"),
      Set("aa1", "aa10", "aa2", "aa3", "aa4", "aa5", "aa6", "aa7", "aa8"),
      Set("aa1", "aa10", "aa2", "aa3", "aa4", "aa5", "aa6", "aa7", "aa9"),
      Set("aa1", "aa10", "aa2", "aa3", "aa4", "aa5", "aa6", "aa8", "aa9"),
      Set("aa1", "aa10", "aa2", "aa3", "aa4", "aa5", "aa7", "aa8", "aa9"),
      Set("aa1", "aa10", "aa2", "aa3", "aa4", "aa6", "aa7", "aa8", "aa9"),
      Set("aa1", "aa10", "aa2", "aa3", "aa5", "aa6", "aa7", "aa8", "aa9"),
      Set("aa1", "aa10", "aa2", "aa4", "aa5", "aa6", "aa7", "aa8", "aa9"),
      Set("aa1", "aa10", "aa3", "aa4", "aa5", "aa6", "aa7", "aa8", "aa9"),
      Set("aa1", "aa11", "aa12", "aa2", "aa3", "aa4", "aa5", "aa6", "aa7", "aa8", "aa9"),
      Set("aa1", "aa11", "aa12", "aa2", "aa3", "aa4", "aa5", "aa6", "aa7", "aa8"),
      Set("aa1", "aa11", "aa12", "aa2", "aa3", "aa4", "aa5", "aa6", "aa7", "aa9"),
      Set("aa1", "aa11", "aa12", "aa2", "aa3", "aa4", "aa5", "aa6", "aa7"),
      Set("aa1", "aa11", "aa12", "aa2", "aa3", "aa4", "aa5", "aa6", "aa8", "aa9"),
      Set("aa1", "aa11", "aa12", "aa2", "aa3", "aa4", "aa5", "aa6", "aa8"),
      Set("aa1", "aa11", "aa12", "aa2", "aa3", "aa4", "aa5", "aa6", "aa9"),
      Set("aa1", "aa11", "aa12", "aa2", "aa3", "aa4", "aa5", "aa7", "aa8", "aa9"),
      Set("aa1", "aa11", "aa12", "aa2", "aa3", "aa4", "aa5", "aa7", "aa8"),
      Set("aa1", "aa11", "aa12", "aa2", "aa3", "aa4", "aa5", "aa7", "aa9"),
      Set("aa1", "aa11", "aa12", "aa2", "aa3", "aa4", "aa5", "aa8", "aa9"),
      Set("aa1", "aa11", "aa12", "aa2", "aa3", "aa4", "aa6", "aa7", "aa8", "aa9"),
      Set("aa1", "aa11", "aa12", "aa2", "aa3", "aa4", "aa6", "aa7", "aa8"),
      Set("aa1", "aa11", "aa12", "aa2", "aa3", "aa4", "aa6", "aa7", "aa9"),
      Set("aa1", "aa11", "aa12", "aa2", "aa3", "aa4", "aa6", "aa8", "aa9"),
      Set("aa1", "aa11", "aa12", "aa2", "aa3", "aa4", "aa7", "aa8", "aa9"),
      Set("aa1", "aa11", "aa12", "aa2", "aa3", "aa5", "aa6", "aa7", "aa8", "aa9"),
      Set("aa1", "aa11", "aa12", "aa2", "aa3", "aa5", "aa6", "aa7", "aa8"),
      Set("aa1", "aa11", "aa12", "aa2", "aa3", "aa5", "aa6", "aa7", "aa9"),
      Set("aa1", "aa11", "aa12", "aa2", "aa3", "aa5", "aa6", "aa8", "aa9"),
      Set("aa1", "aa11", "aa12", "aa2", "aa3", "aa5", "aa7", "aa8", "aa9"),
      Set("aa1", "aa11", "aa12", "aa2", "aa3", "aa6", "aa7", "aa8", "aa9"),
      Set("aa1", "aa11", "aa12", "aa2", "aa4", "aa5", "aa6", "aa7", "aa8", "aa9"),
      Set("aa1", "aa11", "aa12", "aa2", "aa4", "aa5", "aa6", "aa7", "aa8"),
      Set("aa1", "aa11", "aa12", "aa2", "aa4", "aa5", "aa6", "aa7", "aa9"),
      Set("aa1", "aa11", "aa12", "aa2", "aa4", "aa5", "aa6", "aa8", "aa9"),
      Set("aa1", "aa11", "aa12", "aa2", "aa4", "aa5", "aa7", "aa8", "aa9"),
      Set("aa1", "aa11", "aa12", "aa2", "aa4", "aa6", "aa7", "aa8", "aa9"),
      Set("aa1", "aa11", "aa12", "aa2", "aa5", "aa6", "aa7", "aa8", "aa9"),
      Set("aa1", "aa11", "aa12", "aa3", "aa4", "aa5", "aa6", "aa7", "aa8", "aa9"),
      Set("aa1", "aa11", "aa12", "aa3", "aa4", "aa5", "aa6", "aa7", "aa8"),
      Set("aa1", "aa11", "aa12", "aa3", "aa4", "aa5", "aa6", "aa7", "aa9"),
      Set("aa1", "aa11", "aa12", "aa3", "aa4", "aa5", "aa6", "aa8", "aa9"),
      Set("aa1", "aa11", "aa12", "aa3", "aa4", "aa5", "aa7", "aa8", "aa9"),
      Set("aa1", "aa11", "aa12", "aa3", "aa4", "aa6", "aa7", "aa8", "aa9"),
      Set("aa1", "aa11", "aa12", "aa3", "aa5", "aa6", "aa7", "aa8", "aa9"),
      Set("aa1", "aa11", "aa12", "aa4", "aa5", "aa6", "aa7", "aa8", "aa9"),
      Set("aa1", "aa11", "aa2", "aa3", "aa4", "aa5", "aa6", "aa7", "aa8", "aa9"),
      Set("aa1", "aa11", "aa2", "aa3", "aa4", "aa5", "aa6", "aa7", "aa8"),
      Set("aa1", "aa11", "aa2", "aa3", "aa4", "aa5", "aa6", "aa7", "aa9"),
      Set("aa1", "aa11", "aa2", "aa3", "aa4", "aa5", "aa6", "aa8", "aa9"),
      Set("aa1", "aa11", "aa2", "aa3", "aa4", "aa5", "aa7", "aa8", "aa9"),
      Set("aa1", "aa11", "aa2", "aa3", "aa4", "aa6", "aa7", "aa8", "aa9"),
      Set("aa1", "aa11", "aa2", "aa3", "aa5", "aa6", "aa7", "aa8", "aa9"),
      Set("aa1", "aa11", "aa2", "aa4", "aa5", "aa6", "aa7", "aa8", "aa9"),
      Set("aa1", "aa11", "aa3", "aa4", "aa5", "aa6", "aa7", "aa8", "aa9"),
      Set("aa1", "aa12", "aa2", "aa3", "aa4", "aa5", "aa6", "aa7", "aa8", "aa9"),
      Set("aa1", "aa12", "aa2", "aa3", "aa4", "aa5", "aa6", "aa7", "aa8"),
      Set("aa1", "aa12", "aa2", "aa3", "aa4", "aa5", "aa6", "aa7", "aa9"),
      Set("aa1", "aa12", "aa2", "aa3", "aa4", "aa5", "aa6", "aa8", "aa9"),
      Set("aa1", "aa12", "aa2", "aa3", "aa4", "aa5", "aa7", "aa8", "aa9"),
      Set("aa1", "aa12", "aa2", "aa3", "aa4", "aa6", "aa7", "aa8", "aa9"),
      Set("aa1", "aa12", "aa2", "aa3", "aa5", "aa6", "aa7", "aa8", "aa9"),
      Set("aa1", "aa12", "aa2", "aa4", "aa5", "aa6", "aa7", "aa8", "aa9"),
      Set("aa1", "aa12", "aa3", "aa4", "aa5", "aa6", "aa7", "aa8", "aa9"),
      Set("aa1", "aa2", "aa3", "aa4", "aa5", "aa6", "aa7", "aa8", "aa9"),
      Set("aa10", "aa11", "aa12", "aa2", "aa3", "aa4", "aa5", "aa6", "aa7", "aa8", "aa9"),
      Set("aa10", "aa11", "aa12", "aa2", "aa3", "aa4", "aa5", "aa6", "aa7", "aa8"),
      Set("aa10", "aa11", "aa12", "aa2", "aa3", "aa4", "aa5", "aa6", "aa7", "aa9"),
      Set("aa10", "aa11", "aa12", "aa2", "aa3", "aa4", "aa5", "aa6", "aa7"),
      Set("aa10", "aa11", "aa12", "aa2", "aa3", "aa4", "aa5", "aa6", "aa8", "aa9"),
      Set("aa10", "aa11", "aa12", "aa2", "aa3", "aa4", "aa5", "aa6", "aa8"),
      Set("aa10", "aa11", "aa12", "aa2", "aa3", "aa4", "aa5", "aa6", "aa9"),
      Set("aa10", "aa11", "aa12", "aa2", "aa3", "aa4", "aa5", "aa7", "aa8", "aa9"),
      Set("aa10", "aa11", "aa12", "aa2", "aa3", "aa4", "aa5", "aa7", "aa8"),
      Set("aa10", "aa11", "aa12", "aa2", "aa3", "aa4", "aa5", "aa7", "aa9"),
      Set("aa10", "aa11", "aa12", "aa2", "aa3", "aa4", "aa5", "aa8", "aa9"),
      Set("aa10", "aa11", "aa12", "aa2", "aa3", "aa4", "aa6", "aa7", "aa8", "aa9"),
      Set("aa10", "aa11", "aa12", "aa2", "aa3", "aa4", "aa6", "aa7", "aa8"),
      Set("aa10", "aa11", "aa12", "aa2", "aa3", "aa4", "aa6", "aa7", "aa9"),
      Set("aa10", "aa11", "aa12", "aa2", "aa3", "aa4", "aa6", "aa8", "aa9"),
      Set("aa10", "aa11", "aa12", "aa2", "aa3", "aa4", "aa7", "aa8", "aa9"),
      Set("aa10", "aa11", "aa12", "aa2", "aa3", "aa5", "aa6", "aa7", "aa8", "aa9"),
      Set("aa10", "aa11", "aa12", "aa2", "aa3", "aa5", "aa6", "aa7", "aa8"),
      Set("aa10", "aa11", "aa12", "aa2", "aa3", "aa5", "aa6", "aa7", "aa9"),
      Set("aa10", "aa11", "aa12", "aa2", "aa3", "aa5", "aa6", "aa8", "aa9"),
      Set("aa10", "aa11", "aa12", "aa2", "aa3", "aa5", "aa7", "aa8", "aa9"),
      Set("aa10", "aa11", "aa12", "aa2", "aa3", "aa6", "aa7", "aa8", "aa9"),
      Set("aa10", "aa11", "aa12", "aa2", "aa4", "aa5", "aa6", "aa7", "aa8", "aa9"),
      Set("aa10", "aa11", "aa12", "aa2", "aa4", "aa5", "aa6", "aa7", "aa8"),
      Set("aa10", "aa11", "aa12", "aa2", "aa4", "aa5", "aa6", "aa7", "aa9"),
      Set("aa10", "aa11", "aa12", "aa2", "aa4", "aa5", "aa6", "aa8", "aa9"),
      Set("aa10", "aa11", "aa12", "aa2", "aa4", "aa5", "aa7", "aa8", "aa9"),
      Set("aa10", "aa11", "aa12", "aa2", "aa4", "aa6", "aa7", "aa8", "aa9"),
      Set("aa10", "aa11", "aa12", "aa2", "aa5", "aa6", "aa7", "aa8", "aa9"),
      Set("aa10", "aa11", "aa12", "aa3", "aa4", "aa5", "aa6", "aa7", "aa8", "aa9"),
      Set("aa10", "aa11", "aa12", "aa3", "aa4", "aa5", "aa6", "aa7", "aa8"),
      Set("aa10", "aa11", "aa12", "aa3", "aa4", "aa5", "aa6", "aa7", "aa9"),
      Set("aa10", "aa11", "aa12", "aa3", "aa4", "aa5", "aa6", "aa8", "aa9"),
      Set("aa10", "aa11", "aa12", "aa3", "aa4", "aa5", "aa7", "aa8", "aa9"),
      Set("aa10", "aa11", "aa12", "aa3", "aa4", "aa6", "aa7", "aa8", "aa9"),
      Set("aa10", "aa11", "aa12", "aa3", "aa5", "aa6", "aa7", "aa8", "aa9"),
      Set("aa10", "aa11", "aa12", "aa4", "aa5", "aa6", "aa7", "aa8", "aa9"),
      Set("aa10", "aa11", "aa2", "aa3", "aa4", "aa5", "aa6", "aa7", "aa8", "aa9"),
      Set("aa10", "aa11", "aa2", "aa3", "aa4", "aa5", "aa6", "aa7", "aa8"),
      Set("aa10", "aa11", "aa2", "aa3", "aa4", "aa5", "aa6", "aa7", "aa9"),
      Set("aa10", "aa11", "aa2", "aa3", "aa4", "aa5", "aa6", "aa8", "aa9"),
      Set("aa10", "aa11", "aa2", "aa3", "aa4", "aa5", "aa7", "aa8", "aa9"),
      Set("aa10", "aa11", "aa2", "aa3", "aa4", "aa6", "aa7", "aa8", "aa9"),
      Set("aa10", "aa11", "aa2", "aa3", "aa5", "aa6", "aa7", "aa8", "aa9"),
      Set("aa10", "aa11", "aa2", "aa4", "aa5", "aa6", "aa7", "aa8", "aa9"),
      Set("aa10", "aa11", "aa3", "aa4", "aa5", "aa6", "aa7", "aa8", "aa9"),
      Set("aa10", "aa12", "aa2", "aa3", "aa4", "aa5", "aa6", "aa7", "aa8", "aa9"),
      Set("aa10", "aa12", "aa2", "aa3", "aa4", "aa5", "aa6", "aa7", "aa8"),
      Set("aa10", "aa12", "aa2", "aa3", "aa4", "aa5", "aa6", "aa7", "aa9"),
      Set("aa10", "aa12", "aa2", "aa3", "aa4", "aa5", "aa6", "aa8", "aa9"),
      Set("aa10", "aa12", "aa2", "aa3", "aa4", "aa5", "aa7", "aa8", "aa9"),
      Set("aa10", "aa12", "aa2", "aa3", "aa4", "aa6", "aa7", "aa8", "aa9"),
      Set("aa10", "aa12", "aa2", "aa3", "aa5", "aa6", "aa7", "aa8", "aa9"),
      Set("aa10", "aa12", "aa2", "aa4", "aa5", "aa6", "aa7", "aa8", "aa9"),
      Set("aa10", "aa12", "aa3", "aa4", "aa5", "aa6", "aa7", "aa8", "aa9"),
      Set("aa10", "aa2", "aa3", "aa4", "aa5", "aa6", "aa7", "aa8", "aa9"),
      Set("aa11", "aa12", "aa2", "aa3", "aa4", "aa5", "aa6", "aa7", "aa8", "aa9"),
      Set("aa11", "aa12", "aa2", "aa3", "aa4", "aa5", "aa6", "aa7", "aa8"),
      Set("aa11", "aa12", "aa2", "aa3", "aa4", "aa5", "aa6", "aa7", "aa9"),
      Set("aa11", "aa12", "aa2", "aa3", "aa4", "aa5", "aa6", "aa8", "aa9"),
      Set("aa11", "aa12", "aa2", "aa3", "aa4", "aa5", "aa7", "aa8", "aa9"),
      Set("aa11", "aa12", "aa2", "aa3", "aa4", "aa6", "aa7", "aa8", "aa9"),
      Set("aa11", "aa12", "aa2", "aa3", "aa5", "aa6", "aa7", "aa8", "aa9"),
      Set("aa11", "aa12", "aa2", "aa4", "aa5", "aa6", "aa7", "aa8", "aa9"),
      Set("aa11", "aa12", "aa3", "aa4", "aa5", "aa6", "aa7", "aa8", "aa9"),
      Set("aa11", "aa2", "aa3", "aa4", "aa5", "aa6", "aa7", "aa8", "aa9"),
      Set("aa12", "aa2", "aa3", "aa4", "aa5", "aa6", "aa7", "aa8", "aa9")
    )
}
@romac
Copy link
Member

romac commented Aug 20, 2024

Not sure if that helps much but it looks like Apalache is sending back a response with error status 13, but I cannot tell exactly why. Perhaps the input Quint sends to Apalache is malformed or something else goes wrong in Apalache. Here is the output with debugging enabled:

$ GRPC_TRACE=all GRPC_VERBOSITY=DEBUG NODE_DEBUG=http2 quint verify --invariant=inv 

(...)

D 2024-08-20T07:28:23.324Z | v1.10.1 93519 | subchannel_call | [10] Received server trailers:
                grpc-status: 13

D 2024-08-20T07:28:23.324Z | v1.10.1 93519 | subchannel_call | [10] received status code 13 from server
D 2024-08-20T07:28:23.324Z | v1.10.1 93519 | subchannel_call | [10] ended with status: code=13 details=""
D 2024-08-20T07:28:23.324Z | v1.10.1 93519 | subchannel_call | [10] close http2 stream with code 8
D 2024-08-20T07:28:23.324Z | v1.10.1 93519 | load_balancing_call | [9] Received status
D 2024-08-20T07:28:23.324Z | v1.10.1 93519 | load_balancing_call | [9] ended with status: code=13 details=""
D 2024-08-20T07:28:23.324Z | v1.10.1 93519 | retrying_call | [8] Received status from child [9]
D 2024-08-20T07:28:23.324Z | v1.10.1 93519 | retrying_call | [8] state=COMMITTED handling status with progress PROCESSED from child [9] in state ACTIVE
D 2024-08-20T07:28:23.324Z | v1.10.1 93519 | retrying_call | [8] ended with status: code=13 details=""
D 2024-08-20T07:28:23.324Z | v1.10.1 93519 | resolving_call | [7] Received status
D 2024-08-20T07:28:23.324Z | v1.10.1 93519 | resolving_call | [7] ended with status: code=13 details=""
Click to show full logs 
❯ GRPC_TRACE=all GRPC_VERBOSITY=DEBUG NODE_DEBUG=http2 quint verify --invariant=inv testFixture/apalache/large_set.qnt
D 2024-08-20T07:28:17.465Z | v1.10.1 93519 | resolving_load_balancer | dns:localhost:8822 IDLE -> IDLE
D 2024-08-20T07:28:17.467Z | v1.10.1 93519 | connectivity_state | (1) dns:localhost:8822 IDLE -> IDLE
D 2024-08-20T07:28:17.467Z | v1.10.1 93519 | dns_resolver | Resolver constructed for target dns:localhost:8822
D 2024-08-20T07:28:17.470Z | v1.10.1 93519 | channel | (1) dns:localhost:8822 Channel constructed with options {}
D 2024-08-20T07:28:17.471Z | v1.10.1 93519 | channel_stacktrace | (1) Channel constructed
    at new InternalChannel (/Users/romac/Informal/Code/quint/quint/node_modules/@grpc/grpc-js/build/src/internal-channel.js:248:23)
    at new ChannelImplementation (/Users/romac/Informal/Code/quint/quint/node_modules/@grpc/grpc-js/build/src/channel.js:35:32)
    at new Client (/Users/romac/Informal/Code/quint/quint/node_modules/@grpc/grpc-js/build/src/client.js:65:36)
    at new ServiceClientImpl (/Users/romac/Informal/Code/quint/quint/node_modules/@grpc/grpc-js/build/src/make-client.js:58:5)
    at loadProtoDefViaReflection (/Users/romac/Informal/Code/quint/quint/dist/src/apalache.js:173:30)
    at tryConnect (/Users/romac/Informal/Code/quint/quint/dist/src/apalache.js:239:19)
    at connect (/Users/romac/Informal/Code/quint/quint/dist/src/apalache.js:328:36)
    at verify (/Users/romac/Informal/Code/quint/quint/dist/src/quintVerifier.js:31:59)
    at verifySpec (/Users/romac/Informal/Code/quint/quint/dist/src/cliCommands.js:590:39)
    at EitherConstructor.asyncChain (/Users/romac/Informal/Code/quint/quint/node_modules/@sweet-monads/either/cjs/index.js:125:16)
D 2024-08-20T07:28:17.471Z | v1.10.1 93519 | channel | (1) dns:localhost:8822 createResolvingCall [0] method="/grpc.reflection.v1alpha.ServerReflection/ServerReflectionInfo", deadline=Infinity
D 2024-08-20T07:28:17.471Z | v1.10.1 93519 | resolving_call | [0] Created
D 2024-08-20T07:28:17.471Z | v1.10.1 93519 | resolving_call | [0] Deadline: Infinity
D 2024-08-20T07:28:17.471Z | v1.10.1 93519 | resolving_call | [0] start called
D 2024-08-20T07:28:17.472Z | v1.10.1 93519 | dns_resolver | Looking up DNS hostname localhost
D 2024-08-20T07:28:17.474Z | v1.10.1 93519 | resolving_load_balancer | dns:localhost:8822 IDLE -> CONNECTING
D 2024-08-20T07:28:17.474Z | v1.10.1 93519 | connectivity_state | (1) dns:localhost:8822 IDLE -> CONNECTING
D 2024-08-20T07:28:17.475Z | v1.10.1 93519 | channel | (1) dns:localhost:8822 callRefTimer.ref | configSelectionQueue.length=1 pickQueue.length=0
D 2024-08-20T07:28:17.475Z | v1.10.1 93519 | resolving_call | [0] write() called with message of length 30
D 2024-08-20T07:28:17.476Z | v1.10.1 93519 | resolving_call | [0] startRead called
D 2024-08-20T07:28:17.476Z | v1.10.1 93519 | dns_resolver | Resolved addresses for target dns:localhost:8822: [::1:8822,127.0.0.1:8822]
D 2024-08-20T07:28:17.477Z | v1.10.1 93519 | subchannel | (2) ::1:8822 Subchannel constructed with options {}
D 2024-08-20T07:28:17.477Z | v1.10.1 93519 | subchannel_refcount | (2) ::1:8822 refcount 0 -> 1
D 2024-08-20T07:28:17.477Z | v1.10.1 93519 | subchannel | (3) 127.0.0.1:8822 Subchannel constructed with options {}
D 2024-08-20T07:28:17.477Z | v1.10.1 93519 | subchannel_refcount | (3) 127.0.0.1:8822 refcount 0 -> 1
D 2024-08-20T07:28:17.477Z | v1.10.1 93519 | subchannel_refcount | (2) ::1:8822 refcount 1 -> 2
D 2024-08-20T07:28:17.477Z | v1.10.1 93519 | subchannel_refcount | (3) 127.0.0.1:8822 refcount 1 -> 2
D 2024-08-20T07:28:17.478Z | v1.10.1 93519 | pick_first | Start connecting to subchannel with address ::1:8822
D 2024-08-20T07:28:17.478Z | v1.10.1 93519 | pick_first | IDLE -> CONNECTING
D 2024-08-20T07:28:17.478Z | v1.10.1 93519 | resolving_load_balancer | dns:localhost:8822 CONNECTING -> CONNECTING
D 2024-08-20T07:28:17.478Z | v1.10.1 93519 | connectivity_state | (1) dns:localhost:8822 CONNECTING -> CONNECTING
D 2024-08-20T07:28:17.478Z | v1.10.1 93519 | channel | (1) dns:localhost:8822 callRefTimer.unref | configSelectionQueue.length=0 pickQueue.length=0
D 2024-08-20T07:28:17.478Z | v1.10.1 93519 | subchannel | (2) ::1:8822 IDLE -> CONNECTING
D 2024-08-20T07:28:17.479Z | v1.10.1 93519 | transport | dns:localhost:8822 creating HTTP/2 session to ::1:8822
HTTP2 93519: Http2Session client: created
D 2024-08-20T07:28:17.480Z | v1.10.1 93519 | channel | (1) dns:localhost:8822 createRetryingCall [1] method="/grpc.reflection.v1alpha.ServerReflection/ServerReflectionInfo"
D 2024-08-20T07:28:17.480Z | v1.10.1 93519 | resolving_call | [0] Created child [1]
D 2024-08-20T07:28:17.480Z | v1.10.1 93519 | retrying_call | [1] start called
D 2024-08-20T07:28:17.480Z | v1.10.1 93519 | channel | (1) dns:localhost:8822 createLoadBalancingCall [2] method="/grpc.reflection.v1alpha.ServerReflection/ServerReflectionInfo"
D 2024-08-20T07:28:17.480Z | v1.10.1 93519 | retrying_call | [1] Created child call [2] for attempt 1
D 2024-08-20T07:28:17.481Z | v1.10.1 93519 | load_balancing_call | [2] start called
D 2024-08-20T07:28:17.481Z | v1.10.1 93519 | load_balancing_call | [2] Pick called
D 2024-08-20T07:28:17.481Z | v1.10.1 93519 | load_balancing_call | [2] Pick result: QUEUE subchannel: null status: undefined undefined
D 2024-08-20T07:28:17.481Z | v1.10.1 93519 | channel | (1) dns:localhost:8822 callRefTimer.ref | configSelectionQueue.length=0 pickQueue.length=1
D 2024-08-20T07:28:17.481Z | v1.10.1 93519 | retrying_call | [1] startRead called
D 2024-08-20T07:28:17.481Z | v1.10.1 93519 | load_balancing_call | [2] startRead called
D 2024-08-20T07:28:17.481Z | v1.10.1 93519 | retrying_call | [1] write() called with message of length 35
D 2024-08-20T07:28:17.481Z | v1.10.1 93519 | load_balancing_call | [2] write() called with message of length 35
(node:93519) Warning: Setting the NODE_DEBUG environment variable to 'http2' can expose sensitive data (such as passwords, tokens and authentication headers) in the resulting log.
(Use `node --trace-warnings ...` to show where the warning was created)
HTTP2 93519: Http2Session <invalid>: socket error [connect ECONNREFUSED ::1:8822]
HTTP2 93519: Http2Session client: destroying
HTTP2 93519: Http2Session client: start closing/destroying Error: connect ECONNREFUSED ::1:8822
    at TCPConnectWrap.afterConnect [as oncomplete] (node:net:1607:16) {
  errno: -61,
  code: 'ECONNREFUSED',
  syscall: 'connect',
  address: '::1',
  port: 8822
}
HTTP2 93519: Http2Session client: finishSessionClose
D 2024-08-20T07:28:17.484Z | v1.10.1 93519 | transport | dns:localhost:8822 connection failed with error connect ECONNREFUSED ::1:8822
D 2024-08-20T07:28:17.484Z | v1.10.1 93519 | subchannel | (2) ::1:8822 CONNECTING -> TRANSIENT_FAILURE
D 2024-08-20T07:28:17.484Z | v1.10.1 93519 | pick_first | Start connecting to subchannel with address 127.0.0.1:8822
D 2024-08-20T07:28:17.484Z | v1.10.1 93519 | subchannel | (3) 127.0.0.1:8822 IDLE -> CONNECTING
D 2024-08-20T07:28:17.484Z | v1.10.1 93519 | transport | dns:localhost:8822 creating HTTP/2 session to 127.0.0.1:8822
HTTP2 93519: Http2Session client: created
HTTP2 93519: Http2Session <invalid>: socket error [connect ECONNREFUSED 127.0.0.1:8822]
HTTP2 93519: Http2Session client: destroying
HTTP2 93519: Http2Session client: start closing/destroying Error: connect ECONNREFUSED 127.0.0.1:8822
    at TCPConnectWrap.afterConnect [as oncomplete] (node:net:1607:16) {
  errno: -61,
  code: 'ECONNREFUSED',
  syscall: 'connect',
  address: '127.0.0.1',
  port: 8822
}
HTTP2 93519: Http2Session client: finishSessionClose
D 2024-08-20T07:28:17.485Z | v1.10.1 93519 | transport | dns:localhost:8822 connection failed with error connect ECONNREFUSED 127.0.0.1:8822
D 2024-08-20T07:28:17.485Z | v1.10.1 93519 | subchannel | (3) 127.0.0.1:8822 CONNECTING -> TRANSIENT_FAILURE
D 2024-08-20T07:28:17.485Z | v1.10.1 93519 | dns_resolver | resolution update delayed by "min time between resolutions" rate limit
D 2024-08-20T07:28:17.485Z | v1.10.1 93519 | pick_first | CONNECTING -> TRANSIENT_FAILURE
D 2024-08-20T07:28:17.485Z | v1.10.1 93519 | resolving_load_balancer | dns:localhost:8822 CONNECTING -> TRANSIENT_FAILURE
D 2024-08-20T07:28:17.485Z | v1.10.1 93519 | channel | (1) dns:localhost:8822 callRefTimer.unref | configSelectionQueue.length=0 pickQueue.length=0
D 2024-08-20T07:28:17.485Z | v1.10.1 93519 | load_balancing_call | [2] Pick called
D 2024-08-20T07:28:17.486Z | v1.10.1 93519 | load_balancing_call | [2] Pick result: TRANSIENT_FAILURE subchannel: null status: 14 No connection established. Last error: connect ECONNREFUSED 127.0.0.1:8822 (2024-08-20T07:28:17.485Z)
D 2024-08-20T07:28:17.486Z | v1.10.1 93519 | connectivity_state | (1) dns:localhost:8822 CONNECTING -> TRANSIENT_FAILURE
D 2024-08-20T07:28:17.486Z | v1.10.1 93519 | load_balancing_call | [2] ended with status: code=14 details="No connection established. Last error: connect ECONNREFUSED 127.0.0.1:8822 (2024-08-20T07:28:17.485Z)"
D 2024-08-20T07:28:17.486Z | v1.10.1 93519 | retrying_call | [1] Received status from child [2]
D 2024-08-20T07:28:17.486Z | v1.10.1 93519 | retrying_call | [1] state=TRANSPARENT_ONLY handling status with progress PROCESSED from child [2] in state ACTIVE
D 2024-08-20T07:28:17.486Z | v1.10.1 93519 | retrying_call | [1] ended with status: code=14 details="No connection established. Last error: connect ECONNREFUSED 127.0.0.1:8822 (2024-08-20T07:28:17.485Z)"
D 2024-08-20T07:28:17.486Z | v1.10.1 93519 | resolving_call | [0] Received status
D 2024-08-20T07:28:17.486Z | v1.10.1 93519 | resolving_call | [0] ended with status: code=14 details="No connection established. Last error: connect ECONNREFUSED 127.0.0.1:8822 (2024-08-20T07:28:17.485Z)"
D 2024-08-20T07:28:17.490Z | v1.10.1 93519 | resolving_load_balancer | dns:localhost:8822 IDLE -> IDLE
D 2024-08-20T07:28:17.490Z | v1.10.1 93519 | connectivity_state | (4) dns:localhost:8822 IDLE -> IDLE
D 2024-08-20T07:28:17.490Z | v1.10.1 93519 | dns_resolver | Resolver constructed for target dns:localhost:8822
D 2024-08-20T07:28:17.490Z | v1.10.1 93519 | channel | (4) dns:localhost:8822 Channel constructed with options {}
D 2024-08-20T07:28:17.490Z | v1.10.1 93519 | channel_stacktrace | (4) Channel constructed
    at new InternalChannel (/Users/romac/Informal/Code/quint/quint/node_modules/@grpc/grpc-js/build/src/internal-channel.js:248:23)
    at new ChannelImplementation (/Users/romac/Informal/Code/quint/quint/node_modules/@grpc/grpc-js/build/src/channel.js:35:32)
    at new Client (/Users/romac/Informal/Code/quint/quint/node_modules/@grpc/grpc-js/build/src/client.js:65:36)
    at new ServiceClientImpl (/Users/romac/Informal/Code/quint/quint/node_modules/@grpc/grpc-js/build/src/make-client.js:58:5)
    at loadProtoDefViaReflection (/Users/romac/Informal/Code/quint/quint/dist/src/apalache.js:173:30)
    at tryConnect (/Users/romac/Informal/Code/quint/quint/dist/src/apalache.js:239:19)
    at /Users/romac/Informal/Code/quint/quint/dist/src/apalache.js:379:41
    at EitherConstructor.asyncChain (/Users/romac/Informal/Code/quint/quint/node_modules/@sweet-monads/either/cjs/index.js:125:16)
    at /Users/romac/Informal/Code/quint/quint/node_modules/@sweet-monads/either/cjs/index.js:14:25
    at process.processTicksAndRejections (node:internal/process/task_queues:95:5)
D 2024-08-20T07:28:17.491Z | v1.10.1 93519 | dns_resolver | Looking up DNS hostname localhost
D 2024-08-20T07:28:17.491Z | v1.10.1 93519 | resolving_load_balancer | dns:localhost:8822 IDLE -> CONNECTING
D 2024-08-20T07:28:17.491Z | v1.10.1 93519 | connectivity_state | (4) dns:localhost:8822 IDLE -> CONNECTING
D 2024-08-20T07:28:17.491Z | v1.10.1 93519 | dns_resolver | Resolved addresses for target dns:localhost:8822: [::1:8822,127.0.0.1:8822]
D 2024-08-20T07:28:17.491Z | v1.10.1 93519 | subchannel_refcount | (2) ::1:8822 refcount 2 -> 3
D 2024-08-20T07:28:17.491Z | v1.10.1 93519 | subchannel_refcount | (3) 127.0.0.1:8822 refcount 2 -> 3
D 2024-08-20T07:28:17.491Z | v1.10.1 93519 | dns_resolver | resolution update delayed by "min time between resolutions" rate limit
D 2024-08-20T07:28:17.491Z | v1.10.1 93519 | pick_first | IDLE -> TRANSIENT_FAILURE
D 2024-08-20T07:28:17.491Z | v1.10.1 93519 | resolving_load_balancer | dns:localhost:8822 CONNECTING -> TRANSIENT_FAILURE
D 2024-08-20T07:28:17.491Z | v1.10.1 93519 | connectivity_state | (4) dns:localhost:8822 CONNECTING -> TRANSIENT_FAILURE
D 2024-08-20T07:28:17.491Z | v1.10.1 93519 | pick_first | TRANSIENT_FAILURE -> TRANSIENT_FAILURE
D 2024-08-20T07:28:17.491Z | v1.10.1 93519 | resolving_load_balancer | dns:localhost:8822 TRANSIENT_FAILURE -> TRANSIENT_FAILURE
D 2024-08-20T07:28:17.491Z | v1.10.1 93519 | connectivity_state | (4) dns:localhost:8822 TRANSIENT_FAILURE -> TRANSIENT_FAILURE
09:28:17.779 [main] INFO at.forsyte.apalache.tla.tooling.opt.ServerCmd -- Loading configuration
# Usage statistics is OFF. We care about your privacy.
# If you want to help our project, consider enabling statistics with config --enable-stats=true.

Output directory: /Users/romac/Informal/Code/quint/quint/_apalache-out/server/2024-08-20T09-28-17_17109933211651838349
# APALACHE version: 0.44.11 | build: 5dee24e                      I@09:28:17.990
Starting server on port 8822...                                   I@09:28:17.997
D 2024-08-20T07:28:18.479Z | v1.10.1 93519 | subchannel | (2) ::1:8822 TRANSIENT_FAILURE -> CONNECTING
D 2024-08-20T07:28:18.480Z | v1.10.1 93519 | transport | dns:localhost:8822 creating HTTP/2 session to ::1:8822
HTTP2 93519: Http2Session client: created
HTTP2 93519: Http2Session <invalid>: socket error [connect ECONNREFUSED ::1:8822]
HTTP2 93519: Http2Session client: destroying
HTTP2 93519: Http2Session client: start closing/destroying Error: connect ECONNREFUSED ::1:8822
    at TCPConnectWrap.afterConnect [as oncomplete] (node:net:1607:16) {
  errno: -61,
  code: 'ECONNREFUSED',
  syscall: 'connect',
  address: '::1',
  port: 8822
}
HTTP2 93519: Http2Session client: finishSessionClose
D 2024-08-20T07:28:18.480Z | v1.10.1 93519 | transport | dns:localhost:8822 connection failed with error connect ECONNREFUSED ::1:8822
D 2024-08-20T07:28:18.480Z | v1.10.1 93519 | subchannel | (2) ::1:8822 CONNECTING -> TRANSIENT_FAILURE
D 2024-08-20T07:28:18.481Z | v1.10.1 93519 | subchannel | (2) ::1:8822 TRANSIENT_FAILURE -> IDLE
D 2024-08-20T07:28:18.481Z | v1.10.1 93519 | subchannel | (2) ::1:8822 IDLE -> CONNECTING
D 2024-08-20T07:28:18.481Z | v1.10.1 93519 | transport | dns:localhost:8822 creating HTTP/2 session to ::1:8822
HTTP2 93519: Http2Session client: created
HTTP2 93519: Http2Session <invalid>: socket error [connect ECONNREFUSED ::1:8822]
HTTP2 93519: Http2Session client: destroying
HTTP2 93519: Http2Session client: start closing/destroying Error: connect ECONNREFUSED ::1:8822
    at TCPConnectWrap.afterConnect [as oncomplete] (node:net:1607:16) {
  errno: -61,
  code: 'ECONNREFUSED',
  syscall: 'connect',
  address: '::1',
  port: 8822
}
HTTP2 93519: Http2Session client: finishSessionClose
D 2024-08-20T07:28:18.481Z | v1.10.1 93519 | transport | dns:localhost:8822 connection failed with error connect ECONNREFUSED ::1:8822
D 2024-08-20T07:28:18.481Z | v1.10.1 93519 | subchannel | (2) ::1:8822 CONNECTING -> TRANSIENT_FAILURE
D 2024-08-20T07:28:18.485Z | v1.10.1 93519 | subchannel | (3) 127.0.0.1:8822 TRANSIENT_FAILURE -> CONNECTING
D 2024-08-20T07:28:18.485Z | v1.10.1 93519 | transport | dns:localhost:8822 creating HTTP/2 session to 127.0.0.1:8822
HTTP2 93519: Http2Session client: created
HTTP2 93519: Http2Session <invalid>: socket error [connect ECONNREFUSED 127.0.0.1:8822]
HTTP2 93519: Http2Session client: destroying
HTTP2 93519: Http2Session client: start closing/destroying Error: connect ECONNREFUSED 127.0.0.1:8822
    at TCPConnectWrap.afterConnect [as oncomplete] (node:net:1607:16) {
  errno: -61,
  code: 'ECONNREFUSED',
  syscall: 'connect',
  address: '127.0.0.1',
  port: 8822
}
HTTP2 93519: Http2Session client: finishSessionClose
D 2024-08-20T07:28:18.485Z | v1.10.1 93519 | transport | dns:localhost:8822 connection failed with error connect ECONNREFUSED 127.0.0.1:8822
D 2024-08-20T07:28:18.485Z | v1.10.1 93519 | subchannel | (3) 127.0.0.1:8822 CONNECTING -> TRANSIENT_FAILURE
D 2024-08-20T07:28:18.486Z | v1.10.1 93519 | subchannel | (3) 127.0.0.1:8822 TRANSIENT_FAILURE -> IDLE
D 2024-08-20T07:28:18.486Z | v1.10.1 93519 | subchannel | (3) 127.0.0.1:8822 IDLE -> CONNECTING
D 2024-08-20T07:28:18.486Z | v1.10.1 93519 | transport | dns:localhost:8822 creating HTTP/2 session to 127.0.0.1:8822
HTTP2 93519: Http2Session client: created
D 2024-08-20T07:28:18.486Z | v1.10.1 93519 | resolving_load_balancer | dns:localhost:8822 TRANSIENT_FAILURE -> TRANSIENT_FAILURE
D 2024-08-20T07:28:18.486Z | v1.10.1 93519 | connectivity_state | (1) dns:localhost:8822 TRANSIENT_FAILURE -> TRANSIENT_FAILURE
HTTP2 93519: Http2Session <invalid>: socket error [connect ECONNREFUSED 127.0.0.1:8822]
HTTP2 93519: Http2Session client: destroying
HTTP2 93519: Http2Session client: start closing/destroying Error: connect ECONNREFUSED 127.0.0.1:8822
    at TCPConnectWrap.afterConnect [as oncomplete] (node:net:1607:16) {
  errno: -61,
  code: 'ECONNREFUSED',
  syscall: 'connect',
  address: '127.0.0.1',
  port: 8822
}
HTTP2 93519: Http2Session client: finishSessionClose
D 2024-08-20T07:28:18.486Z | v1.10.1 93519 | transport | dns:localhost:8822 connection failed with error connect ECONNREFUSED 127.0.0.1:8822
D 2024-08-20T07:28:18.486Z | v1.10.1 93519 | subchannel | (3) 127.0.0.1:8822 CONNECTING -> TRANSIENT_FAILURE
D 2024-08-20T07:28:18.492Z | v1.10.1 93519 | dns_resolver | resolution update delayed by "min time between resolutions" rate limit
D 2024-08-20T07:28:19.492Z | v1.10.1 93519 | dns_resolver | resolution update delayed by "min time between resolutions" rate limit
D 2024-08-20T07:28:21.523Z | v1.10.1 93519 | subchannel | (2) ::1:8822 TRANSIENT_FAILURE -> CONNECTING
D 2024-08-20T07:28:21.524Z | v1.10.1 93519 | transport | dns:localhost:8822 creating HTTP/2 session to ::1:8822
HTTP2 93519: Http2Session client: created
HTTP2 93519: Http2Session client: setting up session handle
HTTP2 93519: Http2Session client: sending settings
HTTP2 93519: Http2Session client: submitting settings
D 2024-08-20T07:28:21.528Z | v1.10.1 93519 | subchannel | (2) ::1:8822 CONNECTING -> READY
D 2024-08-20T07:28:21.529Z | v1.10.1 93519 | pick_first | Pick subchannel with address ::1:8822
D 2024-08-20T07:28:21.529Z | v1.10.1 93519 | subchannel_refcount | (2) ::1:8822 refcount 3 -> 4
D 2024-08-20T07:28:21.529Z | v1.10.1 93519 | subchannel_refcount | (2) ::1:8822 refcount 4 -> 3
D 2024-08-20T07:28:21.529Z | v1.10.1 93519 | subchannel_refcount | (3) 127.0.0.1:8822 refcount 3 -> 2
D 2024-08-20T07:28:21.529Z | v1.10.1 93519 | pick_first | TRANSIENT_FAILURE -> READY
D 2024-08-20T07:28:21.529Z | v1.10.1 93519 | resolving_load_balancer | dns:localhost:8822 TRANSIENT_FAILURE -> READY
D 2024-08-20T07:28:21.529Z | v1.10.1 93519 | connectivity_state | (1) dns:localhost:8822 TRANSIENT_FAILURE -> READY
D 2024-08-20T07:28:21.529Z | v1.10.1 93519 | pick_first | Pick subchannel with address ::1:8822
D 2024-08-20T07:28:21.530Z | v1.10.1 93519 | subchannel_refcount | (2) ::1:8822 refcount 3 -> 4
D 2024-08-20T07:28:21.530Z | v1.10.1 93519 | subchannel_refcount | (2) ::1:8822 refcount 4 -> 3
D 2024-08-20T07:28:21.530Z | v1.10.1 93519 | subchannel_refcount | (3) 127.0.0.1:8822 refcount 2 -> 1
D 2024-08-20T07:28:21.530Z | v1.10.1 93519 | pick_first | TRANSIENT_FAILURE -> READY
D 2024-08-20T07:28:21.530Z | v1.10.1 93519 | resolving_load_balancer | dns:localhost:8822 TRANSIENT_FAILURE -> READY
D 2024-08-20T07:28:21.530Z | v1.10.1 93519 | connectivity_state | (4) dns:localhost:8822 TRANSIENT_FAILURE -> READY
HTTP2 93519: Http2Session client: settings received
D 2024-08-20T07:28:21.588Z | v1.10.1 93519 | transport | (5) ::1:8822 local settings acknowledged by remote: {"headerTableSize":4096,"enablePush":true,"initialWindowSize":65535,"maxFrameSize":16384,"maxConcurrentStreams":4294967295,"maxHeaderListSize":4294967295,"maxHeaderSize":4294967295,"enableConnectProtocol":false}
D 2024-08-20T07:28:21.783Z | v1.10.1 93519 | dns_resolver | resolution update delayed by "min time between resolutions" rate limit
D 2024-08-20T07:28:22.129Z | v1.10.1 93519 | subchannel | (3) 127.0.0.1:8822 TRANSIENT_FAILURE -> CONNECTING
D 2024-08-20T07:28:22.129Z | v1.10.1 93519 | transport | dns:localhost:8822 creating HTTP/2 session to 127.0.0.1:8822
HTTP2 93519: Http2Session client: created
HTTP2 93519: Http2Session client: setting up session handle
HTTP2 93519: Http2Session client: sending settings
HTTP2 93519: Http2Session client: submitting settings
D 2024-08-20T07:28:22.132Z | v1.10.1 93519 | subchannel | (3) 127.0.0.1:8822 CONNECTING -> READY
HTTP2 93519: Http2Session client: settings received
D 2024-08-20T07:28:22.137Z | v1.10.1 93519 | transport | (6) 127.0.0.1:8822 local settings acknowledged by remote: {"headerTableSize":4096,"enablePush":true,"initialWindowSize":65535,"maxFrameSize":16384,"maxConcurrentStreams":4294967295,"maxHeaderListSize":4294967295,"maxHeaderSize":4294967295,"enableConnectProtocol":false}
D 2024-08-20T07:28:22.496Z | v1.10.1 93519 | channel | (4) dns:localhost:8822 createResolvingCall [3] method="/grpc.reflection.v1alpha.ServerReflection/ServerReflectionInfo", deadline=Infinity
D 2024-08-20T07:28:22.497Z | v1.10.1 93519 | resolving_call | [3] Created
D 2024-08-20T07:28:22.497Z | v1.10.1 93519 | resolving_call | [3] Deadline: Infinity
D 2024-08-20T07:28:22.497Z | v1.10.1 93519 | resolving_call | [3] start called
D 2024-08-20T07:28:22.499Z | v1.10.1 93519 | resolving_call | [3] write() called with message of length 30
D 2024-08-20T07:28:22.499Z | v1.10.1 93519 | channel | (4) dns:localhost:8822 createRetryingCall [4] method="/grpc.reflection.v1alpha.ServerReflection/ServerReflectionInfo"
D 2024-08-20T07:28:22.499Z | v1.10.1 93519 | resolving_call | [3] Created child [4]
D 2024-08-20T07:28:22.499Z | v1.10.1 93519 | retrying_call | [4] start called
D 2024-08-20T07:28:22.499Z | v1.10.1 93519 | channel | (4) dns:localhost:8822 createLoadBalancingCall [5] method="/grpc.reflection.v1alpha.ServerReflection/ServerReflectionInfo"
D 2024-08-20T07:28:22.499Z | v1.10.1 93519 | retrying_call | [4] Created child call [5] for attempt 1
D 2024-08-20T07:28:22.499Z | v1.10.1 93519 | load_balancing_call | [5] start called
D 2024-08-20T07:28:22.499Z | v1.10.1 93519 | load_balancing_call | [5] Pick called
D 2024-08-20T07:28:22.499Z | v1.10.1 93519 | load_balancing_call | [5] Pick result: COMPLETE subchannel: (2) ::1:8822 status: undefined undefined
HTTP2 93519: Http2Session client: initiating request
HTTP2 93519: Http2Session client: connected, initializing request
D 2024-08-20T07:28:22.502Z | v1.10.1 93519 | transport_flowctrl | (5) ::1:8822 local window size: 65535 remote window size: 1048576
D 2024-08-20T07:28:22.502Z | v1.10.1 93519 | transport_internals | (5) ::1:8822 session.closed=false session.destroyed=false session.socket.destroyed=false
D 2024-08-20T07:28:22.503Z | v1.10.1 93519 | load_balancing_call | [5] Created child call [6]
D 2024-08-20T07:28:22.503Z | v1.10.1 93519 | retrying_call | [4] write() called with message of length 35
D 2024-08-20T07:28:22.503Z | v1.10.1 93519 | load_balancing_call | [5] write() called with message of length 35
D 2024-08-20T07:28:22.503Z | v1.10.1 93519 | subchannel_call | [6] write() called with message of length 35
D 2024-08-20T07:28:22.503Z | v1.10.1 93519 | subchannel_call | [6] sending data chunk of length 35
D 2024-08-20T07:28:22.503Z | v1.10.1 93519 | resolving_call | [3] startRead called
D 2024-08-20T07:28:22.503Z | v1.10.1 93519 | retrying_call | [4] startRead called
D 2024-08-20T07:28:22.503Z | v1.10.1 93519 | load_balancing_call | [5] startRead called
HTTP2 93519: Http2Stream 1 [Http2Session client]: headers received
HTTP2 93519: Http2Stream 1 [Http2Session client]: emitting stream 'response' event
D 2024-08-20T07:28:22.539Z | v1.10.1 93519 | subchannel_call | [6] Received server headers:
                :status: 200
                content-type: application/grpc
                grpc-encoding: identity
                grpc-accept-encoding: gzip

D 2024-08-20T07:28:22.540Z | v1.10.1 93519 | load_balancing_call | [5] Received metadata
D 2024-08-20T07:28:22.540Z | v1.10.1 93519 | retrying_call | [4] Received metadata from child [5]
D 2024-08-20T07:28:22.540Z | v1.10.1 93519 | retrying_call | [4] Committing call [5] at index 0
D 2024-08-20T07:28:22.540Z | v1.10.1 93519 | resolving_call | [3] Received metadata
D 2024-08-20T07:28:22.540Z | v1.10.1 93519 | subchannel_call | [6] receive HTTP/2 data frame of length 881
D 2024-08-20T07:28:22.540Z | v1.10.1 93519 | subchannel_call | [6] parsed message of length 881
D 2024-08-20T07:28:22.540Z | v1.10.1 93519 | subchannel_call | [6] pushing to reader message of length 881
D 2024-08-20T07:28:22.541Z | v1.10.1 93519 | load_balancing_call | [5] Received message
D 2024-08-20T07:28:22.541Z | v1.10.1 93519 | retrying_call | [4] Received message from child [5]
D 2024-08-20T07:28:22.541Z | v1.10.1 93519 | resolving_call | [3] Received message
D 2024-08-20T07:28:22.541Z | v1.10.1 93519 | resolving_call | [3] Finished filtering received message
D 2024-08-20T07:28:22.542Z | v1.10.1 93519 | resolving_call | [3] halfClose called
D 2024-08-20T07:28:22.542Z | v1.10.1 93519 | retrying_call | [4] halfClose called
D 2024-08-20T07:28:22.542Z | v1.10.1 93519 | load_balancing_call | [5] halfClose called
D 2024-08-20T07:28:22.542Z | v1.10.1 93519 | subchannel_call | [6] end() called
D 2024-08-20T07:28:22.542Z | v1.10.1 93519 | subchannel_call | [6] calling end() on HTTP/2 stream
HTTP2 93519: Http2Stream 1 [Http2Session client]: shutting down writable on _final
D 2024-08-20T07:28:22.547Z | v1.10.1 93519 | resolving_load_balancer | dns:localhost:8822 IDLE -> IDLE
D 2024-08-20T07:28:22.547Z | v1.10.1 93519 | connectivity_state | (7) dns:localhost:8822 IDLE -> IDLE
D 2024-08-20T07:28:22.547Z | v1.10.1 93519 | dns_resolver | Resolver constructed for target dns:localhost:8822
D 2024-08-20T07:28:22.547Z | v1.10.1 93519 | channel | (7) dns:localhost:8822 Channel constructed with options {
  "grpc.max_receive_message_length": 1073741824,
  "grpc.max_send_message_length": 1073741824
}
D 2024-08-20T07:28:22.548Z | v1.10.1 93519 | channel_stacktrace | (7) Channel constructed
    at new InternalChannel (/Users/romac/Informal/Code/quint/quint/node_modules/@grpc/grpc-js/build/src/internal-channel.js:248:23)
    at new ChannelImplementation (/Users/romac/Informal/Code/quint/quint/node_modules/@grpc/grpc-js/build/src/channel.js:35:32)
    at new Client (/Users/romac/Informal/Code/quint/quint/node_modules/@grpc/grpc-js/build/src/client.js:65:36)
    at new ServiceClientImpl (/Users/romac/Informal/Code/quint/quint/node_modules/@grpc/grpc-js/build/src/make-client.js:58:5)
    at loadGrpcClient (/Users/romac/Informal/Code/quint/quint/dist/src/apalache.js:222:18)
    at /Users/romac/Informal/Code/quint/quint/dist/src/apalache.js:240:26
    at EitherConstructor.map (/Users/romac/Informal/Code/quint/quint/node_modules/@sweet-monads/either/cjs/index.js:75:40)
    at tryConnect (/Users/romac/Informal/Code/quint/quint/dist/src/apalache.js:240:10)
    at process.processTicksAndRejections (node:internal/process/task_queues:95:5)
    at async verify (/Users/romac/Informal/Code/quint/quint/dist/src/quintVerifier.js:31:30)
D 2024-08-20T07:28:22.552Z | v1.10.1 93519 | channel | (7) dns:localhost:8822 createResolvingCall [7] method="/shai.cmdExecutor.CmdExecutor/run", deadline=Infinity
D 2024-08-20T07:28:22.552Z | v1.10.1 93519 | resolving_call | [7] Created
D 2024-08-20T07:28:22.552Z | v1.10.1 93519 | resolving_call | [7] Deadline: Infinity
D 2024-08-20T07:28:22.552Z | v1.10.1 93519 | resolving_call | [7] start called
D 2024-08-20T07:28:22.552Z | v1.10.1 93519 | dns_resolver | Looking up DNS hostname localhost
D 2024-08-20T07:28:22.552Z | v1.10.1 93519 | resolving_load_balancer | dns:localhost:8822 IDLE -> CONNECTING
D 2024-08-20T07:28:22.552Z | v1.10.1 93519 | connectivity_state | (7) dns:localhost:8822 IDLE -> CONNECTING
D 2024-08-20T07:28:22.552Z | v1.10.1 93519 | channel | (7) dns:localhost:8822 callRefTimer.ref | configSelectionQueue.length=1 pickQueue.length=0
D 2024-08-20T07:28:22.552Z | v1.10.1 93519 | resolving_call | [7] startRead called
D 2024-08-20T07:28:22.555Z | v1.10.1 93519 | resolving_call | [7] write() called with message of length 1228671
D 2024-08-20T07:28:22.555Z | v1.10.1 93519 | resolving_call | [7] halfClose called
D 2024-08-20T07:28:22.555Z | v1.10.1 93519 | resolving_call | [3] startRead called
D 2024-08-20T07:28:22.555Z | v1.10.1 93519 | retrying_call | [4] startRead called
D 2024-08-20T07:28:22.555Z | v1.10.1 93519 | load_balancing_call | [5] startRead called
D 2024-08-20T07:28:22.555Z | v1.10.1 93519 | dns_resolver | Resolved addresses for target dns:localhost:8822: [::1:8822,127.0.0.1:8822]
D 2024-08-20T07:28:22.555Z | v1.10.1 93519 | subchannel | (8) ::1:8822 Subchannel constructed with options {
  "grpc.max_receive_message_length": 1073741824,
  "grpc.max_send_message_length": 1073741824
}
D 2024-08-20T07:28:22.555Z | v1.10.1 93519 | subchannel_refcount | (8) ::1:8822 refcount 0 -> 1
D 2024-08-20T07:28:22.555Z | v1.10.1 93519 | subchannel | (9) 127.0.0.1:8822 Subchannel constructed with options {
  "grpc.max_receive_message_length": 1073741824,
  "grpc.max_send_message_length": 1073741824
}
D 2024-08-20T07:28:22.555Z | v1.10.1 93519 | subchannel_refcount | (9) 127.0.0.1:8822 refcount 0 -> 1
D 2024-08-20T07:28:22.555Z | v1.10.1 93519 | subchannel_refcount | (8) ::1:8822 refcount 1 -> 2
D 2024-08-20T07:28:22.555Z | v1.10.1 93519 | subchannel_refcount | (9) 127.0.0.1:8822 refcount 1 -> 2
D 2024-08-20T07:28:22.555Z | v1.10.1 93519 | pick_first | Start connecting to subchannel with address ::1:8822
D 2024-08-20T07:28:22.555Z | v1.10.1 93519 | pick_first | IDLE -> CONNECTING
D 2024-08-20T07:28:22.555Z | v1.10.1 93519 | resolving_load_balancer | dns:localhost:8822 CONNECTING -> CONNECTING
D 2024-08-20T07:28:22.555Z | v1.10.1 93519 | connectivity_state | (7) dns:localhost:8822 CONNECTING -> CONNECTING
D 2024-08-20T07:28:22.555Z | v1.10.1 93519 | channel | (7) dns:localhost:8822 callRefTimer.unref | configSelectionQueue.length=0 pickQueue.length=0
D 2024-08-20T07:28:22.555Z | v1.10.1 93519 | subchannel | (8) ::1:8822 IDLE -> CONNECTING
D 2024-08-20T07:28:22.555Z | v1.10.1 93519 | transport | dns:localhost:8822 creating HTTP/2 session to ::1:8822
HTTP2 93519: Http2Session client: created
D 2024-08-20T07:28:22.556Z | v1.10.1 93519 | channel | (7) dns:localhost:8822 createRetryingCall [8] method="/shai.cmdExecutor.CmdExecutor/run"
D 2024-08-20T07:28:22.556Z | v1.10.1 93519 | resolving_call | [7] Created child [8]
D 2024-08-20T07:28:22.556Z | v1.10.1 93519 | retrying_call | [8] start called
D 2024-08-20T07:28:22.556Z | v1.10.1 93519 | channel | (7) dns:localhost:8822 createLoadBalancingCall [9] method="/shai.cmdExecutor.CmdExecutor/run"
D 2024-08-20T07:28:22.556Z | v1.10.1 93519 | retrying_call | [8] Created child call [9] for attempt 1
D 2024-08-20T07:28:22.556Z | v1.10.1 93519 | load_balancing_call | [9] start called
D 2024-08-20T07:28:22.556Z | v1.10.1 93519 | load_balancing_call | [9] Pick called
D 2024-08-20T07:28:22.556Z | v1.10.1 93519 | load_balancing_call | [9] Pick result: QUEUE subchannel: null status: undefined undefined
D 2024-08-20T07:28:22.556Z | v1.10.1 93519 | channel | (7) dns:localhost:8822 callRefTimer.ref | configSelectionQueue.length=0 pickQueue.length=1
D 2024-08-20T07:28:22.556Z | v1.10.1 93519 | retrying_call | [8] startRead called
D 2024-08-20T07:28:22.556Z | v1.10.1 93519 | load_balancing_call | [9] startRead called
D 2024-08-20T07:28:22.556Z | v1.10.1 93519 | retrying_call | [8] write() called with message of length 1228676
D 2024-08-20T07:28:22.556Z | v1.10.1 93519 | retrying_call | [8] Committing call [9] at index 0
D 2024-08-20T07:28:22.556Z | v1.10.1 93519 | load_balancing_call | [9] write() called with message of length 1228676
D 2024-08-20T07:28:22.556Z | v1.10.1 93519 | retrying_call | [8] halfClose called
HTTP2 93519: Http2Stream 1 [Http2Session client]: headers received
HTTP2 93519: Http2Stream 1 [Http2Session client]: emitting stream 'trailers' event
D 2024-08-20T07:28:22.557Z | v1.10.1 93519 | subchannel_call | [6] Received server trailers:
                grpc-status: 0

D 2024-08-20T07:28:22.557Z | v1.10.1 93519 | subchannel_call | [6] received status code 0 from server
D 2024-08-20T07:28:22.557Z | v1.10.1 93519 | subchannel_call | [6] close http2 stream with code 0
D 2024-08-20T07:28:22.557Z | v1.10.1 93519 | subchannel_call | [6] ended with status: code=0 details=""
D 2024-08-20T07:28:22.557Z | v1.10.1 93519 | load_balancing_call | [5] Received status
D 2024-08-20T07:28:22.557Z | v1.10.1 93519 | load_balancing_call | [5] ended with status: code=0 details=""
D 2024-08-20T07:28:22.557Z | v1.10.1 93519 | retrying_call | [4] Received status from child [5]
D 2024-08-20T07:28:22.557Z | v1.10.1 93519 | retrying_call | [4] state=COMMITTED handling status with progress PROCESSED from child [5] in state ACTIVE
D 2024-08-20T07:28:22.557Z | v1.10.1 93519 | retrying_call | [4] ended with status: code=0 details=""
D 2024-08-20T07:28:22.557Z | v1.10.1 93519 | resolving_call | [3] Received status
D 2024-08-20T07:28:22.557Z | v1.10.1 93519 | resolving_call | [3] ended with status: code=0 details=""
HTTP2 93519: Http2Stream 1 [Http2Session client]: closed with code 0, closed true, readable false
HTTP2 93519: Http2Stream 1 [Http2Session client]: destroying stream
D 2024-08-20T07:28:22.558Z | v1.10.1 93519 | subchannel_call | [6] HTTP/2 stream closed with code 0
HTTP2 93519: Http2Session client: setting up session handle
HTTP2 93519: Http2Session client: sending settings
HTTP2 93519: Http2Session client: submitting settings
D 2024-08-20T07:28:22.558Z | v1.10.1 93519 | subchannel | (8) ::1:8822 CONNECTING -> READY
D 2024-08-20T07:28:22.558Z | v1.10.1 93519 | pick_first | Pick subchannel with address ::1:8822
D 2024-08-20T07:28:22.558Z | v1.10.1 93519 | subchannel_refcount | (8) ::1:8822 refcount 2 -> 3
D 2024-08-20T07:28:22.558Z | v1.10.1 93519 | subchannel_refcount | (8) ::1:8822 refcount 3 -> 2
D 2024-08-20T07:28:22.558Z | v1.10.1 93519 | subchannel_refcount | (9) 127.0.0.1:8822 refcount 2 -> 1
D 2024-08-20T07:28:22.558Z | v1.10.1 93519 | pick_first | CONNECTING -> READY
D 2024-08-20T07:28:22.558Z | v1.10.1 93519 | resolving_load_balancer | dns:localhost:8822 CONNECTING -> READY
D 2024-08-20T07:28:22.558Z | v1.10.1 93519 | channel | (7) dns:localhost:8822 callRefTimer.unref | configSelectionQueue.length=0 pickQueue.length=0
D 2024-08-20T07:28:22.558Z | v1.10.1 93519 | load_balancing_call | [9] Pick called
D 2024-08-20T07:28:22.558Z | v1.10.1 93519 | load_balancing_call | [9] Pick result: COMPLETE subchannel: (8) ::1:8822 status: undefined undefined
D 2024-08-20T07:28:22.558Z | v1.10.1 93519 | connectivity_state | (7) dns:localhost:8822 CONNECTING -> READY
HTTP2 93519: Http2Session client: initiating request
HTTP2 93519: Http2Session client: connected, initializing request
D 2024-08-20T07:28:22.558Z | v1.10.1 93519 | transport_flowctrl | (10) ::1:8822 local window size: 65535 remote window size: 65535
D 2024-08-20T07:28:22.558Z | v1.10.1 93519 | transport_internals | (10) ::1:8822 session.closed=false session.destroyed=false session.socket.destroyed=false
D 2024-08-20T07:28:22.558Z | v1.10.1 93519 | load_balancing_call | [9] Created child call [10]
D 2024-08-20T07:28:22.558Z | v1.10.1 93519 | subchannel_call | [10] write() called with message of length 1228676
D 2024-08-20T07:28:22.559Z | v1.10.1 93519 | subchannel_call | [10] sending data chunk of length 1228676
HTTP2 93519: Http2Session client: settings received
D 2024-08-20T07:28:22.563Z | v1.10.1 93519 | transport | (10) ::1:8822 local settings acknowledged by remote: {"headerTableSize":4096,"enablePush":true,"initialWindowSize":65535,"maxFrameSize":16384,"maxConcurrentStreams":4294967295,"maxHeaderListSize":4294967295,"maxHeaderSize":4294967295,"enableConnectProtocol":false}
D 2024-08-20T07:28:22.564Z | v1.10.1 93519 | load_balancing_call | [9] halfClose called
D 2024-08-20T07:28:22.564Z | v1.10.1 93519 | subchannel_call | [10] end() called
D 2024-08-20T07:28:22.564Z | v1.10.1 93519 | subchannel_call | [10] calling end() on HTTP/2 stream
HTTP2 93519: Http2Stream 1 [Http2Session client]: shutting down writable on _final
PASS #0: SanyParser                                               I@09:28:22.940
HTTP2 93519: Http2Stream 1 [Http2Session client]: headers received
HTTP2 93519: Http2Stream 1 [Http2Session client]: emitting stream 'response' event
D 2024-08-20T07:28:23.323Z | v1.10.1 93519 | subchannel_call | [10] Received server headers:
                :status: 200
                content-type: application/grpc
                grpc-encoding: identity
                grpc-accept-encoding: gzip

D 2024-08-20T07:28:23.323Z | v1.10.1 93519 | load_balancing_call | [9] Received metadata
D 2024-08-20T07:28:23.324Z | v1.10.1 93519 | retrying_call | [8] Received metadata from child [9]
D 2024-08-20T07:28:23.324Z | v1.10.1 93519 | resolving_call | [7] Received metadata
HTTP2 93519: Http2Stream 1 [Http2Session client]: headers received
HTTP2 93519: Http2Stream 1 [Http2Session client]: emitting stream 'trailers' event
D 2024-08-20T07:28:23.324Z | v1.10.1 93519 | subchannel_call | [10] Received server trailers:
                grpc-status: 13

D 2024-08-20T07:28:23.324Z | v1.10.1 93519 | subchannel_call | [10] received status code 13 from server
D 2024-08-20T07:28:23.324Z | v1.10.1 93519 | subchannel_call | [10] ended with status: code=13 details=""
D 2024-08-20T07:28:23.324Z | v1.10.1 93519 | subchannel_call | [10] close http2 stream with code 8
D 2024-08-20T07:28:23.324Z | v1.10.1 93519 | load_balancing_call | [9] Received status
D 2024-08-20T07:28:23.324Z | v1.10.1 93519 | load_balancing_call | [9] ended with status: code=13 details=""
D 2024-08-20T07:28:23.324Z | v1.10.1 93519 | retrying_call | [8] Received status from child [9]
D 2024-08-20T07:28:23.324Z | v1.10.1 93519 | retrying_call | [8] state=COMMITTED handling status with progress PROCESSED from child [9] in state ACTIVE
D 2024-08-20T07:28:23.324Z | v1.10.1 93519 | retrying_call | [8] ended with status: code=13 details=""
D 2024-08-20T07:28:23.324Z | v1.10.1 93519 | resolving_call | [7] Received status
D 2024-08-20T07:28:23.324Z | v1.10.1 93519 | resolving_call | [7] ended with status: code=13 details=""
quint verify <input>

Verify a Quint specification via Apalache

Options:
  --help                Show help                                      [boolean]
  --version             Show version number                            [boolean]
  --out                 output file (suppresses all console output)     [string]
  --main                name of the main module (by default, computed from
                        filename)                                       [string]
  --init                name of the initializer action[string] [default: "init"]
  --step                name of the step action       [string] [default: "step"]
  --invariant           the invariants to check, separated by commas (e.g.)
                                                                        [string]
  --temporal            the temporal properties to check, separated by commas
                                                                        [string]
  --out-itf             output the trace in the Informal Trace Format to file
                        (suppresses all console output)                 [string]
  --max-steps           the maximum number of steps in every trace
                                                          [number] [default: 10]
  --random-transitions  choose transitions at random (= use symbolic simulation)
                                                      [boolean] [default: false]
  --apalache-config     path to an additional Apalache configuration file (in
                        JSON)                                           [string]
  --verbosity           control how much output is produced (0 to 5)
                                                           [number] [default: 2]
  --server-endpoint     Apalache server endpoint hostname:port
                                            [string] [default: "localhost:8822"]

Error: 13 INTERNAL:
    at callErrorFromStatus (/Users/romac/Informal/Code/quint/quint/node_modules/@grpc/grpc-js/build/src/call.js:31:19)
    at Object.onReceiveStatus (/Users/romac/Informal/Code/quint/quint/node_modules/@grpc/grpc-js/build/src/client.js:192:76)
    at Object.onReceiveStatus (/Users/romac/Informal/Code/quint/quint/node_modules/@grpc/grpc-js/build/src/client-interceptors.js:360:141)
    at Object.onReceiveStatus (/Users/romac/Informal/Code/quint/quint/node_modules/@grpc/grpc-js/build/src/client-interceptors.js:323:181)
    at /Users/romac/Informal/Code/quint/quint/node_modules/@grpc/grpc-js/build/src/resolving-call.js:99:78
    at process.processTicksAndRejections (node:internal/process/task_queues:77:11)
for call at
    at ServiceClientImpl.makeUnaryRequest (/Users/romac/Informal/Code/quint/quint/node_modules/@grpc/grpc-js/build/src/client.js:160:32)
    at ServiceClientImpl.run (/Users/romac/Informal/Code/quint/quint/node_modules/@grpc/grpc-js/build/src/make-client.js:105:19)
    at Object.<anonymous> (/Users/romac/Informal/Code/quint/quint/dist/src/apalache.js:224:55)
    at node:internal/util:431:7
    at new Promise (<anonymous>)
    at Object.run (node:internal/util:417:12)
    at Object.check (/Users/romac/Informal/Code/quint/quint/dist/src/apalache.js:147:28)
    at /Users/romac/Informal/Code/quint/quint/dist/src/quintVerifier.js:32:53
    at EitherConstructor.asyncChain (/Users/romac/Informal/Code/quint/quint/node_modules/@sweet-monads/either/cjs/index.js:125:16)
    at verify (/Users/romac/Informal/Code/quint/quint/dist/src/quintVerifier.js:32:29) {
  code: 13,
  details: '',
  metadata: Metadata { internalRepr: Map(0) {}, options: {} }
}

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Assignees
No one assigned
Labels
None yet
Projects
None yet
Milestone
No milestone
Development

No branches or pull requests
2 participants
@romac @konnov