From 46b67ad3f9b173ad5d6f55ae4ee7c61bc686ef0e Mon Sep 17 00:00:00 2001 From: Andrew Helwer Date: Tue, 16 Dec 2025 12:12:15 -0800 Subject: [PATCH] Remove tabs from VectorClocks.tla TLAPM does not like tabs Signed-off-by: Andrew Helwer --- modules/VectorClocks.tla | 34 +++++++++++++++++----------------- 1 file changed, 17 insertions(+), 17 deletions(-) diff --git a/modules/VectorClocks.tla b/modules/VectorClocks.tla index 76c299b..fbfb0c2 100644 --- a/modules/VectorClocks.tla +++ b/modules/VectorClocks.tla @@ -37,22 +37,22 @@ CausalOrder(log, clock(_), node(_), domain(_)) == Imagine a log containing lines such as: - [pkt |-> - [vc |-> - [1 |-> 20, - 0 |-> 10, - 3 |-> 16, - 7 |-> 21, - 4 |-> 10, - 6 |-> 21]], - node |-> 5, - ... - ] - - CausalOrder(log, - LAMBDA line: line.pkt.vc, - LAMBDA line: line.node, - LAMBDA vc : DOMAIN vc) + [pkt |-> + [vc |-> + [1 |-> 20, + 0 |-> 10, + 3 |-> 16, + 7 |-> 21, + 4 |-> 10, + 6 |-> 21]], + node |-> 5, + ... + ] + + CausalOrder(log, + LAMBDA line: line.pkt.vc, + LAMBDA line: line.node, + LAMBDA vc : DOMAIN vc) *) CHOOSE newlog \in { f \in @@ -60,4 +60,4 @@ CausalOrder(log, clock(_), node(_), domain(_)) == Range(f) = Range(log) } : IsCausalOrder(newlog, clock) -=============================================================================== \ No newline at end of file +===============================================================================