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