Core    to    Smv   
Mutual Exclusion