// ************************************************************************** // // // // 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 // // // // ************************************************************************** // // First, 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. // // In addition to Schizo00, an immediate assignment that is executed in the // // surface of a local declaration and that overlaps with the assignment // // next(x) := 3 at termination time, does NOT yield a write conflict. // // ************************************************************************** // module Schizo01(nat{4} !y) { loop { nat{4} x; y = x; // y receives the default value of x x = 1; next(x) = 2; w1: pause; y = x; // y will be 2 w2: pause; next(x) = 3; // this is dead code! } } satisfies { step0: assert (y==1); step1: assert A G((y==0) -> X(y==2)); step2: assert A G((y==2) -> X(y==1)); }