8b520284cb
#12: All 5 untranslated SpeckDL patterns now emit valid JS: - notIn → !.has(), old() → drop, union → Set spread, set diff → filter, append() → [...X, Y], length() → .length - ==/!= operator replacement fixed (word-boundary regression) - Postcondition object comparisons get @ts-expect-error TS2839 #11: Generator auto-detects opaque identifier types used in state variables and action params, emits 'type X = any' before class. - State properties use ! (non-null assertion) for strict mode TigerBeetleLedger → tsc --noEmit = 0 errors. 37/37 tests pass.
59 lines
1.9 KiB
TypeScript
59 lines
1.9 KiB
TypeScript
// Auto-generated by speckl-compile from KafkaKRaft
|
|
// DO NOT EDIT MANUALLY — regenerate from .speckdl source
|
|
|
|
export const KafkaKRaftState = {
|
|
Candidate: 'candidate',
|
|
Leader: 'leader',
|
|
} as const;
|
|
export type KafkaKRaftState = typeof KafkaKRaftState[keyof typeof KafkaKRaftState];
|
|
|
|
|
|
|
|
|
|
export class KafkaKRaftMachine {
|
|
currentTerm: number;
|
|
state: KafkaKRaftState;
|
|
votedFor: Option(NodeId);
|
|
log: LogEntry[];
|
|
commitIndex: number;
|
|
nextIndex: Map<NodeId, number>;
|
|
matchIndex: Map<NodeId, number>;
|
|
votesGranted: Set<NodeId>;
|
|
decisionLog: any[] = [];
|
|
|
|
constructor() {
|
|
// No init block defined
|
|
}
|
|
|
|
RequestVote(candidate: NodeId, lastLogTerm: number, lastLogIndex: number) {
|
|
if (!(this.state == KafkaKRaftState.Candidate)) throw new Error('Guard failed: this.state == KafkaKRaftState.Candidate');
|
|
if (!(this.currentTerm >= lastLogTerm)) throw new Error('Guard failed: this.currentTerm >= lastLogTerm');
|
|
this.votesGranted = new Set([...this.votesGranted, candidate]);
|
|
}
|
|
|
|
HandleRequestVoteRequest(candidate: NodeId, candidateTerm: number, lastLogTerm: number, lastLogIndex: number) {
|
|
if (!(this.currentTerm >= candidateTerm)) throw new Error('Guard failed: this.currentTerm >= candidateTerm');
|
|
this.votedFor = Some(candidate);
|
|
}
|
|
|
|
BecomeLeader() {
|
|
if (!(this.state == KafkaKRaftState.Candidate)) throw new Error('Guard failed: this.state == KafkaKRaftState.Candidate');
|
|
if (!(this.votesGranted.size >= 3)) throw new Error('Guard failed: this.votesGranted.size >= 3');
|
|
this.state = KafkaKRaftState.Leader;
|
|
this.commitIndex = length(this.log);
|
|
}
|
|
|
|
AppendEntries(follower: NodeId) {
|
|
if (!(this.state == KafkaKRaftState.Leader)) throw new Error('Guard failed: this.state == KafkaKRaftState.Leader');
|
|
this.log = append(this.log, newEntry);
|
|
}
|
|
|
|
|
|
|
|
// V1: Always(TermMonotonicity)
|
|
async verify1(): Promise<boolean> {
|
|
// TODO: Model-check or monitor
|
|
// Temporal: Always(TermMonotonicity)
|
|
return true;
|
|
}
|
|
}
|