[prev in list] [next in list] [prev in thread] [next in thread] 

List:       avispa-users
Subject:    [Avispa-users] Send a set over a channel
From:       Pura Mihai <puramihai () gmail ! com>
Date:       2010-03-17 8:59:02
Message-ID: b61346f11003170159u1190657em9f3eb7f03cfc57f3 () mail ! gmail ! com
[Download RAW message or body]

[Attachment #2 (multipart/alternative)]


I have just tested the approach suggested by Tigran S. Avanesov:

role node(N   : agent,
            RouteN : message,
            Snd, Rcv  : channel(dy))
played_by N def=
local State : nat,
    RP : text,
    T,I : agent,
    Ni : text
init State := 1
transition
forwardrdp. State = 1 /\ Rcv(RP'.I'.T'.Ni'.RouteN')
          =|> State' := 1 /\  Snd(RP'.I'.T'.Ni'.RouteN'.N)
end role

The problem is that in environment role I have several instances for the
role node. And all these instances should do the same thing: receive the
message, add their identities and then send the message to the next node.
Using the above approach the message format changes for each forwarding. So
the next node will not accept the forwarded message.

For example:
       node(U,S2,R2)
      /\node(K,S4,R4)
      /\target(V,S3,R3)

the second node will not accept de message

Mihai

[Attachment #5 (text/html)]

<div>I have just tested the approach suggested by Tigran S. Avanesov:</div>
<div> </div>
<div>role node(N   : agent,<br>            RouteN : message,</div>
<div>            Snd, Rcv  : channel(dy))<br>played_by N def=<br>local State : \
nat,<br>    RP : text,<br>    T,I : agent,<br>    Ni : text<br>init State := \
1<br>transition<br>forwardrdp. State = 1 /\ \
Rcv(RP&#39;.I&#39;.T&#39;.Ni&#39;.RouteN&#39;)</div>

<div>          =|&gt; State&#39; := 1 /\  \
Snd(RP&#39;.I&#39;.T&#39;.Ni&#39;.RouteN&#39;.N)<br>end role</div> <div> </div>
<div>The problem is that in environment role I have several instances for the role \
node. And all these instances should do the same thing: receive the message, add \
their identities and then send the message to the next node.. Using the above \
approach the message format changes for each forwarding. So the next node will not \
accept the forwarded message.</div>

<div> </div>
<div>For example:</div>
<div>       node(U,S2,R2)<br>      /\node(K,S4,R4)<br>      /\target(V,S3,R3) </div>
<div> </div>
<div>the second node will not accept de message </div>
<div> </div>
<div>Mihai</div>
<div> </div>



_______________________________________________
Avispa-users mailing list
Avispa-users@avispa-project.org
http://mail63.csoft.net/mailman/listinfo/avispa-users


[prev in list] [next in list] [prev in thread] [next in thread]