Home Work Exercise -- Week 1 on CCS


Note. Please explain what is going on, what are the processes (capable
of) doing, what are you thinking.



1) Consider the following CCS processes:

    Susan   =def   'work . 'coin . coke . Susan ;
    Robert  =def   'play . Robert + coke . Robert ;

    Disp1   =def   coin . ('coke . Disp1 + 'sprite . Disp1) ;
    Disp2   =def   coin . 'coke . Disp2 + coin . 'sprite . Disp2 ;

    SysA    =def   ( Disp1 | Susan ) \ {coin,coke,sprite} ;
    SysB    =def   ( Disp2 | Susan ) \ {coin,coke,sprite} ;
    SysC    =def   ( ( Disp1 | Susan ) | Robert ) \ {coin,coke,sprite} ;

a) Give the shortest derivation sequence (completely specified with
all inference trees) that leads to deadlock(*) (if it exists) and the
transition diagram for process: SysA 

b) Give the shortest derivation sequence (completely specified with
all inference trees) that leads to deadlock(*) (if it exists) and the
transition diagram for process: SysB 

c) Give the set of all traces and the transition diagram for process:
SysC




* Deadlock is when a process P is different from 0 and gets stuck
  i.e. there is no applicable rule such that P --a-> P' (where a is an
  action).


2) You are given two Christmas lights connected by a cable. Each light
has a small programmable controller which can send a signal to the
light, making it flash. The two controllers can also send signals to
each other. Define a process which models this system in such a way
that the lights flash in the order 1,2,1,2,1,2,...