module STimer ( RUNNING process running, READY queue ready, BLOCKED queue period_yield, BLOCKED queue blocked ) { process = { // bool flag_period; /************/ time start; time execution_time; /************/ /*persistant*/ timer /*timerA*/ reload; int reload_capacite; // should be in timerA requires time deadline; } /* timerA = { int reload_capacite; }*/ int capacite = 0; time serveur_period = ticks_to_time(0); void parent_update_deadline(time); time dead = ticks_to_time(0); handler (event e) { On unblock.timer.reload { dead = now() + serveur_period; /*if(alive(e.target))*/ { e.target/*.reload*/.reload_capacite = time_to_ticks(e.target.execution_time); e.target.execution_time = ticks_to_time(0); /* reload the timer combined with the process e.target */ start_relative_timer(e.target.reload,dead); // e.target.flag_period = false; } //recharge la capacité du serveur en fonction du la consommation de e.target capacite += e.target./*reload.*/reload_capacite;//e.target shouldn't be here if (capacite > 0) { foreach(p in period_yield) { p => ready; } parent_update_deadline(dead); } } On system.clocktick { // timer interrupt next(); if(capacite > 0) { capacite--; } if(capacite <= 0) { if (!empty(running)) { running => period_yield; running.execution_time += now()-e.target.start; } foreach(p in READY) { p => period_yield; } } } } interface = { void attach(requires process p) { p.start = now(); p.execution_time = ticks_to_time(0); p.reload_capacite = 0; next(); } void set_serveur_period (int sp) { serveur_period = ticks_to_time(sp); } void set_serveur_capacite (int cp) { capacite = cp; } } transition(process p1) = { /* On yield*; On block*; On preempt */ Before running => READY, blocked { p1.execution_time += now()-p1.start; if(!empty(ready)) { process p = select(); if(p.deadline != p1.deadline) { parent_update_deadline(p.deadline); } } } /* On process.end, detach */ On blocked => TERMINATED { p1.execution_time += now()-p1.start; p1/*.reload*/.reload_capacite = time_to_ticks(p1.execution_time); } /* On unblock.nonpreemptive, unblock.preemptive */ Before blocked => ready { if (empty(running) && empty(ready)) { parent_update_deadline(p1.deadline); } } After READY => running { running.start = now(); } } }