[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

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

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 DataSourceBDataSourceB[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

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 on the web visit https://groups.google.com/d/msgid/tlaplus/CACgksMR0vjOFFxeG-ezFv0b489%3Dwf%3DjfXZiFzhw_82qA0YZkCg%40mail.gmail.com.