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"*)
=================================================================================
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
.
.
.