Enter a pi-calculus in the box below, and press the "submit" button to invoke deadlock-free analysis. Examples are given below. Note that on this web interface, only small examples can be tested (as the time-out is set to 1 second). To test larger examples or other features of TyPiCal, please download the source code from here.

/*** one input and one ouput ***/ x?y | x!1

/*** deadlocked process ***/ new x in new y in x?z.y!z | y?z.x!z

/*** Not deadlocked --- there is an ouput x! to break the deadlock ***/ new x in new y in x?z.y!z | y?z.x!z | x!1

/*** lock-free, two dining philosophers ***/ new philos1 in new philos2 in new fork1 in new fork2 in /*** a left-handed philosopher, who picks the left fork first ***/ *philos1?x.(let left=fst(x) in let right=snd(x) in left?w.right?w.(left!() | right!() | eating1!() | philos1!(left,right))) | philos1!(fork1,fork2) | /*** a left-handed philosopher, who picks the left fork first ***/ *philos2?x.(let left=fst(x) in let right=snd(x) in right?w.left?w.(left!() | right!() | eating2!() | philos2!(left,right))) | philos2!(fork2,fork1) | /*** forks ***/ fork1!() | fork2!()

/*** deadlocked, two dining philosophers ***/ new philos1 in new philos2 in new fork1 in new fork2 in /*** a left-handed philosopher, who picks the left fork first ***/ *philos1?x.(let left=fst(x) in let right=snd(x) in left?w.right?w.(left!() | right!() | eating1!() | philos1!(left,right))) | philos1!(fork1,fork2) | /*** a right-handed philosopher, who picks the left fork first ***/ *philos2?x.(let left=fst(x) in let right=snd(x) in left?w.right?w.(left!() | right!() | eating2!() | philos2!(left,right))) | philos2!(fork2,fork1) | /*** forks ***/ fork1!() | fork2!()

/**** The symbol table example taken from **** Deng and Sangiorgi, "Ensuring Termination by Typability," Information and Computation **** The changes from the original example are: **** (1) Synchronous outputs have been replaced with asynchronous ones. **** (2) nil has been replaced by a dummy channel, and an extra parameter has been added to p, **** which expresses whether b is nil. ****/ (new p in *(p?x. let a=fst(x) in let b=fst(snd(x)) in let n=fst(snd(snd(x))) in let s = fst(snd(snd(snd(x)))) in let empty = snd(snd(snd(snd(x)))) in /*** p?(a,b,n,s,empty). ***/ a?y.let t = fst(y) in let r = snd(y) in /*** a?(t,r). ***/ if t=s then (r!n | p!(a,(b,(n,(s,empty))))) else if empty then (r!(n+1) | new c in new dummy in (p!(c,(dummy,(n+1,(t,true)))) | p!(a,(c,(n,(s,false)))) | *dummy?z.let r=snd(z) in r!0))/*** A dummy process to respond to any request immediately. Actually, it is never called.***/ else (b!(t,r) | p!(a,(b,(n,(s,false)))))) | (new dummy in p!(a,(dummy,(1,(s0,true)))) | *dummy?z.let r=snd(z) in r!0) ) | a!(1,r1) | a!(2,r2) | a!(3,r3) | a!(4,r3) | r1?x.O | r2?x.O