Termination in a deadlocked state
Currently SePi does not distinguish normal termination from termination due to a deadlocked situation.
This process terminates successfully
new x y : *!integer x!77
even though in the end there is a process in the x-y channel queue. This is ok for x-y is unrestricted. In this case, I suggest that we leave the final message of the interpreter as is:
<terminated>
This process terminates in a a deadlocked situation:
new x y : !integer.end x!5. y?x
In the end, there is a process in the x-y channel queue. But x-y is linear. In this case I suggest that the interpreter ends with something like this:
<deadlock on channel x-y>
Similarly, at the end of the run of this process
new w1 r1 : !integer.end new w2 r2 : !integer.end w1!5. w2!7 | r2?x. r1?y
we should read
<deadlock on channels w1-x1 and w2-x2>