Interlocking data safe conversion method for formal verification and translator

A translator, comprising:

• one or more processors;
• and
• memory and computer program code stored in memory and running on the one or more processors, wherein the computer program code and memory are configured, when executed by the one or more processors, to cause the one or more processors to convert an input file into a format file capable of being identified by a formal verification tool,
• wherein the one or more processors identifies a header keyword in the input file, and converts a variable type associated with each keyword according to a conversion rule and rearranges the converted data to generate the format file capable of being identified by the formal verification tool;
• and
• wherein the conversion rule comprises:
• with regard to an integer type I, the input data is an integer, a null value, or NA, and the one or more processors converts an integer into an integer and converts the null value and the NA into null;
• with regard to a Boolean type B, the input data is 1, 0, Y, N, a null value, or NA, and the one or more processors converts 1 and Y into true, converts 0 and N into false and converts the null value and the NA into null;
• with regard to a text type T, the input data is any character string, a null value, or NA, and the one or more processors outputs the character string intact and converts the null value and the NA into null;
• and
• with regard to a form type L, the input data is any character string, and the one or more processors separates data in a form with ‘,’ and outputs ‘[ ]’ for an empty form;
• and
• wherein the input file comprises an interlocking information table in interlocking data, a device interface information table, a station yard description data, and interlocking Boolean logic data;
• and
• wherein the one or more processors converts the interlocking information table and the device interface information table into an LCF format file;
• and
• wherein:
• the one or more processors reads turnout position information in the interlocking information table and differentiates positioning and anti-positioning of a turnout with an independent conversion description in the generated LCF format file;
• the one or more processors reads beyond limit conditions of a section in the interlocking information table and differentiates the beyond limit conditions with an independent conversion description in the generated LCF format file;
• and
• the one or more processors reads conflicting routes in the interlocking information table and corresponding conflicting route types, and differentiates the conflicting routes and the conflicting route types with an independent conversion description in the generated LCF format file.