File content as of revision 0:6477530de2c0:

/* VMachine */
void VMachine(void const *i)
{
    int CurrentState = VMACHINE_INITIAL;
    RtosTimer local_timer = RtosTimer(VMachine_timer, osTimerPeriodic,(void *)0);
    local_timer.start(1);
    while (true) {
        switch (CurrentState) {
            case VMACHINE_AEVENT:
                if(VMachine_clock >= AVI && global_time >= CURRENT_URI) {
                    SyncStatus[VPACE] = agre_time;
                    CurrentState = VMACHINE_INITIAL;
                    pc.printf("VPace ");
                    pc.printf("Time: %ld", agre_time);
                    pc.printf("\n");
                }
                break;
            case VMACHINE_INTER:
                if (global_time >= CURRENT_URI){
                    SyncStatus[VPACE] = agre_time;
                    CurrentState = VMACHINE_INITIAL;
                    pc.printf("VPace ");
                    pc.printf("Time: %ld", agre_time);
                    pc.printf("\n");
                }
                break;
        }
        for(int trn=10; trn<=16; trn++) {
            if(TRANS[trn].source == CurrentState){
                TRANS[trn].active = true;
            }else{
                TRANS[trn].active = false;
            }
            if(TRANS[trn].active) {
                if(EVAL_GUARD(trn)) {
                    if(TRANS[trn].syncid == NONE || agre_time - SyncStatus[TRANS[trn].syncid] < Broadcase_delay) {
                        CurrentState = TRANS[trn].dest;
                        ASSIGN(trn);
                    }
                }
            }
        }
    }
}