system earthquake;

resource CPU;
resource buffer;
resource data_exp;

/*
 * M O D E L E R
 *
 */

process modeler(1);

var x_m clock;

state sleeping_m #start ;
  deadline eager;
    informal "arrive_m";
    nextstate waiting_c; 
endstate;

state waiting_c;
  deadline eager;
  acquire CPU;
    informal "compute";
    set x_m := 0;
    nextstate computing;
endstate;

state computing;
  deadline delayable;
  when x_m >= 23 and x_m <= 25;
    informal "computed";
    reset x_m;
    release CPU;
    nextstate waiting_u;
endstate;

state waiting_u;
  deadline eager;
  acquire CPU, buffer;
    informal "update";
    set x_m := 0;
    nextstate updating;
endstate;

state updating;
  deadline delayable;
  when x_m = 10;
    informal "updated";
    reset x_m;
    release CPU, buffer;
    task ({data}0).updated := true;
    nextstate sleeping_m;
endstate;
endprocess;

/*
 * D A T A
 *
 */

process data(1);

var updated boolean := false public;
var y clock;

state start #start ; 
    set y := 0;
    nextstate fresh;
endstate;

state fresh;
  deadline eager;
  provided updated;
    informal "refresh";
    set y := 0;
    task updated := false;
    nextstate fresh;

  deadline eager;
  acquire data_exp;
  when y >= 130;
    informal "expire";
    nextstate expired;
endstate;

state expired;
  deadline eager;
  provided updated;
    informal "refresh";
    release data_exp;
    set y := 0;
    task updated := false;
    nextstate fresh;
endstate;

endprocess;

/*
 * P U L S E R
 *
 */

process pulser(1);

var x_p clock;
var t_p clock;

state start #start ;
    set t_p := 0;
    nextstate sleeping_p; 
endstate;

state sleeping_p;
  deadline eager;
  when t_p >= 32 and t_p <= 145;
    informal "arrive_p";
    set t_p := 0;
    nextstate waiting_r;
endstate;

state waiting_r;
  deadline eager;
  acquire CPU, buffer, data_exp;
  when t_p <= 85;
    informal "read";
    set x_p := 0;
    nextstate reading;

  
  deadline eager;
  when t_p >= 86;
    informal "error";
    nextstate waiting_r;
endstate;

state reading;
  deadline delayable;
  when x_p = 2 and t_p <= 87;
    informal "write";
    release buffer, data_exp;
    set x_p := 0;
    nextstate writing;
endstate;

state writing;
  deadline delayable;
  when x_p = 58 and t_p <= 145;
    informal "written";
    release CPU;
    reset x_p;
    nextstate sleeping_p;
endstate;

endprocess;

endsystem;