Focustro TLA+

consistency.cfg

CONSTANTS
    ClientIds = {c1, c2}
    ObjectIds = {o1, o2}
    PropNames = {p1, p2}
    Values = {v1, v2, v3}
    NULL = NULL
    MaxWrites = 3
    MaxNetworkFailures = 2

SPECIFICATION Spec

PROPERTY Properties

consistency.tla

This is a specification of the server synchronisation for Focustro.

I am not very experienced with TLA+, so this shouldn't be considered good style.
Let me know if you think this can be improved.

------------------------ MODULE consistency ------------------------
EXTENDS Integers, Sequences, TLC

CONSTANTS ClientIds, ObjectIds, PropNames, Values, NULL, MaxWrites, MaxNetworkFailures
VARIABLES clientStates, serverState, usedIds, writeCount, networkFailures

Init ==
    (* Clients start with an empty set of objects and a NULL lastTimestamp *)
    /\  clientStates = [
            clientId \in ClientIds |->
                [
                    objects |-> [objectId \in ObjectIds |-> NULL],
                    writeQueue |-> << >>,
                    lastTimestamp |-> NULL,
                    inbox |-> << >>
                ]
        ]
    (* The server starts with an empty set of objects and a 0 timestamp *)
    /\  serverState = [
            objects |-> [objectId \in ObjectIds |-> NULL],
            timestamp |-> 0,
            inbox |-> << >>
        ]
    (* Simulate UUIDs by keeping track of used IDs *)
    /\  usedIds = {}
    (* Keep track of the number of writes to limit the state space to MaxWrites *)
    /\  writeCount = 0
    (* Keep track of the number of failures to limit the state space to MaxNetworkFailures *)
    /\  networkFailures = 0

(* Client actions *)

(* A client creates a new object using a unique ID *)
CreateObject(clientId, objectId, object) ==
    /\ 	writeCount < MaxWrites
    /\ 	objectId \notin usedIds
    /\ 	clientStates[clientId].objects[objectId] = NULL
    /\ 	clientStates' = [
            clientStates EXCEPT
            ![clientId].objects[objectId] = object,
            (* queue a 'create' operation *)
            ![clientId].writeQueue = Append(@,
                [
                    writeId |-> writeCount,
                    op |-> "create",
                    id |-> objectId,
                    object |-> object
                ]
            )
        ]
    /\ 	usedIds' = usedIds \union {objectId}
    /\ 	writeCount' = writeCount + 1
    /\ 	UNCHANGED << serverState, networkFailures >>

(* A client updates a property of an existing object *)
ModifyProperty(clientId, objectId, property, value) ==
    /\ 	writeCount < MaxWrites
    /\ 	clientStates[clientId].objects[objectId] /= NULL
    /\ 	clientStates' = [
            clientStates EXCEPT
            ![clientId].objects[objectId][property] = value,
            (* queue an 'update' operation *)
            ![clientId].writeQueue = Append(@,
                [
                    writeId |-> writeCount, 
                    op |-> "update", 
                    id |-> objectId, 
                    property |-> property, 
                    value |-> value
                ]
            )
        ]
    /\ 	writeCount' = writeCount + 1
    /\ 	UNCHANGED << usedIds, serverState, networkFailures >>


(* A client should periodically send a sync request to the server *)
ClientSend(clientId) ==
    (* To limit the state space, only send one message at a time to the server *)
    /\  serverState.inbox = << >>
    (* Don't send if there are messages waiting to be processed from the server *)
    /\  clientStates[clientId].inbox = << >>
    /\  \/  clientStates[clientId].writeQueue /= << >>
        \/  clientStates[clientId].lastTimestamp /= serverState.timestamp
    /\  serverState' = [
            serverState EXCEPT
            !.inbox = Append(@, [
                clientId |-> clientId,
                lastTimestamp |-> clientStates[clientId].lastTimestamp,
                write |->
                    IF clientStates[clientId].writeQueue /= << >>
                        THEN Head(clientStates[clientId].writeQueue)
                        ELSE NULL
            ])
        ]
    /\  UNCHANGED << clientStates, usedIds, writeCount, networkFailures >>

(* The client receives a response from the server *)
ClientRecv(clientId) ==
    /\  clientStates[clientId].inbox /= << >>
    /\  clientStates' =
            LET msg == Head(clientStates[clientId].inbox)
                writes == clientStates[clientId].writeQueue
                check(write) == write.writeId /= msg.ack
            IN [
                clientStates EXCEPT 
                ![clientId].inbox = Tail(@),
                ![clientId].writeQueue = SelectSeq(writes, check),
                ![clientId].lastTimestamp = msg.timestamp,
                ![clientId].objects = [
                    objectId \in ObjectIds |->
                        IF objectId \in DOMAIN msg.updates
                            THEN msg.updates[objectId]
                            ELSE @[objectId]
                ]
            ]
    /\  UNCHANGED << serverState, usedIds, writeCount, networkFailures >>

