// ************************************************************************** // // // // 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 Gonthier03(event !out_111,!out_110,!out_101,!out_100, !out_011,!out_010,!out_001,!out_000) { loop { event x1; weak abort { p1: pause; emit(x1); } || loop { event x2; weak abort { p2: pause; emit(x2); } || loop { event x3; weak abort { p3: pause; emit(x3); } || loop { case (!x1 & !x2 & !x3) do emit(out_000); (!x1 & !x2 & x3) do emit(out_001); (!x1 & x2 & !x3) do emit(out_010); (!x1 & x2 & x3) do emit(out_011); ( x1 & !x2 & !x3) do emit(out_100); ( x1 & !x2 & x3) do emit(out_101); ( x1 & x2 & !x3) do emit(out_110); ( x1 & x2 & x3) do emit(out_111); default nothing; p4: pause; } when(x3); } when(x2); } when(x1); } } satisfies { spec_out_000 : assert A G A X out_000; spec_out_001 : assert A G A X !out_001; spec_out_010 : assert A G A X !out_010; spec_out_011 : assert A G A X !out_011; spec_out_100 : assert A G A X out_100; spec_out_101 : assert A G A X !out_101; spec_out_110 : assert A G A X out_110; spec_out_111 : assert A G A X out_111; }