Fumbling Through TLA+

[Curt Flowers]

I've created another spec in my journey to learn TLA+

I got the spec to run with no errors (yay!) however, whenever I start to believe I'm starting to understand TLA+...I get errors for which I don't understand.

Today's Error is that my MTypeInv is violated by my init formula (MInit). But no matter how I switch it around, it keeps giving the same error leading me to believe I simply don't understand what's happening. Much of the spec below is pieced together from some of the examples in the book, so I'm still not 100% confident with them. Meaning I don't believe I could write them without some aid to look at. Its unclear when I should put something in  [ ]  and when its not needed i.e.  \A, \E  . I believe   [ ]  to be a function which operates on a Set (its domain) or an element of that set? But I keep getting errors when I believe this to be true or I just don't know how to write that properly without using others specs as a template.

Below is my spec (which runs fine with no errors from TLC) and all the versions of my MTypeInv (below the dashed line) that keep giving me the same error. I've added comments throughout at the bottom.

 ------------------------------- MODULE motion -------------------------------
CONSTANT M

VARIABLE mState, movant, respondent

MTypeOK ==
  /\ mState \in [M -> {"motion", "response", "reply", "surreply", "hearing", "granted", "denied", "ruling"}]
  /\ movant \in {"idle", "active"}
  /\ respondent \in {"idle", "active"}
 
 
 
MInit ==
  /\ mState = [m \in M |-> "motion"]
  /\ movant = "active"
  /\ respondent = "idle"
 
MotionResponse(m) ==
  /\ mState[m] = "motion"
  /\ mState' = [mState EXCEPT ![m] = "response"]
  /\ movant' = "idle"
  /\ respondent' = "active"
 

ResponseReply(m) ==
  /\ mState[m] = "response"
  /\ mState' = [mState EXCEPT ![m] = "reply"]
  /\ movant' = "active"
  /\ respondent' = "idle"

SurReply(m) ==
  /\ mState[m] = "reply"
  /\ mState' = [mState EXCEPT ![m] = "surreply"]
  /\ movant' = "active"
  /\ respondent' = "idle"

Hearing(m) ==
  /\ mState[m] \in {"motion", "response", "reply", "surreply"}
  /\ mState' = [mState EXCEPT ![m] = "hearing"]
  /\ movant' = "idle"
  /\ UNCHANGED respondent

MotionRuling(m) ==
  /\ mState[m] \in {"motion", "response", "reply", "surreply", "hearing"}
  /\ mState' = [mState EXCEPT ![m] = "ruling"]
  /\ movant' = "idle"
  /\ respondent' = "idle"

MNext == \E m \in M : MotionResponse(m)
  \/ ResponseReply(m)
  \/ SurReply(m)
  \/ Hearing(m)
  \/ MotionRuling(m)
  \*\/ UNCHANGED <<mState>>
 
-----------------------------------------------------------------------------

What I'm trying to check is that:

  \/ /\ while mState is either "motion" or "reply"

     /\ movant is not "idle"

     /\ respondent is not "active"

  \/ /\ while mState is either "response" or "surreply"

     /\ movant is not "active"

     /\ respondent is not "idle"

This is similar to the Asynchronous Interface in Chapter 3 of Specifying Systems (my template). "idle" and "active" could easily be replaced with {0,1} but either way I just don't know how to even write the equivalent of my pseudo code in TLA without errors. Therefore I have to attempt to write it out a separate functions/formula??? and combine them with a conjunction /\. I can't even get that to work all the time, though this spec has no parsing errors.

After attempting to run TLC, I continually get the below error which, should not be an error because its suppose to be in that state. The opposite is not suppose to happen at this step. Even if I change around movant and respondent states, I get the same error:

Invariant NewTypeOK is violated by the initial state:
/\ mState = [m1 |-> "motion"]
/\ respondent = "idle"
/\ movant = "active"

The only conclusion is that there is an error in my thinking of how I believe TLA to work.

