-
Notifications
You must be signed in to change notification settings - Fork 13
CnectDefs
pjljvandelaar edited this page Jun 4, 2018
·
3 revisions
Connection Definitions¶
Syntax¶
cnectDefs | "CNECTDEF" cnectDef (";" cnectDef )* "ENDDEF" |
cnectDef | cnectName "::=" cnectType cnectItem* |
cnectType | "CLIENTSOCK" | "SERVERSOCK" |
cnectItem | "CHAN" "OUT" channelName "HOST" hostName "PORT" portNumber | "CHAN" "IN" channelName "HOST" hostName "PORT" portNumber | "ENCODE" channelName "?" [varDecl](VarDecl) "->" "!" [valExpr](ValExpr) | "DECODE" channelName "!" [valExpr](ValExpr) "<-" "?" [varDecl](VarDecl) |
cnectName | [CapsId](CapsId) |
channelName | [CapsId](CapsId) |
hostName | [String](Data_Type) |
portNumber | [Int](Data_Type) |
Semantics¶
Define connections with outside world, and the mapping from abstract TorXakis channels to the concrete outside-world connections. Currently, only socket connections (of type String) are supported. A socket has a hostname, such as "localhost", and a portNumber.
Examples¶
The statement
CNECTDEF Sut ::= CLIENTSOCK CHAN OUT Action HOST "localhost" PORT 7890 ENCODE Action ? opn -> ! toString(opn) CHAN IN Result :: HOST "localhost" PORT 7890 DECODE Result ! fromString(s) <- ? s ENDDEF
specifies a socket connection, called Sut
, to the outside world where
- TorXakis is the client side;
- there is one outgoing and one incoming channel,
Action
andResult
, respectively; - the types of messages communicated on channels
Action
andResult
can be found in the corresponding channel definition CHANDEF; - the predefined function
toString
is used to map a message of channelAction
to a string for the socket (localhost,7890); - the predefined function
fromString
is used to map a string from socket (localhost,7890) to a message on channelResult
; - both channels the outside world are accessed via one socket on the same machine, i.e., localhost on portNumber 7890; one channel is
IN
and one isOUT
.
Note that -
OUT
andIN
are viewed from the point of view of TorXakis, i.e., if this CNECTDEF specifies the connection to the system under test (SUT) thenOUT
is the input for the SUT, andIN
is the output of the SUT; - each channel must map uniquely (bijectively) to a triple (
IN
/OUT
,hostName,portNumber).
The statement
CNECTDEF Sim ::= SERVERSOCK CHAN IN Action :: Operation HOST "localhost" PORT 7890 DECODE Action ! fromString(s) <- ? s CHAN OUT Result :: Int HOST "localhost" PORT 7890 ENCODE Result ? result -> ! toString(result) ENDDEF
specifies a socket connection, called Sim
, to the outside world, where
- TorXakis is the server side;
- there is one incoming and one outgoing channel,
Action
andResult
, respectively; - the channel mappings are the inverse of the previous connection definition, implying that this connection can be used for a simulator simulating the same model as used above for testing.
- Socket streams must have UTF-8 string encoding, without byte order mark.
- The new line format must be Linux (\n). When using the Windows style (\r\n) the \r is considered part of the output string.