Can I get the command line used by the toolbox?

36 views
Skip to first unread message

Guo Hua

unread,
Oct 14, 2023, 10:47:18 AM10/14/23
to tlaplus
Is there an approach that would allow me to determine the exact command line used by the toolbox during model checker? This would enable me to rerun the model checker later using TLC/tlatools.jar through the command line.

Guo

Markus Kuppe

unread,
Oct 14, 2023, 2:44:06 PM10/14/23
to tla...@googlegroups.com
The Toolbox records the command in the ~/.tlaplus/.metadata/.log file.

Markus

Guo Hua

unread,
Oct 15, 2023, 1:27:15 AM10/15/23
to tlaplus
Got It. Thank you for your response.

Guo
Reply all
Reply to author
Forward
0 new messages