After breaking down the formula (not even sure that's the right word anymore) in parts I can get parts to work, like the one immediately following this comment.

bothNotActive ==
\A m1 \in M : ~ /\ movant = "active"
                /\ respondent = "active"
 

             
movantIdle ==
  /\ movant = "idle"
  /\ respondent = "active"
 
respondentIdle ==
  /\ movant = "active"
  /\ respondent = "idle"
 
MTypeInv ==
  /\ bothNotActive
  /\ movantIdle
  /\ mState = "motion"

NewTypeOK ==
  /\ ~movant = "active"
  /\ ~respondent = "idle"
  /\ \A m \in M : mState \in [M -> {"response", "surreply"}]

I also tried the above with the  ~  on the outside as mentioned below.

This was another definition I tried but I didn't work either. There was the definition in front. Just commenting things out
 (* \/ /\ mState = "response"
    \/ /\ mState = "surreply"
       /\ movant = "active"
       /\ respondent = "idle" *)

I tried adding the For All (statement/function/formula???) to the end but I keep getting the same error. I also don't understand how the  ~  works. If its on the outside of the  /\  list then it seems to apply to all of the list vs in front of the variable
  (* ~ /\ movant = "idle"
       /\ respondent = "active"
       /\ \A m1 \in M : \/ /\ mState[m1] = "motion"
                      \/ /\ mState[m1] = "surreply"*)

=================================================================================           

[Stephan Merz]

Hello,

What I'm trying to check is that:

  \/ /\ while mState is either "motion" or "reply"

     /\ movant is not "idle"

     /\ respondent is not "active"

  \/ /\ while mState is either "response" or "surreply"

     /\ movant is not "active"

     /\ respondent is not "idle"

I'm assuming that your constant set M contains not just one element, otherwise the representation of mState as a function would be wasteful. But then, the above is ambiguous: do you mean that mState[m] is either "motion" or "reply" *for some m \in M* or that it has one of these values *for all m \in M*? (Of course, more intricate readings such as "for a majority of the elements of M" are also possible, but I'll ignore them here.)

Along the same lines, a definition such as

bothNotActive ==
\A m1 \in M : ~ /\ movant = "active"
                /\ respondent = "active"

