Thanks for your quick reply, Leslie.
In a student project last year our student extended the toolbox to
build a "Linearisability checker"
using TLC as a backend. As a frontend she modified the toolbox code
which worked fine.
The student has left now and we are not able to rebuild the toolbox
with her modified
code. This could be due to changes in the toolbox or our lack of
knowledge of how to
integrate code into maven. Hence we are stuck and contemplating to
build our own
frontend from scratch.
For the time being we want to run some experiments in batch mode.
On 10/02/17 11:05, Leslie Lamport
TLC allows only a
restricted class of expressions in a configuration file.
See "Specifying Systems" for the exact syntax. Why aren't
you running TLC from the Toolbox?