Train Control Table Syntax

14 January 2024
trains

This page is as per EGG 1648 - Control Tables Format and Syntax. My interpretation of the syntax without may be incorrect, but seems to work fine based on the examples they provide.

What follows are the inference rules for their Control Tables Syntax, which nominally is expressions of the form 31AT. [31BT. 31CT w 202N]. [31XT. 31YT w 202R]. I assume that we have a judgement specifying what constitutes an atom within the syntax, i.e., what constitutes a valid 31AT. Additionally, I arbitrarily use right-associativity, to remove ambiguity, although AND/OR are both left and right-associative, the associativity of WHEN is unknown.

\begin{matrix} \begin{matrix} *:･ﾟmagic *:･ﾟ \end{matrix} \\ x BAtom \end{matrix} R_{1}

\begin{matrix} \begin{matrix} x BAtom \end{matrix} \\ x BNot \end{matrix} R_{2}

\begin{matrix} \begin{matrix} x BNot \end{matrix} \\ x BAnd \end{matrix} R_{3}

\begin{matrix} \begin{matrix} x BAnd \end{matrix} \\ x BWhen \end{matrix} R_{4}

\begin{matrix} \begin{matrix} x BWhen \end{matrix} \\ x BOr \end{matrix} R_{5}

\begin{matrix} \begin{matrix} x BOr \end{matrix} \\ (x) BAtom \end{matrix} R_{6}

\begin{matrix} \begin{matrix} x BAtom \end{matrix} \\ not x BNot \end{matrix} R_{7}

\begin{matrix} \begin{matrix} x BNot y BAnd \end{matrix} \\ x . y BAnd \end{matrix} R_{8}

\begin{matrix} \begin{matrix} x BAnd y BWhen \end{matrix} \\ x w y BWhen \end{matrix} R_{9}

\begin{matrix} \begin{matrix} x BWhen y BOr \end{matrix} \\ x or y BOr \end{matrix} R_{10}

An example derivation is as follows:

\begin{matrix} \begin{matrix} \begin{matrix} \begin{matrix}  \end{matrix} \\ 31AT BAtom \end{matrix} & \begin{matrix} \begin{matrix} \begin{matrix} \begin{matrix} \begin{matrix} \begin{matrix}  \end{matrix} \\ 31BT BAtom \end{matrix} & \begin{matrix} \begin{matrix} 31CT BAtom & 202N BAtom \end{matrix} \\ 31CT w 202N BWith \end{matrix} (by R_{9}) \end{matrix} \\ 31BT. 31CT w 202N BAnd \end{matrix} (by R_{8}) \end{matrix} \\ [31BT. 31CT w 202N] BAtom \end{matrix} (by R_{6}) \end{matrix} \\ 31AT. [31BT. 31CT w 202N] BAnd \end{matrix} (by R_{8})