| 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). 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: 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+unsubscribe@xxxxxxxxxxxxxxxx. To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/E61D7C8B-060D-4551-95F7-DC886150F2C5%40gmail.com. |