up to matchings

Author: Ioana

concret.ml

@@ -11,15 +11,71 @@ let concretise s sigs =
       (fun trace eid ->
         let event = Poset.get_event_by_id eid s.LinearPoset.pos in
         let step = Event.get_step event in
+
+        let () = if (!Param.debug_mode) then
+                   (Format.printf "concret of event\n";
+                    Event.print_event event) in
+
         let lhs_state =
           try Transition.get_rhs_state
                 (TraceConcret.get_first_transition trace)
-          with Failure s -> init_state in
-        let (rhs_state,_) = Replay.do_step sigs lhs_state step in
-        let trans = Transition.make lhs_state rhs_state in
+          with Failure s -> init_state ~with_connected_components:false in
+
+        let () = if (!Param.debug_mode) then
+                   (Format.printf "lhs_state\n";
+                    Edges.debug_print (Format.std_formatter)
+                                      (lhs_state.Replay.graph)) in
+        let lhs_copy = Transition.copy_state lhs_state in
+        let (rhs_state,_) = Replay.do_step sigs lhs_copy step in
+
+        let () = if (!Param.debug_mode) then
+                   (Format.printf "rhs_state\n";
+                    Edges.debug_print (Format.std_formatter)
+                                      (rhs_state.Replay.graph)) in
+
+        let trans = Transition.make lhs_state rhs_state eid in
 
         TraceConcret.add_transition trace trans)
       TraceConcret.empty s.LinearPoset.seq in
   trace
 
-let concret s sigs = concretise (linears s) sigs
+let concret s sigs =
+  let trace = concretise (linears s) sigs in
+  List.rev trace
+
+let context_of_application s1 s2 sigs env =
+  let contact_map = Model.contact_map env in
+
+  let t1 = concret s1 sigs in
+  let pt1 = TraceConcret.pattern_trace sigs contact_map t1 in
+  let graph1 = TraceConcret.get_last_context pt1 in
+
+  let t2 = concret s2 sigs in
+  let pt2 = TraceConcret.pattern_trace sigs contact_map t2 in
+  let graph2 = TraceConcret.get_last_context pt2 in
+
+  let () = if (!Param.debug_mode) then
+             (TraceConcret.print pt1 sigs;TraceConcret.print pt2 sigs) in
+  let () = Format.printf "@.trace1 = ";TraceConcret.print pt1 sigs;
+           Format.printf "@.trace2 = ";TraceConcret.print pt2 sigs;
+           Format.printf "@.graph1 = "; Transition.print_side graph1 sigs ;
+           Format.printf "@.graph2 = "; Transition.print_side graph2 sigs in
+  let g1 = List.hd graph1 in
+  let g2 = List.hd graph2 in
+  let cc_list = Pattern.infs g1 g2 in
+  let () = Format.printf "@.the infs =";
+           List.iter (fun cc -> Pattern.print_cc ~new_syntax:true ~sigs:sigs
+                                                 ~with_id:true
+                                                 (Format.std_formatter) cc;
+                                Format.printf ";;   ")
+                     cc_list in
+  let () =
+    List.iter
+      (fun cc ->
+        List.iter (fun m ->
+                    Format.printf "@.matching %a@." Renaming.print_full m;
+                    (*let pushout = Pattern.pushout m g1 g2 in
+                    Format.printf "pushout =";
+                    Transition.print_side [pushout] sigs*))
+                  (Pattern.matchings cc g1)) cc_list in
+  ()

concret.mli

@@ -1,2 +1,4 @@
 
 val concret : Poset.t -> Signature.s -> TraceConcret.s
+val context_of_application :
+  Poset.t -> Poset.t -> Signature.s -> Model.t -> unit

event.ml

@@ -15,7 +15,10 @@ let test_event event_id event_label =
  { event_id; event_label; step = Trace.Dummy "none"; }
 
 let print_event e =
