debug example

Author: Ioana

concret.ml

@@ -39,7 +39,6 @@ let print_morphisms compose2 =
   Format.printf "@.compose2 = ";
   List.iter (fun (a,b)-> Format.printf "(%d,%d) " a b) compose2
 
-
 (*********** functions on morphisms as lists *)
 let list_to_renaming ls =
   match
@@ -119,58 +118,74 @@ let compose_matchings mg1 m1 n1 m2' n2 m2 mg2 =
   let partial1 =
     List.filter (fun (a1,b1) -> List.mem b1 (domain list_m2')) compose1 in
   let () = if (!Param.debug_mode) then print_morphs2 compose1 partial1 in
+(*  let comp1 = compose partial1 list_m2' in
+  let () = print_morphisms comp1 in
+  let comp2 = compose comp1 n2 in
+  let () = print_morphisms comp2 in
+  let comp3 = compose comp2 m2 in
+  let () = print_morphisms comp3 in
+  let () = print_morphisms mg2 in *)
   let compose2 =
     compose (compose (compose (compose partial1 list_m2') n2) m2) mg2 in
   let () = if (!Param.debug_mode) then print_morphisms compose2 in
   list_to_renaming compose2
 
-let print_conflict = function
-  | (i1,s1,l1,int1)::(i2,s2,l2,int2)::_ ->
-     if (int1!= int2) then
-       Format.printf
-         "on internal state of %d:%d=%d and %d:%d=%d" i1 s1 int1 i2 s2 int2
-     else (Format.printf "on link of %d:%d " i1 s1 ;
-           (match l1 with
-            | Pattern.Free -> Format.printf " free "
-            | Pattern.Link (n1,ns1) -> Format.printf "(%d, %d)" n1 ns1
-            | _ -> ());
-           Format.printf "and %d:%d " i2 s2;
-           (match l2 with
-            | Pattern.Free -> Format.printf " free "
-            | Pattern.Link (n1,ns1) -> Format.printf "(%d, %d)" n1 ns1
-            | _ -> ()))
-  | _ ->
-     raise (ExceptDefn.Internal_Error("conflict must return two nodes"))
+let print_conflict sigs (cc1,i1,cc2,i2,s,internal) =
+  let () =
+    Format.printf "no context for inhibition due to conflict on cc1 = ";
+    Lib.print_cc sigs cc1;
+    Format.printf " and cc2 = "; Lib.print_cc sigs cc2;
+    Format.printf " due to conflict on " in
+  let () =
+    if internal then Format.printf "internal states of "
+    else Format.printf "links of " in
+  Format.printf "%d of cc1 and %d of cc2 on site %d @." i1 i2 s
 
 let build_context
       sigs domain (n1,cc1,id1) (n2,cc2,id2) graph1 graph2 m1 m2 m2' inf=
   let find_cc n m graph =
-    (*    let (n',_) = List.find (fun (_,i) -> (i=id)) n in*)
+    (*graph:(morphism,pattern.cc,pattern.id) list*)
     let (rule_id,abstract_id) = List.hd n in
     let (_,concrete_id) = List.find (fun (i,_) -> (i=abstract_id)) m in
-    let (mg,g,_) =
-      List.find
+    let cc_of_graph,rest =
+      List.partition
         (fun (m,_,_) -> List.exists (fun (c,_) -> c=concrete_id) m) graph in
-    (n,mg,g) in
-  let (n1',mg1,g1) = find_cc n1 m1 graph1 in
-  let (n2',mg2,g2) = find_cc n2 m2 graph2 in
+    match cc_of_graph with
+    | (mg,g,_)::[] -> (n,mg,g,rest)
+    | _ ->
+       raise (ExceptDefn.Internal_Error("only one cc should match in graph")) in
+  let (n1',mg1,g1,rest1) = find_cc n1 m1 graph1 in
+  let (n2',mg2,g2,rest2) = find_cc n2 m2 graph2 in
+  (*let () =
+    Format.printf "build_context @.@.";
+    Lib.print_cc sigs g1;Lib.print_cc sigs g2;
+    Lib.print_cc sigs cc1;Lib.print_cc sigs cc2 in*)
   let m = compose_matchings mg1 m1 n1' m2' n2' m2 mg2 in
   (* let () = if (!Param.debug_mode) then print_build_context sigs m in *)
   let context = Pattern.merge_on_inf domain m g1 g2 in
   match context with
-  | (None,conflict) ->
-     let () =
-       if (!Param.verb) then
-         (Format.printf "no context for inhibition due to conflict ";
-          print_conflict conflict) in
-        false
+  | (None,Some conflict) ->
+     let () = if (!Param.verb) then print_conflict sigs conflict in
+     false
+  | (None,None) ->
+     raise (ExceptDefn.Internal_Error("no pushout must return conflict"))
   | (Some c,_) ->
      let () =
        if (!Param.verb) then
          (Format.printf "witness context for inhibition = ";
           Lib.print_cc sigs c;
+          List.iter
+            (fun (_,cc,_) ->
+              Pattern.print_cc
+                ~new_syntax:true ~sigs ~with_id:true (Format.std_formatter) cc)
+            rest1;
+          List.iter
+            (fun (_,cc,_) ->
+              Pattern.print_cc
+                ~new_syntax:true ~sigs ~with_id:true (Format.std_formatter) cc)
+            rest2;
           Format.printf "@. due to inf = ";
-          Lib.print_cc sigs inf) in
+          Lib.print_cc sigs inf; Format.printf "@.") in
      true
 
 let all_possible lhs1 lhs2 sigs domain graph1 graph2 m1 m2 actions =
@@ -215,7 +230,6 @@ let all_possible lhs1 lhs2 sigs domain graph1 graph2 m1 m2 actions =
 let context_of_application e1 s1 e2 s2 sigs env =
   let env' = Model.domain env in
   let domain = Pattern.PreEnv.of_env env' in
-
   let (graph1,lhs1,m1,actions) = Poset.concrete env env' sigs e1 s1 in
   let (graph2,lhs2,m2,_) = Poset.concrete env env' sigs e2 s2 in
 

formulas.ml

@@ -304,23 +304,18 @@ let denotations (_,_,domain as m) fm =
          vals
          (List.filter (fun d -> domain_match_sort d "Poset") domain)
     | [] ->
-       if (holds m valuation fm) then
-         let () =
-           if (!Param.verb) then
-             (Format.printf "true on valuation :@.";
-              List.iter
-                (fun v -> Format.printf "%s = " v;
-                          Domain.print_domain (valuation(v))) (free_var fm);
-              Format.printf "@.@.") in
+       let () =
+         if (!Param.verb) then
+           (Format.printf "on valuation :@.";
+            List.iter
+              (fun v -> Format.printf "%s = " v;
+                        Domain.print_domain (valuation(v))) (free_var fm);
+            Format.printf "@.") in
+       if holds m valuation fm then
+         let () = if (!Param.verb) then Format.printf "holds true @.@." in
          (valuation::vals)
        else
-         let () =
-           if (!Param.verb) then
-             (Format.printf "@. false on valuation :@.";
-              List.iter
-                (fun v -> Format.printf "%s = " v;
-                          Domain.print_domain (valuation(v))) (free_var fm);
-              Format.printf "@.@.") in
+         let () = if (!Param.verb) then Format.printf "holds false @.@." in
          vals in
   let default_valuation x = raise (ExceptDefn.Uninterpreted_Variable(x)) in
   denote_var (free_var fm) default_valuation []

poset.ml

@@ -91,8 +91,8 @@ let prepare_for_morphism p =
     {kappa = false;filename = p.filename;events;prec_1;prec_star=None;inhibit;}
 
 let sort p =
-  let rev_inhibit = List.map (fun (a,b) -> (b,a)) p.inhibit in
-  let to_order = p.prec_1 @ rev_inhibit in
+  (*let rev_inhibit = List.map (fun (a,b) -> (b,a)) p.inhibit in*)
+  let to_order = p.prec_1 @ p.inhibit in
   let rec sort_pairs = function
     | [] -> []
     | ls ->
@@ -195,7 +195,7 @@ let make sigs env replay_state =
   let (env',list) = Replay.cc_of_state replay_state env in
   (env',list)
 
-let concretise s linear sigs =
+let concretise env s linear sigs =
   let () = if (!Param.debug_mode) then
              (Format.printf "concretise linear poset :";
               List.iter (fun i -> Format.printf "%d " i) linear) in
@@ -212,18 +212,19 @@ let concretise s linear sigs =
         let (env',graph) = make sigs env rhs_state in
         let trace' = TraceConcret.add_transition sigs trace graph eid in
         (trace',rhs_state,env'))
-      (TraceConcret.empty,init_state,(Pattern.PreEnv.empty sigs))
+      (TraceConcret.empty,init_state,(Pattern.PreEnv.of_env env))
       linear in
   (List.rev trace)
 
-let concrete model env sigs e p = match (Event.concrete e) with
+let concrete model env sigs e p =
+  match (Event.concrete e) with
     None ->
     let past_e = past e p in
-    let linear = linearisation past_e in
-    let t = concretise past_e linear sigs in
     let () =
       if (!Param.debug_mode) then
         (Format.printf "past of e@.";print_poset past_e) in
+    let linear = linearisation past_e in
+    let t = concretise env past_e linear sigs in
     let lhs_graph = TraceConcret.get_last_lhs_graph t in
     let graph = match lhs_graph with
       | None ->

posets_test/test3/c0.json

@@ -1 +1 @@
-{"nodes":[[13,["Obs","Apy",[[["Is_Free",{"agent":{"id":1833,"type":0},"site":2}],["Is_Free",{"agent":{"id":1833,"type":0},"site":0}],["Has_Internal",{"agent":{"id":1833,"type":0},"site":0},0],["Is_Here",{"id":1833,"type":0}]]],{"id":336,"time":9.685577604775046,"event":4007}]],[12,["Rule",3,{"tests":[[["Is_Here",{"id":1833,"type":0}],["Has_Internal",{"agent":{"id":1833,"type":0},"site":0},0],["Is_Free",{"agent":{"id":1833,"type":0},"site":0}],["Is_Here",{"id":2036,"type":2}],["Is_Bound_to",{"agent":{"id":2036,"type":2},"site":0},{"agent":{"id":1833,"type":0},"site":2}]]],"actions":[["Free",{"agent":{"id":2036,"type":2},"site":0}],["Free",{"agent":{"id":1833,"type":0},"site":2}]]},{"id":335,"time":9.685577604775046,"event":4007}]],[11,["Rule",5,{"tests":[[["Is_Here",{"id":1833,"type":0}],["Has_Internal",{"agent":{"id":1833,"type":0},"site":0},1],["Is_Free",{"agent":{"id":1833,"type":0},"site":0}],["Is_Here",{"id":2036,"type":2}],["Is_Bound_to",{"agent":{"id":2036,"type":2},"site":0},{"agent":{"id":1833,"type":0},"site":2}],["Is_Here",{"id":1963,"type":1}],["Is_Bound_to",{"agent":{"id":1963,"type":1},"site":0},{"agent":{"id":1833,"type":0},"site":1}]]],"actions":[["Mod_internal",{"agent":{"id":1833,"type":0},"site":0},0]]},{"id":302,"time":9.209427748659548,"event":3929}]],[10,["Rule",0,{"tests":[[["Is_Here",{"id":1963,"type":1}],["Is_Free",{"agent":{"id":1963,"type":1},"site":0}]],[["Is_Here",{"id":1833,"type":0}],["Has_Internal",{"agent":{"id":1833,"type":0},"site":0},1],["Is_Free",{"agent":{"id":1833,"type":0},"site":0}],["Is_Free",{"agent":{"id":1833,"type":0},"site":1}]]],"actions":[["Bind",{"agent":{"id":1963,"type":1},"site":0},{"agent":{"id":1833,"type":0},"site":1}]]},{"id":193,"time":7.123196678201288,"event":3623}]],[9,["Rule",7,{"tests":[[["Is_Here",{"id":1833,"type":0}],["Is_Here",{"id":910,"type":1}],["Is_Bound_to",{"agent":{"id":910,"type":1},"site":0},{"agent":{"id":1833,"type":0},"site":1}],["Is_Here",{"id":1844,"type":2}],["Is_Bound_to",{"agent":{"id":1844,"type":2},"site":1},{"agent":{"id":910,"type":1},"site":1}]]],"actions":[["Free",{"agent":{"id":910,"type":1},"site":0}],["Free",{"agent":{"id":1833,"type":0},"site":1}]]},{"id":92,"time":4.733225988126882,"event":3299}]],[7,["Rule",1,{"tests":[[["Is_Here",{"id":2036,"type":2}],["Is_Free",{"agent":{"id":2036,"type":2},"site":0}]],[["Is_Here",{"id":1833,"type":0}],["Is_Free",{"agent":{"id":1833,"type":0},"site":2}],["Is_Here",{"id":910,"type":1}],["Is_Bound_to",{"agent":{"id":910,"type":1},"site":0},{"agent":{"id":1833,"type":0},"site":1}]]],"actions":[["Bind",{"agent":{"id":2036,"type":2},"site":0},{"agent":{"id":1833,"type":0},"site":2}]]},{"id":0,"time":0.5157215022070692,"event":2600}]],[8,["Rule",6,{"tests":[[["Is_Here",{"id":1844,"type":2}],["Is_Free",{"agent":{"id":1844,"type":2},"site":1}]],[["Is_Here",{"id":910,"type":1}],["Is_Free",{"agent":{"id":910,"type":1},"site":1}]]],"actions":[["Bind",{"agent":{"id":1844,"type":2},"site":1},{"agent":{"id":910,"type":1},"site":1}]]},{"id":35,"time":2.6277817503951044,"event":3070}]],[6,["Rule",0,{"tests":[[["Is_Here",{"id":910,"type":1}],["Is_Free",{"agent":{"id":910,"type":1},"site":0}]],[["Is_Here",{"id":1833,"type":0}],["Has_Internal",{"agent":{"id":1833,"type":0},"site":0},1],["Is_Free",{"agent":{"id":1833,"type":0},"site":0}],["Is_Free",{"agent":{"id":1833,"type":0},"site":1}]]],"actions":[["Bind",{"agent":{"id":910,"type":1},"site":0},{"agent":{"id":1833,"type":0},"site":1}]]},{"id":-1,"time":0.023673981155164017,"event":601}]],[5,["Init",[["Create",{"id":2036,"type":2},[[0],[1]]],["Free",{"agent":{"id":2036,"type":2},"site":1}],["Free",{"agent":{"id":2036,"type":2},"site":0}]]]],[4,["Init",[["Create",{"id":1963,"type":1},[[0],[1]]],["Free",{"agent":{"id":1963,"type":1},"site":1}],["Free",{"agent":{"id":1963,"type":1},"site":0}]]]],[3,["Init",[["Create",{"id":1844,"type":2},[[0],[1]]],["Free",{"agent":{"id":1844,"type":2},"site":1}],["Free",{"agent":{"id":1844,"type":2},"site":0}]]]],[2,["Init",[["Create",{"id":1833,"type":0},[[0,1],[1],[2]]],["Free",{"agent":{"id":1833,"type":0},"site":2}],["Free",{"agent":{"id":1833,"type":0},"site":1}],["Free",{"agent":{"id":1833,"type":0},"site":0}],["Mod_internal",{"agent":{"id":1833,"type":0},"site":0},1]]]],[1,["Init",[["Create",{"id":910,"type":1},[[0],[1]]],["Free",{"agent":{"id":910,"type":1},"site":1}],["Free",{"agent":{"id":910,"type":1},"site":0}]]]]],"cause":[{"from":12,"to":13},{"from":11,"to":12},{"from":10,"to":11},{"from":7,"to":11},{"from":9,"to":10},{"from":4,"to":10},{"from":8,"to":9},{"from":6,"to":9},{"from":3,"to":8},{"from":1,"to":8},{"from":6,"to":7},{"from":5,"to":7},{"from":2,"to":6},{"from":1,"to":6}],"inhibit":[]}
+{"nodes":[[13,["Obs","Apy",[[["Is_Free",{"agent":{"id":1833,"type":0},"site":2}],["Is_Free",{"agent":{"id":1833,"type":0},"site":0}],["Has_Internal",{"agent":{"id":1833,"type":0},"site":0},0],["Is_Here",{"id":1833,"type":0}]]],{"id":336,"time":9.685577604775046,"event":4007}]],[12,["Rule",3,{"tests":[[["Is_Here",{"id":1833,"type":0}],["Has_Internal",{"agent":{"id":1833,"type":0},"site":0},0],["Is_Free",{"agent":{"id":1833,"type":0},"site":0}],["Is_Here",{"id":2036,"type":2}],["Is_Bound_to",{"agent":{"id":2036,"type":2},"site":0},{"agent":{"id":1833,"type":0},"site":2}]]],"actions":[["Free",{"agent":{"id":2036,"type":2},"site":0}],["Free",{"agent":{"id":1833,"type":0},"site":2}]]},{"id":335,"time":9.685577604775046,"event":4007}]],[11,["Rule",5,{"tests":[[["Is_Here",{"id":1833,"type":0}],["Has_Internal",{"agent":{"id":1833,"type":0},"site":0},1],["Is_Free",{"agent":{"id":1833,"type":0},"site":0}],["Is_Here",{"id":2036,"type":2}],["Is_Bound_to",{"agent":{"id":2036,"type":2},"site":0},{"agent":{"id":1833,"type":0},"site":2}],["Is_Here",{"id":1963,"type":1}],["Is_Bound_to",{"agent":{"id":1963,"type":1},"site":0},{"agent":{"id":1833,"type":0},"site":1}]]],"actions":[["Mod_internal",{"agent":{"id":1833,"type":0},"site":0},0]]},{"id":302,"time":9.209427748659548,"event":3929}]],[10,["Rule",0,{"tests":[[["Is_Here",{"id":1963,"type":1}],["Is_Free",{"agent":{"id":1963,"type":1},"site":0}]],[["Is_Here",{"id":1833,"type":0}],["Has_Internal",{"agent":{"id":1833,"type":0},"site":0},1],["Is_Free",{"agent":{"id":1833,"type":0},"site":0}],["Is_Free",{"agent":{"id":1833,"type":0},"site":1}]]],"actions":[["Bind",{"agent":{"id":1963,"type":1},"site":0},{"agent":{"id":1833,"type":0},"site":1}]]},{"id":193,"time":7.123196678201288,"event":3623}]],[9,["Rule",7,{"tests":[[["Is_Here",{"id":1833,"type":0}],["Is_Here",{"id":910,"type":1}],["Is_Bound_to",{"agent":{"id":910,"type":1},"site":0},{"agent":{"id":1833,"type":0},"site":1}],["Is_Here",{"id":1844,"type":2}],["Is_Bound_to",{"agent":{"id":1844,"type":2},"site":1},{"agent":{"id":910,"type":1},"site":1}]]],"actions":[["Free",{"agent":{"id":910,"type":1},"site":0}],["Free",{"agent":{"id":1833,"type":0},"site":1}]]},{"id":92,"time":4.733225988126882,"event":3299}]],[7,["Rule",1,{"tests":[[["Is_Here",{"id":2036,"type":2}],["Is_Free",{"agent":{"id":2036,"type":2},"site":0}]],[["Is_Here",{"id":1833,"type":0}],["Is_Free",{"agent":{"id":1833,"type":0},"site":2}],["Is_Here",{"id":910,"type":1}],["Is_Bound_to",{"agent":{"id":910,"type":1},"site":0},{"agent":{"id":1833,"type":0},"site":1}]]],"actions":[["Bind",{"agent":{"id":2036,"type":2},"site":0},{"agent":{"id":1833,"type":0},"site":2}]]},{"id":0,"time":0.5157215022070692,"event":2600}]],[8,["Rule",6,{"tests":[[["Is_Here",{"id":1844,"type":2}],["Is_Free",{"agent":{"id":1844,"type":2},"site":1}]],[["Is_Here",{"id":910,"type":1}],["Is_Free",{"agent":{"id":910,"type":1},"site":1}]]],"actions":[["Bind",{"agent":{"id":1844,"type":2},"site":1},{"agent":{"id":910,"type":1},"site":1}]]},{"id":35,"time":2.6277817503951044,"event":3070}]],[6,["Rule",0,{"tests":[[["Is_Here",{"id":910,"type":1}],["Is_Free",{"agent":{"id":910,"type":1},"site":0}]],[["Is_Here",{"id":1833,"type":0}],["Has_Internal",{"agent":{"id":1833,"type":0},"site":0},1],["Is_Free",{"agent":{"id":1833,"type":0},"site":0}],["Is_Free",{"agent":{"id":1833,"type":0},"site":1}]]],"actions":[["Bind",{"agent":{"id":910,"type":1},"site":0},{"agent":{"id":1833,"type":0},"site":1}]]},{"id":-1,"time":0.023673981155164017,"event":601}]],[5,["Init",[["Create",{"id":2036,"type":2},[[0],[1]]],["Free",{"agent":{"id":2036,"type":2},"site":1}],["Free",{"agent":{"id":2036,"type":2},"site":0}]]]],[4,["Init",[["Create",{"id":1963,"type":1},[[0],[1]]],["Free",{"agent":{"id":1963,"type":1},"site":1}],["Free",{"agent":{"id":1963,"type":1},"site":0}]]]],[3,["Init",[["Create",{"id":1844,"type":2},[[0],[1]]],["Free",{"agent":{"id":1844,"type":2},"site":1}],["Free",{"agent":{"id":1844,"type":2},"site":0}]]]],[2,["Init",[["Create",{"id":1833,"type":0},[[0,1],[1],[2]]],["Free",{"agent":{"id":1833,"type":0},"site":2}],["Free",{"agent":{"id":1833,"type":0},"site":1}],["Free",{"agent":{"id":1833,"type":0},"site":0}],["Mod_internal",{"agent":{"id":1833,"type":0},"site":0},1]]]],[1,["Init",[["Create",{"id":910,"type":1},[[0],[1]]],["Free",{"agent":{"id":910,"type":1},"site":1}],["Free",{"agent":{"id":910,"type":1},"site":0}]]]]],"cause":[{"from":12,"to":13},{"from":11,"to":12},{"from":10,"to":11},{"from":7,"to":11},{"from":9,"to":10},{"from":4,"to":10},{"from":8,"to":9},{"from":6,"to":9},{"from":3,"to":8},{"from":1,"to":8},{"from":6,"to":7},{"from":5,"to":7},{"from":2,"to":6},{"from":1,"to":6}],"inhibit":[{"from":7,"to":9}]}

script_test3

@@ -1 +1 @@
-./main.native posets_test/test3/c0.json posets_test/test3/c1.json posets_test/test3/c2.json posets_test/test3/c3.json posets_test/test3/c4.json posets_test/test3/c5.json -env posets_test/test3/env.json -f posets_test/test3/test1
+./main.native posets_test/test3/c0.json posets_test/test3/c1.json posets_test/test3/c2.json posets_test/test3/c3.json posets_test/test3/c4.json posets_test/test3/c5.json -env posets_test/test3/env.json -f posets_test/test3/test2