Re: [tlaplus] Syntax of cfg file

[Markus Kuppe <tlaplus-google-group@xxxxxxxxxxx>]

On 15.03.20 10:45, Stephan Merz wrote:
> Please check chapter 14 (in particular 14.7.1) of Specifying Systems, as
> well as [1] and the links on that page.
> 
> Stephan
> 
> [1] http://lamport.azurewebsites.net/tla/tools.html
> 
>> On 15 Mar 2020, at 18:36, narganapathy@xxxxxxxxx
>> <mailto:narganapathy@xxxxxxxxx> wrote:
>>
>> I would like to run TLC from a command line on a linux server. However
>> for that I need to generate a cfg file for the model. Is there
>> documentation on how to author these ? The TLA+ toolbox IDE generates
>> MC.cfg but its cryptic (for example it does not everything I typed
>> into the model UI and it has some generated strings). So I can't infer
>> what the syntax is. Thanks


Hi,

it's not so much what the Toolbox generates, but the config file syntax
that makes things cryptic for more involved tasks.  Also, the config
file only contains the TLA+ specific part of model checking (constants,
invariants, ...).  Runtime configuration - such as tuning flags - are
passed to TLC as command-line parameters.

I suggest to set up a model in the Toolbox and have it generate MC.tla
and MC.cfg.  Then, copy the Spec.toolbox/Model_1/ directory to the
remote machine.  The actual command-line - that the Toolbox pieced
together - can be found in the Toolbox log file
~/.tlaplus/.metadata/.log.  Grep for the string "TLC COMMAND-LINE"
(example below).

Note that it is more convenient to run CloudTLC [1], which can also be
invoked from the command-line.

Hope this helps,
Markus

[1] https://tla.msr-inria.inria.fr/tlatoolbox/doc/cloudtlc/

--

!MESSAGE TLC COMMAND-LINE (CWD:
/home/markus/src/TLA/_specs/models/tlcbugs/CM11/SUT.toolbox/Model_1):
/opt/TLA+Toolbox/plugins/org.lamport.openjdk.linux.x86_64_13.0.1.3/jre/bin/java
-XX:MaxDirectMemorySize=3974m -Xmx1989m
-Dtlc2.tool.fp.FPSet.impl=tlc2.tool.fp.OffHeapDiskFPSet
-XX:+UseParallelGC -DTLA-Library=/usr/local/lib/tlaps/
-Dfile.encoding=UTF-8 -classpath
/opt/TLA+Toolbox/plugins/org.lamport.tlatools_1.0.0.202003111724:/opt/TLA+Toolbox/plugins/org.lamport.tlatools_1.0.0.202003111724/lib/*:/opt/TLA+Toolbox/plugins/org.lamport.tlatools_1.0.0.202003111724/lib/javax.mail/*:/opt/TLA+Toolbox/plugins/org.lamport.tlatools_1.0.0.202003111724/class:/usr/local/lib/tlaps//*
tlc2.TLC -fp 111 -config MC.cfg -coverage 3 -workers 2 -tool -metadir
/home/markus/src/TLA/_specs/models/tlcbugs/CM11/SUT.toolbox/Model_1 MC

-- 
You received this message because you are subscribed to the Google Groups "tlaplus" group.
To unsubscribe from this group and stop receiving emails from it, send an email to tlaplus+unsubscribe@xxxxxxxxxxxxxxxx.
To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/af428553-86cd-f486-ec7b-2858ad009130%40lemmster.de.