For your second problem, the error is in the _expression_:
\A i \in {1..Len(rcvd)}: sent[i] = rcvd[i]
which, when rcvd = << >>, is equivalent to
I presume you somehow made an error when copying your spec and the /\ in the definition of NextFIFO should be a \/ , otherwise I believe your spec should have deadlocked in the initial state.
For your first problem, it should take TLC ages because your spec has an infinite number of reachable states. If you were checking that TypeOK is an invariant, it would eventually produce an invariant-violated error. You seem to be under the impression that the definition of TypeOK somehow constrains the set of reachable states. Since it doesn't appear anywhere in the your spec, which I presume is formula SpecFIFO, it obviously has no effect on the spec's possible behaviors. (The key to understanding TLA+ is to learn to read what the math says, rather than what you want it to say.) TLC would have no trouble evaluating the _expression_ TypeOK if you replaced the occurrences of BoundedSeq with Seq.
You can model check your spec by letting it run forever, and stopping TLC when you get bored. (If you are checking an invariant that isn't one, TLC will eventually discover the error.) Or, you can use a state constraint. Go to the Advanced Options page of your model and click on Help > Dynamic Help > Advanced Options Page to find out how.
Leslie
I'm trying to create a FIFO channel in a different way than the one in "Speciying Systems". However, I am unexperienced with TLA+ and I'm getting some errors.
I have tried to use a Sequence to specify the sent, received, lost, and data on transit. This should allow me to specify the corresponding behaviors for duplication and lost messages. However, I get the following error "Attempted to apply tuple to a non-integer argument".
It seems that this is because TLC can not check infinite sets like: ch \in Seq(Messages)
So, I tried to use a BoundedSeq as defined in another thread:
BoundedSeq(Data, n) == UNION{[x -> Data]: x \in {1..y : y \in 0..n}}
The problem then is two fold:
1) The TLC takes ages with small n and Data size (10 and 2, respectively). ?
2) I get another error:
Attempted to apply function:
<< >>
to argument {}, which is not in the domain of the function.
While working on the initial state:
/\ ch = << >>
/\ sent = << >>
/\ rcvd = << >>
/\ lost = << >>
So, I wonder how should I approach the problem.
Thanks,
marc
PS: Spec below:
------------------------------ MODULE Channel ------------------------------
EXTENDS Sequences, Integers
CONSTANTS Messages, MAX_SENT
VARIABLE ch, lost, sent, rcvd
----------------------------------------------------------------------------
BoundedSeq(Data, n) == UNION{[x -> Data]: x \in {1..y : y \in 0..n}}
\* I can not use Seq(Messages) because the TLC can not check infinite sets
TypeOK == /\ ch \in BoundedSeq(Messages,MAX_SENT)
/\ sent \in BoundedSeq(Messages,MAX_SENT)
/\ rcvd \in BoundedSeq(Messages,MAX_SENT)
/\ lost \in BoundedSeq(Messages,MAX_SENT)
Init == /\ ch = << >>
/\ sent = << >>
/\ rcvd = << >>
/\ lost = << >>
Send(d) == /\ ch' = Append(ch,d)
/\ sent' = Append(sent,d)
/\ UNCHANGED <<rcvd,lost>>
Receive == /\ Len(ch) > 0
/\ ch' = Tail(ch)
/\ rcvd' = Append(rcvd,Head(ch))
/\ UNCHANGED <<sent,lost>>
----------------------------------------------------------------------------
\* FIFO specification
InvariantFIFO == /\ Len(sent) >= Len(rcvd)
/\ \A i \in {1..Len(rcvd)}: sent[i] = rcvd[i]
NextFIFO == (\E d \in Messages: Send(d)) /\ Receive
SpecFIFO == (Init /\ [][NextFIFO]_<<ch,sent,rcvd,lost>>)
--
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...@xxxxxxxxxxxxxxxx.
To post to this group, send email to tla...@xxxxxxxxxxxxxxxx.
Visit this group at http://groups.google.com/group/tlaplus?hl=en.
For more options, visit https://groups.google.com/groups/opt_out.