I’ve been trying to model the file synchronization process of project files between two systems. I know that it is not the best model for file syncing, but I still want to write a spec for it to put it in my master thesis as one possible way of doing it (for the specific use case of mine).
Core Idea:Project files are identified using two components: their relativePath and their hash. Based on this there are the following cases:
When not syncing users can perform the following operations on local or remote system:
Users can sync their local state to match the remote system on file basis. If a file is missing remotely but present locally, they have the option to delete it. If the file exists on the remote but not on the local system, it can be copied from the remote. If both systems have the same version, no action is required, apart if the path differs. If the paths differs it can be renamed to match remote. However, if the versions differ and have the same path, the user can pull the version from the remote and both files will be renamed to avoid conflicts (e.g., appending _vl for the local version and _vr for the remote version).
The main difficulty I faced was modeling the renaming process. If the file versions are different, renaming can happen recursively, like this: {original_name)_vl_vr_vl_vr. To avoid state explosion, I introduced a constraint on the maximum recursion depth to limit the number of possible states. But I am not really a fan of having this in my spec.
While the model captures the core behaviors, I’m wondering if there’s a more elegant way to model this or if a more experienced specification writer would approach it differently.
One thing that helps simplify the process is the constraint that the remote system cannot be modified by the local user. This means there’s no need to model concurrent operations, which reduces the complexity of the spec.
I’m also wondering if I might be missing any crucial invariants in my system. Are there any essential conditions or behaviors I haven’t accounted for that could cause issues in the synchronization process? Also my current spec does not allow to define more then two entries for each constant without exploding in complexity, making we wonder if these small sets effectively represent what I am trying to model.
Thanks for taking your time to read this. Just starting with TLA+, so apologies if my spec is a bit ruff.
---
Pierre
--Attachment:
ProjectSync.tla
Description: Binary data
SPECIFICATION Spec
INVARIANT TypeOK
CONSTANTS
Systems = {"local", "remote"}
BasePaths = {"p1","p2"}
Hashes = {"h1","h3"}
MaxPathLen = 2