// ************************************************************************** // // // // 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 // // // // ************************************************************************** // // A simple program to test the immediate and delayed assignments done in the // // surface work correctly. // // ************************************************************************** // module Schizo04(nat{4} a) { a = 1; loop { nat{4} c; c = a; next(c) = c+2; w: pause; a = c+1; } } satisfies { s1 : assert (a==1); s2 : assert A X (a==4); s3 : assert A X X (a==7); }