[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]
What is the difference between tlc and tlaps?
I want use tla/pluscal to verify our system.
I'm confused about tlc and tlaps, I can use tlc to verify system by write liveness and Invariants, it's can find the counterexample but use huge time. the tlc seem not use SMT solver, I noticed some formal language like alloy use the SMT slover .
and tlaps also use solver, it can do same thing like tlc? Or They focus on different areas?