[tlaplus] Re: Video Tutorial (Request for Feedback)

On Wednesday, November 17, 2021 at 8:15:19 PM UTC-7 jone...@xxxxxxxxx wrote:

Hello, Jeremy

I'm a beginner in TLA+, but I might give you a few suggestions.

You said you disable deadlock detection because the system is allowed to stop. Although I believe that to be true, a more precise way to say "the system can stop working" is using "UNCHANGED Vars" as an action in your Next statement.

To improve the flowchart, I'd recommend you change the way you wrote your Next statement into a disjunction of actions.

Your example says:

Next ==
   \/ IHaveSoda
      /\ IHaveSoda' = FALSE
      /\ IWantSoda' = TRUE
      /\ UNCHANGED <<Money, sodaMachine>>
   \/ IWantSoda /\ IHaveMoney
      /\ PutMoneyInMachine
   \/ /\ ~IWantSoda \/ ~SodaMachineHasSoda
      /\ UNCHANGED vars

I'd change it to:

PutMoneyInMachine ==
/\ IWantSoda
/\ IHaveMoney
/\ SodaMachineHasSoda
/\ Money' = Money - 1
/\ IHaveSoda' = TRUE
/\ sodaMachine' = sodaMachine - 1
/\ IWantSoda' = FALSE

DrinkSoda ==
/\ IHaveSoda
/\ IHaveSoda' = FALSE
/\ IWantSoda' = TRUE
/\ UNCHANGED <<Money, sodaMachine>>

NothingHappens == UNCHANGED vars

Next ==
\/ DrinkSoda
\/ PutMoneyInMachine
\/ NothingHappens

That way, when you generate the flowchart, you'll know which action was taken in each step.

Did I miss any details about your specification?

Best,

Jones

On Monday, 15 November 2021 at 14:20:54 UTC-3 Jeremy Wright wrote:
Hello,

I recorded a tutorial using TLA+ and the dump dot feature as a means to sketch simple designs.

https://youtu.be/alyqcphUaiI

During the iteration of the design I disable deadlock detection (with a justification), but I am suspicious of my reasoning: https://youtu.be/alyqcphUaiI?t=1260

The specification I used is here: https://github.com/JeremyLWright/specs/blob/master/algorithm/SodaMachine/SodaMachine.tla

I feel there is probably a better method to continue checking temporal properties instead of disabling deadlock detection. If someone has the time I'd appreciate any feedback.

Finally, this was a fun process sketching the spec, then recording the video. I'd like to make more. If anyone has ideas that would be interesting I'd happily considering doing a similar video tutorial.

Sincerely,
Jeremy