// **************************************************************************
//
//    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;
}