/* computes the elapsed computation time within the current period */ module ElapsedTime(RUNNING process running, BLOCKED queue period_yield, BLOCKED queue blocked) { process = { time start_time; time elapsed_time; requires timer end_period; } handler (event e) { // code under tests should be done with aspects On unblock.preemptive { if (e.target in blocked && !empty(running)) { running.elapsed_time += now() - running.start_time; running.start_time = now(); } next(); } On unblock.timer.end_period { e.target.elapsed_time = ticks_to_time(0); e.target.start_time = now(); if (e.target in period_yield && !empty(running)) { running.elapsed_time += now() - running.start_time; running.start_time = now(); } next(); } } interface = { void attach (requires process p) { p.elapsed_time = ticks_to_time(0); p.start_time = now(); next(); } } transition(process p) = { Before running => READY, BLOCKED { p.elapsed_time += (now() - p.start_time); } On READY => running { p.start_time = now(); } } }