Re: [tlaplus] Fumbling Through TLA+

/\ 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?*)
/\ jdState \in JD

Yes, this is idiomatic, it means that the variable `jdState' can take any element of set JD initially.

(*Same as above. However this one would be CONSTANT D. Are both correct and one more verbose or just wrong? I feel without reference to the CONSTANT D, its not right*)
/\ dState \in {"corporation", "foreignCorporation", "individual", "foreignIndividual", "incompententIndividual", "minor", "unincorporatedAssocation", "partnership", "US", "USOfficer", "localGov", "stateGov", "foreignGov", "USEmployee", "USAgency", "USCorporation", "USOfficerIndividual", "USEmployeeIndividual"}

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.

wPending(s,j,w) == ...

A warning: the parameter s occurs nowhere within the right-hand side of the definition!

(*while I'm getting no errors, is this correct? The main error is still stopping me from running the checker.*)
/\ days' = IF jdState[j] = "within" /\ days > 61 THEN days + 1
ELSE IF jdState[j] = "outside" /\ days > 91 THEN days + 1

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?

Lastly, can someone explain what "->" means?

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.

Also, the "maps to" symbol ( |-> ).

[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

On 2 Apr 2019, at 20:38, Curt Flowers <curtycurt01@xxxxxxxxx> wrote:

Looks like I'm back again with some struggles. I've started on my second module but I'm getting errors I don't understand how to fix but the larger issues is I simply don't understand some basic things. Feeling like I'm guessing is not a good. Its like any other language: I understand what I'm looking at faster than I can actually write it out correctly. Or in this case, write a proper spec. I'm re-reading through the Specifying Systems, and trying to learn the underline math areas better outside of TLA to try and understand how the formulas are put together better. Still, I'm unsure of a lot when it comes to applying what I do *think* I understand to my spec. But I digress. Going to keep trying (please point me to resources for better understanding if anyone has suggestions). The new issue: (questions added and highlighted throughout)

EXTENDS Naturals
CONSTANT S, D, JD, W
VARIABLE days, dState, jdState, sState, wState

\*Defendant
DTypeOK ==
dState \in [D -> {"corporation", "foreignCorporation", "individual", "incompententIndividual", "minor", "unincorporatedAssocation", "partnership", "US", "USOfficer", "localGov", "stateGov", "foreignGov", "USEmployee", "USAgency", "USCorporation", "USOfficerIndividual", "USEmployeeIndividual"}]

\*Summons
STypeOK ==
sState \in [S -> {"summons", "served", "summonsPending", "noService", "serviceByMail", "failedService"}]

\*Waiver
WTypeOK ==
wState \in [W -> {"noWaiver", "noticeOfWaiver", "waiverRejected", "waiverAccepted", "waiverPending", "waiverFiled"}]

SInit ==
     /\ sState = [s \in S |-> {"noService"}]
     /\ wState = [w \in W |-> {"noWaiver"}]

     (*is this the way to say any element of JD can be the init state?*)
     /\ jdState \in JD

     (*Same as above. However this one would be CONSTANT D. Are both correct and one more verbose or just wrong? I feel without reference to the CONSTANT D, its not right*)
     /\ dState \in {"corporation", "foreignCorporation", "individual", "foreignIndividual", "incompententIndividual", "minor", "unincorporatedAssocation", "partnership", "US", "USOfficer", "localGov", "stateGov", "foreignGov", "USEmployee", "USAgency", "USCorporation", "USOfficerIndividual", "USEmployeeIndividual"}
     /\ days = 0

wPending(s,j,w) ==
(*is this the correct way to say any of these can be the state?*)
/\ dState \in {"cor pration", "individual", "unincorporatedAssocation"}

(*Again, I'd like to say that it can be either state though I have have it as only one as I was going to make another definition to hack together something that I could get working before refactoring*)
/\ jdState[j] = "within"
/\ wState[w] = "noWaiver"
/\ days = 0
/\ wState' = [wState EXCEPT ![w] = "waiverPending"]

(*while I'm getting no errors, is this correct? The main error is still stopping me from running the checker.*)
/\ days' = IF jdState[j] = "within" /\ days > 61 THEN days + 1
                          ELSE IF jdState[j] = "outside" /\ days > 91 THEN days + 1
/\ UNCHANGED <<sState, jdState, dState>> <-- This is where the error is (line 48).
...

<Screen Shot 2019-04-02 at 1.06.33 PM.png>

Lastly, can someone explain what "->" means? When using it in TypeOK invariant (main because it worked in the last module, not because I understand it correctly), it works. I've looked thought the book and don't understand exactly what it means. Online it says it can mean "implies" (which is this =>) but it used heavily thoughout the writings in the book which in context makes sense, but when I need to use it in specs, I not sure what it does.

Also, the "maps to" symbol ( |-> ). Does this mean that a variable equals a specific element, like: sState = [s \in S |-> {"noService"}]?

--
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.
<Screen Shot 2019-04-02 at 1.06.33 PM.png>