using replay...

Author: Ioana

concret.ml

@@ -1,24 +1,25 @@
 let linears s =
   LinearPoset.linearisations(s)
 
-let concretise (s:LinearPoset.t) =
+let concretise s sigs =
   let () = if (!Param.debug_mode) then
              (Format.printf "concretise linear poset :";
               List.iter (fun i -> Format.printf "%d " i) s.LinearPoset.seq) in
-  let (trace,_) =
+  let init_state = Replay.init_state in
+  let trace =
     List.fold_left
-      (fun (trace,rf) eid ->
+      (fun trace eid ->
         let event = Poset.get_event_by_id eid s.LinearPoset.pos in
         let step = Event.get_step event in
-        let m = Transition.get_rhs (TraceConcret.get_first_transition trace) in
-        let (trans,new_nodes,new_ports) =
-          Transition.make m step
-                          trace.TraceConcret.node_names
-                          trace.TraceConcret.port_names in
-        ((TraceConcret.add_transition trace trans new_nodes new_ports),
-         ((eid,trans)::rf)))
-      (TraceConcret.empty,[]) s.LinearPoset.seq in
-  trace
+        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
 
+        TraceConcret.add_transition trace trans)
+      TraceConcret.empty s.LinearPoset.seq in
+  trace
 
-let concret (s:Poset.t) = concretise (linears s)
+let concret s sigs = concretise (linears s) sigs

concret.mli

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

formulas.ml

@@ -243,10 +243,13 @@ let obs = function
     Domain.Pos p -> p
   | _ -> raise (ExceptDefn.Malformed_Args("obs"))
 
-let negative_influence = function
+let negative_influence env = function
     (Domain.Pos p1, Domain.Pos p2) ->
-    let t = Concret.concret p1 in
-    let () = if (!Param.debug_mode) then TraceConcret.print t in
+    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*)
     true
    | _ ->  raise(ExceptDefn.Malformed_Args("negative_influence"))
 
@@ -260,7 +263,7 @@ let check_pred p =
     (String.equal is_label "label")
   else false
 
-let interpretation t =
+let interpretation env t =
   let domain = (List.map (fun p -> Domain.Pos(p)) (Domain.get_posets(t)))@
                  (List.map (fun e -> Domain.Ev(e)) (Domain.get_events(t))) in
   let func f args =
@@ -284,6 +287,6 @@ let interpretation t =
       | ("equal_events", [e1;e2]) -> equal_events (e1,e2)
       | ("sub_posets", [p1;p2]) -> sub_poset (p1,p2)
       | ("negative_influence", [p1;p2]) ->
-         negative_influence (p1,p2)
+         negative_influence env (p1,p2)
       | _ -> raise (ExceptDefn.Uninterpreted_Predicate(p)) in
   (func,pred,domain)

formulas.mli

@@ -21,7 +21,7 @@ val holds : (string -> Domain.domain list -> Domain.domain) *
                 (Domain.domain list) ->
             (string -> Domain.domain) -> Domain.domain fol formula -> bool
 
-val interpretation : Domain.t ->
+val interpretation : Model.t -> Domain.t ->
                      (string -> Domain.domain list -> Domain.domain) *
                        (string -> Domain.domain list -> bool) *
                          Domain.domain list

main.ml

@@ -91,7 +91,7 @@ let () =
                     [Formulas.Var "s1";
                      Formulas.Var "s2"]))) in
 
-  let m = Formulas.interpretation posets in
+  let m = Formulas.interpretation env posets in
   let () = Format.printf "\n evaluate formula\n" in
   (evaluate fm_neg m empty_valuation)
 

traceConcret.ml

@@ -1,23 +1,18 @@
 
-type t = {
-    transitions : Transition.t list;
-    node_names : Maps.node_map;
-    port_names : Maps.port_map;
-  }
+type s = Transition.s list
 
-let empty = {transitions = [];node_names=[];port_names=[]}
+type t = Transition.t list
 
-let print t = List.iter (fun trans -> Transition.print trans) t.transitions
+let empty = []
 
-let get_first_transition t =
-  try
-    List.hd t.transitions
-  with Failure s -> Transition.empty
+(*
+let print t sigs = List.iter (fun trans -> Transition.print trans sigs) t
+ *)
 
-let get_last_transition t =
-    List.nth t.transitions ((List.length t.transitions)-1)
+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 add_transition trace trans new_nodes new_ports =
-  {transitions=trans::trace.transitions;
-   node_names=new_nodes;
-   port_names=new_ports;}
+let pattern_trace contact_map sigs pre_env trace =
+  List.map (fun trans ->
+             Transition.pattern_transition contact_map sigs pre_env trans) trace

traceConcret.mli

@@ -1,14 +1,13 @@
+type s = Transition.s list
+type t = Transition.t list
 
-type t = {
-    transitions : Transition.t list;
-    node_names : Maps.node_map;
-    port_names : Maps.port_map;
-  }
 
-val empty: t
-val print: t -> unit
+val empty: s
+(*val print: t -> Signature.s -> unit*)
 
-val get_last_transition: t -> Transition.t
-val get_first_transition: t -> Transition.t
-val add_transition: t -> Transition.t -> Maps.node_map ->
-                     Maps.port_map ->t
+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