// ************************************************************************** //
//                                                                            //
//    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                                             //
//                                                                            //
// ************************************************************************** //
// This is an unrolling of Rivest with N=3 together with an acyclic version.  //
// ************************************************************************** //

module Rivest03(event [3]bool ?x, event [6]bool y) {
    loop{
        y[0] = x[0]&y[5];
        y[1] = x[1]|y[0];
        y[2] = x[2]&y[1];
        y[3] = x[0]|y[2];
        y[4] = x[1]&y[3];
        y[5] = x[2]|y[4];
        assert(y[0] == (x[0]&x[2] | x[0]&x[1]));
        assert(y[2] == (x[1]&x[2] | x[0]&x[2]));
        assert(y[4] == (x[0]&x[1] | x[1]&x[2]));
        assert(y[1] == (x[1] | x[0]&x[2]));
        assert(y[3] == (x[0] | x[1]&x[2]));
        assert(y[5] == (x[2] | x[0]&x[1]));
        pause;
    }
}
drivenby {
    bv{3} w;
    for(i=0..7) {
        pause;
        w = nat2bv(i,3);
        for(j=0..2)
            x[j] = w{j};
    }
}