tla_tools将这些脚本放在您的PATH上，它们应该可以帮助您运行。请注意，您可能需要使用适当的路径修改lib/common。此外，据我所知，所有这些工具都希望在与输入文件相同的目录中运行。例子：joe@hostname ~/src/some/path $ tlc2 blah.tla 例子 joe@hostname ~/src/tla_tools/examples $ pcal-trans 3pc.tla pcal.trans Version 1.8 of 2 Apr 2013 Parsing completed. Translation completed. New file 3pc.tla written. New file 3pc.cfg written. joe@hostname ~/src/tla_tools/examples $ tlc2 3pc.