// ************************************************************************** // // 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 // // ************************************************************************** module IncDecAdd( int ?x, ?y, x_sum, x1, y1 ) { x1 = x; y1 = y; x_sum = x+y; while (x1>0) { next(x1) = x1-1; next(y1) = y1+1; ell1:pause; } while (x1<0) { next(x1) = x1+1; next(y1) = y1-1; ell2:pause; } } satisfies { s1 : assert A F terminate; s2 : assert A G (terminate -> (y1==x_sum)); s3 : assert A [(y1==x_sum) SW terminate]; }