concretisation

Author: Ioana

concret.ml

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

concret.mli

@@ -39,12 +39,12 @@ let add_posets p current_posets =
   { poset_list = p::current_posets.poset_list;
     event_list = p.Poset.events@current_posets.event_list; }
 
-let set_posets file_list sigs =
+let set_posets file_list env =
   let posets : t = { poset_list = []; event_list = []; } in
   let posets_file =
     List.fold_left
       (fun t file ->
-        let s = Poset.read_poset_from_file file sigs in
+        let s = Poset.read_poset_from_file file env in
         add_posets s t) posets file_list in
   let () = if (!Param.debug_mode)
            then (Format.printf "\nset_posets";

domain.ml

@@ -15,6 +15,6 @@ val print_posets: t -> unit
 val print_domain : domain -> unit
 val print_domain_list : domain list -> unit
 
-val set_posets : string list -> Model.t -> t
+val set_posets : string list -> Model.t option -> t
 
 val get_poset_from_filename : string -> domain list -> domain

domain.mli

@@ -3,28 +3,37 @@ open Lib
 
 type t = {
     event_id : int; (* local id inside a story *)
-    event_label : string;
+    rule_id : int; (* id of primitive rule *)
+    event_label : string; (*label of corresponding ast rule *)
     step : Trace.step ;
   }
 
-let get_id e = e.event_id
-let get_label e = e.event_label
-let get_step e = e.step
+let id e = e.event_id
+let rule_id e = e.rule_id
+let label e = e.event_label
+let step e = e.step
 
 let test_event event_id event_label =
- { event_id; event_label; step = Trace.Dummy "none"; }
+ { event_id; rule_id = -1; event_label; step = Trace.Dummy "none"; }
 
 let print_event e =
   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 rule_id_of_json = function
+    | Trace.Rule (id,_,_) -> id
+    | Trace.Pert _ -> -1
+    | Trace.Init _ -> -2
+    | Trace.Obs _ -> -3
+    | Trace.Dummy _ | Trace.Subs _ -> -4
+
 let nodes_of_json env = function
   | `List [`Int id; step_json] ->
      let step = Trace.step_of_yojson step_json in
-     let env = Some env in
      let () = Trace.print_label_of_step ?env (Format.str_formatter) step in
-     let label = Format.flush_str_formatter () in
-     { event_id = id; event_label = label; step;}
+     let event_label = Format.flush_str_formatter () in
+     let rule_id = rule_id_of_json step in
+     { event_id = id; rule_id; event_label; step;}
   | x -> raise (Yojson.Basic.Util.Type_error ("Incorrect node of json",x))

event.ml

@@ -1,16 +1,18 @@
 open Yojson
 
 type t = {
-    event_id : int; (* local id inside a story *)
+    event_id : int;
+    rule_id : int;
     event_label : string;
     step : Trace.step ;
   }
 
-val nodes_of_json : Model.t -> Yojson.Basic.json -> t
+val nodes_of_json : Model.t option -> Yojson.Basic.json -> t
 
-val get_id : t -> int
-val get_label : t -> string
-val get_step : t -> Trace.step
+val id : t -> int
+val label : t -> string
+val step : t -> Trace.step
+val rule_id : t -> int
 
 val print_event : t -> unit
 val test_event : int -> string -> t

event.mli

@@ -174,7 +174,7 @@ let denotations (_,_,domain as m) fm =
 (**** Interpretation ****)
 
 let label x = match x with
-  | Domain.Ev e -> (Event.get_label e)
+  | Domain.Ev e -> (Event.label e)
   | Domain.Pos _ ->
      raise (ExceptDefn.Malformed_Args("label"))
 
@@ -203,15 +203,23 @@ let membership = function
     (Domain.Ev e, Domain.Pos p) -> List.mem e (p.Poset.events)
   | _ -> raise (ExceptDefn.Malformed_Args("membership"))
 
