progress

TAEditor/TAGraph.ml

-    type def = unit
+    type def = string list
 
-    type state = string * (string list)
-    type arc = float
+    type invariant = string
+    type guard = string
+    type state = string * invariant * bool * bool
+    type arc = string * guard * string list
     type attribute_id = int
     type attribute = [ `Choice of string list
                      | `ControlPoint of DrawingGeom.point
                      | `String of string
                      | `Color of string ]
 
+    let string_of_reset r =
+      Printf.sprintf "{%s}" (List.fold_left (fun x s -> if x="" then s else x^","^s) "" r)
+                   
+    let list_of_bool b = 
+      if b then ["true"; "false"]
+      else ["false"; "true"]
 
-    let init_def () = ()
-    let init_arc _ _ = Some 1.0
+    let init_def () = []
+    let init_arc _ _ = Some ("a","true",[])
 
     let state_id = ref 0
     let init_state () = incr state_id;
-                        ((string_of_int !state_id), ["toto"])
-    let draw_state (s,_) p = [
-                              `Circle (p,10.0);
-                              `Text(p,s);
-      ]
-    let draw_arc arc (source_sh,target_sh) =
+                        ((string_of_int !state_id), "true", !state_id=1 , false)
+    let draw_state (s,inv,init,final) p = 
+      let l = 
+      [
+        `Circle (p,10.0);
+        `Text(p,s^ (if inv<> "true" then ","^inv else ""));
+      ] in
+      if final then (`Circle (p,13.0))::l
+      else l
+
+    let draw_arc (label,inv,reset) (source_sh,target_sh) =
       let open DrawingGeom in
       let pos1 = center_shape source_sh in
       let pos2 = center_shape target_sh in
-      let text = string_of_float arc in
+      let text = Printf.sprintf "[%s],%s,%s" label inv (string_of_reset reset) in
 
       if source_sh<>target_sh then begin
       shapes_of_path source_sh [`Text (0.5,text)] ~arrow2:(Some (fun x y -> `Arrow (x,y))) target_sh
@@ -34,43 +47,43 @@
         end
 
 
-    let get_state_attr (s, at) =
-      "Node", ((0,"content",`String s) ::
-       (List.mapi (fun i sv -> (i+1),"attribute "^(string_of_int (i+1)),(`String sv )) at))
-
-    let update_state_attr (s,at) attr_id = function
-      | None ->
-         if attr_id = 0 then Some ("",at)
-         else
-           let _,listat = List.fold_left (fun (i,l) at ->
-                              if attr_id = i+1 then
-                                (i+1, l) else (i+1, at::l)) (0,[]) at in
-           Some (s,listat)
-      | Some (`String newv) ->
-         if attr_id = 0 then Some (newv,at)
-         else
-           let _,listat = List.fold_left (fun (i,l) at ->
-                              if attr_id = i+1 then
-                                (i+1, newv::l) else (i+1, at::l)) (0,[]) at in
-           Some (s,listat)
+    let get_state_attr (s,inv,init,final) =
+      "State", [(0,"content",`String s) ;
+                (1,"invariant", `String inv) ;
+                (2, "initial", `Choice (list_of_bool init)) ;
+                (3, "final", `Choice (list_of_bool final)) 
+              ]
+
+    let update_state_attr (s,inv,init,final) attr_id = function
+      | None -> (match attr_id with
+                   0 -> Some ("",inv,init,final)
+                 | 1 -> Some (s,"true",init,final)
+                 | _ -> Some (s,inv,init,final)        
+                )
+      | Some (`String newv) when attr_id = 0 ->
+         Some (newv,inv,init,final)
+      | Some (`String newinv) when attr_id = 1 ->
+         Some (s,newinv,init,final)
+      | Some (`Choice (v::_)) when attr_id =2 ->
+         Some (s,inv,v="true",final)
+      | Some (`Choice (v::_)) when attr_id =3 ->
+         Some (s,inv,init,v="true")       
       | _ -> None
 
-    let get_new_state_attr (s,at) _ = []
-
-    let get_arc_attr prob =
-      "Arc", [(0,"Probability",`String (string_of_float prob)) ]
-
-    let update_arc_attr _ _ = function
-      | None ->
-         begin try let p = 1.0 in
-             if p>= 0.0 && p<= 1.0 then Some p else None
-               with _ -> None
-         end
-      | Some (`String v) ->
-         begin try let p = float_of_string v in
-             if p>= 0.0 && p<= 1.0 then Some p else None
-               with _ -> None
-         end
+    let get_new_state_attr (s,inv,init,final) _ = []
+
+    let get_arc_attr (label,guard,reset) =
+      "Arc", [(0,"label",`String label);
+              (1,"guard",`String guard);
+              (2,"reset",`String (string_of_reset reset));
+             ]
+
+    let update_arc_attr (label,guard,reset) attr_id = function
+      | Some (`String v) when attr_id = 0 ->
+         Some (v,guard,reset)
+      | Some (`String v) when attr_id = 1 ->
+         Some (label,v,reset)
+                
       | _ -> None
 
     let get_new_arc_attr atlist _ = []
@@ -85,8 +98,8 @@
     let print = 
       ["dot" , (fun f stateit arcit ->
       Format.fprintf f "digraph {\n";
-      stateit (fun _ (s,_) (x,y) -> Format.fprintf f "%s [pos=\"%f,%f\"];\n" s (x) (y));
-      arcit (fun _ _ ((_,(source,_),_),(_,(target,_),_)) ->
+      stateit (fun _ (s,_,_,_) (x,y) -> Format.fprintf f "%s [pos=\"%f,%f\"];\n" s (x) (y));
+      arcit (fun _ _ ((_,(source,_,_,_),_),(_,(target,_,_,_),_)) ->
           Format.fprintf f "%s -> %s;\n" source target);
       Format.fprintf f "}") , "markovChain.dot"
                 ]