// ************************************************************************** // // // // 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 program below has cyclic dependencies that can not be resolved. The // guarded actions are: // // i1&o1 => o2 = True // i2&o2 => o1 = True // // ************************************************************************** // module P21(event ?i1,?i2,o1,o2) { { if(o1 & i1) emit(o2); || if(o2 & i2) emit(o1); } assert(!o1 & !o2); //but not causal for i1=i2=true } drivenby drv0 { i1 = false; i2 = false; } drivenby drv1 { i1 = false; i2 = true; } drivenby drv2 { i1 = true; i2 = false; } drivenby drv3 { i1 = true; i2 = true; }