Model-checking specification with large(ish) set of records

Apalache Questions
1

Hi all, I’m trying to model-check this specification: SCP-TLA/Balloting.tla at variant-types · nano-o/SCP-TLA · GitHub

Unfortunately, just checking that TypeOK is inductive for a very small system size (see ApaBalloting.tla) is extremely slow and eats up dozens of GB of memory (you can try with make test). However, TLC explores it exhaustively in seconds.

I presume that this is because the set of messages (variable sent) is a set of records with too many fields (and some are nested records), and this creates too many variables in the SMT encoding. I’m afraid this might be an intrinsic limitation of Apalache’s SMT encoding techniques, but I’d be happy to hear otherwise! Any tips?

2

Hi Giuliano,

Right. Checking inductiveness of TypeOK may easily explode the SMT encoding. Looking at your example, indeed, it does explode beyond reasonable.

Let’s dissect what’s going on a little bit:

TypeOK ==
    /\ ballot \in [N -> BallotOrNull]
    /\ phase \in [N -> Phase]
    /\ prepared \in [N -> BallotOrNull]
    /\ aCounter \in [N -> BallotNumber]
    /\ h \in [N -> BallotOrNull]
    /\ c \in [N -> BallotOrNull]
    /\ sent \in [N -> SUBSET Message]
    /\ byz \in SUBSET N

For most types, Apalache simplifies the membership check. For instance, prepared \in [N -> BallotOrNull] is rewritten to:

  DOMAIN prepared = { "N1_OF_NODE", "N2_OF_NODE", "N3_OF_NODE" }
    /\ (\A t_2m_1 \in { "N1_OF_NODE", "N2_OF_NODE", "N3_OF_NODE" }:
      DOMAIN (prepared[t_2m_1]) = { "counter", "value" }
        /\ prepared[t_2m_1]["counter"] \in { 0, 1 } \union {-1}
        /\ prepared[t_2m_1]["value"] \in { 0, 1 })

However, in the case of variant types, no simplification is made. So sent \in [N -> SUBSET Message] is partially simplified as:

  DOMAIN sent = { "N1_OF_NODE", "N2_OF_NODE", "N3_OF_NODE" }
    /\ (\A t_3j_1 \in { "N1_OF_NODE", "N2_OF_NODE", "N3_OF_NODE" }:
      \A t_3k_1 \in sent[t_3j_1]:
        t_3k_1
          \in {
            Variant("PREPARE", m_113):
              m_113 \in
                {
                  [ballot |-> t_38_1,
                    prepared |-> t_39_1,
                    aCounter |-> t_3a_1,
                    hCounter |-> t_3b_1,
                    cCounter |-> t_3c_1]:
                    t_38_1 \in
                      {
                        [counter |-> t_34_1, value |-> t_35_1]:
                          t_34_1 \in { 0, 1 },
                          t_35_1 \in { 0, 1 }
                      },
                    t_39_1 \in
                      {
                        [counter |-> t_36_1, value |-> t_37_1]:
                          t_36_1 \in { 0, 1 } \union {-1},
                          t_37_1 \in { 0, 1 }
                      },
                    t_3a_1 \in { 0, 1 },
                    t_3b_1 \in { 0, 1 } \union {-1},
                    t_3c_1 \in { 0, 1 } \union {-1}
                }
          }
            \union {
              Variant("COMMIT", m_114):
                m_114 \in
                  {
                    [ballot |-> t_3f_1,
                      preparedCounter |-> t_3g_1,
                      hCounter |-> t_3h_1,
                      cCounter |-> t_3i_1]:
                      t_3f_1 \in
                        {
                          [counter |-> t_3d_1, value |-> t_3e_1]:
                            t_3d_1 \in { 0, 1 },
                            t_3e_1 \in { 0, 1 }
                        },
                      t_3g_1 \in { 0, 1 },
                      t_3h_1 \in { 0, 1 } \union {-1},
                      t_3i_1 \in { 0, 1 } \union {-1}
                  }
            })

There are two issues:

  1. We have to iterate over two sets.
  2. Under two quantifiers, each time a set of several hundred elements is constructed.

I believe that this can be avoided, if we introduce a simplification rule similar to the rule for records.

3

Thanks! I can split the sent variable into two variables, one for each type of message, and then not use a variant type at all. I don’t understand fully what is going on, but it sounds like this might help.

4

I tried it here and it helps: SCP-TLA/Balloting.tla at apalache · nano-o/SCP-TLA · GitHub