MC100_2_faulty_TestFailure.tla

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

EXTENDS MC100_2_faulty

(* Initial state *)

State1 ==
TRUE
(* Transition 0 to State2 *)

State2 ==
/\ Faulty = { "n100",
  "n16",
  "n19",
  "n2",
  "n32",
  "n36",
  "n42",
  "n44",
  "n5",
  "n61",
  "n63",
  "n70",
  "n72",
  "n74",
  "n8",
  "n82",
  "n85",
  "n86" }
/\ blockchain = 1
    :> [NextVS |->
        { "n16",
          "n2",
          "n3",
          "n36",
          "n40",
          "n47",
          "n48",
          "n57",
          "n59",
          "n62",
          "n70",
          "n72",
          "n81",
          "n89",
          "n9",
          "n93" },
      VS |->
        { "n1",
          "n10",
          "n100",
          "n11",
          "n12",
          "n13",
          "n14",
          "n15",
          "n16",
          "n17",
          "n18",
          "n19",
          "n2",
          "n20",
          "n21",
          "n22",
          "n23",
          "n24",
          "n25",
          "n26",
          "n27",
          "n28",
          "n29",
          "n3",
          "n30",
          "n31",
          "n32",
          "n33",
          "n34",
          "n35",
          "n36",
          "n37",
          "n38",
          "n39",
          "n4",
          "n40",
          "n41",
          "n42",
          "n43",
          "n44",
          "n45",
          "n46",
          "n47",
          "n48",
          "n49",
          "n5",
          "n50",
          "n51",
          "n52",
          "n53",
          "n54",
          "n55",
          "n56",
          "n57",
          "n58",
          "n59",
          "n6",
          "n60",
          "n61",
          "n62",
          "n63",
          "n64",
          "n65",
          "n66",
          "n67",
          "n68",
          "n69",
          "n7",
          "n70",
          "n71",
          "n72",
          "n73",
          "n74",
          "n75",
          "n76",
          "n77",
          "n78",
          "n79",
          "n8",
          "n80",
          "n81",
          "n82",
          "n83",
          "n84",
          "n85",
          "n86",
          "n87",
          "n88",
          "n89",
          "n9",
          "n90",
          "n91",
          "n92",
          "n93",
          "n94",
          "n95",
          "n96",
          "n97",
          "n98",
          "n99" },
      height |-> 1,
      lastCommit |-> {},
      time |-> 1]
  @@ 2
    :> [NextVS |->
        { "n1",
          "n10",
          "n100",
          "n11",
          "n12",
          "n13",
          "n14",
          "n15",
          "n16",
          "n17",
          "n18",
          "n19",
          "n20",
          "n21",
          "n22",
          "n23",
          "n25",
          "n26",
          "n27",
          "n28",
          "n29",
          "n30",
          "n31",
          "n32",
          "n33",
          "n34",
          "n35",
          "n36",
          "n37",
          "n38",
          "n39",
          "n4",
          "n40",
          "n41",
          "n42",
          "n43",
          "n45",
          "n46",
          "n48",
          "n49",
          "n5",
          "n50",
          "n51",
          "n52",
          "n53",
          "n54",
          "n55",
          "n56",
          "n58",
          "n59",
          "n6",
          "n60",
          "n61",
          "n64",
          "n65",
          "n66",
          "n67",
          "n68",
          "n69",
          "n7",
          "n71",
          "n73",
          "n75",
          "n76",
          "n77",
          "n78",
          "n8",
          "n82",
          "n83",
          "n84",
          "n85",
          "n86",
          "n88",
          "n89",
          "n90",
          "n91",
          "n92",
          "n93",
          "n94",
          "n95",
          "n96",
          "n97",
          "n98",
          "n99" },
      VS |->
        { "n16",
          "n2",
          "n3",
          "n36",
          "n40",
          "n47",
          "n48",
          "n57",
          "n59",
          "n62",
          "n70",
          "n72",
          "n81",
          "n89",
          "n9",
          "n93" },
      height |-> 2,
      lastCommit |->
        { "n1",
          "n10",
          "n100",
          "n11",
          "n12",
          "n13",
          "n14",
          "n15",
          "n16",
          "n17",
          "n18",
          "n19",
          "n2",
          "n21",
          "n22",
          "n23",
          "n24",
          "n25",
          "n26",
          "n27",
          "n28",
          "n29",
          "n30",
          "n31",
          "n32",
          "n33",
          "n34",
          "n35",
          "n36",
          "n37",
          "n38",
          "n39",
          "n4",
          "n40",
          "n41",
          "n42",
          "n43",
          "n44",
          "n45",
          "n46",
          "n47",
          "n49",
          "n5",
          "n50",
          "n51",
          "n52",
          "n53",
          "n54",
          "n55",
          "n56",
          "n57",
          "n58",
          "n59",
          "n6",
          "n60",
          "n61",
          "n63",
          "n64",
          "n65",
          "n66",
          "n67",
          "n68",
          "n69",
          "n7",
          "n70",
          "n71",
          "n72",
          "n73",
          "n74",
          "n75",
          "n76",
          "n77",
          "n78",
          "n79",
          "n8",
          "n80",
          "n81",
          "n82",
          "n83",
          "n84",
          "n85",
          "n86",
          "n87",
          "n88",
          "n89",
          "n9",
          "n90",
          "n91",
          "n92",
          "n93",
          "n94",
          "n95",
          "n96",
          "n97",
          "n98",
          "n99" },
      time |-> 2]
  @@ 3
    :> [NextVS |->
        { "n1",
          "n10",
          "n100",
          "n11",
          "n12",
          "n13",
          "n14",
          "n15",
          "n16",
          "n17",
          "n18",
          "n19",
          "n2",
          "n20",
          "n21",
          "n22",
          "n23",
          "n24",
          "n25",
          "n26",
          "n27",
          "n28",
          "n29",
          "n3",
          "n30",
          "n31",
          "n32",
          "n33",
          "n34",
          "n35",
          "n36",
          "n37",
          "n38",
          "n39",
          "n4",
          "n40",
          "n41",
          "n42",
          "n43",
          "n44",
          "n45",
          "n46",
          "n47",
          "n48",
          "n49",
          "n5",
          "n50",
          "n51",
          "n52",
          "n53",
          "n54",
          "n55",
          "n56",
          "n57",
          "n58",
          "n59",
          "n6",
          "n60",
          "n61",
          "n62",
          "n63",
          "n64",
          "n65",
          "n66",
          "n67",
          "n68",
          "n69",
          "n7",
          "n70",
          "n71",
          "n72",
          "n73",
          "n74",
          "n75",
          "n76",
          "n77",
          "n78",
          "n79",
          "n8",
          "n80",
          "n81",
          "n82",
          "n83",
          "n84",
          "n85",
          "n86",
          "n87",
          "n88",
          "n89",
          "n9",
          "n90",
          "n91",
          "n92",
          "n93",
          "n94",
          "n95",
          "n96",
          "n97",
          "n98",
          "n99" },
      VS |->
        { "n1",
          "n10",
          "n100",
          "n11",
          "n12",
          "n13",
          "n14",
          "n15",
          "n16",
          "n17",
          "n18",
          "n19",
          "n20",
          "n21",
          "n22",
          "n23",
          "n25",
          "n26",
          "n27",
          "n28",
          "n29",
          "n30",
          "n31",
          "n32",
          "n33",
          "n34",
          "n35",
          "n36",
          "n37",
          "n38",
          "n39",
          "n4",
          "n40",
          "n41",
          "n42",
          "n43",
          "n45",
          "n46",
          "n48",
          "n49",
          "n5",
          "n50",
          "n51",
          "n52",
          "n53",
          "n54",
          "n55",
          "n56",
          "n58",
          "n59",
          "n6",
          "n60",
          "n61",
          "n64",
          "n65",
          "n66",
          "n67",
          "n68",
          "n69",
          "n7",
          "n71",
          "n73",
          "n75",
          "n76",
          "n77",
          "n78",
          "n8",
          "n82",
          "n83",
          "n84",
          "n85",
          "n86",
          "n88",
          "n89",
          "n90",
          "n91",
          "n92",
          "n93",
          "n94",
          "n95",
          "n96",
          "n97",
          "n98",
          "n99" },
      height |-> 3,
      lastCommit |->
        { "n16",
          "n3",
          "n36",
          "n40",
          "n47",
          "n48",
          "n59",
          "n62",
          "n72",
          "n9",
          "n93" },
      time |-> 3]
