Verify scheduler data structure

• The refinement type for message is also changed to use the ID which is generated from the arrival sequence.
• Verify two functions in the scheduler.h file that enqueue and dequeue messages.