// ************************************************************************** // // // // 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 // // // // ************************************************************************** // // This program goes back to Gontier's PhD thesis. It shows that a local // // variable can generate arbitrarily many reincarnations if its declaration // // is nested within loops and abortions. Gontier's original program is given // // also in [Berr99,page 138] as program P18. // // ************************************************************************** // module Gonthier01(event !out_1,!out_0) { loop { event x1; weak abort { w1: pause; emit(x1); } || loop { if(x1) emit(out_1); else emit(out_0); w2: pause; } when(x1); } } satisfies { spec_out_0 : assert A G A X out_0; spec_out_1 : assert A G A X out_1; }