/\ fetchedLightBlocks = 1
    :> [Commits |->
        { "n1",
          "n10",
          "n100",
          "n11",
          "n12",
          "n13",
          "n14",
          "n15",
          "n16",
          "n17",
          "n18",
          "n19",
          "n2",
          "n20",
          "n21",
          "n22",
          "n23",
          "n24",
          "n25",
          "n26",
          "n27",
          "n28",
          "n29",
          "n3",
          "n30",
          "n31",
          "n32",
          "n33",
          "n34",
          "n35",
          "n36",
          "n37",
          "n38",
          "n39",
          "n4",
          "n40",
          "n41",
          "n42",
          "n43",
          "n44",
          "n45",
          "n46",
          "n47",
          "n48",
          "n49",
          "n5",
          "n50",
          "n51",
          "n52",
          "n53",
          "n54",
          "n55",
          "n56",
          "n57",
          "n58",
          "n59",
          "n6",
          "n60",
          "n61",
          "n62",
          "n63",
          "n64",
          "n65",
          "n66",
          "n67",
          "n68",
          "n69",
          "n7",
          "n70",
          "n71",
          "n72",
          "n73",
          "n74",
          "n75",
          "n76",
          "n77",
          "n78",
          "n79",
          "n8",
          "n80",
          "n81",
          "n82",
          "n83",
          "n84",
          "n85",
          "n86",
          "n87",
          "n88",
          "n89",
          "n9",
          "n90",
          "n91",
          "n92",
          "n93",
          "n94",
          "n95",
          "n96",
          "n97",
          "n98",
          "n99" },
      header |->
        [NextVS |->
            { "n16",
              "n2",
              "n3",
              "n36",
              "n40",
              "n47",
              "n48",
              "n57",
              "n59",
              "n62",
              "n70",
              "n72",
              "n81",
              "n89",
              "n9",
              "n93" },
          VS |->
            { "n1",
              "n10",
              "n100",
              "n11",
              "n12",
              "n13",
              "n14",
              "n15",
              "n16",
              "n17",
              "n18",
              "n19",
              "n2",
              "n20",
              "n21",
              "n22",
              "n23",
              "n24",
              "n25",
              "n26",
              "n27",
              "n28",
              "n29",
              "n3",
              "n30",
              "n31",
              "n32",
              "n33",
              "n34",
              "n35",
              "n36",
              "n37",
              "n38",
              "n39",
              "n4",
              "n40",
              "n41",
              "n42",
              "n43",
              "n44",
              "n45",
              "n46",
              "n47",
              "n48",
              "n49",
              "n5",
              "n50",
              "n51",
              "n52",
              "n53",
              "n54",
              "n55",
              "n56",
              "n57",
              "n58",
              "n59",
              "n6",
              "n60",
              "n61",
              "n62",
              "n63",
              "n64",
              "n65",
              "n66",
              "n67",
              "n68",
              "n69",
              "n7",
              "n70",
              "n71",
              "n72",
              "n73",
              "n74",
              "n75",
              "n76",
              "n77",
              "n78",
              "n79",
              "n8",
              "n80",
              "n81",
              "n82",
              "n83",
              "n84",
              "n85",
              "n86",
              "n87",
              "n88",
              "n89",
              "n9",
              "n90",
              "n91",
              "n92",
              "n93",
              "n94",
              "n95",
              "n96",
              "n97",
              "n98",
              "n99" },
          height |-> 1,
          lastCommit |-> {},
          time |-> 1]]
/\ history = 0
    :> [current |->
        [Commits |->
            { "n1",
              "n10",
              "n100",
              "n11",
              "n12",
              "n13",
              "n14",
              "n15",
              "n16",
              "n17",
              "n18",
              "n19",
              "n2",
              "n20",
              "n21",
              "n22",
              "n23",
              "n24",
              "n25",
              "n26",
              "n27",
              "n28",
              "n29",
              "n3",
              "n30",
              "n31",
              "n32",
              "n33",
              "n34",
              "n35",
              "n36",
              "n37",
              "n38",
              "n39",
              "n4",
              "n40",
              "n41",
              "n42",
              "n43",
              "n44",
              "n45",
              "n46",
              "n47",
              "n48",
              "n49",
              "n5",
              "n50",
              "n51",
              "n52",
              "n53",
              "n54",
              "n55",
              "n56",
              "n57",
              "n58",
              "n59",
              "n6",
              "n60",
              "n61",
              "n62",
              "n63",
              "n64",
              "n65",
              "n66",
              "n67",
              "n68",
              "n69",
              "n7",
              "n70",
              "n71",
              "n72",
              "n73",
              "n74",
              "n75",
              "n76",
              "n77",
              "n78",
              "n79",
              "n8",
              "n80",
              "n81",
              "n82",
              "n83",
              "n84",
              "n85",
              "n86",
              "n87",
              "n88",
              "n89",
              "n9",
              "n90",
              "n91",
              "n92",
              "n93",
              "n94",
              "n95",
              "n96",
              "n97",
              "n98",
              "n99" },
          header |->
            [NextVS |->
                { "n16",
                  "n2",
                  "n3",
                  "n36",
                  "n40",
                  "n47",
                  "n48",
                  "n57",
                  "n59",
                  "n62",
                  "n70",
                  "n72",
                  "n81",
                  "n89",
                  "n9",
                  "n93" },
              VS |->
                { "n1",
                  "n10",
                  "n100",
                  "n11",
                  "n12",
                  "n13",
                  "n14",
                  "n15",
                  "n16",
                  "n17",
                  "n18",
                  "n19",
                  "n2",
                  "n20",
                  "n21",
                  "n22",
                  "n23",
                  "n24",
                  "n25",
                  "n26",
                  "n27",
                  "n28",
                  "n29",
                  "n3",
                  "n30",
                  "n31",
                  "n32",
                  "n33",
                  "n34",
                  "n35",
                  "n36",
                  "n37",
                  "n38",
                  "n39",
                  "n4",
                  "n40",
                  "n41",
                  "n42",
                  "n43",
                  "n44",
                  "n45",
                  "n46",
                  "n47",
                  "n48",
                  "n49",
                  "n5",
                  "n50",
                  "n51",
                  "n52",
                  "n53",
                  "n54",
                  "n55",
                  "n56",
                  "n57",
                  "n58",
                  "n59",
                  "n6",
                  "n60",
                  "n61",
                  "n62",
                  "n63",
                  "n64",
                  "n65",
                  "n66",
                  "n67",
                  "n68",
                  "n69",
                  "n7",
                  "n70",
                  "n71",
                  "n72",
                  "n73",
                  "n74",
                  "n75",
                  "n76",
                  "n77",
                  "n78",
                  "n79",
                  "n8",
                  "n80",
                  "n81",
                  "n82",
                  "n83",
                  "n84",
                  "n85",
                  "n86",
                  "n87",
                  "n88",
                  "n89",
                  "n9",
                  "n90",
                  "n91",
                  "n92",
                  "n93",
                  "n94",
                  "n95",
                  "n96",
                  "n97",
                  "n98",
                  "n99" },
              height |-> 1,
              lastCommit |-> {},
              time |-> 1]],
      now |-> 1402,
      verdict |-> "SUCCESS",
      verified |->
        [Commits |->
            { "n1",
              "n10",
              "n100",
              "n11",
              "n12",
              "n13",
              "n14",
              "n15",
              "n16",
              "n17",
              "n18",
              "n19",
              "n2",
              "n20",
              "n21",
              "n22",
              "n23",
              "n24",
              "n25",
              "n26",
              "n27",
              "n28",
              "n29",
              "n3",
              "n30",
              "n31",
              "n32",
              "n33",
              "n34",
              "n35",
              "n36",
              "n37",
              "n38",
              "n39",
              "n4",
              "n40",
              "n41",
              "n42",
              "n43",
              "n44",
              "n45",
              "n46",
              "n47",
              "n48",
              "n49",
              "n5",
              "n50",
              "n51",
              "n52",
              "n53",
              "n54",
              "n55",
              "n56",
              "n57",
              "n58",
              "n59",
              "n6",
              "n60",
              "n61",
              "n62",
              "n63",
              "n64",
              "n65",
              "n66",
              "n67",
              "n68",
              "n69",
              "n7",
              "n70",
              "n71",
              "n72",
              "n73",
              "n74",
              "n75",
              "n76",
              "n77",
              "n78",
              "n79",
              "n8",
              "n80",
              "n81",
              "n82",
              "n83",
              "n84",
              "n85",
              "n86",
              "n87",
              "n88",
              "n89",
              "n9",
              "n90",
              "n91",
              "n92",
              "n93",
              "n94",
              "n95",
              "n96",
              "n97",
              "n98",
              "n99" },
          header |->
            [NextVS |->
                { "n16",
                  "n2",
                  "n3",
                  "n36",
                  "n40",
                  "n47",
                  "n48",
                  "n57",
                  "n59",
                  "n62",
                  "n70",
                  "n72",
                  "n81",
                  "n89",
                  "n9",
                  "n93" },
              VS |->
                { "n1",
                  "n10",
                  "n100",
                  "n11",
                  "n12",
                  "n13",
                  "n14",
                  "n15",
                  "n16",
                  "n17",
                  "n18",
                  "n19",
                  "n2",
                  "n20",
                  "n21",
                  "n22",
                  "n23",
                  "n24",
                  "n25",
                  "n26",
                  "n27",
                  "n28",
                  "n29",
                  "n3",
                  "n30",
                  "n31",
                  "n32",
                  "n33",
                  "n34",
                  "n35",
                  "n36",
                  "n37",
                  "n38",
                  "n39",
                  "n4",
                  "n40",
                  "n41",
                  "n42",
                  "n43",
                  "n44",
                  "n45",
                  "n46",
                  "n47",
                  "n48",
                  "n49",
                  "n5",
                  "n50",
                  "n51",
                  "n52",
                  "n53",
                  "n54",
                  "n55",
                  "n56",
                  "n57",
                  "n58",
                  "n59",
                  "n6",
                  "n60",
                  "n61",
                  "n62",
                  "n63",
                  "n64",
                  "n65",
                  "n66",
                  "n67",
                  "n68",
                  "n69",
                  "n7",
                  "n70",
                  "n71",
                  "n72",
                  "n73",
                  "n74",
                  "n75",
                  "n76",
                  "n77",
                  "n78",
                  "n79",
                  "n8",
                  "n80",
                  "n81",
                  "n82",
                  "n83",
                  "n84",
                  "n85",
                  "n86",
                  "n87",
                  "n88",
                  "n89",
                  "n9",
                  "n90",
                  "n91",
                  "n92",
                  "n93",
                  "n94",
                  "n95",
                  "n96",
                  "n97",
                  "n98",
                  "n99" },
              height |-> 1,
              lastCommit |-> {},
              time |-> 1]]]
