// ************************************************************************** // // // // 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 is a variation of Edward's variation of Gonthier's program. // // In contrast to Edward's program, we use state variables below. // // ************************************************************************** // module Schizo07(event !out_11,!out_10,!out_01,!out_00) { loop { event x1; weak abort { p1: pause; emit(x1); } || loop { event x2; weak abort { p2: pause; emit(x2); } || loop { bool a,b; a = x1; b = x2; p3: pause; case ( a & b) do emit(out_11); ( a & !b) do emit(out_10); (!a & b) do emit(out_01); (!a & !b) do emit(out_00); default nothing; } when(x2); } when(x1); } } satisfies { initial : assert !out_11 & !out_10 & !out_01 & !out_00; after : assert A G A X (!out_11 & !out_10 & !out_01 & out_00); }