Translating the CDL input to a SPIN program:

A non deterministic assignment is required for a variable of type integer,
but it's not implemented!
A non deterministic assignment is required for a variable of type integer,
but it's not implemented!
A non deterministic assignment is required for a variable of type integer,
but it's not implemented!
A non deterministic assignment is required for a variable of type integer,
but it's not implemented!
A non deterministic assignment is required for a variable of type integer,
but it's not implemented!
A non deterministic assignment is required for a variable of type integer,
but it's not implemented!
A non deterministic assignment is required for a variable of type integer,
but it's not implemented!
A non deterministic assignment is required for a variable of type integer,
but it's not implemented!
A non deterministic assignment is required for a variable of type integer,
but it's not implemented!
A non deterministic assignment is required for a variable of type integer,
but it's not implemented!