------------------------- MODULE counterexample ------------------------- EXTENDS MC50_2_faulty (* Initial state *) State1 == TRUE (* Transition 0 to State2 *) State2 == /\ Faulty = { "n11", "n16", "n20", "n21", "n25", "n26", "n27", "n3", "n33", "n36", "n38", "n39", "n4", "n46", "n50" } /\ blockchain = 1 :> [NextVS |-> { "n1", "n10", "n11", "n13", "n15", "n16", "n17", "n2", "n20", "n21", "n22", "n23", "n24", "n27", "n28", "n29", "n3", "n32", "n33", "n36", "n37", "n38", "n4", "n42", "n43", "n45", "n47", "n48", "n49", "n5", "n50", "n7", "n8", "n9" }, VS |-> { "n1", "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", "n35", "n36", "n37", "n38", "n39", "n4", "n40", "n41", "n42", "n43", "n44", "n45", "n46", "n47", "n48", "n49", "n5", "n50", "n6", "n7", "n8", "n9" }, height |-> 1, lastCommit |-> {}, time |-> 1] @@ 2 :> [NextVS |-> { "n1", "n13", "n17", "n2", "n22", "n23", "n24", "n26", "n28", "n29", "n30", "n35", "n36", "n41", "n43", "n45", "n48", "n50", "n6", "n7", "n9" }, VS |-> { "n1", "n10", "n11", "n13", "n15", "n16", "n17", "n2", "n20", "n21", "n22", "n23", "n24", "n27", "n28", "n29", "n3", "n32", "n33", "n36", "n37", "n38", "n4", "n42", "n43", "n45", "n47", "n48", "n49", "n5", "n50", "n7", "n8", "n9" }, height |-> 2, lastCommit |-> { "n1", "n10", "n11", "n13", "n14", "n15", "n16", "n17", "n18", "n19", "n20", "n21", "n22", "n23", "n24", "n25", "n26", "n27", "n28", "n29", "n3", "n30", "n31", "n32", "n33", "n34", "n35", "n36", "n37", "n39", "n4", "n40", "n41", "n42", "n43", "n44", "n46", "n47", "n49", "n5", "n50", "n6", "n7", "n8", "n9" }, time |-> 2] @@ 3 :> [NextVS |-> { "n1", "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", "n35", "n36", "n37", "n38", "n39", "n4", "n40", "n41", "n42", "n43", "n44", "n45", "n46", "n47", "n48", "n49", "n5", "n50", "n6", "n7", "n8", "n9" }, VS |-> { "n1", "n13", "n17", "n2", "n22", "n23", "n24", "n26", "n28", "n29", "n30", "n35", "n36", "n41", "n43", "n45", "n48", "n50", "n6", "n7", "n9" }, height |-> 3, lastCommit |-> { "n1", "n10", "n11", "n15", "n17", "n2", "n20", "n21", "n22", "n24", "n27", "n28", "n3", "n33", "n36", "n38", "n42", "n45", "n48", "n49", "n50", "n7", "n9" }, time |-> 3] /\ fetchedLightBlocks = 1 :> [Commits |-> { "n1", "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", "n35", "n36", "n37", "n38", "n39", "n4", "n40", "n41", "n42", "n43", "n44", "n45", "n46", "n47", "n48", "n49", "n5", "n50", "n6", "n7", "n8", "n9" }, header |-> [NextVS |-> { "n1", "n10", "n11", "n13", "n15", "n16", "n17", "n2", "n20", "n21", "n22", "n23", "n24", "n27", "n28", "n29", "n3", "n32", "n33", "n36", "n37", "n38", "n4", "n42", "n43", "n45", "n47", "n48", "n49", "n5", "n50", "n7", "n8", "n9" }, VS |-> { "n1", "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", "n35", "n36", "n37", "n38", "n39", "n4", "n40", "n41", "n42", "n43", "n44", "n45", "n46", "n47", "n48", "n49", "n5", "n50", "n6", "n7", "n8", "n9" }, height |-> 1, lastCommit |-> {}, time |-> 1]] /\ history = 0 :> [current |-> [Commits |-> { "n1", "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", "n35", "n36", "n37", "n38", "n39", "n4", "n40", "n41", "n42", "n43", "n44", "n45", "n46", "n47", "n48", "n49", "n5", "n50", "n6", "n7", "n8", "n9" }, header |-> [NextVS |-> { "n1", "n10", "n11", "n13", "n15", "n16", "n17", "n2", "n20", "n21", "n22", "n23", "n24", "n27", "n28", "n29", "n3", "n32", "n33", "n36", "n37", "n38", "n4", "n42", "n43", "n45", "n47", "n48", "n49", "n5", "n50", "n7", "n8", "n9" }, VS |-> { "n1", "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", "n35", "n36", "n37", "n38", "n39", "n4", "n40", "n41", "n42", "n43", "n44", "n45", "n46", "n47", "n48", "n49", "n5", "n50", "n6", "n7", "n8", "n9" }, height |-> 1, lastCommit |-> {}, time |-> 1]], now |-> 3, verdict |-> "SUCCESS", verified |-> [Commits |-> { "n1", "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", "n35", "n36", "n37", "n38", "n39", "n4", "n40", "n41", "n42", "n43", "n44", "n45", "n46", "n47", "n48", "n49", "n5", "n50", "n6", "n7", "n8", "n9" }, header |-> [NextVS |-> { "n1", "n10", "n11", "n13", "n15", "n16", "n17", "n2", "n20", "n21", "n22", "n23", "n24", "n27", "n28", "n29", "n3", "n32", "n33", "n36", "n37", "n38", "n4", "n42", "n43", "n45", "n47", "n48", "n49", "n5", "n50", "n7", "n8", "n9" }, VS |-> { "n1", "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", "n35", "n36", "n37", "n38", "n39", "n4", "n40", "n41", "n42", "n43", "n44", "n45", "n46", "n47", "n48", "n49", "n5", "n50", "n6", "n7", "n8", "n9" }, height |-> 1, lastCommit |-> {}, time |-> 1]]] /\ latestVerified = [Commits |-> { "n1", "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", "n35", "n36", "n37", "n38", "n39", "n4", "n40", "n41", "n42", "n43", "n44", "n45", "n46", "n47", "n48", "n49", "n5", "n50", "n6", "n7", "n8", "n9" }, header |-> [NextVS |-> { "n1", "n10", "n11", "n13", "n15", "n16", "n17", "n2", "n20", "n21", "n22", "n23", "n24", "n27", "n28", "n29", "n3", "n32", "n33", "n36", "n37", "n38", "n4", "n42", "n43", "n45", "n47", "n48", "n49", "n5", "n50", "n7", "n8", "n9" }, VS |-> { "n1", "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", "n35", "n36", "n37", "n38", "n39", "n4", "n40", "n41", "n42", "n43", "n44", "n45", "n46", "n47", "n48", "n49", "n5", "n50", "n6", "n7", "n8", "n9" }, height |-> 1, lastCommit |-> {}, time |-> 1]] /\ lightBlockStatus = 1 :> "StateVerified" /\ nextHeight = 2 /\ now = 3 /\ nprobes = 0 /\ prevCurrent = [Commits |-> { "n1", "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", "n35", "n36", "n37", "n38", "n39", "n4", "n40", "n41", "n42", "n43", "n44", "n45", "n46", "n47", "n48", "n49", "n5", "n50", "n6", "n7", "n8", "n9" }, header |-> [NextVS |-> { "n1", "n10", "n11", "n13", "n15", "n16", "n17", "n2", "n20", "n21", "n22", "n23", "n24", "n27", "n28", "n29", "n3", "n32", "n33", "n36", "n37", "n38", "n4", "n42", "n43", "n45", "n47", "n48", "n49", "n5", "n50", "n7", "n8", "n9" }, VS |-> { "n1", "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", "n35", "n36", "n37", "n38", "n39", "n4", "n40", "n41", "n42", "n43", "n44", "n45", "n46", "n47", "n48", "n49", "n5", "n50", "n6", "n7", "n8", "n9" }, height |-> 1, lastCommit |-> {}, time |-> 1]] /\ prevNow = 3 /\ prevVerdict = "SUCCESS" /\ prevVerified = [Commits |-> { "n1", "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", "n35", "n36", "n37", "n38", "n39", "n4", "n40", "n41", "n42", "n43", "n44", "n45", "n46", "n47", "n48", "n49", "n5", "n50", "n6", "n7", "n8", "n9" }, header |-> [NextVS |-> { "n1", "n10", "n11", "n13", "n15", "n16", "n17", "n2", "n20", "n21", "n22", "n23", "n24", "n27", "n28", "n29", "n3", "n32", "n33", "n36", "n37", "n38", "n4", "n42", "n43", "n45", "n47", "n48", "n49", "n5", "n50", "n7", "n8", "n9" }, VS |-> { "n1", "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", "n35", "n36", "n37", "n38", "n39", "n4", "n40", "n41", "n42", "n43", "n44", "n45", "n46", "n47", "n48", "n49", "n5", "n50", "n6", "n7", "n8", "n9" }, height |-> 1, lastCommit |-> {}, time |-> 1]] /\ state = "working" (* Transition 3 to State3 *) State3 == /\ Faulty = { "n11", "n16", "n20", "n21", "n25", "n26", "n27", "n3", "n33", "n36", "n38", "n39", "n4", "n46", "n50" } /\ blockchain = 1 :> [NextVS |-> { "n1", "n10", "n11", "n13", "n15", "n16", "n17", "n2", "n20", "n21", "n22", "n23", "n24", "n27", "n28", "n29", "n3", "n32", "n33", "n36", "n37", "n38", "n4", "n42", "n43", "n45", "n47", "n48", "n49", "n5", "n50", "n7", "n8", "n9" }, VS |-> { "n1", "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", "n35", "n36", "n37", "n38", "n39", "n4", "n40", "n41", "n42", "n43", "n44", "n45", "n46", "n47", "n48", "n49", "n5", "n50", "n6", "n7", "n8", "n9" }, height |-> 1, lastCommit |-> {}, time |-> 1] @@ 2 :> [NextVS |-> { "n1", "n13", "n17", "n2", "n22", "n23", "n24", "n26", "n28", "n29", "n30", "n35", "n36", "n41", "n43", "n45", "n48", "n50", "n6", "n7", "n9" }, VS |-> { "n1", "n10", "n11", "n13", "n15", "n16", "n17", "n2", "n20", "n21", "n22", "n23", "n24", "n27", "n28", "n29", "n3", "n32", "n33", "n36", "n37", "n38", "n4", "n42", "n43", "n45", "n47", "n48", "n49", "n5", "n50", "n7", "n8", "n9" }, height |-> 2, lastCommit |-> { "n1", "n10", "n11", "n13", "n14", "n15", "n16", "n17", "n18", "n19", "n20", "n21", "n22", "n23", "n24", "n25", "n26", "n27", "n28", "n29", "n3", "n30", "n31", "n32", "n33", "n34", "n35", "n36", "n37", "n39", "n4", "n40", "n41", "n42", "n43", "n44", "n46", "n47", "n49", "n5", "n50", "n6", "n7", "n8", "n9" }, time |-> 2] @@ 3 :> [NextVS |-> { "n1", "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", "n35", "n36", "n37", "n38", "n39", "n4", "n40", "n41", "n42", "n43", "n44", "n45", "n46", "n47", "n48", "n49", "n5", "n50", "n6", "n7", "n8", "n9" }, VS |-> { "n1", "n13", "n17", "n2", "n22", "n23", "n24", "n26", "n28", "n29", "n30", "n35", "n36", "n41", "n43", "n45", "n48", "n50", "n6", "n7", "n9" }, height |-> 3, lastCommit |-> { "n1", "n10", "n11", "n15", "n17", "n2", "n20", "n21", "n22", "n24", "n27", "n28", "n3", "n33", "n36", "n38", "n42", "n45", "n48", "n49", "n50", "n7", "n9" }, time |-> 3] /\ fetchedLightBlocks = 1 :> [Commits |-> { "n1", "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", "n35", "n36", "n37", "n38", "n39", "n4", "n40", "n41", "n42", "n43", "n44", "n45", "n46", "n47", "n48", "n49", "n5", "n50", "n6", "n7", "n8", "n9" }, header |-> [NextVS |-> { "n1", "n10", "n11", "n13", "n15", "n16", "n17", "n2", "n20", "n21", "n22", "n23", "n24", "n27", "n28", "n29", "n3", "n32", "n33", "n36", "n37", "n38", "n4", "n42", "n43", "n45", "n47", "n48", "n49", "n5", "n50", "n7", "n8", "n9" }, VS |-> { "n1", "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", "n35", "n36", "n37", "n38", "n39", "n4", "n40", "n41", "n42", "n43", "n44", "n45", "n46", "n47", "n48", "n49", "n5", "n50", "n6", "n7", "n8", "n9" }, height |-> 1, lastCommit |-> {}, time |-> 1]] @@ 2 :> [Commits |-> { "n1", "n10", "n11", "n13", "n15", "n17", "n2", "n20", "n21", "n22", "n24", "n27", "n28", "n3", "n38", "n4", "n42", "n43", "n47", "n48", "n49", "n5", "n50", "n7", "n9" }, header |-> [NextVS |-> { "n1", "n13", "n17", "n2", "n22", "n23", "n24", "n26", "n28", "n29", "n30", "n35", "n36", "n41", "n43", "n45", "n48", "n50", "n6", "n7", "n9" }, VS |-> { "n1", "n10", "n11", "n13", "n15", "n16", "n17", "n2", "n20", "n21", "n22", "n23", "n24", "n27", "n28", "n29", "n3", "n32", "n33", "n36", "n37", "n38", "n4", "n42", "n43", "n45", "n47", "n48", "n49", "n5", "n50", "n7", "n8", "n9" }, height |-> 2, lastCommit |-> { "n1", "n10", "n11", "n13", "n14", "n15", "n16", "n17", "n18", "n19", "n20", "n21", "n22", "n23", "n24", "n25", "n26", "n27", "n28", "n29", "n3", "n30", "n31", "n32", "n33", "n34", "n35", "n36", "n37", "n39", "n4", "n40", "n41", "n42", "n43", "n44", "n46", "n47", "n49", "n5", "n50", "n6", "n7", "n8", "n9" }, time |-> 2]] /\ history = 0 :> [current |-> [Commits |-> { "n1", "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", "n35", "n36", "n37", "n38", "n39", "n4", "n40", "n41", "n42", "n43", "n44", "n45", "n46", "n47", "n48", "n49", "n5", "n50", "n6", "n7", "n8", "n9" }, header |-> [NextVS |-> { "n1", "n10", "n11", "n13", "n15", "n16", "n17", "n2", "n20", "n21", "n22", "n23", "n24", "n27", "n28", "n29", "n3", "n32", "n33", "n36", "n37", "n38", "n4", "n42", "n43", "n45", "n47", "n48", "n49", "n5", "n50", "n7", "n8", "n9" }, VS |-> { "n1", "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", "n35", "n36", "n37", "n38", "n39", "n4", "n40", "n41", "n42", "n43", "n44", "n45", "n46", "n47", "n48", "n49", "n5", "n50", "n6", "n7", "n8", "n9" }, height |-> 1, lastCommit |-> {}, time |-> 1]], now |-> 3, verdict |-> "SUCCESS", verified |-> [Commits |-> { "n1", "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", "n35", "n36", "n37", "n38", "n39", "n4", "n40", "n41", "n42", "n43", "n44", "n45", "n46", "n47", "n48", "n49", "n5", "n50", "n6", "n7", "n8", "n9" }, header |-> [NextVS |-> { "n1", "n10", "n11", "n13", "n15", "n16", "n17", "n2", "n20", "n21", "n22", "n23", "n24", "n27", "n28", "n29", "n3", "n32", "n33", "n36", "n37", "n38", "n4", "n42", "n43", "n45", "n47", "n48", "n49", "n5", "n50", "n7", "n8", "n9" }, VS |-> { "n1", "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", "n35", "n36", "n37", "n38", "n39", "n4", "n40", "n41", "n42", "n43", "n44", "n45", "n46", "n47", "n48", "n49", "n5", "n50", "n6", "n7", "n8", "n9" }, height |-> 1, lastCommit |-> {}, time |-> 1]]] @@ 1 :> [current |-> [Commits |-> { "n1", "n10", "n11", "n13", "n15", "n17", "n2", "n20", "n21", "n22", "n24", "n27", "n28", "n3", "n38", "n4", "n42", "n43", "n47", "n48", "n49", "n5", "n50", "n7", "n9" }, header |-> [NextVS |-> { "n1", "n13", "n17", "n2", "n22", "n23", "n24", "n26", "n28", "n29", "n30", "n35", "n36", "n41", "n43", "n45", "n48", "n50", "n6", "n7", "n9" }, VS |-> { "n1", "n10", "n11", "n13", "n15", "n16", "n17", "n2", "n20", "n21", "n22", "n23", "n24", "n27", "n28", "n29", "n3", "n32", "n33", "n36", "n37", "n38", "n4", "n42", "n43", "n45", "n47", "n48", "n49", "n5", "n50", "n7", "n8", "n9" }, height |-> 2, lastCommit |-> { "n1", "n10", "n11", "n13", "n14", "n15", "n16", "n17", "n18", "n19", "n20", "n21", "n22", "n23", "n24", "n25", "n26", "n27", "n28", "n29", "n3", "n30", "n31", "n32", "n33", "n34", "n35", "n36", "n37", "n39", "n4", "n40", "n41", "n42", "n43", "n44", "n46", "n47", "n49", "n5", "n50", "n6", "n7", "n8", "n9" }, time |-> 2]], now |-> 3, verdict |-> "SUCCESS", verified |-> [Commits |-> { "n1", "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", "n35", "n36", "n37", "n38", "n39", "n4", "n40", "n41", "n42", "n43", "n44", "n45", "n46", "n47", "n48", "n49", "n5", "n50", "n6", "n7", "n8", "n9" }, header |-> [NextVS |-> { "n1", "n10", "n11", "n13", "n15", "n16", "n17", "n2", "n20", "n21", "n22", "n23", "n24", "n27", "n28", "n29", "n3", "n32", "n33", "n36", "n37", "n38", "n4", "n42", "n43", "n45", "n47", "n48", "n49", "n5", "n50", "n7", "n8", "n9" }, VS |-> { "n1", "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", "n35", "n36", "n37", "n38", "n39", "n4", "n40", "n41", "n42", "n43", "n44", "n45", "n46", "n47", "n48", "n49", "n5", "n50", "n6", "n7", "n8", "n9" }, height |-> 1, lastCommit |-> {}, time |-> 1]]] /\ latestVerified = [Commits |-> { "n1", "n10", "n11", "n13", "n15", "n17", "n2", "n20", "n21", "n22", "n24", "n27", "n28", "n3", "n38", "n4", "n42", "n43", "n47", "n48", "n49", "n5", "n50", "n7", "n9" }, header |-> [NextVS |-> { "n1", "n13", "n17", "n2", "n22", "n23", "n24", "n26", "n28", "n29", "n30", "n35", "n36", "n41", "n43", "n45", "n48", "n50", "n6", "n7", "n9" }, VS |-> { "n1", "n10", "n11", "n13", "n15", "n16", "n17", "n2", "n20", "n21", "n22", "n23", "n24", "n27", "n28", "n29", "n3", "n32", "n33", "n36", "n37", "n38", "n4", "n42", "n43", "n45", "n47", "n48", "n49", "n5", "n50", "n7", "n8", "n9" }, height |-> 2, lastCommit |-> { "n1", "n10", "n11", "n13", "n14", "n15", "n16", "n17", "n18", "n19", "n20", "n21", "n22", "n23", "n24", "n25", "n26", "n27", "n28", "n29", "n3", "n30", "n31", "n32", "n33", "n34", "n35", "n36", "n37", "n39", "n4", "n40", "n41", "n42", "n43", "n44", "n46", "n47", "n49", "n5", "n50", "n6", "n7", "n8", "n9" }, time |-> 2]] /\ lightBlockStatus = 1 :> "StateVerified" @@ 2 :> "StateVerified" /\ nextHeight = 2 /\ now = 3 /\ nprobes = 1 /\ prevCurrent = [Commits |-> { "n1", "n10", "n11", "n13", "n15", "n17", "n2", "n20", "n21", "n22", "n24", "n27", "n28", "n3", "n38", "n4", "n42", "n43", "n47", "n48", "n49", "n5", "n50", "n7", "n9" }, header |-> [NextVS |-> { "n1", "n13", "n17", "n2", "n22", "n23", "n24", "n26", "n28", "n29", "n30", "n35", "n36", "n41", "n43", "n45", "n48", "n50", "n6", "n7", "n9" }, VS |-> { "n1", "n10", "n11", "n13", "n15", "n16", "n17", "n2", "n20", "n21", "n22", "n23", "n24", "n27", "n28", "n29", "n3", "n32", "n33", "n36", "n37", "n38", "n4", "n42", "n43", "n45", "n47", "n48", "n49", "n5", "n50", "n7", "n8", "n9" }, height |-> 2, lastCommit |-> { "n1", "n10", "n11", "n13", "n14", "n15", "n16", "n17", "n18", "n19", "n20", "n21", "n22", "n23", "n24", "n25", "n26", "n27", "n28", "n29", "n3", "n30", "n31", "n32", "n33", "n34", "n35", "n36", "n37", "n39", "n4", "n40", "n41", "n42", "n43", "n44", "n46", "n47", "n49", "n5", "n50", "n6", "n7", "n8", "n9" }, time |-> 2]] /\ prevNow = 3 /\ prevVerdict = "SUCCESS" /\ prevVerified = [Commits |-> { "n1", "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", "n35", "n36", "n37", "n38", "n39", "n4", "n40", "n41", "n42", "n43", "n44", "n45", "n46", "n47", "n48", "n49", "n5", "n50", "n6", "n7", "n8", "n9" }, header |-> [NextVS |-> { "n1", "n10", "n11", "n13", "n15", "n16", "n17", "n2", "n20", "n21", "n22", "n23", "n24", "n27", "n28", "n29", "n3", "n32", "n33", "n36", "n37", "n38", "n4", "n42", "n43", "n45", "n47", "n48", "n49", "n5", "n50", "n7", "n8", "n9" }, VS |-> { "n1", "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", "n35", "n36", "n37", "n38", "n39", "n4", "n40", "n41", "n42", "n43", "n44", "n45", "n46", "n47", "n48", "n49", "n5", "n50", "n6", "n7", "n8", "n9" }, 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:42:20 UTC 2020 \* https://github.com/informalsystems/apalache