|
|NET
|
|
|
|
|
|SPECIFICATION DAWN_Specification
|
|
|Signature
|
|
|include "pair";
|
|
|sort AGENT;
|
|
|#sort U;
|
|
|function initU: gives MS<AGENT>;
|
|
|function initM: AGENT, AGENT gives PAIR<AGENT,AGENT>;
|
|
|function M: AGENT gives MS<PAIR<AGENT,AGENT>>;
|
|
|function N: AGENT gives MS<PAIR<AGENT,AGENT>>;
|
|
|function U: gives MS<AGENT>;
|
|
|
|
|
|
|
|
;
|
|
|Axioms
|
|
|agents: forall x: inMS(x,U());
|
|
|UisSET: isSET(U());
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
;
|
|
|Variables
|
|
|var x as AGENT;
|
|
|var y as AGENT;
|
|
|
|
|
;
|
|
|Model
|
|
|AGENT = enumerate {'a','b','c'};
|
|
|#U = enumerate{'a','b','c'};
|
|
|function M: c as AGENT gives MS<PAIR<AGENT,AGENT>>
|
|
|begin
|
|
| var n as AGENT;
|
|
| var m as MS<PAIR<AGENT,AGENT>>;
|
|
| foreach n in AGENT do
|
|
| m[(c,n)] = 1;
|
|
| od
|
|
| return m;
|
|
| end
|
|
|
|
|
|function initU: u as AGENT gives AGENT
|
|
|begin
|
|
| #var u as AGENT;
|
|
| #var v as SET<AGENT>;
|
|
| #foreach u in AGENT do
|
|
| # v[u] = 1;
|
|
| #od
|
|
| #return v;
|
|
| return u;
|
|
| end
|
|
|
|
|
|function initM: q as AGENT, w as AGENT gives PAIR<AGENT, AGENT>
|
|
|begin
|
|
| #var q as AGENT;
|
|
|# var w as AGENT;
|
|
| #var t as PAIR<AGENT,AGENT>;
|
|
| #foreach q in AGENT do
|
|
| # foreach w in AGENT do
|
|
| # t[(q,w)] = 1;
|
|
| # od
|
|
| #od
|
|
| #return t;
|
|
| return pair(q,w);
|
|
|end
|
|
|
|
|
|function N: o as AGENT gives MS<PAIR<AGENT, AGENT>>
|
|
| begin
|
|
| var p as AGENT;
|
|
| var d as MS<PAIR<AGENT,AGENT>>;
|
|
| foreach p in AGENT do
|
|
| d[(p,o)] = 1;
|
|
| od
|
|
| return d;
|
|
| end
|
|
|
|
|
|function U: gives MS<AGENT>
|
|
|begin
|
|
| var v as AGENT;
|
|
| var res as MS<AGENT>;
|
|
| foreach v in AGENT do
|
|
| res[v] = 1;
|
|
| od
|
|
| return res;
|
|
|end
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
;
|
|
|PLACES
|
|
|negotiating 2
|
|
|Sort
|
|
|AGENT
|
|
;
|
|
;
|
|
|agreed 3
|
|
|Sort
|
|
|AGENT
|
|
;
|
|
;
|
|
|envelopes 4
|
|
|Sort
|
|
|PAIR<AGENT, AGENT>
|
|
;
|
|
;
|
|
|mailbox 5
|
|
|Sort
|
|
|PAIR<AGENT, AGENT>
|
|
;
|
|
;
|
|
;
|
|
|TRANSITIONS
|
|
|t2 6
|
|
;
|
|
|t3 7
|
|
;
|
|
|t4 8
|
|
;
|
|
|t1 17
|
|
;
|
|
;
|
|
|ARCS
|
|
|2 --> 8 9
|
|
|inj(x)
|
|
;
|
|
;
|
|
|8 --> 3 10
|
|
|inj(x)
|
|
;
|
|
;
|
|
|3 --> 7 11
|
|
|inj(x)
|
|
;
|
|
;
|
|
|7 --> 2 12
|
|
|inj(x)
|
|
;
|
|
;
|
|
|5 --> 7 13
|
|
|inj(pair(x,y))
|
|
;
|
|
;
|
|
|7 --> 4 14
|
|
|inj(pair(y,x))
|
|
;
|
|
;
|
|
|5 --> 6 15
|
|
|inj(pair(x,y))
|
|
;
|
|
;
|
|
|6 --> 4 16
|
|
|inj(pair(y,x))
|
|
;
|
|
;
|
|
|4 --> 17 18
|
|
|inj(pair(x,y))
|
|
;
|
|
;
|
|
|17 --> 5 19
|
|
|inj(pair(y,x))
|
|
;
|
|
;
|
|
|2 --> 17 20
|
|
|inj(x)
|
|
;
|
|
;
|
|
|17 --> 2 21
|
|
|inj(x)
|
|
;
|
|
;
|
|
|2 --> 6 22
|
|
|inj(x)
|
|
;
|
|
;
|
|
|6 --> 2 23
|
|
|inj(x)
|
|
;
|
|
;
|
|
|8 --> 4 24
|
|
|cross(inj(x),U())
|
|
;
|
|
;
|
|
|4 --> 8 25
|
|
|cross(inj(x),U())
|
|
;
|
|
;
|
|
;
|
|
|MARKING
|
|
|2
|
|
|U()
|
|
;
|
|
|4
|
|
|cross(U(),U())
|
|
;
|
|
;
|
|
|NET_END
|
|
EDITOR_INFOS
|
|
PAGES
|
|
1 518x518+564+258 1
|
|
;
|
|
PLACE
|
|
3 :
|
|
1 417.0 248.0
|
|
{'Sort': (-30, -13, 1)}
|
|
.
|
|
4 :
|
|
1 239.0 174.0
|
|
{'Initial Marking': (3, 0, 0), 'Sort': (-74, -12, 1)}
|
|
.
|
|
2 :
|
|
1 68.0 242.0
|
|
{'Initial Marking': (1, 0, 0), 'Sort': (15, -19, 1)}
|
|
.
|
|
5 :
|
|
1 239.0 322.0
|
|
{'Sort': (84, 1, 1)}
|
|
.
|
|
;
|
|
TRANSITION
|
|
6 :
|
|
1 152.0 243.0
|
|
.
|
|
7 :
|
|
1 332.0 248.0
|
|
.
|
|
8 :
|
|
1 239.0 77.0
|
|
.
|
|
17 :
|
|
1 239.0 250.0
|
|
.
|
|
;
|
|
ARC
|
|
9 :
|
|
1 0 0 SMOOTH POINT 83.5 81.0
|
|
{}
|
|
.
|
|
12 :
|
|
1 0 0 SMOOTH POINT 332.0 367.125 332.0 366.25 167.0 368.5 80.5 317.75
|
|
{}
|
|
.
|
|
10 :
|
|
1 0 0 SMOOTH POINT 392.0 82.0
|
|
{}
|
|
.
|
|
13 :
|
|
1 0 0
|
|
{}
|
|
.
|
|
16 :
|
|
1 0 0
|
|
{}
|
|
.
|
|
19 :
|
|
1 0 0
|
|
{}
|
|
.
|
|
22 :
|
|
1 0 0 SMOOTH POINT 109.0 228.5
|
|
{}
|
|
.
|
|
25 :
|
|
1 0 0 SMOOTH POINT 209.0 110.5
|
|
{}
|
|
.
|
|
15 :
|
|
1 0 0
|
|
{}
|
|
.
|
|
18 :
|
|
1 0 0
|
|
{}
|
|
.
|
|
21 :
|
|
1 0 0 SMOOTH POINT 149.5 319.0
|
|
{}
|
|
.
|
|
24 :
|
|
1 0 0 SMOOTH POINT 261.0 146.5
|
|
{}
|
|
.
|
|
11 :
|
|
1 0 0
|
|
{}
|
|
.
|
|
14 :
|
|
1 0 0
|
|
{}
|
|
.
|
|
20 :
|
|
1 0 0 SMOOTH POINT 154.5 192.0
|
|
{}
|
|
.
|
|
23 :
|
|
1 0 0 SMOOTH POINT 111.0 257.5
|
|
{}
|
|
.
|
|
;
|
|
END_EDITOR
|