From dd9f9000e13c8006d290c7b1c96902a6233fd663 Mon Sep 17 00:00:00 2001 From: Heidi Howard <1835251+heidihoward@users.noreply.github.com> Date: Mon, 25 Nov 2024 16:15:17 +0000 Subject: [PATCH 1/9] qc -> byzqc --- pirateship.tla | 16 ++++++++-------- 1 file changed, 8 insertions(+), 8 deletions(-) diff --git a/pirateship.tla b/pirateship.tla index aeb6fcc..f948263 100644 --- a/pirateship.tla +++ b/pirateship.tla @@ -90,7 +90,7 @@ LogEntry == [ view: Views, tx: Txs, \* For convenience, we represent a quorum certificate as a set but it can only be empty or a singleton - qc: SUBSET QCs] + byzQC: SUBSET QCs] \* A log is a sequence of log entries. The index of the log entry is its sequence number/height \* We do not explicitly model the parent relationship, the parent of log entry i is log entry i-1 @@ -156,18 +156,18 @@ Init == \* Actions IsQC(e) == - e.qc # {} + e.byzQC # {} \* Given a log l, returns the index of the highest log entry with a quorum certificate, 0 if the log contains no QCs HighestQC(l) == LET idx == SelectLastInSeq(l, IsQC) - IN IF idx = 0 THEN 0 ELSE Max(l[idx].qc) + IN IF idx = 0 THEN 0 ELSE Max(l[idx].byzQC) \* Given a log l, returns the index of the highest log entry with a quorum certificate over a quorum certificate HighestQCOverQC(l) == LET lidx == HighestQC(l) idx == SelectLastInSubSeq(l, 1, lidx, IsQC) - IN IF idx = 0 THEN 0 ELSE Max(l[idx].qc) + IN IF idx = 0 THEN 0 ELSE Max(l[idx].byzQC) Max2(a,b) == IF a > b THEN a ELSE b Min2(a,b) == IF a < b THEN a ELSE b @@ -282,7 +282,7 @@ SendEntries(p) == /\ log' = [log EXCEPT ![p] = Append(@, [ view |-> view[p], tx |-> tx, - qc |-> MaxQC(log[p], matchIndex'[p])])] + byzQC |-> MaxQC(log[p], matchIndex'[p])])] /\ network' = [r \in R |-> [s \in R |-> IF s # p \/ r=p THEN network[r][s] ELSE Append(network[r][s], [ @@ -308,7 +308,7 @@ Timeout(r) == /\ matchIndex' = [matchIndex EXCEPT ![r] = [s \in R |-> 0]] /\ UNCHANGED <> -\* The view of the highest qc in log l, -1 if log contains no qcs +\* The view of the highest byzQC in log l, -1 if log contains no qcs HighestQCView(l) == LET idx == HighestQC(l) IN IF idx = 0 THEN -1 ELSE l[idx].view @@ -522,12 +522,12 @@ WellFormedLogInv == WellFormedQCsInv == \A r \in CR : \A i \in DOMAIN log[r] : - \A q \in log[r][i].qc : + \A q \in log[r][i].byzQC : \* qcs are always for previous entries /\ q < i \* qcs are always formed in the current view /\ log[r][q].view = log[r][i].view \* qcs are in increasing order /\ \A j \in 1..i-1 : - \A qj \in log[r][j].qc: qj < q + \A qj \in log[r][j].byzQC: qj < q ==== \ No newline at end of file From f4603c31875a256dbe3ef369fa5a015df2badac3 Mon Sep 17 00:00:00 2001 From: Heidi Howard <1835251+heidihoward@users.noreply.github.com> Date: Tue, 26 Nov 2024 10:18:32 +0000 Subject: [PATCH 2/9] moving commit index into blocks --- pirateship.tla | 29 ++++++++++++++++------------- 1 file changed, 16 insertions(+), 13 deletions(-) diff --git a/pirateship.tla b/pirateship.tla index f948263..f9fddde 100644 --- a/pirateship.tla +++ b/pirateship.tla @@ -83,14 +83,15 @@ Primary(v) == \* Quorum certificates are simply the index of the log entry they confirm \* Quorum certificates do not need views as they are always formed in the current view \* Note that in the specification, we do not model signatures anywhere. This means that signatures are omitted from the logs and messages. When modelling byzantine faults, byz replicas will not be permitted to form messages which would be discarded by honest replicas. -QCs == Nat +QC == Nat \* Each log entry contains just a view, a txn and optionally, a quorum certificate LogEntry == [ view: Views, tx: Txs, \* For convenience, we represent a quorum certificate as a set but it can only be empty or a singleton - byzQC: SUBSET QCs] + byzQC: SUBSET QC, + crashQC: QC] \* A log is a sequence of log entries. The index of the log entry is its sequence number/height \* We do not explicitly model the parent relationship, the parent of log entry i is log entry i-1 @@ -100,8 +101,7 @@ AppendEntries == [ type: {"AppendEntries"}, view: Views, \* In practice, it suffices to send only the log entry to append, however, for the sake of the spec, we send the entire log as we need to check that the replica has the parent of the log entry to append - log: Log, - commitIndex: Nat] + log: Log] Votes == [ type: {"Vote"}, @@ -158,14 +158,18 @@ Init == IsQC(e) == e.byzQC # {} +\* Given a log l, returns the index of the highest log entry with a crash QC, 0 if the log contains no entries +HighestCrashQC(l) == + IF l = <<>> THEN 0 ELSE Last(l).crashQC + \* Given a log l, returns the index of the highest log entry with a quorum certificate, 0 if the log contains no QCs -HighestQC(l) == +HighestByzQC(l) == LET idx == SelectLastInSeq(l, IsQC) IN IF idx = 0 THEN 0 ELSE Max(l[idx].byzQC) \* Given a log l, returns the index of the highest log entry with a quorum certificate over a quorum certificate HighestQCOverQC(l) == - LET lidx == HighestQC(l) + LET lidx == HighestByzQC(l) idx == SelectLastInSubSeq(l, 1, lidx, IsQC) IN IF idx = 0 THEN 0 ELSE Max(l[idx].byzQC) @@ -205,7 +209,7 @@ ReceiveEntries(r, p) == ] \* replica updates its crash commit index provided the new commit index is greater than the current one \* the only time a crash commit index can decrease is on the receipt of a NewLeader message if there's been a byz attack - /\ crashCommitIndex' = [crashCommitIndex EXCEPT ![r] = Max2(@, Head(network[r][p]).commitIndex)] + /\ crashCommitIndex' = [crashCommitIndex EXCEPT ![r] = Max2(@, HighestCrashQC(log'[r]))] \* assumes that a replica can safely byz commit if there's a quorum certificate over a quorum certificate /\ byzCommitIndex' = [byzCommitIndex EXCEPT ![r] = Max2(@, HighestQCOverQC(log'[r]))] /\ UNCHANGED <> @@ -266,7 +270,7 @@ ReceiveVote(p, r) == /\ UNCHANGED <> MaxQC(l, m) == - IF MaxQuorum(l, m, 0) > HighestQC(l) + IF MaxQuorum(l, m, 0) > HighestByzQC(l) THEN {MaxQuorum(l, m, 0)} ELSE {} @@ -282,14 +286,14 @@ SendEntries(p) == /\ log' = [log EXCEPT ![p] = Append(@, [ view |-> view[p], tx |-> tx, + crashQC |-> crashCommitIndex[p], byzQC |-> MaxQC(log[p], matchIndex'[p])])] /\ network' = [r \in R |-> [s \in R |-> IF s # p \/ r=p THEN network[r][s] ELSE Append(network[r][s], [ type |-> "AppendEntries", view |-> view[p], - log |-> log'[p], - commitIndex |-> crashCommitIndex[p]])]] + log |-> log'[p]])]] /\ UNCHANGED <> \* Replica r times out @@ -310,7 +314,7 @@ Timeout(r) == \* The view of the highest byzQC in log l, -1 if log contains no qcs HighestQCView(l) == - LET idx == HighestQC(l) IN + LET idx == HighestByzQC(l) IN IF idx = 0 THEN -1 ELSE l[idx].view \* True if log l is valid log choice from the set of logs ls. @@ -408,8 +412,7 @@ ModifyAppendEntries(m) == [ type |-> "AppendEntries", view |-> m.view, log |-> SubSeq(m.log,1,Len(m.log)-1) \o - <<[Last(m.log) EXCEPT !.tx = 1]>>, - commitIndex |-> m.commitIndex + <<[Last(m.log) EXCEPT !.tx = 1]>> ] From a2a11e86659218bac598ce1388ca57aa4e2ee91e Mon Sep 17 00:00:00 2001 From: Heidi Howard <1835251+heidihoward@users.noreply.github.com> Date: Tue, 26 Nov 2024 10:22:22 +0000 Subject: [PATCH 3/9] naming again --- pirateship.tla | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/pirateship.tla b/pirateship.tla index f9fddde..4660139 100644 --- a/pirateship.tla +++ b/pirateship.tla @@ -162,12 +162,12 @@ IsQC(e) == HighestCrashQC(l) == IF l = <<>> THEN 0 ELSE Last(l).crashQC -\* Given a log l, returns the index of the highest log entry with a quorum certificate, 0 if the log contains no QCs +\* Given a log l, returns the index of the highest log entry with a byzantine QC, 0 if the log contains no QCs HighestByzQC(l) == LET idx == SelectLastInSeq(l, IsQC) IN IF idx = 0 THEN 0 ELSE Max(l[idx].byzQC) -\* Given a log l, returns the index of the highest log entry with a quorum certificate over a quorum certificate +\* Given a log l, returns the index of the highest log entry with a byzQC over a byzQC HighestQCOverQC(l) == LET lidx == HighestByzQC(l) idx == SelectLastInSubSeq(l, 1, lidx, IsQC) From a7fc6cff2789b483348dd13adec2546ebdfb79e8 Mon Sep 17 00:00:00 2001 From: Heidi Howard <1835251+heidihoward@users.noreply.github.com> Date: Tue, 26 Nov 2024 11:38:48 +0000 Subject: [PATCH 4/9] well formed logs --- MCpirateship.cfg | 1 - SIMpirateship.cfg | 3 +-- pirateship.tla | 42 ++++++++++++++++++++++++++---------------- 3 files changed, 27 insertions(+), 19 deletions(-) diff --git a/MCpirateship.cfg b/MCpirateship.cfg index a83f9ea..03fd37c 100644 --- a/MCpirateship.cfg +++ b/MCpirateship.cfg @@ -22,7 +22,6 @@ INVARIANT ByzLogInv OneLeaderPerTermInv WellFormedLogInv - WellFormedQCsInv PROPERTIES CommittedLogAppendOnlyProp diff --git a/SIMpirateship.cfg b/SIMpirateship.cfg index 2eb504d..33a8560 100644 --- a/SIMpirateship.cfg +++ b/SIMpirateship.cfg @@ -12,7 +12,7 @@ CONSTANT R = {a,b,c,Z} BR = {Z} - MaxByzActions = 2 + MaxByzActions = 0 INVARIANT TypeOK @@ -21,7 +21,6 @@ INVARIANT ByzLogInv OneLeaderPerTermInv WellFormedLogInv - WellFormedQCsInv PROPERTIES CommittedLogAppendOnlyProp diff --git a/pirateship.tla b/pirateship.tla index 4660139..29d1979 100644 --- a/pirateship.tla +++ b/pirateship.tla @@ -184,6 +184,24 @@ MaxQuorum(l, m, default) == THEN i ELSE RMaxQuorum(i-1) IN RMaxQuorum(Len(l)) +\* Checks if a log l is well formed e.g. terms are monotonically increasing +WellFormedLog(l) == + \A i \in DOMAIN l : + \* check views are monotonically increasing + /\ i > 1 => l[i-1].view <= l[i].view + \* check byzQCs are well formed + /\ \A q \in l[i].byzQC : + \* byzQCs are always for previous entries + /\ q < i + \* byzQCs are always formed in the current view + /\ l[q].view = l[i].view + \* byzQCs are in increasing order + /\ \A j \in 1..i-1 : + \A qj \in l[j].byzQC: qj < q + \* check crashQCs are well formed + /\ l[i].crashQC < i + /\ i > 1 => l[i-1].crashQC <= l[i].crashQC + \* Replica r handling AppendEntries from primary p ReceiveEntries(r, p) == \* there must be at least one message pending @@ -196,6 +214,8 @@ ReceiveEntries(r, p) == /\ Last(Head(network[r][p]).log).view = view[r] \* the replica only appends (one entry at a time) to its log /\ log[r] = Front(Head(network[r][p]).log) + \* received log must be well formed + /\ WellFormedLog(Head(network[r][p]).log) \* for convenience, we replace the replica's log with the received log but in practice we are only appending one entry /\ log' = [log EXCEPT ![r] = Head(network[r][p]).log] \* we remove the AppendEntries message and reply with a Vote message. @@ -223,6 +243,8 @@ ReceiveNewLeader(r, p) == /\ Head(network[r][p]).type = "NewLeader" \* the replica must be in the same view or lower /\ view[r] \leq Head(network[r][p]).view + \* received log must be well formed + /\ WellFormedLog(Head(network[r][p]).log) \* update the replica's local view \* note that we do not dispatch a view change message as a primary has already been elected /\ view' = [view EXCEPT ![r] = Head(network[r][p]).view] @@ -366,7 +388,8 @@ BecomePrimary(r) == /\ primary' = [primary EXCEPT ![r] = TRUE] \* primary updates its commit indexes \* Crash commit index may be decreased if there's been an byz attack - /\ crashCommitIndex' = [crashCommitIndex EXCEPT ![r] = Min2(@, Len(log'[r]))] + /\ crashCommitIndex' = [crashCommitIndex EXCEPT + ![r] = Max2(Min2(@, Len(log'[r])), HighestCrashQC(log'[r]))] /\ UNCHANGED <> \* Replicas will discard messages from previous views or extra view changes messages @@ -518,19 +541,6 @@ IndexBoundsInv == /\ byzCommitIndex[r] <= crashCommitIndex[r] WellFormedLogInv == - \A r \in CR : - \A i, j \in DOMAIN log[r] : - i < j => log[r][i].view <= log[r][j].view - -WellFormedQCsInv == - \A r \in CR : - \A i \in DOMAIN log[r] : - \A q \in log[r][i].byzQC : - \* qcs are always for previous entries - /\ q < i - \* qcs are always formed in the current view - /\ log[r][q].view = log[r][i].view - \* qcs are in increasing order - /\ \A j \in 1..i-1 : - \A qj \in log[r][j].byzQC: qj < q + \A r \in CR : WellFormedLog(log[r]) + ==== \ No newline at end of file From bdf4f4583f994411ccb5881ebccddbcf4e21c719 Mon Sep 17 00:00:00 2001 From: Heidi Howard <1835251+heidihoward@users.noreply.github.com> Date: Tue, 26 Nov 2024 11:39:44 +0000 Subject: [PATCH 5/9] byzantine action back to 2 --- SIMpirateship.cfg | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/SIMpirateship.cfg b/SIMpirateship.cfg index 33a8560..d9ba7dc 100644 --- a/SIMpirateship.cfg +++ b/SIMpirateship.cfg @@ -12,7 +12,7 @@ CONSTANT R = {a,b,c,Z} BR = {Z} - MaxByzActions = 0 + MaxByzActions = 2 INVARIANT TypeOK From 1b146c55e7ae6a487af2aa80e56f4c987e127d58 Mon Sep 17 00:00:00 2001 From: Heidi Howard <1835251+heidihoward@users.noreply.github.com> Date: Tue, 26 Nov 2024 14:10:47 +0000 Subject: [PATCH 6/9] adding crash only CI --- .github/workflows/tla.yml | 4 +++- SIMpirateshipCrash.cfg | 39 +++++++++++++++++++++++++++++++++++++++ 2 files changed, 42 insertions(+), 1 deletion(-) create mode 100644 SIMpirateshipCrash.cfg diff --git a/.github/workflows/tla.yml b/.github/workflows/tla.yml index 561e070..41a967f 100644 --- a/.github/workflows/tla.yml +++ b/.github/workflows/tla.yml @@ -17,7 +17,9 @@ jobs: run: wget https://nightly.tlapl.us/dist/tla2tools.jar - name: Get (nightly) CommunityModules run: wget https://github.com/tlaplus/CommunityModules/releases/latest/download/CommunityModules-deps.jar - - name: Random simulation with TLC + - name: Random simulation with TLC (crash) + run: java -Dtlc2.TLC.stopAfter=600 -XX:+UseParallelGC -jar tla2tools.jar -workers auto -simulate SIMpirateship.tla -config SIMpirateshipCrash.cfg + - name: Random simulation with TLC (byzantine) run: java -Dtlc2.TLC.stopAfter=600 -XX:+UseParallelGC -jar tla2tools.jar -workers auto -simulate SIMpirateship.tla tlc-verify: diff --git a/SIMpirateshipCrash.cfg b/SIMpirateshipCrash.cfg new file mode 100644 index 0000000..33a8560 --- /dev/null +++ b/SIMpirateshipCrash.cfg @@ -0,0 +1,39 @@ +SPECIFICATION Spec + +CONSTANT + Timeout <- SIMTimeout + + Txs = {1,2,3,4} + + a = a + b = b + c = c + Z = Z + R = {a,b,c,Z} + BR = {Z} + + MaxByzActions = 0 + +INVARIANT + TypeOK + IndexBoundsInv + LogInv + ByzLogInv + OneLeaderPerTermInv + WellFormedLogInv + +PROPERTIES + CommittedLogAppendOnlyProp + ByzCommittedLogAppendOnlyProp + +CONSTRAINTS + CrashCommitIndexAt1 + CrashCommitIndexAt2 + ByzCommitIndexAt1 + ByzCommitIndexAt2 + +POSTCONDITION + MonitorPostcondition + +_PERIODIC + PrintMonitors \ No newline at end of file From 531e5ca794292d45e6eb20e7648641972b6c80ff Mon Sep 17 00:00:00 2001 From: Heidi Howard <1835251+heidihoward@users.noreply.github.com> Date: Tue, 26 Nov 2024 16:02:41 +0000 Subject: [PATCH 7/9] earlier detection --- MCpirateship.cfg | 1 + SIMpirateship.cfg | 3 ++- pirateship.tla | 8 +++++++- 3 files changed, 10 insertions(+), 2 deletions(-) diff --git a/MCpirateship.cfg b/MCpirateship.cfg index 03fd37c..1bae06f 100644 --- a/MCpirateship.cfg +++ b/MCpirateship.cfg @@ -22,6 +22,7 @@ INVARIANT ByzLogInv OneLeaderPerTermInv WellFormedLogInv + QuorumAgreementInv PROPERTIES CommittedLogAppendOnlyProp diff --git a/SIMpirateship.cfg b/SIMpirateship.cfg index d9ba7dc..636fee4 100644 --- a/SIMpirateship.cfg +++ b/SIMpirateship.cfg @@ -12,7 +12,7 @@ CONSTANT R = {a,b,c,Z} BR = {Z} - MaxByzActions = 2 + MaxByzActions = 0 INVARIANT TypeOK @@ -21,6 +21,7 @@ INVARIANT ByzLogInv OneLeaderPerTermInv WellFormedLogInv + QuorumAgreementInv PROPERTIES CommittedLogAppendOnlyProp diff --git a/pirateship.tla b/pirateship.tla index 29d1979..59e84ec 100644 --- a/pirateship.tla +++ b/pirateship.tla @@ -184,7 +184,7 @@ MaxQuorum(l, m, default) == THEN i ELSE RMaxQuorum(i-1) IN RMaxQuorum(Len(l)) -\* Checks if a log l is well formed e.g. terms are monotonically increasing +\* Checks if a log l is well formed e.g. views are monotonically increasing WellFormedLog(l) == \A i \in DOMAIN l : \* check views are monotonically increasing @@ -543,4 +543,10 @@ IndexBoundsInv == WellFormedLogInv == \A r \in CR : WellFormedLog(log[r]) +\* Classic CFT safety property - if a log entry is committed on one replica, it is present on crash quorum of replicas +QuorumAgreementInv == + byzActions = 0 => + \A i \in R: \E q \in CQ: + \A j \in q: IsPrefix(Committed(i), log[j]) + ==== \ No newline at end of file From 3865a2633ad920cffaf48140643cdb68baf9dc2c Mon Sep 17 00:00:00 2001 From: Heidi Howard <1835251+heidihoward@users.noreply.github.com> Date: Wed, 27 Nov 2024 10:19:22 +0000 Subject: [PATCH 8/9] making crashQCs optional --- pirateship.tla | 37 +++++++++++++++++++++++++------------ 1 file changed, 25 insertions(+), 12 deletions(-) diff --git a/pirateship.tla b/pirateship.tla index 59e84ec..a2818ef 100644 --- a/pirateship.tla +++ b/pirateship.tla @@ -91,7 +91,7 @@ LogEntry == [ tx: Txs, \* For convenience, we represent a quorum certificate as a set but it can only be empty or a singleton byzQC: SUBSET QC, - crashQC: QC] + crashQC: SUBSET QC] \* A log is a sequence of log entries. The index of the log entry is its sequence number/height \* We do not explicitly model the parent relationship, the parent of log entry i is log entry i-1 @@ -155,22 +155,26 @@ Init == ---- \* Actions -IsQC(e) == +IsByzQC(e) == e.byzQC # {} -\* Given a log l, returns the index of the highest log entry with a crash QC, 0 if the log contains no entries +IsCrashQC(e) == + e.crashQC # {} + +\* Given a log l, returns the index of the highest log entry with a crash QC, 0 if the log contains no crash QCs HighestCrashQC(l) == - IF l = <<>> THEN 0 ELSE Last(l).crashQC + LET idx == SelectLastInSeq(l, IsCrashQC) + IN IF idx = 0 THEN 0 ELSE Max(l[idx].crashQC) -\* Given a log l, returns the index of the highest log entry with a byzantine QC, 0 if the log contains no QCs +\* Given a log l, returns the index of the highest log entry with a byzQC, 0 if the log contains no byzQCs HighestByzQC(l) == - LET idx == SelectLastInSeq(l, IsQC) + LET idx == SelectLastInSeq(l, IsByzQC) IN IF idx = 0 THEN 0 ELSE Max(l[idx].byzQC) \* Given a log l, returns the index of the highest log entry with a byzQC over a byzQC HighestQCOverQC(l) == LET lidx == HighestByzQC(l) - idx == SelectLastInSubSeq(l, 1, lidx, IsQC) + idx == SelectLastInSubSeq(l, 1, lidx, IsByzQC) IN IF idx = 0 THEN 0 ELSE Max(l[idx].byzQC) Max2(a,b) == IF a > b THEN a ELSE b @@ -199,8 +203,12 @@ WellFormedLog(l) == /\ \A j \in 1..i-1 : \A qj \in l[j].byzQC: qj < q \* check crashQCs are well formed - /\ l[i].crashQC < i - /\ i > 1 => l[i-1].crashQC <= l[i].crashQC + /\ \A q \in l[i].crashQC : + \* crashQCs are always for previous entries + /\ q < i + \* crashQCs are in increasing order + /\ \A j \in 1..i-1 : + \A qj \in l[j].crashQC: qj < q \* Replica r handling AppendEntries from primary p ReceiveEntries(r, p) == @@ -291,7 +299,12 @@ ReceiveVote(p, r) == MaxQuorum(log[p], matchIndex'[p], @)] /\ UNCHANGED <> -MaxQC(l, m) == +MaxCrashQC(l,p) == + IF crashCommitIndex[p] > HighestCrashQC(l) + THEN {crashCommitIndex[p]} + ELSE {} + +MaxByzQC(l, m) == IF MaxQuorum(l, m, 0) > HighestByzQC(l) THEN {MaxQuorum(l, m, 0)} ELSE {} @@ -308,8 +321,8 @@ SendEntries(p) == /\ log' = [log EXCEPT ![p] = Append(@, [ view |-> view[p], tx |-> tx, - crashQC |-> crashCommitIndex[p], - byzQC |-> MaxQC(log[p], matchIndex'[p])])] + crashQC |-> MaxCrashQC(log[p], p), + byzQC |-> MaxByzQC(log[p], matchIndex'[p])])] /\ network' = [r \in R |-> [s \in R |-> IF s # p \/ r=p THEN network[r][s] ELSE Append(network[r][s], [ From da9d0897104f7b61c229853206d5a515ba3ce6b6 Mon Sep 17 00:00:00 2001 From: Heidi Howard <1835251+heidihoward@users.noreply.github.com> Date: Wed, 27 Nov 2024 10:51:52 +0000 Subject: [PATCH 9/9] return SIMpirateship to byz actions --- SIMpirateship.cfg | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/SIMpirateship.cfg b/SIMpirateship.cfg index 636fee4..a360189 100644 --- a/SIMpirateship.cfg +++ b/SIMpirateship.cfg @@ -12,7 +12,7 @@ CONSTANT R = {a,b,c,Z} BR = {Z} - MaxByzActions = 0 + MaxByzActions = 2 INVARIANT TypeOK