-let equal_posets = function
+let morphisms_posets f = function
     (Domain.Pos p1, Domain.Pos p2) ->
     (match (p1.Poset.kappa, p2.Poset.kappa) with
      | (true, true) ->
-        Morphism.isomorphism (Poset.remove_obs(p1)) (Poset.remove_obs(p2))
-     | (true, false) -> Morphism.isomorphism (Poset.remove_obs(p1)) p2
-     | (false, true) -> Morphism.isomorphism p1 (Poset.remove_obs(p2))
-     | (false, false) -> Morphism.isomorphism p1 p2 )
-  | _ -> raise(ExceptDefn.Malformed_Args("equal posets"))
+        let () = if (!Param.debug_mode) then
+                   (Format.printf "kappa posets - remove obs@.") in
+        f (Poset.remove_event p1 (Poset.obs p1))
+          (Poset.remove_event p2 (Poset.obs p2))
+     | (true, false) ->
+        f (Poset.remove_event p1 (Poset.obs p1)) p2
+     | (false, true) ->
+        f p1 (Poset.remove_event p2 (Poset.obs p2))
+     | (false, false) -> f p1 p2)
+  | _ -> raise(ExceptDefn.Malformed_Args("morphisms posets"))
+
+let equal_posets = morphisms_posets Morphism.isomorphism
+let sub_poset = morphisms_posets Morphism.morphism
 
 let equal_events = function
     (Domain.Ev e1, Domain.Ev e2) ->
@@ -222,19 +230,6 @@ let equal_events = function
     else false
   | _ -> raise(ExceptDefn.Malformed_Args("equal events"))
 
-let sub_poset = function
-    (Domain.Pos p1, Domain.Pos p2) ->
-    (match (p1.Poset.kappa, p2.Poset.kappa) with
-     | (true, true) ->
-        let () = if (!Param.debug_mode) then
-                   (Format.printf
-                      "sub_poset: posets are kappa type - remove obs\n";) in
-        Morphism.morphism (Poset.remove_obs(p1)) (Poset.remove_obs(p2))
-     | (true, false) -> Morphism.morphism (Poset.remove_obs(p1)) p2
-     | (false, true) -> Morphism.morphism p1 (Poset.remove_obs(p2))
-     | (false, false) -> Morphism.morphism p1 p2 )
-  | _ -> raise(ExceptDefn.Malformed_Args("sub_posets"))
-
 let intro = function
     Domain.Pos p -> Poset.intro p
   | _ -> raise (ExceptDefn.Malformed_Args("intro"))
@@ -246,7 +241,9 @@ let obs = function
 let negative_influence env = function
     (Domain.Ev e1, Domain.Pos p1, Domain.Ev e2, Domain.Pos p2) ->
     let sigs = Model.signatures env in
-    let () = Concret.context_of_application p1 p2 sigs env in
+(*    let past1 = Poset.past e1 p1 in
+    let past2 = Poset.past e2 p2 in*)
+    let () = Concret.context_of_application e1 p1 e2 p2 sigs env in
     true
    | _ ->  raise(ExceptDefn.Malformed_Args("negative_influence"))
 

formulas.ml

@@ -9,12 +9,6 @@ let options = [
     ("-env", Arg.Set_string env_file, "file name for environment");
     ("-debug", Arg.Set debug_mode, "print internal info");]
 
-let test_z3 t =
-  let posets = Domain.get_posets t in
-  let p1 = List.nth posets 0 in
-  let p2 = List.nth posets 3 in
-  Z3morphism.get_morphism p1 p2
-
 let test_subset t =
   let posets = Domain.get_posets t in
   let p1 = List.nth posets 2 in
@@ -35,6 +29,16 @@ let test_subset t =
          Formulas.R("sub_posets", [Formulas.Var "x"; Formulas.Var "y"]))) in
   (valuation,fm)
 
+let fm_neg =
+  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"])))))
+
 let empty_valuation = function
     _ -> failwith "empty valuation"
 
@@ -84,33 +88,21 @@ let () =
   let () = set_flags () in
   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 posets = Domain.set_posets (!files) (Some env) in
   let () = if (!Param.debug_mode) then Format.printf "read posets\n" in
