[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[tlaplus] TLAPS Command Line Toolbox Mode

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


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

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 tlaplus+unsubscribe@xxxxxxxxxxxxxxxx.
To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/2c54fc2c-a9a5-457c-96cc-97fa3415bfacn%40googlegroups.com.