// **************************************************************************
//
//    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 Quartz file describes the Chinese Ring Puzzle which can be
//  stated as follows: Assume there is a safe box that has n knobs
//  k[0],...,k[n-1] such that each knob k[i] has only two possible
//  positions: open (false) or close (true). The knobs can be turned
//  independently:
//      (1) initially, all knobs are in their closed position
//      (2) the leftmost knob k[n-1] can always be turned
//      (3) if one does not choose k[n-1], then the only other knob
//          that can be turned is the one directly to the right of
//          the first closed knob from the left
//      (4) if the last knob k[0] is the only one in the closed
//          position, then the above rule does not apply and the
//          only choice left is to turn k[n-1]
//      (5) at each point of time, only one knob can be turned
//
//  It is to be shown that from the initial position, there is a
//  sequence to bring all knobs in the open position. As explained
//  in [ScKr97a], each state has either two transitions due to
//  rules (2) and (3) or only one due to (2) and (4).
//
//  It has been proved in [ScKr97a] that for n knobs, the minimal
//  length sequence to open the safe box has a length len(n) defined
//  as follows:
//      - if n is odd,  then len(n) := (2/3)*(2^n-0.5)
//      - if n is even, then len(n) := (2/3)*(2^n-1.0)
//  Hence, the diameter of the module grows with O(2^n), which is
//  also the growth of the number of states.
//
// **************************************************************************

macro size = 4;

module ChineseRing(
    bool ?leftmost,
    [size]bool knob, left
) {
    for(i=0..size-1)
        knob[i] = true;
    always {
        if(leftmost)
            next(knob[size-1]) = not(knob[size()-1]);
        else {
            // define: left[i] holds iff all knob[n-1]..knob[i] are false
            left[size-1] = !knob[size()-1];
            for(i=0 .. size-2)
                left[(size-2)-i] = left[(size()-1)-i] & !knob[(size()-2)-i];
            // now turn knob[i] where left[i+2] & !left[i+1] holds
            for(i=0 .. size-3)
                if(left[i+2] & !left[i+1])
                    next(knob[i]) = not(knob[i]);
                if(knob[size-1])
                    next(knob[size-2]) = not(knob[size()-2]);
        }
    }
} satisfies {
    // the safe box can be opened
    opening_sequence_exists[ProveA]: assert
        E F forall(j=0..size-1) not(knob[j]);
    // this specification is intensionally false as it is used to
    // determine a counterexample to open the safe box
    opening_sequence_does_not_exist[DisProveA]: assert
        A G exists(j=0..size-1) knob[j];
}