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


nat x_0_0,x_1_0,x_2_0,x_3_0;
nat x_0_3,x_1_3,x_2_3,x_3_3;
thread BitonicSort_4 {
    bool c_0_1_0,c_0_1_2,c_0_3_1,c_1_2_1,c_2_3_0,c_3_2_2;
nat x_0_1,x_1_1,x_2_1,x_3_1;
nat x_0_2,x_1_2,x_2_2,x_3_2;
    c_0_1_0 = x_0_0<x_1_0;
    x_0_1 = (nat)(c_0_1_0&(bool)x_0_0 | (!c_0_1_0)&(bool)x_1_0);
    x_1_1 = (nat)(c_0_1_0&(bool)x_1_0 | (!c_0_1_0)&(bool)x_0_0);
    c_2_3_0 = x_2_0<x_3_0;
    x_2_1 = (nat)(c_2_3_0&(bool)x_2_0 | (!c_2_3_0)&(bool)x_3_0);
    x_3_1 = (nat)(c_2_3_0&(bool)x_3_0 | (!c_2_3_0)&(bool)x_2_0);
    c_0_3_1 = x_0_1<x_3_1;
    x_0_2 = (nat)(c_0_3_1&(bool)x_0_1 | (!c_0_3_1)&(bool)x_3_1);
    x_3_2 = (nat)(c_0_3_1&(bool)x_3_1 | (!c_0_3_1)&(bool)x_0_1);
    c_1_2_1 = x_1_1<x_2_1;
    x_1_2 = (nat)(c_1_2_1&(bool)x_1_1 | (!c_1_2_1)&(bool)x_2_1);
    x_2_2 = (nat)(c_1_2_1&(bool)x_2_1 | (!c_1_2_1)&(bool)x_1_1);
    c_0_1_2 = x_0_2<x_1_2;
    x_0_3 = (nat)(c_0_1_2&(bool)x_0_2 | (!c_0_1_2)&(bool)x_1_2);
    x_1_3 = (nat)(c_0_1_2&(bool)x_1_2 | (!c_0_1_2)&(bool)x_0_2);
    c_3_2_2 = x_3_2<x_2_2;
    x_3_3 = (nat)(c_3_2_2&(bool)x_3_2 | (!c_3_2_2)&(bool)x_2_2);
    x_2_3 = (nat)(c_3_2_2&(bool)x_2_2 | (!c_3_2_2)&(bool)x_3_2);
}