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

*From*: Stephan Merz <stephan.merz@xxxxxxxxx>*Date*: Tue, 9 Apr 2019 19:04:12 +0200*References*: <bd0c4d46-753e-4cfa-8c70-bac91a52b3fd@googlegroups.com> <1287F129-1A1A-4E50-BDC2-A3B60514D446@gmail.com> <edbb77cb-b6a4-446e-b8b9-d9057522fe17@googlegroups.com> <ECFA4287-6C72-47A1-9D0F-312CE71572B8@gmail.com> <83961f24-139a-4c66-a1fa-fd2f427ef54c@googlegroups.com> <f1693af8-8b92-475e-9a05-c9c6aa99780d@googlegroups.com>

Hello Curt, a few remarks and answers to your questions: /\ sState = [s \in S |-> {"noService"}] This assigns to sState a function mapping each element of s to the set containing the single element "noService". Such a construction is useful if you want to remember different statuses for each "s", say, {"serviceByMail", "failedService"}, to say that a service by mail was attempted but unsuccessful. Looking at your type invariant, it looks like you want to associate each "s" with a single status and write /\ sState = [s \in S |-> "noService"] in the initial condition (i.e., without the set braces). (*is this the way to say any element of JD can be the init state?*) Yes, this is idiomatic, it means that the variable `jdState' can take any element of set JD initially.
Not sure I understand your question or intention. First of all, the type invariant for dState says that it should be a function whereas here it's just a set. I have no feeling for what your constants (S, D, JD, W) represent. If they stand for entities or actors in the system then associating each of them a status (using a function) makes sense. If you are modeling a single entity, no need for using a function. If you'd assign the above set to D in the "What is the model" pane of the Toolbox, you should either use a constant (and typically use model values instead of strings) or introduce a definition D == {"corporation", ...} and eliminate the constant. But I may be completely mistaken about your objective.
A warning: the parameter s occurs nowhere within the right-hand side of the definition!
As you noticed, you are missing a final ELSE (TLA+ is not an imperative language and conditional expressions must be fully defined). Also, the logic looks a bit strange to me: you increment the counter when a threshold is *exceeded*? Shouldn't it be incremented as long as you are below the threshold?
The _expression_ [S -> T] denotes the set of functions that map each element of S (the domain of the function) to some element of T. This typically appears in type correctness invariants to describe the shape of functions that a variable may hold.
[x \in S |-> t] denotes the function with domain S that maps each element x of S to the (value of) the _expression_ t. Unlike the above, it is a single, concrete function. Typically appears in initial conditions or actions to initialize or update a function (which you may think of as an array). If you have some familiarity with functional programming, it is analogous to a lambda-_expression_. Hope this helps, 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 post to this group, send email to tlaplus@xxxxxxxxxxxxxxxx. Visit this group at https://groups.google.com/group/tlaplus. For more options, visit https://groups.google.com/d/optout. |

**Follow-Ups**:**Re: [tlaplus] Fumbling Through TLA+***From:*Curt Flowers

**References**:**[tlaplus] Fumbling Through TLA+***From:*Curt Flowers

**Re: [tlaplus] Fumbling Through TLA+***From:*Stephan Merz

**Re: [tlaplus] Fumbling Through TLA+***From:*Curt Flowers

**Re: [tlaplus] Fumbling Through TLA+***From:*Stephan Merz

**Re: [tlaplus] Fumbling Through TLA+***From:*Curt Flowers

**Re: [tlaplus] Fumbling Through TLA+***From:*Curt Flowers

- Prev by Date:
**[tlaplus] [JOB] Open-source distributed systems proving with TLA+** - Next by Date:
**Re: [tlaplus] Fumbling Through TLA+** - Previous by thread:
**Re: [tlaplus] Fumbling Through TLA+** - Next by thread:
**Re: [tlaplus] Fumbling Through TLA+** - Index(es):