-  Format.printf " (%i, %s)  " (e.event_id) (e.event_label)
+  Format.printf "\n(%i, %s) " (e.event_id) (e.event_label)
+
+let print_complete_event e =
+  print_event e;Trace.print_step (Format.std_formatter) e.step;Format.printf"\n"
 
 let nodes_of_json env = function
   | `List [`Int id; step_json] ->

formulas.ml

@@ -244,12 +244,9 @@ let obs = function
   | _ -> raise (ExceptDefn.Malformed_Args("obs"))
 
 let negative_influence env = function
-    (Domain.Pos p1, Domain.Pos p2) ->
+    (Domain.Ev e1, Domain.Pos p1, Domain.Ev e2, Domain.Pos p2) ->
     let sigs = Model.signatures env in
-    let t = Concret.concret p1 sigs in
-    let pre_env = Pattern.minimal_env sigs contact_map in
-    let pattern_trace = TraceConcret.pattern_trace contact_map sigs pre_env t in
-(*    let () = if (!Param.debug_mode) then TraceConcret.print t sigs in*)
+    let () = Concret.context_of_application p1 p2 sigs env in
     true
    | _ ->  raise(ExceptDefn.Malformed_Args("negative_influence"))
 
@@ -286,7 +283,7 @@ let interpretation env t =
       | ("equal_posets", [p1;p2]) -> equal_posets (p1,p2)
       | ("equal_events", [e1;e2]) -> equal_events (e1,e2)
       | ("sub_posets", [p1;p2]) -> sub_poset (p1,p2)
-      | ("negative_influence", [p1;p2]) ->
-         negative_influence env (p1,p2)
+      | ("negative_influence", [e1;p1;e2;p2]) ->
+         negative_influence env (e1,p1,e2,p2)
       | _ -> raise (ExceptDefn.Uninterpreted_Predicate(p)) in
   (func,pred,domain)

main.ml

@@ -85,17 +85,21 @@ let () =
   let json = Yojson.Basic.from_file (!env_file) in
   let env = Model.of_yojson json in
   let posets = Domain.set_posets (!files) env in
+  let () = if (!Param.debug_mode) then Format.printf "read posets\n" in
   let fm_neg =
-    (Formulas.Atom(
-         Formulas.R("negative_influence",
-                    [Formulas.Var "s1";
-                     Formulas.Var "s2"]))) in
+    Formulas.Exists
+      ("e2","Event",
+       Formulas.Exists
+         ("e1","Event",
+          (Formulas.Atom(
+               Formulas.R("negative_influence",
+                          [Formulas.Var "e1"; Formulas.Var "s1";
+                           Formulas.Var "e2"; Formulas.Var "s2"]))))) in
 
   let m = Formulas.interpretation env posets in
   let () = Format.printf "\n evaluate formula\n" in
   (evaluate fm_neg m empty_valuation)
 
-
   (*  test_z3 posets*)
   (*
   let m = Formulas.interpretation posets in

traceConcret.ml

@@ -5,14 +5,22 @@ type t = Transition.t list
 
 let empty = []
 
-(*
-let print t sigs = List.iter (fun trans -> Transition.print trans sigs) t
- *)
-
 let get_first_transition t = List.hd t
 let get_last_transition t = List.nth t ((List.length t)-1)
 let add_transition trace trans = trans::trace
 
-let pattern_trace contact_map sigs pre_env trace =
+let pattern_trace sigs contact_map trace =
+  let () = if (!Param.debug_mode) then Format.printf "pattern of trace\n" in
   List.map (fun trans ->
-             Transition.pattern_transition contact_map sigs pre_env trans) trace
+             Transition.pattern_transition sigs contact_map trans) trace
+
+let print t sigs =
+  List.iter
+    (fun trans ->
+      Transition.print_side trans.Transition.lhs sigs; Format.printf " => ") t;
+  let trans = get_last_transition t in
+  Transition.print_side trans.Transition.rhs sigs
+
+let get_last_context t =
+  let trans = get_last_transition t in
+  trans.Transition.rhs

traceConcret.mli

@@ -3,11 +3,10 @@ type t = Transition.t list
 
 
 val empty: s
