Maude-help mailing list

[rza AT Cs.Nott.AC.UK]

dear All,

 I have received a reply (with a very good suggestion) from Francisco 
Durán regarding my question on Parallel composition in Core Maude.

---------- Forwarded message ----------
From: Francisco Durán 
<duran AT lcc.uma.es>
To: Abdur Rakib 
<rza AT Cs.Nott.AC.UK>
Subject: Re: [Maude-help] Parallel composition in Core Maude
Date: Thu, 30 Jul 2009 00:59:36 -0500

Hi Abdur,

Notice that in rewriting logic you have concurrency in the sense that  
rules can be applied to any (disjoint) subterms concurrently. It looks  
however like you are counting the number of rewrites, and it is clear  
that you need two of your rules to be applied to get what you want.

May be you should write the rules in a different way, perhaps what you  
are looking for is something like

crl C1:Config || C2:Config
  => C1':Config || C2':Config
  if C1:Config => C1':Config /\ C2:Config => C2':Config .

Regards,

Francisco


El 30/07/2009, a las 0:16, 
rza AT Cs.Nott.AC.UK
 escribió:

> Dear Francisco,
>
> Thanks for your kind reply. You are right that we are getting what's  
> expected from the encoding. However, the encoding itself is wrong.
>
> In the encoding : from a given Config < 'a 'e > , Agent1 can fire  
> all three of its rules non-deterministically in one step transition.  
> Similarly from a given Config [ 'A 'D ] , Agent2 can fire all two of  
> its rules non-deterministically in one step transition. Now  
> according to the current encoding if I give a Config < 'a 'e > ||  
> [ 'A 'E ] , then PC will fire all its five rules (basically imported  
> from Agent1 and Agent2) non-deterministically in one step  
> transition. The five branches coming in the following way:
>
>            branch 1 :   [label b] || do nothing
>            branch 2 :   [label c] || do nothing
>            branch 3 :   [label d] || do nothing
>            branch 4 :   do nothing || [label B]
>            branch 5 :   do nothing || [label C]
>
> And the above happens exactly the way I declared the operator op _|| 
> _ : Config Config -> Config [assoc comm] .
>
> However, I would like to declare and define an operator _||_ in such  
> a way so that from a given Config < 'a 'e > || [ 'A 'E ] I will get  
> six branches in one step transition, like the following(where each  
> agent perform an rule firing action parallely)
>
>             branch 1 :  [label b] || [label B]
>             branch 2 :  [label c] || [label B]
>             branch 3 :  [label d] || [label B]
>             branch 4 :  [label b] || [label C]
>             branch 5 :  [label c] || [label C]
>             branch 6 :  [label d] || [label C]
>
>
> Best regards,
> --Abdur
>
>
>
>
>
>
>
> On Jul 30 2009, Francisco Durán wrote:
>
> > Hi Abdur,
> > I don't see what the problem is. Can you explain it?
> > I think you are getting what's expected.
> > Best,
> > Paco
> > ---------------
> > Maude> search < 'a 'a > || ['A 'A ] =>* < w:WM > || [ w1:WM ] .
> > search in PC : < 'a 'a > || ['A 'A] =>* < w:WM > || [w1:WM] .
> > Solution 1 (state 0)
> > states: 1  rewrites: 0 in 0ms cpu (0ms real) (0 rewrites/second)
> > w:WM --> 'a 'a
> > w1:WM --> 'A 'A
> > Solution 2 (state 1)
> > states: 2  rewrites: 1 in 0ms cpu (0ms real) (6944 rewrites/second)
> > w:WM --> 'a 'b
> > w1:WM --> 'A 'A
> > Solution 3 (state 2)
> > states: 3  rewrites: 2 in 0ms cpu (0ms real) (9174 rewrites/second)
> > w:WM --> 'a 'c
> > w1:WM --> 'A 'A
> > Solution 4 (state 3)
> > states: 4  rewrites: 3 in 0ms cpu (0ms real) (10238 rewrites/second)
> > w:WM --> 'a 'd
> > w1:WM --> 'A 'A
> > Solution 5 (state 4)
> > states: 5  rewrites: 4 in 0ms cpu (0ms real) (10989 rewrites/second)
> > w:WM --> 'a 'a
> > w1:WM --> 'A 'B
> > Solution 6 (state 5)
> > states: 6  rewrites: 5 in 0ms cpu (0ms real) (11389 rewrites/second)
> > w:WM --> 'a 'a
> > w1:WM --> 'A 'C
> > Solution 7 (state 6)
> > states: 7  rewrites: 6 in 0ms cpu (0ms real) (11834 rewrites/second)
> > w:WM --> 'b 'b
> > w1:WM --> 'A 'A
> > Solution 8 (state 7)
> > states: 8  rewrites: 7 in 0ms cpu (0ms real) (12237 rewrites/second)
> > w:WM --> 'b 'c
> > w1:WM --> 'A 'A
> > Solution 9 (state 8)
> > states: 9  rewrites: 8 in 0ms cpu (0ms real) (12558 rewrites/second)
> > w:WM --> 'b 'd
> > w1:WM --> 'A 'A
> > Solution 10 (state 9)
> > states: 10  rewrites: 9 in 0ms cpu (0ms real) (12857 rewrites/second)
> > w:WM --> 'a 'b
> > w1:WM --> 'A 'B
> > Solution 11 (state 10)
> > states: 11  rewrites: 10 in 0ms cpu (0ms real) (13106 rewrites/ 
> > second)
> > w:WM --> 'a 'b
> > w1:WM --> 'A 'C
> > Solution 12 (state 11)
> > states: 12  rewrites: 12 in 0ms cpu (0ms real) (14319 rewrites/ 
> > second)
> > w:WM --> 'c 'c
> > w1:WM --> 'A 'A
> > Solution 13 (state 12)
> > states: 13  rewrites: 13 in 0ms cpu (0ms real) (14380 rewrites/ 
> > second)
> > w:WM --> 'c 'd
> > w1:WM --> 'A 'A
> > Solution 14 (state 13)
> > states: 14  rewrites: 14 in 0ms cpu (1ms real) (14432 rewrites/ 
> > second)
> > w:WM --> 'a 'c
> > w1:WM --> 'A 'B
> > Solution 15 (state 14)
> > states: 15  rewrites: 15 in 1ms cpu (1ms real) (14478 rewrites/ 
> > second)
> > w:WM --> 'a 'c
> > w1:WM --> 'A 'C
> > Solution 16 (state 15)
> > states: 16  rewrites: 18 in 1ms cpu (1ms real) (16245 rewrites/ 
> > second)
> > w:WM --> 'd 'd
> > w1:WM --> 'A 'A
> > Solution 17 (state 16)
> > states: 17  rewrites: 19 in 1ms cpu (1ms real) (16253 rewrites/ 
> > second)
> > w:WM --> 'a 'd
> > w1:WM --> 'A 'B
> > Solution 18 (state 17)
> > states: 18  rewrites: 20 in 1ms cpu (1ms real) (16220 rewrites/ 
> > second)
> > w:WM --> 'a 'd
> > w1:WM --> 'A 'C
> > Solution 19 (state 18)
> > states: 19  rewrites: 24 in 1ms cpu (1ms real) (18362 rewrites/ 
> > second)
> > w:WM --> 'a 'a
> > w1:WM --> 'B 'B
> > Solution 20 (state 19)
> > states: 20  rewrites: 25 in 1ms cpu (1ms real) (18274 rewrites/ 
> > second)
> > w:WM --> 'a 'a
> > w1:WM --> 'B 'C
> > Solution 21 (state 20)
> > states: 21  rewrites: 30 in 1ms cpu (1ms real) (20790 rewrites/ 
> > second)
> > w:WM --> 'a 'a
> > w1:WM --> 'C 'C
> > Solution 22 (state 21)
> > states: 22  rewrites: 31 in 1ms cpu (1ms real) (20489 rewrites/ 
> > second)
> > w:WM --> 'b 'b
> > w1:WM --> 'A 'B
> > Solution 23 (state 22)
> > states: 23  rewrites: 32 in 1ms cpu (1ms real) (20343 rewrites/ 
> > second)
> > w:WM --> 'b 'b
> > w1:WM --> 'A 'C
> > Solution 24 (state 23)
> > states: 24  rewrites: 33 in 1ms cpu (1ms real) (20109 rewrites/ 
> > second)
> > w:WM --> 'b 'c
> > w1:WM --> 'A 'B
> > Solution 25 (state 24)
> > states: 25  rewrites: 34 in 1ms cpu (1ms real) (19976 rewrites/ 
> > second)
> > w:WM --> 'b 'c
> > w1:WM --> 'A 'C
> > Solution 26 (state 25)
> > states: 26  rewrites: 35 in 1ms cpu (1ms real) (19785 rewrites/ 
> > second)
> > w:WM --> 'b 'd
> > w1:WM --> 'A 'B
> > Solution 27 (state 26)
> > states: 27  rewrites: 36 in 1ms cpu (1ms real) (19704 rewrites/ 
> > second)
> > w:WM --> 'b 'd
> > w1:WM --> 'A 'C
> > Solution 28 (state 27)
> > states: 28  rewrites: 40 in 1ms cpu (2ms real) (21019 rewrites/ 
> > second)
> > w:WM --> 'a 'b
> > w1:WM --> 'B 'B
> > Solution 29 (state 28)
> > states: 29  rewrites: 41 in 1ms cpu (2ms real) (20843 rewrites/ 
> > second)
> > w:WM --> 'a 'b
> > w1:WM --> 'B 'C
> > Solution 30 (state 29)
> > states: 30  rewrites: 46 in 2ms cpu (2ms real) (22515 rewrites/ 
> > second)
> > w:WM --> 'a 'b
> > w1:WM --> 'C 'C
> > Solution 31 (state 30)
> > states: 31  rewrites: 47 in 2ms cpu (2ms real) (22296 rewrites/ 
> > second)
> > w:WM --> 'c 'c
> > w1:WM --> 'A 'B
> > Solution 32 (state 31)
> > states: 32  rewrites: 48 in 2ms cpu (2ms real) (22150 rewrites/ 
> > second)
> > w:WM --> 'c 'c
> > w1:WM --> 'A 'C
> > Solution 33 (state 32)
> > states: 33  rewrites: 49 in 2ms cpu (2ms real) (21904 rewrites/ 
> > second)
> > w:WM --> 'c 'd
> > w1:WM --> 'A 'B
> > Solution 34 (state 33)
> > states: 34  rewrites: 50 in 2ms cpu (2ms real) (21758 rewrites/ 
> > second)
> > w:WM --> 'c 'd
> > w1:WM --> 'A 'C
> > Solution 35 (state 34)
> > states: 35  rewrites: 54 in 2ms cpu (2ms real) (22756 rewrites/ 
> > second)
> > w:WM --> 'a 'c
> > w1:WM --> 'B 'B
> > Solution 36 (state 35)
> > states: 36  rewrites: 55 in 2ms cpu (2ms real) (22550 rewrites/ 
> > second)
> > w:WM --> 'a 'c
> > w1:WM --> 'B 'C
> > Solution 37 (state 36)
> > states: 37  rewrites: 60 in 2ms cpu (2ms real) (23856 rewrites/ 
> > second)
> > w:WM --> 'a 'c
> > w1:WM --> 'C 'C
> > Solution 38 (state 37)
> > states: 38  rewrites: 61 in 2ms cpu (2ms real) (23643 rewrites/ 
> > second)
> > w:WM --> 'd 'd
> > w1:WM --> 'A 'B
> > Solution 39 (state 38)
> > states: 39  rewrites: 62 in 2ms cpu (2ms real) (23493 rewrites/ 
> > second)
> > w:WM --> 'd 'd
> > w1:WM --> 'A 'C
> > Solution 40 (state 39)
> > states: 40  rewrites: 66 in 2ms cpu (2ms real) (24300 rewrites/ 
> > second)
> > w:WM --> 'a 'd
> > w1:WM --> 'B 'B
> > Solution 41 (state 40)
> > states: 41  rewrites: 67 in 2ms cpu (2ms real) (24126 rewrites/ 
> > second)
> > w:WM --> 'a 'd
> > w1:WM --> 'B 'C
> > Solution 42 (state 41)
> > states: 42  rewrites: 72 in 2ms cpu (3ms real) (25263 rewrites/ 
> > second)
> > w:WM --> 'a 'd
> > w1:WM --> 'C 'C
> > Solution 43 (state 42)
> > states: 43  rewrites: 82 in 2ms cpu (3ms real) (27758 rewrites/ 
> > second)
> > w:WM --> 'b 'b
> > w1:WM --> 'B 'B
> > Solution 44 (state 43)
> > states: 44  rewrites: 83 in 3ms cpu (3ms real) (27492 rewrites/ 
> > second)
> > w:WM --> 'b 'b
> > w1:WM --> 'B 'C
> > Solution 45 (state 44)
> > states: 45  rewrites: 85 in 3ms cpu (3ms real) (27525 rewrites/ 
> > second)
> > w:WM --> 'b 'b
> > w1:WM --> 'C 'C
> > Solution 46 (state 45)
> > states: 46  rewrites: 86 in 3ms cpu (3ms real) (27249 rewrites/ 
> > second)
> > w:WM --> 'b 'c
> > w1:WM --> 'B 'B
> > Solution 47 (state 46)
> > states: 47  rewrites: 87 in 3ms cpu (3ms real) (27060 rewrites/ 
> > second)
> > w:WM --> 'b 'c
> > w1:WM --> 'B 'C
> > Solution 48 (state 47)
> > states: 48  rewrites: 89 in 3ms cpu (3ms real) (27092 rewrites/ 
> > second)
> > w:WM --> 'b 'c
> > w1:WM --> 'C 'C
> > Solution 49 (state 48)
> > states: 49  rewrites: 90 in 3ms cpu (3ms real) (26873 rewrites/ 
> > second)
> > w:WM --> 'b 'd
> > w1:WM --> 'B 'B
> > Solution 50 (state 49)
> > states: 50  rewrites: 91 in 3ms cpu (3ms real) (26686 rewrites/ 
> > second)
> > w:WM --> 'b 'd
> > w1:WM --> 'B 'C
> > Solution 51 (state 50)
> > states: 51  rewrites: 93 in 3ms cpu (3ms real) (26693 rewrites/ 
> > second)
> > w:WM --> 'b 'd
> > w1:WM --> 'C 'C
> > Solution 52 (state 51)
> > states: 52  rewrites: 103 in 3ms cpu (3ms real) (28746 rewrites/ 
> > second)
> > w:WM --> 'c 'c
> > w1:WM --> 'B 'B
> > Solution 53 (state 52)
> > states: 53  rewrites: 104 in 3ms cpu (3ms real) (28540 rewrites/ 
> > second)
> > w:WM --> 'c 'c
> > w1:WM --> 'B 'C
> > Solution 54 (state 53)
> > states: 54  rewrites: 106 in 3ms cpu (4ms real) (28349 rewrites/ 
> > second)
> > w:WM --> 'c 'c
> > w1:WM --> 'C 'C
> > Solution 55 (state 54)
> > states: 55  rewrites: 107 in 3ms cpu (4ms real) (28083 rewrites/ 
> > second)
> > w:WM --> 'c 'd
> > w1:WM --> 'B 'B
> > Solution 56 (state 55)
> > states: 56  rewrites: 108 in 3ms cpu (4ms real) (27885 rewrites/ 
> > second)
> > w:WM --> 'c 'd
> > w1:WM --> 'B 'C
> > Solution 57 (state 56)
> > states: 57  rewrites: 110 in 3ms cpu (4ms real) (27904 rewrites/ 
> > second)
> > w:WM --> 'c 'd
> > w1:WM --> 'C 'C
> > Solution 58 (state 57)
> > states: 58  rewrites: 120 in 4ms cpu (4ms real) (29680 rewrites/ 
> > second)
> > w:WM --> 'd 'd
> > w1:WM --> 'B 'B
> > Solution 59 (state 58)
> > states: 59  rewrites: 121 in 4ms cpu (4ms real) (29504 rewrites/ 
> > second)
> > w:WM --> 'd 'd
> > w1:WM --> 'B 'C
> > Solution 60 (state 59)
> > states: 60  rewrites: 123 in 4ms cpu (4ms real) (29524 rewrites/ 
> > second)
> > w:WM --> 'd 'd
> > w1:WM --> 'C 'C
> > No more solutions.
> > states: 60  rewrites: 132 in 4ms cpu (4ms real) (30520 rewrites/ 
> > second)
> > El 29/07/2009, a las 18:24, 
> > rza AT Cs.Nott.AC.UK
> >  escribió:
> > > Hi All,
> > >
> > >  Could you please help me, if you have an idea on how to achieve   
> > > Parallel Composition when modeling a Multi-agent system in Core   
> > > Maude . I have a very simple example below, there are two rule- 
> > based  > agents (modules) viz. Agent1 and Agent2. Each of them  
> > having some  > rules that they can fire non-deterministically. Now  
> > I would like to  > declare another module, say PC which will  
> > contain a parallel  > composition operator using which agents can  
> > fire rules concurrently.  > In the following model it can't be  
> > achieved but I am seeking a help  > on how can I model PC? if it is  
> > really possible. I saw a paper  > "Implementing CCS in Maude..."  
> > but I could not use the idea...
> > >
> > > Best regds,
> > > --Abdur
> > >
> > > **********************************************
> > > *****************Model*********************
> > > mod Sorts-Decl is
> > > pr QID .
> > > sorts Constant WM Config .  *** WM stands for working memory
> > > subsort Qid < Constant .
> > > subsort Constant < WM .
> > > op __ : WM WM -> WM [comm assoc] .
> > > endm
> > >
> > >
> > >
> > > mod Agent1 is
> > > pr Sorts-Decl .
> > > op <_> : WM -> Config .
> > > var w : WM .
> > > rl [b] : < 'a w >  => < 'b w > .
> > > rl [c] : < 'a w >  => < 'c w > .
> > > rl [d] : < 'a w >  => < 'd w > .
> > > endm
> > >
> > >
> > >
> > > mod Agent2 is
> > > pr Sorts-Decl .
> > > op [_] : WM -> Config .
> > > var w : WM .
> > > rl [B] : [ 'A w ]  => [ 'B w ] .
> > > rl [C] : [ 'A w ]  => [ 'C w ] .
> > > endm
> > >
> > >
> > > mod PC is
> > >
> > > pr Agent1 .
> > > pr Agent2 .
> > >
> > > op _||_ : Config Config -> Config [assoc comm] .
> > >
> > > endm
> > >
> > > *********************************************************
> > > *********************************************************
> > >
> > > These are the outputs which definitely not parallel composition
> > > when exploring the search space......
> > >
> > > Maude> search < 'a 'd > || ['A 'D ] =>* < 'c w:WM > || [ w1:WM ] .
> > > search in PC : < 'a 'd > || ['A 'D] =>* < 'c w:WM > || [w1:WM] .
> > >
> > > Solution 1 (state 2)
> > > states: 3  rewrites: 2 in 0ms cpu (0ms real) (~ rewrites/second)
> > > w:WM --> 'd
> > > w1:WM --> 'A 'D
> > >
> > > Solution 2 (state 8)
> > > states: 9  rewrites: 8 in 0ms cpu (0ms real) (~ rewrites/second)
> > > w:WM --> 'd
> > > w1:WM --> 'B 'D
> > >
> > > Solution 3 (state 9)
> > > states: 10  rewrites: 9 in 0ms cpu (0ms real) (~ rewrites/second)
> > > w:WM --> 'd
> > > w1:WM --> 'C 'D
> > >
> > > No more solutions.
> > > states: 12  rewrites: 17 in 0ms cpu (0ms real) (~ rewrites/second)
> > > Maude> show search graph .
> > > state 0, Config: < 'a 'd > || ['A 'D]
> > > arc 0 ===> state 1 (rl < 'a w:WM > => < 'b w:WM > [label b] .)
> > > arc 1 ===> state 2 (rl < 'a w:WM > => < 'c w:WM > [label c] .)
> > > arc 2 ===> state 3 (rl < 'a w:WM > => < 'd w:WM > [label d] .)
> > > arc 3 ===> state 4 (rl ['A w:WM] => ['B w:WM] [label B] .)
> > > arc 4 ===> state 5 (rl ['A w:WM] => ['C w:WM] [label C] .)
> > >
> > > state 1, Config: < 'b 'd > || ['A 'D]
> > > arc 0 ===> state 6 (rl ['A w:WM] => ['B w:WM] [label B] .)
> > > arc 1 ===> state 7 (rl ['A w:WM] => ['C w:WM] [label C] .)
> > >
> > > state 2, Config: < 'c 'd > || ['A 'D]
> > > arc 0 ===> state 8 (rl ['A w:WM] => ['B w:WM] [label B] .)
> > > arc 1 ===> state 9 (rl ['A w:WM] => ['C w:WM] [label C] .)
> > >
> > > state 3, Config: < 'd 'd > || ['A 'D]
> > > arc 0 ===> state 10 (rl ['A w:WM] => ['B w:WM] [label B] .)
> > > arc 1 ===> state 11 (rl ['A w:WM] => ['C w:WM] [label C] .)
> > >
> > > state 4, Config: < 'a 'd > || ['B 'D]
> > > arc 0 ===> state 6 (rl < 'a w:WM > => < 'b w:WM > [label b] .)
> > > arc 1 ===> state 8 (rl < 'a w:WM > => < 'c w:WM > [label c] .)
> > > arc 2 ===> state 10 (rl < 'a w:WM > => < 'd w:WM > [label d] .)
> > >
> > > state 5, Config: < 'a 'd > || ['C 'D]
> > > arc 0 ===> state 7 (rl < 'a w:WM > => < 'b w:WM > [label b] .)
> > > arc 1 ===> state 9 (rl < 'a w:WM > => < 'c w:WM > [label c] .)
> > > arc 2 ===> state 11 (rl < 'a w:WM > => < 'd w:WM > [label d] .)
> > >
> > > state 6, Config: < 'b 'd > || ['B 'D]
> > >
> > > state 7, Config: < 'b 'd > || ['C 'D]
> > >
> > > state 8, Config: < 'c 'd > || ['B 'D]
> > >
> > > state 9, Config: < 'c 'd > || ['C 'D]
> > >
> > > state 10, Config: < 'd 'd > || ['B 'D]
> > >
> > > state 11, Config: < 'd 'd > || ['C 'D]
> > > Maude>
> > >
> > >
> > > This message has been checked for viruses but the contents of an   
> > > attachment
> > > may still contain software viruses, which could damage your  
> > computer  > system:
> > > you are advised to perform your own checks. Email communications   
> > > with the
> > > University of Nottingham may be monitored as permitted by UK  >  
> > legislation.
> > >
> > > _______________________________________________
> > > Maude-help mailing list
> > > 
> > Maude-help AT maude.cs.uiuc.edu
> > > http://maude.cs.uiuc.edu/cgi-bin/mailman/listinfo/maude-help
>
> This message has been checked for viruses but the contents of an  
> attachment
> may still contain software viruses, which could damage your computer  
> system:
> you are advised to perform your own checks. Email communications  
> with the
> University of Nottingham may be monitored as permitted by UK  
> legislation.



This message has been checked for viruses but the contents of an attachment
may still contain software viruses, which could damage your computer system:
you are advised to perform your own checks. Email communications with the
University of Nottingham may be monitored as permitted by UK legislation.