murphismv/MOESI.m at master · lyj238/murphismv · GitHub

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
const num_clients: 3;

type client : 1..num_clients;
    locationType: enum{ M, OSTATUS, E, S, I};

var a : array[client] of locationType;

ruleset i : client do
rule "rule_t1"
    a[i] = E ==>
begin
    a[i] := M;
endrule;

rule "rule_t2"
    a[i] = I ==>
begin
    for j: client do
    if (j = i) then a[j] := S;
    elsif (a[j] = E) then a[j] := S;
    elsif (a[j] = M) then a[j] := OSTATUS;
    else a[j] := a[j];
    endif;
    endfor;
endrule;

rule "rul_t3"
    a[i] = S ==>
begin
    for j: client do
    if (j = i) then a[j] := E;
    else a[j] := I;
    endif;
    endfor;
endrule;

rule "rul_t4"
    a[i] = OSTATUS ==>
begin
    for j: client do
    if (j = i) then a[j] := E;
    else a[j] := I;
    endif;
    endfor;
endrule;

rule "rul_t5"
    a[i] = I ==>
begin
    for j: client do
    if (j = i) then a[j] := E;
    else a[j] := I;
    endif;
    endfor;
endrule;
endruleset;

startstate
begin
 for i: client do
    a[i] := I;
  endfor;
endstartstate;