-  let fm_neg =
-    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
+
+(*  test_z3 posets*)
+(*  let () = parse_fm () in
   List.iteri
     (fun i fm ->
       Format.printf "\n evaluate formula %i:\n" i;
       (evaluate fm m empty_valuation))
-    (!read_fm)
-  *)
-  (*
+    (!read_fm)*)
+(*
   let (valuation,fm) = test_subset posets in
   if (Formulas.holds m valuation fm) then Format.printf"true\n"
-  else Format.printf "false\n"
-   *)
+  else Format.printf "false\n"*)

main.ml

@@ -63,9 +63,9 @@ let check_combination p1 p2 =
 
 let gen_all_morphs p1 p2 =
   let l1 =
-    List.map (fun e -> (Event.get_id e, Event.get_label e)) p1.Poset.events in
+    List.map (fun e -> (Event.id e, Event.label e)) p1.Poset.events in
   let l2 =
-    List.map (fun e -> (Event.get_id e, Event.get_label e)) p2.Poset.events in
+    List.map (fun e -> (Event.id e, Event.label e)) p2.Poset.events in
   let combins = combinations (List.length l1) l2 in
   List.flatten
     (List.map
@@ -77,9 +77,9 @@ let gen_all_morphs p1 p2 =
 let check_labels m p1 p2 =
   List.fold_left
     (fun ok_so_far (id1,id2) ->
-      let e1 = List.find (fun e -> (Event.get_id e) = id1) p1.Poset.events in
-      let e2 = List.find (fun e -> (Event.get_id e) = id2) p2.Poset.events in
-      ok_so_far && ((Event.get_label e1)= (Event.get_label e2)))
+      let e1 = List.find (fun e -> (Event.id e) = id1) p1.Poset.events in
+      let e2 = List.find (fun e -> (Event.id e) = id2) p2.Poset.events in
+      ok_so_far && ((Event.label e1)= (Event.label e2)))
     true (IntMap.bindings m)
 
 let check_prec m p1 p2 =

morphism.ml

@@ -17,10 +17,10 @@ let empty_poset =
 let get_events_from_poset p = p.events
 
 let get_event_by_id i p =
-  List.find (fun e -> (Event.get_id e) = i) (get_events_from_poset p)
+  List.find (fun e -> (Event.id e) = i) (get_events_from_poset p)
 
 let get_events_by_id_list ls p =
-  List.filter (fun e -> List.mem (Event.get_id e) ls) p.events
+  List.filter (fun e -> List.mem (Event.id e) ls) p.events
 
 let print_poset p =
   Format.printf "events (id, label) : \n";
@@ -41,15 +41,15 @@ let edges_of_json json =
       let e2 = member "to" json |> to_int in
       (e1,e2)) json
 
-let read_poset_from_file file sigs =
+let read_poset_from_file file env =
   let json = Yojson.Basic.from_file file in
   let open Yojson.Basic.Util in
   let nodes = json |> member "nodes" |> to_list in
   let edges_cause = json |> member "cause" |> to_list in
   let edges_inhibit = json |> member "inhibit" |> to_list in
   { kappa = true;
     filename = Some file;
-    events = List.mapi (fun i l -> Event.nodes_of_json sigs l) nodes;
+    events = List.mapi (fun i l -> Event.nodes_of_json env l) nodes;
     prec_1 = edges_of_json edges_cause;
     prec_star = None;
     inhibit = edges_of_json edges_inhibit}
