CCS Examples

Counter.json

{
  "showCode": true,
  "gravity": false,
  "showLabels": false,
  "showGlobals": false
}

Counter.pi

// INITIALLY Counter value is 0 //
Z[i,d,z]|E[i,d,z]

// DEFINITIONS //

// Zero process
Z[i,d,z] :=
    z<>.Z[i,d,z]
  + i().new r.(
      BZ[r,i,d,z] | C[r,i,d,z]
  )
// Blocked Zero process
BZ[r,i,d,z] := r().Z[i,d,z]

// Successor process
// r is the name of the next process
C[r,i,d,z] :=
    d().Fire[r]
  + i().new s.(
      BC[s,r,i,d,z] | C[s,i,d,z]
  )
// Blocked successor, waiting on s
BC[s,r,i,d,z] := s().C[r,i,d,z]
Fire[r] := r<>

// Environment just to trigger actions randomly
E[i,d,z] :=
    i<>.E[i,d,z]
  + d<>.E[i,d,z]
  + z().E[i,d,z]