add syntax highlighting

spec/protocol-spec/experiments/n6f1b0.qnt

@@ -1,3 +1,4 @@
+// -*- mode: Bluespec; -*-
 // A specification instance for n=6, f=1, and no Byzantine faults
 module n6f1b0 {
   import replica(
@@ -11,4 +12,4 @@ module n6f1b0 {
     VALID_BLOCKS = Set("val_b0", "val_b1"),
     INVALID_BLOCKS = Set("inv_b3")
   ).* from "../replica"
-}
+}

spec/protocol-spec/experiments/n6f1b0_guided_no_proposing_leader.qnt

@@ -1,3 +1,4 @@
+// -*- mode: Bluespec; -*-
 // A specification instance for n=6, f=1, and 1 Byzantine fault
 //
 // Due to import/export limitations of Quint, use the definitions starting with g_:
@@ -38,4 +39,4 @@ module n6f1b1_two_blocks {
 
     ]
   ).* from "../guided_replica"
-}
+}

spec/protocol-spec/experiments/n6f1b1.qnt

@@ -1,3 +1,4 @@
+// -*- mode: Bluespec; -*-
 // A specification instance for n=6, f=1, and 1 Byzantine fault
 module n6f1b1 {
   import replica(
@@ -11,4 +12,4 @@ module n6f1b1 {
     VALID_BLOCKS = Set("val_b0", "val_b1"),
     INVALID_BLOCKS = Set("inv_b3")
   ).* from "../replica"
-}
+}

spec/protocol-spec/experiments/n6f1b1_guided_dead_lock.qnt

@@ -1,3 +1,5 @@
+// -*- mode: Bluespec; -*-
+//
 // A specification instance for n=6, f=1, and 1 Byzantine fault
 //
 /// Test a liveness issue where some validators have the HighQC but don't have the block payload and have to wait for it,
@@ -42,4 +44,4 @@ module n6f1b1_two_blocks {
             OnProposalStep("n1"), OnProposalStep("n2"), OnProposalStep("n3"), OnProposalStep("n4"), OnProposalStep("n5"),
         ]
     ).* from "../guided_replica"
-}
+}

spec/protocol-spec/experiments/n6f1b1_guided_two_blocks.qnt

@@ -1,3 +1,5 @@
+// -*- mode: Bluespec; -*-
+//
 // A specification instance for n=6, f=1, and 1 Byzantine fault
 //
 // Due to import/export limitations of Quint, use the definitions starting with g_:
@@ -29,4 +31,4 @@ module n6f1b1_two_blocks {
       OnCommitStep("n0"), OnCommitStep("n0"), OnCommitStep("n0"), OnCommitStep("n0"), OnCommitStep("n0"),
     ]
   ).* from "../guided_replica"
-}
+}

spec/protocol-spec/experiments/n6f1b2.qnt

@@ -1,3 +1,5 @@
+// -*- mode: Bluespec; -*-
+//
 // A specification instance for n=6, f=1, and 2 Byzantine faults
 module n6f1b2 {
   import replica(
@@ -11,4 +13,4 @@ module n6f1b2 {
     VALID_BLOCKS = Set("val_b0", "val_b1"),
     INVALID_BLOCKS = Set("inv_b3")
   ).* from "../replica"
-}
+}

spec/protocol-spec/experiments/n6f1b2_boxed.qnt

@@ -1,3 +1,5 @@
+// -*- mode: Bluespec; -*-
+//
 // A specification instance for n=6, f=1, and 2 Byzantine faults.
 // We box the number of different steps.
 module n6f1b2_boxed {
@@ -137,4 +139,4 @@ module n6f1b2_boxed {
       }
     }
   }
-}
+}

spec/protocol-spec/experiments/n6f1b2_guided_agreement.qnt

@@ -1,3 +1,5 @@
+// -*- mode: Bluespec; -*-
+//
 // A specification instance for n=6, f=1, and 2 Byzantine faults
 //
 // Due to import/export limitations of Quint, use the definitions starting with g_:
