diff --git a/CMU-CS-96-180.ps b/CMU-CS-96-180.ps new file mode 100644 index 0000000..4a830ee Binary files /dev/null and b/CMU-CS-96-180.ps differ diff --git a/make-archive.sh b/make-archive.sh index fb0b257..3f71db5 100644 --- a/make-archive.sh +++ b/make-archive.sh @@ -2,7 +2,7 @@ TOPFILES="LICENSE.txt AUTHORS VERSION Makefile" -SRCFILES="src/Makefile src/Utils.ml src/Lexer.mll src/Parser.mly src/Syntax.ml src/Normalize.ml src/Minim.ml src/Semop.ml src/Control.ml src/Presyntax.ml src/Pave.ml src/NormTests.ml src/STests.ml src/examples/*.ccs" +SRCFILES="src/Makefile src/Utils.ml src/Lexer.mll src/Parser.mly src/Syntax.ml src/Normalize.ml src/Minim.ml src/Semop.ml src/Control.ml src/Presyntax.ml src/Formula.ml src/Pave.ml src/NormTests.ml src/STests.ml src/examples/*.ccs" DATE=$(date "+%d-%m-%Y") echo "v.${DATE}" > ./VERSION diff --git a/rapport/.gitignore b/rapport/.gitignore new file mode 100644 index 0000000..53373f9 --- /dev/null +++ b/rapport/.gitignore @@ -0,0 +1,4 @@ +*.log +*~ +*.aux +*.pdf \ No newline at end of file diff --git a/rapport/rapport.tex b/rapport/rapport.tex new file mode 100644 index 0000000..05bc1dd --- /dev/null +++ b/rapport/rapport.tex @@ -0,0 +1,294 @@ + + +\pdfminorversion 7 +\pdfobjcompresslevel 3 + +\documentclass[a4paper]{article} +\special{papersize=210mm,297mm} +\usepackage[utf8]{inputenc} +\usepackage[T1]{fontenc} +\usepackage{cite} +\usepackage[francais]{babel} +\usepackage[bookmarks=false,colorlinks,linkcolor=blue]{hyperref} +\usepackage[top=3cm,bottom=2cm,left=3cm,right=2cm]{geometry} +\usepackage{graphicx} +\usepackage{subfig} +\usepackage{eso-pic} +\usepackage{array} +\usepackage{color} +\usepackage{url} +\usepackage{listings} +\usepackage{eurosym} +\usepackage{url} +\usepackage{textcomp} +\usepackage{fancyhdr} +\usepackage{tikz} +\usetikzlibrary{automata,positioning} + +\definecolor{lightgray}{gray}{0.9} + +\title{Projet de SACC} +\author{Rémy \textsc{El-Sibaie Besognet} -- Roven \textsc{Gabriel}} + +\newcommand{\HRule}{\rule{\linewidth}{0.5mm}} + + +\begin{document} + +\maketitle + +\section{Introduction} + +Le logiciel Pave est un interprète pour un langage de modélisation de +système concurrent : CCS\footnote{Calculus of communicating +systems}. Il a été développé par les différentes générations +d'étudiants de l'UE SACC. La dernière pierre ajoutée à cet édifice est +la prise en main du $\mu$-Calcul dans l'interprète. Après l'ajout de +sucre syntaxique, l'objectif est d'implémenter un algorithme de +vérification d'un processus décrit en CCS à partir d'une formule +$\mu$-Calcul. + +On appelle cette vérification du \emph{Model Checking}. On vérifie +que la description d'un programme est fidèle à sa spécification de +façon automatique. On présentera ici deux algorithme pour le +Model Checking +à hauteur de notre compréhension : local et global. Seul +l'algorithme local a été écrit dans la version proposée par notre binôme. + +%% \section{$\mu$-Calcul par valeur} + +\section{Modifications préliminaires} + +Avant de pouvoir implémenter la vérification de formules, nous avons effectués +quelques modifications dans l'optique d'améliorer l'utilisation de \texttt{pave}. +Nous avons amélioré l'affichage d'erreur qui non seulement n'arrête pas le +programme mais aussi est plus clair. + +\begin{verbatim} +> prop A = ; + ^ +Parser error at line 1 char 14: ~;~ +> +\end{verbatim} + +Nous avons modifié le parseur afin de pouvoir définir et vérifier des formules du +$\mu$-calcul et défini l'AST représentant les formules. Nous avons deux +particularités notables : les modalités sont représentées sous forme de triplet +\emph{(force, type, restriction)} et les opérations \texttt{Mu} et \texttt{Nu} +embarquent directement l'environement qui sera utilisé dans le \texttt{check local}. + +\section{Model checking local} + +L'algorithme de model checking local a été inspiré par Glynn Winskel +dans \emph{Topics in concurrency}. Le principe est en fait assez +simple. On parcourt récursivement le processus et la formule en +vérifiant que chaque état du processus vérifie la formule. On traite +les cas triviaux en traduisant simplement l'opérateur $\mu$-Calcul en +opérateur booléen inductivement. + +\begin{lstlisting}[language=caml] +let rec check def_map prop_map formula nproc = + let rec check_internal = function + | FTrue -> true + | FFalse -> false + | FNot formula -> not @@ check_internal formula + | FAnd (f1, f2) -> check_internal f1 && check_internal f2 + | FOr (f1, f2) -> check_internal f1 || check_internal f2 + | FImplies (f1, f2) -> check_internal f1 |> not || check_internal f2 + | ... +\end{lstlisting} + +On considère un processus $p$. Dans le cas des modalités, on récupère +toutes les dérivations possibles de $p$ dont la transition est +étiquetée par la bonne action (sans oublier \texttt{<>} +et \texttt{[]}) et on construit un ensemble de processus qui +correspond aux suivants de $p$. On appelle récursivement notre +fonction \texttt{check} sur les éléments de cet ensemble avec la +formule sans la modalité. + +La partie concernant les points fixes n'était pas triviale. L'idée est +de définir une fonction de \emph{subtitution} et de remplacer +récursivement le résultat courant dans l'appel suivant. + +\begin{lstlisting}[language=caml] +let beta_reduce in_formula expected_var replacement = + let rec beta_reduce in_formula = + match in_formula with + | FTrue | FFalse -> in_formula + | FAnd (f1, f2) -> FAnd(beta_reduce f1, beta_reduce f2) + | FOr (f1, f2) -> FOr(beta_reduce f1, beta_reduce f2) + | FImplies (f1, f2) -> FImplies(beta_reduce f1, beta_reduce f2) + | FModal (modality, formula) -> FModal(modality, beta_reduce formula) + | FInvModal (modality, formula) -> FInvModal(modality, beta_reduce formula) + | FProp _ -> in_formula + | FVar var when var = expected_var -> replacement + | FVar _ -> in_formula + | FMu (x, env, formula) -> FMu(x, env, beta_reduce formula) + | FNu (x, env, formula) -> FNu(x, env, beta_reduce formula) + | FNot formula -> FNot (beta_reduce formula) + in + beta_reduce in_formula +\end{lstlisting} + +\subsection{Trace} + +Afin de mieux comprendre les raison d'une propriété fausse, nous avons +ajouté la fonctionnalitée de trace. Ainsi, à chaque étape dans +l'algorithme, la formule courante et processus courant sont stockés et +restitués à la fin de l'opération. Ainsi nous obtenons le chemin qui +arrive à la propriété fausse. + +\begin{verbatim} +checklocal ~(true) |- a!, a?; +Trace : + a!,a?,0 -| ~True + a?,0 -| True +FALSE PROPERTY +\end{verbatim} + +Dans cet exemple nous pouvons voir que c'est à +l'étape \verb|a?,0| associé à la +formule \verb|True| que la propriété devient fausse. + +\begin{verbatim} +def P = a!,P + b!,P; +def D = P || c!; + +checklocal true |- D; +Trace : + D() -| True + (c!,0||P()) -| True + (c!,0||P()) -| True + (c!,0||P()) -| True + (c!,0||P()) -| True + P() -| True + P() -| True + P() -| True +FALSE PROPERTY +\end{verbatim} + +Un autre exemple de trace qui nous permet de voir que \verb|c!| ne +peut apparaitre qu'une seule fois, la consomation de cette action est +clairement visible sur les processus utilisés à gauche. + +\section{Model Checking global} + +L'algorithme global pour le Model Checking a, lui, été inspiré par +Sergey Berezin dans \emph{Model Checking algorithms for +$\mu$-Calculus} L'implémentation de cet algorithme dans le projet a +été arrêtée par manque de compréhension de l'article présenté et de +l'idée même de la méthode dite globale. Nous n'avons pas compris les +paramètres et ce qu'était sensé rendre l'algorithme. + +Notre première démarche a été de vouloir le résoudre avec la méthode +proposée des BDD, d'où la présence du module correspondant. La +traduction d'une formule vers un BDD demandait préalablement d'avoir +compris l'algorithme simple. Nous avons donc tenté cette approche sans +plus de succès. + + +\section{Exemples} + +\subsection{Définition de propriétés usuelles} +\begin{verbatim} +prop Exercice5 = Mu(X).true or (<.>true and [.]X): +prop Possibly(A) = Mu(X).A or <.>X; +prop Deadlock = [.]false; +prop Always(A) = Nu(X).A and [.]X; +prop Continue = <.>true; +prop Eventualy(A) = Mu(X).A or ([.]X and <.> true); +\end{verbatim} + +\subsection{Vérifications} +\begin{verbatim} +def D2 = a!,(b? + D2); +\end{verbatim} + +\begin{verbatim} +> checklocal Always(Continue) |- D2; +Trace : + D2() -| Always(Continue) + D2() -| Nu(X){()}.(Continue and [.]X) + D2() -| (Continue and [.]Nu(X){(D2())}.(Continue and [.]X)) + D2() -| Continue + D2() -| <.>True + (b?,0+D2()) -| True + D2() -| [.]Nu(X){(D2())}.(Continue and [.]X) + (b?,0+D2()) -| Nu(X){(D2())}.(Continue and [.]X) + (b?,0+D2()) -| (Continue and [.]Nu(X){((b?,0+D2()),D2())}.(Continue and [.]X)) + (b?,0+D2()) -| Continue + (b?,0+D2()) -| <.>True + 0 -| True + (b?,0+D2()) -| True + (b?,0+D2()) -| [.]Nu(X){((b?,0+D2()),D2())}.(Continue and [.]X) + 0 -| Nu(X){((b?,0+D2()),D2())}.(Continue and [.]X) + 0 -| (Continue and [.]Nu(X){(0,(b?,0+D2()),D2())}.(Continue and [.]X)) + 0 -| Continue + 0 -| <.>True + (b?,0+D2()) -| Nu(X){((b?,0+D2()),D2())}.(Continue and [.]X) +FALSE PROPERTY +\end{verbatim} + +Le processus ne s'execute pas à l'infini tout le temps. + +\begin{verbatim} +> checklocal Possibly(Continue) |- D2; +TRUE PROPERTY + +> checklocal Possibly(Deadlock) |- D2; +TRUE PROPERTY +\end{verbatim} + +Il est cependant possible qu'il s'execute à l'infini ou qu'il s'arrête. + +\begin{verbatim} +> checklocal Always(Deadlock) |- D2; +Trace : + D2() -| Always(Deadlock) + D2() -| Nu(X){()}.(Deadlock and [.]X) + D2() -| (Deadlock and [.]Nu(X){(D2())}.(Deadlock and [.]X)) + D2() -| Deadlock + D2() -| [.]False + (b?,0+D2()) -| False +FALSE PROPERTY + +\end{verbatim} + +Il ne s'arrête donc pas tout le temps. + +\begin{verbatim} +def E = d!,c!,e!; +def F = (c!,b!,a!,b! || c!,a!,b!); +def G = (c!,b!,a!,b! || c!,a!,b! || E); + +prop SuiteAAC = Possibly(true); + +> checklocal SuiteAAC |- F; +Trace : + F() -| SuiteAAC + F() -| Possibly(True) + F() -| Mu(X){()}.(True or <.>X) + F() -| not Nu(X){()}.not (True or <.>not X) + +[...] + 0 -| <.>not Nu(X){(0,b!,0,(b!,0||b!,0),(a!,b!,0||b!,0), + (b!,0||c!,a!,b!,0),(a!,b!,0||c!,a!,b!,0),(b!,a!,b!,0||c!,a!,b!,0),F()a}. + not (True or <.>not X) +FALSE PROPERTY + +> checklocal SuiteAAC |- G; +TRUE PROPERTY +\end{verbatim} + +Dans cet exemple nous pouvons observer que la +séquence \texttt{a!,a!,c!} n'est possible dans le processus F que si +un troisième processus parallel E contenant +\texttt{c!} est défini. + +\end{document} + +# Local Variables: +# compile-command: "rubber -d rapport.tex" +# End: + +%% LocalWords: Glynn Winskel Topics concurrency diff --git a/src/.gitignore b/src/.gitignore index 66679b0..875cd71 100644 --- a/src/.gitignore +++ b/src/.gitignore @@ -2,4 +2,7 @@ _build pave stests lts.dot -lts_mini.dot \ No newline at end of file +lts_mini.dot +*~ +*.swp +.vimrc diff --git a/src/Control.ml b/src/Control.ml index 9616126..37b7332 100644 --- a/src/Control.ml +++ b/src/Control.ml @@ -2,6 +2,7 @@ open Printf open Utils open Syntax +open Formula open Normalize open Semop open Minim @@ -28,6 +29,13 @@ Command summary:\n\ wlts -> show labelled transition system\n\ wmini -> minimize process\n\ wfbisim ? ~~ -> check weak bisimilarity (fast)\n\ + prop = | \n\ + prop ( , ) = \n\ + -> register a new propertie with/without params\n\ + checklocal |- \n\ + -> local model checking on the given proc\n\ + checkglobal |- \n\ + -> local model checking on the given proc\n\ ---\n\ help -> this help message\n\ quit -> quit the program\n\ @@ -39,11 +47,18 @@ let script_mode = ref false ;; exception Constdef_Exception of string ;; exception Typedef_Exception of string ;; -let handle_help () = +type error = Unbound_Proposition of string +exception Error of error + +let print_error = function + | Unbound_Proposition s -> printf "unbound proposition %s" s + + +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 +66,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 +80,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 +91,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 +111,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 +137,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,22 +148,24 @@ 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 +let global_proposition_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) ; 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 +183,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 +192,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 +211,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,44 +238,46 @@ 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 "> %s %s ~ %s\n%!" str (string_of_process p1) + (string_of_process p2) ; printf "Calculate %s...\n%!" str2; let start_time = Sys.time() in let np1 = normalize p1 in let np2 = normalize p2 in try - let bsm = f_bisim global_definition_map np1 np2 - in - let end_time = Sys.time() - in + let bsm = f_bisim global_definition_map np1 np2 in + let end_time = Sys.time() in let print (np1, np2) = printf "{ %s ; %s }\n" (string_of_nprocess np1) (string_of_nprocess np2) in - printf "the processes are %s\n(elapsed time=%fs)\n%!" str3 (end_time-.start_time) ; + printf "the processes are %s\n(elapsed time=%fs)\n%!" str3 + (end_time-.start_time) ; BSet.iter print bsm with Failure "Not bisimilar" -> - let end_time = Sys.time() - in - printf "the processes are *not* %s\n(elapsed time=%fs)\n%!" str3 (end_time-.start_time) + let end_time = Sys.time() in + printf "the processes are *not* %s\n(elapsed time=%fs)\n%!" + str3 (end_time-.start_time) let common_is_bisim f_bisim str str2 p1 p2 = if !script_mode then - printf "> %s ? %s ~ %s\n%!" str (string_of_process p1) (string_of_process p2) ; + printf "> %s ? %s ~ %s\n%!" str + (string_of_process p1) (string_of_process p2) ; let ok,time = timing (fun () -> let np1 = normalize p1 in 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) ; + if !script_mode then + printf "> %s ? %s ~ %s\n%!" str1 + (string_of_process p1) (string_of_process p2) ; let ok,time = timing (fun () -> let np1 = normalize p1 in let np2 = normalize p2 in @@ -277,30 +296,73 @@ let handle_wlts p = common_lts (lts (weak_transitions false)) "wlts" p let handle_minimization p = common_minimization derivatives "mini" p -let handle_wminimization p = common_minimization (weak_transitions false) "wmini" p +let handle_wminimization p = common_minimization + (weak_transitions false) "wmini" p + + +let handle_bisim p1 p2 = common_bisim construct_bisimilarity + "bisim" "bisimilarity" "bisimilar" p1 p2 +let handle_wbisim p1 p2 = common_bisim construct_weak_bisimilarity + "wbisim" "weak bisimilarity" "weakly bisimilar" p1 p2 -let handle_bisim p1 p2 = common_bisim construct_bisimilarity "bisim" "bisimilarity" "bisimilar" p1 p2 -let handle_wbisim p1 p2 = common_bisim construct_weak_bisimilarity "wbisim" "weak bisimilarity" "weakly bisimilar" p1 p2 +let handle_is_bisim p1 p2 = common_is_bisim is_bisimilar + "bisim" "bisimilar" p1 p2 +let handle_is_fbisim p1 p2 = common_is_fbisim derivatives + "fbisim" "bisimilar" p1 p2 -let handle_is_bisim p1 p2 = common_is_bisim is_bisimilar "bisim" "bisimilar" p1 p2 +let handle_is_wbisim p1 p2 = common_is_bisim is_weakly_bisimilar + "wbisim" "weakly bisimilar" p1 p2 -let handle_is_fbisim p1 p2 = common_is_fbisim derivatives "fbisim" "bisimilar" p1 p2 +let handle_is_fwbisim p1 p2 = common_is_fbisim (weak_transitions false) + "wfbisim" "weakly bisimilar" p1 p2 -let handle_is_wbisim p1 p2 = common_is_bisim is_weakly_bisimilar "wbisim" "weakly bisimilar" p1 p2 +let handle_deriv p = common_deriv derivatives (TSet.iter (fun t -> + printf "%s\n" (string_of_derivative t))) "deriv" "derivatives" p -let handle_is_fwbisim p1 p2 = common_is_fbisim (weak_transitions false) "wfbisim" "weakly bisimilar" p1 p2 +let handle_wderiv p = common_deriv (weak_derivatives false) + printPfixMap "wderiv" "weak derivatives" p -let handle_deriv p = common_deriv derivatives (TSet.iter (fun t -> printf "%s\n" (string_of_derivative t))) "deriv" "derivatives" p +let handle_tderiv p = common_deriv (weak_derivatives true) + printPfixMap "tderiv" "tau derivatives" p -let handle_wderiv p = common_deriv (weak_derivatives false) printPfixMap "wderiv" "weak derivatives" p -let handle_tderiv p = common_deriv (weak_derivatives true) printPfixMap "tderiv" "tau derivatives" p +(** Mu Calculus *) +let fetch_prop key = + Hashtbl.find global_proposition_map key +let register_proposition prop = + Hashtbl.replace global_proposition_map (string_of_prop_header prop) prop +let handle_prop name params formula = + if !script_mode then + printf "> %s\n%!" (string_of_formula formula) ; + register_proposition @@ Proposition(name, params, formula); + printf "Proposition '%s' registered\n%!" name + + +let handle_check_local formula process = + let nproc = Normalize.normalize process in + let res, trace = + Local.check global_definition_map global_proposition_map + [formula, nproc] formula nproc + in + if res then printf "TRUE PROPERTY\n\n" + else begin + printf "Trace : \n"; + List.iter + (fun (formula, process) -> + printf "\t%s -| %s\n" + (Normalize.string_of_nprocess process) + (Formula.string_of_formula formula)) + (List.rev trace); + printf "FALSE PROPERTY\n\n" + end + +let handle_check_global formula process = Global.check formula process diff --git a/src/Formula.ml b/src/Formula.ml new file mode 100644 index 0000000..f58ceb5 --- /dev/null +++ b/src/Formula.ml @@ -0,0 +1,91 @@ +(*** Representation of mu-calculus formulae ***) + +open Printf + +open Normalize +open Presyntax +open Utils + + +(* mu-calculus formulae *) + +type restr = Rin | Rout | Rany | Rpref of preprefix list +type existence = Possibly | Necessity +type strength = Weak | Strong +type modality = strength * existence * restr + +let string_of_restr = function + | Rout -> "!" + | Rin -> "?" + | Rany -> "." + | Rpref acts -> string_of_collection_no_block "," string_of_preprefix acts + +let string_of_existence = function Possibly -> sprintf "<%s>" + | Necessity -> sprintf "[%s]" + +let string_of_strongness f r = function Weak -> f (f r) + | Strong -> f r + +let string_of_modality (s, e, r) = + string_of_strongness (string_of_existence e) (string_of_restr r) s + + +type formula = + | FTrue + | FFalse + | FNot of formula + | FAnd of formula * formula + | FOr of formula * formula + | FImplies of formula * formula + | FModal of modality * formula + | FInvModal of modality * formula + | FProp of string * formula list + | FVar of string + | FMu of string * nprocess list * formula + | FNu of string * nprocess list * formula + +let rec string_of_formula : formula -> string = function + | FTrue -> "True" + | FFalse -> "False" + | 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) + | 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 "(" ")" "," string_of_formula params) + | FVar var -> var + | FNot f -> sprintf "not %s" (string_of_formula f) + | FMu(x, env, f) -> + sprintf "Mu(%s){%s}.%s" x (string_of_args string_of_nprocess env) + (string_of_formula f) + | FNu(x, env, f) -> + sprintf "Nu(%s){%s}.%s" x (string_of_args string_of_nprocess env) + (string_of_formula f) + +type proposition = Proposition of string * string list * formula + +let string_of_prop_header (Proposition(name, _, _)) = + name + +let string_of_proposition (Proposition(_, _, formula) as prop) = + "prop " ^ (string_of_prop_header prop) ^ " = " ^ (string_of_formula formula) + +let rec formula_of_preformula formula = + (* printf "Transforming %s\n" @@ string_of_formula formula; *) + match formula with + | FTrue -> formula + | FFalse -> formula + | FNot _ -> formula + | FAnd (f1, f2) -> FAnd (formula_of_preformula f1, formula_of_preformula f2) + | FOr (f1, f2) -> FOr (formula_of_preformula f1, formula_of_preformula f2) + | FImplies (f1, f2) -> FImplies (formula_of_preformula f1, formula_of_preformula f2) + | FModal (m, f) -> FModal (m, formula_of_preformula f) + | FInvModal (m, f) -> FInvModal (m, formula_of_preformula f) + | FProp (prop, params) -> + (* printf "%s : Not implemented\n" @@ string_of_formula formula; *) + FProp(prop, List.map formula_of_preformula params) + | FVar _ -> + (* printf "%s : Not implemented\n" @@ string_of_formula formula; *) + formula + | FMu (x, env, f) -> FMu (x, env, formula_of_preformula f) + | FNu (x, env, f) -> FNu (x, env, formula_of_preformula f) diff --git a/src/Global.ml b/src/Global.ml new file mode 100644 index 0000000..eed1801 --- /dev/null +++ b/src/Global.ml @@ -0,0 +1,65 @@ +(** Global Model Checking Module *) + + +type error = +| No_global_not + +exception Error of error + +let print_error = function + | No_global_not -> Printf.printf "Cannot global check formula with negation" + + + + +(* + L p = sous ensemble de Top tq p est vraie + T action = relation binaire sur t en fonction de a +*) + +let rec simple_eval process defs formula env = + let lts = Semop.lts defs Semop.derivatives process in + let rec eval formula env = + let open Formula in + match formula with + | FNot _ -> raise @@ Error (No_global_not) + | FTrue -> lts + | FFalse -> [] + | FAnd (f1, f2) -> eval f1 env @ eval f2 env + | FOr (f1, f2) -> eval f1 env @ eval f2 env + | _ -> assert false + in eval formula env + +let rec obdd_of_modality env modality = + match modality with + (* | Strong, Possibly, Rany _ *) + (* | Strong, Possibly, Rout *) + (* | Strong, Possibly, Rin -> *) + (* | (Weak, _, _), T_Tau -> *) + (* | (_, _, Rpref acts), label -> *) + | _ -> assert false + + + +let rec obdd_of_formula env formula = + let open Formula in + let open Obdd in + match formula with + | FTrue -> One + | FFalse -> Zero + | FNot _ -> raise @@ Error (No_global_not) + | FAnd (f1, f2) -> inter (obdd_of_formula env f1) + (obdd_of_formula env f2) + | FOr (f1, f2) -> union (obdd_of_formula env f1) + (obdd_of_formula env f2) + (* | FImplies of formula * formula *) + | FModal (modality, f) -> + inter (obdd_of_formula env f) (obdd_of_modality env f) + (* | FInvModal of modality * formula *) + (* | FProp of string * formula list *) + (* | FVar v -> assert false *) + (* | FMu of string * nprocess list * formula *) + (* | FNu of string * nprocess list * formula *) + | _ -> assert false + +let check _formula _proc = assert false (* TODO *) diff --git a/src/Lexer.mll b/src/Lexer.mll index b39dfbc..3eeb43b 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" @@ -63,6 +63,10 @@ let tild = "~" let semicol = ";" let ws = (['\t' ' ']*) let colon = ':' + +let implies_1 = "==>" +let implies_2 = "=>" + let cmd_help = "help" let cmd_quit = "quit" let cmd_norm = "norm" @@ -83,10 +87,25 @@ let cmd_wlts = "wlts" let cmd_wmini = "wmini" let cmd_wfbisim = "wfbisim" +let cmd_prop = "prop" +let cmd_check = "check" +let cmd_check_local = "checklocal" +let cmd_check_global = "checkglobal" + +let sat_1 = "|-" +let sat_2 = "satisfies" + +let mu_1 = "Mu" +let mu_2 = "mu" +let mu_3 = "MU" +let nu_1 = "Nu" +let nu_2 = "nu" +let nu_3 = "NU" + rule token = parse | ws {token lexbuf} - | eol + | eol { incr line; token lexbuf } | cmt @@ -115,8 +134,8 @@ let cmd_wfbisim = "wfbisim" | 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 } @@ -150,21 +169,40 @@ let cmd_wfbisim = "wfbisim" | cmd_free { FREE } | cmd_bound { BOUND } | cmd_names { NAMES } - + + | implies_1 { IMPLIES } + | implies_2 { IMPLIES } + | cmd_wderiv { WDERIV } | cmd_tderiv { TDERIV } | cmd_wbisim { WBISIM } | cmd_wlts { WLTS } | cmd_wmini { WMINI } | cmd_wfbisim { WFBISIM } - + + | mu_1 { MU } + | mu_2 { MU } + | mu_3 { MU } + + | nu_1 { NU } + | nu_2 { NU } + | nu_3 { NU } + + | cmd_prop { PROP } + | cmd_check { CHECK_LOCAL } + | cmd_check_local { CHECK_LOCAL } + | cmd_check_global { CHECK_GLOBAL } + + | 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/Local.ml b/src/Local.ml new file mode 100644 index 0000000..968386f --- /dev/null +++ b/src/Local.ml @@ -0,0 +1,155 @@ +(** Local Model Checking Module *) + +open Formula +open Semop + +type error = +| Unbound_Proposition of string +| Unmatching_length of string + +exception Error of error + +(* Trace, tuple of labels visited and + process remaining to execute *) +type trace = (formula * Normalize.nprocess) list + +let print_error = function + | Unbound_Proposition s -> Printf.printf "unbound proposition %s\n" s + | Unmatching_length s -> + Printf.printf "unmatching length on proposition %s\n" s + +let transitions_of def_map nproc = Semop.derivatives def_map nproc +let weak_transitions_of def_map nproc = + Semop.weak_derivatives true def_map nproc + + +let check_label_prefixes lbl pref = + let open Presyntax in + match pref, lbl with + | PTau, T_Tau -> true + | (PIn (PName s1), (T_In s2)) when s1 = s2 -> true + | (POut (PName s1), (T_Out s2)) when s1 = s2 -> true + | _ -> false + + + +let rec next_process_set def_map modality inv transitions = + let choose transition destination_set = + let _, mod_to_check, destination = transition in + match modality, mod_to_check with + | ((Strong | Weak), _, Rany), _ + | ((Strong | Weak), _, Rout), (T_Out _) + | ((Strong | Weak), _, Rin), (T_In _) -> + PSet.add destination destination_set + | (Weak, _, _), T_Tau -> + PSet.union destination_set @@ + (PrefixMap.fold (fun k d a -> PSet.union d a) + (weak_transitions_of def_map destination) + destination_set) + | (_, _, Rpref acts), label when not inv -> + if List.exists (check_label_prefixes label) acts then + PSet.add destination destination_set + else destination_set + | (_, _, Rpref acts), label when inv -> + if not @@ List.exists (check_label_prefixes label) acts then + PSet.add destination destination_set + else destination_set + | _ -> destination_set + in TSet.fold choose transitions PSet.empty + + +let beta_reduce in_formula expected_var replacement = + let rec beta_reduce in_formula = + match in_formula with + | FTrue | FFalse -> in_formula + | FAnd (f1, f2) -> FAnd(beta_reduce f1, beta_reduce f2) + | FOr (f1, f2) -> FOr(beta_reduce f1, beta_reduce f2) + | FImplies (f1, f2) -> FImplies(beta_reduce f1, beta_reduce f2) + | FModal (modality, formula) -> FModal(modality, beta_reduce formula) + | FInvModal (modality, formula) -> FInvModal(modality, beta_reduce formula) + | FProp _ -> in_formula + | FVar var when var = expected_var -> replacement + | FVar _ -> in_formula + | FMu (x, env, formula) -> FMu(x, env, beta_reduce formula) + | FNu (x, env, formula) -> FNu(x, env, beta_reduce formula) + | FNot formula -> FNot (beta_reduce formula) + in + beta_reduce in_formula + +let rec check def_map prop_map trace formula nproc = + let rec check_internal trace = function + | FTrue -> (true, trace) + | FNot formula -> + let okay1, trace1 = check_internal ((formula, nproc)::trace) formula in + (not okay1, trace1) + | FFalse -> (false, trace) + | FAnd (f1, f2) -> + let okay1, trace1 = check_internal ((f1, nproc)::trace) f1 in + if not okay1 then okay1, trace1 else + let okay2, trace2 = check_internal ((f2, nproc)::trace1) f2 in + (okay1 && okay2, trace2) + | FOr (f1, f2) -> + let okay1, trace1 = check_internal ((f1, nproc)::trace) f1 in + if okay1 then okay1, trace else + let okay2, trace2 = check_internal ((f2, nproc)::trace1) f2 in + (okay1 || okay2, trace2) + | FImplies (f1, f2) -> + let okay1, trace1 = check_internal ((f1, nproc)::trace) f1 in + if not okay1 then not okay1, trace1 else + let okay2, trace2 = check_internal ((f2, nproc)::trace1) f2 in + (not okay1 || okay2, trace2) + | FModal (modality, formula) -> + check_modality def_map prop_map trace modality false formula nproc + | FInvModal (modality, formula) -> + check_modality def_map prop_map trace modality true formula nproc + | FProp (prop_name, params) -> + check_prop_call def_map prop_map prop_name trace formula params nproc + | FVar var -> + check_prop_call def_map prop_map var trace formula [] nproc + | FMu (x, env, mu_formula) -> + let formula' = + FNot (FNu (x, env, FNot (beta_reduce mu_formula x (FNot (FVar x))))) + in check_internal ((formula', nproc)::trace) formula' + | FNu (_, env, _) when List.mem nproc env -> (true, trace) + | FNu (x, env, formula) -> + let reduced_formula = + beta_reduce formula x @@ FNu(x, nproc::env, formula) + in + check_internal ((reduced_formula, nproc)::trace) reduced_formula + in + check_internal trace formula + + +and check_modality def_map prop_map trace modality inv formula process = + let ts = transitions_of def_map process in + let operator, acc_init = match modality with + | _, Necessity, _ -> (&&), true + | _, Possibly, _ -> (||), false + in + let folding element (acc_okay, acc_trace) = + let okay1, trace1 = + check def_map prop_map ((formula, element)::acc_trace) formula element + in + (operator okay1 acc_okay, trace1) + in + PSet.fold folding (next_process_set def_map modality inv ts) (acc_init, trace) + + +and check_prop_call def_map prop_map prop_name trace formula params process = + let (Proposition (_, param_names, formula)) = + try + Hashtbl.find prop_map prop_name + with Not_found -> raise @@ Error(Unbound_Proposition prop_name) + in + let params_length1 = List.length params in + let params_length2 = List.length param_names in + if params_length1 <> params_length2 then + raise @@ Error (Unmatching_length prop_name) + else + let params_map = List.combine param_names params in + let reduce_param formula (param_name, param_content) = + beta_reduce formula param_name param_content + in + let reduced_formula = List.fold_left reduce_param formula params_map in + check def_map prop_map ((reduced_formula, process)::trace) + reduced_formula process diff --git a/src/Makefile b/src/Makefile index cecc3cb..02ed38d 100644 --- a/src/Makefile +++ b/src/Makefile @@ -1,7 +1,7 @@ SRCS = $(wildcard *.ml *.mli *.mll *.mly) TARGS = stests pave KIND = native # d.byte -FLAGS = -w,Ae,-warn-error,A +FLAGS = -w,Ae#,-warn-error,A all: $(TARGS) diff --git a/src/Minim.ml b/src/Minim.ml index 8b59e81..98f3fa3 100755 --- a/src/Minim.ml +++ b/src/Minim.ml @@ -26,6 +26,7 @@ module GSet = Set.Make ( type transitions = nprocess list * label * nprocess list + (* transition set *) module TsSet = Set.Make ( struct type t = transitions @@ -50,26 +51,26 @@ let string_of_graph g = acc ^ (sprintf "%s has prevs %s\n" (string_of_gstate dst) (string_of_gset string_of_gstate prevs)) in - GMap.fold folder g "" + 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" + (fun s part -> s ^ "\n" ^ (string_of_gset string_of_gstate part)) "" parts) + ^ "\n" let build_graph f_deriv init_graph init_partition defs ps = let rec add_to_partition part elem = match part with - | [] -> [GSet.singleton elem] - | set::ss -> - begin - match (GSet.choose set, elem) with - | (PState _, PState _) -> - (GSet.add elem set)::ss - | (LState(_,a,_), LState(_,b,_)) when a = b -> - (GSet.add elem set)::ss - | _ -> set::(add_to_partition ss elem) - end + | [] -> [GSet.singleton elem] + | set::ss -> + begin + match (GSet.choose set, elem) with + | (PState _, PState _) -> + (GSet.add elem set)::ss + | (LState(_,a,_), LState(_,b,_)) when a = b -> + (GSet.add elem set)::ss + | _ -> set::(add_to_partition ss elem) + end in let rec f (graph, part) procs_todo procs_done = try @@ -97,93 +98,92 @@ let build_graph f_deriv init_graph init_partition defs ps = PSet.remove p (PSet.union (PSet.diff next_procs procs_done) procs_todo) in let new_procs_done = PSet.add p procs_done in - f (new_graph, new_part) new_procs_todo new_procs_done + f (new_graph, new_part) new_procs_todo new_procs_done with Not_found -> (graph, part) in match ps with - | [] -> (init_graph, init_partition) - | p1::[] -> f (init_graph, init_partition) (PSet.singleton p1) PSet.empty - | p1::p2::[] -> - let tmp = f (init_graph, init_partition) (PSet.singleton p1) PSet.empty - in f tmp (PSet.singleton p2) PSet.empty - | _ -> (init_graph, init_partition) + | [] -> (init_graph, init_partition) + | p1::[] -> f (init_graph, init_partition) (PSet.singleton p1) PSet.empty + | p1::p2::[] -> + let tmp = f (init_graph, init_partition) (PSet.singleton p1) PSet.empty + in f tmp (PSet.singleton p2) PSet.empty + | _ -> (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) in let rec f1 pt pr = match pt with - | [] -> [] - | h1::t1 -> (f2 h1 pr)@(f1 t1 pr) - and f2 pt pr = + | [] -> [] + | h1::t1 -> (f2 h1 pr)@(f1 t1 pr) + and f2 pt pr = match pr with - | [] -> [pt] - | h2::t2 -> let (spl1, spl2) = split pt h2 in - if GSet.is_empty spl1 || GSet.is_empty spl2 then - f2 pt t2 - else - [spl1 ; spl2] + | [] -> [pt] + | h2::t2 -> let (spl1, spl2) = split pt h2 in + if GSet.is_empty spl1 || GSet.is_empty spl2 then + f2 pt t2 + else + [spl1 ; spl2] in let part' = f1 part prevs in if (List.length part = List.length 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) + | LState _ -> false + | PState _ -> true) partition in let pstates = List.map (fun set -> - GSet.fold - (fun x acc -> match x with - | PState (_, np) -> np::acc - | LState _ -> acc) set [] + GSet.fold + (fun x acc -> match x with + | PState (_, np) -> np::acc + | LState _ -> acc) set [] ) ps and lstates = List.map (fun set -> - GSet.fold - (fun x acc -> match x with - | PState _ -> acc - | LState t -> t::acc) set [] + GSet.fold + (fun x acc -> match x with + | PState _ -> acc + | LState t -> t::acc) set [] ) ls in let rec f transs todos = match todos with - | [] -> transs - | cp::t -> - begin - let p = List.hd cp in - let labs = - List.fold_left - (fun acc x -> - match List.filter (fun (src,_,_) -> src = p) x with - | [] -> acc - | t::_ -> t::acc - ) - [] lstates - in let transs' = - List.fold_left - (fun acc (_,lbl,dst) -> - let cdl = List.filter - (fun x -> List.mem dst x) pstates in - assert ((List.length cdl) = 1); - let cd = List.hd cdl in - TsSet.add (cp, lbl, cd) acc - ) transs labs - in f transs' t - end - in - f TsSet.empty pstates + | [] -> transs + | cp::t -> + begin + let p = List.hd cp in + let labs = + List.fold_left + (fun acc x -> + match List.filter (fun (src,_,_) -> src = p) x with + | [] -> acc + | t::_ -> t::acc + ) + [] lstates + in let transs' = + List.fold_left + (fun acc (_,lbl,dst) -> + let cdl = List.filter + (fun x -> List.mem dst x) pstates in + assert ((List.length cdl) = 1); + let cd = List.hd cdl in + TsSet.add (cp, lbl, cd) acc + ) transs labs + in f transs' t + end + in f TsSet.empty pstates let minimize f_deriv defs proc = @@ -191,14 +191,14 @@ let minimize f_deriv defs proc = let init_partition = [GSet.singleton (PState(false,proc))] in let (graph, partition) = build_graph f_deriv init_graph init_partition defs [proc] in (*print_endline "STATE GRAPH :"; - print_string (string_of_graph graph); - print_string "PARTITION :"; - print_string (string_of_partition partition);*) - let partition' = refine (graph, partition) in - (*print_string "PARTITION REFINED :"; - print_string (string_of_partition partition');*) - let transitions = build_lts partition' in - TsSet.fold (fun t acc -> t :: acc) transitions [] + print_string (string_of_graph graph); + print_string "PARTITION :"; + print_string (string_of_partition partition);*) + let partition' = refine (graph, partition) in + (*print_string "PARTITION REFINED :"; + print_string (string_of_partition partition');*) + let transitions = build_lts partition' in + TsSet.fold (fun t acc -> t :: acc) transitions [] let is_fbisimilar f_deriv defs p1 p2 = let root = PState(true,(SSet.empty,NSilent)) in diff --git a/src/Normalize.ml b/src/Normalize.ml index c351aa9..c0bf02c 100644 --- a/src/Normalize.ml +++ b/src/Normalize.ml @@ -38,7 +38,7 @@ let string_of_nprocess (res, nproc) = else "new" ^ (string_of_args (fun x -> x) (SSet.elements res)) ^ "[" ^ (string_of_nproc nproc) ^ "]" - + let is_normalized (_, nproc,_) = let rec norm = function | NPrefix (_,q) -> norm q @@ -102,16 +102,16 @@ let denormalize (res, nproc) = | NRename(var,name,p) -> Rename (var,name,denorm_sub p) in SSet.fold (fun n p -> Res (n, p)) res (denorm_sub nproc) - + (***) -let rec mem_target a list = +let rec mem_target a list = match list with | [] -> false | (target,_)::tl -> if (target = a) then true else mem_target a tl -let mem_value a list = +let mem_value a list = match list with - | [] -> false + | [] -> false | (_,value)::tl -> if (value = a) then true else mem_target a tl @@ -130,13 +130,13 @@ let simple_normalize proc = let rec snorm_one map = function | Silent -> Silent | Prefix (Tau, proc) -> Prefix (Tau, snorm_one map proc) - | Prefix (In name, proc) -> + | Prefix (In name, proc) -> Prefix (In (SMap.find name map), snorm_one map proc) | Prefix (Out name, proc) -> Prefix (Out (SMap.find name map), snorm_one map proc) | Sum (proc1, proc2) -> Sum(snorm_one map proc1, snorm_one map proc2) | Par (proc1, proc2) -> Par(snorm_one map proc1, snorm_one map proc2) - | Res (name, proc) -> + | Res (name, proc) -> let fname = gen() in let map' = SMap.add name fname map @@ -153,16 +153,16 @@ let simple_normalize proc = Rename(old,value', snorm_one map proc) in let tmpproc = - snorm_one init_map proc + snorm_one init_map proc in let findname name map = - if SSet.mem name !nus - then + if SSet.mem name !nus + then name else SMap.find name map in - let rec norm_sub map = function + let rec norm_sub map = function | Silent -> NSilent | Prefix (Tau, proc) -> NPrefix (Tau, norm_sub map proc) | Prefix (In name, proc) -> NPrefix (In (findname name map), norm_sub map proc) @@ -184,7 +184,7 @@ let simple_normalize proc = | Res (_, proc) -> norm_sub map proc | Call (name, args) -> NCall (name, args) | Rename (old,value,proc) -> - let value' = + let value' = if SMap.mem value map then findname value map else value @@ -259,8 +259,8 @@ let complex_normalize ((bounded : SSet.t), nproc) frees = NPrefix (Out (SMap.find name name_map), rename np) | NSum nps -> NSum (List.map rename nps) | NPar nps -> NPar (List.map rename nps) - | NRename(var,name,np) -> - let name' = + | NRename(var,name,np) -> + let name' = if SMap.mem name name_map then SMap.find name name_map else name @@ -303,7 +303,7 @@ let nproc_subst nproc m n = let nsubst (res, nproc) m n = (SSet.add n (SSet.remove m res), nproc_subst nproc m n) - + let rec nsubsts p ms ns = match (ms,ns) with | ([],[]) -> p | ([],_) -> failwith "nsubsts: bad cosupport" diff --git a/src/Obdd.ml b/src/Obdd.ml new file mode 100644 index 0000000..79486f6 --- /dev/null +++ b/src/Obdd.ml @@ -0,0 +1,111 @@ + +type unique = int + +type t = Zero | One | Node of unique * int * t * t +type obdd = t + +module S = Set.Make( + struct + type t = int + let compare = compare + end +) +type elt = S.t + +let zero = Zero +let empty = zero +let is_empty obdd = obdd == Zero +let one = One + +let unique = function + | Zero -> 0 + | One -> 1 + | Node (u , _, _, _) -> u + +let hash_node i o1 o2 = (19 * (19 * i + unique o1) + unique o2) land max_int + +let unique_ref = ref 2 + +module HashedObdd = struct + type t = obdd + let hash = function + | Zero -> 0 + | One -> 1 + | Node (_, i, o1, o2) -> hash_node i o1 o2 + let equal k1 k2 = match k1, k2 with + | One, One + | Zero, Zero -> true + | Node (_, i1, l1, r1), Node (_, i2, l2, r2) -> + i1 = i2 && unique l1 = unique l2 && unique r1 = unique r2 + | _ -> false +end + +module Obddtbl = Hashtbl.Make (HashedObdd) + +let hsize = 19997 (* 200323 *) + + +module H2 = Hashtbl.Make + (struct + type t = obdd * obdd + let hash (o1, o2) = (19 * unique o1 + unique o2) land max_int + let equal (o11, o12) (o21, o22) = o11 == o21 && o12 == o22 + end) + + +let construct = + let global_table = Obddtbl.create hsize in + fun i o1 o2 -> + if o2 = Zero then o1 else + let obdd = Node (!unique_ref, i, o1, o2) in + try + Obddtbl.find global_table obdd + with Not_found -> + Obddtbl.add global_table obdd obdd; + incr unique_ref; + obdd + +let memo_rec2 f = + let h = H2.create hsize in + let rec g x = + try H2.find h x + with Not_found -> let y = f g x in H2.add h x y; y + in + g + +let union = memo_rec2 ( + fun union -> function + | Node(_, i, o1, o2), One + | One, Node(_, i, o1, o2) -> construct i (union (o1, One)) o2 + | One, One -> One + | Zero, o | o, Zero -> o + | (Node (_, i1, l1, r1) as o1), (Node (_, i2, l2, r2) as o2) -> + if i1 = i2 then + construct i1 (union (l1, l2)) (union (r1, r2)) + else if i1 > i2 then + construct i2 (union (o1, l2)) r2 + else + construct i1 (union (l1, o2)) r1 +) + +let union o1 o2 = union (o1, o2) + +let inter = memo_rec2 ( + fun inter -> function + | Node(_, _, o1, _), One + | One, Node(_, _, o1, _) -> inter (o1, One) + | One, One -> One + | Zero, _ + | _, Zero -> Zero + | (Node (_, i1, l1, r1) as o1), + (Node (_, i2, l2, r2) as o2) -> + if i1 = i2 then + construct i1 (inter (l1, l2)) (inter (r1, r2)) + else if i1 > i2 then + inter (o1, l2) + else + inter (o2, l1) + ) + +let inter o1 o2 = inter (o1, o2) + diff --git a/src/Parser.mly b/src/Parser.mly index 946df37..09b920e 100644 --- a/src/Parser.mly +++ b/src/Parser.mly @@ -3,18 +3,19 @@ open Utils open Presyntax + open Formula let rec mkRes ns p = match ns with | [] -> 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) (* @@ -33,7 +34,7 @@ %} /* reserved keywords */ -%token DEF TRUE FALSE END NEW TAU DIV WHEN CONSTDEF TYPEDEF +%token DEF TRUE FALSE END NEW TAU DIV WHEN CONSTDEF TYPEDEF MU NU /* identifiers */ %token IDENT @@ -59,6 +60,11 @@ %token WMINI %token WFBISIM +%token PROP +%token CHECK_LOCAL +%token CHECK_GLOBAL +%token SATISFY + %token HELP %token QUIT @@ -70,11 +76,12 @@ %token IF THEN ELSE INF SUP INFEQ SUPEQ DIFF DOTDOT LACCOL RACCOL /* operators */ -%token PAR PLUS DOT OUT IN MINUS DIV MULT MOD AND OR NOT +%token PAR PLUS DOT OUT IN MINUS DIV MULT MOD AND OR NOT IMPLIES %nonassoc RENAME %left PAR %left AND , OR +%right IMPLIES %nonassoc INF , INFEQ, SUP, SUPEQ, DIFF, EQUAL %left PLUS , MINUS %left MULT , DIV , MOD @@ -93,78 +100,80 @@ %type process %type prefix %type expr +%type modality +%type formula /* grammar */ %% script: | EOF { false } | statement SEMICOL { true } - | statement error { raise (Fatal_Parse_Error "missing ';' after statement") } + | statement error { raise @@ Fatal_Parse_Error "missing ';' after statement"} minmax: | CONST { $1 } | 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") } @@ -173,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") } @@ -183,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") } @@ -201,66 +210,80 @@ | 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 list_of_names RPAREN EQUAL formula + /* prop_name params fmla */ + { Control.handle_prop $2 $4 (formula_of_preformula $7) } + | PROP IDENT EQUAL formula + /* prop_name fmla */ + { Control.handle_prop $2 [] (formula_of_preformula $4) } + + | CHECK_LOCAL formula SATISFY process + { Control.handle_check_local (formula_of_preformula $2) (process_of_preprocess $4) } + + | CHECK_GLOBAL formula SATISFY process + { Control.handle_check_global (formula_of_preformula $2) (process_of_preprocess $4) } + | HELP { Control.handle_help () } | QUIT { 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") } @@ -281,8 +304,12 @@ | expr OUT LPAREN expr RPAREN { PSend($1,$4) } | expr IN LPAREN VAR COLON IDENT RPAREN { PReceive($1,$4,$6) } + list_of_prefixes: + | prefix { [$1] } + | prefix COMMA list_of_prefixes { $1::$3 } + rename : - | LBRACKET list_of_renames RBRACKET { $2 } + | LBRACKET list_of_renames RBRACKET { $2 } list_of_renames : | IDENT DIV IDENT { [($3,$1)] } @@ -334,5 +361,47 @@ | /* empty */ { [] } | expr list_of_exprs { $1::$2 } + + list_of_formulas: + | /* empty */ { [] } + | formula list_of_formulas { $1::$2 } + + formula: + | TRUE { FTrue } + | FALSE { FFalse } + | LPAREN formula RPAREN { $2 } + | formula AND formula { FAnd ($1,$3) } + | formula OR formula { FOr ($1,$3) } + | formula IMPLIES formula { FImplies ($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 list_of_formulas RPAREN { FProp($1,$3) } + | IDENT { FVar($1) } + + modality: + | INF list_of_prefixes SUP { Strong, Possibly, Rpref $2 } + | INF OUT SUP { Strong, Possibly, Rout } + | INF IN SUP { Strong, Possibly, Rin } + | INF DOT SUP { Strong, Possibly, Rany } + + | INF INF list_of_prefixes SUP SUP { Weak, Possibly, Rpref $3 } + | INF INF OUT SUP SUP { Weak, Possibly, Rout } + | INF INF IN SUP SUP { Weak, Possibly, Rin } + | INF INF DOT SUP SUP { Weak, Possibly, Rany } + + | LBRACKET list_of_prefixes RBRACKET { Strong, Necessity, Rpref $2 } + | LBRACKET OUT RBRACKET { Strong, Necessity, Rout } + | LBRACKET IN RBRACKET { Strong, Necessity, Rin} + | LBRACKET DOT RBRACKET { Strong, Necessity, Rany } + + | LBRACKET LBRACKET list_of_prefixes RBRACKET RBRACKET { + Weak, Necessity, Rpref $3 } + | LBRACKET LBRACKET OUT RBRACKET RBRACKET { Weak, Necessity, Rout } + | LBRACKET LBRACKET IN RBRACKET RBRACKET { Weak, Necessity, Rin } + | LBRACKET LBRACKET DOT RBRACKET RBRACKET { Weak, Necessity, Rany } + + %% (* end of grammar *) diff --git a/src/Pave.ml b/src/Pave.ml index 8d0583e..37949cd 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"^ @@ -36,12 +36,13 @@ Arg.parse [ printf "%s\n%!" banner;; -let parse_error_msg lexbuf = +let parse_error_msg ?interactive_mode:(inter=false) lexbuf = let p = lexbuf.Lexing.lex_curr_p in let l = p.Lexing.pos_lnum in let c = p.Lexing.pos_cnum - p.Lexing.pos_bol in let tok = Lexing.lexeme lexbuf in + if inter then printf "%s^\n" @@ String.make (c + 1) ' '; printf "Parser error at line %d char %d: ~%s~\n%!" l c tok ;; match !load_file with @@ -53,29 +54,37 @@ match !load_file with let lexbuf = Lexing.from_channel stdin in try ignore (Parser.script Lexer.token lexbuf) - with + 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 + | Parsing.Parse_error -> + parse_error_msg ~interactive_mode:true lexbuf + | Control.Error e -> Control.print_error e + | Local.Error e -> Local.print_error e + | Global.Error e -> Global.print_error e + done | Some 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 = + let continue = try Parser.script Lexer.token lexbuf - with + 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 -> + | Parsing.Parse_error -> parse_error_msg lexbuf ; true + | Control.Error e -> Control.print_error e; true + | Local.Error e -> Local.print_error e; true + | Global.Error e -> Global.print_error e; true + in if continue then loop (); in diff --git a/src/Presyntax.ml b/src/Presyntax.ml index f2c6fc3..8e75c47 100644 --- a/src/Presyntax.ml +++ b/src/Presyntax.ml @@ -5,6 +5,9 @@ open Utils open Syntax +exception Typedef_Exception of string +exception Vardef_Exception of string ;; + let env_const = ref SMap.empty ;; let env_var = ref SMap.empty ;; @@ -14,7 +17,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 +25,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 +37,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 +63,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,23 +77,25 @@ 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 | PInt i -> Int i | PName str -> Name str | PConst name -> Int (SMap.find name !env_const) - | PVar name -> (SMap.find name !env_var) + | PVar name -> begin + try (SMap.find name !env_var) with Not_found -> raise @@ Vardef_Exception name + end | 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 || b2 ) + Bool ( b1 || b2 ) | PAdd (preexpr1, preexpr2) -> let i1 = int_of_value (interprete_preexpr preexpr1 ) @@ -135,7 +140,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 +154,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 +186,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) @@ -221,7 +226,6 @@ let rec string_of_preprocess = function | PGuard(g,p) -> sprintf "when (%s) %s" (string_of_preexpr g) (string_of_preprocess p) -exception Vardef_Exception of string ;; let make_int_list min max = let rec make_aux m = @@ -236,17 +240,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,54 +261,55 @@ 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) -> Res(nvar, (process_of_preprocess pproc) ) - | PCall( nom, pexprList) -> Call (nom, (List.map interprete_preexpr pexprList)) + | PCall( nom, pexprList) -> Call (nom, + (List.map interprete_preexpr pexprList)) | 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 +324,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 +337,21 @@ 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 -> + | (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 -> (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 -> + raise @@ Vardef_Exception nomVar); + let val_list = + try value_list (SMap.find theType !env_type) with Not_found -> raise @@ Typedef_Exception theType + in + 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 @@ -349,7 +359,8 @@ let definitions_of_predefinition : predefinition -> definition list = (env_var := SMap.remove nomVar !env_var; List.flatten def_list) in - printf "Transforming definition:\n%s\n%!" (string_of_predefinition predef) ; + printf "Transforming definition:\n%s\n%!" + (string_of_predefinition predef) ; def_of_predef_aux name [] preparams preproc - + diff --git a/src/README b/src/README new file mode 100644 index 0000000..bfae45d --- /dev/null +++ b/src/README @@ -0,0 +1,91 @@ + + +Les modules à modifier : + +Formula.formula_of_preformula : +Conversion d'une formule de mu-calcul par valeur (ou pré-formule) en formule de mu-calcul pur (fonction formula_of_preformula.ml dans Formula.ml) + + +Control.handle_prop : définition d'une variable prop (une relation n-aire) +- On ajoute simplement une formule à l'environnement + + +Control.handle_local_check : +- effectue un check local pour vérifier la satisfiabilité de la formule +- Topics in concurrency : page 47, Chapter 4 Logics for processes +algo : page 61 to 68 + + +Control.handle_global_check : +- effectue un check global +- dans l'article Model Checking Algorithms for the µ-calculus (CMU) + + + + + + +TODO : + + + + +CCS et µcalcul "pur" et "par valeur" : + +Vu en cours : + +µ-calcul "pur" : + + A |- P : Ok s'il existe P' tel que P-a!->P' et A |- P' + +<> A |- P + Ok si il existe un P' tq + - P -tau-> *P1 -a!-> P2 -tau -> *P' + - et A |- P' + + +µ-calcul par valeur : + +const %N=3 +type Range = [0..%N] + +def Incr = in ?($n:Range), + [when $n < %N out!($n+1), Incr + when $n = %N stop !,0] + + + +Ceci est transformé en CCS pur de la façon suivante : + + +def Incr = + +in_0 ?, [out_1 !,Incr + 0] + ++ in_1 ?, [out_2 !,Incr + 0] + ++ in_2 ?, [out_3 !,Incr + 0] + ++ in_3, [0 + stop !,0] + + +Une formule "par valeur" comme par exemple : + + +forall $n:Range, $n < %N ==> true + +devient une formule "pure" : + + +(true => True) + +and (true => True) + +and (true => True) + + + + +On ajoute : +Forall +Exists +conditions du type : \ No newline at end of file diff --git a/src/Semop.ml b/src/Semop.ml index 046c268..e0f1117 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 = @@ -62,8 +62,7 @@ let derivatives defs ((orig_res, orig_np) as orig_nproc) = match lab with | T_Tau -> true | T_In n | T_Out n -> not (SSet.mem n res) - in - TSet.filter filter derivs + in TSet.filter filter derivs in let renames var name derivs= let folder (src, lab, (dres,dest)) acc = @@ -71,10 +70,8 @@ let derivatives defs ((orig_res, orig_np) as orig_nproc) = | T_Tau -> T_Tau | T_In n -> T_In (if n = var then name else n) | T_Out n -> T_Out (if n = var then name else n) - in - TSet.add (src, lab', (dres,NRename(var,name,dest))) acc - in - TSet.fold folder derivs TSet.empty + in TSet.add (src, lab', (dres,NRename(var,name,dest))) acc + in TSet.fold folder derivs TSet.empty in let rec f res np = match np with @@ -87,13 +84,13 @@ let derivatives defs ((orig_res, orig_np) as orig_nproc) = in let (body_res, body_np) = normalize body in let derivs = f body_res body_np in - restrict body_res derivs + 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 + renames var name derivs | NSum nps -> List.fold_left (fun acc np -> TSet.union (f res np) acc) TSet.empty nps @@ -113,48 +110,42 @@ let derivatives defs ((orig_res, orig_np) as orig_nproc) = (*compteur, accu processus, accu restrictions*) let rec gen_name n = let new_n = "f" ^ (string_of_int n) in - if SSet.mem new_n in_frees || SSet.mem new_n in_res - then gen_name (succ n) - else (succ n, new_n) + if SSet.mem new_n in_frees || SSet.mem new_n in_res + then gen_name (succ n) + else (succ n, new_n) in let (new_cnt, new_name) = gen_name cnt in (new_cnt, nproc_subst acc_in name new_name, SSet.add new_name (SSet.remove name acc_in_res)) (* nproc_subst renames the first encountered label != Tau - or the name in a Rename node + or the name in a Rename node We delete the passage and we rename name by new_name in the set - *) - in + *) 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) - 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 = - let new_n = "f" ^ (string_of_int n) in - if SSet.mem new_n np_frees || SSet.mem new_n res - then gen_name (succ n) - else (succ n, new_n) - in - let (new_cnt, new_name) = gen_name cnt in - (new_cnt, - List.map (fun np -> nproc_subst np name new_name) - acc_oths, - SSet.add new_name (SSet.remove name acc_oths_res)) - in - let (_, new_oths, new_oths_res) = - SSet.fold folder_oths np_forbid (0, oths_np, res) - in - renormalize (SSet.union new_in_res new_oths_res, - NPar (new_in :: new_oths)) - in - TSet.add (src, lab, new_dst) acc - in - (TSet.fold folder nexts acc_par, (nexts, oths_np) :: acc_simpl) - in - List.fold_left folder (TSet.empty, []) nps + (*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 = + let new_n = "f" ^ (string_of_int n) in + if SSet.mem new_n np_frees || SSet.mem new_n res + then gen_name (succ n) + else (succ n, new_n) + in + let (new_cnt, new_name) = gen_name cnt in + (new_cnt, + List.map (fun np -> nproc_subst np name new_name) + acc_oths, + SSet.add new_name (SSet.remove name acc_oths_res)) + in + let (_, new_oths, new_oths_res) = + SSet.fold folder_oths np_forbid (0, oths_np, res) + in renormalize (SSet.union new_in_res new_oths_res, + NPar (new_in :: new_oths)) + in TSet.add (src, lab, new_dst) acc + in (TSet.fold folder nexts acc_par, (nexts, oths_np) :: acc_simpl) + in List.fold_left folder (TSet.empty, []) nps in let folder ((map, _) as acc) (elt_set, oths) = let folder' (_, lab, dst) ((map', set') as acc') = @@ -163,40 +154,34 @@ let derivatives defs ((orig_res, orig_np) as orig_nproc) = try SMap.add org ((dst,oths) :: SMap.find org map') map' with Not_found -> SMap.add org [(dst,oths)] map' in - try - let dsts' = SMap.find opp map in - let folder acc (np, oths') = - let oths_np = - List.filter (fun e -> List.memq e oths) oths' - in - let nproc' = - let p1 = denormalize np in - let p2 = denormalize dst in - let oths_p = - List.map (fun np -> denormalize (res, np)) oths_np - in - let p = - List.fold_left (fun acc p -> Par (p, acc)) Silent - (p1 :: p2 :: oths_p) - in - normalize p - in - TSet.add (orig_nproc, T_Tau, nproc') acc + try + let dsts' = SMap.find opp map in + let folder acc (np, oths') = + let oths_np = + List.filter (fun e -> List.memq e oths) oths' in - (new_map', List.fold_left folder set' dsts') - with Not_found -> (new_map', set') - in - match lab with - | T_Tau -> acc' - | T_In n -> add_taus (n ^ "?") (n ^ "!") - | T_Out n -> add_taus (n ^ "!") (n ^ "?") - in - TSet.fold folder' elt_set acc - in - snd (List.fold_left folder (SMap.empty, set_par) set_simpl) + let nproc' = + let p1 = denormalize np in + let p2 = denormalize dst in + let oths_p = + List.map (fun np -> denormalize (res, np)) oths_np + in + let p = + List.fold_left (fun acc p -> Par (p, acc)) Silent + (p1 :: p2 :: oths_p) + in normalize p + in TSet.add (orig_nproc, T_Tau, nproc') acc + in (new_map', List.fold_left folder set' dsts') + with Not_found -> (new_map', set') + in match lab with + | T_Tau -> acc' + | T_In n -> add_taus (n ^ "?") (n ^ "!") + | T_Out n -> add_taus (n ^ "!") (n ^ "?") + in TSet.fold folder' elt_set acc + in snd (List.fold_left folder (SMap.empty, set_par) set_simpl) in let derivs = f orig_res orig_np in - restrict orig_res derivs + restrict orig_res derivs ;; let lts deriv_f defs p = @@ -239,13 +224,13 @@ let construct_bisimilarity defs nproc1 nproc2 = try construct (BSet.add dsts acc_bsm) dst1 dst2 with Failure "Bad path" -> search (TSet.remove ty acc_dys) in - search dys + search dys in - TSet.fold (folder d2s false) d1s - (TSet.fold (folder d1s true) d2s bsm) + TSet.fold (folder d2s false) d1s + (TSet.fold (folder d1s true) d2s bsm) in - try construct (BSet.singleton (nproc1, nproc2)) nproc1 nproc2 - with Failure "Bad path" -> failwith "Not bisimilar" + try construct (BSet.singleton (nproc1, nproc2)) nproc1 nproc2 + with Failure "Bad path" -> failwith "Not bisimilar" ;; let is_bisimilar defs nproc1 nproc2 = @@ -264,8 +249,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 +277,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 +299,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 +317,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 +334,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 +348,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 @@ -373,12 +358,12 @@ let weak_derivatives tau_only defs (orig_restrict, p) : PSet.t PrefixMap.t = let (body_res, body_np) = normalize body in let derivs = weak_deriv_aux pfix_key entry_map ((SSet.union restrict body_res), body_np) in PrefixMap.filter (fun k _ -> not (is_restricted body_res k)) derivs - (* on ne filtre que sur body_res -> restrict sera au pire filtré à la sortie - * de weak_derivatives, et plus d'états dans la map peut empêcher des récursions *) + (* on ne filtre que sur body_res -> restrict sera au pire filtré à la sortie + * de weak_derivatives, et plus d'états dans la map peut empêcher des récursions *) | 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 +375,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 +393,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 +414,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 +435,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 +452,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 diff --git a/src/Syntax.ml b/src/Syntax.ml index 0bc9ad1..bdf8eac 100644 --- a/src/Syntax.ml +++ b/src/Syntax.ml @@ -61,7 +61,7 @@ let def_values = function let def_body = function | Definition (_,_,body) -> body -let string_of_def_header (Definition (name,values,_)) = +let string_of_def_header (Definition (name,values,_)) = name ^ (string_of_args string_of_value values) let string_of_definition = function @@ -103,7 +103,7 @@ let namesOfValues vs = (* freeNames: process -> SSet.t *) let rec freeNames = function - | Call (_, vs) -> + | Call (_, vs) -> List.fold_left (fun fn v -> match v with | Name n -> SSet.add n fn | _ -> fn) SSet.empty vs @@ -114,9 +114,9 @@ let rec freeNames = function | Sum (proc1, proc2) | Par (proc1, proc2) -> SSet.union (freeNames proc1) (freeNames proc2) | Res (name, proc) -> SSet.remove name (freeNames proc) - | Rename (old , value , proc) -> + | Rename (old , value , proc) -> let fn = freeNames proc - in (* XXX: this is not clear + in (* XXX: this is not clear if SSet.mem old fn then SSet.add value (SSet.remove old fn) else fn *) @@ -153,20 +153,20 @@ let substPrefix p m n = match p with | Tau -> Tau | In(a) -> if a = n then (In m) else (In a) | Out(a) -> if a = n then (Out m) else (Out a) - -let substName a b c = if a = c then b else a + +let substName a b c = if a = c then b else a let substValue v m n = match v with | Name a -> Name (substName a m n) | _ -> v - -let rec subst p m (* overrides *) n = + +let rec subst p m (* overrides *) n = match p with | Silent -> Silent | Prefix(a,q) -> Prefix((substPrefix a m n),(subst q m n)) | Sum(q,r) -> Sum((subst q m n),(subst r m n)) | Par(q,r) -> Par((subst q m n),(subst r m n)) - | Res(a,q) -> + | Res(a,q) -> if a = n then Res(a,q) else if a = m @@ -174,7 +174,7 @@ let rec subst p m (* overrides *) n = in Res(fname, (subst (subst q fname a) m n)) else Res(a,(subst q m n)) | Call(d,vs) -> Call(d,(List.map (fun v -> substValue v m n) vs)) - | Rename (old,value,q) -> Rename(substName old m n,substName value m n,subst q m n) + | Rename (old,value,q) -> Rename(substName old m n,substName value m n,subst q m n) let rec substs p ms ns = match (ms,ns) with | ([],[]) -> p diff --git a/src/Utils.ml b/src/Utils.ml index fd5cd6b..b3f08ca 100644 --- a/src/Utils.ml +++ b/src/Utils.ml @@ -3,6 +3,7 @@ open Printf (* globa parser exception *) exception Fatal_Parse_Error of string ;; +exception Non_Implemented_Exception (* string sets and maps *) @@ -22,6 +23,14 @@ let string_of_collection (op:string) (cl:string) (sep:string) in op ^ (str lst) ^ cl +let string_of_collection_no_block (sep:string) + (tostr: 'a -> string) (lst: 'a list) = + let rec str = function + | [] -> "" + | e::[] -> tostr e + | e::es -> (tostr e) ^ sep ^ (str es) + in str lst + let string_of_list tostr lst = string_of_collection "[" "]" ";" tostr lst let string_of_args tostr lst = string_of_collection "(" ")" "," tostr lst @@ -29,7 +38,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 +60,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 = diff --git a/src/examples/formula.ccs b/src/examples/formula.ccs new file mode 100644 index 0000000..3dd445b --- /dev/null +++ b/src/examples/formula.ccs @@ -0,0 +1,46 @@ +def D = a!, b?,(a! + b?); + +prop StartA = true; +prop NotStartA = false; +prop AllSecondB = [.]true; +prop ExistsSecondB = <.>true; +prop ExistsThirdA = <.>true; +prop EndsWithA = Mu(X).[.]false or [.]X; + +checklocal StartA |- D; +checklocal NotStartA |- D; +checklocal AllSecondB |- D; +checklocal ExistsSecondB |- D; +checklocal AllThirdA |- D; +checklocal ExistsThirdA |- D; +checklocal EndsWithA |- D; + +def P = a!,Q; +def Q = a!,P; + +prop AllA = Nu(X).X; + +checklocal AllA |- P; + +prop AllB = Nu(X).X; + +checklocal AllB |- P; + +prop Exercice5 = Mu(X).true or (<.>true and [.]X): +prop Possibly(A) = Mu(X).A or <.>X; +prop Deadlock = [.]false; +prop Always(A) = Nu(X).A and [.]X; +prop Continue = <.>true; +prop Eventualy(A) = Mu(X).A or ([.]X and <.> true); + +checklocal Always(Continue) |- P; +checklocal Possibly(Deadlock) |- P; +checklocal Possibly(Continue) |- D; +checklocal Always(Deadlock) |- D; + +def D2 = a!,(b? + D2); + +checklocal Always(Continue) |- D2; +checklocal Possibly(Continue) |- D2; +checklocal Possibly(Deadlock) |- D2; +checklocal Always(Deadlock) |- D2; diff --git a/src/examples/testtrace.ccs b/src/examples/testtrace.ccs new file mode 100644 index 0000000..8123c60 --- /dev/null +++ b/src/examples/testtrace.ccs @@ -0,0 +1,9 @@ +def P = a!,Q; +def Q = b!,P; +prop B = Nu(X).X; +checklocal B |- P; + +prop B1 = Nu(X).X; +checklocal B1 |- P; + +checklocal B or B1 |- P;