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