/\ latestVerified = [Commits |->
    { "n1",
      "n10",
      "n100",
      "n11",
      "n12",
      "n13",
      "n14",
      "n15",
      "n16",
      "n17",
      "n18",
      "n19",
      "n2",
      "n20",
      "n21",
      "n22",
      "n23",
      "n24",
      "n25",
      "n26",
      "n27",
      "n28",
      "n29",
      "n3",
      "n30",
      "n31",
      "n32",
      "n33",
      "n34",
      "n35",
      "n36",
      "n37",
      "n38",
      "n39",
      "n4",
      "n40",
      "n41",
      "n42",
      "n43",
      "n44",
      "n45",
      "n46",
      "n47",
      "n48",
      "n49",
      "n5",
      "n50",
      "n51",
      "n52",
      "n53",
      "n54",
      "n55",
      "n56",
      "n57",
      "n58",
      "n59",
      "n6",
      "n60",
      "n61",
      "n62",
      "n63",
      "n64",
      "n65",
      "n66",
      "n67",
      "n68",
      "n69",
      "n7",
      "n70",
      "n71",
      "n72",
      "n73",
      "n74",
      "n75",
      "n76",
      "n77",
      "n78",
      "n79",
      "n8",
      "n80",
      "n81",
      "n82",
      "n83",
      "n84",
      "n85",
      "n86",
      "n87",
      "n88",
      "n89",
      "n9",
      "n90",
      "n91",
      "n92",
      "n93",
      "n94",
      "n95",
      "n96",
      "n97",
      "n98",
      "n99" },
  header |->
    [NextVS |->
        { "n16",
          "n2",
          "n3",
          "n36",
          "n40",
          "n47",
          "n48",
          "n57",
          "n59",
          "n62",
          "n70",
          "n72",
          "n81",
          "n89",
          "n9",
          "n93" },
      VS |->
        { "n1",
          "n10",
          "n100",
          "n11",
          "n12",
          "n13",
          "n14",
          "n15",
          "n16",
          "n17",
          "n18",
          "n19",
          "n2",
          "n20",
          "n21",
          "n22",
          "n23",
          "n24",
          "n25",
          "n26",
          "n27",
          "n28",
          "n29",
          "n3",
          "n30",
          "n31",
          "n32",
          "n33",
          "n34",
          "n35",
          "n36",
          "n37",
          "n38",
          "n39",
          "n4",
          "n40",
          "n41",
          "n42",
          "n43",
          "n44",
          "n45",
          "n46",
          "n47",
          "n48",
          "n49",
          "n5",
          "n50",
          "n51",
          "n52",
          "n53",
          "n54",
          "n55",
          "n56",
          "n57",
          "n58",
          "n59",
          "n6",
          "n60",
          "n61",
          "n62",
          "n63",
          "n64",
          "n65",
          "n66",
          "n67",
          "n68",
          "n69",
          "n7",
          "n70",
          "n71",
          "n72",
          "n73",
          "n74",
          "n75",
          "n76",
          "n77",
          "n78",
          "n79",
          "n8",
          "n80",
          "n81",
          "n82",
          "n83",
          "n84",
          "n85",
          "n86",
          "n87",
          "n88",
          "n89",
          "n9",
          "n90",
          "n91",
          "n92",
          "n93",
          "n94",
          "n95",
          "n96",
          "n97",
          "n98",
          "n99" },
      height |-> 1,
      lastCommit |-> {},
      time |-> 1]]
/\ lightBlockStatus = 1 :> "StateVerified"
/\ nextHeight = 2
/\ now = 1402
/\ nprobes = 0
/\ prevCurrent = [Commits |->
    { "n1",
      "n10",
      "n100",
      "n11",
      "n12",
      "n13",
      "n14",
      "n15",
      "n16",
      "n17",
      "n18",
      "n19",
      "n2",
      "n20",
      "n21",
      "n22",
      "n23",
      "n24",
      "n25",
      "n26",
      "n27",
      "n28",
      "n29",
      "n3",
      "n30",
      "n31",
      "n32",
      "n33",
      "n34",
      "n35",
      "n36",
      "n37",
      "n38",
      "n39",
      "n4",
      "n40",
      "n41",
      "n42",
      "n43",
      "n44",
      "n45",
      "n46",
      "n47",
      "n48",
      "n49",
      "n5",
      "n50",
      "n51",
      "n52",
      "n53",
      "n54",
      "n55",
      "n56",
      "n57",
      "n58",
      "n59",
      "n6",
      "n60",
      "n61",
      "n62",
      "n63",
      "n64",
      "n65",
      "n66",
      "n67",
      "n68",
      "n69",
      "n7",
      "n70",
      "n71",
      "n72",
      "n73",
      "n74",
      "n75",
      "n76",
      "n77",
      "n78",
      "n79",
      "n8",
      "n80",
      "n81",
      "n82",
      "n83",
      "n84",
      "n85",
      "n86",
      "n87",
      "n88",
      "n89",
      "n9",
      "n90",
      "n91",
      "n92",
      "n93",
      "n94",
      "n95",
      "n96",
      "n97",
      "n98",
      "n99" },
  header |->
    [NextVS |->
        { "n16",
          "n2",
          "n3",
          "n36",
          "n40",
          "n47",
          "n48",
          "n57",
          "n59",
          "n62",
          "n70",
          "n72",
          "n81",
          "n89",
          "n9",
          "n93" },
      VS |->
        { "n1",
          "n10",
          "n100",
          "n11",
          "n12",
          "n13",
          "n14",
          "n15",
          "n16",
          "n17",
          "n18",
          "n19",
          "n2",
          "n20",
          "n21",
          "n22",
          "n23",
          "n24",
          "n25",
          "n26",
          "n27",
          "n28",
          "n29",
          "n3",
          "n30",
          "n31",
          "n32",
          "n33",
          "n34",
          "n35",
          "n36",
          "n37",
          "n38",
          "n39",
          "n4",
          "n40",
          "n41",
          "n42",
          "n43",
          "n44",
          "n45",
          "n46",
          "n47",
          "n48",
          "n49",
          "n5",
          "n50",
          "n51",
          "n52",
          "n53",
          "n54",
          "n55",
          "n56",
          "n57",
          "n58",
          "n59",
          "n6",
          "n60",
          "n61",
          "n62",
          "n63",
          "n64",
          "n65",
          "n66",
          "n67",
          "n68",
          "n69",
          "n7",
          "n70",
          "n71",
          "n72",
          "n73",
          "n74",
          "n75",
          "n76",
          "n77",
          "n78",
          "n79",
          "n8",
          "n80",
          "n81",
          "n82",
          "n83",
          "n84",
          "n85",
          "n86",
          "n87",
          "n88",
          "n89",
          "n9",
          "n90",
          "n91",
          "n92",
          "n93",
          "n94",
          "n95",
          "n96",
          "n97",
          "n98",
          "n99" },
      height |-> 1,
      lastCommit |-> {},
      time |-> 1]]
