Check GLSM state machine for correctness

[d-lowl]

• Must terminate (eventually potentially reach termination state)
• Must be fully connected
• Must not have transitions from the final state