Translating the CDL input to a SPIN program:

The local variable semaphore becomes global (global_semaphore_0).
The local variable state becomes global (global_state_0).
The local variable state becomes global (global_state_1).