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