Can not edit "What is the model" and "What is the behavior spec?"
Chen Fu
I am new to TLA plus and was writing my first spec (end of email). When I tried to create a new model, and navigate to the "Model Overview" page, I can not do anything. The radio button "Initial predicate and next-state relation" is grey and I can not click. The edit box under "What is the model" does not accept any input.
I am using newly downloaded TLAToolbox-1.4.8-win32.win32.x86_64.zip from http://research.microsoft.com/en-us/um/people/lamport/tla/tools.html.
the machines runs Windows server 2012, Java version 1.8 x64
below are the spec (PlusCal with translation)
======================================================================
EXTENDS Integers
CONSTANT PckCount
ASSUME PckCount \in Nat \ {0}
Remove(i, seq) == [ j \in 1..(Len(seq) - 1) |-> IF j < i THEN seq[j] ELSE seq[j+1]]
(******************************************************************************
--algorithm ExaUdpProtocol
{
\* msgC channel Sender -> Receiver
\* ackC channel Receiver -> Receiver
\* output contains received packets
\* each packet is represented by its sequence number, i.e. an integer
variables output = <<>>; msgC = <<>>; ackC = <<>>;
macro Send(m, chan) {
chan := Append(chan, m)
}
\* Receive can get packet in the middle of the channel
\* to simulate packet arriving out of order
macro Rcv(v, chan) {
with ( i \in 1..Len(chan))
{
v := chan[i];
chan := Remove(i, chan);
}
}
process (Sender = "S")
variables toSend = 0; ack = 0;
{
s: while (TRUE) {
either {
await toSend < PckCount ;
\* send two packets before checking for ack
with ( msg \in { x \in toSend..(toSend+1) : x < PckCount })
{
Send(msg, msgC);
}
}
or {
Rcv(ack, ackC);
\* if ack received, send next two packets
if (ack = toSend + 2) {
toSend := toSend + 2;
}
}
}
}
process (Receiver = "R")
variables next = 0; msg = 0;
{
r: while (TRUE) {
either {
\* only send ack every other packets
await (next % 2 = 0) { Send(next, ackC) }
}
or {
Rcv(msg, msgC);
if (msg = next) {
next := next + 1 ;
output := Append(output, msg)
}
}
}
}
process (LoseMsg = "L")
{
\* Simulate loss of packet over network
l: while (TRUE) {
either with ( i \in 1..Len(msgC)) { msgC := Remove(i, msgC) }
or with ( i \in 1..Len(ackC)) { ackC := Remove(i, ackC) }
}
}
}
******************************************************************************)
\* BEGIN TRANSLATION
VARIABLES output, msgC, ackC, toSend, ack, next, msg
vars == << output, msgC, ackC, toSend, ack, next, msg >>
ProcSet == {"S"} \cup {"R"} \cup {"L"}
Init == (* Global variables *)
/\ output = <<>>
/\ msgC = <<>>
/\ ackC = <<>>
(* Process Sender *)
/\ toSend = 0
/\ ack = 0
(* Process Receiver *)
/\ next = 0
/\ msg = 0
Sender == /\ \/ /\ toSend < PckCount
/\ \E msg \in { x \in toSend..(toSend+1) : x < PckCount }:
msgC' = Append(msgC, msg)
/\ UNCHANGED <<ackC, toSend, ack>>
\/ /\ \E i \in 1..Len(ackC):
/\ ack' = ackC[i]
/\ ackC' = Remove(i, ackC)
/\ IF ack' = toSend + 2
THEN /\ toSend' = toSend + 2
ELSE /\ TRUE
/\ UNCHANGED toSend
/\ msgC' = msgC
/\ UNCHANGED << output, next, msg >>
Receiver == /\ \/ /\ (next % 2 = 0) { Send(next, ackC) }
/\ UNCHANGED <<output, msgC, next, msg>>
\/ /\ \E i \in 1..Len(msgC):
/\ msg' = msgC[i]
/\ msgC' = Remove(i, msgC)
/\ IF msg' = next
THEN /\ next' = next + 1
/\ output' = Append(output, msg')
ELSE /\ TRUE
/\ UNCHANGED << output, next >>
/\ UNCHANGED << ackC, toSend, ack >>
LoseMsg == /\ \/ /\ \E i \in 1..Len(msgC):
msgC' = Remove(i, msgC)
/\ ackC' = ackC
\/ /\ \E i \in 1..Len(ackC):
ackC' = Remove(i, ackC)
/\ msgC' = msgC
/\ UNCHANGED << output, toSend, ack, next, msg >>
Next == Sender \/ Receiver \/ LoseMsg
Spec == Init /\ [][Next]_vars
\* END TRANSLATION
Leslie Lamport
Dear Chen Fu,
You have discovered two amusing bugs or features:
- The SANY parser does not complain if it tries to parse a file without
a module.
- The Translate PlusCal Algorithm command will translate a PlusCal
algorithm, even if it does not occur inside a module.
Even if I decide that they are bugs, it's unlikely that they will be
fixed soon.
In any case, your problem will be solved by putting your specification
inside a module, which begins something like:
-------- MODULE Name --------
Leslie
Chen Fu
-------------------------- MODULE UdpMultiPackets --------------------------
=============================================================================
\* Modification History
\* Last modified Fri Apr 24 11:13:11 PDT 2015 by chenfu
\* Created Thu Apr 23 16:33:20 PDT 2015 by chenfu
\* This is a multi-packet transportation protocol over UDP
\* A Sender has PckCount number of packets to send to an Receiver, over a
\* unreliable UDP network, which could lose or reorder packets.
\*
\* We want to ensures that under strong fairness (if infinitely often m is
\* in the message queue then it is eventually received), all packets are
\* eventually received.
\*
\* Thanks Dr. Lamport for guidance!
--
You received this message because you are subscribed to a topic in the Google Groups "tlaplus" group.
To unsubscribe from this topic, visit https://groups.google.com/d/topic/tlaplus/Uv7oQ6wYXcc/unsubscribe.
To unsubscribe from this group and all its topics, send an email to tlaplus+u...@googlegroups.com.
To post to this group, send email to tla...@googlegroups.com.
Visit this group at http://groups.google.com/group/tlaplus.
For more options, visit https://groups.google.com/d/optout.
Chen Fu
---------------------------- MODULE OneBitClock ----------------------------
=============================================================================
\* Modification History
\* Last modified Fri Apr 24 13:27:44 PDT 2015 by chenfu
\* Created Fri Apr 24 13:25:41 PDT 2015 by chenfu
VARIABLE b
Init1 == (b=0) \/ (b=1)
Next1 == \/ /\ b = 0
/\ b' = 1
\/ /\ b = 1
/\ b' = 0
Leslie Lamport
The Toolbox is doing exactly what it should with your specification,
which is
--------------------- MODULE UdpMultiPackets -----------------
==============================================================
You seem to have a lot of stuff in the file that is not part of your
specification and is ignored, as it should be.
Chen Fu
--