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.
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, juris: 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
\*CONSTANT D \* Rule 4(b) states that all defendants must be serverd to start the case
(***********************************************************************)
(* 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 ==
{"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
(* Kept here to reference later for future specs: {"USMarshal","deputyMarshal","appointed"} *)
\* 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 \* extention days. 30, 60 or 90 days would likely be standard
/\ extState \in BOOLEAN \* REPORT: BOOLEAN keyword doesn't highlight
/\ jState \in J \* jurisdiction of defendant
/\ psState \in PS \* type of process Server
/\ reqExt \in BOOLEAN \* did plantiff request an extention
/\ 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 servering 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>>
(***********************************************************************)
(* Extention of service process *)
(***********************************************************************)
sExtention ==
/\ 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 \* IF/THEN/ELSE for foreign entities
/\ 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 \* IF/THEN/ELSE for foreign entities
/\ 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
=============================================================================