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