State-Based (CvRDT) sync engine. Replicas exchange full or delta-compressed state using Hybrid Logical Clock (HLC) timestamps for causal ordering. Network trait: Highly resilient to lossy/unstable topologies (UDP, peer-to-peer mesh, radio datalinks) because state merges are fully idempotent. Requirements traceability: - HLR-SYNC-STATE: State-based sync with vector clocks - HLR-SYNC-DELTA: Delta computation for partial state exchange
Note: 6 public item(s) shown below; 1 private internal item(s) are in the
privatesection.
type Replica_State (Max_Replicas : Positive) is record
HLC_Clock : CRDT.HLC.Instance;
SV : Core.VTime (1 .. Max_Replicas);
end record;type Sync_Config is record
Max_Replicas : Positive := 32;
Delta_Sync : Boolean := True;
HLC_Node : Core.Replica_Id;
end record;function Compute_Delta (Local : CRDT.Sync.State_Based.Replica_State; Remote_SV : CRDT.Core.VTime) return Standard.Natural [Post]
| Parameter | Description |
|---|---|
Local |
Local replica state. |
Remote_SV |
Remote state vector. |
Returns: Count of replicas where local is ahead of remote.
function Create (Config : CRDT.Sync.State_Based.Sync_Config) return CRDT.Sync.State_Based.Replica_State
| Parameter | Description |
|---|---|
Config |
Sync configuration. |
Returns: Freshly initialised replica state.
function Is_Ahead (SV : CRDT.Core.VTime; TS : CRDT.Core.Lamport_Time) return Standard.Boolean [Post]
| Parameter | Description |
|---|---|
SV |
State vector to check. |
TS |
Lamport timestamp to compare against. |
Returns: True if the SV has entry at or past TS.
procedure Merge (Local : CRDT.Sync.State_Based.Replica_State; Remote : CRDT.Sync.State_Based.Replica_State) [Depends]
| Parameter | Description |
|---|---|
Local |
Local state to update. |
Remote |
Remote state to merge from. |
- type
Replica_State