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.The pdf version is: https://lamport.azurewebsites.net/tla/book-02-08-08.pdfOn 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.htmlOn 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.
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 view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/decf0404-13ee-4c7c-833b-e5be1a5122ae%40googlegroups.com.
--Best,
Shiyao
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+unsubscribe@xxxxxxxxxxxxxxxx.
To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/c6df75bf-0b6e-4577-8bf6-0d5c80aee171%40googlegroups.com.