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

Dr.Elham Mahmoudzadeh