Commit aab6423f authored by erwan's avatar erwan
Browse files

Update: use lib/sasacore/topology.ml file in dot.ml

instead of duplicating its content
parent ef99119a
(* Time-stamp: <modified the 22/03/2019 (at 09:28) by Erwan Jahier> *)
(* Time-stamp: <modified the 22/03/2019 (at 14:30) by Erwan Jahier> *)
open Process
......@@ -15,7 +15,7 @@ let (gen_atmost_macro : int -> string) =
for i=1 to n do
for j=1 to n do
let istr = string_of_int j in
str := !str ^ (if i=j then "x"^istr else ("not(x"^istr^")"));
str := !str ^ (if i=j then " x"^istr^" " else ("not(x"^istr^")"));
str := !str ^ (if j<n then " and " else
if i =n then "" else ") or\n\t\t(");
done;
......@@ -60,12 +60,12 @@ let (f: Process.t list -> string) =
let nl = List.filter (fun n -> n>1) nl in
let atmost_macro_l = List.map gen_atmost_macro nl in
let atmost_macro = String.concat "\n" atmost_macro_l in
let atleastone = "("^(String.concat " or " al)^") and " in
(* let atleastone = "("^(String.concat " or " al)^") and " in *)
let macro = Printf.sprintf "%s
%s
let demon_prop(%s,\n\t%s:bool):bool =\n\t\t%s\n\t\t%s%s"
let demon_prop(%s,\n\t%s:bool):bool =\n\t\t%s%s"
(Mypervasives.entete "--" SasaVersion.str SasaVersion.sha)
atmost_macro (ins "\n\t") (outs "\n\t") atleastone acti_if_enab one_per_process
atmost_macro (ins "\n\t") (outs "\n\t") acti_if_enab one_per_process
in
let distributed = Printf.sprintf
......
# Time-stamp: <modified the 22/03/2019 (at 09:55) by Erwan Jahier>
# Time-stamp: <modified the 22/03/2019 (at 14:47) by Erwan Jahier>
test: p.cmxs
test: p.cmxs ring.lut
$(sasa) -l 200 ring.dot
......
# Time-stamp: <modified the 22/03/2019 (at 09:54) by Erwan Jahier>
# Time-stamp: <modified the 22/03/2019 (at 14:48) by Erwan Jahier>
test: cmxs
test: cmxs ring.lut
$(sasa) ring.dot
cmxs: ring.cmxs ringroot.cmxs
......
#require "ocamlgraph";;
open Graph
open Graph.Dot_ast
open Data
open Event
(* XXX duplicated from lib/sasacore/topology.ml:
make a user lib out of it.
*)
type node_id = string
type node = {
id: node_id;
file: string;
init: (string * string) list;
}
type edge = node_id * node_id list
type t = node list * string
type node_info_t = (string, node) Hashtbl.t
let node_info:node_info_t = Hashtbl.create 100
type node_succ_t = (string, string list) Hashtbl.t
let node_succ:node_succ_t = Hashtbl.create 100
let (of_id:Dot_ast.id -> string) =
function Ident str | Html str | Number str | String str -> str
let (of_node_id:Dot_ast.node_id -> string) = fun id -> of_id (fst id)
let (of_node:Dot_ast.node -> string) = function
| NodeId node_id -> of_node_id node_id
| NodeSub _subgraph -> assert false
let (get_file: Dot_ast.node_id -> Dot_ast.attr list -> string) =
fun node_id attrs ->
let attrs = List.flatten attrs in
try (
match List.assoc (Ident "algo") attrs with
None -> assert false
| Some id -> of_id id
)
with Not_found -> failwith ((of_node_id node_id)^" should have an algo attribute")
let (get_init: Dot_ast.attr list -> (string * string) list ) =
fun attrs ->
let attrs = List.flatten attrs in (* XXX why a list of list ? *)
let init_list =
List.fold_left
(fun acc (id,idopt) ->
if id <> Ident "init" then acc else
match idopt with
| Some (String id) -> (
try
let i = String.index id '=' in
let l = String.length id in
(String.sub id 0 i, String.sub id (i+1) (l-i-1))::acc
with
Not_found -> acc
)
| _ -> acc
)
[]
attrs
in
init_list
let (do_stmt: bool -> node list -> Dot_ast.stmt -> node list) =
fun directed n stmt ->
match stmt with
| Node_stmt (node_id, attrs) ->
let id = of_node_id node_id in
let inits = get_init attrs in
let node = { id=id ; file = get_file node_id attrs ; init = inits } in
if Hashtbl.mem node_info id then
failwith (id ^ " defined twice")
else
Hashtbl.add node_info id node;
node::n
| Edge_stmt (node, nodes, _attrs) ->
let node = of_node node in
let nodes = List.map of_node nodes in
(* for egdes written "a -- b -- c -- d", which
is a shortcut for "
a -- b
b -- c
c -- d
"
Graph.Dot.parse_dot_ast returns the pair a,[b,c,d]
which is weird IMHO.
The code below add the missing edges:
*)
let add_edge n1 n2 =
if n1 = n2 then failwith
(Printf.sprintf "Bad topology: %s can not ne a neighbor of itself!" n1);
let pn1 = try Hashtbl.find node_succ n1 with Not_found -> [] in
let pn2 = try Hashtbl.find node_succ n2 with Not_found -> [] in
Hashtbl.replace node_succ n1 (n2::pn1);
if not directed then Hashtbl.replace node_succ n2 (n1::pn2);
n2
in
ignore (List.fold_left add_edge node nodes);
n
| Attr_graph _attrs -> n
| Attr_node _attrs -> n
| Attr_edge _attrs -> n
| Equal (_id1, _id2) -> assert false
| Subgraph _subgraph -> assert false
let (read: string -> t) = fun f ->
let dot_file = Graph.Dot.parse_dot_ast f in
assert (not dot_file.strict);
let res = List.fold_left (do_stmt dot_file.digraph) [] dot_file.stmts in
List.rev res,f
;;
let succ str = try Hashtbl.find node_succ str with Not_found -> []
(* XXX bad name: process? *)
type pid = {
open Topology
type process = {
name: string;
actions: (string * bool * bool) list; (* (action name, enabled, active) *)
vars: (string * Data.v) list (* pid local vars*)
......@@ -138,8 +23,8 @@ let (is_parent: string -> int -> Event.t -> bool) =
| Some (I j) -> i = j
| _ -> false
let (get_pidl : node list -> string -> Event.t -> pid list) =
fun nodes f e ->
let (get_processes : string -> Event.t -> process list) =
fun f e ->
if e.kind <> Ltop then (
print_string "print_dot should be called from Ltop event\n";
failwith "exit print_dot"
......@@ -152,8 +37,8 @@ let (get_pidl : node list -> string -> Event.t -> pid list) =
| _ -> assert false
in
let enab, other = List.fold_left sortv ([],[]) l in
let rec (build_pidl: pid list -> (string * string * Data.v) list ->
(string * string * Data.v) list -> pid list) =
let rec (build_pidl: process list -> (string * string * Data.v) list ->
(string * string * Data.v) list -> process list) =
fun pidl enab other ->
match enab with
| [] -> pidl
......@@ -182,8 +67,9 @@ let (get_pidl : node list -> string -> Event.t -> pid list) =
(* Compute a dot from the content of e.data *)
let print_dot (nodes,f) e =
let (pidl : pid list) = get_pidl nodes f e in
let print_dot g f e =
let nodes = g.nodes in
let (pidl : process list) = get_processes f e in
let oc = open_out ("sasa-"^f) in
let nodes_decl =
String.concat "\n"
......@@ -219,7 +105,7 @@ let print_dot (nodes,f) e =
List.flatten
(List.map
(fun n ->
let l = succ n.id in
let l = g.succ n.id in
List.mapi (fun i t ->
if is_parent n.id i e then
Printf.sprintf "%s -> %s" n.id t
......@@ -271,7 +157,7 @@ let get_removable pl =
List.map (fun p -> p.name) pl
let next_round nodes f e =
let (pl : pid list) = get_pidl nodes f e in
let (pl : process list) = get_processes f e in
let p_with_enable_action =
List.filter
(fun p -> List.exists (fun (_,enab,acti) -> enab&&not(acti)) p.actions)
......@@ -282,7 +168,7 @@ let next_round nodes f e =
flush stdout;
let rec go cpidl e =
let e = step e in
let pl = get_pidl nodes f e in
let pl = get_processes f e in
let removable = get_removable pl in
Printf.printf "Current process: %s\n" (String.concat "," cpidl);
Printf.printf "Removable process: %s\n" (String.concat "," removable);
......@@ -302,11 +188,15 @@ You migth want to add something along those lines at the end of your rdbg-sessio
(the name of the dot file and the path to the dot.ml file migth need to be adapted
to your context tough):
;;
#require \"ocamlgraph\";;
#mod_use \"../../lib/algo/algo.ml\";;
#use \"../../lib/sasacore/topology.ml\";;
#use \"../rdbg-utils/dot.ml\";;
let nodes,dotfile = read \"g.dot\";;
let d () = print_dot (nodes, dotfile) !e;;
let dotfile = \"g.dot\";;
let p = Topology.read dotfile;;
let d () = print_dot (p.nodes, dotfile) !e;;
let sd () = s();d();;
let nr () = e:=next_round nodes dotfile !e; d();;
let nr () = e:=next_round p.nodes dotfile !e; d();;
let _ = n (); d (); Sys.command (\"zathura sasa-g.dot.pdf&\")
......
Supports Markdown
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment