Promela model for event queue

process_run
1 typedef event_data {
2 mtype: process_event_t ev;
3 mtype: process_data_t data;
4 int p;
5 }
6 event_data events[PROCESS_CONF_NUMEVENTS];

Structure of event queue

Promela model of event queue
https://people.iut.ac.ir/en/mahmoudzadeh/promela-model-event-queue