Maude-help mailing list

[rza AT Cs.Nott.AC.UK]

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.