-
Notifications
You must be signed in to change notification settings - Fork 1
/
P.4ml
160 lines (136 loc) · 9.91 KB
/
P.4ml
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
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
domain P extends PError, PData
{
}
domain PError extends PData
{
ERROR0 ::= (String).
ERROR1 ::= (Id, String).
ERROR2 ::= (Id, Id, String).
}
domain PData
{
PUnit ::= new (name: String).
PUnitContains ::= new (unitName: String, fileName: String).
DependsOn ::= new (thisUnitName: String, thatUnitName: String + { NIL }).
IdList ::= new (val: Integer + String, tl: any IdList + { NIL }).
Id ::= { NIL } + Integer + String + IdList.
Float ::= new (val: Real).
/*************************************************************/
/**************** Type Language ************/
/*************************************************************/
Qualifier ::= { NONE, MOVE, SWAP }.
StringList ::= new (hd: String, tl: any StringList + { NIL }).
IntegerList ::= new (hd: Integer, tl: any IntegerList + { NIL }).
EnumTypeDef ::= new (name: String, elems: any StringList, values: any IntegerList + { NIL }, id: any Id).
TypeDef ::= new (name: String, type: any TypeExpr + { NIL }, id: any Id).
NameType ::= new (name: String).
BaseType ::= new ({ NULL, BOOL, INT, FLOAT, STRING, ANY, EVENT, MACHINE}).
AnyType ::= new (perm: String + { NIL, DATA }).
AnyTypeDecl ::= new (perm: String, id: Id).
TupType ::= new (hd: any TypeExpr, tl: any TupType + { NIL }).
NmdTupType ::= new (hd: any NmdTupTypeField, tl: any NmdTupType + { NIL }).
SeqType ::= new (x: any TypeExpr).
SetType ::= new (x: any TypeExpr).
MapType ::= new (k: any TypeExpr, v: any TypeExpr).
NmdTupTypeField ::= new (name: any String, type: any TypeExpr).
InterfaceType ::= new (ev: any NonNullEventName, tail: any InterfaceType + { NIL }).
TypeExpr ::= NameType + BaseType + AnyType + TupType + NmdTupType + SeqType + SetType + MapType + InterfaceType.
/*************************************************************/
/**************** Action Language ************/
/*************************************************************/
//// Expressions
Name ::= new (name: String, id: any Id).
New ::= new (name: String, args: any Exprs + { NIL }, id: any Id).
FunApp ::= new (name: String, args: any Exprs + { NIL }, label: Natural, id: any Id).
NulApp ::= new (op: Integer + Boolean + Float + { THIS, NONDET, FAIRNONDET, NULL, HALT }, id: any Id).
UnApp ::= new (op: { NOT, NEG, KEYS, VALUES, SIZEOF }, arg1: any Expr, id: any Id).
BinApp ::= new (op: { ADD, SUB, MUL, DIV, AND, OR, EQ, NEQ, LT, LE, GT, GE, IDX, IN }, arg1: any Expr, arg2: any Expr, id: any Id).
Field ::= new (arg: any Expr, name: String + Natural, id: any Id).
Default ::= new (type: any TypeExpr, id: any Id).
Cast ::= new (arg: any Expr, type: any TypeExpr, id: any Id).
Convert ::= new (arg: any Expr, type: any TypeExpr, id: any Id).
Clone ::= new (arg: any Expr, id: any Id).
SetAcc ::= new (set: any Expr, idx: any Expr, id: any Id).
MapAcc ::= new (map: any Expr, idx: any Expr, id: any Id).
Choose ::= new (expr: any Expr, id: any Id).
Tuple ::= new (body: any Exprs, id: any Id).
NamedTuple ::= new (body: any NamedExprs, id: any Id).
Exprs ::= new (qual: Qualifier, head: any Expr, tail: any Exprs + { NIL }).
NamedExprs ::= new (field: String, exp: any Expr, tail: any NamedExprs + { NIL }).
Expr ::= Name + New + FunApp + NulApp + UnApp + BinApp + Field + Default + Cast + Convert + Tuple + NamedTuple + SetAcc + MapAcc + Clone + Choose.
ExprsExt ::= Expr + Exprs + NamedExprs.
//// Statements
NewStmt ::= new (name: String, args: any Exprs + { NIL }, aout: any Name + { NIL }, id: any Id).
Raise ::= new (ev: any Expr, args: any Exprs + { NIL }, id: any Id).
Send ::= new (dest: any Expr, ev: any Expr, args: any Exprs + { NIL }, id: any Id).
/* Announce ::= new (ev: any Expr, args: any Exprs + { NIL }, id: any Id). */
Announce ::= new (ev: any Expr, args: any Expr + { NIL }, id: any Id).
FunStmt ::= new (name: String, args: any Exprs + { NIL }, aout: any Name + { NIL }, label: Natural, id: any Id).
NulStmt ::= new (op: { SKIP, POP }, id: any Id).
BinStmt ::= new (op: { REMOVE, ASSIGN, INSERT }, arg1: any Expr + { NIL }, qual: Qualifier, arg2: any Expr, id: any Id).
InsertStmt ::= new (arg1: any Expr + { NIL }, index: any Expr, arg2: any Expr, id: any Id).
Return ::= new (expr: any Expr + { NIL }, id: any Id).
While ::= new (cond: any Expr, body: any Stmt, id: any Id).
Ite ::= new (cond: any Expr, true: any Stmt, false: any Stmt, id: any Id).
Seq ::= new (s1: any Stmt, s2: any Stmt, id: any Id).
Cases ::= new (trig: String + { NULL, HALT }, action: any AnonFunDecl, cases: any Cases + { NIL }, id: any Id).
Receive ::= new (cases: any Cases, label: Natural, id: any Id).
/* Assert ::= new (cond: any Expr, msg: String + { NIL }, id: any Id). */
Assert ::= new (cond: any Expr, msg: Expr + { NIL }, id: any Id).
Segments ::= new (formatArg: Natural, str: String, tl: any Segments + { NIL }).
Print ::= new (msg: String, segs: any Segments + { NIL }, args: any Exprs + { NIL }, id: any Id).
/* Goto ::= new (dst: any QualifiedName, args: any Exprs + { NIL }, id: any Id). */
Goto ::= new (dst: any QualifiedName, args: any Expr + { NIL }, id: any Id).
Break ::= new (id: any Id).
Continue ::= new (id: any Id).
Stmt ::= NewStmt + Raise + Send + Announce + FunStmt + NulStmt + BinStmt + Return + While + Ite + Seq + Receive + Assert + Print + Goto + Break + Continue.
/**************************************************************/
/*********** Module system declarations *******************/
/**************************************************************/
EventSetDecl ::= fun (name : String -> id: any Id).
EventSetContains ::= new (evset: any EventSetDecl, ev: NonNullEventName).
EventSet ::= fun (name: String -> list: any EventNameList + { NIL }).
InterfaceDef ::= fun (name: String -> evsetName: String + { ALL, NIL }, argType: any TypeExpr, id: any Id).
InterfaceDecl ::= new (name: String, evList: any InterfaceType + { ALL, NIL }, argType: any TypeExpr, id: any Id).
MachineReceives ::= new (mach: String, ev: NonNullEventName + { ALL }).
MachineSends ::= new (mach: String, ev: NonNullEventName + { ALL }).
/*************************************************************/
/**************** State Machine Declarations *************/
/*************************************************************/
EventDecl ::= new (name: String, card: any QueueConstraint, type: any TypeExpr + { NIL }, id: any Id).
MachineKind ::= fun (name: String -> kind: { REAL, SPEC }).
MachineCard ::= fun (name: String -> card: any QueueConstraint).
MachineStart ::= fun (name: String -> start: any QualifiedName).
MachineDecl ::= new (name: String, id: any Id).
MachineProtoDecl ::= fun (name: String -> constType: any TypeExpr).
ObservesDecl ::= new (spec: String, ev: NonNullEventName).
VarDecl ::= fun (name: String, owner: String -> type: any TypeExpr, id: any Id).
// For both FunDecl and AnonFunDecl, the order of locals in the input file is left to right
// and top to bottom (since multiple variable declaration lists are allowed).
// For FunDecl, the order of params is left to right.
// For AnonFunDecl, the order of envVars is left to right and top to bottom.
// Thus, the numbering of variables is consistent across nested scopes.
FunDecl ::= fun (name: String, owner: String + { NIL } -> params: any NmdTupType + { NIL }, return: any TypeExpr + { NIL }, locals: any NmdTupType + { NIL }, body: any Stmt + { NIL }, id: any Id).
FunProtoDecl ::= fun (name: String -> params: any NmdTupType + { NIL }, return: any TypeExpr + { NIL }).
GlobalFunCreates ::= new (name: String, m: String).
// envVars doesn't seem to be used in functions in the current P implementation, removing for now
// AnonFunDecl ::= new (owner: String + { NIL }, ownerFun: String + { NIL }, locals: any NmdTupType + { NIL }, body: any Stmt, envVars: any NmdTupType, id: any Id).
AnonFunDecl ::= new (owner: String + { NIL }, ownerFun: String + { NIL }, locals: any NmdTupType + { NIL }, body: any Stmt, id: any Id).
StateDecl ::= fun (name: any QualifiedName, owner: String -> entryAction: any AnonFunDecl + String, exitFun: any AnonFunDecl + String, temperature: { HOT, WARM, COLD }, id: any Id).
TransDecl ::= fun (src: StateDecl, trig: String + { NULL, HALT } -> dst: any QualifiedName, action: any { PUSH } + AnonFunDecl + String, id: any Id).
DoDecl ::= fun (src: StateDecl, trig: String + { NULL, HALT } -> action: any { DEFER, IGNORE } + AnonFunDecl + String, id: any Id).
PDecl ::= AnyTypeDecl + EventDecl + MachineDecl + VarDecl + AnonFunDecl + FunDecl + StateDecl + TransDecl + DoDecl + EventSetDecl + InterfaceDef + InterfaceDecl + MachineSends + MachineReceives + TypeDef + EnumTypeDef.
AssumeMaxInstances ::= new (bound: Natural).
AssertMaxInstances ::= new (bound: Natural).
QualifiedName ::= new (name: String, qualifier: any QualifiedName + { NIL }).
QueueConstraint ::= AssumeMaxInstances + AssertMaxInstances + { NIL }.
EventName ::= String + { NULL, HALT }.
EventNameList ::= new (hd: EventName, tl: any EventNameList + { NIL }).
NonNullEventName ::= String + { HALT }.
/*************************************************************/
/**************** Annotations *************/
/*************************************************************/
Annotation ::= new (ant: Annotatable, key: String, value: any AnnotValue, id: any Id).
Annotatable ::= EventDecl + MachineDecl + VarDecl + FunDecl + FunProtoDecl + StateDecl + TransDecl + DoDecl + { NIL }.
AnnotValue ::= Integer + String + Boolean + { NULL }.
}