TLAPS Command Line Toolbox Mode

44 views

Skip to first unread message

Willy Schultz

unread,

Sep 17, 2021, 10:40:22 PM9/17/21

to tlaplus

When running tlapm [1], the command line tool for TLAPS, is there any functional difference between "toolbox" mode [2] and "non toolbox" mode, other than the format of the tlapm output? For example, should commands like

tlapm --toolbox 0 0 --stretch 3 -v --cleanfp --timing Lemmas.tla

and

tlapm --stretch 3 -v --cleanfp --timing Lemmas.tla

be equivalent in terms of tlapm internal behavior, ignoring the differences in output format?

[1] https://github.com/tlaplus/tlapm

[2] https://github.com/tlaplus/tlaplus/blob/d977051118f63b9c97d7d4c4d6af27183971ada3/general/docs/tlapm-toolbox-interface.txt

Reply all

Reply to author

Forward

0 new messages