Plt2013 8

(C) Ralf Lämmel, Andrei Varanovich, University of Koblenz Landau

Logistics

Assignment

This assignment relates to the following simple Prolog code for CCS:

https://github.com/rlaemmel/pltcourse/tree/master/src/ccs

See system.pro for the definition of a sample system and its explanation.

Understanding the one-step relation

Consider the following trace of applying the relation to the sample system.

$ pwd
/home/billg/projects/pltcourse/src/ccs
$ swipl -q -f main.pro 
?- step(name(system),A,E).
A = out(foo),
E = (name(producer)'|'name(consumer)) ;
A = out(bar),
E = (name(producer)'|'name(consumer)) ;
A = in(foo),
E = (name(producer)'|'out(bla), name(consumer)) ;
A = in(bar),
E = (name(producer)'|'out(bla), name(consumer)) ;
A = tau,
E = (name(producer)'|'out(bla), name(consumer)) ;
A = tau,
E = (name(producer)'|'out(bla), name(consumer)).

?-

Clearly, several actions are possibly according to the one-step relation. Please, explain the resulting actions. Are any of these actions less "desirable" than others? Please, explain all rules for the one-step relation and clarify how the rules relate to the formal definition described in the lecture (slide 31).

Understanding the closure relation

Consider the following trace of applying the relation to the sample system.

$ swipl -q -f main.pro 
?- many(2,name(system),L,E).
L = [out(foo), out(foo)],
E = (name(producer)'|'name(consumer)) .

?-

Please, explain in some convincing manner (relating to formal details of syntax and semantics of CCS) why we need a restriction on length (or some other restriction) when taking the closure of the one-step relation. We didn't need this sort of restriction in any previous setting in this course. How come?

Implement restriction

Please, extend the Prolog code to cover label restriction (i.e., internalization of labels) as discussed and formalized in the lecture. Once you have implemented restriction, please revise the definition of system so that you make use of it. That is, the system should only talk to itself in terms of foos and bars. Demonstrate the difference by using step/3 or many/4.

Implement relabeling.

Please, extend the Prolog code to cover relabeling as discussed and formalized in the lecture. Once you have implemented relabeling, please revise the definition of system so that you make use of it — somehow.