| Hello Pierre-Louis,
thanks for sharing the spec, here are a few comments:
- The operators ValidPath and Sessions are not used (but ValidPaths and Session are), I suggest removing unused operators.
- A valid path consists of a base path followed by a sequence of rename tags. This suggests defining
ValidPaths == BasePaths \X Seq(RenameTags) or ValidPaths == [base : BasePaths, tags: Seq(RenameTags)]
which is simpler than your definition. The potential drawback is that your renaming operators would have to be adapted, such as
LocalRenamePath(p) == [base |-> p.base, tags |-> Append(p.tags, "vl")]
but perhaps this is in fact clearer than just a global Append.
I also suggest expressing the constraint on path length through a state constraint in the configuration file rather than including it in the TLA spec because this is only needed for bounding the state space for model checking, not for expressing the logic of the protocol. These changes will probably allow you to get rid of the operator CanRenamePath.
- The definitions of the two operators PullAndRenameIfSamePathDifferentHash and RenameIfSameHashDifferentPath are very similar. In the first definition, the part
[…, ![remoteSystem] = ((@ \ {sremote}) \cup {sremote})]
looks fishy (in particular because the condition ensures that remote appears among the sessions of the remote system), and if you remove it, the only differences are the guards SamePathDifferentHash(slocal, sremote) and SameHashDifferentPath(slocal, sremote), so it looks like you could have a single operator with the disjunction of these guards.
- I believe that most of your guards expressing that certain entities are different (e.g. newHash # oldSession.hash or localSystem # remoteSystem) could be removed because either they are unnecessary (for example, if the two systems are the same you cannot have a local session but no remote session with the same path) or because equality simply leads to a stuttering transition, which is possible anyway.
- Finally, a spec is usually written with the objective of ensuring that certain properties hold. Your TypeOK is a good start (and in fact it is not entirely trivial), but perhaps you could think of additional properties. I do not immediately see additional safety properties: if we had some principal entities and some backup systems, one could think of sessions appearing on backups only if they already exist in a principal entity, but your setup is entirely symmetric. But perhaps you could think of some fairness properties for syncing sessions that would make copies converge, assuming that a session is no longer edited or something along these lines?
Hope you find this helpful, Stephan On 14 Apr 2026, at 11:53, Pierre-Louis Suckrow <suckrowpierre@xxxxxxxxx> wrote:
Hey all, 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: - Paths and Hashes Match:
- If the path exists in both systems (local and remote), and both paths and hashes are identical:
- No Diff: No changes required.
- Same Path, Different Hashes:
- If the paths are the same but the hashes differ:
- Alternate Versions: The file exists in both systems with different versions.
- Different Paths, Same Hash:
- If the paths are different, but the hashes match:
- Different Names: The file is the same but renamed in one of the systems.
- Missing on Remote:
- If the path exists on the local system but not on the remote:
- Missing: The file is absent on the remote system.
- New on Remote:
- If the path exists on the remote system but not locally:
- New: The file is newly added to the remote system.
When not syncing users can perform the following operations on local or remote system: - Add Files: Users can add new project files.
- Rename Files: This changes the file's path but keeps the same hash.
- Edit Files: Editing a file causes its hash to change, indicating a different version.
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
--
You received this message because you are subscribed to the Google Groups "tlaplus" group.
To unsubscribe from this group and stop receiving emails from it, send an email to tlaplus+unsubscribe@xxxxxxxxxxxxxxxx.
To view this discussion visit https://groups.google.com/d/msgid/tlaplus/fe6647e7-dc35-43f4-9ae0-82755e0dfa40n%40googlegroups.com.
<ProjectSync.tla><ProjectSync.cfg>
You received this message because you are subscribed to the Google Groups "tlaplus" group.
To unsubscribe from this group and stop receiving emails from it, send an email to tlaplus+unsubscribe@xxxxxxxxxxxxxxxx.
To view this discussion visit https://groups.google.com/d/msgid/tlaplus/30D92F32-1DCA-488B-849F-006F3C384EBD%40gmail.com.
|