------------------------- MODULE counterexample ------------------------- EXTENDS MC100_2_faulty (* Initial state *) State1 == TRUE (* Transition 0 to State2 *) State2 == /\ Faulty = { "n1", "n10", "n11", "n13", "n14", "n16", "n17", "n18", "n22", "n23", "n25", "n29", "n34", "n36", "n4", "n42", "n43", "n46", "n47", "n5", "n53", "n6", "n60", "n63", "n66", "n7", "n71", "n75", "n78", "n81", "n82", "n88", "n93", "n99" } /\ blockchain = 1 :> [NextVS |-> { "n10", "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", "n36", "n37", "n38", "n4", "n40", "n41", "n42", "n43", "n44", "n45", "n46", "n47", "n48", "n49", "n5", "n51", "n52", "n54", "n55", "n57", "n58", "n59", "n6", "n60", "n61", "n62", "n63", "n64", "n65", "n66", "n67", "n68", "n69", "n7", "n70", "n71", "n72", "n73", "n74", "n75", "n76", "n77", "n79", "n80", "n81", "n83", "n84", "n85", "n86", "n87", "n88", "n89", "n9", "n90", "n91", "n94", "n95", "n97", "n98" }, 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 |-> { "n100", "n11", "n12", "n14", "n2", "n22", "n26", "n28", "n31", "n33", "n39", "n40", "n41", "n42", "n44", "n46", "n48", "n49", "n50", "n55", "n56", "n58", "n59", "n69", "n70", "n73", "n76", "n82", "n88", "n96", "n99" }, VS |-> { "n10", "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", "n36", "n37", "n38", "n4", "n40", "n41", "n42", "n43", "n44", "n45", "n46", "n47", "n48", "n49", "n5", "n51", "n52", "n54", "n55", "n57", "n58", "n59", "n6", "n60", "n61", "n62", "n63", "n64", "n65", "n66", "n67", "n68", "n69", "n7", "n70", "n71", "n72", "n73", "n74", "n75", "n76", "n77", "n79", "n80", "n81", "n83", "n84", "n85", "n86", "n87", "n88", "n89", "n9", "n90", "n91", "n94", "n95", "n97", "n98" }, height |-> 2, lastCommit |-> { "n1", "n10", "n100", "n11", "n12", "n13", "n14", "n15", "n16", "n18", "n19", "n2", "n21", "n22", "n23", "n24", "n25", "n26", "n28", "n29", "n3", "n30", "n31", "n32", "n33", "n35", "n36", "n37", "n4", "n40", "n41", "n43", "n44", "n45", "n46", "n47", "n48", "n49", "n5", "n50", "n51", "n53", "n55", "n56", "n57", "n58", "n6", "n61", "n62", "n63", "n65", "n67", "n69", "n7", "n70", "n71", "n72", "n73", "n75", "n77", "n79", "n8", "n80", "n81", "n82", "n83", "n84", "n87", "n88", "n89", "n9", "n91", "n92", "n93", "n95", "n97", "n98" }, 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 |-> { "n100", "n11", "n12", "n14", "n2", "n22", "n26", "n28", "n31", "n33", "n39", "n40", "n41", "n42", "n44", "n46", "n48", "n49", "n50", "n55", "n56", "n58", "n59", "n69", "n70", "n73", "n76", "n82", "n88", "n96", "n99" }, height |-> 3, lastCommit |-> { "n10", "n11", "n14", "n15", "n2", "n21", "n22", "n25", "n26", "n27", "n28", "n3", "n30", "n31", "n33", "n34", "n36", "n37", "n38", "n44", "n45", "n46", "n47", "n51", "n52", "n54", "n57", "n58", "n59", "n6", "n60", "n61", "n62", "n64", "n65", "n66", "n68", "n69", "n7", "n70", "n71", "n72", "n73", "n74", "n76", "n77", "n79", "n81", "n83", "n84", "n85", "n86", "n87", "n89", "n9", "n90", "n97", "n98" }, 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 |-> { "n10", "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", "n36", "n37", "n38", "n4", "n40", "n41", "n42", "n43", "n44", "n45", "n46", "n47", "n48", "n49", "n5", "n51", "n52", "n54", "n55", "n57", "n58", "n59", "n6", "n60", "n61", "n62", "n63", "n64", "n65", "n66", "n67", "n68", "n69", "n7", "n70", "n71", "n72", "n73", "n74", "n75", "n76", "n77", "n79", "n80", "n81", "n83", "n84", "n85", "n86", "n87", "n88", "n89", "n9", "n90", "n91", "n94", "n95", "n97", "n98" }, 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 |-> { "n10", "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", "n36", "n37", "n38", "n4", "n40", "n41", "n42", "n43", "n44", "n45", "n46", "n47", "n48", "n49", "n5", "n51", "n52", "n54", "n55", "n57", "n58", "n59", "n6", "n60", "n61", "n62", "n63", "n64", "n65", "n66", "n67", "n68", "n69", "n7", "n70", "n71", "n72", "n73", "n74", "n75", "n76", "n77", "n79", "n80", "n81", "n83", "n84", "n85", "n86", "n87", "n88", "n89", "n9", "n90", "n91", "n94", "n95", "n97", "n98" }, 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 |-> 3, 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 |-> { "n10", "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", "n36", "n37", "n38", "n4", "n40", "n41", "n42", "n43", "n44", "n45", "n46", "n47", "n48", "n49", "n5", "n51", "n52", "n54", "n55", "n57", "n58", "n59", "n6", "n60", "n61", "n62", "n63", "n64", "n65", "n66", "n67", "n68", "n69", "n7", "n70", "n71", "n72", "n73", "n74", "n75", "n76", "n77", "n79", "n80", "n81", "n83", "n84", "n85", "n86", "n87", "n88", "n89", "n9", "n90", "n91", "n94", "n95", "n97", "n98" }, 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 |-> { "n10", "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", "n36", "n37", "n38", "n4", "n40", "n41", "n42", "n43", "n44", "n45", "n46", "n47", "n48", "n49", "n5", "n51", "n52", "n54", "n55", "n57", "n58", "n59", "n6", "n60", "n61", "n62", "n63", "n64", "n65", "n66", "n67", "n68", "n69", "n7", "n70", "n71", "n72", "n73", "n74", "n75", "n76", "n77", "n79", "n80", "n81", "n83", "n84", "n85", "n86", "n87", "n88", "n89", "n9", "n90", "n91", "n94", "n95", "n97", "n98" }, 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 = 3 /\ 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 |-> { "n10", "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", "n36", "n37", "n38", "n4", "n40", "n41", "n42", "n43", "n44", "n45", "n46", "n47", "n48", "n49", "n5", "n51", "n52", "n54", "n55", "n57", "n58", "n59", "n6", "n60", "n61", "n62", "n63", "n64", "n65", "n66", "n67", "n68", "n69", "n7", "n70", "n71", "n72", "n73", "n74", "n75", "n76", "n77", "n79", "n80", "n81", "n83", "n84", "n85", "n86", "n87", "n88", "n89", "n9", "n90", "n91", "n94", "n95", "n97", "n98" }, 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 = 3 /\ 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 |-> { "n10", "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", "n36", "n37", "n38", "n4", "n40", "n41", "n42", "n43", "n44", "n45", "n46", "n47", "n48", "n49", "n5", "n51", "n52", "n54", "n55", "n57", "n58", "n59", "n6", "n60", "n61", "n62", "n63", "n64", "n65", "n66", "n67", "n68", "n69", "n7", "n70", "n71", "n72", "n73", "n74", "n75", "n76", "n77", "n79", "n80", "n81", "n83", "n84", "n85", "n86", "n87", "n88", "n89", "n9", "n90", "n91", "n94", "n95", "n97", "n98" }, 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 3 to State3 *) State3 == /\ Faulty = { "n1", "n10", "n11", "n13", "n14", "n16", "n17", "n18", "n22", "n23", "n25", "n29", "n34", "n36", "n4", "n42", "n43", "n46", "n47", "n5", "n53", "n6", "n60", "n63", "n66", "n7", "n71", "n75", "n78", "n81", "n82", "n88", "n93", "n99" } /\ blockchain = 1 :> [NextVS |-> { "n10", "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", "n36", "n37", "n38", "n4", "n40", "n41", "n42", "n43", "n44", "n45", "n46", "n47", "n48", "n49", "n5", "n51", "n52", "n54", "n55", "n57", "n58", "n59", "n6", "n60", "n61", "n62", "n63", "n64", "n65", "n66", "n67", "n68", "n69", "n7", "n70", "n71", "n72", "n73", "n74", "n75", "n76", "n77", "n79", "n80", "n81", "n83", "n84", "n85", "n86", "n87", "n88", "n89", "n9", "n90", "n91", "n94", "n95", "n97", "n98" }, 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 |-> { "n100", "n11", "n12", "n14", "n2", "n22", "n26", "n28", "n31", "n33", "n39", "n40", "n41", "n42", "n44", "n46", "n48", "n49", "n50", "n55", "n56", "n58", "n59", "n69", "n70", "n73", "n76", "n82", "n88", "n96", "n99" }, VS |-> { "n10", "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", "n36", "n37", "n38", "n4", "n40", "n41", "n42", "n43", "n44", "n45", "n46", "n47", "n48", "n49", "n5", "n51", "n52", "n54", "n55", "n57", "n58", "n59", "n6", "n60", "n61", "n62", "n63", "n64", "n65", "n66", "n67", "n68", "n69", "n7", "n70", "n71", "n72", "n73", "n74", "n75", "n76", "n77", "n79", "n80", "n81", "n83", "n84", "n85", "n86", "n87", "n88", "n89", "n9", "n90", "n91", "n94", "n95", "n97", "n98" }, height |-> 2, lastCommit |-> { "n1", "n10", "n100", "n11", "n12", "n13", "n14", "n15", "n16", "n18", "n19", "n2", "n21", "n22", "n23", "n24", "n25", "n26", "n28", "n29", "n3", "n30", "n31", "n32", "n33", "n35", "n36", "n37", "n4", "n40", "n41", "n43", "n44", "n45", "n46", "n47", "n48", "n49", "n5", "n50", "n51", "n53", "n55", "n56", "n57", "n58", "n6", "n61", "n62", "n63", "n65", "n67", "n69", "n7", "n70", "n71", "n72", "n73", "n75", "n77", "n79", "n8", "n80", "n81", "n82", "n83", "n84", "n87", "n88", "n89", "n9", "n91", "n92", "n93", "n95", "n97", "n98" }, 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 |-> { "n100", "n11", "n12", "n14", "n2", "n22", "n26", "n28", "n31", "n33", "n39", "n40", "n41", "n42", "n44", "n46", "n48", "n49", "n50", "n55", "n56", "n58", "n59", "n69", "n70", "n73", "n76", "n82", "n88", "n96", "n99" }, height |-> 3, lastCommit |-> { "n10", "n11", "n14", "n15", "n2", "n21", "n22", "n25", "n26", "n27", "n28", "n3", "n30", "n31", "n33", "n34", "n36", "n37", "n38", "n44", "n45", "n46", "n47", "n51", "n52", "n54", "n57", "n58", "n59", "n6", "n60", "n61", "n62", "n64", "n65", "n66", "n68", "n69", "n7", "n70", "n71", "n72", "n73", "n74", "n76", "n77", "n79", "n81", "n83", "n84", "n85", "n86", "n87", "n89", "n9", "n90", "n97", "n98" }, 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 |-> { "n10", "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", "n36", "n37", "n38", "n4", "n40", "n41", "n42", "n43", "n44", "n45", "n46", "n47", "n48", "n49", "n5", "n51", "n52", "n54", "n55", "n57", "n58", "n59", "n6", "n60", "n61", "n62", "n63", "n64", "n65", "n66", "n67", "n68", "n69", "n7", "n70", "n71", "n72", "n73", "n74", "n75", "n76", "n77", "n79", "n80", "n81", "n83", "n84", "n85", "n86", "n87", "n88", "n89", "n9", "n90", "n91", "n94", "n95", "n97", "n98" }, 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 |-> { "n10", "n11", "n12", "n13", "n15", "n16", "n17", "n18", "n19", "n2", "n20", "n21", "n23", "n24", "n26", "n27", "n28", "n29", "n3", "n30", "n31", "n32", "n33", "n34", "n36", "n37", "n38", "n4", "n40", "n42", "n43", "n44", "n46", "n47", "n48", "n49", "n5", "n51", "n52", "n54", "n55", "n57", "n58", "n59", "n6", "n60", "n62", "n63", "n64", "n65", "n66", "n67", "n68", "n69", "n7", "n70", "n71", "n72", "n75", "n76", "n77", "n79", "n80", "n81", "n83", "n85", "n86", "n87", "n88", "n89", "n9", "n91", "n94", "n95", "n97", "n98" }, header |-> [NextVS |-> { "n100", "n11", "n12", "n14", "n2", "n22", "n26", "n28", "n31", "n33", "n39", "n40", "n41", "n42", "n44", "n46", "n48", "n49", "n50", "n55", "n56", "n58", "n59", "n69", "n70", "n73", "n76", "n82", "n88", "n96", "n99" }, VS |-> { "n10", "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", "n36", "n37", "n38", "n4", "n40", "n41", "n42", "n43", "n44", "n45", "n46", "n47", "n48", "n49", "n5", "n51", "n52", "n54", "n55", "n57", "n58", "n59", "n6", "n60", "n61", "n62", "n63", "n64", "n65", "n66", "n67", "n68", "n69", "n7", "n70", "n71", "n72", "n73", "n74", "n75", "n76", "n77", "n79", "n80", "n81", "n83", "n84", "n85", "n86", "n87", "n88", "n89", "n9", "n90", "n91", "n94", "n95", "n97", "n98" }, height |-> 2, lastCommit |-> { "n1", "n10", "n100", "n11", "n12", "n13", "n14", "n15", "n16", "n18", "n19", "n2", "n21", "n22", "n23", "n24", "n25", "n26", "n28", "n29", "n3", "n30", "n31", "n32", "n33", "n35", "n36", "n37", "n4", "n40", "n41", "n43", "n44", "n45", "n46", "n47", "n48", "n49", "n5", "n50", "n51", "n53", "n55", "n56", "n57", "n58", "n6", "n61", "n62", "n63", "n65", "n67", "n69", "n7", "n70", "n71", "n72", "n73", "n75", "n77", "n79", "n8", "n80", "n81", "n82", "n83", "n84", "n87", "n88", "n89", "n9", "n91", "n92", "n93", "n95", "n97", "n98" }, 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 |-> { "n10", "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", "n36", "n37", "n38", "n4", "n40", "n41", "n42", "n43", "n44", "n45", "n46", "n47", "n48", "n49", "n5", "n51", "n52", "n54", "n55", "n57", "n58", "n59", "n6", "n60", "n61", "n62", "n63", "n64", "n65", "n66", "n67", "n68", "n69", "n7", "n70", "n71", "n72", "n73", "n74", "n75", "n76", "n77", "n79", "n80", "n81", "n83", "n84", "n85", "n86", "n87", "n88", "n89", "n9", "n90", "n91", "n94", "n95", "n97", "n98" }, 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 |-> 3, 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 |-> { "n10", "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", "n36", "n37", "n38", "n4", "n40", "n41", "n42", "n43", "n44", "n45", "n46", "n47", "n48", "n49", "n5", "n51", "n52", "n54", "n55", "n57", "n58", "n59", "n6", "n60", "n61", "n62", "n63", "n64", "n65", "n66", "n67", "n68", "n69", "n7", "n70", "n71", "n72", "n73", "n74", "n75", "n76", "n77", "n79", "n80", "n81", "n83", "n84", "n85", "n86", "n87", "n88", "n89", "n9", "n90", "n91", "n94", "n95", "n97", "n98" }, 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 |-> { "n10", "n11", "n12", "n13", "n15", "n16", "n17", "n18", "n19", "n2", "n20", "n21", "n23", "n24", "n26", "n27", "n28", "n29", "n3", "n30", "n31", "n32", "n33", "n34", "n36", "n37", "n38", "n4", "n40", "n42", "n43", "n44", "n46", "n47", "n48", "n49", "n5", "n51", "n52", "n54", "n55", "n57", "n58", "n59", "n6", "n60", "n62", "n63", "n64", "n65", "n66", "n67", "n68", "n69", "n7", "n70", "n71", "n72", "n75", "n76", "n77", "n79", "n80", "n81", "n83", "n85", "n86", "n87", "n88", "n89", "n9", "n91", "n94", "n95", "n97", "n98" }, header |-> [NextVS |-> { "n100", "n11", "n12", "n14", "n2", "n22", "n26", "n28", "n31", "n33", "n39", "n40", "n41", "n42", "n44", "n46", "n48", "n49", "n50", "n55", "n56", "n58", "n59", "n69", "n70", "n73", "n76", "n82", "n88", "n96", "n99" }, VS |-> { "n10", "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", "n36", "n37", "n38", "n4", "n40", "n41", "n42", "n43", "n44", "n45", "n46", "n47", "n48", "n49", "n5", "n51", "n52", "n54", "n55", "n57", "n58", "n59", "n6", "n60", "n61", "n62", "n63", "n64", "n65", "n66", "n67", "n68", "n69", "n7", "n70", "n71", "n72", "n73", "n74", "n75", "n76", "n77", "n79", "n80", "n81", "n83", "n84", "n85", "n86", "n87", "n88", "n89", "n9", "n90", "n91", "n94", "n95", "n97", "n98" }, height |-> 2, lastCommit |-> { "n1", "n10", "n100", "n11", "n12", "n13", "n14", "n15", "n16", "n18", "n19", "n2", "n21", "n22", "n23", "n24", "n25", "n26", "n28", "n29", "n3", "n30", "n31", "n32", "n33", "n35", "n36", "n37", "n4", "n40", "n41", "n43", "n44", "n45", "n46", "n47", "n48", "n49", "n5", "n50", "n51", "n53", "n55", "n56", "n57", "n58", "n6", "n61", "n62", "n63", "n65", "n67", "n69", "n7", "n70", "n71", "n72", "n73", "n75", "n77", "n79", "n8", "n80", "n81", "n82", "n83", "n84", "n87", "n88", "n89", "n9", "n91", "n92", "n93", "n95", "n97", "n98" }, time |-> 2]], now |-> 3, 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 |-> { "n10", "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", "n36", "n37", "n38", "n4", "n40", "n41", "n42", "n43", "n44", "n45", "n46", "n47", "n48", "n49", "n5", "n51", "n52", "n54", "n55", "n57", "n58", "n59", "n6", "n60", "n61", "n62", "n63", "n64", "n65", "n66", "n67", "n68", "n69", "n7", "n70", "n71", "n72", "n73", "n74", "n75", "n76", "n77", "n79", "n80", "n81", "n83", "n84", "n85", "n86", "n87", "n88", "n89", "n9", "n90", "n91", "n94", "n95", "n97", "n98" }, 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 |-> { "n10", "n11", "n12", "n13", "n15", "n16", "n17", "n18", "n19", "n2", "n20", "n21", "n23", "n24", "n26", "n27", "n28", "n29", "n3", "n30", "n31", "n32", "n33", "n34", "n36", "n37", "n38", "n4", "n40", "n42", "n43", "n44", "n46", "n47", "n48", "n49", "n5", "n51", "n52", "n54", "n55", "n57", "n58", "n59", "n6", "n60", "n62", "n63", "n64", "n65", "n66", "n67", "n68", "n69", "n7", "n70", "n71", "n72", "n75", "n76", "n77", "n79", "n80", "n81", "n83", "n85", "n86", "n87", "n88", "n89", "n9", "n91", "n94", "n95", "n97", "n98" }, header |-> [NextVS |-> { "n100", "n11", "n12", "n14", "n2", "n22", "n26", "n28", "n31", "n33", "n39", "n40", "n41", "n42", "n44", "n46", "n48", "n49", "n50", "n55", "n56", "n58", "n59", "n69", "n70", "n73", "n76", "n82", "n88", "n96", "n99" }, VS |-> { "n10", "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", "n36", "n37", "n38", "n4", "n40", "n41", "n42", "n43", "n44", "n45", "n46", "n47", "n48", "n49", "n5", "n51", "n52", "n54", "n55", "n57", "n58", "n59", "n6", "n60", "n61", "n62", "n63", "n64", "n65", "n66", "n67", "n68", "n69", "n7", "n70", "n71", "n72", "n73", "n74", "n75", "n76", "n77", "n79", "n80", "n81", "n83", "n84", "n85", "n86", "n87", "n88", "n89", "n9", "n90", "n91", "n94", "n95", "n97", "n98" }, height |-> 2, lastCommit |-> { "n1", "n10", "n100", "n11", "n12", "n13", "n14", "n15", "n16", "n18", "n19", "n2", "n21", "n22", "n23", "n24", "n25", "n26", "n28", "n29", "n3", "n30", "n31", "n32", "n33", "n35", "n36", "n37", "n4", "n40", "n41", "n43", "n44", "n45", "n46", "n47", "n48", "n49", "n5", "n50", "n51", "n53", "n55", "n56", "n57", "n58", "n6", "n61", "n62", "n63", "n65", "n67", "n69", "n7", "n70", "n71", "n72", "n73", "n75", "n77", "n79", "n8", "n80", "n81", "n82", "n83", "n84", "n87", "n88", "n89", "n9", "n91", "n92", "n93", "n95", "n97", "n98" }, time |-> 2]] /\ lightBlockStatus = 1 :> "StateVerified" @@ 2 :> "StateVerified" /\ nextHeight = 2 /\ now = 3 /\ nprobes = 1 /\ prevCurrent = [Commits |-> { "n10", "n11", "n12", "n13", "n15", "n16", "n17", "n18", "n19", "n2", "n20", "n21", "n23", "n24", "n26", "n27", "n28", "n29", "n3", "n30", "n31", "n32", "n33", "n34", "n36", "n37", "n38", "n4", "n40", "n42", "n43", "n44", "n46", "n47", "n48", "n49", "n5", "n51", "n52", "n54", "n55", "n57", "n58", "n59", "n6", "n60", "n62", "n63", "n64", "n65", "n66", "n67", "n68", "n69", "n7", "n70", "n71", "n72", "n75", "n76", "n77", "n79", "n80", "n81", "n83", "n85", "n86", "n87", "n88", "n89", "n9", "n91", "n94", "n95", "n97", "n98" }, header |-> [NextVS |-> { "n100", "n11", "n12", "n14", "n2", "n22", "n26", "n28", "n31", "n33", "n39", "n40", "n41", "n42", "n44", "n46", "n48", "n49", "n50", "n55", "n56", "n58", "n59", "n69", "n70", "n73", "n76", "n82", "n88", "n96", "n99" }, VS |-> { "n10", "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", "n36", "n37", "n38", "n4", "n40", "n41", "n42", "n43", "n44", "n45", "n46", "n47", "n48", "n49", "n5", "n51", "n52", "n54", "n55", "n57", "n58", "n59", "n6", "n60", "n61", "n62", "n63", "n64", "n65", "n66", "n67", "n68", "n69", "n7", "n70", "n71", "n72", "n73", "n74", "n75", "n76", "n77", "n79", "n80", "n81", "n83", "n84", "n85", "n86", "n87", "n88", "n89", "n9", "n90", "n91", "n94", "n95", "n97", "n98" }, height |-> 2, lastCommit |-> { "n1", "n10", "n100", "n11", "n12", "n13", "n14", "n15", "n16", "n18", "n19", "n2", "n21", "n22", "n23", "n24", "n25", "n26", "n28", "n29", "n3", "n30", "n31", "n32", "n33", "n35", "n36", "n37", "n4", "n40", "n41", "n43", "n44", "n45", "n46", "n47", "n48", "n49", "n5", "n50", "n51", "n53", "n55", "n56", "n57", "n58", "n6", "n61", "n62", "n63", "n65", "n67", "n69", "n7", "n70", "n71", "n72", "n73", "n75", "n77", "n79", "n8", "n80", "n81", "n82", "n83", "n84", "n87", "n88", "n89", "n9", "n91", "n92", "n93", "n95", "n97", "n98" }, time |-> 2]] /\ prevNow = 3 /\ 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 |-> { "n10", "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", "n36", "n37", "n38", "n4", "n40", "n41", "n42", "n43", "n44", "n45", "n46", "n47", "n48", "n49", "n5", "n51", "n52", "n54", "n55", "n57", "n58", "n59", "n6", "n60", "n61", "n62", "n63", "n64", "n65", "n66", "n67", "n68", "n69", "n7", "n70", "n71", "n72", "n73", "n74", "n75", "n76", "n77", "n79", "n80", "n81", "n83", "n84", "n85", "n86", "n87", "n88", "n89", "n9", "n90", "n91", "n94", "n95", "n97", "n98" }, 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 = "finishedSuccess" (* The following formula holds true in the last state and violates the invariant *) InvariantViolation == state = "finishedSuccess" /\ Cardinality((DOMAIN fetchedLightBlocks)) = 2 ================================================================================ \* Created by Apalache on Wed Nov 18 13:48:30 UTC 2020 \* https://github.com/informalsystems/apalache