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

*From*: Georgios Chinis <georgios.chinis@xxxxxxxxx>*Date*: Mon, 7 Dec 2020 17:29:32 +0100

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" ] ]

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

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 )

<>[](\A u \in

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:

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.

**Follow-Ups**:

- Prev by Date:
**Re: [tlaplus] How to say "Taking Action A leads to X"?** - Next by Date:
**[tlaplus] Initial state doesn't satisfy type invariant** - Previous by thread:
**Re: [tlaplus] How to say "Taking Action A leads to X"?** - Next by thread:
**Re: [tlaplus] A temporal formula to specify that the value of a record does not change** - Index(es):