Re: [tlaplus] What is the difference between tlc and tlaps?

[Stephan Merz <stepha...@xxxxxxxxx>]

Hello,

TLC is a so-called "explicit-state" model checker that computes the state space generated by your specification and can then verify (safety and liveness) properties fully automatically. Its main constraint is state space explosion: the size of the state space grows exponentially with the number of processes etc., and this leads to a corresponding increase in verification time. There are a number of techniques to push back the frontiers of what TLC can handle effectively, including using symbolic constants, symmetry reduction etc., but the most important one is for you to decide how big you need your model to be to have enough confidence in correctness.

TLAPS is an interactive proof assistant: you provide a proof of why your system satisfies a property, and TLAPS can check if that proof is logically consistent and complete. It uses different automatic back-ends, including SMT solvers, to check proof steps, but it is still the user who designs and writes the proof. Although the effort is independent of the size of the state space, and also infinite-state systems can be verified in this way, I would not recommend using TLAPS for users who do not have sufficient experience with theorem proving.

As you say, there are symbolic model checkers that do not need to compute reachable states explicitly, and these are often based on SAT or SMT solvers. There is a project underway for designing and implementing a symbolic model checker for (a significant sublanguage of) TLA+, and I am sure it will be announced here when it becomes available for testing.

Regards,
Stephan


> On 23 Aug 2017, at 07:28, wangyu...@xxxxxxxxx wrote:
> 
> 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?
> 
> 
> -- 
> 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+u...@xxxxxxxxxxxxxxxx.
> To post to this group, send email to tla...@xxxxxxxxxxxxxxxx.
> Visit this group at https://groups.google.com/group/tlaplus.
> For more options, visit https://groups.google.com/d/optout.