tck-reach returns syntax error, unexpected &&, expecting )

[alzeha]

Hi,

given the following uppaal model

<?xml version="1.0" encoding="utf-8"?>
<!DOCTYPE nta PUBLIC '-//Uppaal Team//DTD Flat System 1.5//EN' 'http://www.it.uu.se/research/group/darts/uppaal/flat-1_5.dtd'>
<nta>
	<declaration>// Place global declarations here.
</declaration>
	<template>
		<name x="5" y="5">Template</name>
		<declaration>// Place local declarations here.
</declaration>
		<location id="id0" x="0" y="0">
			<name x="-10" y="-34">A</name>
		</location>
		<location id="id1" x="136" y="0">
			<name x="126" y="-34">B</name>
			<label kind="invariant" x="126" y="17">((1 &amp;&amp; 1) &amp;&amp; (1 &amp;&amp; 0))</label>
		</location>
		<init ref="id0"/>
		<transition id="id2">
			<source ref="id1"/>
			<target ref="id0"/>
			<nail x="85" y="68"/>
		</transition>
		<transition id="id3">
			<source ref="id0"/>
			<target ref="id1"/>
		</transition>
	</template>
	<system>// Place template instantiations here.
Process = Template();
// List one or more processes to be composed into a system.
system Process;
</system>
	<queries>
		<query>
			<formula/>
			<comment/>
		</query>
	</queries>
</nta>

(please recognize the invariant)

uppaal-to-tchecker outputs

# 
# This file has been generated automatically with uppaal-to-tchecker
# 
system:min_ex.xml
# no iodecl
# compilation of process Process
process:Process
location:Process:A{initial:}
location:Process:B{invariant:(1 && ((1 && 1) && (1 && 0)))}
# global event for Uppaal unlabelled edges
event:tau
edge:Process:B:A:tau{}
edge:Process:A:B:tau{}

That was quite surprising for me since according to https://github.com/ticktac-project/tchecker/wiki/TChecker-file-format#expressions, the invariant of location B is not a proper tchecker expression.

tck-syntax agrees:

$ tck-syntax -c min_ex.tck 
ERROR: 9.30-58 syntax error, unexpected &&, expecting ) (at 1.17-18)
ERROR: Syntax error
2 error(s)

This is a bug in utot, right?

Best,
Alexander