is strange since the bound variable m1 doesn't appear in the body, and indeed there is no reason why it should as long as the body only refers to `movant' and `respondent', which are not functions but just take scalar values.

Assuming the conditions in the informal statement are intended existentially ("there exists ..."), the invariant can be written as

\/ /\ \E m \in M : mState[m] \in {"motion", "reply"}

   /\ movant # "idle"    \* "#" is the ASCII representation of "not equal"

   /\ respondent # "active"

\/ /\ \E m \in M : mState[m] \in {"response", "surreply"}

   /\ movant # "active"
   /\ respondent # "idle"

Informally, this predicate asserts that the system that you are specifying can be in one of two classes of states (separated by "\/"). In the first class, some m \in M is in state "motion" or "reply" and (/\) the conditions expressed in the two following lines hold. The second class is described similarly.

Considering your invariant definition

NewTypeOK == 
  /\ ~movant = "active"
  /\ ~respondent = "idle"
  /\ \A m \in M : mState \in [M -> {"response", "surreply"}]

this is clearly not satisfied by the initial states of your system (as TLC tells you) because the initial condition implies

(i) mState[m] = "motion" for all m \in M  ... so it is not "response" or "surreply"

(ii) movant = "active"   ... so it is not different from "active"

(iii) respondent = "idle"   ... so it is not different from "idle"

In fact, each of the conjuncts of the claimed invariant is violated in the initial state, showing that there is some real misunderstanding of logical formulas or of the meaning of invariants.

I have not tried to understand your spec and guess what your actual invariant might be.

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+u...@googlegroups.com.
To post to this group, send email to tla...@googlegroups.com.
Visit this group at https://groups.google.com/group/tlaplus.
For more options, visit https://groups.google.com/d/optout.

[Curt Flowers]

I'm assuming that your constant set M contains not just one element...

Correct.
...[M -> {"motion", "response", "reply", "surreply", "hearing", "granted", "denied", "ruling"}]

mState[m] is either "motion" or "reply" *

Yes, this is what I'm trying to say. When the state of a motion (m) is in either "motion" or "reply" then movant should = "active" (not not be "idle"). I tried that and I got an error saying that my  function requires 1 arg, which confused me. But I digress.

...is strange since the bound variable m1 doesn't appear in the body...

This is one of the "templates" I was talking about before. This is from TCConsistent.

TCConsistent == 
  \A rm1, rm2 \in RM : ~ /\ rmState[rm1] = "aborted"
                                      /\ rmState[rm2] = "committed"

I understand what the formula/function is saying. My formula doesn't use two different sets, so m1 and m2 would not be relevant. Each motion stands alone is not compared to each other like resource managers (RM) of TCommit. It was an experiment as I test out my understanding (or lack there of) hoping to stumble upon a correct answer and the glean why it did work and what I did wrong. While that has happened a few times, this time it did not.

...showing that there is some real misunderstanding of logical formulas...

An invariant is true in every reachable state. If that's not the meaning then I also don't understand that. I thought/think I understood logical formulas, but that's also why I'm here. I'm unsure its the understanding or the writing of logical formulas (like any other language. Understanding is not the same as speaking it).

the invariant can be written as...

Reading your version, I can see the error in my understanding of how to write TLA, but your formula makes sense to me. However, I still got the same error. One thing I'm sure of is how to read these error statements. I know this is a "better" error (Error-Trace) than the one I was getting it's still the same error.

[Stephan Merz]

...is strange since the bound variable m1 doesn't appear in the body...

This is one of the "templates" I was talking about before. This is from TCConsistent.

TCConsistent == 
  \A rm1, rm2 \in RM : ~ /\ rmState[rm1] = "aborted"
                                      /\ rmState[rm2] = "committed"

I understand what the formula/function is saying. My formula doesn't use two different sets, so m1 and m2 would not be relevant. Each motion stands alone is not compared to each other like resource managers (RM) of TCommit. It was an experiment as I test out my understanding (or lack there of) hoping to stumble upon a correct answer and the glean why it did work and what I did wrong. While that has happened a few times, this time it did not.

TCConsistent is not using two sets but one set RM. It says that the states of any two *elements* rm1 and rm2 of that set must agree in the sense that it cannot be the case that one has decided to abort (is in state "aborted") whereas the other one has decided to commit (is in state "committed"). This is a different pattern than your assertion, which links the state of a single motion (an element of set M) with states of movant / respondent (that are not elements of M). At any rate, a formula

  \A x \in S : P     or     \E x \in S : P

where P does not contain x is just equivalent to P, assuming that S is non-empty (if S is empty then the \A formula is equivalent to TRUE and the \E formula is equivalent to FALSE).

the invariant can be written as...

Reading your version, I can see the error in my understanding of how to write TLA, but your formula makes sense to me. However, I still got the same error. One thing I'm sure of is how to read these error statements. I know this is a "better" error (Error-Trace) than the one I was getting it's still the same error.

OK, the invariant suggested in the previous message asserted that the system can be in one of two classes of states: one in which some m is in state "motion" or "reply" and some conditions hold, and one in which some m is in state "response" or "surreply" and certain conditions hold. But now TLC shows you that there exist states that are not covered by these two classes, namely a state where (the only) m is in state "hearing". For your invariant to be true at all states of the execution, these states must be covered by the invariant, presumably by adding a disjunct

\/ ...

\/ ...

\/ /\ \E m \in M : mState[m] = "hearing"

   /\ ... \* whatever conditions you expect to hold for the other variables

Figuring out invariants can be quite hard when you aren't used to this way of thinking about your system, but they structure your thinking about the system.

Did you try what happens if set M contains more than one element? I'd expect you to see new counter-examples.

Regards,

Stephan

[Curt Flowers]

I still can't get this to work. I've tried everything. I keep getting an error saying mState is undefined or not an operator with the:

\E m \in M : mState[m] = "anything state here"

Went back to HyperBook and looked at the Math section. Everything lines up. I used the examples as templates that I modified to make sense with my spec (of course that is questionable at this point).

However, after talking with you I did redesign the spec as I noticed I didn't have enough states. There needed to an idle period (both movant and respondent "idle") after each state.

Still...with all my effort, I've emerged empty handed. I've been working on this all day. I can get BothNotActiveInv to work just fine but anything that mention mState or M doesn't work.

I did use the "Evaluate Constant Expression" section and found that if I put:

m \in M # "any state here" it came back TRUE (and if = to any state, FALSE).

That is the closet I got to something working. So it recognizes m \in M but on with any elements of the set of M.

[Stephan Merz]

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?*)
     /\ 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 <curty...@gmail.com> 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+u...@googlegroups.com.
To post to this group, send email to tla...@googlegroups.com.
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>

[Curt Flowers]

Stephan, as usual, thank you for your reply. Funny enough you have already helped me without saying a word. After 3 days of getting stuck, I sent my last post. Then after about 24 hours of no response, I went back and looked at your original response to my first spec and decided to start from scratch. I opened up the hyperbook, specifying systems, learntla.com and your original thorough response to me. The follow working spec (yay!) is what I came up with after 3 days.

You made a comment about using the wrong pattern and that was the light bulb moment when I decided to start over again and realized why I was struggling so much.

I'm working an v3 of the spec as there are too many variables and in Specifying Systems, Lamport converts the asyn spec to chan to make it easier to use within other specs. This is what I'm trying to do now. Thus far I've identified the the following as being related, but still wondering if I could combine them more:

Extension of service

ext \in [days: Nat, deadline: ED, granted: BOOLEAN, request: BOOLEAN]

Defendant
def \in [type: D, jurisdiction: J, service: PS]

Summons

sum \in [waiver: W, summons: S, days: Nat]

The only variable left is cState (the case itself). If you (or anyone) have any suggestions, that would great. I'm going to go through your last reply and see what else I can glean. Again, thank you for responding. I was thinking for a second that I've been forsaken in the forum :D

------------------------------ MODULE summons2 ------------------------------
EXTENDS Naturals 
       
  (***********************************************************************)
  (* To avoid the proliferation of variables, once working properly      *)
  (* convert the extState, extDays and reqExt into a record. Converting  *)
  (* other variables would also make the spec cleaner and more simple.   *)
  (* The numbers in the comments represent what should go together.      *)
  (***********************************************************************)
VARIABLE cState,      \* state of the case to have a clear end of the process
         days,        \* elapsed days
         dState,      \* state of defendant
         extDays,     \*1 if an extention is granted, the amount of days before the case will close if a defendant isn't servered
         extDeadline, \*1 how many days the judge granted to complete service
         extState,    \*1 state of service extention. Simulates random choice of the extention be granted or denied with a motion
         jState,      \* state of jurisdiction
         sState,      \* state of the summons process
         wState,      \* state of the waiver process
         psState,     \* type of process server used
         reqExt       \*1 selects randomly if the user wants an extention of service (a state of the summons process)
        
-----------------------------------------------------------------------------
  (***********************************************************************)
  (*           Set definitions to make the spec cleaner                  *)
  (*           and avoid unnecessary use of CONSTANTS                    *)
  (***********************************************************************)
C ==                     \* while there are more states, they are not relevant in this spec
  {"open","pleadings", "withdrawn", "dismissed"}

D ==                     \* type of defendant

  {"corporation", "foreignCorporation", "individual",

   "foreignIndividual", "incompententIndividual", "minorIndividual",

   "unincorporatedAssocation", "partnership", "US", "USOfficer",
   "localGov", "stateGov", "foreignGov", "USEmployee", "USAgency",
   "USCorporation", "USOfficerIndividual", "USEmployeeIndividual"}
  

ED ==                    \* extention deadline
  {30, 60, 90}           \* alloted days by a judge to server the defendant before the case will be dismissed
J ==                     \* withhin or outside the jurisdiction of the US
  {"within", "outside"}
 
PS ==                    \* Because the process is not specified on how these servers are picked, its too detailed use them all
  {"notAssigned",        \* the court doesn't assign a processServer until the summons needs to be servered
   "processServer",      \* processServer will represent any type of processServer for the spec
   "foreignServer"}      \* for processes in other countries 
  
   \* TODO: figure out if TLA can pick a random element within a set?
      
S ==
  {"summonsNotStarted",  \* the time before any action taken
   "served",             \* party servered
   "pendingService",     \* out for service (120 days)
   "waivedService",      \* service was waived
   "extendedService",    \* 2nd attempt after process server time elapsed/failed
   "failedService"}      \* time for service has elapsed/failed

W ==
   {"waiverSkipped",     \* skipped the waiver process
    "waiverNotStarted",  \* time before waiver action taken
    "waiverNotReceived", \* no response recived or rejected without "good cause"
    "waiverAccepted",    \* party accepted waiver of service and filed with the court
    "waiverPending"}     \* notice of waiver sent to party
   
vars ==                  \* represent all variables
  {cState, days, dState, extDays, extDeadline, extState, jState, sState, wState, psState,reqExt}

-----------------------------------------------------------------------------
  (***********************************************************************)
  (*                  Type correctness of variables                      *)
  (***********************************************************************)
sTypeOK ==
  /\ cState \in C           \* state of case
  /\ days \in Nat           \* Rule 4(m) Time limit for service is 120 days
  /\ dState \in D           \* type of Defendants      
  /\ extDays \in Nat        \* days elapsed from start. Will eliminate when converted to records
  /\ extDeadline \in ED     \* extension days. 30, 60 or 90 days would likely be standard
  /\ extState \in BOOLEAN   \* REPORT BUG: BOOLEAN keyword doesn't highlight
  /\ jState \in J           \* jurisdiction of defendant
  /\ psState \in PS         \* type of process Server
  /\ reqExt \in BOOLEAN     \* did plaintiff request an extension
  /\ sState \in S           \* state of the summons           
  /\ wState \in W           \* state of the waiver of service process
 
waiverSummonsInv ==         \* can't serve a defendant who filed a waiver
  ~/\ sState = "served"     \*??? when is it too late to accept a waiver
   /\ wState = "waiverAccepted"
  
caseDismissedInv ==         \* case can't be dismissed and started. This and the above are very similar. REWRITE
  ~\/ /\ cState ="dismissed"
      /\ sState = "served"
   \/ /\ cState ="dismissed"
      /\ wState = "waiverAccepted"
     

-----------------------------------------------------------------------------
  (***********************************************************************)
  (*   Spec for the summons process in the US for serving a lawsuit.   *)
  (***********************************************************************)
 
sInit ==
  /\ cState = "open"
  /\ days = 0
  /\ dState \in D
  /\ extDays = 0
  /\ extDeadline \in ED
  /\ extState \in {TRUE, FALSE}
  /\ jState \in J
  /\ psState = "notAssigned"
  /\ reqExt \in BOOLEAN
  /\ sState = "summonsNotStarted"
  /\ wState \in {"waiverNotStarted", "waiverSkipped"}

  (***********************************************************************)
  (*       Waiver process before servering a summons on defendants       *)
  (***********************************************************************)

wSent ==
  /\ cState = "open"
  /\ days \in Nat \* why doesn't {0..121} work and Nat does???
  /\ dState \in {"corporation", "foreignCorporation", "individual", "foreignIndividual", "unincorporatedAssocation", "partnership"} \* do i need to make a subset for this or US aka notUS
  /\ extDays = 0
  /\ extDeadline \in ED
  /\ extState \in BOOLEAN
  /\ jState \in J \* check Rule 4(l) on what is defendant is outside the J of the US. corps and other entities are definitely within that.
  /\ psState = "notAssigned"
  /\ reqExt \in BOOLEAN
  /\ sState = "summonsNotStarted"
  /\ wState = "waiverNotStarted"
 
  /\ days' = days + 1
  /\ wState' = "waiverPending"
  /\ UNCHANGED <<cState, dState, extDays, extDeadline, extState, jState, psState, reqExt, sState>>

wPending ==
  /\ cState = "open"
  /\ IF jState = "within"
     THEN days =< 30
     ELSE IF jState = "outside"
          THEN days =< 60
          ELSE days \in Nat
  /\ dState \in {"corporation", "foreignCorporation", "individual", "foreignIndividual", "unincorporatedAssocation", "partnership"}
  /\ extDays = 0
  /\ extDeadline \in ED
  /\ extState \in BOOLEAN
  /\ jState \in J
  /\ psState = "notAssigned"
  /\ reqExt \in BOOLEAN
  /\ sState = "summonsNotStarted"
  /\ wState = "waiverPending"
 
  /\ days' = days + 1
  /\ UNCHANGED <<cState, dState, extDays, extDeadline, extState, jState, psState, reqExt, sState, wState>>

wAccepted ==
  /\ cState = "open"
  /\ days \in Nat
  /\ dState \in {"corporation", "foreignCorporation", "individual", "foreignIndividual", "unincorporatedAssocation", "partnership"}
  /\ extDays = 0
  /\ extDeadline \in ED
  /\ extState \in BOOLEAN
  /\ jState \in J
  /\ psState \in PS
  /\ reqExt \in BOOLEAN
  /\ sState \notin {"served", "waivedService"}
  /\ wState \in {"waiverPending", "waiverNotReceived"}
 
  \*/\ cState' = "pleadings"
  /\ days' = days + 1 \* may need to skip days++ or do after deadline check
  /\ sState' = "waivedService"
  /\ wState' = "waiverAccepted"
  /\ UNCHANGED <<cState, dState, extDays, extDeadline, extState, jState, psState, reqExt>>
 
wRejected ==
  /\ cState \notin {"dismissed", "withdrawn"}
  /\ IF jState = "within"
     THEN days > 30
     ELSE IF jState = "outside"
          THEN days > 60
          ELSE days \in Nat
  /\ dState \in {"corporation", "foreignCorporation", "individual", "foreignIndividual", "unincorporatedAssocation", "partnership"}
  /\ extDays = 0
  /\ extDeadline \in ED
  /\ extState \in BOOLEAN
  /\ jState \in J
  /\ psState = "notAssigned"
  /\ reqExt \in BOOLEAN
  /\ sState = "summonsNotStarted"
  /\ wState = "waiverPending"

  /\ days' = days + 1
  /\ wState' = IF /\ jState = "within"
                  /\ days > 30
               THEN  "waiverNotReceived"
               ELSE IF /\ jState = "outside"
                       /\ days > 60
                    THEN "waiverNotReceived"
                    ELSE "waiverNotReceived"
  /\ UNCHANGED <<cState, dState, extDays, extDeadline, extState, jState, psState, reqExt, sState>>
 
  (***********************************************************************)
  (*                The summons process during a lawsuit                 *)
  (***********************************************************************)
 
sSent ==
  /\ cState = "open"
  /\ days \in Nat
  /\ IF jState = "within"
     THEN dState \notin {"foreignIndividual", "foreignGov"}
     ELSE IF jState = "outside"
          THEN dState \in {"foreignIndividual", "foreignGov"}
          ELSE dState \in D
  /\ extDays = 0
  /\ extDeadline \in ED
  /\ extState \in BOOLEAN
  /\ jState \in J
  /\ psState = "notAssigned"
  /\ reqExt \in BOOLEAN
  /\ sState = "summonsNotStarted"
  /\ wState \in {"waiverNotReceived", "waiverSkipped"}
 
  /\ sState' = "pendingService"
  /\ days' = days + 1
  /\ IF jState = "within"
     THEN psState' = "processServer"
     ELSE IF jState = "outside"
          THEN psState' = "foreignServer"
          ELSE psState = "notAssigned"
  /\ UNCHANGED <<cState, dState, extDays, extDeadline, extState, jState, reqExt, wState>>

sPending ==
  /\ cState = "open"
  /\ IF jState = "within"
     THEN days =< 120
     ELSE IF jState = "outside"
          THEN days =< 180  \* there is no stated limit to the time when dealing with foreign actors
          ELSE days \in Nat \* why doesn't {0..121} work and Nat does???
  /\ dState \in D
  /\ extDays = 0
  /\ extDeadline \in ED
  /\ extState \in BOOLEAN
  /\ jState \in J
  /\ psState # "notAssigned"
  /\ reqExt \in BOOLEAN
  /\ sState \in {"pendingService", "extendedService"}
  /\ wState = "waiverNotReceived"
 
  /\ days' = days + 1
  /\ UNCHANGED <<cState, dState, extDays, extDeadline, extState, jState, psState, reqExt, sState, wState>>
 
\* TODO: add served after sExtention as disjunction or new definition
served ==
  /\ cState = "open"
  /\ IF jState = "within"              \* days within service time limit
     THEN days =< 120
     ELSE IF jState = "outside"
          THEN days =< 180
          ELSE days \in Nat
  /\ dState \in D
  /\ extDays = 0
  /\ extDeadline \in ED
  /\ extState \in BOOLEAN
  /\ jState \in J
  /\ psState # "notAssigned"
  /\ reqExt \in BOOLEAN
  /\ sState \in {"pendingService", "extendedService"}
  /\ wState = "waiverNotReceived"

  /\ cState' = "pleadings"
  /\ sState' = "served"
  /\ UNCHANGED << days, dState, extDays, extDeadline, extState, jState, psState, reqExt, wState>>
 
sFailure ==
  /\ cState = "open"
  /\ IF jState = "within"              \* days to serve have elapsed
     THEN days > 120
     ELSE IF jState = "outside"
          THEN days > 180
          ELSE days \in Nat
  /\ dState \in D \* IF/THEN/ELSE for foreign entities
  /\ extDays = 0
  /\ extDeadline \in ED
  /\ extState = FALSE
  /\ jState \in J
  /\ psState # "notAssigned"
  /\ reqExt \in BOOLEAN
  /\ sState = "pendingService"
  /\ wState = "waiverNotReceived"

  /\ cState' = "dismissed"
  /\ sState' = "failedService"
  /\ UNCHANGED << days, dState, extDays, extDeadline, extState, jState, psState, reqExt, wState>>

  (***********************************************************************)
  (*                    Extension of service process                     *)
  (***********************************************************************)

sExtension ==
  /\ cState = "open"
  /\ IF jState = "within"
     THEN days > 120
     ELSE IF jState = "outside"
          THEN days > 180
          ELSE days \in Nat
  /\ dState \in D
  /\ extDays = 0
  /\ extDeadline \in ED
  /\ extState = TRUE
  /\ jState \in J
  /\ psState # "notAssigned"
  /\ reqExt = TRUE
  /\ sState = "pendingService"
  /\ wState = "waiverNotReceived"

  /\ days' = days + 1
  /\ extDays' = extDays + 1
  /\ sState' = "extendedService"
  /\ UNCHANGED <<cState, dState, extDeadline, extState, jState, psState, reqExt, wState>>

extPending ==
  /\ cState = "open"
  /\ IF jState = "within"
     THEN days > 120
     ELSE IF jState = "outside"
          THEN days > 180
          ELSE days \in Nat
  /\ dState \in D
  /\ extDays =< extDeadline
  /\ extDeadline \in ED
  /\ extState = TRUE
  /\ jState \in J
  /\ psState # "notAssigned"
  /\ reqExt = TRUE
  /\ sState = "extendedService"
  /\ wState = "waiverNotReceived"
 
  /\ days' = days + 1
  /\ extDays' = extDays + 1
  /\ UNCHANGED <<cState, dState, extDeadline, extState, jState, psState, reqExt, sState, wState>>
 
extFailure ==
  /\ cState = "open"
  /\ IF jState = "within"              \* days to serve have elapsed
     THEN days > 120
     ELSE IF jState = "outside"
          THEN days > 180
          ELSE days \in Nat
  /\ dState \in D
  /\ extDays > extDeadline
  /\ extDeadline \in ED
  /\ extState = TRUE
  /\ jState \in J
  /\ psState # "notAssigned"
  /\ reqExt = TRUE
  /\ sState = "extendedService"
  /\ wState = "waiverNotReceived"

  /\ cState' = "dismissed"
  /\ sState' = "failedService"
  /\ UNCHANGED << days, dState, extDays, extDeadline, extState, jState, psState, reqExt, wState>>

  (***********************************************************************)
  (*      Getting the case dismissed or withdrawing from the case        *)
  (***********************************************************************)
 
caseDismissed ==                       \* rule4m
  /\ cState = "open"
  /\ IF jState = "within"              \* days to serve have elapsed
     THEN days > 120
     ELSE IF jState = "outside"
          THEN days > 180
          ELSE days \in Nat
  /\ dState \in D
  /\ extDays > extDeadline \/ extDays = 0
  /\ extDeadline \in ED
  /\ extState \in BOOLEAN
  /\ jState \in J
  /\ psState # "notAssigned"
  /\ reqExt \in BOOLEAN
  /\ sState \notin {"waivedService", "served"}
  /\ wState = "waiverNotReceived"
 
  /\ cState' = "dismissed"
  /\ sState' = "failedService"
  /\ UNCHANGED << days, dState, extDays, extDeadline, extState, jState, psState, reqExt, wState>>
 
caseWithdrawn ==
  /\ cState \in {"open", "pleadings"}
  /\ days \in Nat
  /\ dState \in D
  /\ extDays \in Nat
  /\ extDeadline \in ED
  /\ extState \in BOOLEAN
  /\ jState \in J
  /\ psState \in PS
  /\ reqExt \in BOOLEAN
  /\ sState \in S
  /\ wState \in W
 
  /\ cState' = "withdrawn"
  /\ UNCHANGED << days, dState, extDays, extDeadline, extState, jState, psState, reqExt, sState, wState>>

(********************************************************************************) 
(*there needs to be a transition from failed waiver to start the summons process*)
(********************************************************************************)
 
waiverProcess ==
  \/ wPending
  \/ wAccepted
  \/ wRejected
  \/ wSent

summonsProcess ==
  \/ sSent
  \/ sPending
  \/ served
  \/ sFailure
  \/ sExtention
  \/ extPending
  \/ extFailure
  \/ caseWithdrawn
  \/ caseDismissed

sNext ==
  \/ waiverProcess
  \/ summonsProcess

-----------------------------------------------------------------------------
summonsSpec == sInit /\ [][sNext]_vars
=============================================================================