What is the difference between tlc and tlaps?

[wangyu...@xxxxxxxxx]

HI all:
  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?