[tlaplus] TLAPS getting slower

[JosEdu Solsona <josedusolsona@xxxxxxxxx>]

Hello!

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.

Cheers,

José

-- 
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.