// ************************************************************************** //
//                                                                            //
//    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 constructive cyclic program is due to Riedel [Ried04]. The assertions //
// indicate an equivalent acyclic version.                                    //
// ************************************************************************** //


module Riedel2(event ?x1,?x2,?x3,y1,y2,y3,y4) {
    always{
        y1 = x2 & x3 | !x2 & !y2;
        y2 = x1 & x3 |  x2 & !y3;
        y3 = x1 & !y1 | x2 & y1 | !x3 & !y4;
        y4 = x1 & !x2 | !y1 | x2 & !y2;
        assert(y1 == (!x2 & !x3 | !x1 & x3 | x2 & x3));
        assert(y2 == (!x1 & x2 & !x3 | x1 & x3));
        assert(y3 == (!x2 & (x1 <-> x3) | x2 & (x1 | x3)));
        assert(y4 == (!x2 & x1 | x2 & !(x1 & x3)));
    }
}
drivenby {
    bv{3} w;
    for(i=0..7) {
        pause;
        w = nat2bv(i,3);
        x1 = w{0};
        x2 = w{1};
        x3 = w{2};
    }
}