// ************************************************************************** // // // // 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 module shows that delayed assignments on local variables that are // // executed at termination time of the local declaration have no effect, // // hence, they are dead code. // // ************************************************************************** // module Schizo00(nat{4} !y) { loop { nat{4} x; y = x; // y receives the default value of x next(x) = 2; w1: pause; y = x; // y will be 2 w2: pause; next(x) = 3; // this is dead code! } } satisfies { step0: assert (y==0); step1: assert A G((y==0) -> X(y==2)); step2: assert A G((y==2) -> X(y==0)); }