// ************************************************************************** // // 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 // // ************************************************************************** // // Checking the Collatz Conjecture // // Given an arbitrary natural number a_0 compute the following series of // numbers a_n where a_{n+1} := a_n div 2 for even a_n and // a_{n+1} := 3*a_n+1 for odd a_n. It has to be checked that for all numbers // a_0, the sequence of numbers finally ends in 1 (except for a_0=0, // which ends in 0). // // ************************************************************************** macro size = 256; macro odd(y) = y % 2 == 1; module Collatz( nat{size} x, y, event !ready ) { y = x; do { if( odd(y) ) next(y) = 3*y+1; else next(y) = y/2; pause; } while( y!=1 and y!=0 ); emit(ready); } satisfies { termination: assert A F ready; }