// ************************************************************************** //
//                                                                            //
//    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=5 together with an acyclic version.  //
// ************************************************************************** //


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