---------------------------- MODULE Synchronizer ----------------------------
VARIABLES threadAWaiting, threadBWaiting

Init == 
  /\ threadAWaiting = FALSE
  /\ threadBWaiting = FALSE
  
waitingForB(threadAVars) == 
  /\ threadAWaiting
  /\ UNCHANGED threadAVars

waitingForA(threadBVars) ==
  /\ threadBWaiting
  /\ UNCHANGED threadBVars
  
threadA(threadAAction) ==
  threadAAction => 
    /\ threadBWaiting => threadBWaiting' = FALSE 
    /\ \neg threadBWaiting => threadAWaiting' = TRUE
    
threadB(threadBAction) ==
  threadBAction => 
    /\ threadAWaiting => threadAWaiting' = FALSE
    /\ \neg threadAWaiting => threadBWaiting' = TRUE
  
SyncThreadActions(threadAVars, threadBVars, threadAAction, threadBAction) ==
  \/ waitingForA(threadBVars) 
  \/ waitingForB(threadAVars)
  \/ threadA(threadAAction)
  \/ threadB(threadBAction)

=============================================================================
\* Modification History
\* Last modified Mon Jun 10 11:09:16 AST 2019 by marko
\* Created Mon Jun 10 09:52:33 AST 2019 by marko