Syntax of cfg file

816 views
Skip to first unread message

nargan...@gmail.com

unread,
Mar 15, 2020, 1:36:49 PM3/15/20
to tlaplus
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

Stephan Merz

unread,
Mar 15, 2020, 1:45:09 PM3/15/20
to tla...@googlegroups.com
Please check chapter 14 (in particular 14.7.1) of Specifying Systems, as well as [1] and the links on that page.

Stephan

On 15 Mar 2020, at 18:36, nargan...@gmail.com 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

--
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+u...@googlegroups.com.
To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/a4426f93-a1d6-4403-bcb9-969174d41218%40googlegroups.com.

Markus Kuppe

unread,
Mar 15, 2020, 1:58:10 PM3/15/20
to tla...@googlegroups.com
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, nargan...@gmail.com
>> <mailto:nargan...@gmail.com> 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

nargan...@gmail.com

unread,
Mar 15, 2020, 2:31:37 PM3/15/20
to tlaplus
Thanks. This is what I did. I pushed all the key  files under toolbox to github and synched to my linux server and ran tlc -config MC.cfg MC.tla  and this seems to work. I will checkout cloudtlc.

Shiyao MA

unread,
Mar 15, 2020, 10:09:29 PM3/15/20
to tlaplus
I have always wondered if the latex source of specifying system book is available.

The current public pdf version has signifcant drawbacks:
1. We cannot search the whole pdf text.  Somehow the file seems to be a "jpg" to the pdf reader.
2. We cannot highlight the text on the pages.




On Monday, 16 March 2020 01:45:09 UTC+8, 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

On 15 Mar 2020, at 18:36, nargan...@gmail.com 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

--
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 tla...@googlegroups.com.

Leslie Lamport

unread,
Mar 18, 2020, 6:47:08 PM3/18/20
to tlaplus
I downloaded the pdf file and was able to search it and highlight text with Adobe Reader.  Some other readers, apparently including the Toolbox's pdf reader, does not support those features on any pdf file.

Leslie

Shiyao MA

unread,
Mar 18, 2020, 9:42:08 PM3/18/20
to tla...@googlegroups.com
Just for the record, the pdf reader I am using is preview.app, which is the default one on mac.


You received this message because you are subscribed to a topic in the Google Groups "tlaplus" group.
To unsubscribe from this topic, visit https://groups.google.com/d/topic/tlaplus/PVa4CZMUQjE/unsubscribe.
To unsubscribe from this group and all its topics, send an email to tlaplus+u...@googlegroups.com.
To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/decf0404-13ee-4c7c-833b-e5be1a5122ae%40googlegroups.com.


--
Best,
Shiyao

Leslie Lamport

unread,
Mar 19, 2020, 7:11:17 PM3/19/20
to tlaplus
I investigated further and found that there did seem to be a problem with the pdf file.  The file was created in 2002.  I believe that pdflatex did not yet have full functionality then, so I probably produced the file from LaTeX's dvi output.  I recreated the pdf file using pdflatex and posted it on the Web.  This should solve the problem.  Thanks for reporting this.

Leslie  


On Wednesday, March 18, 2020 at 6:42:08 PM UTC-7, Shiyao MA wrote:
Just for the record, the pdf reader I am using is preview.app, which is the default one on mac.


On Thu, Mar 19, 2020 at 6:47 AM Leslie Lamport  wrote:
I downloaded the pdf file and was able to search it and highlight text with Adobe Reader.  Some other readers, apparently including the Toolbox's pdf reader, does not support those features on any pdf file.

Leslie

On Sunday, March 15, 2020 at 7:09:29 PM UTC-7, Shiyao MA wrote:
I have always wondered if the latex source of specifying system book is available.

The current public pdf version has signifcant drawbacks:
1. We cannot search the whole pdf text.  Somehow the file seems to be a "jpg" to the pdf reader.
2. We cannot highlight the text on the pages.




On Monday, 16 March 2020 01:45:09 UTC+8, 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, nargan...@gmail.com 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

--
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 tla...@googlegroups.com.
To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/a4426f93-a1d6-4403-bcb9-969174d41218%40googlegroups.com.

--
You received this message because you are subscribed to a topic in the Google Groups "tlaplus" group.
To unsubscribe from this topic, visit https://groups.google.com/d/topic/tlaplus/PVa4CZMUQjE/unsubscribe.


--
Best,
Shiyao

Shiyao MA

unread,
Mar 20, 2020, 12:07:23 PM3/20/20
to tla...@googlegroups.com
Thanks for that.

I've attached the TOC to the pdf file.

In case anyone find it useful, I post a link to the file here:




To unsubscribe from this group and all its topics, send an email to tlaplus+u...@googlegroups.com.
To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/c6df75bf-0b6e-4577-8bf6-0d5c80aee171%40googlegroups.com.


--
Best,
Shiyao
Reply all
Reply to author
Forward
0 new messages