如何用TLA+工具箱有效地使用git

Question

TLA+工具箱创建了许多文件和目录。使用规范和模型并将它们保存在git中并使用工具箱的好方法是什么？正常的工作流是什么样子的？

Answer 1

在我的.gitignore中，我完全忽略了.gitignore。这意味着模型配置没有保留在回购中，这是不理想的。

使用VS代码插件可以获得良好的工作流，该插件依赖于顶级.cfg文件、配置模型常量和要检查哪些不变量/属性。

这是我的.gitignore

*.dvi
*.old
*.out
*.pdf
*.tex
*.toolbox

我保留了一个Makefile，它具有一些有用的任务，比如清理这些辅助文件，以及在一个单独的dist/文件夹中维护打印得很好的PDF。

JAVA ?= java
TLA2TOOLS_JAR = "tla2tools.jar"
TLA2TOOLS ?= $(JAVA) --class-path $(TLA2TOOLS_JAR)
TLA2TEX ?= $(JAVA) --class-path ../$(TLA2TOOLS_JAR) \
                                           tla2tex.TLA -latexCommand "pdflatex" -shade -grayLevel 0.9

DISTDIR = dist
PDFS = $(addprefix $(DISTDIR)/, $(patsubst %.tla, %.pdf, $(wildcard *.tla)))

all: dist

pdfs: $(PDFS)

$(DISTDIR)/%.pdf: %.tla
        cd $(DISTDIR) && $(TLA2TEX) ../$^

dist: pdfs clean

clean:
        @echo "Cleaning auxiliary TLA2TeX files"
        @rm -f $(DISTDIR)/*.aux $(DISTDIR)/*.dvi $(DISTDIR)/*.log $(DISTDIR)/*.tex

distclean: clean
        rm -f $(DISTDIR)/*.pdf

.PHONY: pdfs dist clean distclean

Answer 2

将此添加到.gitignore中只会保留模型参数文件，如MySpec.toolbox/MySpec__Model_1.lauch，如果所有其他文件丢失，则只需恢复该模型：

# TLA+ Toolbox files, this will keep <spec_name>__<model_name>.launch
/*.toolbox/.settings
/*.toolbox/.project
/*.toolbox/*/*
/*.toolbox/*_SnapShot_*.launch
# TLA+ Toolbox PDF production artifacts
/*.toolbox/*.aux
/*.toolbox/*.log
/*.toolbox/*.tex
/*.toolbox/*.pdf
/*.pdf

您可以通过以下步骤验证这一点：

提交MySpec.toolbox/MySpec__Model_1.lauch

• close工具箱中的规范(如果不提交，工具箱将显示一个错误，下次打开它时可以取消)，

• 退出了MySpec.toolbox/中的toolbox

• delete everything，除了使用Add New Spec...

• recreate的MySpec__Model_1.lauch

• reopen toolbox

• reopen之外，还有一个与以前同名的模型，Model_1在本例中

• 保存和关闭模型

• 退出工具箱

• ，删除工具箱在保存模型

<代码>H 130时对MySpec.toolbox/MySpec__Model_1.lauch所做的更改，重新打开工具箱<代码>H 231<代码>F 232

目前唯一的缺点是，参数调用fpIndex存储在MySpec.toolbox/MySpec__Model_1.lauch中，在每次执行模型时都会发生变化，参见https://tla.msr-inria.inria.fr/tlatoolbox/doc/model/tlc-options-page.html中的指纹种子索引。这将导致此文件每次出现在git中已更改的文件中。