/\ prevNow = 1402
/\ prevVerdict = "SUCCESS"
/\ prevVerified = [Commits |->
    { "n1",
      "n10",
      "n100",
      "n11",
      "n12",
      "n13",
      "n14",
      "n15",
      "n16",
      "n17",
      "n18",
      "n19",
      "n2",
      "n20",
      "n21",
      "n22",
      "n23",
      "n24",
      "n25",
      "n26",
      "n27",
      "n28",
      "n29",
      "n3",
      "n30",
      "n31",
      "n32",
      "n33",
      "n34",
      "n35",
      "n36",
      "n37",
      "n38",
      "n39",
      "n4",
      "n40",
      "n41",
      "n42",
      "n43",
      "n44",
      "n45",
      "n46",
      "n47",
      "n48",
      "n49",
      "n5",
      "n50",
      "n51",
      "n52",
      "n53",
      "n54",
      "n55",
      "n56",
      "n57",
      "n58",
      "n59",
      "n6",
      "n60",
      "n61",
      "n62",
      "n63",
      "n64",
      "n65",
      "n66",
      "n67",
      "n68",
      "n69",
      "n7",
      "n70",
      "n71",
      "n72",
      "n73",
      "n74",
      "n75",
      "n76",
      "n77",
      "n78",
      "n79",
      "n8",
      "n80",
      "n81",
      "n82",
      "n83",
      "n84",
      "n85",
      "n86",
      "n87",
      "n88",
      "n89",
      "n9",
      "n90",
      "n91",
      "n92",
      "n93",
      "n94",
      "n95",
      "n96",
      "n97",
      "n98",
      "n99" },
  header |->
    [NextVS |->
        { "n16",
          "n2",
          "n3",
          "n36",
          "n40",
          "n47",
          "n48",
          "n57",
          "n59",
          "n62",
          "n70",
          "n72",
          "n81",
          "n89",
          "n9",
          "n93" },
      VS |->
        { "n1",
          "n10",
          "n100",
          "n11",
          "n12",
          "n13",
          "n14",
          "n15",
          "n16",
          "n17",
          "n18",
          "n19",
          "n2",
          "n20",
          "n21",
          "n22",
          "n23",
          "n24",
          "n25",
          "n26",
          "n27",
          "n28",
          "n29",
          "n3",
          "n30",
          "n31",
          "n32",
          "n33",
          "n34",
          "n35",
          "n36",
          "n37",
          "n38",
          "n39",
          "n4",
          "n40",
          "n41",
          "n42",
          "n43",
          "n44",
          "n45",
          "n46",
          "n47",
          "n48",
          "n49",
          "n5",
          "n50",
          "n51",
          "n52",
          "n53",
          "n54",
          "n55",
          "n56",
          "n57",
          "n58",
          "n59",
          "n6",
          "n60",
          "n61",
          "n62",
          "n63",
          "n64",
          "n65",
          "n66",
          "n67",
          "n68",
          "n69",
          "n7",
          "n70",
          "n71",
          "n72",
          "n73",
          "n74",
          "n75",
          "n76",
          "n77",
          "n78",
          "n79",
          "n8",
          "n80",
          "n81",
          "n82",
          "n83",
          "n84",
          "n85",
          "n86",
          "n87",
          "n88",
          "n89",
          "n9",
          "n90",
          "n91",
          "n92",
          "n93",
          "n94",
          "n95",
          "n96",
          "n97",
          "n98",
          "n99" },
      height |-> 1,
      lastCommit |-> {},
      time |-> 1]]
/\ state = "working"

(* Transition 5 to State3 *)

State3 ==
/\ Faulty = { "n100",
  "n16",
  "n19",
  "n2",
  "n32",
  "n36",
  "n42",
  "n44",
  "n5",
  "n61",
  "n63",
  "n70",
  "n72",
  "n74",
  "n8",
  "n82",
  "n85",
  "n86" }
/\ blockchain = 1
    :> [NextVS |->
        { "n16",
          "n2",
          "n3",
          "n36",
          "n40",
          "n47",
          "n48",
          "n57",
          "n59",
          "n62",
          "n70",
          "n72",
          "n81",
          "n89",
          "n9",
          "n93" },
      VS |->
        { "n1",
          "n10",
          "n100",
          "n11",
          "n12",
          "n13",
          "n14",
          "n15",
          "n16",
          "n17",
          "n18",
          "n19",
          "n2",
          "n20",
          "n21",
          "n22",
          "n23",
          "n24",
          "n25",
          "n26",
          "n27",
          "n28",
          "n29",
          "n3",
          "n30",
          "n31",
          "n32",
          "n33",
          "n34",
          "n35",
          "n36",
          "n37",
          "n38",
          "n39",
          "n4",
          "n40",
          "n41",
          "n42",
          "n43",
          "n44",
          "n45",
          "n46",
          "n47",
          "n48",
          "n49",
          "n5",
          "n50",
          "n51",
          "n52",
          "n53",
          "n54",
          "n55",
          "n56",
          "n57",
          "n58",
          "n59",
          "n6",
          "n60",
          "n61",
          "n62",
          "n63",
          "n64",
          "n65",
          "n66",
          "n67",
          "n68",
          "n69",
          "n7",
          "n70",
          "n71",
          "n72",
          "n73",
          "n74",
          "n75",
          "n76",
          "n77",
          "n78",
          "n79",
          "n8",
          "n80",
          "n81",
          "n82",
          "n83",
          "n84",
          "n85",
          "n86",
          "n87",
          "n88",
          "n89",
          "n9",
          "n90",
          "n91",
          "n92",
          "n93",
          "n94",
          "n95",
          "n96",
          "n97",
          "n98",
          "n99" },
      height |-> 1,
      lastCommit |-> {},
      time |-> 1]
  @@ 2
    :> [NextVS |->
        { "n1",
          "n10",
          "n100",
          "n11",
          "n12",
          "n13",
          "n14",
          "n15",
          "n16",
          "n17",
          "n18",
          "n19",
          "n20",
          "n21",
          "n22",
          "n23",
          "n25",
          "n26",
          "n27",
          "n28",
          "n29",
          "n30",
          "n31",
          "n32",
          "n33",
          "n34",
          "n35",
          "n36",
          "n37",
          "n38",
          "n39",
          "n4",
          "n40",
          "n41",
          "n42",
          "n43",
          "n45",
          "n46",
          "n48",
          "n49",
          "n5",
          "n50",
          "n51",
          "n52",
          "n53",
          "n54",
          "n55",
          "n56",
          "n58",
          "n59",
          "n6",
          "n60",
          "n61",
          "n64",
          "n65",
          "n66",
          "n67",
          "n68",
          "n69",
          "n7",
          "n71",
          "n73",
          "n75",
          "n76",
          "n77",
          "n78",
          "n8",
          "n82",
          "n83",
          "n84",
          "n85",
          "n86",
          "n88",
          "n89",
          "n90",
          "n91",
          "n92",
          "n93",
          "n94",
          "n95",
          "n96",
          "n97",
          "n98",
          "n99" },
      VS |->
        { "n16",
          "n2",
          "n3",
          "n36",
          "n40",
          "n47",
          "n48",
          "n57",
          "n59",
          "n62",
          "n70",
          "n72",
          "n81",
          "n89",
          "n9",
          "n93" },
      height |-> 2,
      lastCommit |->
        { "n1",
          "n10",
          "n100",
          "n11",
          "n12",
          "n13",
          "n14",
          "n15",
          "n16",
          "n17",
          "n18",
          "n19",
          "n2",
          "n21",
          "n22",
          "n23",
          "n24",
          "n25",
          "n26",
          "n27",
          "n28",
          "n29",
          "n30",
          "n31",
          "n32",
          "n33",
          "n34",
          "n35",
          "n36",
          "n37",
          "n38",
          "n39",
          "n4",
          "n40",
          "n41",
          "n42",
          "n43",
          "n44",
          "n45",
          "n46",
          "n47",
          "n49",
          "n5",
          "n50",
          "n51",
          "n52",
          "n53",
          "n54",
          "n55",
          "n56",
          "n57",
          "n58",
          "n59",
          "n6",
          "n60",
          "n61",
          "n63",
          "n64",
          "n65",
          "n66",
          "n67",
          "n68",
          "n69",
          "n7",
          "n70",
          "n71",
          "n72",
          "n73",
          "n74",
          "n75",
          "n76",
          "n77",
          "n78",
          "n79",
          "n8",
          "n80",
          "n81",
          "n82",
          "n83",
          "n84",
          "n85",
          "n86",
          "n87",
          "n88",
          "n89",
          "n9",
          "n90",
          "n91",
          "n92",
          "n93",
          "n94",
          "n95",
          "n96",
          "n97",
          "n98",
          "n99" },
      time |-> 2]
  @@ 3
    :> [NextVS |->
        { "n1",
          "n10",
          "n100",
          "n11",
          "n12",
          "n13",
          "n14",
          "n15",
          "n16",
          "n17",
          "n18",
          "n19",
          "n2",
          "n20",
          "n21",
          "n22",
          "n23",
          "n24",
          "n25",
          "n26",
          "n27",
          "n28",
          "n29",
          "n3",
          "n30",
          "n31",
          "n32",
          "n33",
          "n34",
          "n35",
          "n36",
          "n37",
          "n38",
          "n39",
          "n4",
          "n40",
          "n41",
          "n42",
          "n43",
          "n44",
          "n45",
          "n46",
          "n47",
          "n48",
          "n49",
          "n5",
          "n50",
          "n51",
          "n52",
          "n53",
          "n54",
          "n55",
          "n56",
          "n57",
          "n58",
          "n59",
          "n6",
          "n60",
          "n61",
          "n62",
          "n63",
          "n64",
          "n65",
          "n66",
          "n67",
          "n68",
          "n69",
          "n7",
          "n70",
          "n71",
          "n72",
          "n73",
          "n74",
          "n75",
          "n76",
          "n77",
          "n78",
          "n79",
          "n8",
          "n80",
          "n81",
          "n82",
          "n83",
          "n84",
          "n85",
          "n86",
          "n87",
          "n88",
          "n89",
          "n9",
          "n90",
          "n91",
          "n92",
          "n93",
          "n94",
          "n95",
          "n96",
          "n97",
          "n98",
          "n99" },
      VS |->
        { "n1",
          "n10",
          "n100",
          "n11",
          "n12",
          "n13",
          "n14",
          "n15",
          "n16",
          "n17",
          "n18",
          "n19",
          "n20",
          "n21",
          "n22",
          "n23",
          "n25",
          "n26",
          "n27",
          "n28",
          "n29",
          "n30",
          "n31",
          "n32",
          "n33",
          "n34",
          "n35",
          "n36",
          "n37",
          "n38",
          "n39",
          "n4",
          "n40",
          "n41",
          "n42",
          "n43",
          "n45",
          "n46",
          "n48",
          "n49",
          "n5",
          "n50",
          "n51",
          "n52",
          "n53",
          "n54",
          "n55",
          "n56",
          "n58",
          "n59",
          "n6",
          "n60",
          "n61",
          "n64",
          "n65",
          "n66",
          "n67",
          "n68",
          "n69",
          "n7",
          "n71",
          "n73",
          "n75",
          "n76",
          "n77",
          "n78",
          "n8",
          "n82",
          "n83",
          "n84",
          "n85",
          "n86",
          "n88",
          "n89",
          "n90",
          "n91",
          "n92",
          "n93",
          "n94",
          "n95",
          "n96",
          "n97",
          "n98",
          "n99" },
      height |-> 3,
      lastCommit |->
        { "n16",
          "n3",
          "n36",
          "n40",
          "n47",
          "n48",
          "n59",
          "n62",
          "n72",
          "n9",
          "n93" },
      time |-> 3]
