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:
- 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.
- 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.
- The MAX_ITERATIONS definition similarly could be moved to a constant to be defined in the model file.
- Instead of hardcoding REQUEST_DATA_FOR_TESTING, you could write a more general _expression_ generating valid possible request data.
- 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.
- 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--On Mon, May 26, 2025 at 12:12 PM Irwansyah Irwansyah <irwansyah@xxxxxxxxx> wrote: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--On Mon, May 26, 2025 at 9:00 PM Andrew Helwer <andrew.helwer@xxxxxxxxx> wrote:Thanks Irwan, yes I would be interested to read it but also don't have a medium account!Andrew--On Monday, May 26, 2025 at 8:37:21 AM UTC-4 Stephan Merz wrote:The article is unfortunately "members-only", and I am disinclined to create an account on yet another Internet site.StephanOn 25 May 2025, at 11:42, Irwansyah Irwansyah <irwa...@xxxxxxxxx> wrote: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--
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 view this discussion visit https://groups.google.com/d/msgid/tlaplus/0757afeb-2e96-4277-95fc-baa46eb93387n%40googlegroups.com.
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+unsubscribe@xxxxxxxxxxxxxxxx.
To view this discussion visit https://groups.google.com/d/msgid/tlaplus/aca444ea-a83a-431b-a821-d8cf8c6af0e3n%40googlegroups.com.
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+unsubscribe@xxxxxxxxxxxxxxxx.
To view this discussion visit https://groups.google.com/d/msgid/tlaplus/CA%2BKOs4w%3DN%3DdWFV55fUzdqU1vd6fGrDeXp8YfuYF5mROiCfpeHg%40mail.gmail.com.
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+unsubscribe@xxxxxxxxxxxxxxxx.
To view this discussion visit https://groups.google.com/d/msgid/tlaplus/CABj%3DxUXQ13GJWtPqpw6P9yfjpVLjUw3dbvf%3DYDOkVq-RpbK2-A%40mail.gmail.com.