Promela model for main()

1	main(void)
2	{
3	process_init();
4	procinit_init();
5	/* Main scheduler loop */
6	while(1) {
7	process_run();
8	}
9
10	return 0;
11	}

1	active proctype main()
2	{ int tmp;
3	chan ret_chan = [0] of int;
4	do
5	:: run process_run(ret_chan);
6	ret_chan ? tmp;
7	od;
8	}

Contiki-rcb-main based on Contiki's source code

Promela model of main()