-
Notifications
You must be signed in to change notification settings - Fork 0
/
msg.maude
84 lines (72 loc) · 3.19 KB
/
msg.maude
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
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
set include BOOL off .
load actor.maude
fmod MSG is protecting ACTOR .
--- ########## SORTS ##########
sorts Msg NeMsgList MsgList MsgType .
--- ########## SUBSORTS ##########
subsort Msg < NeMsgList < MsgList .
--- ########## OPS ##########
--- op mtMsg : -> Msg [ctor] .
op mtMsgList : -> MsgList [ctor] .
--- Message Types
op App : -> MsgType . --- app message
op ReleaseReq : -> MsgType . --- created by app messages to trigger update info
op ReleaseRecv : -> MsgType . --- sent by updateInfo telling other actors they can release
op AckRelease : -> MsgType . --- sent by actors receiving ack release to empty data structures
--- Messages
--- The three types are App, Req_Release, and Ack_Release.
--- I guess there should be another kind of message for asking an actor to take a snapshot?
--- An App message can do any combination of the following things all at once
--- - Add all references in the message to the target actor’s state; AND
--- - Create new App messages, each of which may contain a set of new references; AND
--- - Spawn new actors; AND
--- - Create new Req_Release messages.
--- TODO: This means that we need newActor to handle cases where ActorList is MT
--- MsgType, the destination of the msg, origin of the message, the sn, snapid, and a reference list
op @_:: dst _:: ori _:: sn _ :: sid _ :: r _@ : MsgType iNat iNat iNat iNat ReferenceList -> Msg [ctor] .
op _$_ : MsgList MsgList -> MsgList [ctor assoc id: mtMsgList] .
op _$_ : NeMsgList MsgList -> MsgList [ctor ditto] .
op _$_ : MsgList NeMsgList -> MsgList [ctor ditto] .
--- returns tt if both msgTypes provided are the same ff otherwise
op _~MsgType_ : MsgType MsgType -> Pred [comm] .
op lenML(_) : MsgList -> iNat .
--- This checks that a destination N occurs in a specific reference in the provided
--- reference list
--- X :: A -> B, B = tt, X :: A -> B, A = ff
op checkDestMsgApp(_,_) : ReferenceList iNat -> Pred .
--- ########## VARS ##########
vars A B C D : iNat .
vars RefA : Reference .
vars RefLiA : ReferenceList .
vars MsgA : Msg .
vars MsgTA MsgTB : MsgType .
vars MsgLiA : MsgList .
--- ########## EQS ##########
eq App ~MsgType App = tt .
eq ReleaseReq ~MsgType ReleaseReq = tt .
eq AckRelease ~MsgType AckRelease = tt .
eq ReleaseRecv ~MsgType ReleaseRecv = tt .
eq MsgTA ~MsgType MsgTB = ff [owise] .
eq checkDestMsgApp(mtRefList, B) = ff .
eq checkDestMsgApp(((A :: B -> C), RefLiA), D) =
(C ~iN D) or checkDestMsgApp(RefLiA, D) .
eq lenML(mtMsgList) = 0 .
eq lenML(MsgA $ MsgLiA) = s lenML(MsgLiA) .
endfm
--- --- ff
--- red checkDestMsgApp(mtRefList, 0) .
--- --- tt
--- red checkDestMsgApp(((0 :: 0 -> 0), (s 0 :: s 0 -> s 0), (s s 0 :: s s 0 -> s s 0)), 0) .
--- --- tt
--- red checkDestMsgApp(((0 :: 0 -> 0), (s 0 :: s 0 -> s 0), (s s 0 :: s s 0 -> s s 0)), s 0) .
--- --- tt
--- red checkDestMsgApp(((0 :: 0 -> 0), (s 0 :: s 0 -> s 0), (s s 0 :: s s 0 -> s s 0)), s s 0) .
--- --- ff
--- red checkDestMsgApp(((0 :: 0 -> 0), (s 0 :: s 0 -> s 0), (s s 0 :: s s 0 -> s s 0)), s s s 0) .
--- --- tt
--- red App ~MsgType App .
--- red ReleaseReq ~MsgType ReleaseReq .
--- red AckRelease ~MsgType AckRelease .
--- --- ff
--- red App ~MsgType ReleaseReq .
--- red ReleaseReq ~MsgType App .