Semaphore - core to smv
#######################

Program description:
--------------------

This program uses a variable semaphore to implement mutual exclusion between two asynchronous processes.
Each process has four states: idle , entering , critical and exiting.
The entering state indicatesthat the process wants to enter its critical region.
If the variable semaphore is false , it goes to the critical state and sets semaphore to true.
On exiting its critical region , the process assigns semaphore to false again.


Translation comments:
---------------------

- Because of user_state being an internal variable of the USER module there are 2 global variables in the smv program - 
  user_state and user_state_USER and their type in smv is the definition of the user defined type in core (state).
- The default entries of user_state user_state_USER and semaphore cases are the current value of the variables, because the 
  HOLD_PREVIOUS flag is on.