From f009459ff693858f633fa8b00e16d8cb7d0723b1 Mon Sep 17 00:00:00 2001 From: Qian-Cheng-nju Date: Tue, 20 Oct 2026 17:09:23 +0000 Subject: [PATCH] Assert the leader domain in Sailfish Signed-off-by: Qian-Cheng-nju --- specifications/dag-consensus/Sailfish.tla | 3 +++ 1 file changed, 3 insertions(+) diff --git a/specifications/dag-consensus/Sailfish.tla b/specifications/dag-consensus/Sailfish.tla index d80499b6..d04d296c 100644 --- a/specifications/dag-consensus/Sailfish.tla +++ b/specifications/dag-consensus/Sailfish.tla @@ -52,6 +52,9 @@ ASSUME BlockingSetsIntersectQuorums == INSTANCE BlockDag \* Import definitions related to DAGs of blocks +\* INSTANCE imports the definition, but does not assert the assumption. +ASSUME LeadersAreNodes + (**************************************************************************************) (* Now we specify the algorithm in the PlusCal language. *) (**************************************************************************************)