------------------------- 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