CODEWITHSUNDEEP
tla+
Jacob Davis-Hansson
Jacob Davis-Hansson

Reputation: 2663

How to assert a given state leads to a another state with variables in TLA+?

Sorry the title is a bit cryptic. I have a TLA+ spec that defines two sets:

variables Requests = {}, Outcomes = {};

I have one set of workers adding requests, and another set or workers fulfilling them and writing to Outcomes. Each request has a unique Id, which the matching Outcome entry will then also contain.

I want to guarantee that any request added to the Requests set is eventually matched by a structure with the same Id in the Outcomes set. I've been trying to do this using the "leads to", ~>, operator, but can't figure out how to resolve the Id matching portion.

I've naively tried something like:

RequestsAreFulfilled == \E req \in Requests: TRUE 
                        ~> \E outcome \in Outcomes : outcome.id = req.id

But this obviously breaks since req is not defined in the second expression. I've considered something along the lines of the second express being "Then there is a state where all Request items are matched by Outcome items", but that doesn't work since the system never terminates - there may very well always be more requests in the Requests set, since Outcomes is always playing catch-up.

What is a way for me to assert that a request is eventually matched with an outcome with the same id?

Upvotes: 3

Views: 343

Answers (1)

Hovercouch
Hovercouch

Reputation: 2314

TLC has some trouble proving liveness properties with nonconstant sets. Let's start with the fixed case, where you have a finite, fixed set of ids. Then we can specify the relation as

\A id \in Ids: (\E r \in req: r.id = id) ~> (\E o \in out: o.id = id)

In this case, though, we're better off using structures, as they're easier to understand and express shared relationships better.

requested = [i \in Ids |-> FALSE];
processed = [i \in Ids |-> FALSE];

\A id \in Ids: requested[i] ~> processed[i]

or

messages = [i \in Ids |-> [requested |-> FALSE, processed |-> FALSE]]
\A id \in Ids: 
   LET m == messages[i]
   IN  m.requested ~> m.processed

If you want an infinite number of messages, one way to get TLC to handle liveness checks is to use a fixed set of ids then add logic to "recycle" finished messages - set both requested and processed to FALSE. Then we can use the always-eventually operator, []<>, to express this:

\A id \in Ids: []<>(requested[i] => processed[i])

Upvotes: 2

Related Questions