Translating the CDL input to a SPIN program:

The type 'state' becomes 'byte'.