@@ -70,7 +70,7 @@ let intro p =
   let intros =
     List.filter
     (fun e ->
-      not(List.exists (fun (i1,i2) -> (Event.get_id e) = i2) p.prec_1))
+      not(List.exists (fun (i1,i2) -> (Event.id e) = i2) p.prec_1))
     p.events in
   let () = if (!Param.debug_mode)
            then (Format.printf "intro events of poset: \n";
@@ -80,16 +80,16 @@ let intro p =
   get_poset_of_events(intros)
 
 (* specialised to the case of one obs - the last one in the list *)
-let remove_obs p =
-  if (p.kappa) then
-    (let obs_id = List.length p.events in
-     let events =
-       List.filter (fun e -> not ((Event.get_id e) = obs_id)) p.events in
-     let prec_1 = List.filter (fun (e1,e2) -> not (e2 = obs_id) ) p.prec_1 in
-     let inhibit = List.filter (fun (e1,e2) -> not (e2 = obs_id) ) p.inhibit in
-     { kappa = false; filename = p.filename; events; prec_1;
-       prec_star= None;inhibit; })
-  else raise (ExceptDefn.Internal_Error("should not be possible"))
+let obs p =
+  if (p.kappa) then List.length p.events
+  else raise (ExceptDefn.Internal_Error("obs of non kappa poset"))
+
+let remove_event p eid =
+  let neither (e1,e2) = not((e1 = eid)||(e2 = eid)) in
+  let events = List.filter (fun e -> not ((Event.id e) = eid)) p.events in
+  let prec_1 = List.filter neither p.prec_1 in
+  let inhibit = List.filter neither p.inhibit in
+  {kappa = false;filename = p.filename; events; prec_1;prec_star= None;inhibit}
 
 let sort_prec ls =
   let rec verif_sort = function
@@ -102,29 +102,28 @@ let sort_prec ls =
 
 (* id of events in interval [0,length(events)] *)
 let get_enriched p =
-  let arr = Array.make ((List.length p.events)+1) [] in
-  let sorted = sort_prec p.prec_1 in
-  let () =
-    List.iter
-      (fun (e1,e2) ->
-        let l2 =
-          List.fold_left
-            (fun acc e -> if (List.mem e acc) then acc else e::acc)
-            arr.(e1) arr.(e2) in
-        arr.(e1) <- e2::l2) sorted in
-  arr
+  match p.prec_star with
+  | Some enr -> enr
+  | None ->
+     let arr = Array.make ((List.length p.events)+1) [] in
+     let sorted = sort_prec p.prec_1 in
+     let () =
+       List.iter
+         (fun (e1,e2) ->
+           let l2 =
+             List.fold_left
+               (fun acc e -> if (List.mem e acc) then acc else e::acc)
+               arr.(e1) arr.(e2) in
+           arr.(e1) <- e2::l2) sorted in
+     let () = p.prec_star <- Some arr in
+     arr
 
 let check_prec_1 e1 e2 p =
   (List.mem e1 p.events)&& (List.mem e2 p.events)&&
     (List.mem (e1.Event.event_id, e2.Event.event_id) p.prec_1)
 
 let check_prec_star e1 e2 p =
-  let enrich = match p.prec_star with
-    | None ->
-       let enr = get_enriched p in
-       let () = p.prec_star <- Some enr in
-       enr
-    | Some enr -> enr in
+  let enrich = get_enriched p in
   let () =
     if (!Param.debug_mode) then
       (Format.printf "check_prec_star \n";
@@ -135,3 +134,19 @@ let check_prec_star e1 e2 p =
        Format.printf "%d =< %d" (e1.Event.event_id) (e2.Event.event_id) ) in
   (List.mem e1 p.events)&& (List.mem e2 p.events)&&
     (List.mem (e2.Event.event_id) enrich.(e1.Event.event_id))
+
+(*check it !!*)
+let past e p =
+  let enrich = get_enriched p in
+  let eid = Event.id e in
+  let events = get_events_by_id_list enrich.(eid) p in
+  let list_mem (e1,e2) =
+    (List.mem e1 enrich.(eid))&&(List.mem e1 enrich.(eid)) in
+  let prec_1 = List.filter list_mem p.prec_1 in
+  let inhibit = List.filter list_mem p.inhibit in
+  {kappa = false;filename = p.filename; events; prec_1;prec_star= None;inhibit}
+
+let same_poset p1 p2 =
+  match (p1.filename,p2.filename) with
+  | (None, _) | (_, None) -> false
+  | (Some f1, Some f2) -> ((String.compare f1 f2)=0)