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

*From*: Curt Flowers <curtycurt01@xxxxxxxxx>*Date*: Wed, 13 Feb 2019 09:17:21 -0800 (PST)*References*: <bd0c4d46-753e-4cfa-8c70-bac91a52b3fd@googlegroups.com> <1287F129-1A1A-4E50-BDC2-A3B60514D446@gmail.com>

Correct**. **

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

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

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.

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"

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

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

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.

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.

**Follow-Ups**:**Re: [tlaplus] Fumbling Through TLA+***From:*Stephan Merz

**References**:**[tlaplus] Fumbling Through TLA+***From:*Curt Flowers

**Re: [tlaplus] Fumbling Through TLA+***From:*Stephan Merz

- Prev by Date:
**Re: [tlaplus] Fumbling Through TLA+** - Next by Date:
**Re: [tlaplus] Fumbling Through TLA+** - Previous by thread:
**Re: [tlaplus] Fumbling Through TLA+** - Next by thread:
**Re: [tlaplus] Fumbling Through TLA+** - Index(es):