// ************************************************************************** // // // // 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 // // // // ************************************************************************** // // In the module below, the value of the local variable "a" is not known. // // Thus, the conditional statement can neither execute its "then" nor its // // "else" branch. Even though the branches would both assign d the value 1, // // the program cannot be executed. The generated guarded actions are as // // follows: // // a => a = True // // True => b = 1 // // True => c = 1 // // a => d = b // // !a => d = c // // ************************************************************************** // module CondStat4(nat b,c,d) { event a; if(a) emit(a); b = 1; c = 1; if(a) d = b; else d = c; } drivenby { nothing; }