/\ fetchedLightBlocks = 1
    :> [Commits |->
        { "n1",
          "n10",
          "n100",
          "n11",
          "n12",
          "n13",
          "n14",
          "n15",
          "n16",
          "n17",
          "n18",
          "n19",
          "n2",
          "n20",
          "n21",
          "n22",
          "n23",
          "n24",
          "n25",
          "n26",
          "n27",
          "n28",
          "n29",
          "n3",
          "n30",
          "n31",
          "n32",
          "n33",
          "n34",
          "n35",
          "n36",
          "n37",
          "n38",
          "n39",
          "n4",
          "n40",
          "n41",
          "n42",
          "n43",
          "n44",
          "n45",
          "n46",
          "n47",
          "n48",
          "n49",
          "n5",
          "n50",
          "n51",
          "n52",
          "n53",
          "n54",
          "n55",
          "n56",
          "n57",
          "n58",
          "n59",
          "n6",
          "n60",
          "n61",
          "n62",
          "n63",
          "n64",
          "n65",
          "n66",
          "n67",
          "n68",
          "n69",
          "n7",
          "n70",
          "n71",
          "n72",
          "n73",
          "n74",
          "n75",
          "n76",
          "n77",
          "n78",
          "n79",
          "n8",
          "n80",
          "n81",
          "n82",
          "n83",
          "n84",
          "n85",
          "n86",
          "n87",
          "n88",
          "n89",
          "n9",
          "n90",
          "n91",
          "n92",
          "n93",
          "n94",
          "n95",
          "n96",
          "n97",
          "n98",
          "n99" },
      header |->
        [NextVS |->
            { "n16",
              "n2",
              "n3",
              "n36",
              "n40",
              "n47",
              "n48",
              "n57",
              "n59",
              "n62",
              "n70",
              "n72",
              "n81",
              "n89",
              "n9",
              "n93" },
          VS |->
            { "n1",
              "n10",
              "n100",
              "n11",
              "n12",
              "n13",
              "n14",
              "n15",
              "n16",
              "n17",
              "n18",
              "n19",
              "n2",
              "n20",
              "n21",
              "n22",
              "n23",
              "n24",
              "n25",
              "n26",
              "n27",
              "n28",
              "n29",
              "n3",
              "n30",
              "n31",
              "n32",
              "n33",
              "n34",
              "n35",
              "n36",
              "n37",
              "n38",
              "n39",
              "n4",
              "n40",
              "n41",
              "n42",
              "n43",
              "n44",
              "n45",
              "n46",
              "n47",
              "n48",
              "n49",
              "n5",
              "n50",
              "n51",
              "n52",
              "n53",
              "n54",
              "n55",
              "n56",
              "n57",
              "n58",
              "n59",
              "n6",
              "n60",
              "n61",
              "n62",
              "n63",
              "n64",
              "n65",
              "n66",
              "n67",
              "n68",
              "n69",
              "n7",
              "n70",
              "n71",
              "n72",
              "n73",
              "n74",
              "n75",
              "n76",
              "n77",
              "n78",
              "n79",
              "n8",
              "n80",
              "n81",
              "n82",
              "n83",
              "n84",
              "n85",
              "n86",
              "n87",
              "n88",
              "n89",
              "n9",
              "n90",
              "n91",
              "n92",
              "n93",
              "n94",
              "n95",
              "n96",
              "n97",
              "n98",
              "n99" },
          height |-> 1,
          lastCommit |-> {},
          time |-> 1]]
  @@ 2
    :> [Commits |-> { "n16", "n2", "n42", "n70", "n72" },
      header |->
        [NextVS |->
            { "n1",
              "n10",
              "n100",
              "n11",
              "n12",
              "n13",
              "n14",
              "n15",
              "n17",
              "n18",
              "n19",
              "n20",
              "n21",
              "n22",
              "n23",
              "n24",
              "n25",
              "n26",
              "n27",
              "n28",
              "n29",
              "n30",
              "n31",
              "n32",
              "n33",
              "n34",
              "n35",
              "n36",
              "n37",
              "n38",
              "n39",
              "n4",
              "n40",
              "n41",
              "n42",
              "n43",
              "n44",
              "n45",
              "n46",
              "n48",
              "n49",
              "n5",
              "n50",
              "n51",
              "n52",
              "n53",
              "n54",
              "n55",
              "n56",
              "n58",
              "n59",
              "n6",
              "n60",
              "n61",
              "n63",
              "n64",
              "n65",
              "n66",
              "n67",
              "n68",
              "n69",
              "n7",
              "n70",
              "n71",
              "n72",
              "n73",
              "n74",
              "n75",
              "n76",
              "n77",
              "n78",
              "n8",
              "n80",
              "n82",
              "n83",
              "n84",
              "n85",
              "n86",
              "n87",
              "n88",
              "n90",
              "n91",
              "n92",
              "n94",
              "n95",
              "n96",
              "n97",
              "n98",
              "n99" },
          VS |->
            { "n20",
              "n36",
              "n45",
              "n48",
              "n50",
              "n64",
              "n73",
              "n74",
              "n88",
              "n98" },
          height |-> 2,
          lastCommit |->
            { "n1",
              "n10",
              "n100",
              "n11",
              "n12",
              "n13",
              "n14",
              "n15",
              "n16",
              "n17",
              "n18",
              "n19",
              "n2",
              "n21",
              "n22",
              "n23",
              "n24",
              "n25",
              "n26",
              "n27",
              "n28",
              "n29",
              "n30",
              "n31",
              "n32",
              "n33",
              "n34",
              "n35",
              "n36",
              "n37",
              "n38",
              "n39",
              "n4",
              "n40",
              "n41",
              "n42",
              "n43",
              "n44",
              "n45",
              "n46",
              "n47",
              "n49",
              "n5",
              "n50",
              "n51",
              "n52",
              "n53",
              "n54",
              "n55",
              "n56",
              "n57",
              "n58",
              "n59",
              "n6",
              "n60",
              "n61",
              "n63",
              "n64",
              "n65",
              "n66",
              "n67",
              "n68",
              "n69",
              "n7",
              "n70",
              "n71",
              "n72",
              "n73",
              "n74",
              "n75",
              "n76",
              "n77",
              "n78",
              "n79",
              "n8",
              "n80",
              "n81",
              "n82",
              "n83",
              "n84",
              "n85",
              "n86",
              "n87",
              "n88",
              "n89",
              "n9",
              "n90",
              "n91",
              "n92",
              "n93",
              "n94",
              "n95",
              "n96",
              "n97",
              "n98",
              "n99" },
          time |-> 2]]
