open Printf;; (* This program generates the Lustre model for the movements of the 2 + 1 configs. n.b. using ocaml as a "meta" language is confortable: symmetry classes are computed with a straightforward (and thus highly reliable ?) algo, while "computing" them by hand whould have been tedious and error-prone ! *) let code (xd,yd) (xu,yu) = let uu = 3*yu + xu in let dd = 3*yd + xd in (9*dd + uu) let sdd (x,y) = (y,x) let sdi (x,y) = (2-y,2-x) let sho (x,y) = (x,2-y) let sve (x,y) = (2-x,y) (* computes the canonical class of a config *) let rec cano d u = let cc = code d u in let min = ref None in (* Printf.printf "(%d,%d) (%d,%d) -> %d\n" (fst d) (snd d) (fst u) (snd u) cc; *) if (code (sdd d) (sdd u)) < cc then ( let m = (cano (sdd d) (sdd u)) in match !min with | None -> min := Some m | Some m' -> assert (m = m') ); if (code (sdi d) (sdi u)) < cc then ( let m = cano (sdi d) (sdi u) in match !min with | None -> min := Some m | Some m' -> assert (m = m') ); if (code (sho d) (sho u)) < cc then ( let m = cano (sho d) (sho u) in match !min with | None -> min := Some m | Some m' -> assert (m = m') ); if (code (sve d) (sve u)) < cc then ( let m = cano (sve d) (sve u) in match !min with | None -> min := Some m | Some m' -> assert (m = m') ); match !min with | Some m -> m | None -> (* Printf.printf "MINIMAL (%d,%d) (%d,%d) -> %d\n" (fst d) (snd d) (fst u) (snd u) cc; *) (d,u) let i2xy i = (i mod 3, i / 3) let xy2i (x,y) = x + 3*y let tab : (int, ((int*int)*(int*int)) list) Hashtbl.t = Hashtbl.create 20 ;; let addtab cc d u = ( let old = try Hashtbl.find tab cc with Not_found -> [] in Hashtbl.replace tab cc ((d,u)::old) ) let ptab () = ( Printf.printf "--- %d classes ---\n" (Hashtbl.length tab); let pen cc dul = ( let pc (d,u) = Printf.printf "[(%d,%d)-(%d,%d)] " (fst d) (snd d) (fst u) (snd u) in Printf.printf "code:%02d " cc; List.iter pc dul; Printf.printf "\n" ) in Hashtbl.iter pen tab ) let declist = ref [] let _ = ( for dd = 0 to 8 do for uu = 0 to 8 do if (uu <> dd) then ( let (dx,dy) = i2xy dd in let (ux,uy) = i2xy uu in let (cd,cu) = cano (dx,dy) (ux,uy) in let cc = code cd cu in declist := (dd,uu,cc)::!declist; (* printf " if (d[%d] and u[%d]) then class%02d else\n" dd uu cc; Printf.printf "(%d,%d) (%d,%d) EQUIV (%d,%d) (%d,%d) = classe %d\n" dx dy ux uy (fst cd) (snd cd) (fst cu) (snd cu) cc; *) addtab cc (dx,dy) (ux,uy) ) ; done done ) (* let _ = ptab () *) let nbclasses = Hashtbl.length tab let _ = ( printf " include \"UsrIntBinary4.lus\" include \"UsrIntBinary.lus\" include \"BoolArrays.lus\" "; printf "type config = bool^9;\n"; printf "const cls_sz = %d;\n" (nbclasses+1); printf "type classe = bool^cls_sz;\n"; let rec pb i v = match i with | 0 -> () | _ -> printf ",%s" v; pb (i-1) v in printf "const bad_class = [true "; pb nbclasses "false"; printf "];\n"; let cpt = ref 0 in let pen cc _ = ( printf "const class%02d = [false " cc; pb !cpt "false"; pb 1 " true"; pb (nbclasses - !cpt -1) "false"; printf "];\n"; incr cpt ) in Hashtbl.iter pen tab ) let _ = ( printf "node cano(d,u: config) returns (c: classe);\n"; printf "let\n c = \n"; let pe (dd, uu, cc) = printf " if (d[%d] and u[%d]) then class%02d else\n" dd uu cc in List.iter pe (List.rev !declist); printf " bad_class;\ntel\n" ) (* from now on, simply flush the rest of the program *) let _ = ( printf " node isconfig(d, u: bool^9) returns (ok: bool); let ok = ba_exact(1,9,d) and ba_exact(1,9,u) and ba_exact(2,9,d or u); tel node model ( d0, u0 : bool^9; -- initial config m1, p1, m3, p3: bool; -- rand moves ) returns ( ok: bool; d, u : bool^9; viewed : bool^9; cls, cls2: classe ); var previewed : bool^9; stuck: bool; count: UsrInt; move: bool; pd, pu: bool^9; m1u, p1u, m3u, p3u : bool^9; let (* freeze everything as soon as stuck *) viewed = if stuck then previewed else (d or u or previewed); previewed = (d0 or u0) -> pre viewed; (* compute encountred classes, once and twice *) cls = cano(d, u) or (cano(d0, u0) -> pre cls); cls2 = (false^cls_sz -> pre cls2) or (move^cls_sz and cano(d, u) and (cano(d0, u0) -> pre cls)); pd = d0 -> pre d; pu = u0 -> pre u; m1u = ba_left_shift(1,9,pu); p1u = ba_right_shift(1,9,pu); m3u = ba_left_shift(3,9,pu); p3u = ba_right_shift(3,9,pu); (* apply moves (if possible) *) (d, u, move) = if (false -> pre stuck) then (pd, pu, false) else if (isconfig(pd, m1u) and m1) then (pd, m1u, true) else if (isconfig(pd, p1u) and p1) then (pd, p1u, true) else if (isconfig(pd, m3u) and m3) then (pd, m3u, true) else if (isconfig(pd, p3u) and p3) then (pd, p3u, true) else (pd, pu, false); stuck = not ba_all(cls_sz,not cls2); count = if (stuck and not (false -> pre stuck)) then ba_count(9, viewed) else (UsrInt_0 -> pre count); (* invariant to check: whenever some class has been encountered twice, the number of viewed mode is less than 7 n.b. count includes the 2 initial nodes d0 and u0, thus it meens ``new nodes <= 4'' *) ok = stuck => UsrIntLt(count, UsrInt_7); tel (* Full proof program, starting from any valid init config - too heavy for the tool lesar (bdd explotion) - works fine with gbac *) node proof(d0, u0: config; m1, p1, m3, p3: bool) returns (ok: bool); var d, u : bool^9; viewed: bool^9; cls, cls2: bool^cls_sz; let assert isconfig(d0, u0); ok, d, u, viewed, cls, cls2 = model(d0, u0, m1,p1,m3,p3); tel (* a test program, to use with luciole *) node test( m1, p1, m3, p3: bool; ) returns ( ok: bool; d, u : bool^9; vus: bool^9; cls: bool^cls_sz; cls2: bool^cls_sz ); let ok, d, u, vus, cls, cls2 = model( [true]|false^8, [false,true]|false^7, m1,p1,m3,p3); tel "; ) let c2lus xy = ( let i = xy2i xy in let rec f i n = if (i = 0) then "true"::(g (n-1)) else "false"::(f (i-1) (n-1)) and g n = if (n = 0) then [] else "false"::(g (n-1)) in let l = f i 9 in String.concat "," l ) (* One proof program for each (canonical) initial config *) let _ = ( let pverif cc dul = ( match (List.rev dul) with | (d,u)::_ -> ( printf "node verif_%02d (" cc; printf " m1, p1, m3, p3: bool ) returns ( ok: bool); var d0, u0, d, u : bool^9; viewed: bool^9; cls, cls2: bool^cls_sz; let ok, d, u, viewed, cls, cls2 = model(d0, u0, m1,p1,m3,p3); "; printf "d0 = [%s];\n" (c2lus d); printf "u0 = [%s];\n" (c2lus u); printf "tel\n"; ) | _ -> assert false ) in Hashtbl.iter pverif tab )