@@ -32,4 +34,4 @@ module n6f1b2_agreement {
       OnCommitStep("n3"), OnCommitStep("n3"), OnCommitStep("n3"), OnCommitStep("n3"), OnCommitStep("n3"),
     ]
   ).* from "../guided_replica"
-}
+}

spec/protocol-spec/experiments/n6f1b3.qnt

@@ -1,3 +1,5 @@
+// -*- mode: Bluespec; -*-
+//
 // A specification instance for n=6, f=1, and 3 Byzantine faults
 module n6f1b0 {
   import replica(
@@ -11,4 +13,4 @@ module n6f1b0 {
     VALID_BLOCKS = Set("val_b0", "val_b1"),
     INVALID_BLOCKS = Set("inv_b3")
   ).* from "../replica"
-}
+}

spec/protocol-spec/experiments/n7f1b0.qnt

@@ -1,3 +1,5 @@
+// -*- mode: Bluespec; -*-
+//
 // A specification instance for n=6, f=1, and no Byzantine faults
 module n7f1b0 {
   import replica(

spec/protocol-spec/experiments/n7f1b0_quided_three_blocks.qnt

@@ -1,3 +1,5 @@
+// -*- mode: Bluespec; -*-
+//
 // A specification instance for n=7, f=1, and 0 byzantine nodes.
 //
 // Due to import/export limitations of Quint, use the definitions starting with g_:
@@ -63,4 +65,4 @@ module n6f1b1_two_blocks {
             OnCommitStep("n0"), OnCommitStep("n0"), OnCommitStep("n0"), OnCommitStep("n0"), OnCommitStep("n0"), OnCommitStep("n0"), 
         ]
     ).* from "../guided_replica"
-}
+}

spec/protocol-spec/experiments/n7f1b1.qnt

@@ -1,3 +1,5 @@
+// -*- mode: Bluespec; -*-
+//
 // A specification instance for n=6, f=1, and no Byzantine faults
 module n7f1b1 {
   import replica(

spec/protocol-spec/guided_replica.qnt

@@ -1,3 +1,4 @@
+// -*- mode: Bluespec; -*-
 // A restriction of replica.qnt to guide the model checker's search
 module guided_replica {
     import types.* from "./types"
@@ -139,4 +140,4 @@ module guided_replica {
             }
         }
     }
-}
+}

spec/protocol-spec/main.qnt

@@ -1,3 +1,4 @@
+// -*- mode: Bluespec; -*-
 /// A few handy small models that are good for debugging and inspection
 module main {
     // A specification instance for n=6, f=1, and 1 Byzantine fault
@@ -12,4 +13,4 @@ module main {
         VALID_BLOCKS = Set("val_b0", "val_b1"),
         INVALID_BLOCKS = Set("inv_b3")
   ) .* from "./replica"
-}
+}

spec/protocol-spec/state_monitor.qnt

@@ -1,3 +1,4 @@
+// -*- mode: Bluespec; -*-
 // A state monitor that allows us to compare new state against the old states.
 // For example, we compare phase transitions.
 // To do so, we save the old replica states in old_replica_state.
@@ -55,4 +56,4 @@ module state_monitor {
 
       i::CORRECT.forall(id => for_replica(id))
     }
-}
+}

spec/protocol-spec/twins_n6f1b1.qnt

@@ -1,3 +1,4 @@
+// -*- mode: Bluespec; -*-
 // This is an explorative module applying the Twins approach 
 // to model byzantine behaviour with 1 faulty replicas and 5 correct replicas.
 module twins {
@@ -31,4 +32,4 @@ module twins {
 
 
   action step = i::correct_step
-}
+}

spec/protocol-spec/twins_n6f1b2.qnt

@@ -1,3 +1,4 @@
+// -*- mode: Bluespec; -*-
 // This is an explorative module applying the Twins approach 
 // to model byzantine behaviour with 2 faulty replicas and 4 correct replicas.
 module twins {
@@ -31,4 +32,4 @@ module twins {
 
 
   action step = i::correct_step
-}
+}