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

*From*: "sadraskol (Thomas Bracher)" <thchblog@xxxxxxxxx>*Date*: Thu, 21 Jan 2021 02:21:40 -0800 (PST)*References*: <efa2ccc2-0fe0-49ad-b893-d7fd286193f0n@googlegroups.com> <CAC7YZZkjf4pZ9hYsHoNF7Uvn63eBC34wzix5Dyv983SU6zmJMg@mail.gmail.com> <c7785a65-add0-4535-a4c1-9bc663fbcd18n@googlegroups.com>

Hello John,

I think Alex answered your first point, but I'll try to express by my own words for you to see how it translates to a formal description.

Say your system is a simple increment/decrement of a global state :

CallToApi(answer) == \/ /\ answer = "200"

/\ i' = i + 1

\/ /\ answer = "400"

/\ i' = i - 1

/\ i' = i + 1

\/ /\ answer = "400"

/\ i' = i - 1

Init == i = 0

Next == LET answer == CHOOSE code \in {"200", "400"}: TRUE

IN CallToApi(answer)

The existential quantifier is the correct way of exploring all possible behavior :

Init == i = 0

Next == \E answer \in {"200", "400"}: CallToApi(answer)

The operator \E corresponds to the correct way of introducing non-determinist behavior in your specifications. TLC will check all possible behaviors for you.

I hope it helped,

Thomas

Le mercredi 20 janvier 2021 à 15:40:58 UTC+1, John a écrit :

Hi Alex,Thank you for your message.1 - IsCHOOSE sub \in ClaimsData : TRUEthe correct way to say that I want TLA+ to pick a value from ClaimsData and label itsub? 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/d674a69e-9548-45ad-9247-f4b2c41ee529n%40googlegroups.com.

**Follow-Ups**:**Re: [tlaplus] Understanding CHOOSE***From:*ron.pr...@xxxxxxxxx

**Re: [tlaplus] Understanding CHOOSE***From:*Younes

**References**:**[tlaplus] Understanding CHOOSE***From:*Park Lay

**Re: [tlaplus] Understanding CHOOSE***From:*'Alex Weisberger' via tlaplus

**Re: [tlaplus] Understanding CHOOSE***From:*John

- Prev by Date:
**Re: [tlaplus] Understanding CHOOSE** - Next by Date:
**[tlaplus] TLAPS getting slower** - Previous by thread:
**Re: [tlaplus] Understanding CHOOSE** - Next by thread:
**Re: [tlaplus] Understanding CHOOSE** - Index(es):