code

Author: Ioana

ast.ml

@@ -1,16 +1,16 @@
-type ('a) link =
+type link =
   | LNK_VALUE of int
   | FREE
   | LNK_ANY
   | LNK_SOME
-  | LNK_TYPE of 'a (* port *)
-    * 'a (*agent_type*)
+  | LNK_TYPE of string (* port *)
+    * string (*agent_type*)
 
 type internal = string list
 
 type port = {port_nme:string;
              port_int:internal;
-             port_lnk:string link list;}
+             port_lnk:link list;}
 
 type agent = (string * port list)
 
@@ -53,4 +53,35 @@ let print = function
   | INIT mix -> Format.printf "\n init "; List.iter (fun a -> print_agent a) mix
   | OBS (name,mix) -> Format.printf "\n obs '%s' " name;
                       List.iter (fun a -> print_agent a) mix
-  | RULE (name,r) -> Format.printf "\n rule '%s' " name; print_rule r;
+  | RULE (name,r) -> Format.printf "\n rule '%s' " name; print_rule r
+
+let empty_rule = {lhs =[];rhs=[];bidirectional=false}
+
+let empty = RULE ("empty",empty_rule)
+
+let get_label = function
+  | INIT mix -> List.fold_left (fun acc (nme,_) -> acc^nme) "" mix
+  | OBS (name,_) -> name
+  | RULE (name,_) ->  name
+
+let get_rule_by_label nme rules =
+  List.find
+    (fun r -> String.equal (get_label r) nme) rules
+
+let get_lhs = function
+  | INIT mix -> []
+  | OBS (name,mix) -> mix
+  | RULE (name,r) -> r.lhs
+
+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

ast.mli

@@ -1,16 +1,16 @@
-type ('a) link =
+type link =
   | LNK_VALUE of int
   | FREE
   | LNK_ANY
   | LNK_SOME
-  | LNK_TYPE of 'a (* port *)
-    * 'a (*agent_type*)
+  | LNK_TYPE of string (* port *)
+    * string (*agent_type*)
 
 type internal = string list
 
 type port = {port_nme:string;
              port_int:internal;
-             port_lnk:string link list;}
+             port_lnk:link list;}
 
 type agent = (string * port list)
 