/\ history = 0
    :> [current |->
        [Commits |->
            { "n1",
              "n10",
              "n100",
              "n11",
              "n12",
              "n13",
              "n14",
              "n15",
              "n16",
              "n17",
              "n18",
              "n19",
              "n2",
              "n20",
              "n21",
              "n22",
              "n23",
              "n24",
              "n25",
              "n26",
              "n27",
              "n28",
              "n29",
              "n3",
              "n30",
              "n31",
              "n32",
              "n33",
              "n34",
              "n35",
              "n36",
              "n37",
              "n38",
              "n39",
              "n4",
              "n40",
              "n41",
              "n42",
              "n43",
              "n44",
              "n45",
              "n46",
              "n47",
              "n48",
              "n49",
              "n5",
              "n50",
              "n51",
              "n52",
              "n53",
              "n54",
              "n55",
              "n56",
              "n57",
              "n58",
              "n59",
              "n6",
              "n60",
              "n61",
              "n62",
              "n63",
              "n64",
              "n65",
              "n66",
              "n67",
              "n68",
              "n69",
              "n7",
              "n70",
              "n71",
              "n72",
              "n73",
              "n74",
              "n75",
              "n76",
              "n77",
              "n78",
              "n79",
              "n8",
              "n80",
              "n81",
              "n82",
              "n83",
              "n84",
              "n85",
              "n86",
              "n87",
              "n88",
              "n89",
              "n9",
              "n90",
              "n91",
              "n92",
              "n93",
              "n94",
              "n95",
              "n96",
              "n97",
              "n98",
              "n99" },
          header |->
            [NextVS |->
                { "n16",
                  "n2",
                  "n3",
                  "n36",
                  "n40",
                  "n47",
                  "n48",
                  "n57",
                  "n59",
                  "n62",
                  "n70",
                  "n72",
                  "n81",
                  "n89",
                  "n9",
                  "n93" },
              VS |->
                { "n1",
                  "n10",
                  "n100",
                  "n11",
                  "n12",
                  "n13",
                  "n14",
                  "n15",
                  "n16",
                  "n17",
                  "n18",
                  "n19",
                  "n2",
                  "n20",
                  "n21",
                  "n22",
                  "n23",
                  "n24",
                  "n25",
                  "n26",
                  "n27",
                  "n28",
                  "n29",
                  "n3",
                  "n30",
                  "n31",
                  "n32",
                  "n33",
                  "n34",
                  "n35",
                  "n36",
                  "n37",
                  "n38",
                  "n39",
                  "n4",
                  "n40",
                  "n41",
                  "n42",
                  "n43",
                  "n44",
                  "n45",
                  "n46",
                  "n47",
                  "n48",
                  "n49",
                  "n5",
                  "n50",
                  "n51",
                  "n52",
                  "n53",
                  "n54",
                  "n55",
                  "n56",
                  "n57",
                  "n58",
                  "n59",
                  "n6",
                  "n60",
                  "n61",
                  "n62",
                  "n63",
                  "n64",
                  "n65",
                  "n66",
                  "n67",
                  "n68",
                  "n69",
                  "n7",
                  "n70",
                  "n71",
                  "n72",
                  "n73",
                  "n74",
                  "n75",
                  "n76",
                  "n77",
                  "n78",
                  "n79",
                  "n8",
                  "n80",
                  "n81",
                  "n82",
                  "n83",
                  "n84",
                  "n85",
                  "n86",
                  "n87",
                  "n88",
                  "n89",
                  "n9",
                  "n90",
                  "n91",
                  "n92",
                  "n93",
                  "n94",
                  "n95",
                  "n96",
                  "n97",
                  "n98",
                  "n99" },
              height |-> 1,
              lastCommit |-> {},
              time |-> 1]],
      now |-> 1402,
      verdict |-> "SUCCESS",
      verified |->
        [Commits |->
            { "n1",
              "n10",
              "n100",
              "n11",
              "n12",
              "n13",
              "n14",
              "n15",
              "n16",
              "n17",
              "n18",
              "n19",
              "n2",
              "n20",
              "n21",
              "n22",
              "n23",
              "n24",
              "n25",
              "n26",
              "n27",
              "n28",
              "n29",
              "n3",
              "n30",
              "n31",
              "n32",
              "n33",
              "n34",
              "n35",
              "n36",
              "n37",
              "n38",
              "n39",
              "n4",
              "n40",
              "n41",
              "n42",
              "n43",
              "n44",
              "n45",
              "n46",
              "n47",
              "n48",
              "n49",
              "n5",
              "n50",
              "n51",
              "n52",
              "n53",
              "n54",
              "n55",
              "n56",
              "n57",
              "n58",
              "n59",
              "n6",
              "n60",
              "n61",
              "n62",
              "n63",
              "n64",
              "n65",
              "n66",
              "n67",
              "n68",
              "n69",
              "n7",
              "n70",
              "n71",
              "n72",
              "n73",
              "n74",
              "n75",
              "n76",
              "n77",
              "n78",
              "n79",
              "n8",
              "n80",
              "n81",
              "n82",
              "n83",
              "n84",
              "n85",
              "n86",
              "n87",
              "n88",
              "n89",
              "n9",
              "n90",
              "n91",
              "n92",
              "n93",
              "n94",
              "n95",
              "n96",
              "n97",
              "n98",
              "n99" },
          header |->
            [NextVS |->
                { "n16",
                  "n2",
                  "n3",
                  "n36",
                  "n40",
                  "n47",
                  "n48",
                  "n57",
                  "n59",
                  "n62",
                  "n70",
                  "n72",
                  "n81",
                  "n89",
                  "n9",
                  "n93" },
              VS |->
                { "n1",
                  "n10",
                  "n100",
                  "n11",
                  "n12",
                  "n13",
                  "n14",
                  "n15",
                  "n16",
                  "n17",
                  "n18",
                  "n19",
                  "n2",
                  "n20",
                  "n21",
                  "n22",
                  "n23",
                  "n24",
                  "n25",
                  "n26",
                  "n27",
                  "n28",
                  "n29",
                  "n3",
                  "n30",
                  "n31",
                  "n32",
                  "n33",
                  "n34",
                  "n35",
                  "n36",
                  "n37",
                  "n38",
                  "n39",
                  "n4",
                  "n40",
                  "n41",
                  "n42",
                  "n43",
                  "n44",
                  "n45",
                  "n46",
                  "n47",
                  "n48",
                  "n49",
                  "n5",
                  "n50",
                  "n51",
                  "n52",
                  "n53",
                  "n54",
                  "n55",
                  "n56",
                  "n57",
                  "n58",
                  "n59",
                  "n6",
                  "n60",
                  "n61",
                  "n62",
                  "n63",
                  "n64",
                  "n65",
                  "n66",
                  "n67",
                  "n68",
                  "n69",
                  "n7",
                  "n70",
                  "n71",
                  "n72",
                  "n73",
                  "n74",
                  "n75",
                  "n76",
                  "n77",
                  "n78",
                  "n79",
                  "n8",
                  "n80",
                  "n81",
                  "n82",
                  "n83",
                  "n84",
                  "n85",
                  "n86",
                  "n87",
                  "n88",
                  "n89",
                  "n9",
                  "n90",
                  "n91",
                  "n92",
                  "n93",
                  "n94",
                  "n95",
                  "n96",
                  "n97",
                  "n98",
                  "n99" },
              height |-> 1,
              lastCommit |-> {},
              time |-> 1]]]
  @@ 1
    :> [current |->
        [Commits |-> { "n16", "n2", "n42", "n70", "n72" },
          header |->
            [NextVS |->
                { "n1",
                  "n10",
                  "n100",
                  "n11",
                  "n12",
                  "n13",
                  "n14",
                  "n15",
                  "n17",
                  "n18",
                  "n19",
                  "n20",
                  "n21",
                  "n22",
                  "n23",
                  "n24",
                  "n25",
                  "n26",
                  "n27",
                  "n28",
                  "n29",
                  "n30",
                  "n31",
                  "n32",
                  "n33",
                  "n34",
                  "n35",
                  "n36",
                  "n37",
                  "n38",
                  "n39",
                  "n4",
                  "n40",
                  "n41",
                  "n42",
                  "n43",
                  "n44",
                  "n45",
                  "n46",
                  "n48",
                  "n49",
                  "n5",
                  "n50",
                  "n51",
                  "n52",
                  "n53",
                  "n54",
                  "n55",
                  "n56",
                  "n58",
                  "n59",
                  "n6",
                  "n60",
                  "n61",
                  "n63",
                  "n64",
                  "n65",
                  "n66",
                  "n67",
                  "n68",
                  "n69",
                  "n7",
                  "n70",
                  "n71",
                  "n72",
                  "n73",
                  "n74",
                  "n75",
                  "n76",
                  "n77",
                  "n78",
                  "n8",
                  "n80",
                  "n82",
                  "n83",
                  "n84",
                  "n85",
                  "n86",
                  "n87",
                  "n88",
                  "n90",
                  "n91",
                  "n92",
                  "n94",
                  "n95",
                  "n96",
                  "n97",
                  "n98",
                  "n99" },
              VS |->
                { "n20",
                  "n36",
                  "n45",
                  "n48",
                  "n50",
                  "n64",
                  "n73",
                  "n74",
                  "n88",
                  "n98" },
              height |-> 2,
              lastCommit |->
                { "n1",
                  "n10",
                  "n100",
                  "n11",
                  "n12",
                  "n13",
                  "n14",
                  "n15",
                  "n16",
                  "n17",
                  "n18",
                  "n19",
                  "n2",
                  "n21",
                  "n22",
                  "n23",
                  "n24",
                  "n25",
                  "n26",
                  "n27",
                  "n28",
                  "n29",
                  "n30",
                  "n31",
                  "n32",
                  "n33",
                  "n34",
                  "n35",
                  "n36",
                  "n37",
                  "n38",
                  "n39",
                  "n4",
                  "n40",
                  "n41",
                  "n42",
                  "n43",
                  "n44",
                  "n45",
                  "n46",
                  "n47",
                  "n49",
                  "n5",
                  "n50",
                  "n51",
                  "n52",
                  "n53",
                  "n54",
                  "n55",
                  "n56",
                  "n57",
                  "n58",
                  "n59",
                  "n6",
                  "n60",
                  "n61",
                  "n63",
                  "n64",
                  "n65",
                  "n66",
                  "n67",
                  "n68",
                  "n69",
                  "n7",
                  "n70",
                  "n71",
                  "n72",
                  "n73",
                  "n74",
                  "n75",
                  "n76",
                  "n77",
                  "n78",
                  "n79",
                  "n8",
                  "n80",
                  "n81",
                  "n82",
                  "n83",
                  "n84",
                  "n85",
                  "n86",
                  "n87",
                  "n88",
                  "n89",
                  "n9",
                  "n90",
                  "n91",
                  "n92",
                  "n93",
                  "n94",
                  "n95",
                  "n96",
                  "n97",
                  "n98",
                  "n99" },
              time |-> 2]],
      now |-> 1402,
      verdict |-> "INVALID",
      verified |->
        [Commits |->
            { "n1",
              "n10",
              "n100",
              "n11",
              "n12",
              "n13",
              "n14",
              "n15",
              "n16",
              "n17",
              "n18",
              "n19",
              "n2",
              "n20",
              "n21",
              "n22",
              "n23",
              "n24",
              "n25",
              "n26",
              "n27",
              "n28",
              "n29",
              "n3",
              "n30",
              "n31",
              "n32",
              "n33",
              "n34",
              "n35",
              "n36",
              "n37",
              "n38",
              "n39",
              "n4",
              "n40",
              "n41",
              "n42",
              "n43",
              "n44",
              "n45",
              "n46",
              "n47",
              "n48",
              "n49",
              "n5",
              "n50",
              "n51",
              "n52",
              "n53",
              "n54",
              "n55",
              "n56",
              "n57",
              "n58",
              "n59",
              "n6",
              "n60",
              "n61",
              "n62",
              "n63",
              "n64",
              "n65",
              "n66",
              "n67",
              "n68",
              "n69",
              "n7",
              "n70",
              "n71",
              "n72",
              "n73",
              "n74",
              "n75",
              "n76",
              "n77",
              "n78",
              "n79",
              "n8",
              "n80",
              "n81",
              "n82",
              "n83",
              "n84",
              "n85",
              "n86",
              "n87",
              "n88",
              "n89",
              "n9",
              "n90",
              "n91",
              "n92",
              "n93",
              "n94",
              "n95",
              "n96",
              "n97",
              "n98",
              "n99" },
          header |->
            [NextVS |->
                { "n16",
                  "n2",
                  "n3",
                  "n36",
                  "n40",
                  "n47",
                  "n48",
                  "n57",
                  "n59",
                  "n62",
                  "n70",
                  "n72",
                  "n81",
                  "n89",
                  "n9",
                  "n93" },
              VS |->
                { "n1",
                  "n10",
                  "n100",
                  "n11",
                  "n12",
                  "n13",
                  "n14",
                  "n15",
                  "n16",
                  "n17",
                  "n18",
                  "n19",
                  "n2",
                  "n20",
                  "n21",
                  "n22",
                  "n23",
                  "n24",
                  "n25",
                  "n26",
                  "n27",
                  "n28",
                  "n29",
                  "n3",
                  "n30",
                  "n31",
                  "n32",
                  "n33",
                  "n34",
                  "n35",
                  "n36",
                  "n37",
                  "n38",
                  "n39",
                  "n4",
                  "n40",
                  "n41",
                  "n42",
                  "n43",
                  "n44",
                  "n45",
                  "n46",
                  "n47",
                  "n48",
                  "n49",
                  "n5",
                  "n50",
                  "n51",
                  "n52",
                  "n53",
                  "n54",
                  "n55",
                  "n56",
                  "n57",
                  "n58",
                  "n59",
                  "n6",
                  "n60",
                  "n61",
                  "n62",
                  "n63",
                  "n64",
                  "n65",
                  "n66",
                  "n67",
                  "n68",
                  "n69",
                  "n7",
                  "n70",
                  "n71",
                  "n72",
                  "n73",
                  "n74",
                  "n75",
                  "n76",
                  "n77",
                  "n78",
                  "n79",
                  "n8",
                  "n80",
                  "n81",
                  "n82",
                  "n83",
                  "n84",
                  "n85",
                  "n86",
                  "n87",
                  "n88",
                  "n89",
                  "n9",
                  "n90",
                  "n91",
                  "n92",
                  "n93",
                  "n94",
                  "n95",
                  "n96",
                  "n97",
                  "n98",
                  "n99" },
              height |-> 1,
              lastCommit |-> {},
              time |-> 1]]]
