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

On Tue, 7 Dec 2021 at 13:58, Jeremy Wright <jeremy@xxxxxxxxxxxx> wrote:

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

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

--
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+unsubscribe@xxxxxxxxxxxxxxxx.
To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/8fdb2085-fd7b-4cfd-8bf1-4505657cd857n%40googlegroups.com.