User Tools
tla:start
Differences
This shows you the differences between two versions of the page.
| Both sides previous revision Previous revision Next revision | Previous revision | ||
|
tla:start [2019/09/03 00:30] jonathan |
tla:start [2019/09/08 19:55] (current) jonathan |
||
|---|---|---|---|
| Line 3: | Line 3: | ||
| On Prism (or the SEL-VM) invoke ''tla'' from the command line. You can also install the TLA+ Toolbox/IDE on your Laptop. | On Prism (or the SEL-VM) invoke ''tla'' from the command line. You can also install the TLA+ Toolbox/IDE on your Laptop. | ||
| + | [[https://www.youtube.com/playlist?list=PLEWQAc3YS7XaULwGamfcKUfPr9HhF2ckk|youtube playlist]] of Introductory Videos for analyzing TLA+ Specifications and checking them for specification error using the TLC modelchecker. | ||
| + | |||
| + | {{ :tla:tla-summary.pdf |TLA+ Summary}} | ||
| ====== What is TLA+ ====== | ====== What is TLA+ ====== | ||
| Line 15: | Line 18: | ||
| 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. | 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. | ||
| - | ====== Introductory Videos ====== | + | ====== Introductory Videos TLA+/TLC ====== |
| ==== A very simple traffic light ==== | ==== A very simple traffic light ==== | ||
tla/start.1567470600.txt.gz · Last modified: 2019/09/03 00:30 by jonathan
Page Tools
