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