A system of railway tracks connects four train stations: A, B, C, and D. There are two trains “Train1” and “Train2” which commute on the line. “Train1” drives from A to D and back, and “Train2” from B to D and back. Both trains always take the complete round-trip route, they are not allowed to commute between individual stations. At the beginning “Train1” is in D and “Train2” in B. The trains do not have to drive in alternating order, i.e. it is possible that “Train1” leaves train station A instantly after arriving.
Additionally, only one of the trains can pass the section between C to D. To ensure safety, one train has to wait at station A, or B respectively, while the other train is driving. Therefore, messages to the other train are sent upon leaving station A resp. B, and upon returning there.
Fig. 4.1. Trains
Model the trains as a composite automaton with orthogonal states which uses only signals for communication.
Imagine the forest around the train tracks was cleared, hence, each train driver can see where the other one is. Please design a second model for the trains, but please use this time only guards for synchronization.