parsing config file in command line mode

[Kirsten Winter <kir...@xxxxxxxxxxxxxx>]

Dear Colleagues,

I want to run TLC from a command line and get
the following parsing error:

TLC2 Version 2.08 of 21 December 2015
Running in Model-Checking mode.
Error: TLC threw an unexpected exception.
This was probably caused by an error in the spec or model.
See the User Output or TLC Console for clues to what happened.
The exception was a tlc2.tool.ConfigFileException
: TLC found an error in the configuration file at line 7
It was expecting = or <-, but did not find it.
Finished in 00s at (2017-02-10 10:12:23)

using the following configuration file:

CONSTANT
  null = 0
  N = 3
  T = {1,2}
  Ref = {1,2,3}
  empty = 0
  undef = <<3,3>>

SPECIFICATION
  Spec

INVARIANTS
  ABS
  INV
  STATUS

If I use the value <<3,3>> directly in the module (instead of using the 
constant "undef") the parser
is happy.

The corresponding module file as well as the configuration file are 
attached.

Thank you for your help,
Kirsten

---------------------------- MODULE dequeue0----------------------------
EXTENDS Status, FiniteSequences, Naturals
VARIABLES head, qTail, pc, mem, tail, nextNode, qHead, retVal, queue, out

CONSTANT Ref, T, null, N, empty, undef

ABS0[q \in FiniteSeq(T, N), h \in Ref \union {null}] == (h = null => Len(q)=0) /\
                   (h /= null => Len(q) /= 0 /\ mem[h][1]=Head(q) /\ ABS0[Tail(q), mem[h][2]])
ABS == ((qHead /= null /\ qTail /= null) =>
        (((mem[qTail][2] = null => (qTail = qHead \/ (Len(queue) /= 0 /\ mem[qTail][1] = queue[Len(queue)])))
        /\ (mem[qTail][2] /= null => (Len(queue) > 1 /\ mem[qTail][1] = queue[Len(queue)-1]) 
             \/ (Len(queue) = 1 /\ qTail = qHead))) 
      /\ ABS0[queue, mem[qHead][2]]))

INV ==  (pc=0 => ( qHead /= null 
                  /\ (qHead /= qTail => mem[qHead][2] /= null)))
    /\ (pc=19 => ( qHead /= null 
                  /\ (qHead /= qTail => mem[qHead][2] /= null)))

STATUS ==  ((pc = 0 => (TRUE))
            /\ (pc = 19 => (TRUE)))
	
Exec ==  (((pc = 33 /\ pc' = 34) \/ (pc = 52 /\ pc'= 53)) /\ TRUE) 
	 \/ (((pc = 21 /\ pc' = 22 /\ Len(queue) = 0)) /\ TRUE /\ UNCHANGED<<queue>>) 
	 \/ (((pc = 22 /\ pc' = 24 /\ Len(queue) = 0)) /\ ((TRUE) \/ (UNCHANGED<<queue>> 
                 /\ out' = out /\ UNCHANGED<<>>))) 
	 \/ (((pc = 22) \/ (pc = 26 /\ pc' /=  27)) /\ UNCHANGED<<queue>> /\ UNCHANGED<<>>) 

Init == /\ queue \in FiniteSeq(T, N) /\ qHead \in Ref \union {null} /\ qTail \in Ref \union {null}
        /\ mem \in [Ref ->(T \X (Ref \union {null})) \union {undef}] 
        /\ ABS 
        /\ head = null /\ pc = 0 /\ tail = null /\ nextNode = null /\ retVal = 0 
        /\ INV /\ out = 0 /\ STATUS
 

dequeue0 ==  pc = 0 /\ pc' = 19  /\ UNCHANGED<<head,qTail,mem,tail,nextNode,qHead,retVal,queue,out>> 

Spec ==  Init /\ [][dequeue0]_<<head, qTail, pc, mem, tail, nextNode, qHead, retVal, queue, out>> 

=============================================================================

CONSTANT
  null = 0
  N = 3
  T = {1,2}
  Ref = {1,2,3}
  empty = 0
  undef = <<3,3>> 

SPECIFICATION
  Spec

INVARIANTS
  ABS 
  INV 
  STATUS