/\ latestVerified = [Commits |->
    { "n1",
      "n10",
      "n100",
      "n11",
      "n12",
      "n13",
      "n14",
      "n15",
      "n16",
      "n17",
      "n18",
      "n19",
      "n2",
      "n20",
      "n21",
      "n22",
      "n23",
      "n24",
      "n25",
      "n26",
      "n27",
      "n28",
      "n29",
      "n3",
      "n30",
      "n31",
      "n32",
      "n33",
      "n34",
      "n35",
      "n36",
      "n37",
      "n38",
      "n39",
      "n4",
      "n40",
      "n41",
      "n42",
      "n43",
      "n44",
      "n45",
      "n46",
      "n47",
      "n48",
      "n49",
      "n5",
      "n50",
      "n51",
      "n52",
      "n53",
      "n54",
      "n55",
      "n56",
      "n57",
      "n58",
      "n59",
      "n6",
      "n60",
      "n61",
      "n62",
      "n63",
      "n64",
      "n65",
      "n66",
      "n67",
      "n68",
      "n69",
      "n7",
      "n70",
      "n71",
      "n72",
      "n73",
      "n74",
      "n75",
      "n76",
      "n77",
      "n78",
      "n79",
      "n8",
      "n80",
      "n81",
      "n82",
      "n83",
      "n84",
      "n85",
      "n86",
      "n87",
      "n88",
      "n89",
      "n9",
      "n90",
      "n91",
      "n92",
      "n93",
      "n94",
      "n95",
      "n96",
      "n97",
      "n98",
      "n99" },
  header |->
    [NextVS |->
        { "n16",
          "n2",
          "n3",
          "n36",
          "n40",
          "n47",
          "n48",
          "n57",
          "n59",
          "n62",
          "n70",
          "n72",
          "n81",
          "n89",
          "n9",
          "n93" },
      VS |->
        { "n1",
          "n10",
          "n100",
          "n11",
          "n12",
          "n13",
          "n14",
          "n15",
          "n16",
          "n17",
          "n18",
          "n19",
          "n2",
          "n20",
          "n21",
          "n22",
          "n23",
          "n24",
          "n25",
          "n26",
          "n27",
          "n28",
          "n29",
          "n3",
          "n30",
          "n31",
          "n32",
          "n33",
          "n34",
          "n35",
          "n36",
          "n37",
          "n38",
          "n39",
          "n4",
          "n40",
          "n41",
          "n42",
          "n43",
          "n44",
          "n45",
          "n46",
          "n47",
          "n48",
          "n49",
          "n5",
          "n50",
          "n51",
          "n52",
          "n53",
          "n54",
          "n55",
          "n56",
          "n57",
          "n58",
          "n59",
          "n6",
          "n60",
          "n61",
          "n62",
          "n63",
          "n64",
          "n65",
          "n66",
          "n67",
          "n68",
          "n69",
          "n7",
          "n70",
          "n71",
          "n72",
          "n73",
          "n74",
          "n75",
          "n76",
          "n77",
          "n78",
          "n79",
          "n8",
          "n80",
          "n81",
          "n82",
          "n83",
          "n84",
          "n85",
          "n86",
          "n87",
          "n88",
          "n89",
          "n9",
          "n90",
          "n91",
          "n92",
          "n93",
          "n94",
          "n95",
          "n96",
          "n97",
          "n98",
          "n99" },
      height |-> 1,
      lastCommit |-> {},
      time |-> 1]]
