diff --git a/generate/test.v b/generate/test.v
index f35336e9f8449f8948a6fc74ca5201fed36bfe27..c82b1e1220034e389731a1203cd4773f95e147b5 100644
--- a/generate/test.v
+++ b/generate/test.v
@@ -1,107 +1,122 @@
Require Import Pactole.Setting Pactole.Util.FSets.FSetInterface.
Require Import Pactole.Observations.LimitedSetObservation.
Require Import Pactole.Models.Rigid Pactole.Models.Similarity.
-Require Import Pactole.Spaces.R2 Rbase.
+Require Import Pactole.Spaces.Ring Reals Pactole.Spaces.Isomorphism.
Section test.
Variable n: nat.
Instance MyRobots: Names := Robots (7 * n) n.
- Instance Loc: Location := make_Location R2.
- Instance VS: RealVectorSpace location := R2_VS.
- Instance ES: EuclideanSpace location := R2_ES.
+ Instance MyRing: RingSpec :=
+ {| ring_size := 5;
+ ring_size_spec:= ltac:(auto) |}.
+ Notation ring_node := (finite_node ring_size).
+ Instance Loc: Location := make_Location ring_node.
- Instance St: State location := OnlyLocation (fun _ => True).
+ Inductive light:= Toto | Rouge.
+ Definition info := (location * light)%type.
+ Instance St : State info := AddInfo light (OnlyLocation (fun f => sigT (fun sim : similarity location => Bijection.section sim == f))).
Variable r: R.
Instance Obs: Observation := limited_set_observation VS r.
Instance RC: robot_choice location :=
{ robot_choice_Setoid := location_Setoid}.
Instance UC: update_choice unit := NoChoice.
- Instance UpdFun:
- update_function (location) (Similarity.similarity location) unit :=
- {update := fun _ _ _ target _ => target;update_compat := ltac:(now repeat intro) }.
- Instance Rigid : RigidSetting.
- Proof using . split. reflexivity. Qed.
+ Instance FC: frame_choice (Z * bool) :=
+ {frame_choice_bijection :=
+ fun nb => if snd nb then Ring.sym (fst nb) else Ring.trans (fst nb);
+ frame_choice_Setoid := eq_setoid _ }.
+ Instance UpdFun: update_function direction (Z * bool) unit :=
+ {
+ update := fun config g _ dir _ => move_along (config (Good g)) dir;
+ update_compat := ltac:(repeat intro; subst; now apply move_along_compat) }.
Instance IC : inactive_choice unit := NoChoiceIna.
Instance InaFun : inactive_function unit := NoChoiceInaFun.
- Definition Robogram_pgm (s : observation): location :=
+ Definition robogram_pgm (s : observation): location :=
let c := (elements s)
in match c with
| nil => (0,0)
| cons pt nil => pt
| cons _ (cons _ _) => isobarycenter c
end.
- Instance Robogram_pgm_compat : Proper (equiv ==> equiv) Robogram_pgm.
+ Instance robogram_pgm_compat : Proper (equiv ==> equiv) robogram_pgm.
(* Proof *)
Admitted.
- Definition Robogram: robogram :=
- {| pgm := Robogram_pgm; pgm_compat := Robogram_pgm_compat |}.
+ Definition robogram: robogram :=
+ {| pgm := robogram_pgm; pgm_compat := robogram_pgm_compat |}.
- Function measure (s : observation) : nat*nat :=
- (0%nat,0%nat).
- Instance measure_compat : Proper (equiv ==> Logic.eq) measure.
- (* Proof *)
- Admitted.
- Variable da: demonic_action.
+ (* Definition of phase *)
+ Definition F (config : configuration):= (* To_Complete *).
+ Definition C (config : configuration):= (* To_Complete *).
+ Definition E (config : configuration):= (* To_Complete *).
+ Definition D (config : configuration):= (* To_Complete *).
+ Definition B (config : configuration):= (* To_Complete *).
+ Definition A (config : configuration):= (* To_Complete *).
+ (* Definition of measure per phase *)
+ Definition F_meas (config : configuration): nat := (* To_Complete *).
+ Definition C_meas (config : configuration): nat := (* To_Complete *).
+ Definition E_meas (config : configuration): nat := (* To_Complete *).
+ Definition D_meas (config : configuration): nat := (* To_Complete *).
+ Definition B_meas (config : configuration): nat := (* To_Complete *).
+ Definition A_meas (config : configuration): nat := (* To_Complete *).
Lemma InGraph: forall config,
- (Ed config ) \/ (Dd config ) \/ (Maj config ) \/ (Gc config ) \/ (Ec config ) \/ (Gd config ) \/ (Sc config ) \/ (Id config ) \/ (Ic config ) \/ (Sd config ) \/ (Dc config ).
- Proof.
-
- Qed.
- Lemma lem_Dc_next_Maj_or_Gathered: forall config ,
- Dc config -> (Maj (round Robogram da config) \/ Gathered (round Robogram da config)).
+ (C config) \/
+ (E config) \/ (D config) \/ (B config) \/ (A config).
Proof.
-
+ (* TODO *)
Qed.
- Lemma lem_Sd_next_Sc_or_Maj: forall config ,
- Sd config -> (Sc (round Robogram da config) \/ Maj (round Robogram da config)).
+ Lemma A_next_B da: forall config,
+ A config = true -> B (round robogram da config) = true.
Proof.
-
+ (* TODO *)
Qed.
- Lemma lem_Ic_next_Maj_or_Gathered: forall config ,
- Ic config -> (Maj (round Robogram da config) \/ Gathered (round Robogram da config)).
+ Lemma B_next_F_or_D_or_C da: forall config,
+ B config = true ->
+ (F (round robogram da config) = true \/
+ D (round robogram da config) = true \/
+ C (round robogram da config) = true).
Proof.
-
+ (* TODO *)
Qed.
- Lemma lem_Id_next_Maj_or_Ic: forall config ,
- Id config -> (Maj (round Robogram da config) \/ Ic (round Robogram da config)).
+ Lemma D_next_E da: forall config,
+ D config = true -> E (round robogram da config) = true.
Proof.
-
+ (* TODO *)
Qed.
- Lemma lem_Sc_next_Maj_or_Gathered: forall config ,
- Sc config -> (Maj (round Robogram da config) \/ Gathered (round Robogram da config)).
+ Lemma E_next_F_or_C da: forall config,
+ E config = true ->
+ (F (round robogram da config) = true \/
+ C (round robogram da config) = true).
Proof.
-
+ (* TODO *)
Qed.
- Lemma lem_Gd_next_Maj_or_Gc: forall config ,
- Gd config -> (Maj (round Robogram da config) \/ Gc (round Robogram da config)).
+ Lemma C_next_F_or_E da: forall config,
+ C config = true ->
+ (F (round robogram da config) = true \/
+ E (round robogram da config) = true).
Proof.
-
+ (* TODO *)
Qed.
- Lemma lem_Ec_next_Maj_or_Gathered_or_Dd: forall config ,
- Ec config -> (Maj (round Robogram da config) \/ Gathered (round Robogram da config) \/ Dd (round Robogram da config)).
- Proof.
-
- Qed.
- Lemma lem_Gc_next_Sd_or_Maj_or_Id_or_Ic_or_Ec_or_Dd_or_Dc: forall config ,
- Gc config -> (Sd (round Robogram da config) \/ Maj (round Robogram da config) \/ Id (round Robogram da config) \/ Ic (round Robogram da config) \/ Ec (round Robogram da config) \/ Dd (round Robogram da config) \/ Dc (round Robogram da config)).
- Proof.
-
- Qed.
- Lemma lem_Maj_next_Gathered: forall config ,
- Maj config -> (Gathered (round Robogram da config)).
- Proof.
-
- Qed.
- Lemma lem_Dd_next_Maj_or_Dc: forall config ,
- Dd config -> (Maj (round Robogram da config) \/ Dc (round Robogram da config)).
- Proof.
-
- Qed.
- Lemma lem_Ed_next_Maj_or_Ec: forall config ,
- Ed config -> (Maj (round Robogram da config) \/ Ec (round Robogram da config)).
+ Definition measure (config : configuration): nat*nat :=
+ if A config then (5, A_meas config)
+ else if B config then (4, B_meas config)
+ else if D config then (3, D_meas config)
+ else if E config then (2, E_meas config)
+ else if C config then (1, C_meas config)
+ else (0, F_meas config).
+ Instance measure_compat : Proper (equiv ==> Logic.eq) measure.
+ (* Proof *)
+ Admitted.
+
+ Definition lt_config x y := Lexprod.lexprod lt lt (measure (!! x)) (measure (!! y)).
+ Lemma wf_lt_config: well_founded lt_config.
Proof.
-
+ (* TODO *)
Qed.
+ Instance lt_config_compat : Proper (equiv ==> equiv ==> iff) lt_config.
+ (* Proof *)
+ Admitted.
+ Theorem round_lt_config : forall config,
+ moving robogram da config <> nil ->
+ lt_config (round robogram da config) config.
End test.
diff --git a/lib/ast.ml b/lib/ast.ml
index 913a9be2983a4da9492bcbf10277c9904190c059..c78bb1a65e21e470ad1ac723d1ab4a091b43b0e3 100644
--- a/lib/ast.ml
+++ b/lib/ast.ml
@@ -64,10 +64,10 @@ type synchro =
*)
type space =
| R
- | Rm
+ | MR of int option
| R2
- | R2m
- | ZnZ of int
+ | MR2 of int option
+ | ZnZ of int option
(* type range:
Full -> Full range
@@ -109,9 +109,9 @@ type color =
Extern -> Light seen by robots other than himself
All -> Light seen by all robots including themselves *)
type light =
- | Intern of color list
- | Extern of color list
- | All of color list
+ | Intern of string list
+ | Extern of string list
+ | All of string list
(* type opacity:
@@ -234,9 +234,9 @@ let rec string_of_expression (e : expr) : string =
let string_of_espace (e:space) : string =
match e with
| R -> "R"
- | Rm -> "Rm"
+ | MR _ -> "mR"
| R2 -> "R2"
- | R2m ->"R2m"
+ | MR2 _ ->"mR2"
| ZnZ _ -> "Ring"
let string_of_color (c : color) : string =
@@ -278,10 +278,15 @@ let info_robot (i : information):bool =
| Robot _ -> true
| _ -> false
+let compar_expr (e1 : expr) (e2: expr) :int =
+ match e1,e2 with
+ | Var x1,Var x2 -> String.compare x1 x2
+ | _ -> -1
+
(*GRAPH*)
module Node = struct
type t = expr
- let compare = compare
+ let compare = compar_expr
let hash = Hashtbl.hash
let equal = (=)
end
@@ -296,6 +301,7 @@ end
module G = Graph.Imperative.Digraph.ConcreteLabeled(Node)(Edge)
module Topological = Graph.Topological.Make(G)
module D = Graph.Traverse.Dfs(G)
+module T = Graph.Components.Make(G)
type edge =
| Nolab of (expr * expr)
@@ -317,8 +323,7 @@ let graph_from_edges (el : edge list)=
| [] -> ()
| (Nolab h)::t -> nolab h ; add_edge t
in add_edge el;
- if not(D.has_cycle g) then g else raise(Failure("Graph is cyclic"))
-
+ g
(**[png_from_graph g name] generates a png file of the graph [g]
@param g [G.t]
@@ -329,7 +334,6 @@ let png_from_graph g name=
let succs = List.map string_of_expression (G.succ g v)in
let v' = string_of_expression v in
let edges = List.fold_left (fun acc s ->
-
acc ^ "\"" ^ v' ^ "\" -> \"" ^ s ^ "\";\n") "" succs in
acc ^ "\"" ^ v' ^ "\";\n" ^ edges
) g "" in
@@ -353,7 +357,137 @@ let assign_height (g : G.t) : (expr * int) list =
let nodes = Topological.fold (fun node acc -> node :: acc) g [] in
assign_order nodes 0 []
-(*/GRAPH*)
+
+
+
+module NodeMap = Map.Make(Node)
+
+(** [update_lowlink v w lowlink] met à jour la valeur de lowlink pour le noeud [v] en fonction du noeud [w]. *)
+let update_lowlink v w lowlink =
+ let v_lowlink = NodeMap.find v lowlink in
+ let w_lowlink = NodeMap.find w lowlink in
+ NodeMap.add v (min v_lowlink w_lowlink) lowlink
+
+(** [update_on_stack w on_stack] supprime le noeud [w] de la liste [on_stack]. *)
+ let update_on_stack w on_stack =
+ List.filter (fun v -> v <> w) on_stack
+
+
+(** [pop_stack v stack on_stack scc] retire les éléments de la pile jusqu'à atteindre le noeud [v].
+ Cela met à jour [on_stack] en supprimant les noeuds retirés de la pile, et [scc] en ajoutant ces noeuds à la nouvelle composante fortement connexe.*)
+ let rec pop_stack v stack on_stack scc =
+ match stack with
+ | w :: rest -> if w <> v then pop_stack v rest (update_on_stack w on_stack) (w :: scc)
+ else rest, (update_on_stack w on_stack), (w :: scc)
+ | [] -> raise(Failure "Error: stack empty")
+
+
+(** [strongconnect v index stack indices lowlink on_stack sccs g] est la fonction qui effectue le parcours en profondeur pour trouver les composantes fortement connexes.
+ Pour chaque successeur [w] de [v] dans le graphe [g], si [w] n'est pas encore visité, il est récursivement visité.
+ Après avoir visité tous les successeurs, si [v] est une racine de SCC, tous les noeuds dans la pile jusqu'à [v] sont ajoutés à une nouvelle SCC.
+ *)
+let rec strongconnect (g : G.t) (v:expr) (index:int) stack indices lowlink on_stack sccs =
+ let indices = NodeMap.add v index indices in
+ let lowlink = NodeMap.add v index lowlink in
+ let stack = v :: stack in
+ let on_stack = v :: on_stack in
+ let index = index + 1 in
+
+ let index, stack, indices, lowlink, on_stack, sccs =
+ G.fold_succ ( fun w (index, stack, indices, lowlink, on_stack, sccs) ->
+ let v_lowlink = NodeMap.find v lowlink in
+ if not (NodeMap.mem w indices) then (
+ let index, stack, indices, lowlink, on_stack, sccs = strongconnect g w index stack indices lowlink on_stack sccs in
+ let w_lowlink = NodeMap.find w lowlink in
+ let lowlink = NodeMap.add v (min v_lowlink w_lowlink) lowlink in
+ (index, stack, indices, lowlink, on_stack, sccs)
+ ) else if List.mem w on_stack then (
+ let w_index = NodeMap.find w indices in
+ let lowlink = NodeMap.add v (min v_lowlink w_index) lowlink in
+ index, stack, indices, lowlink, on_stack, sccs
+ ) else (
+ index, stack, indices, lowlink, on_stack, sccs
+ )
+ ) g v (index,stack,indices,lowlink,on_stack,sccs) in
+
+ if NodeMap.find v lowlink = NodeMap.find v indices then
+ let stack, on_stack, scc = pop_stack v stack on_stack [] in
+ let sccs = scc :: sccs in
+ index, stack, indices, lowlink, on_stack, sccs
+ else
+ index, stack, indices, lowlink, on_stack, sccs
+
+(** [tarjan g] est la fonction principale qui initialise les structures de données et lance le parcours en profondeur.
+ et renvoie la liste des composants fortements connexes*)
+let tarjan g =
+ (*Tarjan : *)
+ let _, _, _, _, _, sccs =
+ G.fold_vertex (fun v (index,stack,indices,lowlink,on_stack,sccs) ->
+ if not (NodeMap.mem v indices) then
+ strongconnect g v index stack indices lowlink on_stack sccs
+ else
+ (index, stack, indices, lowlink, on_stack, sccs)
+ ) g (0,[],NodeMap.empty,NodeMap.empty,[],[])
+ in
+ sccs
+
+
+ module SCC = struct
+ type t = expr list
+ let compare = Stdlib.compare
+ let hash = Hashtbl.hash
+ let equal = (=)
+ end
+
+ module G2 = Graph.Imperative.Digraph.ConcreteLabeled(SCC)(Edge)
+
+ (**[string_of_expr_list expr_list] retourne une chaine de caractere à partir d'une liste d'expression tel que [[X;Y]] correspondant à : string_of_expression X, string_of_expression Y, .... *)
+let string_of_expr_list expr_list =
+ let string_list = List.map string_of_expression expr_list in
+ String.concat ", " string_list
+
+(**[png_from_graph2 g ] renvoie l'image au format png du graphe [g]
+ @param g de type [G2.t] graphe de liste de liste d'expression, composants fortement connexe *)
+let png_from_graph2 (g:G2.t) (name : string) :unit =
+ let graph = G2.fold_vertex (fun v acc ->
+ let succs = List.map string_of_expr_list (G2.succ g v)in
+ let v' = string_of_expr_list v in
+ let edges = List.fold_left (fun acc s ->
+ acc ^ "\"" ^ v' ^ "\" -> \"" ^ s ^ "\";\n") "" succs in
+ acc ^ "\"" ^ v' ^ "\";\n" ^ edges
+ ) g "" in
+ let dot = "digraph G {\nrankdir=LR;\nranksep=1;\n" ^ graph ^"\nsplines=true;\noverlap=false; "^"}" in
+ let oc = open_out ("./generate/"^name^"_measure.dot") in
+ Printf.fprintf oc "%s\n" dot;
+ close_out oc;
+ ignore (Sys.command ("dot -Tpng ./generate/"^name^"_measure.dot -o ./generate/"^ name^"_measure.png"))
+
+
+(** [scc_graph g] retourne le graphe G2.t correspondant au graphe de composants fortement connexe du graphe [g]
+ en recupérant la liste des composants fortement connexe et en les ajoutant au graphe G2.t créé[scc_graph].
+ Ensuite, la fonction itère sur chaque SCC et ajoute des arêtes entre les SCC en se basant sur le graphe original [g].
+ Pour chaque sommet dans un SCC, elle itère sur ses successeurs et trouve le SCC auquel chaque successeur appartient.
+ Si le SCC du sommet et le SCC du successeur sont différents, une arête est ajoutée entre les SCC correspondants dans [scc_graph].
+
+ @param g [G.t]
+ @return [scc_graph] de type [G2.t], le graphe des composants fortement connexe de [g] *)
+let scc_graph g =
+ let scc_list = tarjan g in
+ let scc_graph = G2.create () in
+ List.iter (fun scc -> G2.add_vertex scc_graph scc) scc_list;
+ let add_edges scc =
+ List.iter (fun v ->
+ G.iter_succ (fun succ ->
+ let succ_scc = List.find (List.exists (fun v' -> v' = succ)) scc_list in
+ if scc <> succ_scc then
+ G2.add_edge scc_graph scc succ_scc;
+ ) g v;
+ ) scc ;
+ in
+ List.iter add_edges scc_list;
+ scc_graph;;
+
+
type measure = Measure of G.t
diff --git a/lib/gencoq.ml b/lib/gencoq.ml
index 15602dafbae5e9d367b19404b60dfbc41a3524b0..af8f74deb6c8025fb9aa1eccb637967452047d78 100644
--- a/lib/gencoq.ml
+++ b/lib/gencoq.ml
@@ -118,7 +118,7 @@ let rec expr_to_coq (r : expr) : Formula.t =
match s with
| Vide -> []
| Some (s',e) -> string_of_expression e :: set_to_coq s'
-
+
(**[instance_R_R2 s d] generates the coq code to instance R and R2
@param space s
@@ -142,11 +142,11 @@ let instance_R_R2 (s:space) (d: information list): stmt list =
(**[instance_Ring n] generates the coq code to instantiate a Ring
@param int n
@return [stmt list]*)
-let instance_ring (n:int) : stmt list =
- let ring = if n > 0 then
- Instance("MyRing",Raw("RingSpec"),Record([Raw("ring_size := "^string_of_int n);Raw("ring_size_spec:= ltac:(auto)")]))
- else
- RawCoq(["Context {RR : RingSpec}."])
+let instance_ring (n:int option) : stmt list =
+ let ring =
+ match n with
+ | Some(n') -> Instance("MyRing",Raw("RingSpec"),Record([Raw("ring_size := "^string_of_int n');Raw("ring_size_spec:= ltac:(auto)")]))
+ | None -> RawCoq(["Context {RR : RingSpec}."])
in
ring::Notation("ring_node",App(Cst "finite_node",[Cst "ring_size"] ))::Instance("Loc",Cst "Location",App(Cst "make_Location",[Cst "ring_node"]))::[]
@@ -210,7 +210,7 @@ let instance_info (fl:field list) : stmt list =
in
(match l with
|Some(Light (x)) -> let l' = match x with | Intern p -> p |Extern p -> p | All p -> p in
- let l'' = String.concat " | " (List.map string_of_color l') in
+ let l'' = String.concat " | " l' in
RawCoq(["Inductive light:= "^l''^"."])
::RawCoq(["Definition info := (location * light)%type."])
::RawCoq(["Instance St : State info := AddInfo light (OnlyLocation (fun f => sigT (fun sim : similarity location => Bijection.section sim == f)))."])::[]
@@ -331,13 +331,15 @@ let generate_robogram (r : expr list) (d: information list) : stmt list =
match (List.map expr_to_coq r) with
| h::_ -> let h' = if get_rigidity d = "Flexible" then Formula.Let("aux s",h,Raw("paths_in_"^get_space d^" (aux s)"))
else h in
- Def ("Robogram_pgm (s : observation)",Raw(valretcoq),h')
- ::RawCoq(["Instance Robogram_pgm_compat : Proper (equiv ==> equiv) Robogram_pgm."])
+ Def ("robogram_pgm (s : observation)",Raw(valretcoq),h')
+ ::RawCoq(["Instance robogram_pgm_compat : Proper (equiv ==> equiv) robogram_pgm."])
::proof_to_complete
- @Def("Robogram",Raw("robogram"),Raw("{| pgm := Robogram_pgm; pgm_compat := Robogram_pgm_compat |}"))
+ @Def("robogram",Raw("robogram"),Raw("{| pgm := robogram_pgm; pgm_compat := robogram_pgm_compat |}"))
::[]
- | [] -> Def ("Robogram_pgm (s : observation)",Raw(valretcoq),Raw("[]")) ::[]
+ | [] -> Def ("robogram_pgm (s : observation)",Raw(valretcoq),Raw("[]")) ::[]
+
+ module Topological = Graph.Topological.Make(Ast.G)
(**[generate_or l] returns the formula "or" from a list of string
@param string list
@@ -348,9 +350,9 @@ match l with
| h::tl -> Or(Cst(h),generate_or tl)
| _ -> Cst("")
-(**[generate_definition_phase g] *)
-let generate_defintion_phase (g : G.t) : stmt list =
- Ast.G.fold_vertex (fun v acc ->
+(**[generate_definition_phase g]returns the list of stmt to generate the coq code for the definition of the phases of the graph [g]*)
+let generate_definition_phase (g : G.t) : stmt list =
+ Topological.fold (fun v acc ->
let func_name = string_of_expression v ^" (config : configuration)" in
RawCoq(["Definition "^func_name^":= (* To_Complete *)."])::acc
) g []
@@ -359,23 +361,24 @@ let generate_defintion_phase (g : G.t) : stmt list =
@param g [G.t]
@return [stmt list]*)
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
+ Topological.fold (fun v acc ->
+ let func_name = string_of_expression v ^"_meas (config : configuration)" in
Def(func_name,Raw("nat"),Raw("(* To_Complete *)"))::acc
) g []
+
(**[generate_lemmas g] returns the list of stmt corresponding to the lemmas extracted from the graph g
@param g [G.t]
@return [stmt list]*)
let generate_lemmas (g : Ast.G.t) : (stmt list * string list) =
- Ast.G.fold_vertex (fun v (acc,s) ->
+ Topological.fold (fun v (acc,s) ->
let string_v = string_of_expression v in
let succs = Ast.G.succ g v in
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
+ let rcs = List.map (fun x -> x ^ " (round robogram da config) = true") string_succs in
(Lemma(string_v^"_next_"^String.concat "_or_" string_succs ^" da",
- Forall("config",InfixOp(Raw(string_v^" config"),"->",(generate_or rcs) )),[Comment("TODO")])::acc,
+ Forall("config",InfixOp(Raw(string_v^" config = true"),"->",(generate_or rcs) )),[Comment("TODO")])::acc,
("("^string_v ^" config)")::s)
else
(acc,s)
@@ -387,8 +390,8 @@ let generate_lemmas (g : Ast.G.t) : (stmt list * string list) =
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 )
+ |(phase,height)::[] -> Formula.Cst("("^ string_of_int height^", "^string_of_expression phase ^"_meas config)")
+ |(phase,height)::tl -> If(Cst(string_of_expression phase ^" config"),Cst("("^ string_of_int height^", "^string_of_expression phase ^"_meas config)"),aux tl )
| _ -> Cst("")
in
aux (Ast.assign_height g)
@@ -401,9 +404,10 @@ let generate_measure (Measure(g): measure) (name_png : string) : stmt list =
let ret = "nat*nat" in
let to_change = generate_if_measure g in
Ast.png_from_graph g name_png;
+ Ast.png_from_graph2 (Ast.scc_graph g;) "scc_graph";
let measure_per_phase = generate_measure_per_phase g in
let lemsgen = let lems = generate_lemmas g in
- Comment("Definition of phase")::generate_defintion_phase g
+ Comment("Definition of phase")::generate_definition_phase g
@Comment("Definition of measure per phase ")::measure_per_phase
@Lemma("InGraph",Forall("config",generate_or (snd lems)),[Comment("TODO")])
::List.rev (fst lems) in
@@ -411,6 +415,14 @@ let generate_measure (Measure(g): measure) (name_png : string) : stmt list =
Def("measure (config : configuration)",Cst(ret),to_change)::
RawCoq(["Instance measure_compat : Proper (equiv ==> Logic.eq) measure."])::proof_to_complete
+let generate_lt =
+ RawCoq(["Definition lt_config x y := Lexprod.lexprod lt lt (measure (!! x)) (measure (!! y))."])
+ :: Lemma("wf_lt_config",Cst("well_founded lt_config"),[Comment("TODO")])
+ :: RawCoq(["Instance lt_config_compat : Proper (equiv ==> equiv ==> iff) lt_config."])
+ ::proof_to_complete
+ @ RawCoq(["Theorem round_lt_config : forall config,
+ moving robogram da config <> nil ->
+ lt_config (round robogram da config) config."]) ::[]
(**[generate_coq d s] generated from the complete description (world, robogram, measure) [d] the named coq instance [s]
@param description of
@@ -421,7 +433,9 @@ let generate_coq (Description(d,r,m) : description) (section_name : string)=
then
let file_out = open_out ("./generate/"^section_name^".v") in
let format_file = Format.formatter_of_out_channel file_out in
- let section = Section(section_name,(generate_instances d)@newline::generate_robogram r d@newline::generate_measure m section_name) in
+ let section = Section(section_name,(generate_instances d)@newline::generate_robogram r d
+ @newline::generate_measure m section_name
+ @newline::generate_lt) in
Format.fprintf format_file "%a@." Coq.pretty_l ((generate_requires d)@[section]);
close_out file_out;
print_endline(section_name^".v is generated")
diff --git a/lib/lexer.mll b/lib/lexer.mll
index 620667eb36d3a1e81f439f827dd9abf0445fd12f..dad71b358ccc297ccc7e8622a33ec24e093268a6 100644
--- a/lib/lexer.mll
+++ b/lib/lexer.mll
@@ -21,9 +21,9 @@ rule token = parse
| "ASYNC" {ASYNC}
| "Space" {SPACE}
| "R" {R}
- | "Rm" {RM}
+ | "mR" {MR}
| "R2" {R2}
- | "R2m" {R2M}
+ | "mR2" {MR2}
| "Ring" {RING}
| "Byzantine" {BYZANTINE}
| "Sensors" {SENSORS}
@@ -46,12 +46,12 @@ rule token = parse
| "Light" {LIGHT}
| "Internal" {INTERNE}
| "External" {EXTERNE}
- | "Red" {RED}
+ (*| "Red" {RED}
| "Blue" {BLUE}
| "Yellow" {YELLOW}
| "Green" {GREEN}
| "Orange" {ORANGE}
- | "Purple" {PURPLE}
+ | "Purple" {PURPLE}*)
| "Opacity" {OPACITY}
| "Opaque" {OPAQUE}
| "Transparent" {TRANSPARENT}
diff --git a/lib/parser.mly b/lib/parser.mly
index 6976383770c9efa8b366aed40c8fa89aafa1006d..fc3655f8035bcbaeb9df3f9c5f90a9d4f55a6e59 100644
--- a/lib/parser.mly
+++ b/lib/parser.mly
@@ -7,12 +7,12 @@
%token <float> FLOAT
%token IS
%token SYNC FSYNC SSYNC ASYNC
-%token SPACE R RM R2 R2M RING
+%token SPACE R MR R2 MR2 RING
%token BYZANTINE
%token SENSORS
%token RANGE FULL LIMITED K_RAND K_ENEMY
%token MULTI NO_MEM WEAKL STRONGL WEAKG STRONGG
-%token LIGHT INTERNE EXTERNE RED BLUE YELLOW GREEN PURPLE ORANGE
+%token LIGHT INTERNE EXTERNE
%token OPACITY OPAQUE TRANSPARENT
%token SHARE FULLCOMPASS CHIRALITY ONEAXEORIEN
%token RIGIDITY RIGIDE FLEXIBLE
@@ -123,14 +123,16 @@ ints :
/* Space R */
| R {R}
/* Space R millefeuille*/
- | RM {Rm}
+ | MR n = INT {MR(Some n)}
+ | MR {MR(None)}
/* Space RxR */
| R2 {R2}
/* Space RxR millefeuille*/
- | R2M {R2m}
+ | MR2 n = INT {MR2(Some n)}
+ | MR2 {MR2(None)}
/*Ring Z/nZ */
- | RING n = INT {ZnZ(n)}
- | RING {ZnZ(0)}
+ | RING n = INT {ZnZ(Some n)}
+ | RING {ZnZ(None)}
%inline sensor :
/*Multi : m*/
@@ -164,19 +166,12 @@ value :
lights:
/*Internal light -> visible only to the robot*/
- | INTERNE LIGHT BRACKETOPEN i = separated_list(SEMICOLON,color) BRACKETCLOSE {Light(Intern i)}
+ | INTERNE LIGHT BRACKETOPEN i = separated_list(SEMICOLON,KEYWORD) BRACKETCLOSE {Light(Intern i)}
/*External light -> visible only to other robots*/
- | EXTERNE LIGHT BRACKETOPEN i = separated_list(SEMICOLON,color) BRACKETCLOSE {Light(Extern i)}
+ | EXTERNE LIGHT BRACKETOPEN i = separated_list(SEMICOLON,KEYWORD) BRACKETCLOSE {Light(Extern i)}
/*Light visible to all*/
- | FULL LIGHT BRACKETOPEN i = separated_list(SEMICOLON,color) BRACKETCLOSE {Light(All i)}
-
-%inline color :
- | RED {Red}
- | BLUE {Blue}
- | YELLOW {Yellow}
- | GREEN {Green}
- | PURPLE {Purple}
- | ORANGE {Orange}
+ | FULL LIGHT BRACKETOPEN i = separated_list(SEMICOLON,KEYWORD) BRACKETCLOSE {Light(All i)}
+
%inline range :
/* Full Range */