Hi,
I am new to TLA.I am exploring TLA+ tools and i am facing problems in this.I have following queries
1)I want to know how to get output for any code.suppose we write code for factorial program(in which we are calculating factorial of a number) so where we will get its output.
2)How to check a model with tlc when there is no liveness property?
Thanks in advance
TLA+ Specification
(2 posts) (2 voices)-
Parul
MemberPosted 5 months ago # -
The first thing you should do is read about TLA and TLA+. See the Documentation/Books page. You will discover that TLA+ is not a programming language. Perhaps you want PlusCal.
1) PlusCal contains a print statement, but it's mostly for debugging. You are more likely to want to check that, at some point in your PlusCal code, x = y!, for some variables x and y. To do that, you would define Factorial in TLA+ and add the assertion x = Factorial(y).
2) You just don't tell TLC to check any liveness property.
Leslie Lamport
Posted 4 months ago #
Reply
You must log in to post.