// ************************************************************************** // // // // 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 condition of the conditional statement yields top.// // However, both the "then" and "else" branch perform the "same" assignment. // // 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 CondStat5(nat b,c,d) { nat a; b = 1; c = 1; if(5/a==1) d = b; else d = c; } drivenby { nothing; }