diff --git a/lib/ast.ml b/lib/ast.ml
index 8cf72829ec1d2647dca907f1375e0974d0724f57..ded326a480848accb8dd281cc6f00ae5b6e25550 100644
--- a/lib/ast.ml
+++ b/lib/ast.ml
@@ -398,6 +398,7 @@ end
module G = Graph.Imperative.Digraph.ConcreteLabeled(Node)(Edge)
+module Topological = Graph.Topological.Make(G)
type edge =
@@ -427,13 +428,25 @@ let graph_from_edges (el : edge list)=
acc ^ "\"" ^ v' ^ "\" -> \"" ^ s ^ "\";\n") "" succs in
acc ^ "\"" ^ v' ^ "\";\n" ^ edges
) g "" in
- let dot = "digraph G {\nrankdir=LR;\n" ^ graph ^ "}" in
+ let dot = "digraph G {\nrankdir=LR;\nranksep=1;\n" ^ graph ^"\nsplines=true;\noverlap=false; "^"}" in
let oc = open_out "graph.dot" in
Printf.fprintf oc "%s\n" dot;
close_out oc;
ignore (Sys.command "dot -Tpng graph.dot -o graph.png")
-
+ (**[assign_heigth g ] retourne la liste d'association phase,poids de phase. Le poids de phase est déduit de l'ordre
+ topologique de la phase
+ @param G.t le graphe dans le quel il faut attribuer les poids aux sommets
+ @return (expr * int) list *)
+ let assign_height (g : G.t) : (expr * int) list =
+ (*let total_nodes = G.nb_vertex g in*)
+ let rec assign_order nodes counter order =
+ match nodes with
+ | [] -> order
+ | h :: tl -> assign_order tl (counter +1) ((h, counter) :: order)
+ in
+ let nodes = Topological.fold (fun node acc -> node :: acc) g [] in
+ assign_order nodes 0 []
(*/GRAPH*)
diff --git a/lib/gencoq.ml b/lib/gencoq.ml
index f991f9f97ac8b3e1ca9a471122bce6586f6c5f0d..b499cb94a446f146c53f68aba032918870f52ff5 100644
--- a/lib/gencoq.ml
+++ b/lib/gencoq.ml
@@ -4,17 +4,6 @@ open Coq
-let geometry =[("isobarycenter",Formula.Raw("isobarycenter"));
- ("barycenter",Formula.Raw("barycenter"));
- ("on_SEC"),Formula.Raw("on_SEC")]
-let observation =[("elements", Formula.Raw("(elements s)"));
- ("support"), Formula.Raw("support s")]
-let direction =[("forward",Formula.Raw("Forward"));
- ("backward",Formula.Raw("Backward"));
- ("selfloop",Formula.Raw("Selfloop"));]
-let correspondance = [("Geometry",geometry);
- ("Obs",observation);
- ("Directions",direction)]
let newline =RawCoq([" "])
let proof_to_complete = [Comment("Proof");RawCoq(["Admitted."])]
@@ -118,7 +107,7 @@ let rec expr_to_coq (r : expr) : Formula.t =
| Fun (s,e) -> Fun(Some s, expr_to_coq e)
| App (f,arg) -> App(expr_to_coq f, [expr_to_coq arg])
| Set s -> Raw("(" ^ String.concat "," (set_to_coq s) ^")")
- | Point (m,f) -> let c = List.assoc_opt m correspondance in
+ | Point (m,f) -> let c = List.assoc_opt m Module.correspondance in
(match c with
|None -> raise(Failure("Probleme "^m^" inconnu"))
|Some x -> (match List.assoc_opt f x with
@@ -360,6 +349,11 @@ match l with
| h::tl -> Or(Cst(h),generate_or tl)
| _ -> Cst("")
+let generate_measure_per_phase (g: Ast.G.t) : stmt list =
+ Ast.G.fold_vertex (fun v acc ->
+ let func_name = string_of_expression v ^"_lt (config : configuration)" in
+ Def(func_name,Raw("nat"),Raw("(* To_Complete *)"))::acc
+ ) g []
(**[generate_lemmas g] retourne la liste de stmt correspondant aux lemmes extrait du graph g
@param g [G.t]
@@ -371,13 +365,23 @@ let generate_lemmas (g : Ast.G.t) : (stmt list * string list) =
if succs <> [] then
let string_succs = (List.map string_of_expression succs) in
let rcs = List.map (fun x -> x ^ " (round Robogram da config)") (string_v::string_succs) in
- (Lemma("lem_"^string_v^"_next_"^String.concat "_or_" string_succs,
- Forall("config",InfixOp(Raw(string_v^" config"),"->",(generate_or rcs) )),[])::acc,
+ (Lemma(string_v^"_next_"^String.concat "_or_" string_succs ^" da",
+ Forall("config",InfixOp(Raw(string_v^" config"),"->",(generate_or rcs) )),[Comment("TODO")])::acc,
("("^string_v ^" config)")::s)
else
(acc,s)
) g ([],[])
+let generate_if_measure (g: Ast.G.t) : Formula.t =
+let rec aux l =
+ match l with
+ |(phase,height)::[] -> Formula.Cst("("^ string_of_int height^", "^string_of_expression phase ^"_lt)")
+ |(phase,height)::tl -> If(Cst(string_of_expression phase ^" config"),Cst("("^ string_of_int height^", "^string_of_expression phase ^"_lt)"),aux tl )
+ | _ -> Cst("")
+in
+ aux (Ast.assign_height g)
+
+ (* List.map (fun (phase,height) -> Comment(string_of_expression phase ^" poid = " ^ string_of_int height) ) height_phase *)
(**[generate_measure m] retourne la liste de stmt correspondant a la generation de la mesure
@@ -385,14 +389,16 @@ let generate_lemmas (g : Ast.G.t) : (stmt list * string list) =
@return [stmt list] *)
let generate_measure (Measure(i,g): measure) : stmt list =
let ret = String.concat "*"(List.init i (fun _ ->"nat")) in
- let to_change = String.concat ","(List.init i (fun _ ->"0%nat"))in
+ let to_change = generate_if_measure g in
Ast.png_from_graph g;
+ let measure_per_phase = generate_measure_per_phase g in
let lemsgen = let lems = generate_lemmas g in
- Lemma("InGraph",Forall("config",generate_or (snd lems)),[])
+ measure_per_phase
+ @Lemma("InGraph",Forall("config",generate_or (snd lems)),[Comment("TODO")])
::List.rev (fst lems) in
- RawCoq(["Function measure (s : observation) : "^ret ^" :=
- ("^to_change^")."; (*TODO: *)
- "Instance measure_compat : Proper (equiv ==> Logic.eq) measure."])::proof_to_complete@Var("da",Cst "demonic_action")::lemsgen
+ lemsgen@
+ Def("measure (config : configuration)",Cst(ret),to_change)::
+ RawCoq(["Instance measure_compat : Proper (equiv ==> Logic.eq) measure."])::proof_to_complete
(**[generate_coq d s] genere a partir de la description complete (world,robogram,measure) [d] l'instance coq nommé [s]
diff --git a/lib/module.ml b/lib/module.ml
new file mode 100644
index 0000000000000000000000000000000000000000..08a73e97774ee76339dd60c6a4e68c5aecb9f60f
--- /dev/null
+++ b/lib/module.ml
@@ -0,0 +1,13 @@
+
+
+let geometry =[("isobarycenter",Formula.Raw("isobarycenter"));
+ ("barycenter",Formula.Raw("barycenter"));
+ ("on_SEC"),Formula.Raw("on_SEC")]
+let observation =[("elements", Formula.Raw("(elements s)"));
+ ("support"), Formula.Raw("support s")]
+let direction =[("forward",Formula.Raw("Forward"));
+ ("backward",Formula.Raw("Backward"));
+ ("selfloop",Formula.Raw("Selfloop"));]
+let correspondance = [("Geometry",geometry);
+ ("Obs",observation);
+ ("Directions",direction)]
\ No newline at end of file
diff --git a/sourcegenerate/test b/sourcegenerate/test
index 5bf0f429835278ff435dfc50071a0b5e982fd860..985b59d9bfdda75eeb53e933558393db42f35779 100644
--- a/sourcegenerate/test
+++ b/sourcegenerate/test
@@ -2,34 +2,41 @@
World :
Sync := FSYNC
Space := R2
-Rigidity := Flexible delta
+Rigidity := Rigid
Byzantine := 8 /*Correspond à 1/8*/
Robot := Private :
Public :
-Sensors := Range : Limited r;
- Multiplicity : Weak Local;
+Sensors := Range : Limited r;
+ Multiplicity : No;
Opacity: Opaque
-ActivelyUpdate := Location ; Light
+ActivelyUpdate := Location
Share := Fullcompass
-Roles := 0 : Compagnon ; 2 : Leader
-
+
Robogram :
-let c = Obs.support in
+let c = Obs.elements in
match c with
| nil -> (0;0)
| pt :: nil -> pt
| _ :: _ :: _ -> Geometry.isobarycenter c
end
+Measure:(a,b)
-/*Measure : avec description graphe + nuple qui correspond a la measure*/
-Measure:(a)
-a -> b
-o -> a
-o -> b
-c -> o
-a -> c
\ No newline at end of file
+Gd -> Gc
+Gd -> Maj
+Gc -> [Id;Ic;Sd;Ec;Dd;Dc;Maj]
+Id -> [Ic;Maj]
+Sd -> [Sc;Maj]
+Ed -> [Ec;Maj]
+Ic -> [Maj;Gathered]
+Sc -> [Maj;Gathered]
+Ec -> [Maj;Gathered;Dd]
+Dd -> Dc
+Dd -> Maj
+Dc -> Gathered
+Dc -> Maj
+Maj -> Gathered