Hello amazing TLA+ community,
I need your help.
I am trying to develop the specification for a system that is going to merge the records of one data source into another data source. There are different rules about how each individual field should be merged. I am trying to develop some invariants to make sure that the merging is correct.
I am having trouble specifying that one field should actually remain unchanged from the merge.
Here is a simple example:
DataSourceA == [ user1 |-> [ fieldA: {"foo"}, fieldB: "value1" ] ]
DataSourceB == [ user1 |-> [ fieldA: {"bar"}, fieldB: "value2" ], user2 |-> [ fieldA: {"aaa"}, fieldB: "value2" ] ]
My constraints (which I would like to model in TLA+) are that at the end of the merge process:
1. All users in DataSourceB are now in DataSourceA
In TLA+:
<>[](DOMAIN DataSourceB \subseteq DOMAIN nfmUsers)
2. If a user exists in DataSourceA and in DataSourceB, then after the merge in DataSourceA the fieldA will contain the union of the values.
In TLA+:
<>[](\A u \in DOMAIN DataSourceB: DataSourceB[u].locations \subseteq DataSourceA[u].locations )
3. If a user exists in DataSourceA and in DataSourceB, then after the merge in DataSourceA the fieldB will remain unchanged (still contain the initial value).
Here is where I am struggling, how do I express this condition?
A closely related condition would be that for all common users, if the value of fieldB is different in the two DataSources then it will always be different:
\A commonUser \in (DOMAIN DataSourceB \intersect DOMAIN DataSourceA):
DataSourceB[u].role /= DataSourceA[u].role ~> [](DataSourceB[u].role /= DataSourceA[u].role)
Which also doesn't work, I get a runtime when I run TLC.
Is there another way to express the requirement that a field in a record should remain unchanged?
Kind Regards,
Georgios Chinis