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
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"}]
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"}]
/\ 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
/\ days = 0
wPending(s,j,w) ==
(*is this the correct way to say any of these can be the state?*)
(*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"]
/\ 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).
ELSE IF jdState[j] = "outside" /\ days > 91 THEN days + 1
/\ UNCHANGED <<sState, jdState, dState>> <-- This is where the error is (line 48).
...
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"}]?