Commit e9a4f9be authored by Benoit Barbot's avatar Benoit Barbot
Browse files

progress

parent b0cb3af5
Pipeline #1748 failed with stage
in 26 seconds
......@@ -26,8 +26,11 @@
`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 (x,y) = p in
let l2 = if init then (`Line (p,(x -. 25.0,y))) :: (`Arrow ((x-.10.0,y),(x -. 25.0,y))) :: l
else l in
if final then (`Circle (p,13.0))::l2
else l2
let draw_arc (label,inv,reset) (source_sh,target_sh) =
let open DrawingGeom in
......@@ -118,13 +121,29 @@
| `Check b -> string_of_bool b
| `ControlPoint _ -> ""
let print_to_prism f def stateit arcit =
let n = ref (-1) in
stateit (fun _ _ _ -> incr n);
Format.fprintf f "pta\nmodule m\n\tstate:[0..%i] init %i;\n" !n 0;
List.iter (fun s -> Format.fprintf f "\t%s:clock;\n" s) def;
arcit (fun _ (label,guard,reset) ((source,(_,invarient,_,_),_),(target,_,_))->
let g2 = if guard = "true" then "" else "&"^guard in
let g3 = if invarient = "true" then "" else "&"^invarient in
Format.fprintf f "\t[%s] (state=%i)%s%s -> (state'=%i)" label source g2 g3 target;
List.iter (fun r -> Format.fprintf f "&(%s'=0)" r) reset;
Format.fprintf f ";\n";
);
Format.fprintf f "endmodule\n"
let print =
["dot" , (fun f stateit arcit ->
["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,_,_,_),_)) ->
Format.fprintf f "%s -> %s;\n" source target);
Format.fprintf f "}") , "markovChain.dot"
Format.fprintf f "}") , "markovChain.dot";
"prism", print_to_prism, "pta.prism"
]
let parse_file _ add_node add_arc = ()
......@@ -90,7 +90,7 @@
| `ControlPoint _ -> ""
let print = [
"dot", (fun f stateit arcit ->
"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,_),_)) ->
......
......@@ -255,7 +255,7 @@ let rec print_path link prev last a = function
Format.fprintf a " %s node {%s}%a" (if link then "--" else "") s (print_path false prev last) q
let print =
[ "tikz", (fun f stateit arcit ->
[ "tikz", (fun f _ stateit arcit ->
(* Format.fprintf f "\\documentclass[]{article}\n\\usepackage{tikz}\n\\begin{document}";*)
Format.fprintf f "\\begin{tikzpicture}\n";
stateit (fun i (s,at) pos->
......
......@@ -30,9 +30,10 @@ module type PREGRAPH =
val parse_file : string -> (state -> DrawingGeom.point -> 'nodeid) -> (arc -> 'nodeid -> 'nodeid -> unit) -> unit
val print: (string * (Format.formatter ->
(( int -> state -> (float*float) -> unit) -> unit) ->
((int -> arc -> ((int*state*(float*float))*(int*state*(float*float))) -> unit) -> unit)
-> unit) * string) list
def ->
(( int -> state -> (float*float) -> unit) -> unit) ->
((int -> arc -> ((int*state*(float*float))*(int*state*(float*float))) -> unit) -> unit)
-> unit) * string) list
end
......@@ -178,7 +179,7 @@ module S (P:PREGRAPH) =
let print_graph =
List.map (fun (name, pfun , file_name) ->
name, (fun out graph ->
pfun out
pfun out graph.def
(fun f ->
Data.iteri (fun k ((),(s,pos)) -> f (Data.unsafe_rev k) !s !pos) graph.state)
(fun f ->
......
Markdown is supported
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