Promela model for call_process