-(*val print: t -> Signature.s -> unit*)
+val print: t -> Signature.s -> unit
 
 val get_last_transition: s -> Transition.s
 val get_first_transition: s -> Transition.s
 val add_transition: s -> Transition.s -> s
-val pattern_trace:
-  (int list * (int * int) list) array array -> Signature.s ->
-  Pattern.PreEnv.t -> s -> t
+val pattern_trace: Signature.s -> Contact_map.t -> s -> t
+val get_last_context: t -> Pattern.cc list

transition.ml

@@ -3,35 +3,49 @@ open Lib
 type t = {
     lhs: Pattern.cc list;
     rhs: Pattern.cc list;
+    eid: int;
   }
 
 type s = {
     lhs_state: Replay.state;
     rhs_state: Replay.state;
+    eid_state: int;
   }
 
-let empty sigs = {lhs=[Pattern.empty_cc sigs];rhs=[Pattern.empty_cc sigs];}
+let empty sigs =
+  {lhs=[Pattern.empty_cc sigs];rhs=[Pattern.empty_cc sigs];eid=(-1)}
+
+let copy_state s = {
+    Replay.graph = (Edges.copy s.Replay.graph); time=s.Replay.time;
+    event = s.Replay.event;connected_components=s.Replay.connected_components;}
+
+let copy s =
+  {lhs_state = (copy_state s.lhs_state);
+   rhs_state = (copy_state s.rhs_state);
+   eid_state = s.eid_state}
+
+let print_side s sigs =
+  List.iter (fun cc -> Pattern.print_cc ~new_syntax:true ~sigs:sigs
+                                        ~with_id:true
+                                        (Format.std_formatter) cc ) s;
+  Format.printf "\n"
 
 let print t sigs =
-  Format.printf "\ntransition\n";
-  List.iter (fun cc ->
-              Pattern.print_cc ~new_syntax:true ~sigs:sigs
-                               (Format.std_formatter) cc ) t.lhs;
-  Format.printf " => ";
-  List.iter (fun cc ->
-              Pattern.print_cc ~new_syntax:true ~sigs:sigs
-                               (Format.std_formatter) cc) t.rhs
-
-let pattern_transition contact_map sigs pre_env s =
+  Format.printf "\ntransition\n"; print_side t.lhs sigs;
+  Format.printf " => "; print_side t.rhs sigs
+
+let pattern_transition sigs contact_map s =
+  let pre_env = Pattern.PreEnv.empty sigs in
   let lhs_state = s.lhs_state in
   let (_,lhs) =
     Snip.patterns_of_mixture contact_map sigs pre_env
                              (lhs_state.Replay.graph) in
+  let pre_env = Pattern.PreEnv.empty sigs in
   let rhs_state = s.rhs_state in
   let (_,rhs) =
     Snip.patterns_of_mixture contact_map sigs pre_env
                              (rhs_state.Replay.graph) in
-  {lhs;rhs}
+  {lhs;rhs;eid=(s.eid_state)}
 
 let get_rhs_state s = s.rhs_state
-let make lhs_state rhs_state = {lhs_state;rhs_state}
+let make lhs_state rhs_state eid_state = {lhs_state;rhs_state;eid_state}

transition.mli

@@ -1,19 +1,22 @@
 type t = {
     lhs: Pattern.cc list;
     rhs: Pattern.cc list;
+    eid: int;
   }
 
 type s = {
     lhs_state: Replay.state;
     rhs_state: Replay.state;
+    eid_state: int;
   }
 
 val empty : Signature.s -> t
 val print : t -> Signature.s -> unit
+val print_side : Pattern.cc list -> Signature.s -> unit
 
 val get_rhs_state : s -> Replay.state
-val make : Replay.state -> Replay.state -> s
+val make : Replay.state -> Replay.state -> int -> s
 
-val pattern_transition:
-  (int list * (int * int) list) array array -> Signature.s ->
-  Pattern.PreEnv.t -> s -> t
+val pattern_transition: Signature.s -> Contact_map.t -> s -> t
+val copy_state: Replay.state ->  Replay.state
+val copy: s ->  s