New instances syntax

CHANGELOG.md

@@ -16,11 +16,15 @@ and this project adheres to [Semantic Versioning](https://semver.org/spec/v2.0.0
 - save the run results to ITF (#727)
 
 ### Changed
+
+- The syntax for instances is now similar to imports (#739)
+
 ### Deprecated
 ### Removed
 ### Fixed
 
 - Heisenbugs in `nondet x = oneOf(S)` should not happen (#712)
+- REPL doesn't show unecessary namespaces for variable names anymore (#739)
 
 ### Security
 

examples/classic/distributed/Paxos/Paxos.qnt

@@ -1,6 +1,10 @@
 // -*- mode: Bluespec; -*-
 // Temp fix for integration tests: mock voting definitions while files are not imported
 module Voting {
+  const Value: Set[int]       // The set of choosable values.
+  const Acceptor: Set[str]    // A set of processes that will choose a value.
+  const Quorum: Set[Set[str]] // The set of "quorums", where a quorum" is a
+
   def ShowsSafeAt(Q, b, v) = true
   val Inv = true
 }
@@ -240,7 +244,7 @@ module Paxos {
   (***************************************************************************/
 
 
-  module V = Voting(*)
+  import Voting(Value = Value, Acceptor = Acceptor, Quorum = Quorum) as V
 
   // Like theorems? Then you should definitely go straight for TLA+
   // THEOREM Spec => V!Spec

examples/cosmos/tendermint/TendermintAcc005.qnt

@@ -660,9 +660,11 @@ module TendermintAcc {
       val AllDecided = Corr.forall(p => decision.get(p) != NilValue)
       AllInMax implies AllDecided
   )
+}
 
-
-  // Tests that demonstrate typical behavior.
+// Tests that demonstrate typical behavior.
+module TendermintTest {
+  import TendermintAcc.*
 
   // Quint will automatically compute the unchanged block in the future
   action unchangedAll = all {
@@ -743,8 +745,8 @@ module TendermintAcc {
   }
 }
 
-module TendermintTest {
-  module Tendermint_n4_f1 = TendermintAcc(
+module InstanceTests {
+  import TendermintTest(
     Corr = Set("p1", "p2", "p3"),
     Faulty = Set("p4"),
     N = 4,
@@ -753,9 +755,9 @@ module TendermintTest {
     InvalidValues = Set("v2"),
     MaxRound = 4,
     Proposer = Map(0 -> "p1", 1 -> "p2", 2 -> "p3", 3 -> "p4", 4 -> "p1")
-  )
+  ) as Tendermint_n4_f1
 
-  module Tendermint_n4_f2 = TendermintAcc(
+  import TendermintTest(
     Corr = Set("p1", "p2", "p3"),
     Faulty = Set("p3", "p4"),
     N = 4,
@@ -764,9 +766,9 @@ module TendermintTest {
     InvalidValues = Set("v2"),
     MaxRound = 4,
     Proposer = Map(0 -> "p1", 1 -> "p2", 2 -> "p3", 3 -> "p4", 4 -> "p1")
-  )
+  ) as Tendermint_n4_f2
 
-  module Tendermint_n5_f2 = TendermintAcc(
+  import TendermintTest(
     Corr = Set("p1", "p2", "p3"),
     Faulty = Set("p4", "p5"),
     N = 5,
@@ -775,5 +777,5 @@ module TendermintTest {
     InvalidValues = Set("v2"),
     MaxRound = 4,
     Proposer = Map(0 -> "p1", 1 -> "p2", 2 -> "p3", 3 -> "p4", 4 -> "p1")
-  )
+  ) as Tendermint_n5_f2
 }

examples/language-features/instances.qnt

@@ -9,15 +9,17 @@ module A {
 
 module Instances {
   pure val MyY = true
+  pure val z = "world"
 
-  module A1 = A(x = 33, y = MyY, z = "hello")
+  import A(x = 33, y = MyY, z = "hello") as A1
 
   // now, we can access F and G via A1::F and A1::G
   val test_F = A1::f(10)
   val test_x = A1::x
 
   // If we want to omit identity bindings such as z = z, we write:
-  module A2 = A(x = 15, y = MyY, *)
+  // import A(x = 15, y = MyY, *) as A2
+  import A(x = 15, y = MyY, z = z) as A2
 
   // the above is equivalent to TLA+'s instance:
   // A2 == INSTANCE A WITH x <- 15, y <- MyY

examples/solidity/SimpleAuction/SimpleAuctionNonComposable.qnt

@@ -56,7 +56,7 @@ module SimpleAuction {
         blockTime: UInt,
         // tokens assigned to the addresses
         balances: Addr -> UInt,
-        // error == true iff an error has occurred (we ignore the exact message) 
+        // error == true iff an error has occurred (we ignore the exact message)
         error: bool,
     }
 
@@ -104,7 +104,7 @@ module SimpleAuction {
     }
 
     // STATE MACHINE: state-dependent definitions and actions
-    
+
     // The state of SimpleAuction
     var auctionState: AuctionState
     // The state of the standard EVM machine
@@ -165,21 +165,21 @@ module SimpleAuction {
         // the proposed bid should not be smaller than the highest bid
         not(value <= auctionState.highestBid),
         // introduce an alias for auctionState, to decrease verbosity
-        val as = auctionState
+        val s = auctionState
         // compute the new pending return for the highest bidder
-        val newReturn = as.pendingReturns.get(as.highestBidder) + as.highestBid
+        val newReturn = s.pendingReturns.get(s.highestBidder) + s.highestBid
         all {
             // uint is 256-bit in Solidity, so an overflow would revert the transaction
-            (as.highestBid != 0) implies (newReturn <= MAX_UINT),
+            (s.highestBid != 0) implies (newReturn <= MAX_UINT),
             // compute the new pending returns
-            val newPendingReturns = as.pendingReturns.set(as.highestBidder, newReturn)
+            val newPendingReturns = s.pendingReturns.set(s.highestBidder, newReturn)
             // update the auction state
             auctionState' =
-                as.with("highestBid", value)
+                s.with("highestBid", value)
                   .with("highestBidder", sender)
                   .with("pendingReturns", newPendingReturns),
             // update the balances
-            val nes = evmSend(evmState, sender, as.addressOfThis, value)
+            val nes = evmSend(evmState, sender, s.addressOfThis, value)
             all {
                 not(nes.error),
                 evmState' = nes

examples/solidity/icse23-fig7/README.md

@@ -72,44 +72,44 @@ With a bit of luck, quint finds a violation in 29 seconds:
 An example execution:
 ---------------------------------------------
 action step0 = all {
-  lotteryMempool::lotteryState' = { tickets: Map(), winningId: 0, drawingPhase: false, owner: "eve" },
-  lotteryMempool::mempool' = Set(),
-  lotteryMempool::lastTx' = { kind: "none", status: "none", sender: "", id: 0, amount: 0, ids: [], amounts: [] },
+  lotteryState' = { tickets: Map(), winningId: 0, drawingPhase: false, owner: "eve" },
+  mempool' = Set(),
+  lastTx' = { kind: "none", status: "none", sender: "", id: 0, amount: 0, ids: [], amounts: [] },
 }
 
 action step1 = all {
-  lotteryMempool::lotteryState' = { tickets: Map(), winningId: 0, drawingPhase: false, owner: "eve" },
-  lotteryMempool::mempool' = Set({ kind: "enterDrawingPhase", status: "pending", sender: "eve", id: 0, amount: 0, ids: [], amounts: [] }),
-  lotteryMempool::lastTx' = { kind: "enterDrawingPhase", status: "pending", sender: "eve", id: 0, amount: 0, ids: [], amounts: [] },
+  lotteryState' = { tickets: Map(), winningId: 0, drawingPhase: false, owner: "eve" },
+  mempool' = Set({ kind: "enterDrawingPhase", status: "pending", sender: "eve", id: 0, amount: 0, ids: [], amounts: [] }),
+  lastTx' = { kind: "enterDrawingPhase", status: "pending", sender: "eve", id: 0, amount: 0, ids: [], amounts: [] },
 }
 
 action step2 = all {
-  lotteryMempool::lotteryState' = { tickets: Map(), winningId: 0, drawingPhase: true, owner: "eve" },
-  lotteryMempool::mempool' = Set(),
-  lotteryMempool::lastTx' = { kind: "enterDrawingPhase", status: "success", sender: "eve", id: 0, amount: 0, ids: [], amounts: [] },
+  lotteryState' = { tickets: Map(), winningId: 0, drawingPhase: true, owner: "eve" },
+  mempool' = Set(),
+  lastTx' = { kind: "enterDrawingPhase", status: "success", sender: "eve", id: 0, amount: 0, ids: [], amounts: [] },
 }
 
 action step3 = all {
-  lotteryMempool::lotteryState' = { tickets: Map(), winningId: 0, drawingPhase: true, owner: "eve" },
-  lotteryMempool::mempool' = Set({ kind: "draw", status: "pending", sender: "eve", id: 3, amount: 0, ids: [], amounts: [] }),
-  lotteryMempool::lastTx' = { kind: "draw", status: "pending", sender: "eve", id: 3, amount: 0, ids: [], amounts: [] },
+  lotteryState' = { tickets: Map(), winningId: 0, drawingPhase: true, owner: "eve" },
+  mempool' = Set({ kind: "draw", status: "pending", sender: "eve", id: 3, amount: 0, ids: [], amounts: [] }),
+  lastTx' = { kind: "draw", status: "pending", sender: "eve", id: 3, amount: 0, ids: [], amounts: [] },
 }
 
 action step4 = all {
-  lotteryMempool::lotteryState' = { tickets: Map(), winningId: 0, drawingPhase: true, owner: "eve" },
-  lotteryMempool::mempool' = Set({ kind: "draw", status: "pending", sender: "eve", id: 3, amount: 0, ids: [], amounts: [] }, { kind: "multiBuy", status: "pending", sender: "eve", id: 0, amount: 0, ids: [3, 5], amounts: [5, 9] }),
-  lotteryMempool::lastTx' = { kind: "multiBuy", status: "pending", sender: "eve", id: 0, amount: 0, ids: [3, 5], amounts: [5, 9] },
+  lotteryState' = { tickets: Map(), winningId: 0, drawingPhase: true, owner: "eve" },
+  mempool' = Set({ kind: "draw", status: "pending", sender: "eve", id: 3, amount: 0, ids: [], amounts: [] }, { kind: "multiBuy", status: "pending", sender: "eve", id: 0, amount: 0, ids: [3, 5], amounts: [5, 9] }),
+  lastTx' = { kind: "multiBuy", status: "pending", sender: "eve", id: 0, amount: 0, ids: [3, 5], amounts: [5, 9] },
 }
 
 action step5 = all {
-  lotteryMempool::lotteryState' = { tickets: Map("eve" -> Map(3 -> 5, 5 -> 9)), winningId: 0, drawingPhase: true, owner: "eve" },
-  lotteryMempool::mempool' = Set({ kind: "draw", status: "pending", sender: "eve", id: 3, amount: 0, ids: [], amounts: [] }),
-  lotteryMempool::lastTx' = { kind: "multiBuy", status: "success", sender: "eve", id: 0, amount: 0, ids: [3, 5], amounts: [5, 9] },
+  lotteryState' = { tickets: Map("eve" -> Map(3 -> 5, 5 -> 9)), winningId: 0, drawingPhase: true, owner: "eve" },
+  mempool' = Set({ kind: "draw", status: "pending", sender: "eve", id: 3, amount: 0, ids: [], amounts: [] }),
+  lastTx' = { kind: "multiBuy", status: "success", sender: "eve", id: 0, amount: 0, ids: [3, 5], amounts: [5, 9] },
 }
 
 run test = {
   step0.then(step1).then(step2).then(step3).then(step4).then(step5)
 }
 ---------------------------------------------
 [nok] Found a violation (28752ms).
-```
+```

quint/cli-tests.md

@@ -80,7 +80,7 @@ Temporarily disabled.
 ### OK on test Tendermint
 
 <!-- !test check Tendermint - Test -->
-    quint test --main TendermintTest ../examples/cosmos/tendermint/TendermintAcc005.qnt
+    quint test --main InstanceTests ../examples/cosmos/tendermint/TendermintAcc005.qnt
 
 ### OK on parse imports
 

quint/io-cli-tests.md

@@ -151,15 +151,15 @@ quint typecheck ./testFixture/typechecking/OverrideErrors.qnt 2> >(sed "s:$(pwd)
 
 <!-- !test err typecheck failure on override -->
 ```
-./testFixture/typechecking/OverrideErrors.qnt:8:21 - error: [QNT000] Couldn't unify bool and int
+./testFixture/typechecking/OverrideErrors.qnt:8:16 - error: [QNT000] Couldn't unify bool and int
 Trying to unify bool and int
 
-8:   module A1 = A(c = 1)
-                       ^
+8:   import A(c = 1) as A1
+                  ^
 
-./testFixture/typechecking/OverrideErrors.qnt:9:21 - error: [QNT201] Instance overrides must be pure values, but the value for c reads variables 'x'
-9:   module A2 = A(c = x)
-                       ^
+./testFixture/typechecking/OverrideErrors.qnt:9:16 - error: [QNT201] Instance overrides must be pure values, but the value for c reads variables 'x'
+9:   import A(c = x) as A2
+                  ^
 
 error: typechecking failed
 ```
@@ -283,23 +283,23 @@ quint run --init=Init --step=Next --seed=abcde --max-steps=4 \
 An example execution:
 ---------------------------------------------
 action step0 = all {
-  counters::n' = 1,
+  n' = 1,
 }
 
 action step1 = all {
-  counters::n' = 2,
+  n' = 2,
 }
 
 action step2 = all {
-  counters::n' = 3,
+  n' = 3,
 }
 
 action step3 = all {
-  counters::n' = 6,
+  n' = 6,
 }
 
 action step4 = all {
-  counters::n' = 12,
+  n' = 12,
 }
 
 run test = {
@@ -326,23 +326,23 @@ quint run --init=Init --step=Next --seed=abcde --max-steps=4 \
 An example execution:
 ---------------------------------------------
 action step0 = all {
-  counters::n' = 1,
+  n' = 1,
 }
 
 action step1 = all {
-  counters::n' = 2,
+  n' = 2,
 }
 
 action step2 = all {
-  counters::n' = 3,
+  n' = 3,
 }
 
 action step3 = all {
-  counters::n' = 4,
+  n' = 4,
 }
 
 action step4 = all {
-  counters::n' = 2,
+  n' = 2,
 }
 
 run test = {
@@ -393,13 +393,13 @@ quint run --max-steps=5 --seed=123 --invariant=totalSupplyDoesNotOverflowInv \
 An example execution:
 ---------------------------------------------
 action step0 = all {
-  coin::minter' = "alice",
-  coin::balances' = Map("alice" -> 0, "bob" -> 0, "charlie" -> 0, "eve" -> 0, "null" -> 0),
+  minter' = "alice",
+  balances' = Map("alice" -> 0, "bob" -> 0, "charlie" -> 0, "eve" -> 0, "null" -> 0),
 }
 
 action step1 = all {
-  coin::minter' = "alice",
-  coin::balances' = Map("alice" -> 0, "bob" -> 0, "charlie" -> 0, "eve" -> 0, "null" -> 60111170443858436966126692514148478804869009443507772171903863504622757871616),
+  minter' = "alice",
+  balances' = Map("alice" -> 0, "bob" -> 0, "charlie" -> 0, "eve" -> 0, "null" -> 60111170443858436966126692514148478804869009443507772171903863504622757871616),
 }
 
 run test = {
@@ -416,7 +416,7 @@ run test = {
 quint run --out-itf=out-itf-example.itf.json --max-steps=5 --seed=123 \
   --invariant=totalSupplyDoesNotOverflowInv \
   ../examples/solidity/Coin/coin.qnt
-cat out-itf-example.itf.json | jq '.states[0]."coin::balances"."#map"[0]'
+cat out-itf-example.itf.json | jq '.states[0]."balances"."#map"[0]'
 rm out-itf-example.itf.json
 ```
 

quint/src/IRprinting.ts

@@ -59,7 +59,7 @@ export function definitionToString(def: QuintDef, includeBody:boolean=true): str
       return `import ${def.path}.${def.name}`
     case 'instance': {
       const overrides = def.overrides.map(o => `${o[0].name} = ${expressionToString(o[1])}`).join(', ')
-      return `module ${def.name} = ${def.protoName}(${overrides})`
+      return `import ${def.protoName}(${overrides}) as ${def.qualifiedName}`
     }
   }
 }

quint/src/ToIrListener.ts

@@ -311,9 +311,8 @@ export class ToIrListener implements QuintListener {
 
   // module Foo = Proto(x = a, y = b)
   exitInstanceMod(ctx: p.InstanceModContext) {
-    const identifiers = ctx.IDENTIFIER()!
-    const instanceName = identifiers[0].text
-    const protoName = identifiers[1].text
+    const protoName = ctx.moduleName().text
+    const qualifiedName = ctx.qualifiedName()?.text
     const names = ctx.name()!
     const nexprs = ctx.expr().length
     const overrides: [QuintLambdaParameter, QuintEx][] = []
@@ -334,7 +333,7 @@ export class ToIrListener implements QuintListener {
     const instance: QuintDef = {
       id,
       kind: 'instance',
-      name: instanceName,
+      qualifiedName: qualifiedName,
       protoName,
       overrides,
       identityOverride,

quint/src/definitionsByName.ts

@@ -32,6 +32,8 @@ export interface TypeDefinition {
   type?: QuintType
   /* Expression or definition id from where the type was collected */
   reference?: bigint
+  /* Optional scope, an id pointing to the QuintIr node that introduces the name */
+  scope?: bigint
 }
 
 /**
@@ -173,7 +175,7 @@ export function copyNames(originTable: DefinitionsByName, namespace?: string, sc
     const name = namespace ? [namespace, identifier].join('::') : identifier
 
     // Copy only unscoped and non-default (referenced) names
-    const valueDefs = defs.filter(d => !d.scope && d.reference).map(d => ({ ...d, identifier: name, scope }))
+    const valueDefs = defs.filter(d => (!d.scope || d.kind === 'const') && d.reference).map(d => ({ ...d, identifier: name, scope }))
 
     if (valueDefs.length > 0) {
       table.valueDefinitions.set(name, valueDefs)
@@ -184,7 +186,7 @@ export function copyNames(originTable: DefinitionsByName, namespace?: string, sc
     const name = namespace ? [namespace, identifier].join('::') : identifier
 
     // Copy only non-default (referenced) names
-    const typeDefs = defs.filter(d => d.reference).map(d => ({ ...d, identifier: name }))
+    const typeDefs = defs.filter(d => !d.scope && d.reference).map(d => ({ ...d, identifier: name, scope }))
 
     if (typeDefs.length > 0) {
       table.typeDefinitions.set(name, typeDefs)