-
Notifications
You must be signed in to change notification settings - Fork 13
ModelDefs
Kerem Ispirli edited this page Jul 14, 2017
·
1 revision
Model Definitions¶
Syntax¶
modelDef | "MODELDEF" modelName "::=" "CHAN" "IN" neChannelNameList? "CHAN" "OUT" neChannelNameList? "BEHAVIOUR" [processBehaviour](ProcessBehaviour) "ENDDEF" |
neChannelNameList | channelName ("," channelName)* |
modelName | [CapsId](CapsId) |
channelName | [CapsId](CapsId) |
Semantics¶
Define a model, with its input and output channels for external communication, and the definition of its behaviour. Input and output channels shall be defined in a channel definition CHANDEF.
Examples¶
The following model synchronizes using the Synchronized Operator || a specification with a sequence.
MODELDEF Model ::= CHAN IN A, B CHAN OUT C, D BEHAVIOUR specification[A,B,C,D](Nil) || sequence[A,B,C,D]() ENDDEF