Morse Reseach group

A simulation tool for tccp programs

This tool is an interpreter for simulating tccp programs. The tool accepts as an input a tccp program with linear constraints over arithmetic variables, and logic constraints over streams. A stream can store text or linear expressions over arithmetic variables.

Below, we present two examples to show how the tool works. Both of the examples are available for simulating at the online simulator selecting photocopier_dummy.tccp or train_dummy.tccp file.

Photocopier example

This program models a photocopier by means of four procedure declarations which represent the user process user(C,A), the photocopier photocopier(C,A,MIdle,E,T), the system process system(MIdle,E,C,A,T) and the initialization of such processes initialize(MIdle).

Streams C and A are the communication channels through which the user sends commands to the photocopier, and the photocopier communicates its state to the user, respectively.

The user waits for the photocopier to be free to send it a new command (make a copy (c), turn on/off (on/off) or do nothing (true)), which is non deterministically chosen. Agent photocopier uses stream T as a counter to check whether a command has been received during MIdle time units and, in another case, to automatically turn off. In the case deadline MIdle has not been reached, agent photocopier accepts the command sent by the user, and behaves accordingly, updating its local state, in stream E, and counter T.

Agent system is in charge of creating and synchronising agents photocopier and user correctly. Finally, initialize creates the initial agents and streams and establishes the value of the time deadline MIdle.

photocopier_dummy.tccp
{user(C,A):- ask(A=[free|_])->tell(true).
 
photocopier(C,A,MIdle,E,T):- exist Aux,Aux',T'
                (tell(T=[Aux|T'])
                || ask(true) -> 
                    now(Aux>0) then
                        now(C=[on|_]) then
                            (tell(E=[going|_]) || tell(T'=[MIdle|_]) || tell(A=[free|_]))
                        else now(C=[off|_]) then
                            (tell(E=[sTOP|_]) || tell(T'=[MIdle|_]) || tell(A=[free|_]))
                             else now(C=[c|_]) then
                                (tell(E=[going|_]) || tell(T'=[MIdle|_]) || tell(A=[free|_]))
                              else (tell(Aux'=Aux-1) || tell(T'=[Aux'|_]) || tell(A=[free|_]))    
                    else (tell(E=[sTOP|_]) || tell(A=[free|_]))).
 
system(MIdle,E,C,A,T):- exist E',C',A',T' (tell(E=[_|E']) 
                       || tell(C=[_|C']) 
                       || tell(A=[_|A']) 
                       || tell(T=[_|T']) 
                       || user(C,A) 
                       || ask(true) -> photocopier(C,A',MIdle,E',T) 
                       || ask(A'=[free|_]) -> (system(MIdle,E',C',A',T'))).
 
initialize(MIdle):- exist E,C,A,T (tell(A=[free|_]) 
                   || tell(T=[MIdle|_]) 
                   || tell(E=[off|_]) 
                   || system(MIdle,E,C,A,T)).
}.initialize(5)

Using the call initialize(MIdle) || tell(MIdle = 5), Figure 1 depicts the state of the store after carrying out 7 steps of the simulation. On the left hand side, we have the symbol table in which each node is created by a procedure call or an exists agent. The root node (N0) is created because the procedure call initialize(MIdle) that contains the parameter MIdle set to 5. In the next step, an exists agent is executed which creates the node N1 containing the list of local variables. Then, several tell agents and a procedure call to system are executed in parallel. The tell agents add values to the heads of A, T and E, and the procedure call adds a new node (N2) with the list of parameters of system pointing to the variables used in the call. In the following step, the exists agent is executed which creates a new node (N3), and the parallel agent comprising four tell agents, a procedure call to user and two ask agents. The first ask can proceed, but the second one blocks because A’ is unbound. Due to parallel execution of the procedure calls (user(C,A) SS photocopier(C,A’,MIdle,E’,T’)), nodes N3 and N4 are created. The rest of the nodes are generated in a similar way. The main memory, on the right, holds information about the value of the variables during the execution. For example, positions 0 and 17 store the information of the variables of the system (MIdle, Aux and Aux’). Observe that Aux (position 5) is a reference to position 0, which keeps a variable represented in disc poly by dimension 0. Another type of element in memory are functors, which represent stream variables. For example, position 1 is a functor whose head is a constant set to free, and whose tail is a reference to 15.

Figure 1: Photocopier example – store state 7 steps

Train example

The system consists of three main procedures: train, gate and gate control and init, the procedure for initialising the system.

Procedure train sends message near to the control when it is approaching the crossing. It also sends the message out when it has passed through the crossing.

Procedure control receives the message from the train, and controls that the gate is going down and up. Control always expects the confirmation from the gate.

The procedure gate receives message from control, and it changes its state to down or up and responds properly.

train_dummy.tccp
{train(ToC,T) :- exist ToC',ToC'',T',T'' 
        (ask(true)->
            (tell(ToC=[near|ToC']) 
            || ask(true)-> ask(true) -> 
                (tell(T=[enter|T']) 
                || ask(true)->ask(true)->ask(true)->ask(true) -> 
                      (tell(T'=[leave|T'']) || tell(ToC'=[out|ToC'']) || train(ToC'',T''))))).    

controller(ToC,ToG,FromG):- exist ToC',ToG',FromG'
            (ask(ToC=[near|_])->
                (tell(ToC=[near|ToC']) 
                || tell(ToG=[down|ToG']) 
                || ask(FromG=[confirm|_]) -> 
                    (tell(FromG=[confirm|FromG']) || controller(ToC',ToG',FromG')))
            +ask(ToC=[out|_])->
                (tell(ToC=[out|ToC']) 
                || tell(ToG=[up|ToG']) 
                || ask(FromG=[confirm|_]) -> 
                    (tell(FromG=[confirm|FromG']) || controller(ToC',ToG',FromG')))).

gate(FromG,ToG,G):-exist FromG',ToG',G'
            (ask(ToG=[down|_])->(tell(ToG=[down|ToG']) || 
                         ask(true)->ask(true)->
                            (tell(G=[down|G']) || tell(FromG=[confirm|FromG']) || gate(FromG',ToG',G')))
            +ask(ToG=[up|_])->(tell(ToG=[up|ToG']) ||
                      ask(true)->ask(true)->
                            (tell(G=[upn|G']) || tell(FromG=[confirm|FromG']) || gate(FromG',ToG',G')))).

init:-exist ToC,T,ToG,FromG,G  (train(ToC,T)
                ||controller(ToC,ToG,FromG)
                ||gate(FromG,ToG,G)).
}.init

In the railway system, the train process selects the second branch of the choice.

Figure 2 shows the state of the global store after executing 10 steps of the railway example. The init() procedure call does not have arguments, so the root node does not contain local variables.

The next exists agent creates node N1 with the local variables. Then, a parallel agent, comprising three procedure calls, is executed. They create three new nodes. The rest of the nodes are created in a similar way.

This tccp example does not have numeric variables, all variables used are stream variables. For this reason, the discrete polyhedron will be true for the entire execution. After 10 steps, the memory has 7 streams that we set up in functor type. For instance, there is a stream at position 4 whose head is a constant stored in position 20 (contains the constant value down) and its tail is a reference to the position 22, which is unbound.

Figure 2: Railway example – store state 10 steps