Getting Started tutorial should refer to a local installation as well

[MarceColl]

Hi!

From lobste.rs I was told to post here, hopefully I haven't made a very dumb mistake.

I followed the Getting Started tutorial and I never got the expected violation both with the simulator and with the validator.

Steps I followed:

• Installed the package in a local folder (I cannot install globally)

  $ npm init
  $ npm i @informalsystems/quint

• Created a new file bank.qnt with the following value

  module bank {
  /// A state variable to store the balance of each account
  var balances: str -> int
  
  pure val ADDRESSES = Set("alice", "bob", "charlie")
  
  action deposit(account, amount) = {
  // Increment balance of account by amount
  balances' = balances.setBy(account, curr => curr + amount)
  }
  
  action withdraw(account, amount) = {
  // Decrement balance of account by amount
  balances' = balances.setBy(account, curr => curr - amount)
  }
  
  action init = {
  // At the initial state, all balances are zero
  balances' = ADDRESSES.mapBy(_ => 0)
  }
  
  action step = {
  // Non-deterministically pick an address and an amount
  nondet account = ADDRESSES.oneOf()
  nondet amount = 1.to(100).oneOf()
  // Non-deterministically choose to either deposit or withdraw
  any {
    deposit(account, amount),
    withdraw(account, amount),
  }
  }
  
  /// An invariant stating that all accounts should have a non-negative balance
  val no_negatives = ADDRESSES.forall(addr => balances.get(addr) >= 0)
  }

Then I ran the command as specified in the tutorial, but prefixed with npm exec

[marcecoll@nixos:~/proj/quint]$ npm exec quint run bank.qnt --invariant=no_negatives
An example execution:

[State 0] { balances: Map("alice" -> 0, "bob" -> 0, "charlie" -> 0) }

[State 1] { balances: Map("alice" -> 0, "bob" -> 0, "charlie" -> -43) }

[State 2] { balances: Map("alice" -> 100, "bob" -> 0, "charlie" -> -43) }

[State 3] { balances: Map("alice" -> 100, "bob" -> 0, "charlie" -> 13) }

[State 4] { balances: Map("alice" -> 100, "bob" -> 88, "charlie" -> 13) }

[State 5] { balances: Map("alice" -> 163, "bob" -> 88, "charlie" -> 13) }

[State 6] { balances: Map("alice" -> 163, "bob" -> 88, "charlie" -> 80) }

[State 7] { balances: Map("alice" -> 229, "bob" -> 88, "charlie" -> 80) }

[State 8] { balances: Map("alice" -> 229, "bob" -> 88, "charlie" -> 46) }

[State 9] { balances: Map("alice" -> 297, "bob" -> 88, "charlie" -> 46) }

[State 10] { balances: Map("alice" -> 297, "bob" -> 88, "charlie" -> -10) }

[State 11] { balances: Map("alice" -> 358, "bob" -> 88, "charlie" -> -10) }

[State 12] { balances: Map("alice" -> 305, "bob" -> 88, "charlie" -> -10) }

[State 13] { balances: Map("alice" -> 305, "bob" -> 88, "charlie" -> -28) }

[State 14] { balances: Map("alice" -> 305, "bob" -> 60, "charlie" -> -28) }

[State 15] { balances: Map("alice" -> 337, "bob" -> 60, "charlie" -> -28) }

[State 16] { balances: Map("alice" -> 337, "bob" -> 60, "charlie" -> -34) }

[State 17] { balances: Map("alice" -> 337, "bob" -> -36, "charlie" -> -34) }

[State 18] { balances: Map("alice" -> 340, "bob" -> -36, "charlie" -> -34) }

[State 19] { balances: Map("alice" -> 268, "bob" -> -36, "charlie" -> -34) }

[State 20] { balances: Map("alice" -> 268, "bob" -> -29, "charlie" -> -34) }

[ok] No violation found (3338ms).
Use --seed=0x24e8cb9731f2f to reproduce.
You may increase --max-samples and --max-steps.
Use --verbosity to produce more (or less) output

I thought maybe the simulator didn't test negative values, but the states clearly contain them. Just in case I tried verify

