No you can also model things that are client-only or server-only using such non-deterministic events.

For example you could have the following client-only properties where you can treat "connection established" as an entirely non-deterministic event that randomly just pops in and happens to the client.

1. Every edit that is stored on the client is preserved in the client's undo/redo log (e.g. a remote edit after a connection established can't clobber any client's local edits that are already preserved in history)

2. Document invariants always hold no matter what connection established/remote edits come in (e.g. even if the document shrinks as a result of remote deletions, the cursor is always in a valid location)

3. Causal consistency and order preservation can be rescoped to also be client-only properties

4. Undoing and redoing with no other local edits always returns back to the original state (e.g. making sure that remote edits coming in don't violate user's expectations about how to get back to a known state) for some definition of "original state" (this depends a lot on how you want to handle merging of remote edits)

5. Remote edits are always applied after a multi-component edit not in the middle (e.g. we never apply a remote edit in the middle of a grapheme cluster such as an emoji or when we're in the middle of writing one).

6. We handle connection affinity properly (e.g. we might have multiple servers for redundancy that can all be connected to, but over the course of a session we cache data for a single endpoint to improve performance that will need to be recalculated if we connect to a new endpoint), so checking that the initial connection to a new endpoint from the client always has the data that the new endpoint needs and we're able to re-establish the connection that doesn't corrupt our client's local data etc.

Etc.

Very helpful. Thank you!