macro Size = 4; module SortArray(event int ?x_in,!y_out) { [Size]int u,v; { // end cell loop { next(v[0]) = u[0]; pause; } || for(i=0..Size-2) do || loop { if(v[i]<u[i+1]) { next(v[i+1]) = v[i]; next(u[i]) = u[i+1]; } else { next(v[i+1]) = u[i+1]; next(u[i]) = v[i]; } pause; } || loop { if(v[Size-1]<x_in) { next(y_out) = v[Size-1]; next(u[Size-1]) = x_in; } else { next(y_out) = x_in; next(u[Size-1]) = v[Size-1]; } pause; } } } drivenby { x_in = 4; pause; x_in = -1; // dummy value pause; x_in = 3; pause; x_in = -1; // dummy value pause; x_in = 1; pause; x_in = -1; // dummy value pause; x_in = 2; pause; x_in = -1; // dummy value pause; for(i=0..6) { x_in = 10; pause; } }