[marcecoll@nixos:~/proj/quint]$ npm exec quint verify bank.qnt --invariant=no_negatives
22:29:48.131 [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: /home/marcecoll/proj/quint/_apalache-out/server/2024-07-31T22-29-48_8519968159157359427
# APALACHE version: 0.44.11 | build: 5dee24e                      I@22:29:48.440
Starting server on port 8822...                                   I@22:29:48.448
The Apalache server is running on port 8822. Press Ctrl-C to stop.
PASS #0: SanyParser                                               I@22:29:52.059
PASS #1: TypeCheckerSnowcat                                       I@22:29:52.305
 > Running Snowcat .::.                                           I@22:29:52.306
 > Your types are purrfect!                                       I@22:29:52.406
 > All expressions are typed                                      I@22:29:52.406
PASS #2: ConfigurationPass                                        I@22:29:52.407
  > Set the initialization predicate to q::init                   I@22:29:52.409
  > Set the transition predicate to q::step                       I@22:29:52.409
PASS #3: DesugarerPass                                            I@22:29:52.413
  > Desugaring...                                                 I@22:29:52.413
PASS #4: InlinePass                                               I@22:29:52.422
Leaving only relevant operators: CInitPrimed, q::init, q::initPrimed, q::step I@22:29:52.422
PASS #5: TemporalPass                                             I@22:29:52.449
  > Rewriting temporal operators...                               I@22:29:52.449
  > No temporal property specified, nothing to encode             I@22:29:52.449
PASS #6: InlinePass                                               I@22:29:52.449
Leaving only relevant operators: CInitPrimed, q::init, q::initPrimed, q::step I@22:29:52.449
PASS #7: PrimingPass                                              I@22:29:52.452
  > Introducing q::initPrimed for q::init'                        I@22:29:52.453
PASS #8: VCGen                                                    I@22:29:52.454
  > No invariant given. Only deadlocks will be checked            I@22:29:52.454
PASS #9: PreprocessingPass                                        I@22:29:52.454
  > Before preprocessing: unique renaming                         I@22:29:52.454
 > Applying standard transformations:                             I@22:29:52.458
  > PrimePropagation                                              I@22:29:52.459
  > Desugarer                                                     I@22:29:52.460
  > UniqueRenamer                                                 I@22:29:52.461
  > Normalizer                                                    I@22:29:52.462
  > Keramelizer                                                   I@22:29:52.465
  > After preprocessing: UniqueRenamer                            I@22:29:52.467
PASS #10: TransitionFinderPass                                    I@22:29:52.475
  > Found 1 initializing transitions                              I@22:29:52.483
  > Found 2 transitions                                           I@22:29:52.485
  > No constant initializer                                       I@22:29:52.486
  > Applying unique renaming                                      I@22:29:52.486
PASS #11: OptimizationPass                                        I@22:29:52.488
 > Applying optimizations:                                        I@22:29:52.492
  > ConstSimplifier                                               I@22:29:52.493
  > ExprOptimizer                                                 I@22:29:52.494
  > SetMembershipSimplifier                                       I@22:29:52.495
  > ConstSimplifier                                               I@22:29:52.495
PASS #12: AnalysisPass                                            I@22:29:52.497
 > Marking skolemizable existentials and sets to be expanded...   I@22:29:52.500
  > Skolemization                                                 I@22:29:52.500
  > Expansion                                                     I@22:29:52.500
  > Remove unused let-in defs                                     I@22:29:52.501
 > Running analyzers...                                           I@22:29:52.503
  > Introduced expression grades                                  I@22:29:52.504
PASS #13: BoundedChecker                                          I@22:29:52.504
Step 0: picking a transition out of 1 transition(s)               I@22:29:52.735
Step 1: picking a transition out of 2 transition(s)               I@22:29:52.791
Step 2: picking a transition out of 2 transition(s)               I@22:29:52.830
Step 3: picking a transition out of 2 transition(s)               I@22:29:52.862
Step 4: picking a transition out of 2 transition(s)               I@22:29:52.892
Step 5: picking a transition out of 2 transition(s)               I@22:29:52.918
Step 6: picking a transition out of 2 transition(s)               I@22:29:52.939
Step 7: picking a transition out of 2 transition(s)               I@22:29:52.964
Step 8: picking a transition out of 2 transition(s)               I@22:29:52.987
Step 9: picking a transition out of 2 transition(s)               I@22:29:53.014
Step 10: picking a transition out of 2 transition(s)              I@22:29:53.047
The outcome is: NoError                                           I@22:29:53.056
[ok] No violation found (5358ms).
You may increase --max-steps.
Use --verbosity to produce more (or less) output.

Some info

[marcecoll@nixos:~/proj/quint]$ npm exec quint -v
10.5.0

[marcecoll@nixos:~/proj/quint]$ node -v
v20.12.2

[marcecoll@nixos:~/proj/quint]$ java -version
openjdk version "21" 2023-09-19
OpenJDK Runtime Environment (build 21+35-nixos)
OpenJDK 64-Bit Server VM (build 21+35-nixos, mixed mode, sharing)

[marcecoll@nixos:~/proj/quint]$ npm -v
10.5.0

[MarceColl]

Actually just after submitting I realized that npm exec quint -v gives the same version as npm -v, so it seems that it consumes npm exec consumes arguments in a weird way.

By running it as npm exec quint verify bank.qnt -- --invariant=no_negatives it does correctly find a violation as expected.

I'm leaving the issue open in case you wanna add something in the docs about this for people that run it from inside a project.

[bugarela]

Ah, great that you found the issue! The npm exec quint -v result was the first thing I spotted, since we are currently at 0.21.1.

I'll add a :bulb: warning in the getting started guide with the proper command for people running it with a local installation. I've used that many times before, but always with npx, so it doesn't have this problem:

npx quint verify bank.qnt --invariant=no_negatives

Thanks for the detailed reporting!

I'll just change the title of this issue so it matches your new request.