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