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.";
  }

  /* Typedefs */

  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).";
  }

  /* Groupings */

  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.";
      }
    }
  }

  /* State data and Configuration */

  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";
          }
        }
      }
    }
  }

  /* RPCs */

  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.";
      }
    }
  }

  /* Notifications */

  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;
    }
  }
}

{
    "turing-machine": {
        "transition-function": {
            "delta": [
                {
                    "label": "separator",
                    "input": {
                        "state": 0,
                        "symbol": "0"
                    },
                    "output": {
                        "state": 1,
                        "symbol": "1"
                    }
                },
                {
                    "label": "write separator",
                    "input": {
                        "state": 2,
                        "symbol": "1"
                    },
                    "output": {
                        "state": 3,
                        "symbol": "0",
                        "head-move": "left"
                    }
                },
                {
                    "label": "right summand",
                    "input": {
                        "state": 1,
                        "symbol": "1"
                    }
                },
                {
                    "label": "final step",
                    "input": {
                        "state": 3,
                        "symbol": ""
                    },
                    "output": {
                        "state": 4
                    }
                },
                {
                    "label": "go home",
                    "input": {
                        "state": 3,
                        "symbol": "1"
                    },
                    "output": {
                        "head-move": "left"
                    }
                },
                {
                    "label": "right end",
                    "input": {
                        "state": 1,
                        "symbol": ""
                    },
                    "output": {
                        "state": 2,
                        "head-move": "left"
                    }
                },
                {
                    "label": "left summand",
                    "input": {
                        "state": 0,
                        "symbol": "1"
                    }
                }
            ]
        }
    }
}