helm/software/matita/contribs/formal_topology/bin/theory_explorer.ml

   1 (**** PROFILING ****)
   2 let ok_time = ref 0.0;;
   3 let ko_time = ref 0.0;;
   4
   5 let profile f x =
   6  let before = Unix.gettimeofday () in
   7  let res = f x in
   8  let after = Unix.gettimeofday () in
   9  let delta = after -. before in
  10   if res then
  11    ok_time := !ok_time +. delta
  12   else
  13    ko_time := !ko_time +. delta;
  14   res
  15 ;;
  16
  17 let _ =
  18  Sys.catch_break true;
  19  at_exit
  20   (function () ->
  21     prerr_endline
  22      ("\nTIME SPENT IN CHECKING GOOD CONJECTURES: " ^ string_of_float !ok_time);
  23     prerr_endline
  24      ("TIME SPENT IN CHECKING BAD CONJECTURES: " ^ string_of_float !ko_time);)
  25 ;;
  26
  27 (**** END PROFILING ****)
  28
  29 type rel = Equal | SubsetEqual | SupersetEqual
  30
  31 let string_of_rel =
  32  function
  33     Equal -> "="
  34   | SubsetEqual -> "⊆"
  35   | SupersetEqual -> "⊇"
  36
  37 (* operator *)
  38 type op = I | C | M
  39
  40 let string_of_op = function I -> "i" | C -> "c" | M -> "-"
  41 let matita_of_op = function I -> "i" | C -> "c" | M -> "m"
  42
  43 (* compound operator *)
  44 type compound_operator = op list
  45
  46 let string_of_cop op =
  47  if op = [] then "id" else String.concat "" (List.map string_of_op op)
  48
  49 let dot_of_cop op = "\"" ^ string_of_cop op ^ "\""
  50
  51 let matita_of_cop v =
  52  let rec aux =
  53   function
  54    | [] -> v
  55    | [op] -> matita_of_op op ^ " " ^ v
  56    | op::tl -> matita_of_op op ^ " (" ^ aux tl ^ ")"
  57  in
  58   aux
  59
  60 let name_of_theorem cop rel cop' =
  61  let cop,rel,cop' =
  62   match rel with
  63      Equal -> cop,"eq",cop'
  64    | SubsetEqual -> cop,"leq",cop'
  65    | SupersetEqual -> cop',"leq",cop
  66  in
  67   rel ^ "_" ^
  68    String.concat "" (List.map matita_of_op cop) ^ "_" ^
  69    String.concat "" (List.map matita_of_op cop')
  70 ;;
  71
  72 (* representative, other elements in the equivalence class,
  73    leq classes, geq classes *)
  74 type equivalence_class =
  75  compound_operator * compound_operator list *
  76   equivalence_class list ref * equivalence_class list ref
  77
  78 let (===) (repr,_,_,_) (repr',_,_,_) = repr = repr';;
  79 let (<=>) (repr,_,_,_) (repr',_,_,_) = repr <> repr';;
  80
  81 let string_of_equivalence_class (repr,others,leq,_) =
  82  String.concat " = " (List.map string_of_cop (repr::others)) ^
  83   (if !leq <> [] then
  84     "\n" ^
  85      String.concat "\n"
  86       (List.map
  87         (function (repr',_,_,_) ->
  88            string_of_cop repr ^ " ⊆ " ^ string_of_cop repr') !leq)
  89    else
  90     "")
  91
  92 let dot_of_equivalence_class (repr,others,leq,_) =
  93  (if others <> [] then
  94    let eq = String.concat " = " (List.map string_of_cop (repr::others)) in
  95     dot_of_cop repr ^ "[label=\"" ^ eq ^ "\"];" ^
  96      if !leq = [] then "" else "\n"
  97   else if !leq = [] then
  98    dot_of_cop repr ^ ";"
  99   else
 100    "") ^
 101    String.concat "\n"
 102     (List.map
 103       (function (repr',_,_,_) ->
 104          dot_of_cop repr' ^ " -> " ^ dot_of_cop repr ^ ";") !leq)
 105
 106 (* set of equivalence classes, infima, suprema *)
 107 type set =
 108  equivalence_class list * equivalence_class list * equivalence_class list
 109
 110 let string_of_set (s,_,_) =
 111  String.concat "\n" (List.map string_of_equivalence_class s)
 112
 113 let ps_of_set (to_be_considered,under_consideration,news) ?processing (s,inf,sup) =
 114  let ch = open_out "xxx.dot" in
 115   output_string ch "digraph G {\n";
 116   (match under_consideration with
 117       None -> ()
 118     | Some repr ->
 119        output_string ch (dot_of_cop repr ^ " [color=yellow];"));
 120   List.iter
 121    (function (repr,_,_,_) ->
 122      if List.exists (function (repr',_,_,_) -> repr=repr') sup then
 123       output_string ch (dot_of_cop repr ^ " [shape=Mdiamond];")
 124      else
 125       output_string ch (dot_of_cop repr ^ " [shape=diamond];")
 126    ) inf ;
 127   List.iter
 128    (function (repr,_,_,_) ->
 129      if not (List.exists (function (repr',_,_,_) -> repr=repr') inf) then
 130       output_string ch (dot_of_cop repr ^ " [shape=polygon];")
 131    ) sup ;
 132   List.iter
 133    (function repr -> output_string ch (dot_of_cop repr ^ " [color=green];")
 134    ) to_be_considered ;
 135   List.iter
 136    (function repr -> output_string ch (dot_of_cop repr ^ " [color=navy];")
 137    ) news ;
 138   output_string ch (String.concat "\n" (List.map dot_of_equivalence_class s));
 139   output_string ch "\n";
 140   (match processing with
 141       None -> ()
 142     | Some (repr,rel,repr') ->
 143        output_string ch (dot_of_cop repr ^ " [color=red];");
 144        let repr,repr' =
 145         match rel with
 146            SupersetEqual -> repr',repr
 147          | Equal
 148          | SubsetEqual -> repr,repr'
 149        in
 150         output_string ch
 151          (dot_of_cop repr' ^ " -> " ^ dot_of_cop repr ^
 152           " [" ^
 153           (match rel with Equal -> "arrowhead=none " | _ -> "") ^
 154           "style=dashed];\n"));
 155   output_string ch "}\n";
 156   close_out ch;
 157   (*ignore (Unix.system "tred xxx.dot > yyy.dot && dot -Tps yyy.dot > xxx.ps")*)
 158   ignore (Unix.system "cp xxx.ps xxx_old.ps && dot -Tps xxx.dot > xxx.ps");
 159   (*ignore (read_line ())*)
 160 ;;
 161
 162 (******** communication with matitawiki ************)
 163 let min_ch,mout_ch = Unix.open_process "../../../matitawiki.opt 2> /dev/null";;
 164
 165 let exec_cmd ?(undo=false) s =
 166  let un = if undo then "un" else "" in
 167 (*prerr_endline ("<pgip><" ^ un ^ "doitem>" ^ s ^ "</" ^ un ^ "doitem></pgip>\n");*)
 168  output_string mout_ch ("<pgip><" ^ un ^ "doitem>" ^ s ^ "</" ^ un ^ "doitem></pgip>\n");
 169  flush mout_ch;
 170  let rec aux v =
 171   let l = input_line min_ch in
 172   let last = String.length l - 1 in
 173    assert (last > 0);
 174    if l.[last] = Char.chr 249 then
 175     int_of_string (String.sub l 0 last)
 176    else
 177     aux l
 178  in
 179   aux "x"
 180 ;;
 181
 182 let exec_cmds =
 183  let rec aux undopos =
 184   function
 185      [] -> true
 186    | he::tl ->
 187       let pos = exec_cmd he in
 188        if pos = -1 then
 189         begin
 190          match undopos with
 191             None -> assert false
 192           | Some undopos ->
 193              assert (exec_cmd ~undo:true (string_of_int (undopos - 1)) <> -1);
 194              false
 195         end
 196        else
 197         match undopos with
 198            None -> aux (Some pos) tl
 199          | _ -> aux undopos tl
 200  in
 201   aux None
 202
 203 let _ =
 204  assert (exec_cmd "set \"baseuri\" \"cic:/matita/theory_former\"." <> -1);
 205  assert (exec_cmd "include \"formal_topology.ma\"." <> -1);
 206 ;;
 207
 208 (********* testing a conjecture *******************)
 209
 210 let test to_be_considered_and_now ((s,_,_) as set) rel candidate repr =
 211  ps_of_set to_be_considered_and_now ~processing:(candidate,rel,repr) set;
 212  print_string
 213   (string_of_cop candidate ^ " " ^ string_of_rel rel ^ " " ^ string_of_cop repr ^ "? ");
 214  flush stdout;
 215 (*
 216  assert (Unix.system "cat log.ma | sed s/^theorem/axiom/g | sed 's/\\. intros.*qed\\././g' > xxx.ma" = Unix.WEXITED 0);
 217  let ch = open_out_gen [Open_append] 0 "xxx.ma" in
 218 *)
 219 (*
 220  let i = ref 0 in
 221   List.iter
 222    (function (repr,others,leq,_) ->
 223      List.iter
 224       (function repr' ->
 225         incr i;
 226         output_string ch
 227          ("axiom ax" ^ string_of_int !i ^
 228           ": \\forall A." ^
 229            matita_of_cop "A" repr ^ " = " ^ matita_of_cop "A" repr' ^ ".\n");
 230       ) others;
 231      List.iter
 232       (function (repr',_,_,_) ->
 233         incr i;
 234         output_string ch
 235          ("axiom ax" ^ string_of_int !i ^
 236           ": \\forall A." ^
 237            matita_of_cop "A" repr ^ " ⊆ " ^ matita_of_cop "A" repr' ^ ".\n");
 238       ) !leq;
 239    ) s;
 240 *)
 241   let candidate',rel',repr' =
 242    match rel with
 243       SupersetEqual -> repr,SubsetEqual,candidate
 244     | Equal
 245     | SubsetEqual -> candidate,rel,repr in
 246   let query1 =
 247    let name = name_of_theorem candidate' rel' repr' in
 248    ("theorem " ^ name ^ ": \\forall A." ^ matita_of_cop "A" candidate' ^
 249       " " ^ string_of_rel rel' ^ " " ^
 250       matita_of_cop "A" repr' ^ ".") in
 251   let query2 = "intros;" in
 252   let query3 = "autobatch size=8 depth=3 width=2." in
 253   let query4 = "qed." in
 254   let query = query1 ^ query2 ^ query3 ^ query4 in
 255 (*
 256   output_string ch (query ^ "\n");
 257   close_out ch;
 258 *)
 259   let res = profile exec_cmds [query1; query2; query3; query4] in
 260 (*
 261   let res =
 262    (*Unix.system "../../../matitac.opt xxx.ma >> log 2>&1" = Unix.WEXITED 0*)
 263    profile Unix.system "../../../matitac.opt xxx.ma > /dev/null 2>&1" = Unix.WEXITED 0
 264   in
 265 *)
 266    ignore (Unix.system "echo '(*' >> log.ma && cat xxx.dot >> log.ma && echo '*)' >> log.ma");
 267    let ch = open_out_gen [Open_append] 0o0600 "log.ma" in
 268    if res then
 269     output_string ch (query ^ "\n")
 270    else
 271     output_string ch ("(* " ^ query ^ "*)\n");
 272    close_out ch;
 273    print_endline (if res then "y" else "n");
 274    res
 275
 276 let remove node = List.filter (fun node' -> node <=> node');;
 277
 278 let add_leq_arc ((_,_,leq,_) as node) ((_,_,_,geq') as node') =
 279  leq := node' :: !leq;
 280  geq' := node :: !geq'
 281 ;;
 282
 283 let add_geq_arc ((_,_,_,geq) as node) ((_,_,leq',_) as node') =
 284  geq := node' :: !geq;
 285  leq' := node :: !leq'
 286 ;;
 287
 288 let remove_leq_arc ((_,_,leq,_) as node) ((_,_,_,geq') as node') =
 289  leq := remove node' !leq;
 290  geq' := remove node !geq'
 291 ;;
 292
 293 let remove_geq_arc ((_,_,_,geq) as node) ((_,_,leq',_) as node') =
 294  geq := remove node' !geq;
 295  leq' := remove node !leq'
 296 ;;
 297
 298 let leq_transitive_closure node node' =
 299  add_leq_arc node node';
 300  let rec remove_transitive_arcs ((_,_,_,geq) as node) (_,_,leq',_) =
 301   let rec remove_arcs_to_ascendents =
 302    function
 303       [] -> ()
 304     | (_,_,leq,_) as node'::tl ->
 305        remove_leq_arc node node';
 306        remove_arcs_to_ascendents (!leq@tl)
 307   in
 308    remove_arcs_to_ascendents !leq';
 309    List.iter (function son -> remove_transitive_arcs son node) !geq
 310  in
 311   remove_transitive_arcs node node'
 312 ;;
 313
 314 let geq_transitive_closure node node' =
 315  add_geq_arc node node';
 316  let rec remove_transitive_arcs ((_,_,leq,_) as node) (_,_,_,geq') =
 317   let rec remove_arcs_to_descendents =
 318    function
 319       [] -> ()
 320     | (_,_,_,geq) as node'::tl ->
 321        remove_geq_arc node node';
 322        remove_arcs_to_descendents (!geq@tl)
 323   in
 324    remove_arcs_to_descendents !geq';
 325    List.iter (function father -> remove_transitive_arcs father node) !leq
 326  in
 327   remove_transitive_arcs node node'
 328 ;;
 329
 330 let (@@) l1 n = if List.exists (function n' -> n===n') l1 then l1 else l1@[n]
 331
 332 let rec leq_reachable node =
 333  function
 334     [] -> false
 335   | node'::_ when node === node' -> true
 336   | (_,_,leq,_)::tl -> leq_reachable node (!leq@tl)
 337 ;;
 338
 339 let rec geq_reachable node =
 340  function
 341     [] -> false
 342   | node'::_ when node === node' -> true
 343   | (_,_,_,geq)::tl -> geq_reachable node (!geq@tl)
 344 ;;
 345
 346 exception SameEquivalenceClass of set * equivalence_class * equivalence_class;;
 347
 348 let locate_using_leq to_be_considered_and_now ((repr,_,leq,geq) as node)
 349  set start
 350 =
 351  let rec aux ((nodes,inf,sup) as set) already_visited =
 352   function
 353      [] -> set
 354    | (repr',_,_,geq') as node' :: tl ->
 355        if List.exists (function n -> n===node') already_visited then
 356         aux set already_visited tl
 357        else if repr=repr' then aux set (node'::already_visited) (!geq'@tl)
 358        else if leq_reachable node' !leq then
 359         aux set (node'::already_visited) (!geq'@tl)
 360        else if test to_be_considered_and_now set SubsetEqual repr repr' then
 361         begin
 362          if List.exists (function n -> n===node') !geq then
 363           (* We have found two equal nodes! *)
 364           raise (SameEquivalenceClass (set,node,node'))
 365          else
 366           begin
 367            let sup = remove node sup in
 368            let inf =
 369             if !geq' = [] then
 370              let inf = remove node' inf in
 371               if !geq = [] then
 372                inf@@node
 373               else
 374                inf
 375             else
 376              inf
 377             in
 378              leq_transitive_closure node node';
 379              aux (nodes,inf,sup) (node'::already_visited) (!geq'@tl)
 380           end
 381         end
 382        else
 383         aux set (node'::already_visited) tl
 384  in
 385   aux set [] start
 386 ;;
 387
 388 let locate_using_geq to_be_considered_and_now ((repr,_,leq,geq) as node)
 389  set start
 390 =
 391  let rec aux ((nodes,inf,sup) as set) already_visited =
 392   function
 393      [] -> set
 394    | (repr',_,leq',_) as node' :: tl ->
 395        if List.exists (function n -> n===node') already_visited then
 396         aux set already_visited tl
 397        else if repr=repr' then aux set (node'::already_visited) (!leq'@tl)
 398        else if geq_reachable node' !geq then
 399         aux set (node'::already_visited) (!leq'@tl)
 400        else if (List.exists (function n -> not (leq_reachable n [node'])) !leq)
 401         then
 402          aux set (node'::already_visited) tl
 403        else if test to_be_considered_and_now set SupersetEqual repr repr' then
 404         begin
 405          if List.exists (function n -> n===node') !leq then
 406           (* We have found two equal nodes! *)
 407           raise (SameEquivalenceClass (set,node,node'))
 408          else
 409           begin
 410            let inf = remove node inf in
 411            let sup =
 412             if !leq' = [] then
 413              let sup = remove node' sup in
 414              if !leq = [] then
 415               sup@@node
 416              else
 417               sup
 418             else
 419              sup
 420            in
 421             geq_transitive_closure node node';
 422             aux (nodes,inf,sup) (node'::already_visited) (!leq'@tl)
 423           end
 424         end
 425        else
 426         aux set (node'::already_visited) tl
 427  in
 428   aux set [] start
 429 ;;
 430
 431 let analyze_one to_be_considered repr hecandidate (news,((nodes,inf,sup) as set)) =
 432 if not (List.for_all (fun ((_,_,_,geq) as node) -> !geq = [] && let rec check_sups = function [] -> true | (_,_,leq,_) as node::tl -> if !leq = [] then List.exists (fun n -> n===node) sup && check_sups tl else check_sups (!leq@tl) in check_sups [node]) inf) then ((*ps_of_set ([],None,[]) set;*) assert false);
 433 if not (List.for_all (fun ((_,_,leq,_) as node) -> !leq = [] && let rec check_infs = function [] -> true | (_,_,_,geq) as node::tl -> if !geq = [] then List.exists (fun n -> n===node) inf && check_infs tl else check_infs (!geq@tl) in check_infs [node]) sup) then (ps_of_set ([],None,[]) set; assert false);
 434  let candidate = hecandidate::repr in
 435   if List.length (List.filter ((=) M) candidate) > 1 then
 436    news,set
 437   else
 438    try
 439     let leq = ref [] in
 440     let geq = ref [] in
 441     let node = candidate,[],leq,geq in
 442     let nodes = nodes@[node] in
 443     let set = nodes,inf@[node],sup@[node] in
 444     let set,start_inf,start_sup =
 445      let repr_node =
 446       match List.filter (fun (repr',_,_,_) -> repr=repr') nodes with
 447          [node] -> node
 448        | _ -> assert false
 449      in
 450       match hecandidate,repr with
 451          I, I::_ -> raise (SameEquivalenceClass (set,node,repr_node))
 452        | I, _ ->
 453           add_leq_arc node repr_node;
 454           (nodes,remove repr_node inf@[node],sup),inf,sup
 455        | C, C::_ -> raise (SameEquivalenceClass (set,node,repr_node))
 456        | C, _ ->
 457           add_geq_arc node repr_node;
 458           (nodes,inf,remove repr_node sup@[node]),inf,sup
 459        | M, M::M::_ -> raise (SameEquivalenceClass (set,node,repr_node))
 460        | M, _ -> set,inf,sup
 461     in
 462     let set =
 463      locate_using_leq (to_be_considered,Some repr,news) node set start_sup in
 464 (
 465 let _,inf,sup = set in
 466 if not (List.for_all (fun ((_,_,_,geq) as node) -> !geq = [] && let rec check_sups = function [] -> true | (_,_,leq,_) as node::tl -> if !leq = [] then List.exists (fun n -> n===node) sup && check_sups tl else check_sups (!leq@tl) in check_sups [node]) inf) then (ps_of_set ([],None,[]) set; assert false);
 467 if not (List.for_all (fun ((_,_,leq,_) as node) -> !leq = [] && let rec check_infs = function [] -> true | (_,_,_,geq) as node::tl -> if !geq = [] then List.exists (fun n -> n===node) inf && check_infs tl else check_infs (!geq@tl) in check_infs [node]) sup) then (ps_of_set ([],None,[]) set; assert false);
 468 );
 469     let set =
 470      locate_using_geq (to_be_considered,Some repr,news) node set start_inf
 471     in
 472 (
 473 let _,inf,sup = set in
 474 if not (List.for_all (fun ((_,_,_,geq) as node) -> !geq = [] && let rec check_sups = function [] -> true | (_,_,leq,_) as node::tl -> if !leq = [] then List.exists (fun n -> n===node) sup && check_sups tl else check_sups (!leq@tl) in check_sups [node]) inf) then (ps_of_set ([],None,[]) set; assert false);
 475 if not (List.for_all (fun ((_,_,leq,_) as node) -> !leq = [] && let rec check_infs = function [] -> true | (_,_,_,geq) as node::tl -> if !geq = [] then List.exists (fun n -> n===node) inf && check_infs tl else check_infs (!geq@tl) in check_infs [node]) sup) then ((*ps_of_set ([],None,[]) set;*) assert false);
 476 );
 477      news@[candidate],set
 478    with
 479     SameEquivalenceClass ((nodes,inf,sup) as set,((r,_,leq_d,geq_d) as node_to_be_deleted),node')->
 480 (
 481 let _,inf,sup = set in
 482 if not (List.for_all (fun ((_,_,_,geq) as node) -> !geq = [] && let rec check_sups = function [] -> true | (_,_,leq,_) as node::tl -> if !leq = [] then List.exists (fun n -> n===node) sup && check_sups tl else check_sups (!leq@tl) in check_sups [node]) inf) then (ps_of_set ([],None,[]) set; assert false);
 483 if not (List.for_all (fun ((_,_,leq,_) as node) -> !leq = [] && let rec check_infs = function [] -> true | (_,_,_,geq) as node::tl -> if !geq = [] then List.exists (fun n -> n===node) inf && check_infs tl else check_infs (!geq@tl) in check_infs [node]) sup) then ((*ps_of_set ([],None,[]) set;*) assert false);
 484 );
 485      let rec clean inf sup res =
 486       function
 487          [] -> inf,sup,res
 488        | node::tl when node===node_to_be_deleted ->
 489           clean inf sup res tl
 490        | (repr',others,leq,geq) as node::tl ->
 491           leq :=
 492            (let rec aux res =
 493              function
 494                 [] -> res
 495               | (_,_,leq,_) as node::tl ->
 496                  if node_to_be_deleted <=> node then
 497                   aux (res@[node]) tl
 498                  else
 499                   (List.filter (fun n ->not (leq_reachable n (res@tl))) !leq)@tl
 500             in
 501              aux [] !leq);
 502           let sup = if !leq = [] then sup@@node else sup in
 503           geq :=
 504            (let rec aux res =
 505              function
 506                 [] -> res
 507               | (_,_,_,geq) as node::tl ->
 508                  if node_to_be_deleted <=> node then
 509                   aux (res@[node]) tl
 510                  else
 511                   (List.filter (fun n ->not (geq_reachable n (res@tl))) !geq)@tl
 512             in
 513              aux [] !geq);
 514           let inf = if !geq = [] then inf@@node else inf in
 515           if node===node' then
 516            clean inf sup ((repr',others@[candidate],leq,geq)::res) tl
 517           else
 518            clean inf sup (node::res) tl
 519      in
 520      let inf,sup,nodes = clean inf sup [] nodes in
 521      let inf = remove node_to_be_deleted inf in
 522      let sup = remove node_to_be_deleted sup in
 523 let set = nodes,inf,sup in
 524 (
 525 let _,inf,sup = set in
 526 if not (List.for_all (fun ((_,_,_,geq) as node) -> !geq = [] && let rec check_sups = function [] -> true | (_,_,leq,_) as node::tl -> if !leq = [] then List.exists (fun n -> n===node) sup && check_sups tl else check_sups (!leq@tl) in check_sups [node]) inf) then (ps_of_set ([],None,[]) set; assert false);
 527 if not (List.for_all (fun ((_,_,leq,_) as node) -> !leq = [] && let rec check_infs = function [] -> true | (_,_,_,geq) as node::tl -> if !geq = [] then List.exists (fun n -> n===node) inf && check_infs tl else check_infs (!geq@tl) in check_infs [node]) sup) then (ps_of_set ([],None,[]) set; assert false);
 528 );
 529       news,(nodes,inf,sup)
 530 ;;
 531
 532 let rec explore i (set:set) news =
 533  let rec aux news set =
 534   function
 535      [] -> news,set
 536    | repr::tl ->
 537       let news,set =
 538        List.fold_right (analyze_one tl repr) [I;C;M] (news,set)
 539       in
 540        aux news set tl
 541  in
 542   let news,set = aux [] set news in
 543    if news = [] then
 544     begin
 545      print_endline ("PUNTO FISSO RAGGIUNTO! i=" ^ string_of_int i);
 546      print_endline (string_of_set set ^ "\n----------------");
 547      ps_of_set ([],None,[]) set
 548     end
 549    else
 550     begin
 551      print_endline ("NUOVA ITERAZIONE, i=" ^ string_of_int i);
 552      print_endline (string_of_set set ^ "\n----------------");
 553      explore (i+1) set news
 554     end
 555 in
 556  let id = [] in
 557  let id_node = id,[],ref [], ref [] in
 558  let set = [id_node],[id_node],[id_node] in
 559   print_endline ("PRIMA ITERAZIONE, i=0, j=0");
 560   print_endline (string_of_set set ^ "\n----------------");
 561   (*ignore (Unix.system "rm -f log");*)
 562   assert (Unix.system "cp formal_topology.ma log.ma" = Unix.WEXITED 0);
 563   ps_of_set ([id],None,[]) set;
 564   explore 1 set [id]
 565 ;;