// ************************************************************************** // // 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 Termination1( int ?x, y ) { y = x; while(y>0) { next(y) = y-1; ell:pause; } } satisfies { s1 : assert A F terminate; }