ChangeVarNameInModule The Transitions of The Flattened Core Program: Transition number 10, original name: RETURN_TO_IDLE_AND_FREE_SEMAPHORE vars changed by assign: user_state semaphore vars changed by relation: Transition number 9, original name: NON_DETERMINISTIC_CRITICAL_OR_EXITING vars changed by assign: user_state vars changed by relation: Transition number 8, original name: ENTERING_BUT_SEMAPHOR_IS_TRUE vars changed by assign: user_state vars changed by relation: Transition number 7, original name: ENTERING_AND_SEMAPHOR_IS_FALSE vars changed by assign: user_state semaphore vars changed by relation: Transition number 6, original name: NON_DETERMINISTIC_IDLE_OR_ENTERING vars changed by assign: user_state vars changed by relation: Transition number 5, original name: NON_DETERMINISTIC_IDLE_OR_ENTERING_USER vars changed by assign: user_state_USER vars changed by relation: Transition number 4, original name: ENTERING_AND_SEMAPHOR_IS_FALSE_USER vars changed by assign: user_state_USER semaphore vars changed by relation: Transition number 3, original name: ENTERING_BUT_SEMAPHOR_IS_TRUE_USER vars changed by assign: user_state_USER vars changed by relation: Transition number 2, original name: NON_DETERMINISTIC_CRITICAL_OR_EXITING_USER vars changed by assign: user_state_USER vars changed by relation: Transition number 1, original name: RETURN_TO_IDLE_AND_FREE_SEMAPHORE_USER vars changed by assign: user_state_USER semaphore vars changed by relation: New types in core program: state with definition of enum Variable user_state_USER is of type state. Variable user_state is of type state. The Variables of the Flattened Program: Variable name: semaphore Transitions that change variable by assign: 1 4 7 10 Transitions that change variable by relation: Variable name: user_state Transitions that change variable by assign: 6 7 8 9 10 Transitions that change variable by relation: Variable name: user_state_USER Transitions that change variable by assign: 1 2 3 4 5 Transitions that change variable by relation: