From e5269a7be093c770f86c26ab9646735d700195c0 Mon Sep 17 00:00:00 2001
From: Kylian Fontaine <kylian.fontaine@etu.univ-lyon1.fr>
Date: Wed, 3 Jul 2024 14:19:05 +0200
Subject: [PATCH] generation nom lemme + lemme conj phase + dsl accepte liste
de sommet pour graph
---
generate/test.v | 111 +++++++++++++++++++++++++++++++++++---------
lib/ast.ml | 5 +-
lib/gencoq.ml | 38 ++++++++-------
lib/graphmeasure.ml | 78 -------------------------------
lib/parser.mly | 8 +++-
5 files changed, 119 insertions(+), 121 deletions(-)
delete mode 100644 lib/graphmeasure.ml
diff --git a/generate/test.v b/generate/test.v
index e2a5475..f35336e 100644
--- a/generate/test.v
+++ b/generate/test.v
@@ -1,38 +1,107 @@
Require Import Pactole.Setting Pactole.Util.FSets.FSetInterface.
-Require Import Pactole.Observations.SetObservation.
-Require Import Pactole.Models.Flexible.
+Require Import Pactole.Observations.LimitedSetObservation.
+Require Import Pactole.Models.Rigid Pactole.Models.Similarity.
Require Import Pactole.Spaces.R2 Rbase.
Section test.
Variable n: nat.
- Instance MyRobots: Names := Robots (9 * n) n.
+ 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.
- Definition path_R2:= path location.
- Definition paths_in_R2: location -> path_R2 := local_straight_path.
- Coercion paths_in_R2 :location >-> path_R2.
Instance St: State location := OnlyLocation (fun _ => True).
- Instance Obs: Observation := set_observation.
+ Variable r: R.
+ Instance Obs: Observation := limited_set_observation VS r.
- Instance RobotChoice: robot_choice (path location) :=
- { robot_choice_Setoid := path_Setoid location}.
- Instance ActiveChoice: update_choice ratio := Flexible.OnlyFlexible.
- Variable delta: R.
- Instance UpdateFunc:
- update_function (path location) (Similarity.similarity location) ratio :=
- FlexibleUpdate delta.
- Instance InactiveChoice : inactive_choice unit := NoChoiceIna.
- Instance InactiveFunc : inactive_function unit := NoChoiceInaFun.
+ 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 IC : inactive_choice unit := NoChoiceIna.
+ Instance InaFun : inactive_function unit := NoChoiceInaFun.
- Definition Robogram_pgm (s : observation): (path location) :=
- let aux s := let c := (elements s)
- in isobarycenter c
- in paths_in_R2 (aux s).
+ 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.
- (* Preuve *)
+ (* Proof *)
Admitted.
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.
+ 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)).
+ Proof.
+
+ Qed.
+ Lemma lem_Sd_next_Sc_or_Maj: forall config ,
+ Sd config -> (Sc (round Robogram da config) \/ Maj (round Robogram da config)).
+ Proof.
+
+ Qed.
+ Lemma lem_Ic_next_Maj_or_Gathered: forall config ,
+ Ic config -> (Maj (round Robogram da config) \/ Gathered (round Robogram da config)).
+ Proof.
+
+ Qed.
+ Lemma lem_Id_next_Maj_or_Ic: forall config ,
+ Id config -> (Maj (round Robogram da config) \/ Ic (round Robogram da config)).
+ Proof.
+
+ Qed.
+ Lemma lem_Sc_next_Maj_or_Gathered: forall config ,
+ Sc config -> (Maj (round Robogram da config) \/ Gathered (round Robogram da config)).
+ Proof.
+
+ Qed.
+ Lemma lem_Gd_next_Maj_or_Gc: forall config ,
+ Gd config -> (Maj (round Robogram da config) \/ Gc (round Robogram da config)).
+ Proof.
+
+ 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)).
+ Proof.
+
+ Qed.
End test.
diff --git a/lib/ast.ml b/lib/ast.ml
index a6ff2f8..8cf7282 100644
--- a/lib/ast.ml
+++ b/lib/ast.ml
@@ -434,8 +434,8 @@ let graph_from_edges (el : edge list)=
ignore (Sys.command "dot -Tpng graph.dot -o graph.png")
-(*/GRAPH*)
+(*/GRAPH*)
type measure = Measure of int * G.t
@@ -562,8 +562,7 @@ let check_light d : bool =
let rec check flist = (
fun x -> match x with
| [] -> true
- | Public (_,Light(Intern _))::_ -> raise(Failure("Error light in wrong field"))
- | Private (_, Light(Extern _))::_ -> raise(Failure("Error light in wrong field"))
+ | Public (_,Light(Intern _))::_ | Private (_, Light(Extern _))::_ -> raise(Failure("Error light in wrong field"))
| _::t-> check t
) flist
in
diff --git a/lib/gencoq.ml b/lib/gencoq.ml
index 991f658..bfca444 100644
--- a/lib/gencoq.ml
+++ b/lib/gencoq.ml
@@ -26,13 +26,13 @@ let get_nb_byz (infos: information list) : int =
in
match byz with
| Some(Byzantines Number x) -> x
- | Some(Byzantines Id liste) -> List.length liste (*TODO: Evidement faux mais a traiter plus tard*)
+ | Some(Byzantines Id _) -> raise(Failure("Generation of byzantines list not implented"))
| _ -> 0
(** [get_val_ret infos] retourne le type de retour du robogram
@param information list correspondant à la description du monde
- @return [string] correspondant a location ou direction POUR LE MOMENT TODO: modif avec actively update
+ @return [string] correspondant a location ou direction POUR LE MOMENT
*)
let get_val_ret (infos : information list) : string =
(* Seulement location et direction pour le moment, TODO: Implementation Light*)
@@ -157,7 +157,6 @@ let instance_R_R2 (s:space) (d: information list): 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}."])
in
@@ -173,7 +172,7 @@ let instance_space (s: space) (d : information list): stmt list =
| R -> instance_R_R2 s d
| R2 -> instance_R_R2 s d
| ZnZ n -> instance_ring n
- | _ ->raise(Failure ("Not implemanted"))
+ | _ ->raise(Failure ("Space Not implemanted"))
in
s'@[]
@@ -265,7 +264,6 @@ let instance_sensors (s:sensor list) : stmt list =
if range != "Full" then Var(range,Raw("R"))
::Instance("Obs",Cst("Observation"),App(Cst ("limited_"^m^"set_observation"),[Cst(errorVS^range)]))
::[]
-
else Instance("Obs",Cst("Observation"),Cst(m^"set_observation"))::[]
(**[require_rigidity r] retourne un stmt permettant de generer le require pour la rigidite [r]
@@ -354,21 +352,25 @@ let generate_robogram (r : expr list) (d: information list) : stmt list =
-(**[generate_lemmas g] retourne la liste de stmt correspondant au lemme extrait du graph g
+(**[generate_lemmas g] retourne la liste de stmt correspondant aux lemmes extrait du graph g
@param g [G.t]
@return [stmt list]*)
-let generate_lemmas (g : Ast.G.t) : stmt list =
- Ast.G.fold_vertex (fun v acc ->
+let generate_lemmas (g : Ast.G.t) : (stmt list * string list) =
+ Ast.G.fold_vertex (fun v (acc,s) ->
let succs = Ast.G.succ g v in
let forall v =
String.concat " " (List.map string_of_expression (Ast.get_param v))
in
if succs <> [] then
- let rcs = List.map (fun x -> x ^ " (round Robogram da config)") (List.map string_of_expression succs) in
- Lemma("lemma"^string_of_int (List.length acc),Forall(("config "^forall v),Raw(string_of_expression v^" config -> "^String.concat " \\/ " rcs)),[])::acc
+ let string_succs = (List.map string_of_expression succs) in
+ let rcs = List.map (fun x -> x ^ " (round Robogram da config)") string_succs in
+ (Lemma("lem_"^string_of_expression v^"_next_"^String.concat "_or_" string_succs,Forall(("config "^forall v),Raw(string_of_expression v^" config -> ("^String.concat " \\/ " rcs^")")),[])::acc,
+ ("("^string_of_expression v ^" config )")::s)
else
- acc
- ) g []
+ (acc,s)
+ ) g ([],[])
+
+
(**[generate_measure m] retourne la liste de stmt correspondant a la generation de la mesure
@param m [measure]
@@ -377,21 +379,23 @@ 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
Ast.png_from_graph g;
- let lems =Var("da",Cst "demonic_action")::List.rev (generate_lemmas g) in
+ let lemsgen = let lems = generate_lemmas g in
+ Lemma("InGraph",Forall("config",Raw(String.concat " \\/ " (snd lems))),[])
+ ::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@lems
+ "Instance measure_compat : Proper (equiv ==> Logic.eq) measure."])::proof_to_complete@Var("da",Cst "demonic_action")::lemsgen
-(**[generate_coq d] genere a partir de la description complete (world,robogram,measure) l'instance coq
- @param descritpion
+(**[generate_coq d s] genere a partir de la description complete (world,robogram,measure) [d] l'instance coq nommé [s]
+ @param description d
+ @param string s
@return [unit] *)
let generate_coq (Description(d,r,m) : description) (section_name : string)=
if Ast.check_light (Description (d,r,m)) &&
Ast.check_activelyup (Description(d,r,m)) &&
Ast.check_sensors_desc (Description(d,r,m))
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) in
diff --git a/lib/graphmeasure.ml b/lib/graphmeasure.ml
deleted file mode 100644
index 20f6b58..0000000
--- a/lib/graphmeasure.ml
+++ /dev/null
@@ -1,78 +0,0 @@
-open Graph
-open Printf
-module Node = struct
- type t = string
- let compare = compare
- let hash = Hashtbl.hash
- let equal = (=)
-end
-
-module Edge = struct
- type t = string
- let compare = compare
- let default = ""
-end
-module G = Graph.Imperative.Digraph.ConcreteLabeled(Node)(Edge)
-
-
-module Dot = Graphviz.Dot(struct
- include G
- let edge_attributes (_,l,_) = [`Label l]
- let default_edge_attributes _ = []
- let get_subgraph _ = None
- let vertex_attributes _ = []
- let vertex_name v = v
- let default_vertex_attributes _ = []
- let graph_attributes _ = []
-end)
-
-type edge =
-| Nolab of (string * string)
-| Lab of (string * string *string)
-
-let graph_from_edges (el : edge list)=
- let g = G.create () in
- let nolab = fun (x, y) ->
- let vx = G.V.create x in
- let vy = G.V.create y in
- G.add_edge g vx vy
- in
- let lab = fun (x, y, z) ->
- let vx = G.V.create x in
- let vz = G.V.create z in
- G.add_edge_e g (vx, y, vz)
- in
- let rec add_edge (el : edge list) =
- match el with
- | [] -> ()
- | (Nolab h)::t -> nolab h ; add_edge t
- | (Lab h)::t -> lab h ; add_edge t
- in add_edge el;
- g
-
-
- let print_relations_test g =
- G.iter_vertex (fun v ->
- let succs = G.succ g v in
- if succs <> [] then (
- printf "Si %s est vrai alors " v;
- let su = String.concat " ou " succs in
- if List.length succs > 1 then
- printf "%s sont vrais.\n" su
- else
- printf "%s est vrai.\n" su
- )
- ) g
-
- let png_from_graph g =
- let graph = G.fold_vertex (fun v acc ->
- let succs = G.succ g 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 {\n" ^ graph ^ "}" 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")
\ No newline at end of file
diff --git a/lib/parser.mly b/lib/parser.mly
index 113c850..60f3cc8 100644
--- a/lib/parser.mly
+++ b/lib/parser.mly
@@ -310,13 +310,16 @@ pattern :
measure:
- | PARENOPEN l = separated_list(COMMA,VARIABLE) PARENCLOSE el = edge_list {Measure(List.length l,graph_from_edges el)}
+ | PARENOPEN l = separated_list(COMMA,VARIABLE) PARENCLOSE el = edge_list {Measure(List.length l,graph_from_edges (List.flatten el))}
edge :
- | v1 = sommet ARROW v2 = sommet {Nolab(v1,v2)}
+ | v1 = sommet ARROW v2 = sommet {[Nolab(v1,v2)]}
+ | v = sommet ARROW BRACKETOPEN sl = separated_list (SEMICOLON,sommet) BRACKETCLOSE {List.map (fun x -> Nolab(v,x))sl}
+
edge_list :
| v = list(edge) { v }
+
sommet :
| p = prop {p}
@@ -324,6 +327,7 @@ prop :
| PARENOPEN prop propop prop PARENCLOSE {BinOp($2,$3,$4)}
| NOT prop {Not $2}
| VARIABLE {Var $1}
+ | KEYWORD {Var $1}
| PARENOPEN f = appfunc PARENCLOSE {f}
propop :
--
GitLab