(* The client loses a response from the server *)
ClientLoseMessage(clientId) ==
    /\  clientStates[clientId].inbox /= << >>
    /\  networkFailures < MaxNetworkFailures
    /\  clientStates' = [clientStates EXCEPT ![clientId].inbox = Tail(@)]
    /\  networkFailures' = networkFailures + 1
    /\  UNCHANGED << serverState, usedIds, writeCount >>

(* Server helpers *)

ApplyWrite(write, serverObjects, timestamp) ==
    IF write = NULL THEN serverObjects ELSE
    IF write.op = "create"
        THEN [serverObjects EXCEPT ![write.id] = [object |-> write.object, updated |-> timestamp]]
        ELSE [serverObjects EXCEPT ![write.id] = [
            object |-> [@.object EXCEPT ![write.property] = write.value],
            updated |-> timestamp
        ]]

UpdatedObjects(serverObjects, clientTimestamp) ==
    IF clientTimestamp = NULL
    THEN LET S == {objectId \in ObjectIds : serverObjects[objectId] /= NULL}
         IN  [ objectId \in S |-> serverObjects[objectId].object ]
    ELSE LET S == {objectId \in ObjectIds : /\ serverObjects[objectId] /= NULL
                                            /\ serverObjects[objectId].updated > clientTimestamp}
         IN  [ objectId \in S |-> serverObjects[objectId].object ]

(* Server actions *)

(* The server receives a message from a client *)
ServerRecv ==
    /\  serverState.inbox /= << >>
    /\  LET msg == Head(serverState.inbox)
            newTimestamp == IF msg.write = NULL
                            THEN serverState.timestamp
                            ELSE serverState.timestamp + 1
        IN
        /\  serverState' = [
                serverState EXCEPT
                !.objects = ApplyWrite(msg.write, serverState.objects, newTimestamp),
                !.inbox = Tail(@),
                !.timestamp = newTimestamp
            ]
        /\  clientStates' = [
                clientStates EXCEPT
                ![msg.clientId].inbox = Append(@,
                    [
                        timestamp |-> newTimestamp,
                        ack |-> IF msg.write = NULL THEN NULL ELSE msg.write.writeId,
                        updates |-> UpdatedObjects(serverState'.objects, msg.lastTimestamp)
                    ]
                )
            ]
    /\	UNCHANGED <<usedIds, writeCount, networkFailures>>

(* The server loses a message from a client *)
ServerLoseMessage ==
    /\  serverState.inbox /= << >>
    /\  networkFailures < MaxNetworkFailures
    /\  serverState' = [
            serverState EXCEPT
            !.inbox = Tail(@)
        ]  
    /\  networkFailures' = networkFailures + 1
    /\	UNCHANGED <<clientStates, usedIds, writeCount>>
    

(* System actions *)

Next == \/  \E clientId \in ClientIds :
            \E objectId \in ObjectIds :
            \E object \in [PropNames -> Values] :
            CreateObject(clientId, objectId, object)
        \/  \E clientId \in ClientIds :
            \E objectId \in ObjectIds :
            \E prop \in PropNames :
            \E value \in Values :
            ModifyProperty(clientId, objectId, prop, value)
        \/  \E clientId \in ClientIds : ClientSend(clientId)
        \/  \E clientId \in ClientIds : ClientRecv(clientId)
        \/  \E clientId \in ClientIds : ClientLoseMessage(clientId)
        \/  ServerRecv
        \/  ServerLoseMessage

AllVars == <<clientStates, usedIds, serverState, writeCount, networkFailures>>

(* Temporal properties *)

(* Assume that the client and server will eventually send/receive requests, even if the network *)
(* is temporarily down *)
Fairness ==
    /\  \A clientId \in ClientIds :
        /\  WF_AllVars(ClientRecv(clientId))
        /\  WF_AllVars(ClientSend(clientId))
    /\  WF_AllVars(ServerRecv)

Spec == Init /\ [][Next]_AllVars /\ Fairness

(* Properties to be checked *)

Consistent ==
    \E clientId1 \in ClientIds :
    \A clientId2 \in ClientIds :
    clientStates[clientId1].objects = clientStates[clientId2].objects

Properties ==
    <>[]Consistent

========================================================================