[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

Re: [tlaplus] Fumbling Through TLA+



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


On 13 Feb 2019, at 17:02, Curt Flowers <curtycurt01@xxxxxxxxx> wrote:

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 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.

--
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.