(********************************************************************* ********************************************************************** File name: pi-calculator.ml Fresh O'Caml program to calculate the possible labelled transitions from a process expression in the Milner-Parrow-Walker Pi-Calculus. Usage: see the section on HOW TO USE THIS FILE, below. Author: A.M.Pitts Date: 2003-08-08 Reference: [SW] Davide Sangiorgi and David Walker, "The pi-calculus: a theory of mobile processes" (CUP, 2001). ********************************************************************* *********************************************************************) (********************************************************************** Some GENERAL FUNCTIONS **********************************************************************) let mapPartial (f : 'a -> 'b option) : 'a list -> 'b list = let rec map (xs : 'a list) : 'b list = match xs with [] -> [] | x :: xs' -> (match f x with None -> map xs' | Some y -> y :: map xs') in map;; (* (mapMatrixPartial f xs ys) returns a list containing all those z for which Some z = f x y, for some x in xs and y in ys *) let mapMatrixPartial (f : 'a -> 'b -> 'c option) (xs: 'a list) (ys : 'b list) : 'c list = let rec m (x : 'a) (ys : 'b list) (zs : 'c list) : 'c list = match ys with [] -> zs | y :: ys' -> (match f x y with None -> m x ys' zs | Some z -> m x ys' (z :: zs)) in let rec ms (xs : 'a list) (ys : 'b list) (zs : 'c list) : 'c list = match xs with [] -> zs | x :: xs' -> ms xs' ys (m x ys zs) in ms xs ys [];; (* append lists without duplicating *) let rec ( ++ ) (xs : 'a list) (ys : 'a list) : 'a list = match ys with [] -> xs | y :: ys' -> if List.exists ((=) y) xs then xs ++ ys' else (y :: xs) ++ ys';; (********************************************************************* SYNTAX We use the following grammar for pi-calculus processes: processes p ::= m guarded sum p | p composition nu x(p) restriction !p replication guarded sums m ::= 0 inaction a prefixed process m + m summation prefixed processes a ::= out c c. p output prefix in c(x). p input prefix tau. p unobservable prefix [c = c]a match prefix where c,x range over names of channels. This grammar is equivalent to [SW, Definition 1.1.1], but corresponds more closely to the datatype proc for processes declared below, which uses use abstraction types, <>(-), when representing operations that bind channel names. Corresponding to the syntactic categories p, m, a given above are datatypes proc, gsum and prefix, declared below. This file does not give a parser for turning strings into values of these datatypes. It does contain print functions for displaying such values as strings obeying the above grammar. *********************************************************************) type t;; (* some type *) type chan = t name;; (* channel names, c,x *) type proc = (* pi-caluclus processes *) Gd of gsum (* m *) | Par of proc * proc (* p1 | p2 *) | Res of <>proc (* nu x(p) *) | Rep of proc (* !p *) and gsum = (* guarded sums, m *) Inact (* 0 *) | Pre of prefix (* a *) | Plus of gsum * gsum (* m1 + m2 *) and prefix = (* prefixes, a *) Out of chan * chan * proc (* out c1 c2. p *) | In of chan * (<>proc) (* in c(x). p *) | Tau of proc (* tau. p *) | Match of chan * chan * prefix;; (* [c1 = c2]a *) (********************************************************************* RENAMING FUNCTION (c |-> c')p gives the result of capture-avoiding substitution in p:proc of the channel name c':chan for all occurrences of c:chan that are not within the scope of a binder <>(-). Note: the definition of rename is remarkably simple! (because of the way FreshML handles binding operations) *********************************************************************) let ( |-> ) (c : chan) (c' :chan) : proc -> proc = let rec rename (p : proc) : proc = match p with Gd m -> Gd(renameg m) | Par(p1, p2) -> Par(rename p1, rename p2) | Res(<>p1) -> Res(<>(rename p1)) | Rep p1 -> Rep(rename p1) and renameg (m : gsum) : gsum = match m with Inact -> Inact | Pre a -> Pre(renamep a) | Plus(m1, m2) -> Plus(renameg m1, renameg m2) and renamep (a : prefix) : prefix = match a with Out(c1, c2, p) -> Out(renamec c1, renamec c2, rename p) | In(c1, <>p) -> In(renamec c1, <>(rename p)) | Tau p -> Tau(rename p) | Match(c1, c2, a) -> Match (renamec c1, renamec c2, renamep a) and renamec (c1 : chan ) : chan = if c1 = c then c' else c1 in rename;; (********************************************************************* LABELLED TRANSITION SYSTEM We are going to use the "late transition system" defined in [SW, Definition 4.3.1]. This is because it enables us to give a _finite_ list of outcomes of one step of transition, relying on the "image finiteness" properties of the labelled transition system---see [SW, Corollary 1.4.6] (which refers to the "early" transition system) and [SW, Lemma 4.3.2] (which explains the close relationship between late and early transitions). According to [SW, Definition 4.3.1], transitions from a process P take the form p |---act---> p' where act is either the unobservable action (tau), free output (out c1 c2), bound output (out c1(c2)), or bound input (in c1(c2)). We collect act and the residual process p' into a pair and then use name-abstraction to take account of binding. Thus the results of a transition from a process p are given by the values of the datatype value declared below. Given p : proc, (next p) : (value list) returns a finite list of distinct values representing all the possible labelled transitions steps from p. *********************************************************************) type value = (* results of a transition *) TauVal of proc (* |---tau---------> p *) | FrOutVal of chan * chan * proc (* |---out c1 c2---> p *) | BnOutVal of chan * (<>proc) (* |---out c(x)----> p *) | InVal of chan * (<>proc);; (* |---in c(x)-----> p *) (* Helper function for the L-PAR-L rule [SW, Table 4.1] *) let parlVal (p : proc) (v : value) : value = match v with TauVal p1 -> TauVal(Par(p1, p)) | FrOutVal(c1, c2, p2) -> FrOutVal(c1, c2, Par(p2, p)) | BnOutVal(c1, <>p2) -> BnOutVal(c1, <>(Par(p2, p))) | InVal(c1, <>p2) -> InVal(c1, <>(Par(p2, p)));; (* Helper function for the L-PAR-R rule [SW, Table 4.1] *) let parrVal (p : proc) (v : value) : value = match v with TauVal p1 -> TauVal(Par(p, p1)) | FrOutVal(c1, c2, p2) -> FrOutVal(c1, c2, Par(p, p2)) | BnOutVal(c1, <>p2) -> BnOutVal(c1, <>(Par(p, p2))) | InVal(c1, <>p2) -> InVal(c1, <>(Par(p, p2)));; (* Synchronised communication between two values using the COMM-L/R and CLOSE-L/R rules [SW, Table 4.1] *) let syncVal (v : value) (v' : value) : value option = match v with FrOutVal(c1, c2, p) -> (match v' with InVal(c1', <>p') -> if c1 = c1' then Some(TauVal(Par(p, (x |-> c2)p'))) else None | _ -> None) | BnOutVal(c, <>p) -> (match v' with InVal(c', <>p') -> if c = c' then Some(TauVal(Res(<>(Par(p, swap x and x' in p'))))) else None | _ -> None) | InVal(c, <>p) -> (match v' with FrOutVal(c1, c2, p') -> if c = c1 then Some(TauVal(Par((x |-> c2)p, p'))) else None | BnOutVal(c', <>p') -> if c = c' then Some(TauVal(Res(<>(Par((swap x' and x in p), p'))))) else None | _ -> None) | _ -> None;; (* Helper function for the L-RES rule [SW, Table 4.1] *) let resVal (c : chan) (v : value) : value option = match v with TauVal p -> Some(TauVal(Res(<>p))) | FrOutVal(c1, c2, p) -> if c = c1 then None else if c = c2 then Some(BnOutVal(c1, <>p)) else Some(FrOutVal(c1, c2, Res(<>p))) | BnOutVal(c1, <>p) -> if c = c1 then None else Some(BnOutVal(c1, <>(Res(<>p)))) | InVal(c1, <>p) -> if c = c1 then None else Some(InVal(c1, <>(Res(<>p))));; (* Helper function for the L-OPEN rule [SW, Table 4.1] *) let resOpenVal (c :chan) (v : value) : value option = match v with FrOutVal(c1, c2, p) -> if c = c1 then None else if c = c2 then Some(BnOutVal(c1, <>p)) else None | _ -> None;; (* Compute the list of distinct values resulting from one step of transition *) let rec next (p : proc) : value list = match p with Gd(Inact) -> [] | Gd(Pre(Out(c1, c2, p'))) -> [FrOutVal(c1, c2, p')] | Gd(Pre(In(c, abs))) -> [InVal(c, abs)] | Gd(Pre(Tau p1)) -> [TauVal p1] | Gd(Pre(Match(c1, c2, pre))) -> if c1 = c2 then next(Gd(Pre pre)) else [] | Gd(Plus(m,m')) -> (next(Gd m)) ++ (next(Gd m')) | Par(p1,p2) -> let vs1 = next p1 in let vs2 = next p2 in (List.map (parlVal p2) vs1) (* apply the PAR-L rule *) ++ (List.map (parrVal p1) vs2) (* apply the PAR-R rule *) ++ (mapMatrixPartial syncVal vs1 vs2) (* apply the COMM-L/R and CLOSE-L/R rules *) | Res(<>p1) -> let vs = next p1 in (mapPartial (resVal x1) vs) (* apply the RES rule *) ++ (mapPartial (resOpenVal x1) vs) (* apply the OPEN rule *) | Rep(p1) as p2 -> let vs = next p1 in (List.map (parlVal p2) vs) (* apply the REP-ACT rule *) ++ (List.map (parlVal p2) (mapMatrixPartial syncVal vs vs)) (* apply the REP-COMM-L/R and REP-CLOSE-L/R rules *);; (********************************************************************* DISPLAYING PROCESSES Recall that we use the following grammar for pi-calculus processes: processes p ::= m guarded sum p | p composition nu x(p) restriction !p replication guarded sums m ::= 0 inaction a prefixed process m + m summation prefixed processes a ::= out c c. p output prefix in c(x). p input prefix tau. p unobservable prefix [c = c]a match prefix where c,x range over names of channels. Given p : proc, print_next p displays p and the possible labelled transitions from p. Free channel names are displayed using c0, c1,.... and bound ones using x0, x1, x2,... with bound names reused within local scopes. *********************************************************************) (* global state to keep track of free channel names; the free component stores a list associating numbers with names; the fc component is intended to store the length of that list *) type state = { mutable free : (chan * int)list; mutable fc : int };; let s : state = { free = []; fc = 0 };; (* local environment to keep track of bound channel names; the free component is a list associating numbers with names; the bc component is intended to be the length of that list *) type env = { bound : (chan * int)list; bc : int };; (* print a channel in the given environment and current state *) let print_chan (e : env) (c : chan) : unit = try let n = List.assoc c e.bound in print_string "x"; print_int n (* print bound names as xn, with n found from the environment *) with Not_found -> (* if there is no entry in e, assume c is free *) let n = try List.assoc c s.free with Not_found -> (* a newly encountered free name, so update the state *) let { free = cs; fc = n } = s in s.free <- (c,n) :: cs; s.fc <- n+1; n (* print free names as cn *) in print_string "c"; print_int n;; (* helper functions for printing parentheses *) let open_paren (prec : int) (op_prec : int) : unit = if prec > op_prec then print_string "(";; let close_paren (prec : int) (op_prec : int) : unit = if prec > op_prec then print_string ")";; (* the main display function *) let print_next (p : proc) : unit = let rec pr (e : env) (prec : int ) (p : proc) : unit = (* print process p in current state with environment e and operator precedence prec *) match p with Gd m -> pr_g e 0 m; | Par(p1, p2) -> open_paren prec 1; pr e 1 p1; print_string " | "; pr e 1 p2; close_paren prec 1 | Res(<>p1) -> let { bound = cs; bc = n } = e in let e' = { bound = (x, n) :: cs; bc = n+1 } in open_paren prec 2; print_string "nu x"; print_int n; print_string " "; pr e' 2 p1; close_paren prec 2 | Rep p1 -> open_paren prec 2; print_string "!"; pr e 2 p1; close_paren prec 2 and pr_g (e : env) (prec : int ) (m : gsum) : unit = match m with Inact -> print_string "0" | Pre a -> pr_p e 2 a; | Plus(m1, m2) -> open_paren prec 0; pr_g e 0 m1; print_string " + "; pr_g e 0 m2; close_paren prec 0 and pr_p (e : env) (prec : int ) (a : prefix) : unit = match a with Out(c1, c2, p) -> open_paren prec 2; print_string "out "; print_chan e c1; print_string " "; print_chan e c2; print_string ". "; pr e 2 p; close_paren prec 2 | In(c, <>p) -> let { bound = cs; bc = n } = e in let e' = { bound = (x, n) :: cs; bc = n+1 } in open_paren prec 2; print_string "in "; print_chan e c; print_string "(x"; print_int n; print_string "). "; pr e' 2 p; close_paren prec 2 | Tau p -> open_paren prec 2; print_string "tau. "; pr e 2 p; close_paren prec 2 | Match(c1, c2, a') -> open_paren prec 2; print_string "["; print_chan e c1; print_string " = "; print_chan e c2; print_string "]"; pr_p e 2 a'; close_paren prec 2 and pr_v (e : env) (v : value) : unit = match v with TauVal p -> print_string "|---tau---> "; pr e 0 p; print_string "\n\n"; | FrOutVal(c1, c2, p) -> print_string "|---out "; print_chan e c1; print_string " "; print_chan e c2; print_string "---> "; pr e 0 p; print_string "\n\n" | BnOutVal(c, <>p) -> let { bound = cs; bc = n } = e in let e' = { bound = (x, n) :: cs; bc = n+1 } in print_string "|---out "; print_chan e c; print_string "(x"; print_int n; print_string ")---> "; pr e' 0 p; print_string "\n\n" | InVal(c, <>p) -> let { bound = cs; bc = n } = e in let e' = { bound = (x, n) :: cs; bc = n+1 } in print_string "|---in "; print_chan e c; print_string "(x"; print_int n; print_string ")---> "; pr e' 0 p; print_string "\n\n" in (* intialise the state *) s.free <- []; s.fc <- 0; (* initial environment *) let e0 = { bound = []; bc = 0} in (* display p *) pr e0 0 p; print_string "\ncan do the following transitions:\n"; (* display the list of possible lsabelled transitions from p *) List.iter (pr_v e0) (next p);; (********************************************************************* HOW TO USE THIS FILE Start the Fresh O'Caml interactive system in the directory where this file is located. Then do #use "pi-calculator.ml";; at the Fresh O'Caml prompt. Now declare some values p of type proc (one example is given below) and use (printNext p) to display the possible late labelled transitions from the process represented by p. *********************************************************************) let example : proc = (* (nu s (out x s.(out s a.(out s b.(0))))) | in x(w).( (in w(v).(in w(u).(out v u.(0)))) | in z(t).(0) ) This process occurs on p40 of [SW]. *) let a = (fresh : chan) in let b = (fresh : chan) in let s = (fresh : chan) in let t = (fresh : chan) in let u = (fresh : chan) in let v = (fresh : chan) in let w = (fresh : chan) in let x = (fresh : chan) in let z = (fresh : chan) in let p1 = Res(<>(Gd(Pre(Out(x, s, Gd(Pre(Out(s, a, Gd( Pre(Out(s, b, Gd Inact))))))))))) in let p2 = Gd(Pre(In(w, <>(Gd(Pre(In(w, <>( Gd(Pre(Out(v, u, Gd Inact))))))))))) in Par(p1, Gd(Pre(In(x, <>(Par(p2, Gd( Pre(In(z,<>(Gd Inact))))))))));; (* print_next example;; *) (********************************************************************* END of pi-calculator.ml *********************************************************************)