/\ lightBlockStatus = 1 :> "StateVerified" @@ 2 :> "StateFailed"
/\ nextHeight = 2
/\ now = 1402
/\ nprobes = 1
/\ prevCurrent = [Commits |-> { "n16", "n2", "n42", "n70", "n72" },
  header |->
    [NextVS |->
        { "n1",
          "n10",
          "n100",
          "n11",
          "n12",
          "n13",
          "n14",
          "n15",
          "n17",
          "n18",
          "n19",
          "n20",
          "n21",
          "n22",
          "n23",
          "n24",
          "n25",
          "n26",
          "n27",
          "n28",
          "n29",
          "n30",
          "n31",
          "n32",
          "n33",
          "n34",
          "n35",
          "n36",
          "n37",
          "n38",
          "n39",
          "n4",
          "n40",
          "n41",
          "n42",
          "n43",
          "n44",
          "n45",
          "n46",
          "n48",
          "n49",
          "n5",
          "n50",
          "n51",
          "n52",
          "n53",
          "n54",
          "n55",
          "n56",
          "n58",
          "n59",
          "n6",
          "n60",
          "n61",
          "n63",
          "n64",
          "n65",
          "n66",
          "n67",
          "n68",
          "n69",
          "n7",
          "n70",
          "n71",
          "n72",
          "n73",
          "n74",
          "n75",
          "n76",
          "n77",
          "n78",
          "n8",
          "n80",
          "n82",
          "n83",
          "n84",
          "n85",
          "n86",
          "n87",
          "n88",
          "n90",
          "n91",
          "n92",
          "n94",
          "n95",
          "n96",
          "n97",
          "n98",
          "n99" },
      VS |->
        { "n20", "n36", "n45", "n48", "n50", "n64", "n73", "n74", "n88", "n98" },
      height |-> 2,
      lastCommit |->
        { "n1",
          "n10",
          "n100",
          "n11",
          "n12",
          "n13",
          "n14",
          "n15",
          "n16",
          "n17",
          "n18",
          "n19",
          "n2",
          "n21",
          "n22",
          "n23",
          "n24",
          "n25",
          "n26",
          "n27",
          "n28",
          "n29",
          "n30",
          "n31",
          "n32",
          "n33",
          "n34",
          "n35",
          "n36",
          "n37",
          "n38",
          "n39",
          "n4",
          "n40",
          "n41",
          "n42",
          "n43",
          "n44",
          "n45",
          "n46",
          "n47",
          "n49",
          "n5",
          "n50",
          "n51",
          "n52",
          "n53",
          "n54",
          "n55",
          "n56",
          "n57",
          "n58",
          "n59",
          "n6",
          "n60",
          "n61",
          "n63",
          "n64",
          "n65",
          "n66",
          "n67",
          "n68",
          "n69",
          "n7",
          "n70",
          "n71",
          "n72",
          "n73",
          "n74",
          "n75",
          "n76",
          "n77",
          "n78",
          "n79",
          "n8",
          "n80",
          "n81",
          "n82",
          "n83",
          "n84",
          "n85",
          "n86",
          "n87",
          "n88",
          "n89",
          "n9",
          "n90",
          "n91",
          "n92",
          "n93",
          "n94",
          "n95",
          "n96",
          "n97",
          "n98",
          "n99" },
      time |-> 2]]
/\ prevNow = 1402
/\ prevVerdict = "INVALID"
/\ prevVerified = [Commits |->
    { "n1",
      "n10",
      "n100",
      "n11",
      "n12",
      "n13",
      "n14",
      "n15",
      "n16",
      "n17",
      "n18",
      "n19",
      "n2",
      "n20",
      "n21",
      "n22",
      "n23",
      "n24",
      "n25",
      "n26",
      "n27",
      "n28",
      "n29",
      "n3",
      "n30",
      "n31",
      "n32",
      "n33",
      "n34",
      "n35",
      "n36",
      "n37",
      "n38",
      "n39",
      "n4",
      "n40",
      "n41",
      "n42",
      "n43",
      "n44",
      "n45",
      "n46",
      "n47",
      "n48",
      "n49",
      "n5",
      "n50",
      "n51",
      "n52",
      "n53",
      "n54",
      "n55",
      "n56",
      "n57",
      "n58",
      "n59",
      "n6",
      "n60",
      "n61",
      "n62",
      "n63",
      "n64",
      "n65",
      "n66",
      "n67",
      "n68",
      "n69",
      "n7",
      "n70",
      "n71",
      "n72",
      "n73",
      "n74",
      "n75",
      "n76",
      "n77",
      "n78",
      "n79",
      "n8",
      "n80",
      "n81",
      "n82",
      "n83",
      "n84",
      "n85",
      "n86",
      "n87",
      "n88",
      "n89",
      "n9",
      "n90",
      "n91",
      "n92",
      "n93",
      "n94",
      "n95",
      "n96",
      "n97",
      "n98",
      "n99" },
  header |->
    [NextVS |->
        { "n16",
          "n2",
          "n3",
          "n36",
          "n40",
          "n47",
          "n48",
          "n57",
          "n59",
          "n62",
          "n70",
          "n72",
          "n81",
          "n89",
          "n9",
          "n93" },
      VS |->
        { "n1",
          "n10",
          "n100",
          "n11",
          "n12",
          "n13",
          "n14",
          "n15",
          "n16",
          "n17",
          "n18",
          "n19",
          "n2",
          "n20",
          "n21",
          "n22",
          "n23",
          "n24",
          "n25",
          "n26",
          "n27",
          "n28",
          "n29",
          "n3",
          "n30",
          "n31",
          "n32",
          "n33",
          "n34",
          "n35",
          "n36",
          "n37",
          "n38",
          "n39",
          "n4",
          "n40",
          "n41",
          "n42",
          "n43",
          "n44",
          "n45",
          "n46",
          "n47",
          "n48",
          "n49",
          "n5",
          "n50",
          "n51",
          "n52",
          "n53",
          "n54",
          "n55",
          "n56",
          "n57",
          "n58",
          "n59",
          "n6",
          "n60",
          "n61",
          "n62",
          "n63",
          "n64",
          "n65",
          "n66",
          "n67",
          "n68",
          "n69",
          "n7",
          "n70",
          "n71",
          "n72",
          "n73",
          "n74",
          "n75",
          "n76",
          "n77",
          "n78",
          "n79",
          "n8",
          "n80",
          "n81",
          "n82",
          "n83",
          "n84",
          "n85",
          "n86",
          "n87",
          "n88",
          "n89",
          "n9",
          "n90",
          "n91",
          "n92",
          "n93",
          "n94",
          "n95",
          "n96",
          "n97",
          "n98",
          "n99" },
      height |-> 1,
      lastCommit |-> {},
      time |-> 1]]
/\ state = "finishedFailure"

(* The following formula holds true in the last state and violates the invariant *)

InvariantViolation ==
  state = "finishedFailure" /\ Cardinality((DOMAIN fetchedLightBlocks)) = 2

================================================================================
\* Created by Apalache on Wed Nov 18 13:53:58 UTC 2020
\* https://github.com/informalsystems/apalache