// ************************************************************************** // // // // eses eses // // eses eses // // eses eseses esesese eses Embedded Systems Group // // ese ese ese ese ese // // ese eseseses eseseses ese Department of Computer Science // // eses eses ese eses // // eses eseses eseseses eses University of Kaiserslautern // // eses eses // // // // ************************************************************************** // // The following implements a causal variant of the followed-by operator of // // the language SIGNAL. It copies the stream x2 except for its first value // // that is replaced with the value that x1 has at that time. This value might // // be absent as well, and therefore the clock of y is only almost clk(x2)). // // ************************************************************************** // macro val(x) = x.0; macro clk(x) = x.1; module Fby(event (int * bool) x1,x2,y) { // await trigger event immediate await(clk(x2) or clk(y)); // ensure clock consistency if(clk(x1)) emit(clk(y)); // produce output values val(y) = val(x1); pause; loop { // await trigger event if(clk(x2) or clk(y)) { // ensure clock consistency emit(clk(x2)); emit(clk(y)); // produce output values val(y) = val(x2); } // negative clock information if(!clk(x2) or !clk(y)) { // ensure clock consistency clk(x2) = false; clk(y) = false; } pause; } }