// **************************************************************************
//
//    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
//
// **************************************************************************
//
//  2x2x2 Rubik's cube (just count reachble states)
//
//  the cube has 3674160 configurations, which can be reached in
//  14 basic moves
//
// **************************************************************************

macro red = 0;
macro blue = 1;
macro green = 2;
macro yellow = 3;
macro orange = 4;
macro white = 5;

module Rubik(
    event ?turnleft, ?turnfront,
    [4]nat{6} front, back,
    [4]nat{6} left,  right,
    [4]nat{6} top,   bot
) {
    // initialisation
    for(i=0..3) next(front[i]) = red;
    for(i=0..3) next(back[i]) = blue;
    for(i=0..3) next(left[i]) = green;
    for(i=0..3) next(right[i]) = yellow;
    for(i=0..3) next(top[i]) = orange;
    for(i=0..3) next(bot[i]) = white;

    // it is sufficient to consider three moves

    always {
        if(turnleft) {
            next(left[0])  = left[2];
            next(left[1])  = left[0];
            next(left[2])  = left[3];
            next(left[3])  = left[1];
            next(back[3])  = bot[0];
            next(back[1])  = bot[2];
            next(top[0])   = back[3];
            next(top[2])   = back[1];
            next(front[0]) = top[0];
            next(front[2]) = top[2];
            next(bot[0])   = front[0];
            next(bot[2])   = front[2];
        } else if(turnfront) {
            next(front[0]) = front[2];
            next(front[1]) = front[0];
            next(front[2]) = front[3];
            next(front[3]) = front[1];
            next(left[3])  = bot[1];
            next(left[1])  = bot[0];
            next(top[2])   = left[3];
            next(top[3])   = left[1];
            next(right[0]) = top[2];
            next(right[2]) = top[3];
            next(bot[0])   = right[2];
            next(bot[2])   = right[0];
        } else {
            next(top[0])   = top[2];
            next(top[1])   = top[0];
            next(top[2])   = top[3];
            next(top[3])   = top[1];
            next(left[0])  = front[0];
            next(left[1])  = front[1];
            next(back[1])  = left[1];
            next(back[0])  = left[0];
            next(right[1]) = back[1];
            next(right[0]) = back[0];
            next(front[0]) = right[0];
            next(front[1]) = right[1];
        }
    }
}