[BUG] Function displayed in the counterexample with multiple indices

[andrey-kuprianov]

Description

In the produced TLA+ counterexample a function is displayed with twice the same index

Input specification

See https://github.com/informalsystems/modelator/blob/c9b54c1c4cd753af833ae4a16b626e4d3a5cab94/modelator/tests/integration/tla/IBC_ics02.tla

The command line parameters used to run the tool

apalache-mc check --cinit=CInit --inv=InvTestClientWith3Heights IBC_ics02.tla

Log files

Here are the last few lines of the produced counterexample that contain the erroneous output:

(* Transition 2 to State3 *)
State3 ==
  ChainIds = { "chainA", "chainB" }
    /\ MaxChainHeight = 10
    /\ MaxClientsPerChain = 5
    /\ action
      = [chainId |-> "chainB",
        clientId |-> 0,
        height |-> 3,
        type |-> "UpdateClient"]
    /\ actionOutcome = "OK"
    /\ chains
      = "chainA"
          :> [clientIdCounter |-> 0,
            clients |-> [ x \in {} |-> x ],
            height |-> 1]
        @@ "chainB"
          :> [clientIdCounter |-> 1,
            clients |->
              0 :> [heights |-> { 1, 2, 3 }] @@ 0 :> [heights |-> { 1, 2, 3 }],
            height |-> 4]

(* The following formula holds true in the last state and violates the invariant *)
InvariantViolation ==
  Skolem((\E c$3 \in ChainIds:
    Skolem((\E cl$2 \in DOMAIN (chains[c$3]["clients"]):
      ConstCardinality((Cardinality(chains[c$3]["clients"][cl$2]["heights"])
        >= 3))))))

System information

• Apalache version: 0.15.11
• OS: Mac
• JDK version: OpenJDK Runtime Environment Zulu15.32+15-CA

[andrey-kuprianov]

It gets even more interesting than that:

(* Transition 2 to State6 *)
State6 ==
  ChainIds = { "chainA", "chainB" }
    /\ MaxChainHeight = 4
    /\ MaxClientsPerChain = 2
    /\ action
      = [chainId |-> "chainA",
        clientId |-> 1,
        height |-> 4,
        type |-> "UpdateClient"]
    /\ actionOutcome = "OK"
    /\ chains
      = "chainA"
          :> [clientIdCounter |-> 2,
            clients |->
              (((1 :> [heights |-> { 1, 3, 4 }]
                      @@ 1 :> [heights |-> { 1, 3, 4 }])
                    @@ 1 :> [heights |-> { 1, 3, 4 }])
                  @@ 1 :> [heights |-> { 1, 3, 4 }])
                @@ 0 :> [heights |-> { 1, 2, 3 }],
            height |-> 7]
        @@ "chainB"
          :> [clientIdCounter |-> 0,
            clients |-> [ x \in {} |-> x ],
            height |-> 1]

[konnov]

Nice. The important thing is that all copies agree on the value for the key 1.

[konnov]

@shonfeder, do you like to have a look at this one? It should be something in https://github.com/informalsystems/apalache/blob/unstable/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/SymbStateDecoder.scala

[shonfeder]

I've identified the root cause and am working on a fix.

[shonfeder]

See #962 for a report on my understanding of the underlying problem, and my (blocking) question on how we want to approach it.

[shonfeder]

Here is a MWE

------------------- MODULE Dup -----------------------

VARIABLES
  \* @type: Int -> Int;
  someFun

Init == someFun = [x \in {0, 0} |-> 1]

Next == UNCHANGED someFun

Inv == 0 \notin DOMAIN someFun

============================================================

Run with

apalache-mc check --inv=Inv Dup.tla

Producing the counterexample:

---------------------------- MODULE counterexample ----------------------------

EXTENDS Dup

(* Constant initialization state *)
ConstInit == TRUE

(* Initial state *)
State0 == someFun = 0 :> 1 @@ 0 :> 1

(* The following formula holds true in the last state and violates the invariant *)
InvariantViolation == 0 \in DOMAIN someFun

================================================================================
(* Created by Apalache on Thu Nov 25 14:50:13 EST 2021 *)
(* https://github.com/informalsystems/apalache *)