My First TLA+ Specification

[Irwansyah Irwansyah]

Hi All!!

Greetings from Jakarta, Indonesia. I am very excited in learning TLA+. After reading many books I still don't understand how to practically using it. Then I stumble upon articles written by Elliot Swart and beginning to grasp the idea. Then I tried to write my own TLA+ spec that implement an informal specification of a PRD on reddit. My goal with TLA+ is to add another step in my software development process, from PRD to formal methods.

If you are interested to read this is the link to my first TLA+ spec article:

https://medium.com/practical-software-craftsman/implementing-two-factor-authentication-using-formal-methods-c2d62a996ecf

Feel free to give feedbacks or letting me know which parts that I need to improve or if my understanding is incorrect.

Irwan

[Stephan Merz]

The article is unfortunately "members-only", and I am disinclined to create an account on yet another Internet site.

Stephan

--
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...@googlegroups.com.
To view this discussion visit https://groups.google.com/d/msgid/tlaplus/0757afeb-2e96-4277-95fc-baa46eb93387n%40googlegroups.com.

[Andrew Helwer]

Thanks Irwan, yes I would be interested to read it but also don't have a medium account!

Andrew

[Irwansyah Irwansyah]

I hope you guys don't mind me attaching the article as a pdf since it is hard to copy and paste it here because of the images and the formatting.

Really looking forward to feedback on whether I am doing this spec correctly or not.

Irwan

To view this discussion visit https://groups.google.com/d/msgid/tlaplus/aca444ea-a83a-431b-a821-d8cf8c6af0e3n%40googlegroups.com.

[Andrew Helwer]

Hi Irwan! Sorry I never got around to reviewing your spec - been a busy few weeks. To set future expectations, we are a relatively small community of volunteers & enthusiasts and our time is granted, not expected. You are a newcomer so are not yet enveloped by any such obligations, but free software communities (like Linux) - while not transactional - operate in terms of mutuality and reciprocity, not obligation. Although already you have been publishing blog posts talking about TLA+ so have certainly made contributions to the community!

With regard to your spec, I think it is quite good overall and very effective for a beginner. Some of the code is cut off by the fixed width of the PDF but I can get the gist. I have the following feedback:

1. You hardcode a set number of user IDs as string numbers. Conventionally you instead might want to declare a constant UserID which is instantiated to some number of abstract values in the model file. This would replace your definition VALID_USERIDS.
2. Your ALL_REQUEST_DATA set could be defined using a set like [UserID -> Request], where Request is a set of records with the fields requested_operation, userId, auth_token, and security_confirmation bound to particular domains. While this would lose some constraints like the userId in the request always matching the UserID element given in the domain, that could be enforced as a statement in a separate TypeOK invariant.
3. The MAX_ITERATIONS definition similarly could be moved to a constant to be defined in the model file.
4. Instead of hardcoding REQUEST_DATA_FOR_TESTING, you could write a more general expression generating valid possible request data.
5. It seems likely you want to use nondeterminism (through disjunction, existential quantification, or set membership) in IsLoginSuccess instead of RandomElement. For a good conceptual overview of how to use nondeterminism in modeling, I thought Hillel Wayne wrote a very nice post about it here.
6. In your invariants, instead of writing expressions of the form IF P THEN Q ELSE TRUE you can write P => Q, since if P is false then the material implication operator => is vacuously true (weird, I know, but we see the value of it here).

Overall, still a very effective spec. You might enjoy putting it into Spectacle so you can manually click around & explore the state space!

Andrew Helwer

To view this discussion visit https://groups.google.com/d/msgid/tlaplus/CA%2BKOs4w%3DN%3DdWFV55fUzdqU1vd6fGrDeXp8YfuYF5mROiCfpeHg%40mail.gmail.com.

[Irwansyah Irwansyah]

Hi Andrew and everyone,

Thanks a lot for the feedback. I thought my first spec was so dumb so no one cared to give any feedback for it :). I've spent weeks reading Z, TLA+ books, articles, etc to come up with that first spec and there are still many things that I haven't grasp, yet like determinism, termination, liveness, eventually operators, and many more.

Just want to let you guys know how hard it is for a mere mortal like me to learn TLA+ :(. Especially, switching from an imperative programming model to TLA+. There should be an easier way and that's the goal that I am pursuing for TLA+. I am hooked with Lamport's vision when watching his videos.

Irwan

To view this discussion visit https://groups.google.com/d/msgid/tlaplus/CABj%3DxUXQ13GJWtPqpw6P9yfjpVLjUw3dbvf%3DYDOkVq-RpbK2-A%40mail.gmail.com.