A temporal formula to specify that the value of a record does not change

[Georgios Chinis]

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

[Stephan Merz]

Hello,

a first observation: you write that you are developing invariants that ensure that your spec is correct but you show liveness properties. I'd indeed encourage you to focus primarily on invariants, perhaps expressing post-conditions such as

mergeDone => (DOMAIN DataSourceB) \subseteq (DOMAIN DataSourceA)

where mergeDone is a predicate that holds when the execution has completed.

Second, I am assuming that the sets that appear in the bounds of quantifiers are constants. TLC will only accept quantification over constants at the top level, i.e. you should write

\A u \in DOMAIN DataSourceB : <>[](...)

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?

How about something like

\A u \in (DOMAIN DataSourceA) \cap (DOMAIN DataSourceB) : [][UNCHANGED DataSourceB[u].fieldB]_vars

if you want to assert that the field never changes or

\A u \in (DOMAIN DataSourceA) \cap (DOMAIN DataSourceB), v \in Values :

   DataSourceB[u].field2 = v => [](mergeDone => DataSourceB[u].field2 = v)

if you are only interested in the initial and final values of the field.

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)

Did you really mean to write "~>" (leads-to) here or rather "=>" (implies)? (And I am assuming that "commonUser" should be "u".)

Regards,

Stephan

--
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+u...@googlegroups.com.
To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/CACgksMR0vjOFFxeG-ezFv0b489%3Dwf%3DjfXZiFzhw_82qA0YZkCg%40mail.gmail.com.