Video Tutorial (Request for Feedback)

[Jeremy Wright]

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

[Jones Martins]

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

[Jeremy Wright]

Hello Jones,

Thank you for the feedback!

I didn't think about adding another "layer" of names in the Next action. However, do so makes the picture so much better! TLC even adds a legend. Beautiful!

I'm going to make a follow up video, and continue making tutorials in this style. Thank you again.

Sincerely,

Jeremy

[Jones Martins]

Hi, Jeremy

Awesome! Now the generated graph is very satisfying.

Best regards,

Jones

--
You received this message because you are subscribed to a topic in the Google Groups "tlaplus" group.
To unsubscribe from this topic, visit https://groups.google.com/d/topic/tlaplus/-RsGI6I_xD0/unsubscribe.
To unsubscribe from this group and all its topics, send an email to tlaplus+u...@googlegroups.com.
To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/8fdb2085-fd7b-4cfd-8bf1-4505657cd857n%40googlegroups.com.