(C) Ralf Lämmel, Andrei Varanovich, University of Koblenz Landau
Logistics
- Course site
- Date published: 09 Jan 2013
- Deadline SVN: 15 Jan 2013 (End of Day)
- SVN: https://svn.uni-koblenz.de/softlang/main/courses/plt1213/students + group name
- Present your solution with your own system.
- Lab assistant calls up teams.
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.