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

[tlaplus] TLAPS getting slower


I have a spec A that refines another spec B. I found that TLAPS is noticeable slower when working on spec A. I guess this is kind of obvious, because A needs to instantiate B, so it is a more "complex" spec.

In any case, i would like to get some advice on the matter. For example, some pattern i see on the TLAPS library is to have modules like X.tla, XTheorems.tla and XTheorems_proofs.tla. As i also have a custom library of operators and another module with theorems about this operators, i wonder if separating the proofs from the statement would have some benefit on performance.


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/37f2fde7-1042-4e11-a249-3f853eaf2280n%40googlegroups.com.