From a02ded5cb92eb467e82e865caefb4e8592aa4b97 Mon Sep 17 00:00:00 2001 From: Pierrick Couderc Date: Wed, 2 Oct 2013 08:47:28 +0200 Subject: [PATCH 01/26] Removed deprecation warning (OCaml 4.01) --- src/Minim.ml | 22 +++++++-------- src/Presyntax.ml | 72 +++++++++++++++++++++++------------------------- 2 files changed, 45 insertions(+), 49 deletions(-) diff --git a/src/Minim.ml b/src/Minim.ml index cc33e4a..2f545bc 100755 --- a/src/Minim.ml +++ b/src/Minim.ml @@ -52,7 +52,7 @@ let string_of_graph g = in GMap.fold folder g "" -let string_of_partition parts = +let string_of_partition parts = (List.fold_left (fun s part -> s ^ "\n" ^ (string_of_gset string_of_gstate part)) "" parts) ^ "\n" @@ -109,12 +109,12 @@ let build_graph f_deriv init_graph init_partition defs ps = | _ -> (init_graph, init_partition) let rec refine (graph, part) = - let prevs = + let prevs = List.map (fun x -> GSet.fold (fun x' acc -> GSet.union acc (GMap.find x' graph)) x GSet.empty) part in - let split part prev = + let split part prev = let p1 = GSet.inter part prev in let p2 = GSet.diff part prev in (p1, p2) @@ -123,11 +123,11 @@ let rec refine (graph, part) = match pt with | [] -> [] | h1::t1 -> (f2 h1 pr)@(f1 t1 pr) - and f2 pt pr = + and f2 pt pr = match pr with | [] -> [pt] | h2::t2 -> let (spl1, spl2) = split pt h2 in - if GSet.is_empty spl1 or GSet.is_empty spl2 then + if GSet.is_empty spl1 || GSet.is_empty spl2 then f2 pt t2 else [spl1 ; spl2] @@ -137,7 +137,7 @@ let rec refine (graph, part) = then part' else refine (graph, part') let build_lts partition = - let (ps, ls) = + let (ps, ls) = List.partition (fun x -> match GSet.choose x with | LState _ -> false | PState _ -> true) @@ -163,15 +163,15 @@ let build_lts partition = | cp::t -> begin let p = List.hd cp in - let labs = + let labs = List.fold_left - (fun acc x -> + (fun acc x -> match List.filter (fun (src,_,_) -> src = p) x with | [] -> acc | t::_ -> t::acc ) [] lstates - in let transs' = + in let transs' = List.fold_left (fun acc (_,lbl,dst) -> let cdl = List.filter @@ -214,7 +214,5 @@ let is_fbisimilar f_deriv defs p1 p2 = build_graph f_deriv init_graph init_partition defs [p1;p2] in let partition' = refine (graph, partition) in let l = List.filter (fun x -> - (GSet.mem pst1 x) or (GSet.mem pst2 x)) partition' in + (GSet.mem pst1 x) || (GSet.mem pst2 x)) partition' in (List.length l) = 1 - - diff --git a/src/Presyntax.ml b/src/Presyntax.ml index 48fa0b6..6ec05d6 100644 --- a/src/Presyntax.ml +++ b/src/Presyntax.ml @@ -14,7 +14,7 @@ type preconstdef = let string_of_preconstdef = function | PConstDef (name,value) -> sprintf "const %%%s = %d" name value - + type pretypedef = | PTDefRange of string * int * int | PTDefEnum of string * SSet.t @@ -22,7 +22,7 @@ type pretypedef = -let env_type = +let env_type = let bool_type = PTDefEnum( "Bool", (SSet.add "True" (SSet.add "False" SSet.empty))) in ref (SMap.add "Bool" bool_type SMap.empty) ;; @@ -34,7 +34,7 @@ let add_to_env_type k v = let string_of_pretypedef = function | PTDefRange (name,min,max) -> sprintf "type %s = [%d..%d]" name min max | PTDefEnum (name,names) -> "type " ^ name ^ " = " ^ (string_of_set (fun x -> x) names) - + type preexpr = | PTrue | PFalse @@ -60,7 +60,7 @@ type preexpr = exception Type_Exception of string -let bool_of_value = function +let bool_of_value = function | Bool b -> b | Name n -> raise (Type_Exception (sprintf "Name %s was received where Bool was expected !!!" n)) | Int i -> raise (Type_Exception (sprintf "Int %d was received where Bool was expected !!!" i)) @@ -74,7 +74,7 @@ let int_of_value = function | Bool b -> raise (Type_Exception (sprintf "Bool %s was received where Int was expected !!!" (if b then "true" else "false"))) | Name n -> raise (Type_Exception (sprintf "Name %s was received where Int was expected !!!" n)) | Int i -> i - + let rec interprete_preexpr : preexpr -> value = function | PTrue -> Bool true | PFalse -> Bool false @@ -83,14 +83,14 @@ let rec interprete_preexpr : preexpr -> value = function | PConst name -> Int (SMap.find name !env_const) | PVar name -> (SMap.find name !env_var) | PNot pexpr -> let b = bool_of_value (interprete_preexpr pexpr) in Bool (not b) - | PAnd (preexpr1, preexpr2) -> + | PAnd (preexpr1, preexpr2) -> let b1 = bool_of_value (interprete_preexpr preexpr1) and b2 = bool_of_value (interprete_preexpr preexpr2) in - Bool ( b1 && b2 ) + Bool ( b1 && b2 ) | POr (preexpr1, preexpr2) -> let b1 = bool_of_value (interprete_preexpr preexpr1) and b2 = bool_of_value (interprete_preexpr preexpr2) in - Bool ( b1 or b2 ) + Bool ( b1 || b2 ) | PAdd (preexpr1, preexpr2) -> let i1 = int_of_value (interprete_preexpr preexpr1 ) @@ -135,7 +135,7 @@ let rec interprete_preexpr : preexpr -> value = function | (Int i1, Int i2) -> Bool ( i1 = i2 ) | (Name n1, Name n2) -> Bool ( n1 = n2 ) | (_, _) -> Bool ( false )) - + | PNeq (preexpr1, preexpr2) -> let p1 = interprete_preexpr preexpr1 and p2 = interprete_preexpr preexpr2 in @@ -149,12 +149,12 @@ let rec interprete_preexpr : preexpr -> value = function let i1 = int_of_value (interprete_preexpr preexpr1 ) and i2 = int_of_value ( interprete_preexpr preexpr2 ) in Bool ( i1 <= i2 ) - + | PSupEq (preexpr1, preexpr2) -> let i1 = int_of_value (interprete_preexpr preexpr1 ) and i2 = int_of_value ( interprete_preexpr preexpr2 ) in Bool ( i1 >= i2 ) - + | PIf (cond, preexpr1, preexpr2) -> let b = bool_of_value (interprete_preexpr cond) in if b then @@ -181,7 +181,7 @@ let rec string_of_preexpr = function | PInf (e1,e2) -> sprintf "(%s) < (%s)" (string_of_preexpr e1) (string_of_preexpr e2) | PSup (e1,e2) -> sprintf "(%s) > (%s)" (string_of_preexpr e1) (string_of_preexpr e2) | PEq (e1,e2) -> sprintf "(%s) = (%s)" (string_of_preexpr e1) (string_of_preexpr e2) - | PNeq (e1,e2) -> sprintf "(%s) <> (%s)" (string_of_preexpr e1) (string_of_preexpr e2) + | PNeq (e1,e2) -> sprintf "(%s) <> (%s)" (string_of_preexpr e1) (string_of_preexpr e2) | PInfEq (e1,e2) -> sprintf "(%s) <= (%s)" (string_of_preexpr e1) (string_of_preexpr e2) | PSupEq (e1,e2) -> sprintf "(%s) >= (%s)" (string_of_preexpr e1) (string_of_preexpr e2) | PIf (c,e1,e2) -> sprintf "if (%s) then (%s) else (%s)" (string_of_preexpr c) (string_of_preexpr e1) (string_of_preexpr e2) @@ -236,17 +236,17 @@ let value_list : pretypedef -> (value list) = function | PTDefRange (_, min,max) ->(make_int_list min max) | PTDefEnum ("Bool" , _) -> [Bool true; Bool false] | PTDefEnum (_ , enum) -> (List.map (fun a -> Name a) (SSet.elements enum)) - + let rec process_of_receive : string -> string -> pretypedef -> preprocess -> process = fun canal nomVar theType pproc -> let val_list = value_list theType in let rec process_of_receive_aux v_list= match v_list with - | [] -> failwith "Empty list" + | [] -> failwith "Empty list" | hd::[] -> (env_var := (SMap.add nomVar hd !env_var); Prefix( In( sprintf "%s_%s" canal (string_of_value hd)), (process_of_preprocess pproc) )) - | hd::tl -> + | hd::tl -> env_var:=(SMap.add nomVar hd !env_var); let pref = Prefix( In( sprintf "%s_%s" canal (string_of_value hd)), (process_of_preprocess pproc) ) in @@ -257,37 +257,37 @@ let rec process_of_receive : string -> string -> pretypedef -> preprocess -> pro and process_of_prefix : preprefix -> preprocess -> process = fun pfix pproc -> match pfix with - | PTau -> Prefix(Tau, (process_of_preprocess pproc) ) + | PTau -> Prefix(Tau, (process_of_preprocess pproc) ) | PIn (pexpr) -> Prefix( In ( string_of_value (interprete_preexpr pexpr)), - (process_of_preprocess pproc) ) + (process_of_preprocess pproc) ) | POut(pexpr) -> Prefix( Out ( string_of_value (interprete_preexpr pexpr)), - (process_of_preprocess pproc) ) - - | PSend(pexprCanal, pexprVal) -> Prefix( Out ( sprintf "%s_%s" + (process_of_preprocess pproc) ) + + | PSend(pexprCanal, pexprVal) -> Prefix( Out ( sprintf "%s_%s" (string_of_value (interprete_preexpr pexprCanal)) (string_of_value (interprete_preexpr pexprVal)) ), (process_of_preprocess pproc)) - | PReceive(pexprCanal, nomVar, nomType) -> + | PReceive(pexprCanal, nomVar, nomType) -> (if SMap.mem nomVar !env_var then raise (Vardef_Exception nomVar)); - let canal = string_of_value (interprete_preexpr pexprCanal) + let canal = string_of_value (interprete_preexpr pexprCanal) and theType = SMap.find nomType !env_type in let prc = process_of_receive canal nomVar theType pproc in (env_var := SMap.remove nomVar !env_var; prc) -and process_of_preprocess : preprocess -> process = - fun preproc -> +and process_of_preprocess : preprocess -> process = + fun preproc -> printf "Transforming process:\n%s\n%!" (string_of_preprocess preproc) ; match preproc with | PSilent -> Silent | PPrefix (pfix, pproc) -> process_of_prefix pfix pproc - - | PSum (pproc1, pproc2) -> - Sum( (process_of_preprocess pproc1), + + | PSum (pproc1, pproc2) -> + Sum( (process_of_preprocess pproc1), (process_of_preprocess pproc2) ) - | PPar (pproc1, pproc2) -> - Par( (process_of_preprocess pproc1), + | PPar (pproc1, pproc2) -> + Par( (process_of_preprocess pproc1), (process_of_preprocess pproc2) ) | PRes (nvar, pproc) -> @@ -298,13 +298,13 @@ and process_of_preprocess : preprocess -> process = | PRename( oldName, newName , pproc) -> Rename( oldName, newName, (process_of_preprocess pproc) ) - | PGuard( pexpr, ppro) -> + | PGuard( pexpr, ppro) -> let b = bool_of_value (interprete_preexpr pexpr) in if b then process_of_preprocess ppro else Silent - + type preparam = | PParamVar of string * string | PParamBool of bool @@ -319,7 +319,7 @@ let string_of_preparam = function type predefinition = PDefinition of string * preparam list * preprocess -let string_of_predef_header (PDefinition (name,params,_)) = +let string_of_predef_header (PDefinition (name,params,_)) = name ^ (string_of_args string_of_preparam params) let string_of_predefinition = function @@ -332,16 +332,16 @@ let definitions_of_predefinition : predefinition -> definition list = (* let rec def_of_predef_aux : string -> value list -> preparam list -> preprocess -> definition list= *) (* function name computed_params preparams preproc -> *) let rec def_of_predef_aux name computed_params preparams preproc = - match preparams with + match preparams with | [] -> [ Definition (name, computed_params, process_of_preprocess preproc) ] | (PParamBool b)::tl -> def_of_predef_aux name (computed_params@[Bool b]) tl preproc | (PParamName n)::tl -> def_of_predef_aux name (computed_params@[Name n]) tl preproc | (PParamInt i)::tl -> def_of_predef_aux name (computed_params@[Int i]) tl preproc - | (PParamVar (nomVar, theType))::tl -> + | (PParamVar (nomVar, theType))::tl -> (if SMap.mem nomVar !env_var then raise (Vardef_Exception nomVar)); let val_list = value_list (SMap.find theType !env_type) in - let def_list = List.map (function v -> + let def_list = List.map (function v -> env_var := (SMap.add nomVar v !env_var); (def_of_predef_aux name (computed_params@[v]) tl preproc) ) val_list @@ -351,5 +351,3 @@ let definitions_of_predefinition : predefinition -> definition list = in printf "Transforming definition:\n%s\n%!" (string_of_predefinition predef) ; def_of_predef_aux name [] preparams preproc - - From 18ba71d3bb62136e3aadc4305cbe78a8de861aa5 Mon Sep 17 00:00:00 2001 From: Pierrick Couderc Date: Wed, 9 Oct 2013 09:55:10 +0200 Subject: [PATCH 02/26] Solved the automatic Failure at start formula_of_preformula missed its argument, so the "failwith" was directly evaluated --- src/Control.ml | 65 +++++++++++++++++++++++--------------------------- src/Formula.ml | 9 ++++--- src/Pave.ml | 59 +++++++++++++++++++++++---------------------- 3 files changed, 64 insertions(+), 69 deletions(-) diff --git a/src/Control.ml b/src/Control.ml index 405bd6a..4256334 100644 --- a/src/Control.ml +++ b/src/Control.ml @@ -39,11 +39,11 @@ let script_mode = ref false ;; exception Constdef_Exception of string ;; exception Typedef_Exception of string ;; -let handle_help () = +let handle_help () = printf "%s\n> %!" help_me let handle_quit () = - printf "bye bye !\n%!" ; + printf "bye bye !\n%!" ; exit 0 let timing operation = @@ -51,13 +51,13 @@ let timing operation = in let result = operation() in let end_time = Sys.time() in - (result, end_time -. start_time) + (result, end_time -. start_time) let handle_constdef (const_name:string) (const_val:int) = (* printf "(handle_constdef %s %d)\n%!" const_name const_val ; *) if not (SMap.mem const_name !Presyntax.env_const) then Presyntax.env_const := SMap.add const_name const_val !Presyntax.env_const - else + else raise (Constdef_Exception const_name) ;; @@ -65,10 +65,10 @@ let handle_typedef_range (type_name:string) (min_val:string) (max_val:string) = (* printf "(handle_typedef_range %s %s %s)\n%!" type_name min_val max_val ; *) if not (SMap.mem type_name !Presyntax.env_type) then let find_val v = - try - SMap.find v !Presyntax.env_const + try + SMap.find v !Presyntax.env_const with - Not_found -> + Not_found -> try int_of_string v with @@ -76,14 +76,14 @@ let handle_typedef_range (type_name:string) (min_val:string) (max_val:string) = in let min = find_val min_val and max = find_val max_val in - - Presyntax.add_to_env_type type_name - ( if min < max then + + Presyntax.add_to_env_type type_name + ( if min < max then Presyntax.PTDefRange (type_name, min, max) else Presyntax.PTDefRange (type_name, max, min) - ) - else + ) + else raise (Typedef_Exception type_name) ;; @@ -96,7 +96,7 @@ let handle_typedef_enum (type_name:string) (names:string list) = in if not (SMap.mem type_name !Presyntax.env_type) then Presyntax.add_to_env_type type_name ( Presyntax.PTDefEnum (type_name, list2set names) ) - else + else raise (Typedef_Exception type_name) ;; @@ -122,7 +122,7 @@ let handle_normalization proc = let proc',time = timing (fun () -> normalize proc) in printf "%s\n%!" (string_of_nprocess proc') ; - printf "(elapsed time=%fs)\n%!" time + printf "(elapsed time=%fs)\n%!" time let handle_struct_congr p q = if !script_mode then @@ -133,7 +133,7 @@ let handle_struct_congr p q = (if ok then printf "the processes *are* structurally congruent\n%!" else printf "the processes are *not* structurally congruent\n%!") ; - printf "(elapsed time=%fs)\n%!" time + printf "(elapsed time=%fs)\n%!" time let global_definition_map = Hashtbl.create 64 @@ -143,12 +143,12 @@ let common_deriv f_deriv f_print str str2 p = printf "Compute %s...\n%!" str2; let op = fun () -> let np = normalize p in - f_deriv global_definition_map np + f_deriv global_definition_map np in let derivs, time = timing op in f_print derivs; - printf "(elapsed time=%fs)\n%!" time + printf "(elapsed time=%fs)\n%!" time let fetch_definition key = Hashtbl.find global_definition_map key @@ -166,7 +166,7 @@ let dot_style_format (p, l, p') = sprintf "\"%s\" -> \"%s\" [ label = \"%s\", fontcolor=red ]" (string_of_nprocess p) (string_of_nprocess p') (string_of_label l) -let dot_style_format' (pl, l, pl') = +let dot_style_format' (pl, l, pl') = sprintf "\"%s\" -> \"%s\" [ label = \"%s\", fontcolor=red ]" (string_of_list string_of_nprocess pl) (string_of_list string_of_nprocess pl') @@ -175,7 +175,7 @@ let dot_style_format' (pl, l, pl') = let common_lts f str p = if !script_mode then printf "> %s %s\n%!" str (string_of_process p) ; - let transs, time = timing (fun () -> f global_definition_map (normalize p)) + let transs, time = timing (fun () -> f global_definition_map (normalize p)) in List.iter (fun t -> printf "%s\n" (string_of_transition t)) transs; printf "\nGenerating %s.dot... %!" str; @@ -194,23 +194,23 @@ let common_lts f str p = fprintf oc "}\n"; close_out oc; printf "done\n(elapsed time=%fs)\n%!" time - + let common_minimization f_deriv str proc = if !script_mode then printf "> %s %s\n%!" str (string_of_process proc) ; printf "Minimize process...\n%!"; let transs, time = timing (fun () -> let p = normalize proc in - minimize f_deriv global_definition_map p) + minimize f_deriv global_definition_map p) in List.iter (fun t -> printf "%s\n" (string_of_transitions t)) transs; printf "\nGenerating lts_mini.dot... %!"; - let nprocs = + let nprocs = List.fold_left (fun acc (x, _, y) -> x::(y::acc)) [] transs in let oc = open_out "lts_mini.dot" in fprintf oc "digraph LTSMINI {\n"; - List.iter + List.iter (fun x -> fprintf oc "\"%s\" [ fontcolor=blue ]\n" (string_of_list string_of_nprocess x)) nprocs; @@ -221,7 +221,7 @@ let common_minimization f_deriv str proc = printf "done\n(elapsed time=%fs)\n%!" time -let common_bisim f_bisim str str2 str3 p1 p2 = +let common_bisim f_bisim str str2 str3 p1 p2 = if !script_mode then printf "> %s %s ~ %s\n%!" str (string_of_process p1) (string_of_process p2) ; printf "Calculate %s...\n%!" str2; @@ -230,7 +230,7 @@ let common_bisim f_bisim str str2 str3 p1 p2 = let np1 = normalize p1 in let np2 = normalize p2 in try - let bsm = f_bisim global_definition_map np1 np2 + let bsm = f_bisim global_definition_map np1 np2 in let end_time = Sys.time() in @@ -252,10 +252,10 @@ let common_is_bisim f_bisim str str2 p1 p2 = let np2 = normalize p2 in f_bisim global_definition_map np1 np2) in - if ok + if ok then printf "the processes *are* %s\n(elapsed time=%fs)\n%!" str2 time else printf "the processes are *not* %s\n(elapsed time=%fs)\n%!" str2 time - + let common_is_fbisim f_deriv str1 str2 p1 p2 = if !script_mode then printf "> %s ? %s ~ %s\n%!" str1 (string_of_process p1) (string_of_process p2) ; @@ -301,13 +301,8 @@ let handle_tderiv p = common_deriv (weak_derivatives true) printPfixMap "tderiv" -let handle_prop _ _ _ = failwith "TODO" - -let handle_check_local _ _ = failwith "TODO" - -let handle_check_global _ _ = failwith "TODO" - - - +let handle_prop _ _ _ = failwith "TODO: handle_prop" +let handle_check_local _ _ = failwith "TODO: handle_check_local" +let handle_check_global _ _ = failwith "TODO: handle_check_global" diff --git a/src/Formula.ml b/src/Formula.ml index 3fddb71..8561451 100644 --- a/src/Formula.ml +++ b/src/Formula.ml @@ -43,7 +43,7 @@ let string_of_modality : modality -> string = function | FWInNecessity -> "[[?]]" | FWAnyNecessity -> "[[.]]" -type formula = +type formula = | FTrue | FFalse | FAnd of formula * formula @@ -55,7 +55,7 @@ type formula = | FVar of string | FMu of string * formula | FNu of string * formula - + let rec string_of_formula : formula -> string = function | FTrue -> "True" | FFalse -> "False" @@ -68,8 +68,7 @@ let rec string_of_formula : formula -> string = function | FVar(var) -> var | FMu(x,f) -> sprintf "Mu(%s).%s" x (string_of_formula f) | FNu(x,f) -> sprintf "Nu(%s).%s" x (string_of_formula f) - -let formula_of_preformula : formula -> formula = - failwith "TODO" +let formula_of_preformula pf : formula -> formula = + failwith "TODO formula_of_preformula" diff --git a/src/Pave.ml b/src/Pave.ml index 8d0583e..741d307 100644 --- a/src/Pave.ml +++ b/src/Pave.ml @@ -4,7 +4,7 @@ open Utils let version_str = "Pave' v.1 r20130910" let usage = "Usage: pave " -let banner = +let banner = "\n"^ "===============\n"^ " .+------+ +------+.\n"^ @@ -44,40 +44,41 @@ let parse_error_msg lexbuf = in printf "Parser error at line %d char %d: ~%s~\n%!" l c tok ;; -match !load_file with +let _ = + match !load_file with | None -> - printf "Interactive mode... \n%!"; + printf "Interactive mode... \n%!"; Control.script_mode := false ; while true do - printf "> %!"; + printf "> %!"; let lexbuf = Lexing.from_channel stdin in - try - ignore (Parser.script Lexer.token lexbuf) - with - | Failure msg -> printf "Failure: %s\n%!" msg - | Fatal_Parse_Error(msg) -> - parse_error_msg lexbuf ; - printf " ==> %s\n%!" msg - | Parsing.Parse_error -> - parse_error_msg lexbuf + try + ignore (Parser.script Lexer.token lexbuf) + with + | Failure msg -> printf "Failure: %s\n%!" msg + | Fatal_Parse_Error(msg) -> + parse_error_msg lexbuf ; + printf " ==> %s\n%!" msg + | Parsing.Parse_error -> + parse_error_msg lexbuf done | Some file -> - printf "Loading file %s... \n%!" file; + printf "Loading file %s... \n%!" file; Control.script_mode := true ; - let lexbuf = Lexing.from_channel (open_in file) in - let rec loop () = - let continue = - try - Parser.script Lexer.token lexbuf - with - | Failure msg -> printf "Failure: %s\n%!" msg ; true - | Fatal_Parse_Error(msg) -> - parse_error_msg lexbuf ; - printf " ==> %s\n%!" msg ; true - | Parsing.Parse_error -> - parse_error_msg lexbuf ; true - in - if continue then loop (); + let lexbuf = Lexing.from_channel (open_in file) in + let rec loop () = + let continue = + try + Parser.script Lexer.token lexbuf + with + | Failure msg -> printf "Failure: %s\n%!" msg ; true + | Fatal_Parse_Error(msg) -> + parse_error_msg lexbuf ; + printf " ==> %s\n%!" msg ; true + | Parsing.Parse_error -> + parse_error_msg lexbuf ; true in - loop () + if continue then loop (); + in + loop () ;; From 404b7a57a97915d1abca5225b79beecfd78e358f Mon Sep 17 00:00:00 2001 From: Pierrick Couderc Date: Sat, 12 Oct 2013 11:47:46 +0200 Subject: [PATCH 03/26] Added draft version of handle_prop Added also printing of formulas for future debug --- src/Control.ml | 18 +++++++++++++++++- src/Formula.ml | 31 +++++++++++++++++++++++++++++-- 2 files changed, 46 insertions(+), 3 deletions(-) diff --git a/src/Control.ml b/src/Control.ml index 4256334..f1668b7 100644 --- a/src/Control.ml +++ b/src/Control.ml @@ -299,9 +299,25 @@ let handle_wderiv p = common_deriv (weak_derivatives false) printPfixMap "wderiv let handle_tderiv p = common_deriv (weak_derivatives true) printPfixMap "tderiv" "tau derivatives" p +type prop = + (string * string list * Formula.formula) -let handle_prop _ _ _ = failwith "TODO: handle_prop" + +let handle_prop n il f = + let namelist = + if List.length il <> 0 then + let il = List.rev il in + "(" ^ (List.fold_left + (fun n acc -> acc ^ ", " ^ n) + (List.hd il) + (List.tl il)) + ^ ")" + else "()" (* Unreachable case *) + in + Formula.string_of_formula f |> + Format.printf "Prop : %s %s : %s@." n namelist; + Formula.add_prop n il f let handle_check_local _ _ = failwith "TODO: handle_check_local" diff --git a/src/Formula.ml b/src/Formula.ml index 8561451..b20f976 100644 --- a/src/Formula.ml +++ b/src/Formula.ml @@ -69,6 +69,33 @@ let rec string_of_formula : formula -> string = function | FMu(x,f) -> sprintf "Mu(%s).%s" x (string_of_formula f) | FNu(x,f) -> sprintf "Nu(%s).%s" x (string_of_formula f) +type prop = string list * formula -let formula_of_preformula pf : formula -> formula = - failwith "TODO formula_of_preformula" +let props : (string, prop) Hashtbl.t = Hashtbl.create 53 + +exception Formdef_exception of string + +(** val add_prop : string -> string list -> formula -> unit *) +let add_prop name idents formula = + if Hashtbl.mem props name then + raise (Formdef_exception name) + else + Hashtbl.add props name (idents, formula) + +let formula_of_preformula pf = + let rec step = function + | FTrue | FFalse as f -> f + | FAnd (f, g) -> FAnd (step f, step g) + | FOr (f, g) -> FOr (step f, step g) + | FImplies (f, g) -> FImplies (step f, step g) + | FModal(m, f) -> FModal (m, step f) + | FInvModal (m, f) -> FInvModal (m, step f) + | FVar v -> FVar v + | FMu (x, f) -> FMu (x, step f) + | FNu (x, f) -> FNu (x, step f) + | FProp (_, _) -> failwith "TODO formula_of_preformula" + in + Format.printf "Preformula received :\n%s@." @@ string_of_formula pf; + let res = step pf in + Format.printf "Result :\n%s@." @@ string_of_formula res; + res From a169aa1f6a48fd20b0d9289750d7ab6a74036cbb Mon Sep 17 00:00:00 2001 From: Pierrick Couderc Date: Sat, 12 Oct 2013 12:39:32 +0200 Subject: [PATCH 04/26] Added variable substitution for props Don't know if that will be useful however. --- src/Formula.ml | 57 ++++++++++++++++++++++++++++++++++++++++---------- 1 file changed, 46 insertions(+), 11 deletions(-) diff --git a/src/Formula.ml b/src/Formula.ml index b20f976..bea4c2e 100644 --- a/src/Formula.ml +++ b/src/Formula.ml @@ -74,26 +74,61 @@ type prop = string list * formula let props : (string, prop) Hashtbl.t = Hashtbl.create 53 exception Formdef_exception of string +exception Unbound_variable of string +exception Unbound_prop of string + +let rec verify_vars f idents = + match f with + | FVar v -> if not (List.mem v idents) then raise (Unbound_variable v) + | FAnd (f,g) | FOr (f,g) | FImplies (f,g) -> + verify_vars f idents; verify_vars g idents + | FModal (_, f) | FInvModal (_, f) -> verify_vars f idents + | FMu (x,f) | FNu (x,f) -> verify_vars f (x :: idents) + | FProp (_, l) -> List.iter (fun v -> verify_vars (FVar v) idents) l + | _ -> () (** val add_prop : string -> string list -> formula -> unit *) let add_prop name idents formula = if Hashtbl.mem props name then raise (Formdef_exception name) else - Hashtbl.add props name (idents, formula) + begin + verify_vars formula idents; + Hashtbl.add props name (idents, formula) + end + +let substitute f sub_list = + let rec step sl = function + | FVar v -> FVar (List.assoc v sl) + | FTrue | FFalse as f -> f + | FAnd (f, g) -> FAnd (step sl f, step sl g) + | FOr (f, g) -> FOr (step sl f, step sl g) + | FImplies (f, g) -> FImplies (step sl f, step sl g) + | FModal(m, f) -> FModal (m, step sl f) + | FInvModal (m, f) -> FInvModal (m, step sl f) + | FMu (x, f) -> FMu (x, step ((x, x)::sl) f) + | FNu (x, f) -> FNu (x, step ((x, x)::sl) f) + | _ -> assert false (* Technically, no Prop should remain *) + in + step sub_list f let formula_of_preformula pf = let rec step = function - | FTrue | FFalse as f -> f - | FAnd (f, g) -> FAnd (step f, step g) - | FOr (f, g) -> FOr (step f, step g) - | FImplies (f, g) -> FImplies (step f, step g) - | FModal(m, f) -> FModal (m, step f) - | FInvModal (m, f) -> FInvModal (m, step f) - | FVar v -> FVar v - | FMu (x, f) -> FMu (x, step f) - | FNu (x, f) -> FNu (x, step f) - | FProp (_, _) -> failwith "TODO formula_of_preformula" + | FTrue | FFalse as f -> f + | FAnd (f, g) -> FAnd (step f, step g) + | FOr (f, g) -> FOr (step f, step g) + | FImplies (f, g) -> FImplies (step f, step g) + | FModal(m, f) -> FModal (m, step f) + | FInvModal (m, f) -> FInvModal (m, step f) + | FVar v -> FVar v + | FMu (x, f) -> FMu (x, step f) + | FNu (x, f) -> FNu (x, step f) + | FProp (s, il) -> + if Hashtbl.mem props s then + let (vars, formula) = Hashtbl.find props s in + substitute formula @@ List.combine vars il + else + raise (Unbound_prop s) in Format.printf "Preformula received :\n%s@." @@ string_of_formula pf; let res = step pf in From e81292b7fce944fadd7c886dc3d6f3f034a5377b Mon Sep 17 00:00:00 2001 From: Pierrick Couderc Date: Sat, 12 Oct 2013 13:21:08 +0200 Subject: [PATCH 05/26] Added props with no arguments --- src/Control.ml | 2 +- src/Parser.mly | 94 ++++++++++++++++++++++++++------------------------ 2 files changed, 50 insertions(+), 46 deletions(-) diff --git a/src/Control.ml b/src/Control.ml index f1668b7..d7c8d35 100644 --- a/src/Control.ml +++ b/src/Control.ml @@ -313,7 +313,7 @@ let handle_prop n il f = (List.hd il) (List.tl il)) ^ ")" - else "()" (* Unreachable case *) + else "()" in Formula.string_of_formula f |> Format.printf "Prop : %s %s : %s@." n namelist; diff --git a/src/Parser.mly b/src/Parser.mly index 94e1a5d..6fd99de 100644 --- a/src/Parser.mly +++ b/src/Parser.mly @@ -10,12 +10,12 @@ | [] -> p | n::ns' -> PRes(n,(mkRes ns' p)) - let mkRename ns p = + let mkRename ns p = let rec ren = function | [] -> p | (old,value) :: ns' -> PRename(old,value,(ren ns')) in - ren (List.rev ns) + ren (List.rev ns) (* @@ -115,65 +115,65 @@ | INT { (string_of_int $1) } statement: - | definition + | definition { let defs = definitions_of_predefinition $1 in - List.iter Control.handle_definition defs + List.iter Control.handle_definition defs } - | CONSTDEF CONST EQUAL INT + | CONSTDEF CONST EQUAL INT { Control.handle_constdef $2 $4 } | TYPEDEF IDENT EQUAL LBRACKET minmax DOTDOT minmax RBRACKET { Control.handle_typedef_range $2 $5 $7 } | TYPEDEF IDENT EQUAL LACCOL list_of_names RACCOL { Control.handle_typedef_enum $2 $5 } - | NORM process + | NORM process { Control.handle_normalization (process_of_preprocess $2) } - | NORM error + | NORM error { raise (Fatal_Parse_Error "missing process to normalize") } | STRUCT process EQEQ process - { Control.handle_struct_congr + { Control.handle_struct_congr (process_of_preprocess $2) (process_of_preprocess $4) } | STRUCT process error { raise (Fatal_Parse_Error "missing '==' for structural congruence") } | STRUCT process EQEQ error { raise (Fatal_Parse_Error "missing process after '==' for structural congruence") } - | STRUCT error + | STRUCT error {raise (Fatal_Parse_Error "missing process before '==' for structural congruence") } - | BISIM IN process TILD process - { Control.handle_is_bisim - (process_of_preprocess $3) + | BISIM IN process TILD process + { Control.handle_is_bisim + (process_of_preprocess $3) (process_of_preprocess $5) } | BISIM IN process error { raise (Fatal_Parse_Error "missing '~' for strong bisimilarity") } | BISIM IN process TILD error { raise (Fatal_Parse_Error "missing process after '~' for strong bisimilarity") } | BISIM process TILD process - { Control.handle_bisim + { Control.handle_bisim (process_of_preprocess $2) (process_of_preprocess $4) } | BISIM process error { raise (Fatal_Parse_Error "missing '~' for strong bisimilarity") } | BISIM process TILD error { raise (Fatal_Parse_Error "missing process after '~' for strong bisimilarity") } - | BISIM error + | BISIM error { raise (Fatal_Parse_Error "missing '?' or process before '~' for strong bisimilarity") } - | FBISIM IN process TILD process - { Control.handle_is_fbisim + | FBISIM IN process TILD process + { Control.handle_is_fbisim (process_of_preprocess $3) (process_of_preprocess $5) } | FBISIM IN process error { raise (Fatal_Parse_Error "missing '~' for strong bisimilarity") } | FBISIM IN process TILD error { raise (Fatal_Parse_Error "missing process after '~' for strong bisimilarity") } - | FBISIM error + | FBISIM error { raise (Fatal_Parse_Error "missing '?' or process before '~' for strong bisimilarity") } - | WBISIM IN process TILD TILD process - { Control.handle_is_wbisim - (process_of_preprocess $3) + | WBISIM IN process TILD TILD process + { Control.handle_is_wbisim + (process_of_preprocess $3) (process_of_preprocess $6) } | WBISIM IN process error { raise (Fatal_Parse_Error "missing '~~' for weak bisimilarity") } @@ -182,9 +182,9 @@ | WBISIM IN process TILD TILD error { raise (Fatal_Parse_Error "missing process after '~~' for weak bisimilarity") } - | WBISIM process TILD TILD process - { Control.handle_wbisim - (process_of_preprocess $2) + | WBISIM process TILD TILD process + { Control.handle_wbisim + (process_of_preprocess $2) (process_of_preprocess $5) } | WBISIM process error { raise (Fatal_Parse_Error "missing '~~' for weak bisimilarity") } @@ -192,13 +192,13 @@ { raise (Fatal_Parse_Error "missing '~' for weak bisimilarity") } | WBISIM process TILD TILD error { raise (Fatal_Parse_Error "missing process after '~~' for weak bisimilarity") } - - | WBISIM error + + | WBISIM error { raise (Fatal_Parse_Error "missing '?' or process before '~~' for weak bisimilarity") } - | WFBISIM IN process TILD TILD process - { Control.handle_is_fwbisim - (process_of_preprocess $3) + | WFBISIM IN process TILD TILD process + { Control.handle_is_fwbisim + (process_of_preprocess $3) (process_of_preprocess $6) } | WFBISIM IN process error { raise (Fatal_Parse_Error "missing '~~' for weak bisimilarity") } @@ -210,46 +210,49 @@ | WDERIV process { Control.handle_wderiv (process_of_preprocess $2) } | WDERIV error - { raise (Fatal_Parse_Error "missing process to derivate") } + { raise (Fatal_Parse_Error "missing process to derivate") } | TDERIV process { Control.handle_tderiv (process_of_preprocess $2) } | TDERIV error - { raise (Fatal_Parse_Error "missing process to derivate") } + { raise (Fatal_Parse_Error "missing process to derivate") } | WLTS process { Control.handle_wlts (process_of_preprocess $2) } | WLTS error - { raise (Fatal_Parse_Error "missing process for LTS") } + { raise (Fatal_Parse_Error "missing process for LTS") } | WMINI process { Control.handle_wminimization (process_of_preprocess $2) } | WMINI error - {raise (Fatal_Parse_Error "missing process for minimization") } - + {raise (Fatal_Parse_Error "missing process for minimization") } + | DERIV process { Control.handle_deriv (process_of_preprocess $2) } | DERIV error - { raise (Fatal_Parse_Error "missing process to derivate") } + { raise (Fatal_Parse_Error "missing process to derivate") } | LTS process { Control.handle_lts (process_of_preprocess $2) } | LTS error - { raise (Fatal_Parse_Error "missing process for LTS") } + { raise (Fatal_Parse_Error "missing process for LTS") } | MINI process { Control.handle_minimization (process_of_preprocess $2) } | MINI error - {raise (Fatal_Parse_Error "missing process for minimization") } + {raise (Fatal_Parse_Error "missing process for minimization") } | FREE process { Control.handle_free (process_of_preprocess $2) } | FREE error - { raise (Fatal_Parse_Error "missing process for free names") } + { raise (Fatal_Parse_Error "missing process for free names") } | BOUND process { Control.handle_bound (process_of_preprocess $2) } | BOUND error - { raise (Fatal_Parse_Error "missing process for bound names") } + { raise (Fatal_Parse_Error "missing process for bound names") } | NAMES process { Control.handle_names (process_of_preprocess $2) } | NAMES error - { raise (Fatal_Parse_Error "missing process for names") } + { raise (Fatal_Parse_Error "missing process for names") } + + | PROP IDENT LPAREN RPAREN EQUAL formula + { Control.handle_prop $2 [] (formula_of_preformula $6) } | PROP IDENT LPAREN list_of_names RPAREN EQUAL formula { Control.handle_prop $2 $4 (formula_of_preformula $7) } @@ -266,20 +269,20 @@ { Control.handle_quit () } process: - | INT - { if $1 = 0 then PSilent + | INT + { if $1 = 0 then PSilent else raise (Fatal_Parse_Error "Only 0 can be used as Silent process") } - | END + | END { PSilent } | prefix { PPrefix($1,PSilent) } | prefix COMMA process { PPrefix($1,$3) } | prefix COMMA error { raise (Fatal_Parse_Error "right-hand process missing after prefix") } | prefix error - { raise (Fatal_Parse_Error "missing ',' after prefix") } + { raise (Fatal_Parse_Error "missing ',' after prefix") } | process PAR process { PPar($1,$3) } | process PAR error - { raise (Fatal_Parse_Error "right-hand process missing in parallel") } + { raise (Fatal_Parse_Error "right-hand process missing in parallel") } | process PLUS process { PSum($1,$3) } | process PLUS error { raise (Fatal_Parse_Error "right-hand process missing in sum") } @@ -302,7 +305,7 @@ list_of_prefixes: | prefix { [$1] } - | prefix COMMA list_of_prefixes { $1::$3 } + | prefix COMMA list_of_prefixes { $1::$3 } rename : | LBRACKET list_of_renames RBRACKET { $2 } @@ -367,6 +370,7 @@ | TILD modality formula { FInvModal($2,$3) } | MU LPAREN IDENT RPAREN DOT formula { FMu ($3,$6) } | NU LPAREN IDENT RPAREN DOT formula { FNu ($3,$6) } + | IDENT LPAREN RPAREN { FProp($1, []) } | IDENT LPAREN list_of_names RPAREN { FProp($1,$3) } | IDENT { FVar($1) } From 3061bf945c37a1ed250c0146916196942f4dca6a Mon Sep 17 00:00:00 2001 From: Pierrick Couderc Date: Sat, 12 Oct 2013 14:15:25 +0200 Subject: [PATCH 06/26] First draft for handle_check_local However, might be completely wrong, and misses a lot of cases since only the trivial one are given. --- src/Control.ml | 16 +++++++++++++++- 1 file changed, 15 insertions(+), 1 deletion(-) diff --git a/src/Control.ml b/src/Control.ml index d7c8d35..ba25469 100644 --- a/src/Control.ml +++ b/src/Control.ml @@ -319,6 +319,20 @@ let handle_prop n il f = Format.printf "Prop : %s %s : %s@." n namelist; Formula.add_prop n il f -let handle_check_local _ _ = failwith "TODO: handle_check_local" +let handle_check_local form proc = + let open Formula in + let rec step proc = function + | FTrue -> true + | FFalse -> false + | FAnd (f, g) -> step proc f && step proc g + | FOr (f, g) -> step proc f || step proc g + | FImplies (f, g) -> not (step proc f) || step proc g + | _ -> assert false + in + let res = step proc form in + if res then + Format.printf "The processor given matches the model@." + else + Format.printf "Doesn't match, here is why : @." let handle_check_global _ _ = failwith "TODO: handle_check_global" From 42ecfe1eb3bc6096d6a8e7176854bd49e71501f9 Mon Sep 17 00:00:00 2001 From: Pierrick Couderc Date: Sat, 12 Oct 2013 16:31:45 +0200 Subject: [PATCH 07/26] Vars from formulas aren't bound by props' argument Well, I think at least... --- src/Formula.ml | 63 +++++++++++++++++++++++++------------------------- 1 file changed, 32 insertions(+), 31 deletions(-) diff --git a/src/Formula.ml b/src/Formula.ml index bea4c2e..e0d5ec1 100644 --- a/src/Formula.ml +++ b/src/Formula.ml @@ -74,18 +74,18 @@ type prop = string list * formula let props : (string, prop) Hashtbl.t = Hashtbl.create 53 exception Formdef_exception of string -exception Unbound_variable of string +(* exception Unbound_variable of string *) exception Unbound_prop of string -let rec verify_vars f idents = - match f with - | FVar v -> if not (List.mem v idents) then raise (Unbound_variable v) - | FAnd (f,g) | FOr (f,g) | FImplies (f,g) -> - verify_vars f idents; verify_vars g idents - | FModal (_, f) | FInvModal (_, f) -> verify_vars f idents - | FMu (x,f) | FNu (x,f) -> verify_vars f (x :: idents) - | FProp (_, l) -> List.iter (fun v -> verify_vars (FVar v) idents) l - | _ -> () +(* let rec verify_vars f idents = *) +(* match f with *) +(* | FVar v -> if not (List.mem v idents) then raise (Unbound_variable v) *) +(* | FAnd (f,g) | FOr (f,g) | FImplies (f,g) -> *) +(* verify_vars f idents; verify_vars g idents *) +(* | FModal (_, f) | FInvModal (_, f) -> verify_vars f idents *) +(* | FMu (x,f) | FNu (x,f) -> verify_vars f (x :: idents) *) +(* | FProp (_, l) -> List.iter (fun v -> verify_vars (FVar v) idents) l *) +(* | _ -> () *) (** val add_prop : string -> string list -> formula -> unit *) let add_prop name idents formula = @@ -93,24 +93,25 @@ let add_prop name idents formula = raise (Formdef_exception name) else begin - verify_vars formula idents; + (* verify_vars formula idents; *) Hashtbl.add props name (idents, formula) end -let substitute f sub_list = - let rec step sl = function - | FVar v -> FVar (List.assoc v sl) - | FTrue | FFalse as f -> f - | FAnd (f, g) -> FAnd (step sl f, step sl g) - | FOr (f, g) -> FOr (step sl f, step sl g) - | FImplies (f, g) -> FImplies (step sl f, step sl g) - | FModal(m, f) -> FModal (m, step sl f) - | FInvModal (m, f) -> FInvModal (m, step sl f) - | FMu (x, f) -> FMu (x, step ((x, x)::sl) f) - | FNu (x, f) -> FNu (x, step ((x, x)::sl) f) - | _ -> assert false (* Technically, no Prop should remain *) - in - step sub_list f +(** Bad understanding : vars aren't bound by props argument *) +(* let substitute f sub_list = *) +(* let rec step sl = function *) +(* | FVar v -> FVar (List.assoc v sl) *) +(* | FTrue | FFalse as f -> f *) +(* | FAnd (f, g) -> FAnd (step sl f, step sl g) *) +(* | FOr (f, g) -> FOr (step sl f, step sl g) *) +(* | FImplies (f, g) -> FImplies (step sl f, step sl g) *) +(* | FModal(m, f) -> FModal (m, step sl f) *) +(* | FInvModal (m, f) -> FInvModal (m, step sl f) *) +(* | FMu (x, f) -> FMu (x, step ((x, x)::sl) f) *) +(* | FNu (x, f) -> FNu (x, step ((x, x)::sl) f) *) +(* | _ -> assert false (\* Technically, no Prop should remain ? *\) *) +(* in *) +(* step sub_list f *) let formula_of_preformula pf = let rec step = function @@ -123,12 +124,12 @@ let formula_of_preformula pf = | FVar v -> FVar v | FMu (x, f) -> FMu (x, step f) | FNu (x, f) -> FNu (x, step f) - | FProp (s, il) -> - if Hashtbl.mem props s then - let (vars, formula) = Hashtbl.find props s in - substitute formula @@ List.combine vars il - else - raise (Unbound_prop s) + | FProp (_, _) -> failwith "Something to do here ?" + (* if Hashtbl.mem props s then *) + (* let (vars, formula) = Hashtbl.find props s in *) + (* substitute formula @@ List.combine vars il *) + (* else *) + (* raise (Unbound_prop s) *) in Format.printf "Preformula received :\n%s@." @@ string_of_formula pf; let res = step pf in From a95916db59cc7edafdfb5cceedbc1ae3de6c2992 Mon Sep 17 00:00:00 2001 From: Pierrick Couderc Date: Sat, 12 Oct 2013 17:29:48 +0200 Subject: [PATCH 08/26] Revert previous commit Mistaken vars and modalities --- src/Formula.ml | 62 +++++++++++++++++++++++++------------------------- 1 file changed, 31 insertions(+), 31 deletions(-) diff --git a/src/Formula.ml b/src/Formula.ml index e0d5ec1..8b9e470 100644 --- a/src/Formula.ml +++ b/src/Formula.ml @@ -74,18 +74,18 @@ type prop = string list * formula let props : (string, prop) Hashtbl.t = Hashtbl.create 53 exception Formdef_exception of string -(* exception Unbound_variable of string *) +exception Unbound_variable of string exception Unbound_prop of string -(* let rec verify_vars f idents = *) -(* match f with *) -(* | FVar v -> if not (List.mem v idents) then raise (Unbound_variable v) *) -(* | FAnd (f,g) | FOr (f,g) | FImplies (f,g) -> *) -(* verify_vars f idents; verify_vars g idents *) -(* | FModal (_, f) | FInvModal (_, f) -> verify_vars f idents *) -(* | FMu (x,f) | FNu (x,f) -> verify_vars f (x :: idents) *) -(* | FProp (_, l) -> List.iter (fun v -> verify_vars (FVar v) idents) l *) -(* | _ -> () *) +let rec verify_vars f idents = + match f with + | FVar v -> if not (List.mem v idents) then raise (Unbound_variable v) + | FAnd (f,g) | FOr (f,g) | FImplies (f,g) -> + verify_vars f idents; verify_vars g idents + | FModal (_, f) | FInvModal (_, f) -> verify_vars f idents + | FMu (x,f) | FNu (x,f) -> verify_vars f (x :: idents) + | FProp (_, l) -> List.iter (fun v -> verify_vars (FVar v) idents) l + | _ -> () (** val add_prop : string -> string list -> formula -> unit *) let add_prop name idents formula = @@ -93,25 +93,25 @@ let add_prop name idents formula = raise (Formdef_exception name) else begin - (* verify_vars formula idents; *) + verify_vars formula idents; Hashtbl.add props name (idents, formula) end (** Bad understanding : vars aren't bound by props argument *) -(* let substitute f sub_list = *) -(* let rec step sl = function *) -(* | FVar v -> FVar (List.assoc v sl) *) -(* | FTrue | FFalse as f -> f *) -(* | FAnd (f, g) -> FAnd (step sl f, step sl g) *) -(* | FOr (f, g) -> FOr (step sl f, step sl g) *) -(* | FImplies (f, g) -> FImplies (step sl f, step sl g) *) -(* | FModal(m, f) -> FModal (m, step sl f) *) -(* | FInvModal (m, f) -> FInvModal (m, step sl f) *) -(* | FMu (x, f) -> FMu (x, step ((x, x)::sl) f) *) -(* | FNu (x, f) -> FNu (x, step ((x, x)::sl) f) *) -(* | _ -> assert false (\* Technically, no Prop should remain ? *\) *) -(* in *) -(* step sub_list f *) +let substitute f sub_list = + let rec step sl = function + | FVar v -> FVar (List.assoc v sl) + | FTrue | FFalse as f -> f + | FAnd (f, g) -> FAnd (step sl f, step sl g) + | FOr (f, g) -> FOr (step sl f, step sl g) + | FImplies (f, g) -> FImplies (step sl f, step sl g) + | FModal(m, f) -> FModal (m, step sl f) + | FInvModal (m, f) -> FInvModal (m, step sl f) + | FMu (x, f) -> FMu (x, step ((x, x)::sl) f) + | FNu (x, f) -> FNu (x, step ((x, x)::sl) f) + | _ -> assert false (* Technically, no Prop should remain ? *) + in + step sub_list f let formula_of_preformula pf = let rec step = function @@ -124,12 +124,12 @@ let formula_of_preformula pf = | FVar v -> FVar v | FMu (x, f) -> FMu (x, step f) | FNu (x, f) -> FNu (x, step f) - | FProp (_, _) -> failwith "Something to do here ?" - (* if Hashtbl.mem props s then *) - (* let (vars, formula) = Hashtbl.find props s in *) - (* substitute formula @@ List.combine vars il *) - (* else *) - (* raise (Unbound_prop s) *) + | FProp (s, il) -> + if Hashtbl.mem props s then + let (vars, formula) = Hashtbl.find props s in + substitute formula @@ List.combine vars il + else + raise (Unbound_prop s) in Format.printf "Preformula received :\n%s@." @@ string_of_formula pf; let res = step pf in From 6cb38a34cf1be2f45c145254549ce93d4b3e5d30 Mon Sep 17 00:00:00 2001 From: Pierrick Couderc Date: Mon, 14 Oct 2013 17:31:19 +0200 Subject: [PATCH 09/26] Added box and diamond checking (first draft) --- src/Control.ml | 105 ++++++++++++++++++++++++++++++++++++++++++++++++- src/Formula.ml | 17 +++++++- 2 files changed, 119 insertions(+), 3 deletions(-) diff --git a/src/Control.ml b/src/Control.ml index ba25469..c6b7a5c 100644 --- a/src/Control.ml +++ b/src/Control.ml @@ -5,6 +5,7 @@ open Syntax open Normalize open Semop open Minim +open Formula let help_me = "\n\ Command summary:\n\ @@ -299,10 +300,75 @@ let handle_wderiv p = common_deriv (weak_derivatives false) printPfixMap "wderiv let handle_tderiv p = common_deriv (weak_derivatives true) printPfixMap "tderiv" "tau derivatives" p + +(*** Mu-Calculus part *) + type prop = (string * string list * Formula.formula) +let compute_derivation p = + let np = normalize p in + derivatives global_definition_map np + +exception Impossible_transition + +let compute_modality modl tr = + + let get_matching_derivations_named act tr acc = + TSet.fold + (fun t acc -> + Format.printf "%s@." @@ string_of_derivative t; + let _, pre, _ = t in + match act, pre with + | FIn s, T_In n | FOut s, T_Out n -> + if s = n then TSet.add t acc else acc + | FTau, T_Tau -> TSet.add t acc + | _, _ -> acc) + tr + acc + in + let get_matching_derivations modl tr = + TSet.fold + (fun t acc -> + let _, pre, _ = t in + match modl, pre with + | FInPossibly, T_In _ | FOutPossibly, T_Out _ -> + Format.printf "Matching@."; TSet.add t acc + | FAnyPossibly, T_Tau -> TSet.add t acc + | _, _ -> acc) + tr + TSet.empty + in + + let get_derivations_necessity modl tr = + TSet.fold + (fun t acc -> + let _, pre, _ = t in + match modl, pre with + | FInNecessity, T_In _ | FOutNecessity, T_Out _ -> + Format.printf "Matching@."; TSet.add t acc + | FAnyNecessity, T_Tau -> TSet.add t acc + | _, _ -> raise Impossible_transition) + tr + TSet.empty + in + + match modl with + | FPossibly acts | FNecessity acts -> + List.fold_left + (fun acc a -> + + Format.printf "%s@." @@ string_of_modality modl; + get_matching_derivations_named (fprefix_of_preprefix a) tr acc) + TSet.empty + acts + | FOutPossibly | FInPossibly | FAnyPossibly -> + Format.printf "%s@." @@ string_of_modality modl; + get_matching_derivations modl tr + | FOutNecessity | FInNecessity | FAnyNecessity -> + get_derivations_necessity modl tr + | _ -> failwith "Only diamond implemented" let handle_prop n il f = let namelist = @@ -320,19 +386,54 @@ let handle_prop n il f = Formula.add_prop n il f let handle_check_local form proc = - let open Formula in let rec step proc = function | FTrue -> true | FFalse -> false | FAnd (f, g) -> step proc f && step proc g | FOr (f, g) -> step proc f || step proc g | FImplies (f, g) -> not (step proc f) || step proc g + | FModal (m, f) when diamond m -> + let d = compute_derivation proc in + let res = compute_modality m d in + TSet.fold (fun t _ -> print_endline @@ string_of_derivative t) res (); + if TSet.is_empty res then false (* meaning there is no transition *) + else + TSet.fold + (fun (_, _, p') acc -> + if acc then acc (* no need to test the transition if one is + true *) + else step (denormalize p') f) + res + false + | FModal (m, f) -> + Format.printf "Box case@."; + (try + let d = compute_derivation proc in + let res = compute_modality m d in + TSet.fold (fun t _ -> print_endline @@ string_of_derivative t) res (); + if TSet.is_empty res then false (* meaning there is no transition *) + else if not (TSet.equal d res) then false (* One transition missing at + least *) + else + begin + Format.printf "Okay, let's test each transition now@."; + TSet.fold + (fun (_, _, p') acc -> + if not acc then acc (* no need to test the transition if one is + false *) + else step (denormalize p') f) + res + true + end + + with + _ -> false) | _ -> assert false in let res = step proc form in if res then Format.printf "The processor given matches the model@." else - Format.printf "Doesn't match, here is why : @." + Format.printf "Doesn't match, here is why : @." let handle_check_global _ _ = failwith "TODO: handle_check_global" diff --git a/src/Formula.ml b/src/Formula.ml index 8b9e470..ac42dfe 100644 --- a/src/Formula.ml +++ b/src/Formula.ml @@ -43,6 +43,22 @@ let string_of_modality : modality -> string = function | FWInNecessity -> "[[?]]" | FWAnyNecessity -> "[[.]]" +let diamond = function + | FPossibly _ -> true + | FOutPossibly | FInPossibly | FAnyPossibly -> true + | _ -> false + +type fprefix = +| FIn of string +| FOut of string +| FTau + +let fprefix_of_preprefix = function + | PIn (PName n) -> FIn n + | POut (PName n) -> FOut n + | PTau -> FTau + | _ as pr -> failwith (Format.sprintf "Received : %s@." @@ string_of_preprefix pr) + type formula = | FTrue | FFalse @@ -97,7 +113,6 @@ let add_prop name idents formula = Hashtbl.add props name (idents, formula) end -(** Bad understanding : vars aren't bound by props argument *) let substitute f sub_list = let rec step sl = function | FVar v -> FVar (List.assoc v sl) From 2ec99703c5035649c3adb3e419cbabaee8ac097c Mon Sep 17 00:00:00 2001 From: Pierrick Couderc Date: Thu, 17 Oct 2013 16:15:09 +0200 Subject: [PATCH 10/26] Refactoring of the modality type More useful this way, easier to decompose and match --- src/Control.ml | 154 ++++----------------------- src/Formula.ml | 279 ++++++++++++++++++++++++++++++++++++++++++------- src/Parser.mly | 46 ++++---- 3 files changed, 282 insertions(+), 197 deletions(-) diff --git a/src/Control.ml b/src/Control.ml index c6b7a5c..c5ef9ad 100644 --- a/src/Control.ml +++ b/src/Control.ml @@ -1,11 +1,10 @@ open Printf - +open Global open Utils open Syntax open Normalize open Semop open Minim -open Formula let help_me = "\n\ Command summary:\n\ @@ -136,8 +135,6 @@ let handle_struct_congr p q = else printf "the processes are *not* structurally congruent\n%!") ; printf "(elapsed time=%fs)\n%!" time -let global_definition_map = Hashtbl.create 64 - let common_deriv f_deriv f_print str str2 p = if !script_mode then printf "> %s %s\n%!" str (string_of_process p) ; @@ -303,137 +300,22 @@ let handle_tderiv p = common_deriv (weak_derivatives true) printPfixMap "tderiv" (*** Mu-Calculus part *) -type prop = - (string * string list * Formula.formula) - -let compute_derivation p = - let np = normalize p in - derivatives global_definition_map np - -exception Impossible_transition - -let compute_modality modl tr = - - let get_matching_derivations_named act tr acc = - TSet.fold - (fun t acc -> - Format.printf "%s@." @@ string_of_derivative t; - let _, pre, _ = t in - match act, pre with - | FIn s, T_In n | FOut s, T_Out n -> - if s = n then TSet.add t acc else acc - | FTau, T_Tau -> TSet.add t acc - | _, _ -> acc) - tr - acc - in - - let get_matching_derivations modl tr = - TSet.fold - (fun t acc -> - let _, pre, _ = t in - match modl, pre with - | FInPossibly, T_In _ | FOutPossibly, T_Out _ -> - Format.printf "Matching@."; TSet.add t acc - | FAnyPossibly, T_Tau -> TSet.add t acc - | _, _ -> acc) - tr - TSet.empty - in - - let get_derivations_necessity modl tr = - TSet.fold - (fun t acc -> - let _, pre, _ = t in - match modl, pre with - | FInNecessity, T_In _ | FOutNecessity, T_Out _ -> - Format.printf "Matching@."; TSet.add t acc - | FAnyNecessity, T_Tau -> TSet.add t acc - | _, _ -> raise Impossible_transition) - tr - TSet.empty - in - - match modl with - | FPossibly acts | FNecessity acts -> - List.fold_left - (fun acc a -> - - Format.printf "%s@." @@ string_of_modality modl; - get_matching_derivations_named (fprefix_of_preprefix a) tr acc) - TSet.empty - acts - | FOutPossibly | FInPossibly | FAnyPossibly -> - Format.printf "%s@." @@ string_of_modality modl; - get_matching_derivations modl tr - | FOutNecessity | FInNecessity | FAnyNecessity -> - get_derivations_necessity modl tr - | _ -> failwith "Only diamond implemented" - -let handle_prop n il f = - let namelist = - if List.length il <> 0 then - let il = List.rev il in - "(" ^ (List.fold_left - (fun n acc -> acc ^ ", " ^ n) - (List.hd il) - (List.tl il)) - ^ ")" - else "()" - in - Formula.string_of_formula f |> - Format.printf "Prop : %s %s : %s@." n namelist; - Formula.add_prop n il f - -let handle_check_local form proc = - let rec step proc = function - | FTrue -> true - | FFalse -> false - | FAnd (f, g) -> step proc f && step proc g - | FOr (f, g) -> step proc f || step proc g - | FImplies (f, g) -> not (step proc f) || step proc g - | FModal (m, f) when diamond m -> - let d = compute_derivation proc in - let res = compute_modality m d in - TSet.fold (fun t _ -> print_endline @@ string_of_derivative t) res (); - if TSet.is_empty res then false (* meaning there is no transition *) - else - TSet.fold - (fun (_, _, p') acc -> - if acc then acc (* no need to test the transition if one is - true *) - else step (denormalize p') f) - res - false - | FModal (m, f) -> - Format.printf "Box case@."; - (try - let d = compute_derivation proc in - let res = compute_modality m d in - TSet.fold (fun t _ -> print_endline @@ string_of_derivative t) res (); - if TSet.is_empty res then false (* meaning there is no transition *) - else if not (TSet.equal d res) then false (* One transition missing at - least *) - else - begin - Format.printf "Okay, let's test each transition now@."; - TSet.fold - (fun (_, _, p') acc -> - if not acc then acc (* no need to test the transition if one is - false *) - else step (denormalize p') f) - res - true - end - - with - _ -> false) - | _ -> assert false - in - let res = step proc form in - if res then - Format.printf "The processor given matches the model@." - else - Format.printf "Doesn't match, here is why : @." +let handle_prop = + (* let namelist = *) + (* if List.length il <> 0 then *) + (* let il = List.rev il in *) + (* "(" ^ (List.fold_left *) + (* (fun n acc -> acc ^ ", " ^ n) *) + (* (List.hd il) *) + (* (List.tl il)) *) + (* ^ ")" *) + (* else "()" *) + (* in *) + (* Formula.string_of_formula f |> *) + (* Format.printf "Prop : %s %s : %s@." n namelist; *) + Formula.add_prop + +let handle_check_local = + Formula.handle_check_local let handle_check_global _ _ = failwith "TODO: handle_check_global" diff --git a/src/Formula.ml b/src/Formula.ml index ac42dfe..a0b22c2 100644 --- a/src/Formula.ml +++ b/src/Formula.ml @@ -4,61 +4,97 @@ open Printf open Presyntax open Utils +open Global +open Normalize +open Semop (* mu-calculus formulae *) -type modality = - | FPossibly of preprefix list - | FOutPossibly - | FInPossibly - | FAnyPossibly - | FWPossibly of preprefix list - | FWOutPossibly - | FWInPossibly - | FWAnyPossibly - | FNecessity of preprefix list - | FOutNecessity - | FInNecessity - | FAnyNecessity - | FWNecessity of preprefix list - | FWOutNecessity - | FWInNecessity - | FWAnyNecessity - -let string_of_modality : modality -> string = function - | FPossibly(acts) -> string_of_collection "<" ">" "," string_of_preprefix acts - | FOutPossibly -> "" - | FInPossibly -> "" - | FAnyPossibly -> "<.>" - | FWPossibly(acts) -> string_of_collection "<<" ">>" "," string_of_preprefix acts - | FWOutPossibly -> "<>" - | FWInPossibly -> "<>" - | FWAnyPossibly -> "<<.>>" - | FNecessity(acts) -> string_of_collection "[" "]" "," string_of_preprefix acts - | FOutNecessity -> "[!]" - | FInNecessity -> "[?]" - | FAnyNecessity -> "[.]" - | FWNecessity(acts) -> string_of_collection "[[" "]]" "," string_of_preprefix acts - | FWOutNecessity -> "[[!]]" - | FWInNecessity -> "[[?]]" - | FWAnyNecessity -> "[[.]]" +(* type modality = *) +(* | FPossibly of preprefix list *) +(* | FOutPossibly *) +(* | FInPossibly *) +(* | FAnyPossibly *) +(* | FWPossibly of preprefix list *) +(* | FWOutPossibly *) +(* | FWInPossibly *) +(* | FWAnyPossibly *) +(* | FNecessity of preprefix list *) +(* | FOutNecessity *) +(* | FInNecessity *) +(* | FAnyNecessity *) +(* | FWNecessity of preprefix list *) +(* | FWOutNecessity *) +(* | FWInNecessity *) +(* | FWAnyNecessity *) -let diamond = function - | FPossibly _ -> true - | FOutPossibly | FInPossibly | FAnyPossibly -> true - | _ -> false type fprefix = | FIn of string +| FInVar of string | FOut of string +| FOutVar of string | FTau let fprefix_of_preprefix = function | PIn (PName n) -> FIn n | POut (PName n) -> FOut n + | PIn (PVar n) -> FInVar n + | POut (PVar n) -> FOutVar n | PTau -> FTau | _ as pr -> failwith (Format.sprintf "Received : %s@." @@ string_of_preprefix pr) +let string_of_fprefix = function + | FIn n | FInVar n -> n ^ "?" + | FOut n | FOutVar n -> n ^ "!" + | FTau -> "tau" + +let parse_preprefix_list = + List.map fprefix_of_preprefix + +type strongness = Strong | Weak +type modal = Possibly | Necessity +type io = + In | Out | Any | Prefix of fprefix list + +type modality = strongness * modal * io + +let string_of_modality (s, m, io) = + let io = match io with + | In -> "!" + | Out -> "?" + | Any -> "." + | Prefix pl -> List.fold_left + (fun acc p -> acc ^ "," ^ (string_of_fprefix p)) + (string_of_fprefix (List.hd pl)) + (List.tl pl) + in + match s, m with + | Strong, Possibly -> Format.sprintf "<%s>" io + | Strong, Necessity -> Format.sprintf "[%s]" io + | Weak, Possibly -> Format.sprintf "<<%s>>" io + | Weak, Necessity -> Format.sprintf "[[%s]]" io + (* | Strong, Possibly, Prefix acts -> string_of_collection "<" ">" "," string_of_preprefix acts *) + (* | -> "" *) + (* | FInPossibly -> "" *) + (* | FAnyPossibly -> "<.>" *) + (* | FWPossibly(acts) -> string_of_collection "<<" ">>" "," string_of_preprefix acts *) + (* | FWOutPossibly -> "<>" *) + (* | FWInPossibly -> "<>" *) + (* | FWAnyPossibly -> "<<.>>" *) + (* | FNecessity(acts) -> string_of_collection "[" "]" "," string_of_preprefix acts *) + (* | FOutNecessity -> "[!]" *) + (* | FInNecessity -> "[?]" *) + (* | FAnyNecessity -> "[.]" *) + (* | FWNecessity(acts) -> string_of_collection "[[" "]]" "," string_of_preprefix acts *) + (* | FWOutNecessity -> "[[!]]" *) + (* | FWInNecessity -> "[[?]]" *) + (* | FWAnyNecessity -> "[[.]]" *) + +let diamond = function + | _, Possibly, _ -> true + | _, _, _ -> false + type formula = | FTrue | FFalse @@ -71,6 +107,7 @@ type formula = | FVar of string | FMu of string * formula | FNu of string * formula + | FNot of formula (* considered only internaly *) let rec string_of_formula : formula -> string = function | FTrue -> "True" @@ -84,6 +121,7 @@ let rec string_of_formula : formula -> string = function | FVar(var) -> var | FMu(x,f) -> sprintf "Mu(%s).%s" x (string_of_formula f) | FNu(x,f) -> sprintf "Nu(%s).%s" x (string_of_formula f) + | FNot f -> sprintf "~%s" @@ string_of_formula f type prop = string list * formula @@ -128,7 +166,7 @@ let substitute f sub_list = in step sub_list f -let formula_of_preformula pf = +let substitute_prop pf = let rec step = function | FTrue | FFalse as f -> f | FAnd (f, g) -> FAnd (step f, step g) @@ -139,6 +177,7 @@ let formula_of_preformula pf = | FVar v -> FVar v | FMu (x, f) -> FMu (x, step f) | FNu (x, f) -> FNu (x, step f) + | FNot f -> FNot (step f) | FProp (s, il) -> if Hashtbl.mem props s then let (vars, formula) = Hashtbl.find props s in @@ -150,3 +189,163 @@ let formula_of_preformula pf = let res = step pf in Format.printf "Result :\n%s@." @@ string_of_formula res; res + + +let formula_of_preformula = substitute_prop + (* let rename_modality = assert false (\* function *\) *) + (* (\* | FPossibility pl -> *\) *) + (* in *) + (* let sub = function *) + (* | FModal (m, f) -> *) + + (* let rename m = *) + (* match fprefix_of_preprefix m with *) + (* | FInVar n -> PIn (PName (n ^ "_" ^ value)) *) + (* | FOutVar n -> POut (PName (n ^ "_" ^ value)) *) + (* | _ -> m *) + (* in *) + (* FModal (m, sub value f) *) + (* | FInvModal (m, f) -> *) + (* let m = *) + (* match fprefix_of_preprefix m with *) + (* | FInVar n -> PIn (PName (n ^ "_" ^ value)) *) + (* | FOutVar n -> POut (PName (n ^ "_" ^ value)) *) + (* | _ -> m *) + (* in *) + (* FInvModal (m, sub value f) *) + (* | FTrue | FFalse as f -> f *) + (* | FAnd (f, g) -> FAnd (sub value f, sub value g) *) + (* | FOr (f, g) -> FOr (sub value f, sub value g) *) + (* | FImplies (f, g) -> FImplies (sub value f, sub value g) *) + (* | FModal(m, f) -> FModal (m, sub value f) *) + (* | FInvModal (m, f) -> FInvModal (m, sub value f) *) + (* | FVar v -> FVar v *) + (* | FMu (x, f) -> FMu (x, sub value f) *) + (* | FNu (x, f) -> FNu (x, sub value f) *) + (* in *) + (* let rec step = function *) + (* | FTrue | FFalse as f -> f *) + (* | FAnd (f, g) -> FAnd (step f, step g) *) + (* | FOr (f, g) -> FOr (step f, step g) *) + (* | FImplies (f, g) -> FImplies (step f, step g) *) + (* | FModal(m, f) -> *) + (* let v = *) + (* if SMap.mem const_name !env_const then *) + (* SMap.find var *) + (* else *) + (* raise (Constdef_Exception const_name) *) + + (* FModal (m, step f) *) + (* | FInvModal (m, f) -> FInvModal (m, step f) *) + (* | FVar v -> FVar v *) + (* | FMu (x, f) -> FMu (x, step f) *) + (* | FNu (x, f) -> FNu (x, step f) *) + (* | FProp (s, il) -> *) + (* if Hashtbl.mem props s then *) + (* let (vars, formula) = Hashtbl.find props s in *) + (* substitute formula @@ List.combine vars il *) + (* else *) + (* raise (Unbound_prop s) *) + (* in *) + (* Format.printf "Preformula received :\n%s@." @@ string_of_formula pf; *) + (* let res = step pf in *) + (* Format.printf "Result :\n%s@." @@ string_of_formula res; *) + (* res *) + +(** Local model checker *) + +(** takes a normalized processor *) +let compute_derivation = + Semop.derivatives global_definition_map + +exception Impossible_transition + +let compute_modality modl tr = + + let get_matching_derivations_named act tr acc = + TSet.fold + (fun t acc -> + let _, pre, _ = t in + match act, pre with + | FIn s, T_In n | FOut s, T_Out n -> + if s = n then TSet.add t acc else acc + | _, T_Tau -> TSet.add t acc + | _, _ -> acc) + tr + acc + in + + let get_matching_derivations io tr = + TSet.fold + (fun t acc -> + let _, pre, _ = t in + match io, pre with + | In, T_In _ | Out, T_Out _ | Any, T_Tau | _, T_Tau -> TSet.add t acc + | _, _ -> acc) + tr + TSet.empty + in + + match modl with + | Strong, _, Prefix acts -> + List.fold_left + (fun acc a -> + get_matching_derivations_named a tr acc) + TSet.empty + acts + | Strong, _, (_ as io) -> + Format.printf "%s@." @@ string_of_modality modl; + get_matching_derivations io tr + | Weak, _, _ -> failwith "Weak not implemented yet" + +let handle_check_local form proc = + let proc = normalize proc in + + let rec step proc = function + | FTrue -> true + | FFalse -> false + | FNot f -> not @@ step proc f + | FAnd (f, g) -> step proc f && step proc g + | FOr (f, g) -> step proc f || step proc g + | FImplies (f, g) -> not (step proc f) || step proc g + | FModal (m, f) when diamond m -> + let d = compute_derivation proc in + let res = compute_modality m d in + TSet.fold (fun t _ -> print_endline @@ string_of_derivative t) res (); + if TSet.is_empty res then false (* meaning there is no transition *) + else + TSet.fold + (fun (_, _, p') acc -> + if acc then acc (* no need to test the transition if one is + true *) + else step p' f) + res + false + | FModal (m, f) -> + Format.printf "Box case@."; + (try + let d = compute_derivation proc in + let res = compute_modality m d in + TSet.fold (fun t _ -> print_endline @@ string_of_derivative t) res (); + if TSet.is_empty res then true (* meaning there is no transition *) + else + begin + Format.printf "Okay, let's test each transition now@."; + TSet.fold + (fun (_, _, p') acc -> + if not acc then acc (* no need to test the transition if one is + false *) + else step p' f) + res + true + end + + with + _ -> false) + | _ -> assert false + in + let res = step proc form in + if res then + Format.printf "The processor given matches the model@." + else + Format.printf "Doesn't match, here is why : @." diff --git a/src/Parser.mly b/src/Parser.mly index 6fd99de..b7574d6 100644 --- a/src/Parser.mly +++ b/src/Parser.mly @@ -252,10 +252,10 @@ { raise (Fatal_Parse_Error "missing process for names") } | PROP IDENT LPAREN RPAREN EQUAL formula - { Control.handle_prop $2 [] (formula_of_preformula $6) } + { Control.handle_prop $2 [] (substitute_prop $6) } | PROP IDENT LPAREN list_of_names RPAREN EQUAL formula - { Control.handle_prop $2 $4 (formula_of_preformula $7) } + { Control.handle_prop $2 $4 (substitute_prop $7) } | CHECK_LOCAL formula SATISFY process { Control.handle_check_local (formula_of_preformula $2) (process_of_preprocess $4) } @@ -375,25 +375,29 @@ | IDENT { FVar($1) } modality: - | INF list_of_prefixes SUP { FPossibly $2 } - | INF OUT SUP { FOutPossibly } - | INF IN SUP { FInPossibly } - | INF DOT SUP { FAnyPossibly } - - | INF INF list_of_prefixes SUP SUP { FWPossibly $3 } - | INF INF OUT SUP SUP { FWOutPossibly } - | INF INF IN SUP SUP { FWInPossibly } - | INF INF DOT SUP SUP { FWAnyPossibly } - - | LBRACKET list_of_prefixes RBRACKET { FNecessity $2 } - | LBRACKET OUT RBRACKET { FOutNecessity } - | LBRACKET IN RBRACKET { FInNecessity } - | LBRACKET DOT RBRACKET { FAnyNecessity } - - | LBRACKET LBRACKET list_of_prefixes RBRACKET RBRACKET { FWNecessity $3 } - | LBRACKET LBRACKET OUT RBRACKET RBRACKET { FWOutNecessity } - | LBRACKET LBRACKET IN RBRACKET RBRACKET { FWInNecessity } - | LBRACKET LBRACKET DOT RBRACKET RBRACKET { FWAnyNecessity } + | INF list_of_prefixes SUP + { Strong, Possibly, Prefix (Formula.parse_preprefix_list $2) } + | INF OUT SUP { Strong, Possibly, Out } + | INF IN SUP { Strong, Possibly, In } + | INF DOT SUP { Strong, Possibly, Any } + + | INF INF list_of_prefixes SUP SUP + { Weak, Possibly, Prefix (Formula.parse_preprefix_list $3) } + | INF INF OUT SUP SUP { Weak, Possibly, Out } + | INF INF IN SUP SUP { Weak, Possibly, In } + | INF INF DOT SUP SUP { Weak, Possibly, Any } + + | LBRACKET list_of_prefixes RBRACKET + { Strong, Necessity, Prefix (Formula.parse_preprefix_list $2) } + | LBRACKET OUT RBRACKET { Strong, Necessity, Out } + | LBRACKET IN RBRACKET { Strong, Necessity, In } + | LBRACKET DOT RBRACKET { Strong, Necessity, Any } + + | LBRACKET LBRACKET list_of_prefixes RBRACKET RBRACKET + { Weak, Necessity, Prefix (Formula.parse_preprefix_list $3) } + | LBRACKET LBRACKET OUT RBRACKET RBRACKET { Weak, Necessity, Out } + | LBRACKET LBRACKET IN RBRACKET RBRACKET { Weak, Necessity, In } + | LBRACKET LBRACKET DOT RBRACKET RBRACKET { Weak, Necessity, Any } %% From 9da427ae1d0acb8837d86b157627075e3aaeec51 Mon Sep 17 00:00:00 2001 From: Pierrick Couderc Date: Thu, 17 Oct 2013 18:15:21 +0200 Subject: [PATCH 11/26] Added Nu and Mu checking Not quite sure they work actually --- src/Formula.ml | 80 ++++++++++++++++++++++++++++++-------------------- src/Utils.ml | 4 +-- 2 files changed, 50 insertions(+), 34 deletions(-) diff --git a/src/Formula.ml b/src/Formula.ml index a0b22c2..781b58b 100644 --- a/src/Formula.ml +++ b/src/Formula.ml @@ -151,6 +151,22 @@ let add_prop name idents formula = Hashtbl.add props name (idents, formula) end + +let reduce f var value = + let rec step = function + | FVar v -> if v = var then value else FVar v + | FTrue | FFalse as f -> f + | FAnd (f, g) -> FAnd (step f, step g) + | FOr (f, g) -> FOr (step f, step g) + | FImplies (f, g) -> FImplies (step f, step g) + | FModal(m, f) -> FModal (m, step f) + | FInvModal (m, f) -> FInvModal (m, step f) + | FMu (x, f) -> FMu (x, step f) + | FNu (x, f) -> FNu (x, step f) + | _ -> assert false (* Technically, no Prop should remain ? *) + in + step f + let substitute f sub_list = let rec step sl = function | FVar v -> FVar (List.assoc v sl) @@ -298,53 +314,53 @@ let compute_modality modl tr = get_matching_derivations io tr | Weak, _, _ -> failwith "Weak not implemented yet" + let handle_check_local form proc = let proc = normalize proc in + let pset = PSet.empty in - let rec step proc = function + let rec step proc pset = function | FTrue -> true | FFalse -> false - | FNot f -> not @@ step proc f - | FAnd (f, g) -> step proc f && step proc g - | FOr (f, g) -> step proc f || step proc g - | FImplies (f, g) -> not (step proc f) || step proc g - | FModal (m, f) when diamond m -> + | FNot f -> not @@ step proc pset f + | FAnd (f, g) -> step proc pset f && step proc pset g + | FOr (f, g) -> step proc pset f || step proc pset g + | FImplies (f, g) -> not (step proc pset f) || step proc pset g + | FModal (m, f) -> let d = compute_derivation proc in let res = compute_modality m d in - TSet.fold (fun t _ -> print_endline @@ string_of_derivative t) res (); - if TSet.is_empty res then false (* meaning there is no transition *) - else + if TSet.is_empty res then not @@ diamond m + else if diamond m then TSet.fold (fun (_, _, p') acc -> if acc then acc (* no need to test the transition if one is true *) - else step p' f) + else step p' pset f) res false - | FModal (m, f) -> - Format.printf "Box case@."; - (try - let d = compute_derivation proc in - let res = compute_modality m d in - TSet.fold (fun t _ -> print_endline @@ string_of_derivative t) res (); - if TSet.is_empty res then true (* meaning there is no transition *) - else - begin - Format.printf "Okay, let's test each transition now@."; - TSet.fold - (fun (_, _, p') acc -> - if not acc then acc (* no need to test the transition if one is - false *) - else step p' f) - res - true - end - - with - _ -> false) + else + TSet.fold + (fun (_, _, p') acc -> + if not acc then acc (* no need to test the transition if one is + false *) + else step p' pset f) + res + true + | FNu (x, f) as nu -> if PSet.mem proc pset then true + else + let f = reduce f x nu in + let pset = PSet.add proc pset in + step proc pset f + + | FMu (x, f) -> + let nu = FNu(x, f) in + let f' = reduce f x @@ FNot nu in + let f = FNot f' in + not @@ step proc pset f + | _ -> assert false in - let res = step proc form in + let res = step proc pset form in if res then Format.printf "The processor given matches the model@." else diff --git a/src/Utils.ml b/src/Utils.ml index fd5cd6b..6b14ee0 100644 --- a/src/Utils.ml +++ b/src/Utils.ml @@ -29,7 +29,7 @@ let string_of_args tostr lst = string_of_collection "(" ")" "," tostr lst let string_of_set tostr set = string_of_collection "{" "}" "," tostr (SSet.elements set) -let string_of_map map = +let string_of_map map = string_of_collection "{" "}" "," (fun (old,value) -> sprintf "%s/%s" value old) (SMap.bindings map) @@ -51,7 +51,7 @@ let forget _ = () (* permutations:: 'a list -> 'a list list *) let rec permutations = - let rec inject_all e n l llen = + let rec inject_all e n l llen = if n > llen then [] else (inject e n l)::(inject_all e (n+1) l llen) and inject e n l = From 4a8bdb6061d5629b295535c7951064062f455023 Mon Sep 17 00:00:00 2001 From: Pierrick Couderc Date: Fri, 18 Oct 2013 13:31:56 +0200 Subject: [PATCH 12/26] Added Bdd.ml --- src/Bdd.ml | 39 +++++++++++++++++++++++++++++++++++++++ src/Formula.ml | 6 ++++++ src/Parser.mly | 2 ++ 3 files changed, 47 insertions(+) create mode 100644 src/Bdd.ml diff --git a/src/Bdd.ml b/src/Bdd.ml new file mode 100644 index 0000000..fc77abf --- /dev/null +++ b/src/Bdd.ml @@ -0,0 +1,39 @@ +(** Implementation of BDDs with hashconsing *) + +type t = {id: int; l: t; r: t} + +let rec null = {id = 0; l = null; r = null} + +let rec one = {id = 1; l = null; r = null} +let rec zero = {id = 2; l = null; r = null} + +type bdd = t + +module S = struct + type t = bdd + + let equal b1 b2 = + b1.l == b2.l && b1.r == b2.r + + let hash b = + 29 * (b.l.id + (29 * b.r.id)) + +end + +module H = Hashtbl.Make(S) + +let create = + let htbl = H.create 53 in + let id = ref 4 in + fun l r -> + if l == r then l + else + let i = !id in + let b = {id = i; l; r} in + try + H.find htbl b + with + Not_found -> + H.add htbl b b; + incr id; + b diff --git a/src/Formula.ml b/src/Formula.ml index 781b58b..116fa6b 100644 --- a/src/Formula.ml +++ b/src/Formula.ml @@ -98,6 +98,7 @@ let diamond = function type formula = | FTrue | FFalse + | FPar of formula | FAnd of formula * formula | FOr of formula * formula | FImplies of formula * formula @@ -112,6 +113,7 @@ type formula = let rec string_of_formula : formula -> string = function | FTrue -> "True" | FFalse -> "False" + | FPar f -> sprintf "(%s)" @@ string_of_formula f | FAnd(f,g) -> sprintf "(%s and %s)" (string_of_formula f) (string_of_formula g) | FOr(f,g) -> sprintf "(%s or %s)" (string_of_formula f) (string_of_formula g) | FImplies(f,g) -> sprintf "(%s ==> %s)" (string_of_formula f) (string_of_formula g) @@ -156,6 +158,7 @@ let reduce f var value = let rec step = function | FVar v -> if v = var then value else FVar v | FTrue | FFalse as f -> f + | FPar f -> FPar (step f) | FAnd (f, g) -> FAnd (step f, step g) | FOr (f, g) -> FOr (step f, step g) | FImplies (f, g) -> FImplies (step f, step g) @@ -171,6 +174,7 @@ let substitute f sub_list = let rec step sl = function | FVar v -> FVar (List.assoc v sl) | FTrue | FFalse as f -> f + | FPar f -> FPar (step sl f) | FAnd (f, g) -> FAnd (step sl f, step sl g) | FOr (f, g) -> FOr (step sl f, step sl g) | FImplies (f, g) -> FImplies (step sl f, step sl g) @@ -185,6 +189,7 @@ let substitute f sub_list = let substitute_prop pf = let rec step = function | FTrue | FFalse as f -> f + | FPar f -> FPar (step f) | FAnd (f, g) -> FAnd (step f, step g) | FOr (f, g) -> FOr (step f, step g) | FImplies (f, g) -> FImplies (step f, step g) @@ -322,6 +327,7 @@ let handle_check_local form proc = let rec step proc pset = function | FTrue -> true | FFalse -> false + | FPar f -> step proc pset f | FNot f -> not @@ step proc pset f | FAnd (f, g) -> step proc pset f && step proc pset g | FOr (f, g) -> step proc pset f || step proc pset g diff --git a/src/Parser.mly b/src/Parser.mly index b7574d6..e058843 100644 --- a/src/Parser.mly +++ b/src/Parser.mly @@ -363,9 +363,11 @@ formula: | TRUE { FTrue } | FALSE { FFalse } + | LPAREN formula RPAREN { FPar $2 } | formula AND formula { FAnd ($1,$3) } | formula OR formula { FOr ($1,$3) } | formula IMPLIES formula { FImplies ($1,$3) } + | modality LPAREN formula RPAREN { FModal($1, $3) } | modality formula { FModal($1,$2) } | TILD modality formula { FInvModal($2,$3) } | MU LPAREN IDENT RPAREN DOT formula { FMu ($3,$6) } From cbc80cb91ed3f07af770ce701a42ff9f536ca2a9 Mon Sep 17 00:00:00 2001 From: Pierrick Couderc Date: Sat, 19 Oct 2013 13:41:20 +0200 Subject: [PATCH 13/26] Improved Bdd implementation --- src/Bdd.ml | 79 ++++++++++++++++++++++++++++++++++++++------------ src/Formula.ml | 14 +++++++++ 2 files changed, 74 insertions(+), 19 deletions(-) diff --git a/src/Bdd.ml b/src/Bdd.ml index fc77abf..753c949 100644 --- a/src/Bdd.ml +++ b/src/Bdd.ml @@ -1,11 +1,11 @@ (** Implementation of BDDs with hashconsing *) -type t = {id: int; l: t; r: t} +type t = {id: int; l: t; r: t; value: int} -let rec null = {id = 0; l = null; r = null} +let rec null = {id = -1; l = null; r = null; value = -1} -let rec one = {id = 1; l = null; r = null} -let rec zero = {id = 2; l = null; r = null} +let one = {id = 0; l = null; r = null; value = -1} +let zero = {id = 1; l = null; r = null; value = -1} type bdd = t @@ -20,20 +20,61 @@ module S = struct end -module H = Hashtbl.Make(S) +module HBdd = Hashtbl.Make(S) let create = - let htbl = H.create 53 in - let id = ref 4 in - fun l r -> - if l == r then l - else - let i = !id in - let b = {id = i; l; r} in - try - H.find htbl b - with - Not_found -> - H.add htbl b b; - incr id; - b + let htbl = HBdd.create 53 in + let id = ref 2 in + fun v l r -> + let i = !id in + let b = {id = i; l; r; value = v} in + try + HBdd.find htbl b + with + Not_found -> + HBdd.add htbl b b; + incr id; + b + +module HPair = Hashtbl.Make( + struct + type t = bdd * bdd + + let equal (b1, b2) (b1', b2') = + S.equal b1 b1' && S.equal b2 b2' + + let hash (b1, b2) = + S.hash b1 + 29 * S.hash b2 + end) + +let is_leaf b = b == one || b == zero + +let boolean_equiv b = + if b == one then true + else if b == zero then false + else assert false + +let apply = + let htbl = HPair.create 53 in + let apply_op op b1 b2 = + let b1 = boolean_equiv b1 in + let b2 = boolean_equiv b2 in + let res = op b1 b2 in + if res then one else zero + in + fun op -> + let rec apply b1 b2 = + try HPair.find htbl (b1, b2) + with Not_found -> + let res = + if is_leaf b1 && is_leaf b2 then + apply_op op b1 b2 + else if b1.value = b2.value then + create b1.value (apply b1.l b2.l) (apply b1.r b2.r) + else if b1.value < b2.value then + create b1.value (apply b1.l b2) (apply b1.r b2) + else create b2.value (apply b1 b2.l) (apply b1 b2.r) + in + HPair.add htbl (b1, b2) res; res + in + apply diff --git a/src/Formula.ml b/src/Formula.ml index 116fa6b..c5d64cb 100644 --- a/src/Formula.ml +++ b/src/Formula.ml @@ -7,6 +7,7 @@ open Utils open Global open Normalize open Semop +open Bdd (* mu-calculus formulae *) @@ -352,6 +353,8 @@ let handle_check_local form proc = else step p' pset f) res true + | FInvModal(m, f) -> + not @@ step proc pset @@ FModal (m,f) | FNu (x, f) as nu -> if PSet.mem proc pset then true else let f = reduce f x nu in @@ -371,3 +374,14 @@ let handle_check_local form proc = Format.printf "The processor given matches the model@." else Format.printf "Doesn't match, here is why : @." + + +let bdd_of_formula f = + (* let fix f l = assert false in *) + let step f _l = + match f with + | FTrue -> one + | FFalse -> zero + | _ -> assert false + in + step f From 4255a789ccf132007b48aa5c7fdcfa526d567398 Mon Sep 17 00:00:00 2001 From: Pierrick Couderc Date: Sat, 19 Oct 2013 14:50:00 +0200 Subject: [PATCH 14/26] Improved bdd with restrict and exists --- src/Bdd.ml | 16 ++++++++++++++++ src/Formula.ml | 19 ++++++++++++++++++- 2 files changed, 34 insertions(+), 1 deletion(-) diff --git a/src/Bdd.ml b/src/Bdd.ml index 753c949..06e5893 100644 --- a/src/Bdd.ml +++ b/src/Bdd.ml @@ -78,3 +78,19 @@ let apply = HPair.add htbl (b1, b2) res; res in apply + +let rec restrict bool value b = + if is_leaf b then b + else + if b.value < value then + let l = restrict bool value b.l in + let r = restrict bool value b.r in + create b.value l r + else if b.value = value then + if bool then b.r else b.l + else b + +let exists value b = + let l = restrict false value b in + let r = restrict true value b in + apply ( or ) l r diff --git a/src/Formula.ml b/src/Formula.ml index c5d64cb..855fbf4 100644 --- a/src/Formula.ml +++ b/src/Formula.ml @@ -378,10 +378,27 @@ let handle_check_local form proc = let bdd_of_formula f = (* let fix f l = assert false in *) - let step f _l = + let implies b1 b2 = (not b1) || b2 in + let xor b1 b2 = ((not b1) && b2) || (b1 && (not b2)) in + let env = [] in + let rec step f env = match f with | FTrue -> one | FFalse -> zero + | FNot f -> apply xor (step f env) one + | FAnd (f1, f2) -> + let b1 = step f1 env in + let b2 = step f2 env in + apply ( && ) b1 b2 + | FOr (f1, f2) -> + let b1 = step f1 env in + let b2 = step f2 env in + apply ( && ) b1 b2 + | FImplies (f1, f2) -> + let b1 = step f1 env in + let b2 = step f2 env in + apply implies b1 b2 + | FModal (_m, _f) -> assert false | _ -> assert false in step f From acd31bd9d1124f9ea51771c2064c532cdfa65daf Mon Sep 17 00:00:00 2001 From: Pierrick Couderc Date: Mon, 21 Oct 2013 14:12:14 +0200 Subject: [PATCH 15/26] Fixed Bdd --- src/Bdd.ml | 33 ++++++++++++++++----------------- src/Formula.ml | 41 ++--------------------------------------- 2 files changed, 18 insertions(+), 56 deletions(-) diff --git a/src/Bdd.ml b/src/Bdd.ml index 06e5893..252b47f 100644 --- a/src/Bdd.ml +++ b/src/Bdd.ml @@ -54,7 +54,7 @@ let boolean_equiv b = else if b == zero then false else assert false -let apply = +let apply op = let htbl = HPair.create 53 in let apply_op op b1 b2 = let b1 = boolean_equiv b1 in @@ -62,22 +62,21 @@ let apply = let res = op b1 b2 in if res then one else zero in - fun op -> - let rec apply b1 b2 = - try HPair.find htbl (b1, b2) - with Not_found -> - let res = - if is_leaf b1 && is_leaf b2 then - apply_op op b1 b2 - else if b1.value = b2.value then - create b1.value (apply b1.l b2.l) (apply b1.r b2.r) - else if b1.value < b2.value then - create b1.value (apply b1.l b2) (apply b1.r b2) - else create b2.value (apply b1 b2.l) (apply b1 b2.r) - in - HPair.add htbl (b1, b2) res; res - in - apply + let rec apply b1 b2 = + try HPair.find htbl (b1, b2) + with Not_found -> + let res = + if is_leaf b1 && is_leaf b2 then + apply_op op b1 b2 + else if b1.value = b2.value then + create b1.value (apply b1.l b2.l) (apply b1.r b2.r) + else if b1.value < b2.value then + create b1.value (apply b1.l b2) (apply b1.r b2) + else create b2.value (apply b1 b2.l) (apply b1 b2.r) + in + HPair.add htbl (b1, b2) res; res + in + apply let rec restrict bool value b = if is_leaf b then b diff --git a/src/Formula.ml b/src/Formula.ml index 855fbf4..e2b2d53 100644 --- a/src/Formula.ml +++ b/src/Formula.ml @@ -9,27 +9,6 @@ open Normalize open Semop open Bdd -(* mu-calculus formulae *) - -(* type modality = *) -(* | FPossibly of preprefix list *) -(* | FOutPossibly *) -(* | FInPossibly *) -(* | FAnyPossibly *) -(* | FWPossibly of preprefix list *) -(* | FWOutPossibly *) -(* | FWInPossibly *) -(* | FWAnyPossibly *) -(* | FNecessity of preprefix list *) -(* | FOutNecessity *) -(* | FInNecessity *) -(* | FAnyNecessity *) -(* | FWNecessity of preprefix list *) -(* | FWOutNecessity *) -(* | FWInNecessity *) -(* | FWAnyNecessity *) - - type fprefix = | FIn of string | FInVar of string @@ -75,22 +54,6 @@ let string_of_modality (s, m, io) = | Strong, Necessity -> Format.sprintf "[%s]" io | Weak, Possibly -> Format.sprintf "<<%s>>" io | Weak, Necessity -> Format.sprintf "[[%s]]" io - (* | Strong, Possibly, Prefix acts -> string_of_collection "<" ">" "," string_of_preprefix acts *) - (* | -> "" *) - (* | FInPossibly -> "" *) - (* | FAnyPossibly -> "<.>" *) - (* | FWPossibly(acts) -> string_of_collection "<<" ">>" "," string_of_preprefix acts *) - (* | FWOutPossibly -> "<>" *) - (* | FWInPossibly -> "<>" *) - (* | FWAnyPossibly -> "<<.>>" *) - (* | FNecessity(acts) -> string_of_collection "[" "]" "," string_of_preprefix acts *) - (* | FOutNecessity -> "[!]" *) - (* | FInNecessity -> "[?]" *) - (* | FAnyNecessity -> "[.]" *) - (* | FWNecessity(acts) -> string_of_collection "[[" "]]" "," string_of_preprefix acts *) - (* | FWOutNecessity -> "[[!]]" *) - (* | FWInNecessity -> "[[?]]" *) - (* | FWAnyNecessity -> "[[.]]" *) let diamond = function | _, Possibly, _ -> true @@ -380,7 +343,7 @@ let bdd_of_formula f = (* let fix f l = assert false in *) let implies b1 b2 = (not b1) || b2 in let xor b1 b2 = ((not b1) && b2) || (b1 && (not b2)) in - let env = [] in + let _env = [] in let rec step f env = match f with | FTrue -> one @@ -393,7 +356,7 @@ let bdd_of_formula f = | FOr (f1, f2) -> let b1 = step f1 env in let b2 = step f2 env in - apply ( && ) b1 b2 + apply ( || ) b1 b2 | FImplies (f1, f2) -> let b1 = step f1 env in let b2 = step f2 env in From 9d7fae0ba7fc828e4beedffbaea8a10ffe04ef90 Mon Sep 17 00:00:00 2001 From: Pierrick Couderc Date: Tue, 29 Oct 2013 14:23:46 +0100 Subject: [PATCH 16/26] Small optim in Bdd.ml (thanks Remy) --- src/Bdd.ml | 5 ++--- 1 file changed, 2 insertions(+), 3 deletions(-) diff --git a/src/Bdd.ml b/src/Bdd.ml index 252b47f..05ad987 100644 --- a/src/Bdd.ml +++ b/src/Bdd.ml @@ -50,9 +50,8 @@ module HPair = Hashtbl.Make( let is_leaf b = b == one || b == zero let boolean_equiv b = - if b == one then true - else if b == zero then false - else assert false + (* if b <> from one and zero, assert false will be evaluated *) + b == one || (b <> 0 && assert false) let apply op = let htbl = HPair.create 53 in From e4187c9d1b3d02d30a981c43b09c56ba01b7edd0 Mon Sep 17 00:00:00 2001 From: Pierrick Couderc Date: Thu, 7 Nov 2013 15:55:20 +0100 Subject: [PATCH 17/26] Beginning of preformula --- src/Bdd.ml | 2 +- src/Formula.ml | 133 +++++++++++++++++++++++++++++++++++++++---------- src/Lexer.mll | 29 +++++++---- src/Parser.mly | 42 +++++++++------- 4 files changed, 152 insertions(+), 54 deletions(-) diff --git a/src/Bdd.ml b/src/Bdd.ml index 05ad987..bd81052 100644 --- a/src/Bdd.ml +++ b/src/Bdd.ml @@ -51,7 +51,7 @@ let is_leaf b = b == one || b == zero let boolean_equiv b = (* if b <> from one and zero, assert false will be evaluated *) - b == one || (b <> 0 && assert false) + b == one || (b <> zero && assert false) let apply op = let htbl = HPair.create 53 in diff --git a/src/Formula.ml b/src/Formula.ml index e2b2d53..9b07cf5 100644 --- a/src/Formula.ml +++ b/src/Formula.ml @@ -59,6 +59,43 @@ let diamond = function | _, Possibly, _ -> true | _, _, _ -> false +type preformula = + | PFTrue + | PFFalse + | PFPar of preformula + | PFAnd of preformula * preformula + | PFOr of preformula * preformula + | PFImplies of preformula * preformula + | PFModal of modality * preformula + | PFInvModal of modality * preformula + | PFProp of string * (string list) + | PFVar of string + | PFMu of string * preformula + | PFNu of string * preformula + | PFForall of preparam * preexpr * preformula + | PFExists of preparam * preexpr * preformula + +let rec string_of_preformula : preformula -> string = function + | PFTrue -> "True" + | PFFalse -> "False" + | PFPar f -> sprintf "(%s)" @@ string_of_preformula f + | PFAnd(f,g) -> sprintf "(%s and %s)" (string_of_preformula f) (string_of_preformula g) + | PFOr(f,g) -> sprintf "(%s or %s)" (string_of_preformula f) (string_of_preformula g) + | PFImplies(f,g) -> sprintf "(%s ==> %s)" (string_of_preformula f) (string_of_preformula g) + | PFModal(m,f) -> (string_of_modality m) ^ (string_of_preformula f) + | PFInvModal(m,f) -> "~" ^ (string_of_modality m) ^ (string_of_preformula f) + | PFProp(prop,params) -> prop ^ (string_of_collection "(" ")" "," (fun s -> s) params) + | PFVar(var) -> var + | PFMu(x,f) -> sprintf "Mu(%s).%s" x (string_of_preformula f) + | PFNu(x,f) -> sprintf "Nu(%s).%s" x (string_of_preformula f) + | PFForall (par, pe, f) -> + sprintf "(forall %s, %s in %s)" + (string_of_preparam par) (string_of_preexpr pe) (string_of_preformula f) + | PFExists (par, pe, f) -> + sprintf "(exists %s, %s in %s)" + (string_of_preparam par) (string_of_preexpr pe) (string_of_preformula f) + + type formula = | FTrue | FFalse @@ -176,7 +213,32 @@ let substitute_prop pf = res -let formula_of_preformula = substitute_prop +let formula_of_preformula pf = + let rec step = function + | PFTrue -> FTrue + | PFFalse -> FFalse + | PFPar f -> FPar (step f) + | PFAnd (f, g) -> FAnd (step f, step g) + | PFOr (f, g) -> FOr (step f, step g) + | PFImplies (f, g) -> FImplies (step f, step g) + | PFModal(m, f) -> FModal (m, step f) + | PFInvModal (m, f) -> FInvModal (m, step f) + | PFVar v -> FVar v + | PFMu (x, f) -> FMu (x, step f) + | PFNu (x, f) -> FNu (x, step f) + | PFProp (s, il) -> + if Hashtbl.mem props s then + let (vars, formula) = Hashtbl.find props s in + substitute formula @@ List.combine vars il + else + raise (Unbound_prop s) + | PFForall (_, _, f) -> step f + | PFExists (_, _, f) -> step f + in + Format.printf "Preformula received :\n%s@." @@ string_of_preformula pf; + let res = step pf in + Format.printf "Result :\n%s@." @@ string_of_formula res; + res (* let rename_modality = assert false (\* function *\) *) (* (\* | FPossibility pl -> *\) *) (* in *) @@ -288,56 +350,77 @@ let handle_check_local form proc = let proc = normalize proc in let pset = PSet.empty in - let rec step proc pset = function - | FTrue -> true - | FFalse -> false - | FPar f -> step proc pset f - | FNot f -> not @@ step proc pset f - | FAnd (f, g) -> step proc pset f && step proc pset g - | FOr (f, g) -> step proc pset f || step proc pset g - | FImplies (f, g) -> not (step proc pset f) || step proc pset g + let rec step proc pset trace = function + | FTrue -> true, trace + | FFalse -> false, trace + | FPar f -> step proc pset trace f + | FNot f -> let r, t = step proc pset trace f in + (not r, t) + | FAnd (f, g) -> let r1, t1 = step proc pset trace f in + let r2, t2 = step proc pset trace g in + if r1 && r2 then true, t1 + else if r1 then false, t2 + else false, t1 + | FOr (f, g) -> let r1, t1 = step proc pset trace f in + let r2, _ = step proc pset trace g in + if r1 || r2 then true, t1 + else false, t1 (* both can be considered as an incorrect + trace *) + | FImplies (f, g) -> + let r1, t1 = step proc pset trace f in + let r2, _t2 = step proc pset trace g in + if not r1 || r2 then true, t1 + else false, t1 | FModal (m, f) -> let d = compute_derivation proc in let res = compute_modality m d in - if TSet.is_empty res then not @@ diamond m + if TSet.is_empty res then (not @@ diamond m, trace) else if diamond m then TSet.fold - (fun (_, _, p') acc -> - if acc then acc (* no need to test the transition if one is + (fun (_, m, p') (r, t) -> + if r then r,t (* no need to test the transition if one is true *) - else step p' pset f) + else step p' pset (m::t) f) res - false + (false, trace) else TSet.fold - (fun (_, _, p') acc -> - if not acc then acc (* no need to test the transition if one is + (fun (_, m, p') (r, t) -> + if not r then r,t (* no need to test the transition if one is false *) - else step p' pset f) + else step p' pset (m::t) f) res - true + (true, trace) | FInvModal(m, f) -> - not @@ step proc pset @@ FModal (m,f) - | FNu (x, f) as nu -> if PSet.mem proc pset then true + let r, t = step proc pset trace @@ FModal (m,f) in + (not r, t) + | FNu (x, f) as nu -> if PSet.mem proc pset then true, trace else let f = reduce f x nu in let pset = PSet.add proc pset in - step proc pset f + step proc pset trace f | FMu (x, f) -> let nu = FNu(x, f) in let f' = reduce f x @@ FNot nu in let f = FNot f' in - not @@ step proc pset f + let r, t = step proc pset trace f in + not r, t | _ -> assert false in - let res = step proc pset form in + let (res, trace) = step proc pset [] form in if res then Format.printf "The processor given matches the model@." else - Format.printf "Doesn't match, here is why : @." - + begin + let t = List.rev trace |> + List.fold_left (fun acc t -> + Format.sprintf "%s --> %s" acc @@ string_of_label t) "" + in + let t = Format.sprintf "%s --> " t in + Format.printf "Doesn't match, here is why: @.%s@." t + end let bdd_of_formula f = (* let fix f l = assert false in *) diff --git a/src/Lexer.mll b/src/Lexer.mll index 7decd26..1d8a3b1 100644 --- a/src/Lexer.mll +++ b/src/Lexer.mll @@ -1,5 +1,5 @@ -{ +{ open Parser let line=ref 1 @@ -11,7 +11,7 @@ let digit = ['0'-'9'] let int = (['1'-'9'] digit*) let cmt = ('#' [^'\n']*) - + let r_def = "def" let r_true = "true" let r_false = "false" @@ -27,6 +27,8 @@ let r_if = "if" let r_then = "then" let r_else = "else" +let r_in = "in" + let r_const = "const" let r_type = "type" @@ -92,6 +94,9 @@ let cmd_check = "check" let cmd_check_local = "checklocal" let cmd_check_global = "checkglobal" +let forall = "forall" +let exists = "exists" + let sat_1 = "|-" let sat_2 = "satisfies" @@ -105,7 +110,7 @@ let nu_3 = "NU" rule token = parse | ws {token lexbuf} - | eol + | eol { incr line; token lexbuf } | cmt @@ -131,11 +136,12 @@ let nu_3 = "NU" | r_if { IF } | r_then { THEN } | r_else { ELSE } + | r_in { INDEF } | r_const { CONSTDEF } | r_type { TYPEDEF } | dotdot { DOTDOT } - | op_dot { DOT } - | op_plus { PLUS } + | op_dot { DOT } + | op_plus { PLUS } | op_minus { MINUS } | op_par { PAR } | op_out { OUT } @@ -169,7 +175,7 @@ let nu_3 = "NU" | cmd_free { FREE } | cmd_bound { BOUND } | cmd_names { NAMES } - + | implies_1 { IMPLIES } | implies_2 { IMPLIES } @@ -180,6 +186,9 @@ let nu_3 = "NU" | cmd_wmini { WMINI } | cmd_wfbisim { WFBISIM } + | forall { FORALL } + | exists { EXISTS } + | mu_1 { MU } | mu_2 { MU } | mu_3 { MU } @@ -195,14 +204,14 @@ let nu_3 = "NU" | sat_1 { SATISFY } | sat_2 { SATISFY } - + | cmd_help { HELP } | cmd_quit { QUIT } - | ident as id + | ident as id { IDENT (id) } | eof { EOF } - | _ { failwith((Lexing.lexeme lexbuf) ^ + | _ { failwith((Lexing.lexeme lexbuf) ^ ": mistake at line " ^ string_of_int !line)} - + { } diff --git a/src/Parser.mly b/src/Parser.mly index e058843..e28d19f 100644 --- a/src/Parser.mly +++ b/src/Parser.mly @@ -71,9 +71,12 @@ /* inturals */ %token INT +/* quantifiers */ +%token FORALL EXISTS + /* punctuation */ %token LPAREN RPAREN LBRACKET RBRACKET COMMA EQUAL EQEQ TILD COLON -%token IF THEN ELSE INF SUP INFEQ SUPEQ DIFF DOTDOT LACCOL RACCOL +%token IF THEN ELSE INF SUP INFEQ SUPEQ DIFF DOTDOT LACCOL RACCOL INDEF /* operators */ %token PAR PLUS DOT OUT IN MINUS DIV MULT MOD AND OR NOT IMPLIES @@ -87,6 +90,7 @@ %left MULT , DIV , MOD %right COMMA %left OUT IN +%left INDEF %nonassoc UNARY @@ -101,7 +105,7 @@ %type prefix %type expr %type modality -%type formula +%type formula /* grammar */ %% @@ -252,10 +256,10 @@ { raise (Fatal_Parse_Error "missing process for names") } | PROP IDENT LPAREN RPAREN EQUAL formula - { Control.handle_prop $2 [] (substitute_prop $6) } + { Control.handle_prop $2 [] (formula_of_preformula $6) } | PROP IDENT LPAREN list_of_names RPAREN EQUAL formula - { Control.handle_prop $2 $4 (substitute_prop $7) } + { Control.handle_prop $2 $4 (formula_of_preformula $7) } | CHECK_LOCAL formula SATISFY process { Control.handle_check_local (formula_of_preformula $2) (process_of_preprocess $4) } @@ -361,20 +365,22 @@ | expr list_of_exprs { $1::$2 } formula: - | TRUE { FTrue } - | FALSE { FFalse } - | LPAREN formula RPAREN { FPar $2 } - | formula AND formula { FAnd ($1,$3) } - | formula OR formula { FOr ($1,$3) } - | formula IMPLIES formula { FImplies ($1,$3) } - | modality LPAREN formula RPAREN { FModal($1, $3) } - | modality formula { FModal($1,$2) } - | TILD modality formula { FInvModal($2,$3) } - | MU LPAREN IDENT RPAREN DOT formula { FMu ($3,$6) } - | NU LPAREN IDENT RPAREN DOT formula { FNu ($3,$6) } - | IDENT LPAREN RPAREN { FProp($1, []) } - | IDENT LPAREN list_of_names RPAREN { FProp($1,$3) } - | IDENT { FVar($1) } + | TRUE { PFTrue } + | FALSE { PFFalse } + | LPAREN formula RPAREN { PFPar $2 } + | formula AND formula { PFAnd ($1,$3) } + | formula OR formula { PFOr ($1,$3) } + | formula IMPLIES formula { PFImplies ($1,$3) } + | modality LPAREN formula RPAREN { PFModal($1, $3) } + | modality formula { PFModal($1,$2) } + | TILD modality formula { PFInvModal($2,$3) } + | MU LPAREN IDENT RPAREN DOT formula { PFMu ($3,$6) } + | NU LPAREN IDENT RPAREN DOT formula { PFNu ($3,$6) } + | IDENT LPAREN RPAREN { PFProp($1, []) } + | IDENT LPAREN list_of_names RPAREN { PFProp($1,$3) } + | IDENT { PFVar($1) } + | FORALL param COMMA expr INDEF formula { PFForall($2, $4, $6) } + | EXISTS param COMMA expr INDEF formula { PFExists($2, $4, $6) } modality: | INF list_of_prefixes SUP From a4f258f01b59f78eacf29e21812b6d1764ee648d Mon Sep 17 00:00:00 2001 From: Pierrick Couderc Date: Thu, 7 Nov 2013 18:24:48 +0100 Subject: [PATCH 18/26] Finished preformula --- src/Formula.ml | 244 ++++++++++++++++++++++++++++++++++--------------- 1 file changed, 169 insertions(+), 75 deletions(-) diff --git a/src/Formula.ml b/src/Formula.ml index 9b07cf5..607fcb6 100644 --- a/src/Formula.ml +++ b/src/Formula.ml @@ -19,14 +19,16 @@ type fprefix = let fprefix_of_preprefix = function | PIn (PName n) -> FIn n | POut (PName n) -> FOut n - | PIn (PVar n) -> FInVar n - | POut (PVar n) -> FOutVar n + | PIn (PVar n) -> FInVar n (* (String.sub n 1 (String.length n - 1)) *) + | POut (PVar n) -> FOutVar n (* (String.sub n 1 (String.length n - 1)) *) | PTau -> FTau | _ as pr -> failwith (Format.sprintf "Received : %s@." @@ string_of_preprefix pr) let string_of_fprefix = function - | FIn n | FInVar n -> n ^ "?" - | FOut n | FOutVar n -> n ^ "!" + | FIn n -> n ^ "?" + | FInVar n -> "var:" ^ n ^ "?" + | FOut n -> n ^ "!" + | FOutVar n -> "var:" ^ n ^ "!" | FTau -> "tau" let parse_preprefix_list = @@ -213,91 +215,183 @@ let substitute_prop pf = res +let substitute_modality m vars = + let rename_modal (s,mo,io) = + match io with + | In | Out | Any -> m + | Prefix l -> + s, mo, Prefix (List.map + (fun fpref -> + match fpref with + | FTau -> FTau + | FOut _ | FIn _ -> fpref + | FInVar s -> Format.printf "I found a variable!@."; + if SMap.mem s vars then + FIn (s ^ "_" ^ (string_of_int @@ int_of_value @@ (SMap.find s vars))) + else fpref + | FOutVar s -> if SMap.mem s vars then + FIn (s ^ "_" ^ (string_of_int @@ int_of_value @@ (SMap.find s vars))) + else fpref) + l) + in + rename_modal m + + let formula_of_preformula pf = - let rec step = function + let open Syntax in + let compute_param p = + match p with + | PParamVar (n, t) -> + n, value_list (SMap.find t !env_type) + | _ -> failwith + (Format.sprintf "Unusable param for mu-calculus:%s@." @@ string_of_preparam p) + in + + let rec test_expr vars = function + | PTrue -> Bool true + | PFalse -> Bool false + | PInt i -> Int i + | PName str -> Name str + | PConst name -> Int (SMap.find name !env_const) + | PVar name -> (SMap.find name vars) + | PNot pexpr -> let b = bool_of_value (test_expr vars pexpr) in Bool (not b) + | PAnd (preexpr1, preexpr2) -> + let b1 = bool_of_value (test_expr vars preexpr1) + and b2 = bool_of_value (test_expr vars preexpr2) in + Bool ( b1 && b2 ) + | POr (preexpr1, preexpr2) -> + let b1 = bool_of_value (test_expr vars preexpr1) + and b2 = bool_of_value (test_expr vars preexpr2) in + Bool ( b1 || b2 ) + + | PAdd (preexpr1, preexpr2) -> + let i1 = int_of_value (test_expr vars preexpr1 ) + and i2 = int_of_value ( test_expr vars preexpr2 ) in + Int ( i1 + i2 ) + + | PSub (preexpr1, preexpr2) -> + let i1 = int_of_value (test_expr vars preexpr1 ) + and i2 = int_of_value ( test_expr vars preexpr2 ) in + Int ( i1 - i2 ) + + | PMul (preexpr1, preexpr2) -> + let i1 = int_of_value (test_expr vars preexpr1 ) + and i2 = int_of_value ( test_expr vars preexpr2 ) in + Int ( i1 * i2 ) + + | PDiv (preexpr1, preexpr2) -> + let i1 = int_of_value (test_expr vars preexpr1 ) + and i2 = int_of_value ( test_expr vars preexpr2 ) in + Int ( i1 / i2 ) + + | PMod (preexpr1, preexpr2) -> + let i1 = int_of_value (test_expr vars preexpr1 ) + and i2 = int_of_value ( test_expr vars preexpr2 ) in + Int ( i1 mod i2 ) + + | PInf (preexpr1, preexpr2) -> + let i1 = int_of_value (test_expr vars preexpr1 ) + and i2 = int_of_value ( test_expr vars preexpr2 ) in + Bool ( i1 < i2 ) + + | PSup (preexpr1, preexpr2) -> + let i1 = int_of_value (test_expr vars preexpr1 ) + and i2 = int_of_value ( test_expr vars preexpr2 ) in + Bool ( i1 > i2 ) + + | PEq (preexpr1, preexpr2) -> + let p1 = test_expr vars preexpr1 + and p2 = test_expr vars preexpr2 in + (match (p1, p2) with + | (Bool b1, Bool b2) -> Bool ( b1 = b2 ) + | (Int i1, Int i2) -> Bool ( i1 = i2 ) + | (Name n1, Name n2) -> Bool ( n1 = n2 ) + | (_, _) -> Bool ( false )) + + | PNeq (preexpr1, preexpr2) -> + let p1 = test_expr vars preexpr1 + and p2 = test_expr vars preexpr2 in + (match (p1, p2) with + | (Bool b1, Bool b2) -> Bool ( b1 <> b2 ) + | (Int i1, Int i2) -> Bool ( i1 <> i2 ) + | (Name n1, Name n2) -> Bool ( n1 <> n2 ) + | (_, _) -> Bool ( true )) + + | PInfEq (preexpr1, preexpr2) -> + let i1 = int_of_value (test_expr vars preexpr1 ) + and i2 = int_of_value ( test_expr vars preexpr2 ) in + Bool ( i1 <= i2 ) + + | PSupEq (preexpr1, preexpr2) -> + let i1 = int_of_value (test_expr vars preexpr1 ) + and i2 = int_of_value ( test_expr vars preexpr2 ) in + Bool ( i1 >= i2 ) + + | PIf (cond, preexpr1, preexpr2) -> + let b = bool_of_value (test_expr vars cond) in + if b then + test_expr vars preexpr1 + else + test_expr vars preexpr2 + in + + let res_of_expr e vars = + match test_expr vars e with + | Bool b -> b + | _ -> failwith "The result of the expression wasn't a boolean expression" + in + + let rec step vars = function | PFTrue -> FTrue | PFFalse -> FFalse - | PFPar f -> FPar (step f) - | PFAnd (f, g) -> FAnd (step f, step g) - | PFOr (f, g) -> FOr (step f, step g) - | PFImplies (f, g) -> FImplies (step f, step g) - | PFModal(m, f) -> FModal (m, step f) - | PFInvModal (m, f) -> FInvModal (m, step f) + | PFPar f -> FPar (step vars f) + | PFAnd (f, g) -> FAnd (step vars f, step vars g) + | PFOr (f, g) -> FOr (step vars f, step vars g) + | PFImplies (f, g) -> FImplies (step vars f, step vars g) + | PFModal(m, f) -> FModal (substitute_modality m vars, step vars f) + | PFInvModal (m, f) -> FInvModal (substitute_modality m vars, step vars f) | PFVar v -> FVar v - | PFMu (x, f) -> FMu (x, step f) - | PFNu (x, f) -> FNu (x, step f) + | PFMu (x, f) -> FMu (x, step vars f) + | PFNu (x, f) -> FNu (x, step vars f) | PFProp (s, il) -> if Hashtbl.mem props s then let (vars, formula) = Hashtbl.find props s in substitute formula @@ List.combine vars il else raise (Unbound_prop s) - | PFForall (_, _, f) -> step f - | PFExists (_, _, f) -> step f + | PFForall (param, expr, f) -> + let n, val_list = compute_param param in + List.fold_left + (fun acc_f i -> + let vars = SMap.add n i vars in + let b = res_of_expr expr vars in + if b then + let f = step vars f in + if acc_f = FTrue then f + else FAnd (f, acc_f) + else acc_f) + FTrue + val_list + + | PFExists (param, expr, f) -> + let n, val_list = compute_param param in + List.fold_left + (fun acc_f i -> + let vars = SMap.add n i vars in + let b = res_of_expr expr vars in + if b then + let f = step vars f in + if acc_f = FFalse then f + else FOr (f, acc_f) + else acc_f) + FFalse + val_list + in Format.printf "Preformula received :\n%s@." @@ string_of_preformula pf; - let res = step pf in + let res = step SMap.empty pf in Format.printf "Result :\n%s@." @@ string_of_formula res; res - (* let rename_modality = assert false (\* function *\) *) - (* (\* | FPossibility pl -> *\) *) - (* in *) - (* let sub = function *) - (* | FModal (m, f) -> *) - - (* let rename m = *) - (* match fprefix_of_preprefix m with *) - (* | FInVar n -> PIn (PName (n ^ "_" ^ value)) *) - (* | FOutVar n -> POut (PName (n ^ "_" ^ value)) *) - (* | _ -> m *) - (* in *) - (* FModal (m, sub value f) *) - (* | FInvModal (m, f) -> *) - (* let m = *) - (* match fprefix_of_preprefix m with *) - (* | FInVar n -> PIn (PName (n ^ "_" ^ value)) *) - (* | FOutVar n -> POut (PName (n ^ "_" ^ value)) *) - (* | _ -> m *) - (* in *) - (* FInvModal (m, sub value f) *) - (* | FTrue | FFalse as f -> f *) - (* | FAnd (f, g) -> FAnd (sub value f, sub value g) *) - (* | FOr (f, g) -> FOr (sub value f, sub value g) *) - (* | FImplies (f, g) -> FImplies (sub value f, sub value g) *) - (* | FModal(m, f) -> FModal (m, sub value f) *) - (* | FInvModal (m, f) -> FInvModal (m, sub value f) *) - (* | FVar v -> FVar v *) - (* | FMu (x, f) -> FMu (x, sub value f) *) - (* | FNu (x, f) -> FNu (x, sub value f) *) - (* in *) - (* let rec step = function *) - (* | FTrue | FFalse as f -> f *) - (* | FAnd (f, g) -> FAnd (step f, step g) *) - (* | FOr (f, g) -> FOr (step f, step g) *) - (* | FImplies (f, g) -> FImplies (step f, step g) *) - (* | FModal(m, f) -> *) - (* let v = *) - (* if SMap.mem const_name !env_const then *) - (* SMap.find var *) - (* else *) - (* raise (Constdef_Exception const_name) *) - - (* FModal (m, step f) *) - (* | FInvModal (m, f) -> FInvModal (m, step f) *) - (* | FVar v -> FVar v *) - (* | FMu (x, f) -> FMu (x, step f) *) - (* | FNu (x, f) -> FNu (x, step f) *) - (* | FProp (s, il) -> *) - (* if Hashtbl.mem props s then *) - (* let (vars, formula) = Hashtbl.find props s in *) - (* substitute formula @@ List.combine vars il *) - (* else *) - (* raise (Unbound_prop s) *) - (* in *) - (* Format.printf "Preformula received :\n%s@." @@ string_of_formula pf; *) - (* let res = step pf in *) - (* Format.printf "Result :\n%s@." @@ string_of_formula res; *) - (* res *) (** Local model checker *) From 61b0d4cbfc072558b646bc0037ca190709b58d68 Mon Sep 17 00:00:00 2001 From: Pierrick Couderc Date: Thu, 7 Nov 2013 21:31:47 +0100 Subject: [PATCH 19/26] Added weak transitions in local checker --- src/Formula.ml | 10 +++++--- src/Semop.ml | 66 +++++++++++++++++++++++++------------------------- 2 files changed, 40 insertions(+), 36 deletions(-) diff --git a/src/Formula.ml b/src/Formula.ml index 607fcb6..17f3ddd 100644 --- a/src/Formula.ml +++ b/src/Formula.ml @@ -396,8 +396,11 @@ let formula_of_preformula pf = (** Local model checker *) (** takes a normalized processor *) -let compute_derivation = - Semop.derivatives global_definition_map +let compute_derivation s = + if s = Weak then + Semop.weak_transitions false global_definition_map + else + Semop.derivatives global_definition_map exception Impossible_transition @@ -466,7 +469,8 @@ let handle_check_local form proc = if not r1 || r2 then true, t1 else false, t1 | FModal (m, f) -> - let d = compute_derivation proc in + let s,_,_ = m in + let d = compute_derivation s proc in let res = compute_modality m d in if TSet.is_empty res then (not @@ diamond m, trace) else if diamond m then diff --git a/src/Semop.ml b/src/Semop.ml index 046c268..3c64cd9 100644 --- a/src/Semop.ml +++ b/src/Semop.ml @@ -52,9 +52,9 @@ module BSet = Set.Make ( end ) -let label_of_prefix =function +let label_of_prefix =function | Tau -> T_Tau | In n -> T_In n | Out n -> T_Out n - + let derivatives defs ((orig_res, orig_np) as orig_nproc) = let restrict res derivs = @@ -90,7 +90,7 @@ let derivatives defs ((orig_res, orig_np) as orig_nproc) = restrict body_res derivs | NPrefix (pref, np) -> TSet.singleton (orig_nproc, label_of_prefix pref, renormalize(res,np)) - | NRename (var,name,np) -> + | NRename (var,name,np) -> let derivs = f res np in renames var name derivs @@ -127,9 +127,9 @@ let derivatives defs ((orig_res, orig_np) as orig_nproc) = in let (_, new_in, new_in_res) = SSet.fold folder_in in_forbid (0, dst, in_res) - (*We rename all the names (at depth 1) + (*We rename all the names (at depth 1) of dst in folder_in by the new name - *) + *) in let folder_oths name (cnt, acc_oths, acc_oths_res) = let rec gen_name n = @@ -264,8 +264,8 @@ let name_of_pfix = function | Tau -> "" | In n -> n | Out n -> n - -let rename_pfix oldp n = + +let rename_pfix oldp n = match oldp with | Tau -> Tau | In _ -> In n @@ -292,14 +292,14 @@ and pmap_add_val map key v = let is_restricted rest pf = SSet.mem (name_of_pfix pf) rest -let prefix_of_label = function +let prefix_of_label = function | T_Tau -> Tau | T_In n -> In n | T_Out n -> Out n - + let weak_derivatives tau_only defs (orig_restrict, p) : PSet.t PrefixMap.t = let rec weak_deriv_aux pfix_key entry_map (restrict, p) = let get_set key = - try + try PrefixMap.find key entry_map with Not_found -> PSet.empty @@ -314,7 +314,7 @@ let weak_derivatives tau_only defs (orig_restrict, p) : PSet.t PrefixMap.t = | NSilent -> add_val pfix_key NSilent | NPrefix (pfix, p') -> (match pfix with - | Tau -> + | Tau -> if in_map pfix_key p' then entry_map else @@ -332,14 +332,14 @@ let weak_derivatives tau_only defs (orig_restrict, p) : PSet.t PrefixMap.t = ) | NSum p_list -> List.fold_left (fun m p -> weak_deriv_aux pfix_key m (restrict, p)) entry_map p_list - - | NPar _ -> + + | NPar _ -> let a_suivre = ref [] in let rmap = ref entry_map in let follow = function (_, lbl, pr') -> let a = prefix_of_label lbl in match (pfix_key, a) with - | Tau, pfix | pfix, Tau -> + | Tau, pfix | pfix, Tau -> if not (pmap_in_map !rmap pfix pr') then (a_suivre:= (pr', pfix) ::!a_suivre; rmap:= pmap_add_val !rmap pfix pr') @@ -349,12 +349,12 @@ let weak_derivatives tau_only defs (orig_restrict, p) : PSet.t PrefixMap.t = (a_suivre:= (pr', Tau) ::!a_suivre; rmap:= pmap_add_val !rmap Tau pr') in - let pl = TSet.elements (derivatives defs (restrict, p)) in - (* Nous avions commencé par écrire notre fonction dans l'optique de ne - pas utiliser derivatives. Cependant à la fin on s'est retrouvé face au problème + let pl = TSet.elements (derivatives defs (restrict, p)) in + (* Nous avions commencé par écrire notre fonction dans l'optique de ne + pas utiliser derivatives. Cependant à la fin on s'est retrouvé face au problème de l'extraction des restrictions dans le cas parallèle. Par manque de temps, nous avons du nous résoudre à utiliser derivatives. - + Vous pourrez trouvez nos essais dans Semop_abandon.ml Notament notre version de derivatives, réservée au cas parallele: par_derivatives *) @@ -363,8 +363,8 @@ let weak_derivatives tau_only defs (orig_restrict, p) : PSet.t PrefixMap.t = else List.iter follow pl); List.fold_left (fun m (p,a) -> weak_deriv_aux a m p) !rmap !a_suivre - - | NCall (name, args) -> + + | NCall (name, args) -> let def_sign = string_of_def_header (Definition(name,args,Silent)) in let Definition (_, _, body) = try Hashtbl.find defs def_sign @@ -378,7 +378,7 @@ let weak_derivatives tau_only defs (orig_restrict, p) : PSet.t PrefixMap.t = | NRename (old, newn, p') -> (*ici on fait un appel réccursif avec une map vide et on trie à la sortie*) let m = weak_deriv_aux pfix_key PrefixMap.empty (restrict, p') - and merger _ s1 s2 = + and merger _ s1 s2 = match s1,s2 with None, Some s -> Some s | Some s, None -> Some s @@ -390,17 +390,17 @@ let weak_derivatives tau_only defs (orig_restrict, p) : PSet.t PrefixMap.t = and find_rename f m = try let s = PrefixMap.find (f old) m in - let s' = - try + let s' = + try PrefixMap.find (f newn) m with Not_found -> PSet.empty - in + in PrefixMap.add (f newn) (PSet.union s s') (PrefixMap.remove (f old) m) - with + with Not_found -> m in - let m'= PrefixMap.map package_set (find_rename (fun x -> Out x) + let m'= PrefixMap.map package_set (find_rename (fun x -> Out x) (find_rename (fun x -> In x) m)) in PrefixMap.merge merger m' entry_map in @@ -408,16 +408,16 @@ let weak_derivatives tau_only defs (orig_restrict, p) : PSet.t PrefixMap.t = let derivs = PrefixMap.filter (fun k _ -> not (is_restricted orig_restrict k)) derivs in pmap_add_val derivs Tau (orig_restrict, p) - + let printPfixMap map = let b = PrefixMap.bindings map in - let print_b (k, s) = + let print_b (k, s) = let l = PSet.elements s in let arrow = Printf.sprintf "==%s==>" (string_of_prefix k) in List.iter (fun p -> print_string arrow; print_endline (string_of_nprocess p)) l in - List.iter print_b b + List.iter print_b b let construct_weak_bisimilarity defs nproc1 nproc2 = @@ -429,9 +429,9 @@ let construct_weak_bisimilarity defs nproc1 nproc2 = let d1s = derivatives defs np1 in let d2s = derivatives defs np2 in - + let folder wds inv (_, lab, dstx) acc_bsm = - let dys = + let dys = try PrefixMap.find (prefix_of_label lab) wds with Not_found -> failwith "Bad path" in @@ -450,7 +450,7 @@ let construct_weak_bisimilarity defs nproc1 nproc2 = in search dys in - TSet.fold (folder wd2s false) d1s + TSet.fold (folder wd2s false) d1s (TSet.fold (folder wd1s true) d2s bsm) in try construct (BSet.singleton (nproc1, nproc2)) nproc1 nproc2 @@ -467,7 +467,7 @@ let is_weakly_bisimilar defs nproc1 nproc2 = *) let pmap_to_trans map orig = let bds = PrefixMap.bindings map in - List.fold_left (fun acc (pfix, dst_set) -> + List.fold_left (fun acc (pfix, dst_set) -> let lbl= label_of_prefix pfix in PSet.fold (fun dst acc' -> TSet.add (orig, lbl, dst) acc') dst_set acc) TSet.empty bds From e072da6b67a7f2939dcafbfac005bcc2c535adf2 Mon Sep 17 00:00:00 2001 From: Pierrick Couderc Date: Wed, 13 Nov 2013 14:15:17 +0100 Subject: [PATCH 20/26] Reworked local checker and beginning refactoring --- src/Bdd.ml | 4 + src/Control.ml | 2 +- src/Formula.ml | 205 +++++++------------------------------------------ 3 files changed, 31 insertions(+), 180 deletions(-) diff --git a/src/Bdd.ml b/src/Bdd.ml index bd81052..dd3572b 100644 --- a/src/Bdd.ml +++ b/src/Bdd.ml @@ -2,6 +2,10 @@ type t = {id: int; l: t; r: t; value: int} + +(* type tree = One | Zero | Tree of tree * tree * int *) +(* and t = int * tree *) + let rec null = {id = -1; l = null; r = null; value = -1} let one = {id = 0; l = null; r = null; value = -1} diff --git a/src/Control.ml b/src/Control.ml index c5ef9ad..ea014e4 100644 --- a/src/Control.ml +++ b/src/Control.ml @@ -316,6 +316,6 @@ let handle_prop = Formula.add_prop let handle_check_local = - Formula.handle_check_local + Check.handle_check_local let handle_check_global _ _ = failwith "TODO: handle_check_global" diff --git a/src/Formula.ml b/src/Formula.ml index 17f3ddd..46acc2c 100644 --- a/src/Formula.ml +++ b/src/Formula.ml @@ -1,13 +1,9 @@ (*** Representation of mu-calculus formulae ***) open Printf - +open Semop open Presyntax open Utils -open Global -open Normalize -open Semop -open Bdd type fprefix = | FIn of string @@ -109,8 +105,8 @@ type formula = | FInvModal of modality * formula | FProp of string * (string list) | FVar of string - | FMu of string * formula - | FNu of string * formula + | FMu of string * PSet.t * formula + | FNu of string * PSet.t * formula | FNot of formula (* considered only internaly *) let rec string_of_formula : formula -> string = function @@ -124,8 +120,8 @@ let rec string_of_formula : formula -> string = function | FInvModal(m,f) -> "~" ^ (string_of_modality m) ^ (string_of_formula f) | FProp(prop,params) -> prop ^ (string_of_collection "(" ")" "," (fun s -> s) params) | FVar(var) -> var - | FMu(x,f) -> sprintf "Mu(%s).%s" x (string_of_formula f) - | FNu(x,f) -> sprintf "Nu(%s).%s" x (string_of_formula f) + | FMu(x, _, f) -> sprintf "Mu(%s).%s" x (string_of_formula f) + | FNu(x, _, f) -> sprintf "Nu(%s).%s" x (string_of_formula f) | FNot f -> sprintf "~%s" @@ string_of_formula f type prop = string list * formula @@ -142,7 +138,7 @@ let rec verify_vars f idents = | FAnd (f,g) | FOr (f,g) | FImplies (f,g) -> verify_vars f idents; verify_vars g idents | FModal (_, f) | FInvModal (_, f) -> verify_vars f idents - | FMu (x,f) | FNu (x,f) -> verify_vars f (x :: idents) + | FMu (x,_,f) | FNu (x,_,f) -> verify_vars f (x :: idents) | FProp (_, l) -> List.iter (fun v -> verify_vars (FVar v) idents) l | _ -> () @@ -162,20 +158,28 @@ let reduce f var value = | FVar v -> if v = var then value else FVar v | FTrue | FFalse as f -> f | FPar f -> FPar (step f) + | FNot f -> FNot (step f) | FAnd (f, g) -> FAnd (step f, step g) | FOr (f, g) -> FOr (step f, step g) | FImplies (f, g) -> FImplies (step f, step g) | FModal(m, f) -> FModal (m, step f) | FInvModal (m, f) -> FInvModal (m, step f) - | FMu (x, f) -> FMu (x, step f) - | FNu (x, f) -> FNu (x, step f) - | _ -> assert false (* Technically, no Prop should remain ? *) + | FMu (x, s, f) -> FMu (x, s, step f) + | FNu (x, s, f) -> FNu (x, s, step f) + | _ -> failwith (string_of_formula f) in step f let substitute f sub_list = let rec step sl = function - | FVar v -> FVar (List.assoc v sl) + | FVar v -> + let s = (List.assoc v sl) in + if Hashtbl.mem props s then + let (vars, formula) = Hashtbl.find props s in + if List.length vars = 0 then formula + else FProp (s, vars) + else + FVar v | FTrue | FFalse as f -> f | FPar f -> FPar (step sl f) | FAnd (f, g) -> FAnd (step sl f, step sl g) @@ -183,13 +187,13 @@ let substitute f sub_list = | FImplies (f, g) -> FImplies (step sl f, step sl g) | FModal(m, f) -> FModal (m, step sl f) | FInvModal (m, f) -> FInvModal (m, step sl f) - | FMu (x, f) -> FMu (x, step ((x, x)::sl) f) - | FNu (x, f) -> FNu (x, step ((x, x)::sl) f) + | FMu (x, s, f) -> FMu (x, s, step ((x, x)::sl) f) + | FNu (x, s, f) -> FNu (x, s, step ((x, x)::sl) f) | _ -> assert false (* Technically, no Prop should remain ? *) in step sub_list f -let substitute_prop pf = +let substitute_prop f = let rec step = function | FTrue | FFalse as f -> f | FPar f -> FPar (step f) @@ -199,8 +203,8 @@ let substitute_prop pf = | FModal(m, f) -> FModal (m, step f) | FInvModal (m, f) -> FInvModal (m, step f) | FVar v -> FVar v - | FMu (x, f) -> FMu (x, step f) - | FNu (x, f) -> FNu (x, step f) + | FMu (x, s, f) -> FMu (x, s, step f) + | FNu (x, s, f) -> FNu (x, s, step f) | FNot f -> FNot (step f) | FProp (s, il) -> if Hashtbl.mem props s then @@ -209,10 +213,7 @@ let substitute_prop pf = else raise (Unbound_prop s) in - Format.printf "Preformula received :\n%s@." @@ string_of_formula pf; - let res = step pf in - Format.printf "Result :\n%s@." @@ string_of_formula res; - res + step f let substitute_modality m vars = @@ -351,8 +352,8 @@ let formula_of_preformula pf = | PFModal(m, f) -> FModal (substitute_modality m vars, step vars f) | PFInvModal (m, f) -> FInvModal (substitute_modality m vars, step vars f) | PFVar v -> FVar v - | PFMu (x, f) -> FMu (x, step vars f) - | PFNu (x, f) -> FNu (x, step vars f) + | PFMu (x, f) -> FMu (x, PSet.empty, step vars f) + | PFNu (x, f) -> FNu (x, PSet.empty, step vars f) | PFProp (s, il) -> if Hashtbl.mem props s then let (vars, formula) = Hashtbl.find props s in @@ -392,157 +393,3 @@ let formula_of_preformula pf = let res = step SMap.empty pf in Format.printf "Result :\n%s@." @@ string_of_formula res; res - -(** Local model checker *) - -(** takes a normalized processor *) -let compute_derivation s = - if s = Weak then - Semop.weak_transitions false global_definition_map - else - Semop.derivatives global_definition_map - -exception Impossible_transition - -let compute_modality modl tr = - - let get_matching_derivations_named act tr acc = - TSet.fold - (fun t acc -> - let _, pre, _ = t in - match act, pre with - | FIn s, T_In n | FOut s, T_Out n -> - if s = n then TSet.add t acc else acc - | _, T_Tau -> TSet.add t acc - | _, _ -> acc) - tr - acc - in - - let get_matching_derivations io tr = - TSet.fold - (fun t acc -> - let _, pre, _ = t in - match io, pre with - | In, T_In _ | Out, T_Out _ | Any, T_Tau | _, T_Tau -> TSet.add t acc - | _, _ -> acc) - tr - TSet.empty - in - - match modl with - | Strong, _, Prefix acts -> - List.fold_left - (fun acc a -> - get_matching_derivations_named a tr acc) - TSet.empty - acts - | Strong, _, (_ as io) -> - Format.printf "%s@." @@ string_of_modality modl; - get_matching_derivations io tr - | Weak, _, _ -> failwith "Weak not implemented yet" - - -let handle_check_local form proc = - let proc = normalize proc in - let pset = PSet.empty in - - let rec step proc pset trace = function - | FTrue -> true, trace - | FFalse -> false, trace - | FPar f -> step proc pset trace f - | FNot f -> let r, t = step proc pset trace f in - (not r, t) - | FAnd (f, g) -> let r1, t1 = step proc pset trace f in - let r2, t2 = step proc pset trace g in - if r1 && r2 then true, t1 - else if r1 then false, t2 - else false, t1 - | FOr (f, g) -> let r1, t1 = step proc pset trace f in - let r2, _ = step proc pset trace g in - if r1 || r2 then true, t1 - else false, t1 (* both can be considered as an incorrect - trace *) - | FImplies (f, g) -> - let r1, t1 = step proc pset trace f in - let r2, _t2 = step proc pset trace g in - if not r1 || r2 then true, t1 - else false, t1 - | FModal (m, f) -> - let s,_,_ = m in - let d = compute_derivation s proc in - let res = compute_modality m d in - if TSet.is_empty res then (not @@ diamond m, trace) - else if diamond m then - TSet.fold - (fun (_, m, p') (r, t) -> - if r then r,t (* no need to test the transition if one is - true *) - else step p' pset (m::t) f) - res - (false, trace) - else - TSet.fold - (fun (_, m, p') (r, t) -> - if not r then r,t (* no need to test the transition if one is - false *) - else step p' pset (m::t) f) - res - (true, trace) - | FInvModal(m, f) -> - let r, t = step proc pset trace @@ FModal (m,f) in - (not r, t) - | FNu (x, f) as nu -> if PSet.mem proc pset then true, trace - else - let f = reduce f x nu in - let pset = PSet.add proc pset in - step proc pset trace f - - | FMu (x, f) -> - let nu = FNu(x, f) in - let f' = reduce f x @@ FNot nu in - let f = FNot f' in - let r, t = step proc pset trace f in - not r, t - - | _ -> assert false - in - let (res, trace) = step proc pset [] form in - if res then - Format.printf "The processor given matches the model@." - else - begin - let t = List.rev trace |> - List.fold_left (fun acc t -> - Format.sprintf "%s --> %s" acc @@ string_of_label t) "" - in - let t = Format.sprintf "%s --> " t in - Format.printf "Doesn't match, here is why: @.%s@." t - end - -let bdd_of_formula f = - (* let fix f l = assert false in *) - let implies b1 b2 = (not b1) || b2 in - let xor b1 b2 = ((not b1) && b2) || (b1 && (not b2)) in - let _env = [] in - let rec step f env = - match f with - | FTrue -> one - | FFalse -> zero - | FNot f -> apply xor (step f env) one - | FAnd (f1, f2) -> - let b1 = step f1 env in - let b2 = step f2 env in - apply ( && ) b1 b2 - | FOr (f1, f2) -> - let b1 = step f1 env in - let b2 = step f2 env in - apply ( || ) b1 b2 - | FImplies (f1, f2) -> - let b1 = step f1 env in - let b2 = step f2 env in - apply implies b1 b2 - | FModal (_m, _f) -> assert false - | _ -> assert false - in - step f From 29846ff912242604e04389192846c1e6dd6d51cd Mon Sep 17 00:00:00 2001 From: Pierrick Couderc Date: Sun, 17 Nov 2013 09:56:29 +0100 Subject: [PATCH 21/26] Some tests for global, nothing conclusive --- src/Bdd.ml | 2 ++ src/Control.ml | 17 +++------------- src/Formula.ml | 40 +++++++++++++++++++++++++++++++++++-- src/Lexer.mll | 5 ++--- src/Parser.mly | 8 ++++---- src/examples/mucalculus.ccs | 12 +++++++++++ 6 files changed, 61 insertions(+), 23 deletions(-) create mode 100644 src/examples/mucalculus.ccs diff --git a/src/Bdd.ml b/src/Bdd.ml index dd3572b..ed9fbd7 100644 --- a/src/Bdd.ml +++ b/src/Bdd.ml @@ -24,6 +24,8 @@ module S = struct end +module HashedBdd = S + module HBdd = Hashtbl.Make(S) let create = diff --git a/src/Control.ml b/src/Control.ml index ea014e4..fdabff6 100644 --- a/src/Control.ml +++ b/src/Control.ml @@ -300,20 +300,9 @@ let handle_tderiv p = common_deriv (weak_derivatives true) printPfixMap "tderiv" (*** Mu-Calculus part *) -let handle_prop = - (* let namelist = *) - (* if List.length il <> 0 then *) - (* let il = List.rev il in *) - (* "(" ^ (List.fold_left *) - (* (fun n acc -> acc ^ ", " ^ n) *) - (* (List.hd il) *) - (* (List.tl il)) *) - (* ^ ")" *) - (* else "()" *) - (* in *) - (* Formula.string_of_formula f |> *) - (* Format.printf "Prop : %s %s : %s@." n namelist; *) - Formula.add_prop +let handle_prop name idents formula = + Formula.add_prop name idents formula(* ; *) + (* ignore (Check.bdd_of_formula formula name) *) let handle_check_local = Check.handle_check_local diff --git a/src/Formula.ml b/src/Formula.ml index 46acc2c..f3fa73d 100644 --- a/src/Formula.ml +++ b/src/Formula.ml @@ -7,8 +7,8 @@ open Utils type fprefix = | FIn of string -| FInVar of string -| FOut of string +| FInVar of string * string +| FOut of string * string | FOutVar of string | FTau @@ -152,6 +152,42 @@ let add_prop name idents formula = Hashtbl.add props name (idents, formula) end +module IMap = Map.Make( + struct + type t = int + let compare = compare + end) + + +let alpha_convert f = + let i = ref 0 in + let rec step f env = + match f with + | FVar v -> + if SMap.mem v env then FVar (SMap.find v env) + else FVar v + + | FTrue | FFalse as f -> f + | FPar f -> FPar (step f env) + | FNot f -> FNot (step f env) + | FAnd (f, g) -> FAnd (step f env, step g env) + | FOr (f, g) -> FOr (step f env, step g env) + | FImplies (f, g) -> FImplies (step f env, step g env) + | FModal(m, f) -> FModal (m, step f env) + | FInvModal (m, f) -> FInvModal (m, step f env) + | FMu (x, s, f) -> + let nx = x ^ "_" ^ (string_of_int !i) in + let env = SMap.add x nx env in + incr i; + FMu (nx, s, step f env) + | FNu (x, s, f) -> + let nx = x ^ "_" ^ (string_of_int !i) in + let env = SMap.add x nx env in + incr i; + FNu (x, s, step f env) + | FProp (_,_) -> f + in + step f SMap.empty let reduce f var value = let rec step = function diff --git a/src/Lexer.mll b/src/Lexer.mll index 1d8a3b1..432d00b 100644 --- a/src/Lexer.mll +++ b/src/Lexer.mll @@ -27,8 +27,6 @@ let r_if = "if" let r_then = "then" let r_else = "else" -let r_in = "in" - let r_const = "const" let r_type = "type" @@ -65,6 +63,7 @@ let tild = "~" let semicol = ";" let ws = (['\t' ' ']*) let colon = ':' +let whereas = "|" let implies_1 = "==>" let implies_2 = "=>" @@ -136,7 +135,6 @@ let nu_3 = "NU" | r_if { IF } | r_then { THEN } | r_else { ELSE } - | r_in { INDEF } | r_const { CONSTDEF } | r_type { TYPEDEF } | dotdot { DOTDOT } @@ -175,6 +173,7 @@ let nu_3 = "NU" | cmd_free { FREE } | cmd_bound { BOUND } | cmd_names { NAMES } + | whereas { WHEREAS } | implies_1 { IMPLIES } | implies_2 { IMPLIES } diff --git a/src/Parser.mly b/src/Parser.mly index e28d19f..4eb8513 100644 --- a/src/Parser.mly +++ b/src/Parser.mly @@ -76,7 +76,7 @@ /* punctuation */ %token LPAREN RPAREN LBRACKET RBRACKET COMMA EQUAL EQEQ TILD COLON -%token IF THEN ELSE INF SUP INFEQ SUPEQ DIFF DOTDOT LACCOL RACCOL INDEF +%token IF THEN ELSE INF SUP INFEQ SUPEQ DIFF DOTDOT LACCOL RACCOL WHEREAS /* operators */ %token PAR PLUS DOT OUT IN MINUS DIV MULT MOD AND OR NOT IMPLIES @@ -90,7 +90,7 @@ %left MULT , DIV , MOD %right COMMA %left OUT IN -%left INDEF +%right WHEREAS %nonassoc UNARY @@ -379,8 +379,8 @@ | IDENT LPAREN RPAREN { PFProp($1, []) } | IDENT LPAREN list_of_names RPAREN { PFProp($1,$3) } | IDENT { PFVar($1) } - | FORALL param COMMA expr INDEF formula { PFForall($2, $4, $6) } - | EXISTS param COMMA expr INDEF formula { PFExists($2, $4, $6) } + | FORALL param COMMA expr WHEREAS formula { PFForall($2, $4, $6) } + | EXISTS param COMMA expr WHEREAS formula { PFExists($2, $4, $6) } modality: | INF list_of_prefixes SUP diff --git a/src/examples/mucalculus.ccs b/src/examples/mucalculus.ccs new file mode 100644 index 0000000..9f70ae1 --- /dev/null +++ b/src/examples/mucalculus.ccs @@ -0,0 +1,12 @@ +def send = a?, send2; +def send2 = b!,(d?, send + c?, send2); +def med = b?, (c!, med + e!, med); +def rec = e?,f?,d!, rec; +def prot = new(b,c,d,e)[send || med || rec]; +prop inv(A) = Nu(X).(A and [.]X); +prop ev(B) = Mu(Y).(Y or ((<.>true) and [.]Y)); +prop tmp1() = true; +prop tmp2() = [f?] ev(tmp1); +prop p2() = inv(tmp2); + +checklocal p2() |- prot; \ No newline at end of file From 4df6fc7ae6286ea13cea9baf68bd8a106f836d45 Mon Sep 17 00:00:00 2001 From: Pierrick Couderc Date: Fri, 22 Nov 2013 14:55:06 +0100 Subject: [PATCH 22/26] Replaced list of names by list of formulas in prop --- src/Control.ml | 1 + src/Formula.ml | 67 +++++++++++++++++++++++-------------- src/Parser.mly | 6 +++- src/examples/mucalculus.ccs | 7 ++-- 4 files changed, 50 insertions(+), 31 deletions(-) diff --git a/src/Control.ml b/src/Control.ml index fdabff6..accd484 100644 --- a/src/Control.ml +++ b/src/Control.ml @@ -301,6 +301,7 @@ let handle_tderiv p = common_deriv (weak_derivatives true) printPfixMap "tderiv" (*** Mu-Calculus part *) let handle_prop name idents formula = + Formula.add_prop name idents formula(* ; *) (* ignore (Check.bdd_of_formula formula name) *) diff --git a/src/Formula.ml b/src/Formula.ml index f3fa73d..46a690c 100644 --- a/src/Formula.ml +++ b/src/Formula.ml @@ -7,8 +7,8 @@ open Utils type fprefix = | FIn of string -| FInVar of string * string -| FOut of string * string +| FInVar of string +| FOut of string | FOutVar of string | FTau @@ -66,7 +66,7 @@ type preformula = | PFImplies of preformula * preformula | PFModal of modality * preformula | PFInvModal of modality * preformula - | PFProp of string * (string list) + | PFProp of string * (preformula list) | PFVar of string | PFMu of string * preformula | PFNu of string * preformula @@ -82,7 +82,11 @@ let rec string_of_preformula : preformula -> string = function | PFImplies(f,g) -> sprintf "(%s ==> %s)" (string_of_preformula f) (string_of_preformula g) | PFModal(m,f) -> (string_of_modality m) ^ (string_of_preformula f) | PFInvModal(m,f) -> "~" ^ (string_of_modality m) ^ (string_of_preformula f) - | PFProp(prop,params) -> prop ^ (string_of_collection "(" ")" "," (fun s -> s) params) + | PFProp(prop,params) -> prop ^ + (string_of_collection "(" ")" "," + (fun s -> + string_of_preformula s) + params) | PFVar(var) -> var | PFMu(x,f) -> sprintf "Mu(%s).%s" x (string_of_preformula f) | PFNu(x,f) -> sprintf "Nu(%s).%s" x (string_of_preformula f) @@ -103,7 +107,7 @@ type formula = | FImplies of formula * formula | FModal of modality * formula | FInvModal of modality * formula - | FProp of string * (string list) + | FProp of string * (formula list) | FVar of string | FMu of string * PSet.t * formula | FNu of string * PSet.t * formula @@ -118,7 +122,11 @@ let rec string_of_formula : formula -> string = function | FImplies(f,g) -> sprintf "(%s ==> %s)" (string_of_formula f) (string_of_formula g) | FModal(m,f) -> (string_of_modality m) ^ (string_of_formula f) | FInvModal(m,f) -> "~" ^ (string_of_modality m) ^ (string_of_formula f) - | FProp(prop,params) -> prop ^ (string_of_collection "(" ")" "," (fun s -> s) params) + | FProp(prop,params) -> + prop ^ (string_of_collection "(" ")" "," + (fun s -> + string_of_formula s) + params) | FVar(var) -> var | FMu(x, _, f) -> sprintf "Mu(%s).%s" x (string_of_formula f) | FNu(x, _, f) -> sprintf "Nu(%s).%s" x (string_of_formula f) @@ -139,7 +147,7 @@ let rec verify_vars f idents = verify_vars f idents; verify_vars g idents | FModal (_, f) | FInvModal (_, f) -> verify_vars f idents | FMu (x,_,f) | FNu (x,_,f) -> verify_vars f (x :: idents) - | FProp (_, l) -> List.iter (fun v -> verify_vars (FVar v) idents) l + (* | FProp (_, l) -> List.iter (fun v -> verify_vars (FVar v) idents) l *) | _ -> () (** val add_prop : string -> string list -> formula -> unit *) @@ -208,14 +216,14 @@ let reduce f var value = let substitute f sub_list = let rec step sl = function - | FVar v -> - let s = (List.assoc v sl) in - if Hashtbl.mem props s then - let (vars, formula) = Hashtbl.find props s in - if List.length vars = 0 then formula - else FProp (s, vars) - else - FVar v + | FVar v -> List.assoc v sl + (* let s = (List.assoc v sl) in *) + (* if Hashtbl.mem props s then *) + (* let (vars, formula) = Hashtbl.find props s in *) + (* if List.length vars = 0 then formula *) + (* else FProp (s, vars) *) + (* else *) + (* FVar v *) | FTrue | FFalse as f -> f | FPar f -> FPar (step sl f) | FAnd (f, g) -> FAnd (step sl f, step sl g) @@ -223,8 +231,8 @@ let substitute f sub_list = | FImplies (f, g) -> FImplies (step sl f, step sl g) | FModal(m, f) -> FModal (m, step sl f) | FInvModal (m, f) -> FInvModal (m, step sl f) - | FMu (x, s, f) -> FMu (x, s, step ((x, x)::sl) f) - | FNu (x, s, f) -> FNu (x, s, step ((x, x)::sl) f) + | FMu (x, s, f) -> FMu (x, s, step ((x, FVar x)::sl) f) + | FNu (x, s, f) -> FNu (x, s, step ((x, FVar x)::sl) f) | _ -> assert false (* Technically, no Prop should remain ? *) in step sub_list f @@ -242,10 +250,10 @@ let substitute_prop f = | FMu (x, s, f) -> FMu (x, s, step f) | FNu (x, s, f) -> FNu (x, s, step f) | FNot f -> FNot (step f) - | FProp (s, il) -> + | FProp (s, fl) -> if Hashtbl.mem props s then let (vars, formula) = Hashtbl.find props s in - substitute formula @@ List.combine vars il + substitute formula @@ List.combine vars fl else raise (Unbound_prop s) in @@ -262,12 +270,14 @@ let substitute_modality m vars = match fpref with | FTau -> FTau | FOut _ | FIn _ -> fpref - | FInVar s -> Format.printf "I found a variable!@."; + | FInVar s -> if SMap.mem s vars then - FIn (s ^ "_" ^ (string_of_int @@ int_of_value @@ (SMap.find s vars))) + let n = String.sub s 1 @@ String.length s - 1 in + FIn (n ^ "_" ^ (string_of_int @@ int_of_value @@ (SMap.find s vars))) else fpref | FOutVar s -> if SMap.mem s vars then - FIn (s ^ "_" ^ (string_of_int @@ int_of_value @@ (SMap.find s vars))) + let n = String.sub s 1 @@ String.length s - 1 in + FOut (n ^ "_" ^ (string_of_int @@ int_of_value @@ (SMap.find s vars))) else fpref) l) in @@ -279,6 +289,7 @@ let formula_of_preformula pf = let compute_param p = match p with | PParamVar (n, t) -> + if not @@ SMap.mem t !env_type then failwith "Not found" else n, value_list (SMap.find t !env_type) | _ -> failwith (Format.sprintf "Unusable param for mu-calculus:%s@." @@ string_of_preparam p) @@ -290,7 +301,10 @@ let formula_of_preformula pf = | PInt i -> Int i | PName str -> Name str | PConst name -> Int (SMap.find name !env_const) - | PVar name -> (SMap.find name vars) + | PVar name -> if not @@ SMap.mem name vars then + failwith "Var not found" + else + (SMap.find name vars) | PNot pexpr -> let b = bool_of_value (test_expr vars pexpr) in Bool (not b) | PAnd (preexpr1, preexpr2) -> let b1 = bool_of_value (test_expr vars preexpr1) @@ -390,10 +404,11 @@ let formula_of_preformula pf = | PFVar v -> FVar v | PFMu (x, f) -> FMu (x, PSet.empty, step vars f) | PFNu (x, f) -> FNu (x, PSet.empty, step vars f) - | PFProp (s, il) -> + | PFProp (s, pfl) -> if Hashtbl.mem props s then - let (vars, formula) = Hashtbl.find props s in - substitute formula @@ List.combine vars il + let (vars', formula) = Hashtbl.find props s in + let fl = List.map (step vars) pfl in + substitute formula @@ List.combine vars' fl else raise (Unbound_prop s) | PFForall (param, expr, f) -> diff --git a/src/Parser.mly b/src/Parser.mly index 4eb8513..bc54593 100644 --- a/src/Parser.mly +++ b/src/Parser.mly @@ -364,6 +364,10 @@ | /* empty */ { [] } | expr list_of_exprs { $1::$2 } + list_of_formulas: + | formula { [$1] } + | formula COMMA list_of_formulas { $1::$3 } + formula: | TRUE { PFTrue } | FALSE { PFFalse } @@ -377,7 +381,7 @@ | MU LPAREN IDENT RPAREN DOT formula { PFMu ($3,$6) } | NU LPAREN IDENT RPAREN DOT formula { PFNu ($3,$6) } | IDENT LPAREN RPAREN { PFProp($1, []) } - | IDENT LPAREN list_of_names RPAREN { PFProp($1,$3) } + | IDENT LPAREN list_of_formulas RPAREN { PFProp($1,$3) } | IDENT { PFVar($1) } | FORALL param COMMA expr WHEREAS formula { PFForall($2, $4, $6) } | EXISTS param COMMA expr WHEREAS formula { PFExists($2, $4, $6) } diff --git a/src/examples/mucalculus.ccs b/src/examples/mucalculus.ccs index 9f70ae1..d5f4448 100644 --- a/src/examples/mucalculus.ccs +++ b/src/examples/mucalculus.ccs @@ -1,3 +1,5 @@ + + def send = a?, send2; def send2 = b!,(d?, send + c?, send2); def med = b?, (c!, med + e!, med); @@ -5,8 +7,5 @@ def rec = e?,f?,d!, rec; def prot = new(b,c,d,e)[send || med || rec]; prop inv(A) = Nu(X).(A and [.]X); prop ev(B) = Mu(Y).(Y or ((<.>true) and [.]Y)); -prop tmp1() = true; -prop tmp2() = [f?] ev(tmp1); -prop p2() = inv(tmp2); -checklocal p2() |- prot; \ No newline at end of file +checklocal inv([f?]ev(true)) |- prot; \ No newline at end of file From 257bff864f294ba198fa011476bdce52eb5ca052 Mon Sep 17 00:00:00 2001 From: Pierrick Couderc Date: Fri, 22 Nov 2013 20:58:31 +0100 Subject: [PATCH 23/26] Global checking : First step ? --- src/Control.ml | 2 +- src/Formula.ml | 20 +++++++++++--------- src/examples/mucalculus.ccs | 37 +++++++++++++++++++++++++++++-------- 3 files changed, 41 insertions(+), 18 deletions(-) diff --git a/src/Control.ml b/src/Control.ml index accd484..761949e 100644 --- a/src/Control.ml +++ b/src/Control.ml @@ -308,4 +308,4 @@ let handle_prop name idents formula = let handle_check_local = Check.handle_check_local -let handle_check_global _ _ = failwith "TODO: handle_check_global" +let handle_check_global = Check.check_global diff --git a/src/Formula.ml b/src/Formula.ml index 46a690c..eb50043 100644 --- a/src/Formula.ml +++ b/src/Formula.ml @@ -37,16 +37,18 @@ type io = type modality = strongness * modal * io +let string_of_io = function + | In -> "?" + | Out -> "!" + | Any -> "." + | Prefix pl -> List.fold_left + (fun acc p -> acc ^ "," ^ (string_of_fprefix p)) + (string_of_fprefix (List.hd pl)) + (List.tl pl) + + let string_of_modality (s, m, io) = - let io = match io with - | In -> "!" - | Out -> "?" - | Any -> "." - | Prefix pl -> List.fold_left - (fun acc p -> acc ^ "," ^ (string_of_fprefix p)) - (string_of_fprefix (List.hd pl)) - (List.tl pl) - in + let io = string_of_io io in match s, m with | Strong, Possibly -> Format.sprintf "<%s>" io | Strong, Necessity -> Format.sprintf "[%s]" io diff --git a/src/examples/mucalculus.ccs b/src/examples/mucalculus.ccs index d5f4448..8d49eef 100644 --- a/src/examples/mucalculus.ccs +++ b/src/examples/mucalculus.ccs @@ -1,11 +1,32 @@ +# Some definitions, as proof of concept +# prop p1() = true; +# prop p2(A) = A; +# prop p3() = true; -def send = a?, send2; -def send2 = b!,(d?, send + c?, send2); -def med = b?, (c!, med + e!, med); -def rec = e?,f?,d!, rec; -def prot = new(b,c,d,e)[send || med || rec]; -prop inv(A) = Nu(X).(A and [.]X); -prop ev(B) = Mu(Y).(Y or ((<.>true) and [.]Y)); +# Check if, after every action, there is no out +prop noIn() = [.][?]false; -checklocal inv([f?]ev(true)) |- prot; \ No newline at end of file +def proc1 = a!, b!, 0; + +# Returns OK +checklocal noIn() |- proc1; + +# After the first action, there is a out +def proc2 = a!, b?, 0; + +# Returns false +checklocal noIn() |- proc2; + +prop possibly(A) = Mu(X).A or <.> X; +prop always(A) = Nu(X). A and [.] X; +prop eventually(A) = Mu(X). A or ((<.>true) and [.] X); + +prop deadlock() = [.] false; + +# Will never end +def Loop = a!, Loop; + +checklocal possibly(deadlock()) |- Loop; +checklocal always(deadlock()) |- Loop; +checklocal eventually(deadlock()) |- Loop; \ No newline at end of file From a4e7dd884fb5ebebe33b4cf91de975522e69c06d Mon Sep 17 00:00:00 2001 From: Pierrick Couderc Date: Sun, 24 Nov 2013 14:14:54 +0100 Subject: [PATCH 24/26] Added comments, examples and corrected the local Mu computation --- src/Formula.ml | 36 ++++++++++++++++++---------- src/examples/mucalculus.ccs | 48 ++++++++++++++++++++++++++++++++----- 2 files changed, 66 insertions(+), 18 deletions(-) diff --git a/src/Formula.ml b/src/Formula.ml index eb50043..757d774 100644 --- a/src/Formula.ml +++ b/src/Formula.ml @@ -5,6 +5,7 @@ open Semop open Presyntax open Utils +(** Type of "named" prefix *) type fprefix = | FIn of string | FInVar of string @@ -12,6 +13,8 @@ type fprefix = | FOutVar of string | FTau +(** Takes a preprefix and gives its corresponding fprefix to be used correctly in + the formula *) let fprefix_of_preprefix = function | PIn (PName n) -> FIn n | POut (PName n) -> FOut n @@ -27,9 +30,11 @@ let string_of_fprefix = function | FOutVar n -> "var:" ^ n ^ "!" | FTau -> "tau" +(** Transform a preprefix list into a fprefix list *) let parse_preprefix_list = List.map fprefix_of_preprefix +(** Types used to represent modalities *) type strongness = Strong | Weak type modal = Possibly | Necessity type io = @@ -59,6 +64,7 @@ let diamond = function | _, Possibly, _ -> true | _, _, _ -> false +(** Type to represent preformula, particularely the ForAll and Exists terms *) type preformula = | PFTrue | PFFalse @@ -99,7 +105,7 @@ let rec string_of_preformula : preformula -> string = function sprintf "(exists %s, %s in %s)" (string_of_preparam par) (string_of_preexpr pe) (string_of_preformula f) - +(** Similar to preformula, without the quantifying clauses *) type formula = | FTrue | FFalse @@ -134,6 +140,7 @@ let rec string_of_formula : formula -> string = function | FNu(x, _, f) -> sprintf "Nu(%s).%s" x (string_of_formula f) | FNot f -> sprintf "~%s" @@ string_of_formula f +(** A prop is a list of bound variables and its formulas *) type prop = string list * formula let props : (string, prop) Hashtbl.t = Hashtbl.create 53 @@ -142,6 +149,7 @@ exception Formdef_exception of string exception Unbound_variable of string exception Unbound_prop of string +(** Will verify if every variable is bound in the prop *) let rec verify_vars f idents = match f with | FVar v -> if not (List.mem v idents) then raise (Unbound_variable v) @@ -168,7 +176,8 @@ module IMap = Map.Make( let compare = compare end) - +(** Converts a variable name to avoid multiple definitions. Never used however, + since the fixed points variables are always in tail position *) let alpha_convert f = let i = ref 0 in let rec step f env = @@ -199,6 +208,7 @@ let alpha_convert f = in step f SMap.empty +(** Replaces a var in f by the formula given *) let reduce f var value = let rec step = function | FVar v -> if v = var then value else FVar v @@ -216,16 +226,11 @@ let reduce f var value = in step f +(** Replaces each Var by its correspondance. Works as a reduce for multiple + vars. Assumes each variable is correctly bound *) let substitute f sub_list = let rec step sl = function | FVar v -> List.assoc v sl - (* let s = (List.assoc v sl) in *) - (* if Hashtbl.mem props s then *) - (* let (vars, formula) = Hashtbl.find props s in *) - (* if List.length vars = 0 then formula *) - (* else FProp (s, vars) *) - (* else *) - (* FVar v *) | FTrue | FFalse as f -> f | FPar f -> FPar (step sl f) | FAnd (f, g) -> FAnd (step sl f, step sl g) @@ -239,6 +244,7 @@ let substitute f sub_list = in step sub_list f +(** Inlines a prop call *) let substitute_prop f = let rec step = function | FTrue | FFalse as f -> f @@ -261,7 +267,7 @@ let substitute_prop f = in step f - +(** Renames a modality *) let substitute_modality m vars = let rename_modal (s,mo,io) = match io with @@ -285,7 +291,7 @@ let substitute_modality m vars = in rename_modal m - +(** Computes a preformula quantified into a correct formula *) let formula_of_preformula pf = let open Syntax in let compute_param p = @@ -297,6 +303,8 @@ let formula_of_preformula pf = (Format.sprintf "Unusable param for mu-calculus:%s@." @@ string_of_preparam p) in + (* From Presyntax, modified not to used a global hashtbl, but a local map + instead *) let rec test_expr vars = function | PTrue -> Bool true | PFalse -> Bool false @@ -406,13 +414,17 @@ let formula_of_preformula pf = | PFVar v -> FVar v | PFMu (x, f) -> FMu (x, PSet.empty, step vars f) | PFNu (x, f) -> FNu (x, PSet.empty, step vars f) - | PFProp (s, pfl) -> + + | PFProp (s, pfl) -> (* inlining *) if Hashtbl.mem props s then let (vars', formula) = Hashtbl.find props s in let fl = List.map (step vars) pfl in substitute formula @@ List.combine vars' fl else raise (Unbound_prop s) + +(* The next two cases compute the qunatification, modifying the modalities to + the value given by the quantification *) | PFForall (param, expr, f) -> let n, val_list = compute_param param in List.fold_left diff --git a/src/examples/mucalculus.ccs b/src/examples/mucalculus.ccs index 8d49eef..4789234 100644 --- a/src/examples/mucalculus.ccs +++ b/src/examples/mucalculus.ccs @@ -5,28 +5,64 @@ # prop p3() = true; # Check if, after every action, there is no out -prop noIn() = [.][?]false; +#prop noIn() = [.][?]false; -def proc1 = a!, b!, 0; +#def proc1 = a!, b!, 0; # Returns OK -checklocal noIn() |- proc1; +#checklocal noIn() |- proc1; # After the first action, there is a out -def proc2 = a!, b?, 0; +#def proc2 = a!, b?, 0; # Returns false -checklocal noIn() |- proc2; +#checklocal noIn() |- proc2; + +# Exercise 1 of TD5 +prop A() = ((true) or (true)); +prop B() = [tau]((true) or (true)); +prop C() = ([a!]false) and ([b?] false); + +def pA = tau, a!, 0 + tau, c!, 0 + a!, 0; + +# Should returns OK +checklocal A() |- pA; + +# Should returns False +checklocal B() |- pA; + +# Should returns False +checklocal C() |- pA; + +# Exercice 5 of TD5 prop possibly(A) = Mu(X).A or <.> X; prop always(A) = Nu(X). A and [.] X; prop eventually(A) = Mu(X). A or ((<.>true) and [.] X); prop deadlock() = [.] false; +prop cont() = <.> true; # Will never end def Loop = a!, Loop; +# Returns false checklocal possibly(deadlock()) |- Loop; + +# OK +checklocal always(cont()) |- Loop; + +# Should returns False checklocal always(deadlock()) |- Loop; -checklocal eventually(deadlock()) |- Loop; \ No newline at end of file + +# OK, since it's a loop +checklocal eventually(cont()) |- Loop; + +# Should return False +checklocal eventually(deadlock()) |- Loop; + +# This example was given in the Exercise 5 +prop correct() = ([start!]true) => eventually((true) or ([.]false)); +def p = start!, a!, b!, p2; +def p2 = c?, p + stop!, 0; +checklocal correct() |- p; From c2b6e70761a8d306c1596fb2687fab07d1f5f019 Mon Sep 17 00:00:00 2001 From: Pierrick Couderc Date: Sun, 24 Nov 2013 15:49:07 +0100 Subject: [PATCH 25/26] Added some examples --- src/examples/mucalculus.ccs | 31 ++++++++++++++++++++++++------- 1 file changed, 24 insertions(+), 7 deletions(-) diff --git a/src/examples/mucalculus.ccs b/src/examples/mucalculus.ccs index 4789234..c66bf60 100644 --- a/src/examples/mucalculus.ccs +++ b/src/examples/mucalculus.ccs @@ -5,18 +5,18 @@ # prop p3() = true; # Check if, after every action, there is no out -#prop noIn() = [.][?]false; +prop noIn() = Nu(X). ([?]false) and [.]X; -#def proc1 = a!, b!, 0; +def proc1 = a!, b!, proc1; # Returns OK -#checklocal noIn() |- proc1; +checklocal noIn() |- proc1; # After the first action, there is a out -#def proc2 = a!, b?, 0; +def proc2 = a!, b?, proc2; # Returns false -#checklocal noIn() |- proc2; +checklocal noIn() |- proc2; # Exercise 1 of TD5 @@ -63,6 +63,23 @@ checklocal eventually(deadlock()) |- Loop; # This example was given in the Exercise 5 prop correct() = ([start!]true) => eventually((true) or ([.]false)); -def p = start!, a!, b!, p2; +def s = start!, p; +def p = a!, b!, p2; def p2 = c?, p + stop!, 0; -checklocal correct() |- p; +checklocal correct() |- s; + +##### +# Some more examples + +# The process first matches A, and after some time B +prop until(A,B) = Nu(X).(B or (A and [.]X)); + +##### +# Some examples of the mucalulus by value + +type Range = [0..3]; +# The process that does in_0?, in_1? and in_2? +prop fa() = forall $in:Range, $in < 3 | (<<$in?>>true); + +# The processes that does at least out_0!, out_1! or out_2! +prop fa() = exists $out:Range, $out < 3 | (<<$out!>>true); From c5616860f66184b98aaa87dc2fe6e965213af4fc Mon Sep 17 00:00:00 2001 From: Pierrick Couderc Date: Mon, 25 Nov 2013 14:47:50 +0100 Subject: [PATCH 26/26] Added missing files --- src/Check.ml | 498 ++++++++++++++++++++++++++++++++++++++++++++++++++ src/Global.ml | 5 + 2 files changed, 503 insertions(+) create mode 100644 src/Check.ml create mode 100644 src/Global.ml diff --git a/src/Check.ml b/src/Check.ml new file mode 100644 index 0000000..14d0bbe --- /dev/null +++ b/src/Check.ml @@ -0,0 +1,498 @@ +open Formula +open Global +open Semop +open Bdd +open Utils + +(** Local model checker *) + +(** takes a normalized processor *) +let compute_derivation s = + if s = Weak then + Semop.weak_transitions false global_definition_map + else + Semop.derivatives global_definition_map + +exception Impossible_transition + +(* Computes derivations for named actions *) +let get_matching_derivations_named act tr acc = + TSet.fold + (fun t acc -> + let _, pre, _ = t in + match act, pre with + | FIn s, T_In n | FOut s, T_Out n -> + if s = n then TSet.add t acc else acc + | FTau, T_Tau -> TSet.add t acc + | _, _ -> acc) + tr + acc + +(* Computes derivation for "polymorphic" actions *) +let get_matching_derivations io tr = + TSet.fold + (fun t acc -> + let _, pre, _ = t in + match io, pre with + | In, T_In _ | Out, T_Out _ | _, T_Tau | Any, _ -> TSet.add t acc + | _, _ -> acc) + tr + TSet.empty + + +(* Returns the transitions that matches the actions in the modality *) +let compute_modality modl tr = + match modl with + | _, _, Prefix acts -> + List.fold_left + (fun acc a -> + get_matching_derivations_named a tr acc) + TSet.empty + acts + | _, _, (_ as io) -> + get_matching_derivations io tr + +(** Main function for the local checker *) +let handle_check_local form proc = + let proc = Normalize.normalize proc in + + let rec step proc trace = function + | FTrue -> true, trace + + | FFalse -> false, trace + + | FVar v -> failwith (Format.sprintf "This variable is unbound: %s@." v) + + | FPar f -> step proc trace f + + | FNot f -> let r, t = step proc trace f in + (not r, t) + + | FAnd (f, g) -> let r1, t1 = step proc trace f in + let r2, t2 = step proc trace g in + if r1 && r2 then true, t1 + else if r1 then false, t2 + else false, t1 + + | FOr (f, g) -> let r1, t1 = step proc trace f in + let r2, _ = step proc trace g in + if r1 || r2 then true, t1 + else false, t1 (* both can be considered as an incorrect + trace *) + + | FImplies (f, g) -> + let r1, t1 = step proc trace f in + let r2, _t2 = step proc trace g in + not r1 || r2, t1 + + | FModal (m, f) -> + let s,_,_ = m in + let d = compute_derivation s proc in + let res = compute_modality m d in (* gets the transitions corresponding to + the modal *) + if TSet.is_empty res then (not @@ diamond m, trace) + else if diamond m then + (* We could have used TSet.exists, but we only can get the boolean + results, not the trace *) + TSet.fold + (fun ((_, m, p') as _tr) (r, t) -> + if r then r,t (* no need to test the transition if one is + true *) + else step p' (m::t) f) + res + (false, trace) + else + TSet.fold + (fun (_, m, p') (r, t) -> + if not r then r,t (* no need to test the transition if one is + false *) + else step p' (m::t) f) + res + (true, trace) + + | FInvModal(m, f) -> + let r, t = step proc trace @@ FModal (m,f) in + (not r, t) + + | FNu (x, s, f) -> + if PSet.mem proc s then true, trace + else + let s = PSet.add proc s in + let f = reduce f x @@ FNu(x, s, f) in + step proc trace f + + | FMu (x, s, f) -> + (* We use the duality of the least fixed point *) + let f = FNot (reduce f x @@ FNot (FVar x)) in + let f = FNot (FNu (x, s, f)) in + step proc trace f + + (* In case that happen, we substitute the prop by its corresponding + formula, that shouldn't however *) + | FProp (s, il) -> + let f = if Hashtbl.mem props s then + let (vars, formula) = Hashtbl.find props s in + substitute formula @@ List.combine vars il + else + raise (Unbound_prop s) in + step proc trace f + + in + let (res, trace) = step proc [] form in + if res then + Format.printf "The processor given matches the model@." + else + begin + let t = List.rev trace |> + List.fold_left (fun acc t -> + Format.sprintf "%s --> %s" acc @@ string_of_label t) "" + in + let t = Format.sprintf "%s --> " t in + Format.printf "Doesn't match, here is why: @.%s@." t + end + +(** Global model checking *) + +(** This is not working, those functions are only draft to show the work done to + understand and implement the global model checking algorithm *) + +let associate_vars f = + let rec step f acc = + match f with + | FTrue | FFalse -> acc + | FVar x -> x :: acc + | FPar f | FNot f -> step f acc + | FAnd (f1, f2) | FImplies (f1, f2) | FOr (f1, f2) -> + let acc = step f1 acc in + step f2 acc + | FModal (_, f) | FInvModal (_, f) -> step f acc + | FProp (_,_) -> assert false (* assuming there is no prop at this state *) + | FMu (_, _, f) | FNu (_, _, f) -> step f acc + in + step f [] + + + +let (bdds : (string, Bdd.bdd) Hashtbl.t)= Hashtbl.create 19 + + +let rec fix f env name = + let rec step f env = + let old = SMap.find name env in + let env = SMap.add name old env in + let res = compute_obdd f env in + if HashedBdd.equal res old then res + else step f env + in + step f env + + +and compute_obdd f env = + + let implies b1 b2 = (not b1) || b2 in + let xor b1 b2 = ((not b1) && b2) || (b1 && (not b2)) in + let rec step f env = + match f with + | FTrue -> one + | FFalse -> zero + | FVar x -> SMap.find x env + | FPar f -> step f env + | FNot f -> apply xor (step f env) one + | FAnd (f1, f2) -> + let b1 = step f1 env in + let b2 = step f2 env in + apply ( && ) b1 b2 + | FOr (f1, f2) -> + let b1 = step f1 env in + let b2 = step f2 env in + apply ( || ) b1 b2 + | FImplies (f1, f2) -> + let b1 = step f1 env in + let b2 = step f2 env in + apply implies b1 b2 + | FModal (m, f) -> + if not @@ diamond m then step (FInvModal(m, FNot f)) env + else assert false + | FInvModal (_m, _f) -> assert false + | FProp (name,_) -> Hashtbl.find bdds name + | FMu (name, _, f) -> fix f (SMap.add name zero env) name + | FNu (name, _, f) -> fix f (SMap.add name one env) name + + in + step f env + +let bdd_of_formula f name = + (* let vars = associate vars f in *) + if Hashtbl.mem bdds name then Hashtbl.find bdds name + else + let bdd = compute_obdd f @@ SMap.empty in + (Hashtbl.add bdds name bdd; + bdd) + +let count_fixpoint f = + let rec step f acc count = + match f with + | FTrue | FFalse -> acc, count + | FVar _ -> step f acc count + | FPar f | FNot f -> step f acc count + | FAnd (f1, f2) | FImplies (f1, f2) | FOr (f1, f2) -> + let acc, count = step f1 acc count in + step f2 acc count + | FModal (_, f) | FInvModal (_, f) -> step f acc count + | FProp (_,_) -> assert false + | FMu (_, _, f) -> step f ((count, true) :: acc) (count+1) + | FNu (_, _, f) -> step f ((count, false) :: acc) (count+1) + in + step f [] 0 + +type ens = + Top | Bot +| Trans of io * ens +| EForAll of ens list +| Exists of ens list + +let rec string_of_ens = function + | Top -> "Top" + | Bot -> "Bot" + | Trans (io, ens) -> "Trans: " ^ (string_of_io io) ^ "->" ^ + (string_of_ens ens) + | EForAll l -> + (List.fold_left + (fun acc e -> acc ^ "; " ^ (string_of_ens e)) "EForAll:[" l) ^ "]" + | Exists l -> + (List.fold_left + (fun acc e -> acc ^ "; " ^ (string_of_ens e)) "Exists:[" l) ^ "]" + +let trans_equiv a b = + match a, b with + | Any, _ | _, Any -> true + | In, In | Out, Out -> true + | In, Prefix pl | Prefix pl, In -> + List.fold_left + (fun acc fp -> + match fp with + | FTau | FIn _ | FInVar _ -> acc + | _ -> false) + true + pl + | Out, Prefix pl | Prefix pl, Out -> + List.fold_left + (fun acc fp -> + match fp with + | FTau | FOut _ | FOutVar _ -> acc + | _ -> false) + true + pl + | _, _ -> a = b + + +let rec union ens1 ens2 = + Format.printf "Union between: %s && %s@." (string_of_ens ens1) (string_of_ens ens2); + match ens1, ens2 with + | Top, _ | _, Top-> Top + | e, Bot | Bot, e -> e + + | Trans (a1, e1), Trans (a2, e2) -> + if a1 = a2 then Trans (a1, union e1 e2) + else Exists ([ens1; ens2]) + + | (Trans (a, e) as t), Exists l + | Exists l, (Trans (a, e) as t) -> + let added = ref false in + let l = List.fold_left + (fun acc el -> + match el with + | Trans (a2, e2) -> + if a2 = a then (added := true; Trans (a, union e e2) :: acc) + else el :: acc + | _ -> el :: acc) + [] + l + in + let l = if !added then l else t :: l in + Exists l + + | (Trans (a, e) as t), (EForAll l) | (EForAll l), (Trans (a, e) as t) -> + let added = ref false in + let l = List.fold_left + (fun acc el -> + match el with + Trans (a2, e2) -> + if a2 = a then (added := true;Trans (a, union e e2) :: acc) + else el :: acc + | _ -> el :: acc) + [] + l + in + let l = if !added then l else t :: l in + EForAll l + + | EForAll l1, EForAll l2 -> + let l = List.fold_left + (fun acc e -> union e acc) (EForAll l2) l1 in + l + + | Exists l1, Exists l2 -> + let l = List.fold_left + (fun acc e -> union acc e) (Exists l2) l1 in + l + + | (Exists _ as c), (EForAll _ as a) | (EForAll _ as a), (Exists _ as c) -> + Exists [c; a] + + +let rec inter ens1 ens2 = + Format.printf "Inter between: %s && %s@." (string_of_ens ens1) (string_of_ens ens2); + match ens1, ens2 with + | _, _ when ens1 = ens2 -> ens1 + | Top, e | e, Top -> e + | _, Bot | Bot, _ -> Bot + + | Trans (a, e1), Trans (b, e2) -> + if trans_equiv a b then + Trans (a, inter e1 e2) + else Bot + + | (Trans (a, e) as t), Exists l | Exists l, (Trans (a, e) as t) -> + let added = ref false in + let l = List.fold_left + (fun acc el -> + match el with + | Trans (a2, e2) -> + if a2 = a then (added := true; Trans (a, inter e e2) :: acc) + else el :: acc + | _ -> el :: acc) + [] + l + in + let l = if !added then l else t :: l in + Exists l + + | (Trans (a, e) as t), EForAll l | EForAll l, (Trans (a, e) as t) -> + let added = ref false in + let l = List.fold_left + (fun acc el -> + match el with + Trans (a2, e2) -> + if a2 = a then (added := true;Trans (a, inter e e2) :: acc) + else el :: acc + | _ -> el :: acc) + [] + l + in + let l = if !added then l else t :: l in + EForAll l + + | EForAll l1, EForAll l2 -> + let l = List.fold_left + (fun acc e -> inter e acc) (EForAll l2) l1 in + l + + | Exists l1, Exists l2 -> + let l = List.fold_left + (fun acc e -> inter acc e) (Exists l2) l1 in + l + + + | (Exists _ as c), (EForAll _ as a) | (EForAll _ as a), (Exists _ as c) -> + Exists [c; a] + +type fp = Nu | Mu + + +let rec evalrec a f env i = + match f with + | FTrue -> Top + | FFalse -> Bot + | FVar v -> SMap.find v env + | FPar f -> evalrec a f env i + + | FAnd (f1, f2) -> + let e1 = evalrec a f1 env i in + let e2 = evalrec a f2 env i in + inter e1 e2 + + | FOr (f1, f2) -> + let e1 = evalrec a f1 env i in + let e2 = evalrec a f2 env i in + union e1 e2 + + | FModal (m, f) | FInvModal (m, f) -> + let _, m, io = m in + let f = evalrec a f env i in + (match m with + | Possibly -> Exists([Trans(io, f)]) + | _ -> EForAll([Trans(io, f)])) + + | FMu (v, _, f) -> fixpoint a Mu v f i env + | FNu (v, _, f) -> fixpoint a Nu v f i env + | FProp (_, _) -> assert false + | FNot _ -> assert false + | FImplies (_, _) -> assert false + +and fixpoint a fp var f i env = + let ens = match fp with Mu -> Top | Nu -> Bot in + for j=0 to i-1 do + let (ty, _) = a.(j) in + if ty = fp then a.(j) <- ty, ens + done; + let r_old = ref a.(i) in + let first = ref true in + while !r_old <> a.(i) || !first do + first := false; + let ty, ens = a.(i) in + r_old := ty, ens; + let env = SMap.add var ens env in + a.(i) <- ty, evalrec a f env (i+1); + done; + let _, ens = a.(i) in + ens + +let check_ens ens proc = + + (* let get_matching_deriv s p a = *) + (* let deriv = compute_derivation s p in *) + (* TSet.fold *) + (* (fun ((_, m, p') as _tr) acc -> *) + (* step p' (m::t) f) *) + (* deriv *) + (* [] *) + (* in *) + + let _proc = Normalize.normalize proc in + let res = match ens with + | Bot -> false + | Top -> true + | Trans(_a, _e) -> assert false + (* let m = Strong, Possibly, a in (\* The first two are just to match the *) + (* modality scheme *\) *) + (* let d = compute_derivation Strong proc in *) + (* let res = compute_modality m d in *) + (* if TSet.is_empty res then false *) + (* else if diamond m then *) + (* TSet.fold *) + (* (fun ((_, m, p') as _tr) (r, t) -> *) + (* (\* Format.printf "t: %s@." @@ string_of_transition tr; *\) *) + (* if r then r,t (\* no need to test the transition if one is *) + (* true *\) *) + (* else step p' (m::t) f) *) + (* res *) + (* false *) + | Exists _l -> assert false + | EForAll _l -> assert false + in + res + +let check_global f _ = + let acc, n = count_fixpoint f in + let a = Array.make n (Mu, Top) in + let rec make acc = + match acc with + | [] -> () + | (i, b)::l -> + a.(i) <- if b then Mu, Top else Nu, Bot; + make l + in + make acc; + let ens = evalrec a f SMap.empty 0 in + Format.printf "Ens: %s@." @@ string_of_ens ens diff --git a/src/Global.ml b/src/Global.ml new file mode 100644 index 0000000..4cb4a59 --- /dev/null +++ b/src/Global.ml @@ -0,0 +1,5 @@ +(** Contains global definitiions that can be used by multiple modules. Avoid + circular dependencies *) + + +let global_definition_map : (string, Syntax.definition) Hashtbl.t = Hashtbl.create 64