coding

Author: Ioana

ast.ml

@@ -74,47 +74,51 @@ let add_free_to_mix mix =
             {port_nme=p.port_nme;port_int=p.port_int; port_lnk=p_lnks}) pl in
       (n,pl')) mix
 
-let split_ports_quarks count port =
+let split_port_quarks id_node id_port port =
   let quark_int = match port.port_int with
     | [] -> []
-    | s::_ -> [(count,port.port_nme,(Rule.INT s))] in
+    | s::_ -> [(id_node,id_port,(Rule.INT s))] in
   match port.port_lnk with
   | [] -> []
   | l::_ -> match l with
             | LNK_VALUE i ->
                let rule_lnk = Rule.LNK (Idgraph.LNK_VALUE i) in
-               (count,port.port_nme,rule_lnk)::quark_int
+               (id_node,id_port,rule_lnk)::quark_int
             | FREE ->
                let rule_lnk = Rule.LNK (Idgraph.FREE) in
-               (count,port.port_nme,rule_lnk)::quark_int
+               (id_node,id_port,rule_lnk)::quark_int
             | LNK_ANY -> quark_int
             | LNK_SOME | LNK_TYPE _ ->
                (raise (ExceptionDefn.Not_Supported
                          ("rules with side effects not supported")))
 
+let split_ports_in_quarks count plist =
+  let (_,qs) =
+    List.fold_left (fun (i,acc) port ->
+                     (i+1,(split_port_quarks count i port)@acc))
+                   (0,[]) plist in
+  qs
+
 let create_quarks mixture count =
   List.fold_left
-    (fun (qs,agent_names,count) ((name:string),plist) ->
-      let qs' =
-        List.fold_left
-          (fun acc port -> (split_ports_quarks count port)@acc) [] plist in
-      (qs'@qs,(count,name)::agent_names,count+1))
-    ([],[],count) mixture
-
-let create_rhs_quarks agent_names mixture =
-  let rec aux qs mixt count ag_nm =
+    (fun (qs,agent_names,port_names,count) ((name:string),plist) ->
+      let qs' = split_ports_in_quarks count plist in
+      let ports = List.mapi (fun i p -> (i,p.port_nme)) plist in
+      (qs'@qs,(count,name)::agent_names,(count,ports)::port_names,count+1))
+    ([],[],[],count) mixture
+
+let create_rhs_quarks agent_names port_names mixture =
+  let rec aux qs mixt count ag_nm po_nm =
     match mixt with
     | (name,plist)::mixt' ->
        if (((List.length ag_nm) >0)&&(List.mem (count,name) ag_nm)) then
-         let qs' =
-           List.fold_left
-             (fun acc port -> (split_ports_quarks count port)@acc) [] plist in
-         aux (qs'@qs) mixt' (count+1) ag_nm
+         let qs' = split_ports_in_quarks count plist in
+         aux (qs'@qs) mixt' (count+1) ag_nm po_nm
        else
-         let (qs',ag_nm',_) = create_quarks mixt (List.length ag_nm) in
-         (qs'@qs, ag_nm'@ag_nm)
-    | [] -> (qs, ag_nm) in
-  aux [] mixture 0 agent_names
+         let (qs',ag_nm',po_nm',_) = create_quarks mixt (List.length ag_nm) in
+         (qs'@qs, ag_nm'@ag_nm, po_nm')
+    | [] -> (qs, ag_nm, po_nm) in
+  aux [] mixture 0 agent_names port_names
 
 let match_il il il' = match (il,il') with
   | (Rule.INT _,Rule.INT _) | (Rule.LNK _,Rule.LNK _) -> true
@@ -123,12 +127,12 @@ let match_il il il' = match (il,il') with
 let remove_quark (n,p,il) ls =
   List.filter
     (fun (n',p',il') ->
-      (not((n=n')&&(String.equal p p')&&(match_il il il')))) ls
+      (not((n=n')&&(p=p')&&(match_il il il')))) ls
 
 let partition_quarks lhs_quarks rhs_quarks =
   let find (n,p,il) rhs =
     List.find (fun (n',p',il') ->
-                (n=n')&&(String.equal p p')&&(match_il il il')) rhs in
+                (n=n')&&(p=p')&&(match_il il il')) rhs in
   let (qlist,rhs)=
     List.fold_left
       (fun (qlist',rhs') (n,p,il) ->
@@ -158,26 +162,27 @@ let partition_quarks lhs_quarks rhs_quarks =
   (modified@qlist)
 
 let create_prefix_map lhs rhs =
-  let (lhs_quarks,lhs_agent_nm,_) = create_quarks lhs 0 in
-  let (rhs_quarks,rhs_agent_nm) = create_rhs_quarks lhs_agent_nm rhs in
+  let (lhs_quarks,lhs_an,lhs_pn,_) = create_quarks lhs 0 in
+  let (rhs_quarks,rhs_an,rhs_pn) = create_rhs_quarks lhs_an lhs_pn rhs in
   let () = Format.printf "rhs_agent = ";
-           List.iter (fun (c,n) -> Format.printf "(%d,%s) " c n) rhs_agent_nm in
-  (partition_quarks lhs_quarks rhs_quarks,rhs_agent_nm)
+           Maps.printn rhs_an; Maps.printp rhs_pn in
+  (partition_quarks lhs_quarks rhs_quarks,rhs_an,rhs_pn)
 
 let clean_rule = function
   | INIT mix ->
-     let (quarks,agent_names) = create_prefix_map [] (add_free_to_mix mix) in
+     let (quarks,agent_names,port_names) =
+       create_prefix_map [] (add_free_to_mix mix) in
      let label = List.fold_left (fun acc (nme,_) -> acc^nme) "" mix in
-     Rule.INIT (label,quarks,agent_names)
+     Rule.INIT (label,quarks,agent_names,port_names)
   | OBS (name,mix) ->
      let mix' = add_free_to_mix mix in
-     let (quarks,agent_names) = create_prefix_map mix' mix'  in
-     Rule.OBS (name,quarks,agent_names)
+     let (quarks,agent_names,port_names) = create_prefix_map mix' mix'  in
+     Rule.OBS (name,quarks,agent_names,port_names)
   | RULE (name,r) ->
      let () = if (r.bidirectional) then
                 (raise (ExceptionDefn.Not_Supported
                           ("bidirectional rules not supported"))) in
      let lhs = add_free_to_mix r.lhs in
      let rhs = add_free_to_mix r.rhs in
-     let (quarks,agent_names) = create_prefix_map lhs rhs in
-     Rule.RULE (name,quarks,agent_names)
+     let (quarks,agent_names,port_names) = create_prefix_map lhs rhs in
+     Rule.RULE (name,quarks,agent_names,port_names)

concret.ml

@@ -20,7 +20,7 @@ let concretise (s:LinearPoset.t) (rs:Rule.t list) =
       (Trace.empty,[]) s.LinearPoset.seq in
   trace
 
-let test_concret (s:LinearPoset.t) (rs:Rule.t list) =
+(*let test_concret (s:LinearPoset.t) (rs:Rule.t list) =
   let () = if (!Parameter.debug_mode) then
              (Format.printf "concretise linear poset :";
               List.iter (fun i -> Format.printf "%d " i) s.LinearPoset.seq) in
@@ -37,5 +37,6 @@ let test_concret (s:LinearPoset.t) (rs:Rule.t list) =
   let () = if (!Parameter.debug_mode) then
               Transition.print trans in
   Trace.empty
+ *)
 
 let concret (s:Poset.t) (rs:Rule.t list) = concretise (linears s) rs

event.ml

@@ -38,7 +38,7 @@ let nodes_of_json (node:Yojson.Basic.json) =
      let () = if ((Quark.exists_mod clean_quarks [0;1])
                   &&(Quark.exists_testmod clean_quarks [0;1])) then
                 (raise (ExceptionDefn.NotKappa_Poset
-                          ("quarks of init event not valid"))) in
+                          ("quarks of obs event not valid"))) in
      { event_id = id; event_label = label; quarks = clean_quarks; }
   | `List [`Int id; `String "INIT"; `List l;
            (`Assoc ["quarks", `List ql])] ->

lib.ml

@@ -1,3 +1,6 @@
+(* interleave 1 [2;3] = [ [1;2;3]; [2;1;3]; [2;3;1] ] *)
+(*permutations [1; 2; 3] =
+[[1; 2; 3]; [2; 1; 3]; [2; 3; 1]; [1; 3; 2]; [3; 1; 2]; [3; 2; 1]] *)
 
 let fst (a,b) = a
 let snd (a,b) = b
@@ -16,16 +19,24 @@ let remove_duplicates l compare =
     | x :: xs -> go (remove_elt x xs compare) (x::acc)
   in go l []
 
-(* interleave 1 [2;3] = [ [1;2;3]; [2;1;3]; [2;3;1] ] *)
 let rec interleave x lst =
-match lst with
-| [] -> [[x]]
-| hd::tl -> (x::lst) :: (List.map (fun y -> hd::y) (interleave x tl))
+  match lst with
+  | [] -> [[x]]
+  | hd::tl -> (x::lst) :: (List.map (fun y -> hd::y) (interleave x tl))
 
-(*permutations [1; 2; 3] =
-[[1; 2; 3]; [2; 1; 3]; [2; 3; 1]; [1; 3; 2]; [3; 1; 2]; [3; 2; 1]] *)
 let rec permutations lst =
-match lst with
-| hd::tl -> List.concat (List.map (interleave hd) (permutations tl))
-| _ -> [lst]
-;;
+  match lst with
+  | hd::tl -> List.concat (List.map (interleave hd) (permutations tl))
+  | _ -> [lst]
+
+let mapping list1 list combine =
+  let list_of_list = permutations list in
+  List.fold_left
+    (fun acc list2 ->
+      try
+        let working_map =
+          List.map2 (fun p1 p2 ->
+                      if (combine p1 p2) then (p1,p2)
+                      else (raise (ExceptionDefn.Mappings()))) list1 list2 in
+        working_map::acc
+      with ExceptionDefn.Mappings() -> acc) [] list_of_list

lib.mli

@@ -4,3 +4,4 @@ val thd : 'a* 'b* 'c -> 'c
 
 val remove_duplicates : 'a list -> ('a -> 'a -> bool) -> 'a list
 val permutations : 'a list -> 'a list list
+val mapping : 'a list -> 'b list -> ('a -> 'b -> bool) -> ('a*'b) list list

notes/ts_graphs.tex

@@ -152,7 +152,7 @@ \subsection{Transition systems}
   Let $t_1:M_1\overset{m_1,p_1}{\Rightarrow} N_1$ and $t_2:M_2\overset{m_2,p_2}{\Rightarrow} N_2$ be two transitions in a trace $\theta:t_1;t_1':t_2';\cdots t_n';t_2$ and let $p_1:L_1{\remb} D_1 {\lemb} R_1$ and $p_2:L_2{\remb} D_2 {\lemb} R_2$ be two corresponding rules. The morphism $M_1\pmorph M_2$ is the composition of $\spo(t_1)\circ\spo(t_1')\circ\dots\spo(t_n')$.
   \begin{description}
   \item[high res inhibition]
-    Let the span $\spa:L_1\remb O\lemb L_2$ be the pullback of the cospan $L_1{\lemb}M{\remb}L_2$ in the multisum of $L_1$ and $L_2$ such that $p_1\redl{-}_{\spa} p_2$. If the diagram commutes
+    Let the span $\spa:L_1\remb O\lemb L_2$ be the pullback of the cospan $L_1{\lemb}M{\remb}L_2$ in the multisum of $L_1$ and $L_2$ such that $p_2\redl{-}_{\spa} p_1$. If the diagram commutes
   \[
   \begin{tikzpicture} %[scale=0.8]
     \node (o) at (1,0) {\(O\)};
@@ -179,7 +179,7 @@ \subsection{Transition systems}
   \]
   then $t_2$ is high res inhibiting $t_1$, denoted $t_2 \Dashv t_1$.
 \item[low res inhibition]
-  If there exists $\spa:L_1\remb O\lemb L_2$ such that $p_1\redl{-}_{\spa} p_2$ and such that the diagram commutes
+  If there exists $\spa:L_1\remb O\lemb L_2$ such that $p_2\redl{-}_{\spa} p_1$ and such that the diagram commutes
   \[
   \begin{tikzpicture} %[scale=0.8]
     \node (o) at (1,0) {\(O\)};
@@ -326,7 +326,7 @@ \subsection{Transition systems}
 
 \begin{definition}[Equivalence on transitions]
   \label{def:equiv_trans}
-  Let $\sim$ be a binary relation on transitions such that $t_1\sim t_1'$ iff there exists $t_2$, $t_1\Diamond_{\text{par}} t_2$ and $t_1' = t_1/t_2$.
+  Let $\sim$ be a binary relation on transitions such that $t_1\sim t_1'$ iff there exists $t_2$, $t_1\Diamond_{\text{par}} t_2$ and $t_1' = t_1/t_2$. We denote $\simeq$ the transitive and reflexive closure of $\sim$.
   %% \begin{itemize}
   %% \item there exists $t_2$, $t_2;t_1$, $\neg(t_2<t_2)$, $\neg(t_2\Diamond_{\text{seq}}t_1)$ and $t_1=t_1|t_2$.
   %% \end{itemize}

rule.ml

@@ -1,36 +1,63 @@
 type lnk_or_int = INT of string
                 | LNK of Idgraph.link
 
-type quark = Tested of (int*string*lnk_or_int)
-            | TestedMod of ((int*string*lnk_or_int)*(int*string*lnk_or_int))
-            | Modified of (int*string*lnk_or_int)
+type quark = Tested of (int*int*lnk_or_int)
+            | TestedMod of ((int*int*lnk_or_int)*(int*int*lnk_or_int))
+            | Modified of (int*int*lnk_or_int)
 
-type rule = string*(quark list)*((int*string) list)
+type rule = string*(quark list)*Maps.node_map*Maps.port_map
 
 type t = INIT of rule
        | OBS of rule
        | RULE of rule
 
-let empty = RULE ("empty",[],[])
+let make_port pid il pname =
+  let (internal,lnk) =
+    (match il with
+     | INT s -> ([s],[])
+     | LNK lnk -> ([],[lnk])) in
+  { Idgraph.port_nme = pname;
+    Idgraph.port_id = pid;
+    Idgraph.port_int = internal;
+    Idgraph.port_lnk = lnk;}
+
+let make_agent aname pname = function
+  | Modified (ag,p,il) ->
+     let port = make_port p il pname in
+     (aname,ag,[port])
+  | _ -> (raise (ExceptionDefn.Internal_Error("make_agent")))
+
+let empty = RULE ("empty",[],[],[])
 
 let get_quarks = function
-  | INIT (_,qs,_) | OBS (_,qs,_) | RULE (_,qs,_) -> qs
+  | INIT (_,qs,_,_) | OBS (_,qs,_,_) | RULE (_,qs,_,_) -> qs
 
 let get_node_map = function
-  | INIT (_,_,nm) | OBS (_,_,nm) | RULE (_,_,nm) -> nm
+  | INIT (_,_,nm,_) | OBS (_,_,nm,_) | RULE (_,_,nm,_) -> nm
+
+let get_port_map = function
+  | INIT (_,_,_,nm) | OBS (_,_,_,nm) | RULE (_,_,_,nm) -> nm
 
 let get_agent = function
     Tested (ag,_,_) | TestedMod ((ag,_,_),_) | Modified (ag,_,_) -> ag
 
 let get_port = function
     Tested (_,p,_) | TestedMod ((_,p,_),_) | Modified (_,p,_) -> p
 
-let print_quarks qlist nmap =
+let get_il = function
+    Tested (_,_,il) | TestedMod ((_,_,il),_) | Modified (_,_,il) -> il
+
+let print_quarks qlist nmap pmap =
   let print_triple (n,p,il) =
     (try
-      let (_,agent_name) = List.find (fun (id,na) -> id=n) nmap in
-      Format.printf "(%s%d,%s," agent_name n p;
-    with _ -> Format.printf "(%d,%s," n p);
+       let (_,agent_name) = List.find (fun (id,na) -> id=n) nmap in
+       Format.printf "(%s%d," agent_name n;
+       (try
+          let (_,plist) = List.find (fun (id,plist) -> id=n) pmap in
+          let (_,port_name) = List.find (fun (idp,na) -> idp=p) plist in
+          Format.printf "%s%d," port_name p;
+        with _ -> Format.printf "%d" p);
+     with _ -> Format.printf "(%d,%d" n p);
     (match il with
        INT i -> Format.printf "int=%s " i
      | LNK lnk ->
@@ -49,37 +76,22 @@ let print_quarks qlist nmap =
   List.iter (fun q -> print_q q) qlist
 
 let print t =
-  let print_rule (label,qs,nmap) =
-    Format.printf "rule %s = " label; print_quarks qs nmap in
+  let print_rule (label,qs,nmap,pmap) =
+    Format.printf "rule %s = " label; print_quarks qs nmap pmap in
   match t with
   | INIT r ->  Format.printf "\ninit ";print_rule r
   | OBS r ->  Format.printf "\nobs ";print_rule r
   | RULE r ->  Format.printf "\nrule ";print_rule r
 
 
 let get_label = function
-  | INIT (name,_,_) | OBS (name,_,_) | RULE (name,_,_) ->  name
+  | INIT (name,_,_,_) | OBS (name,_,_,_) | RULE (name,_,_,_) ->  name
 
 let get_rule_by_label nme rules =
   List.find (fun r -> String.equal (get_label r) nme) rules
 
-(*
-let get_rhs = function
-  | INIT mix -> mix
-  | OBS (name,mix) -> mix
-  | RULE (name,r) -> r.rhs
-
-let is_init = function
-  | INIT _ -> true
-  | OBS _ | RULE _ -> false
-
-let is_obs = function
-  | OBS _ -> true
-  | INIT _ | RULE _  -> false
- *)
-
 let filter_on_port p quarks =
-  List.filter (fun q -> (String.equal (get_port q) p)) quarks
+  List.filter (fun q -> (get_port q)=p) quarks
 
 let filter_on_node n quarks =
   List.filter (fun q -> ((get_agent q)=n)) quarks
@@ -109,12 +121,11 @@ let mod_il = function Modified (_,_,il) -> (match il with
                     | _ -> None
 
 let find_replace (n1,n2) (p1,p2) quarks =
-  let () = Format.printf "find_replace (%d,%d) (%s,%d)" n1 n2 p1 p2 in
   List.map (function
-            |Tested (n,p,il) as q -> if ((n=n1)&&(String.equal p1 p)) then
-                                       Tested (n2,p,il) else q
+            |Tested (n,p,il) as q -> if ((n=n1)&&(p1=p)) then
+                                       Tested (n2,p2,il) else q
             |TestedMod ((n,p,il),(_,_,il')) as q ->
-                        if ((n=n1)&&(String.equal p1 p)) then
-                          TestedMod ((n2,p,il),(n2,p,il')) else q
-            |Modified (n,p,il) as q -> if ((n=n1)&&(String.equal p1 p)) then
-                                         Modified (n2,p,il) else q) quarks
+                        if ((n=n1)&&(p1=p)) then
+                          TestedMod ((n2,p2,il),(n2,p2,il')) else q
+            |Modified (n,p,il) as q -> if ((n=n1)&&(p1=p)) then
+                                         Modified (n2,p2,il) else q) quarks