blob: abd6794b0b3ed3a787b405ab0c3f1ef4bc42901b (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
255
256
257
258
259
260
261
262
|
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;
}
}
}
|
