Web Demo Interface for TyPiCal: Type-based static analyzer for the Pi-Calculus

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.


Examples

Cut and paste an example below into the box above. In the output, the red color shows an input (?) or output (!) that may get deadlocked, and the blue color shows an input or output that is deadlock-free.

Example 1

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

Example 2

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

Example 3

/*** 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

Example 4

/*** 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!()

Example 5

/*** 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!()

Example 6

/**** 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