Improve promela model with non-critical section