Can not edit "What is the model" and "What is the behavior spec?"

[Chen Fu <chen...@xxxxxxxxx>]

Hi:

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