Translating the CDL input to a SPIN program:

The type 'digit' becomes 'byte'.
The integer variable input is not initialized in the input program.
In the SPIN program its initial value is 0.
A non deterministic assignment is required for a variable of type integer,
but it's not implemented!