module turing-machine { namespace "http://example.net/turing-machine"; prefix tm; description "Data model for the Turing Machine."; revision 2013-12-27 { description "Initial revision."; } typedef tape-symbol { type string { length "0..1"; } description "Type of symbols appearing in tape cells. A blank is represented as an empty string where necessary."; } typedef cell-index { type int64; description "Type for indexing tape cells."; } typedef state-index { type uint16; description "Type for indexing states of the control unit."; } typedef head-dir { type enumeration { enum "left"; enum "right"; } default "right"; description "Possible directions for moving the read/write head, one cell to the left or right (default)."; } grouping tape-cells { description "The tape of the Turing Machine is represented as a sparse array."; list cell { key "coord"; description "List of non-blank cells."; leaf coord { type cell-index; description "Coordinate (index) of the tape cell."; } leaf symbol { type tape-symbol { length "1"; } description "Symbol appearing in the tape cell. Blank (empty string) is not allowed here because the 'cell' list only contains non-blank cells."; } } } container turing-machine { description "State data and configuration of a Turing Machine."; leaf state { type state-index; config false; mandatory true; description "Current state of the control unit. The initial state is 0."; } leaf head-position { type cell-index; config false; mandatory true; description "Position of tape read/write head."; } container tape { config false; description "The contents of the tape."; uses tape-cells; } container transition-function { description "The Turing Machine is configured by specifying the transition function."; list delta { key "label"; unique "input/state input/symbol"; description "The list of transition rules."; leaf label { type string; description "An arbitrary label of the transition rule."; } container input { description "Input parameters (arguments) of the transition rule."; leaf state { type state-index; mandatory true; description "Current state of the control unit."; } leaf symbol { type tape-symbol; mandatory true; description "Symbol read from the tape cell."; } } container output { description "Output values of the transition rule."; leaf state { type state-index; description "New state of the control unit. If this leaf is not present, the state doesn't change."; } leaf symbol { type tape-symbol; description "Symbol to be written to the tape cell. If this leaf is not present, the symbol doesn't change."; } leaf head-move { type head-dir; description "Move the head one cell to the left or right"; } } } } } rpc initialize { description "Initialize the Turing Machine as follows: 1. Put the control unit into the initial state (0). 2. Move the read/write head to the tape cell with coordinate zero. 3. Write the string from the 'tape-content' input parameter to the tape, character by character, starting at cell 0. The tape is othewise empty."; input { leaf tape-content { type string; default ""; description "The string with which the tape shall be initialized. The leftmost symbol will be at tape coordinate 0."; } } } rpc run { description "Start the Turing Machine operation."; } rpc run-until { description "Start the Turing Machine operation and let it run until it is halted or ALL the defined breakpoint conditions are satisfied."; input { leaf state { type state-index; description "What state the control unit has to be at for the execution to be paused."; } leaf head-position { type cell-index; description "Position of tape read/write head for which the breakpoint applies."; } container tape { description "What content the tape has to have for the breakpoint to apply."; uses tape-cells; } } output { leaf step-count { type uint64; description "The number of steps executed since the last 'run-until' call."; } leaf halted { type boolean; description "'True' if the Turing machine is halted, 'false' if it is only paused."; } } } notification halted { description "The Turing Machine has halted. This means that there is no transition rule for the current state and tape symbol."; leaf state { type state-index; mandatory true; description "The state of the control unit in which the machine has halted."; } } notification paused { description "The Turing machine has reached a breakpoint and was paused."; leaf state { type state-index; mandatory true; description "State of the control unit in which the machine was paused."; } leaf head-position { type cell-index; mandatory true; description "Position of tape read/write head when the machine was paused."; } container tape { description "Content of the tape when the machine was paused."; uses tape-cells; } } }