// ************************************************************************** // // // // 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 module Schizo has been discussed on SLAP04 as a program // // having a difficult schizophrenic behavior. We show its equivalence to a // // simplified version that has been obtained by job code generation. // // ************************************************************************** // macro range = 4; module SLAP04a(event ?x1,?x2, nat{range} !y) { weak abort loop { nat{range} a; a = 0; weak abort loop { nat{range} b; b = a; next(b)=a+b; pause; y=a; next(a)=a-b; next(b)=a*b; } when(x2); } when(x1); }