-
Notifications
You must be signed in to change notification settings - Fork 8
Rules implemented by the State Machines (Distributed Logic)
A paper was written by Benedek Horváth, Raimund Andreas Konnerth, Zsolt Mázló for the Scientific Student’s Conference at BME in 2014. The title of the paper is Elosztott biztonságkritikus rendszerek modellvezérelt fejlesztése and was written in Hungarian. The relevant parts are pp. 35—45.
At the time of the Scientific Student’s Conference we used BridgePoint as a designer and simulator tool for creating State Machines. The relevant models and transformations are stored in the BP2UPPAAL module, that has been deprecated since that time. It is because we switched for Yakindu Statechart Tools that is an easier-to-handle and more robust tool on this purpose.
As a general rule of thumb we interchangeably use statecharts and state machines in terminology.
In Yakindu we redesigned the state machines and separated them for different satecharts. We designed a (general) statechart for the Section, and a separate one for the Turnot, that can either be a Normal Turnout or an English Turnout.
The Section's statechart is a composite one which means, if the top-level statechart consists of two states: Free Section and OccupiedSection. The former one is a simple state, with on-event event-handling, while the latter one is a composite state consisting of many other states. However, there are no parallel regions in either states.
As for the turnouts although we separate between Normal Turnout and English Turnout, in the naming of the statecharts there is no difference between them. That is because, it was easier to integrate the glue code with the generated one, since less references had to be replaced. Of course in the details of the statecharts there are differences between them, because they are different up to an extent.
The Normal Turnout's model is stored here, while the English Turnout's model is stored here. It should be noted that the same Section models are used for both turnouts.
The highest level of the Turnout statechart makes difference between StraightTurnout and DivergentTurnout. Inside each state there are multiple parallel regions. Each event that is relevant from the locking protocol’s perspective is in a separate region that means, the different lockings (from different directions) can be handled in parallel due to the good nature of Yakindu Statecharts.
It should be noted as well, that if a locking comes from a direction that is perpenticular to the recent direction of the turnout (e.g. a train would come from divergent direction while the turnout is straight), the the respective train will be stopped immediately. In case of a StraightTurnout (DivergentTurnout) it is handled by the HandlerStraight (HandlerDivergent) region of the StraightTurnout (DivergentTurnout) state (respectively).
It is detailed in the paper referred in the Theoretical background section of this documentation.
When a train occupies a section, then the respective Section's statechart sends a sectionLockFrom:direction event to the turnout which it connects from the respective direction. After that the Turnout checks whether its direction is perpenticular to the one from which the section sent the event. If it is, the train must stop on the section (otherwise it would cut the turnout).
If it is not, then the Turnout checks to connecting section (other side of the turnout) if there is a train there. If there is, then on both sections the trains must be stopped. If there is no train there, then the neighbouring turnouts in BOTH directions are checked. (Both directions should be checked, because the statecharts do not know where the train is heading to physically on the track, and they always presume that the train would come towards the turnout.)
If from any of the neighbouring turnouts a passage denied or lock answer is received, then the train must be stopped on the section that originated the locking protocol. Otherwise the train is free to go.
If a turnout receives a lock request from a neighbouring turnout, then it decides whether there is any train on the local turnout’s (that received the recent lock request) territory (the turnout itself and the connecting sections according to the turnout’s direction). If there is and this turnout’s priority is lower than the one’s priority who sent the lock request, then this local turnout will stop the train that is on its territory, and allow the remote turnout to let the remote train come. Otherwise if the local turnout’s priority is higher than the remote turnout’s, then the remote turnout must stop the train that would come near to the local turnout.
If there is no train on the territory of the turnout then any train can come from the remote turnouts' territory.
It is detailed in the paper referred in the Theoretical background section of this documentation.
The section revoke protocol is periodically applied when a section is locked. It means the section sends a lock request to the turnout it connects to. It is the same protocol that is used for deciding whether the train should be stopped, but at this time if the train can go (according to the reply received from the turnout), then the section will be unlocked and the train is free to go.