[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

Re: [tlaplus] Understanding CHOOSE

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!

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 on the web visit https://groups.google.com/d/msgid/tlaplus/c7785a65-add0-4535-a4c1-9bc663fbcd18n%40googlegroups.com.