@@ -24,4 +24,16 @@ type rule = {
 type t = INIT of mixture
        | OBS of string*mixture
        | RULE of string*rule
+
+val empty : t
+
+val print_port : port -> unit
 val print : t -> unit
+
+val get_label : t -> String.t
+val get_rule_by_label : String.t -> t list -> t
+
+val get_lhs : t -> mixture
+val get_rhs : t -> mixture
+val is_init : t -> bool
+val is_obs : t -> bool

concret.ml

@@ -1,14 +1,41 @@
 
-let decorate s = [s]
-
 let linears s =
   LinearPoset.linearisations(s)
 
-let refine (t:Trace.t) (r: (Event.t*Transition.t) list) s id = [Trace.empty]
+let concretise (s:LinearPoset.t) (rs:Ast.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
+  let (trace,_) =
+    List.fold_left
+      (fun (trace,rf) eid ->
+        let event = Poset.get_event_by_id eid s.LinearPoset.pos in
+        let rname = Event.get_label event in
+        let rule = Ast.get_rule_by_label rname rs in
+        let m = Transition.get_rhs (Trace.get_first_transition trace) in
+        let trans = Transition.make m rule (Event.get_quarks event) in
+        ((Trace.add_transition trace trans), ((eid,trans)::rf)))
+          (* else (raise (ExceptionDefn.NotKappa_Poset *)
+          (*                ("quarks of event "^rname^" not valid")))) *)
+      (Trace.empty,[]) s.LinearPoset.seq in
+  trace
+
+let test_concret (s:LinearPoset.t) (rs:Ast.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
+  let event = Poset.get_event_by_id 4 s.LinearPoset.pos in
+  let rname = Event.get_label event in
+  let rule = Ast.get_rule_by_label rname rs in
+
+  let () = if (!Parameter.debug_mode) then
+             (Format.printf "info on first event ";
+              Event.print_event event;
+              Ast.print rule) in
 
-let concretise (s:LinearPoset.t) id concretisations1 =
-  List.fold_left
-    (fun concretisations2
-         (t,r) -> refine t r s id) [] concretisations1
+  let trans = Transition.make [] rule (Event.get_quarks event) in
+  let () = if (!Parameter.debug_mode) then
+              Transition.print trans in
+  Trace.empty
 
-let concret (s:Poset.t) = concretise (linears s) 0 []
+let concret (s:Poset.t) (rs:Ast.t list) = concretise (linears s) rs

concret.mli

@@ -1,2 +1,2 @@
 
-val concret : Poset.t -> Trace.t list
+val concret : Poset.t -> Ast.t list -> Trace.t

domain.ml

@@ -51,8 +51,8 @@ let set_posets file_list =
       (fun t file ->
         let s = Poset.read_poset_from_file file in
         add_posets s t) posets file_list in
-  let posets' = add_posets (Poset.test_poset) posets_file in
+  (*let posets' = add_posets (Poset.test_poset) posets_file in*)
   let () = if (!Parameter.debug_mode)
            then (Format.printf "set_posets: \n";
-                 print_posets posets') in
-  posets'
+                 print_posets posets_file) in
+  posets_file

event.ml

@@ -1,4 +1,7 @@
 open Yojson
+open Lib
+
+(*module IntMap = Map.Make(struct type t = int let compare = compare end)*)
 
 type quark =
   | Tested of (int*int*int)
@@ -13,6 +16,7 @@ type t = {
 
 let get_id e = e.event_id
 let get_label e = e.event_label
+let get_quarks e = e.quarks
 
 let test_event event_id event_label =
  { event_id; event_label; quarks = []; }
@@ -66,3 +70,48 @@ let nodes_of_json (node:Yojson.Basic.json) =
        List.map (fun q -> quarks_of_json q) ql in
      { event_id = id; event_label = init_label; quarks = quarks_ls; }
   | _ -> raise (Yojson.Basic.Util.Type_error ("Not in the cflow format",`Null))
+
+let quarks_tested qs =
+  List.filter (function
+                 Tested _ -> true
+               | Modified _ | TestedMod _ -> false) qs
+
+let quarks_testedMod qs =
+  List.filter (function
+                 TestedMod _ -> true
+               | Modified _ | Tested _ -> false) qs
+
+let quarks_modified qs =
+  List.filter (function
+                 Modified _ -> true
+               | Tested _ | TestedMod _ -> false) qs
+
+let get_nodes qs =
+  List.fold_left
+    (fun nodes -> function
+      | Modified (ni,pi,il)| Tested (ni,pi,il)| TestedMod (ni,pi,il) ->
+         if (List.mem ni nodes) then nodes else ni::nodes) [] qs
+
+let get_nodes_ports qs =
+  let n = List.length (get_nodes qs) in
+  let myhash = Hashtbl.create n in
+
+  let build_port_list n p qs =
+    let (qs_np,rest)=
+      List.partition
+        (function
+         | Modified (ni,pi,_)| Tested (ni,pi,_)| TestedMod (ni,pi,_) ->
+            (n=ni)&&(p=pi)) qs in
+    let plist =
+      List.map
+        (function Modified t| Tested t| TestedMod t -> Lib.thd t) qs_np in
+    (plist,rest) in
+
+  let rec build_map qs = match qs with
+    | [] -> myhash
+    | q::rs -> match q with
+               | Modified (ni,pi,_)| Tested (ni,pi,_)| TestedMod (ni,pi,_) ->
+                  let (port,rest) = build_port_list ni pi qs in
+                  let () = if (pi >= 0) then Hashtbl.add myhash ni (pi,port) in
+                  build_map rest in
+  build_map qs

event.mli

@@ -1,5 +1,7 @@
 open Yojson
 
+(*module IntMap : Map.S with type key = int*)
+
 type quark =
   | Tested of (int*int*int)
   | Modified of (int*int*int)
@@ -15,6 +17,13 @@ val nodes_of_json : Yojson.Basic.json -> t
 
 val get_id : t -> int
 val get_label : t -> string
+val get_quarks : t -> quark list
 
 val print_event : t -> unit
 val test_event : int -> string -> t
+
+val quarks_tested : quark list -> quark list
+val quarks_testedMod : quark list -> quark list
+val quarks_modified : quark list -> quark list
+val get_nodes : quark list -> int list
+val get_nodes_ports : quark list -> (int, (int*int list)) Hashtbl.t

exceptionDefn.ml

@@ -1,7 +1,10 @@
 exception Syntax_Error of string
+exception Not_Supported of string
+exception NotKappa_Poset of string
 exception Malformed_Decl of string
 exception Malformed_Args of string
 exception Internal_Error of string
 exception Uninterpreted_Variable of string
 exception Uninterpreted_Predicate of string
 exception Uninterpreted_Function of string
+exception Mappings of unit

formulas.ml

@@ -167,9 +167,6 @@ let denotations (_,_,domain as m) fm =
          vals
          (List.filter (fun d -> domain_match_sort d "Poset") domain)
     | [] ->
- (*      let () = if (!Parameter.debug_mode) then
-                  Format.printf "holds test for valuation ";
-                print_valuation v (vars) in*)
        if (holds m valuation fm) then (valuation::vals) else (vals) in
   let default_valuation x = raise (ExceptionDefn.Uninterpreted_Variable(x)) in
   denote_var (free_var fm) default_valuation []
@@ -246,17 +243,15 @@ let obs = function
     Domain.Pos p -> p
   | _ -> raise (ExceptionDefn.Malformed_Args("obs"))
 
-let negative_influence = function
-    (Domain.Ev e1, Domain.Pos p1, Domain.Ev e2, Domain.Pos p2) ->
-    let bla = Concret.concret p1 in
+let negative_influence rules = function
+    (Domain.Pos p1, Domain.Pos p2) ->
+    let t = Concret.concret p1 rules in
+    let () = if (!Parameter.debug_mode) then Trace.print t in
     true
    | _ ->  raise(ExceptionDefn.Malformed_Args("negative_influence"))
 
 let id_label_event str = function
-    [e] ->
-(*    let () = if (!Parameter.debug_mode) then
-               Format.printf "id_label_event %s\n" str in*)
-    ((label e) = str)
+    [e] -> ((label e) = str)
   | _ -> raise (ExceptionDefn.Malformed_Args("id_label_event"))
 
 let check_pred p =
@@ -265,7 +260,7 @@ let check_pred p =
     (String.equal is_label "label")
   else false
 
-let interpretation t =
+let interpretation t rules =
   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 =
@@ -288,7 +283,7 @@ let interpretation 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", [x1;p1;x2;p2]) ->
-         negative_influence (x1,p1,x2,p2)
+      | ("negative_influence", [p1;p2]) ->
+         negative_influence rules (p1,p2)
       | _ -> raise (ExceptionDefn.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 : Domain.t -> Ast.t list ->
                      (string -> Domain.domain list -> Domain.domain) *
                        (string -> Domain.domain list -> bool) *
                          Domain.domain list