Re: [tlaplus] Syntax of cfg file

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...@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

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