Hi Alex,
Thank you for your message.
1 - Is CHOOSE sub \in ClaimsData : TRUE the correct way to say that I want TLA+ to pick a value from ClaimsData and label it sub ? How would you have expressed it ?
2 - In my module, I'm trying to represent the bahviour of an external API (which may respond with a 200 HTTP status or a 4XX or 5XX HTTP status : 2 states => Success OR Failure). Briefly put, how would you describe an external API that your system consumes and needs to react predictably according to the API's response (success or failure) ? (the "randomness" part is how often do you get a Successful/Failed response. The difficulty is how do I describe this beahviour ?
Thank you!