Expressions
Expressions define how values can be constructed in the logic of IPL. In this section we describe the general framework of constructing expressions, and show how to reason about them and where this is possible within an IPL model.
Values
We can create values of a certain type, or we can declare a local variable and assign a value to it and it then automatically becomes of this type. For concrete values refer to the examples of literals given in the Basic Types section. Recall for example we can create concrete initial values for fields within the state:
For concrete values of compound types, the name of the type is given with literals corresponding to each of the argument types in brackets. For example the time 8 a.m. can be given as UTCTimeOnly (8, 0, 0, None)
- the None
in this case is an example of a missing option case - this is discussed further in the section on Optional Types.
For enumeration types it is possible to use only the value provided by the enum. For example with the Side
enumeration type one can construct the simple value SellShort
. In the case where the names of enumeration cases clash, a typing error may occur in IPL. For example, the Buy
entry also appears in the AdvSide
enumeration type. In this case the name must be Qualified by writing Side.Buy
to denote that this value belongs to the Side
enumeration type.
Set Literals can be expressed using the []
notation - for example
Fresh values
A keyword in IPL is fresh()
which implicitly creates a new value for a particular field, but not one whose precise value we need to know about. A classic example is the ExecID
of a sent acknowledgement may need to be generated, but the precise value is not of logical importance, purely that has not appeared before in the model.
Operators
For manipulation with numeric values and variables IPL provides one with the standard arithmetic operations +
, -
(both binary and unary), *
and /
together with the comparison operators >
, <
, >=
and <=
. The equality operator ==
and its negation !=
are used to compare values of the same kind. For the Boolean algebra there are &&
, ||
operators, unary negation !
and, useful in certain circumstances, an implication operator ==>
and an equivalence operator <==>
.
The if-then-else construction can be used as a ternary operator to make an inline conditional expression. The condition, and both conditional branches must be expressions too.
Lastly, one can use a list inclusion in
operator to check whether a certain value is present in a list
Arithmetic operations
The operators +
, -
, *
and /
apply to any number type - in our case float
and int
. Furthermore, >
, <
, >=
and <=
apply in general to any comparable. A comparable type is either an int
or a float
or a compound datatype with purely number or optional number types. For example one can compare two variables of type UTCTimeOnly(int,int,int,?int)
:
Further to this, as a special operation it is possible to add elements of type Duration
to the type UTCTimeStamp
:
More such operators are forthcoming in IPL.
Referencing Fields
In order to reference fields in the model, IPL uses a Qualified Name convention. For the purposes of this section we demonstrate this using the state, but it applies equally to actions and messages - this is discussed further in the section on Messages and Actions.
When referencing the value of a field such as the Limit
field of the state we write state.Limit
. To reference an internal record field such as the opening_time
field of the venue_times
record we write state.venue_times.opening_time
.
Optional Cases
Recall from the Optional Types section, that optional types are used within IPL to represent information which may not be present. Let us say we are reasoning with the Limit
field from the state defined in the section on Defining State:
In order to reason about Limit
we need to be able to determine if it is present or not, and if so, make use of its value. IPL includes a special keyword present
which can be used as follows
which returns an expression value 1.0
if it is present.
If the value of Limit
is not present, then its value is by definition the literal None
. If it is present then it contains its value within the constructor Some
. We can extract this value by using a case
statment as follows:
which returns a boolean expression of equating to true
if and only if the Limit
field of state if present and its values is greater than 0.0
. The variable x
is referred to as the capture variable which stores the value in the Limit
. The None
and Some
clauses in this style of case expression must both be present but can be in any order.
This version of the case
operator exists within expressions and is functional in style. This means it is used in expressions only and both the branches must be present and contain an expression of the same type. This is comparison to the imperative style case statement shown in Imperative Code Blocks where it is not necessary for each branch to be present and each branch contains imperative code rather than expressions, as is the case for functional cases shown in this section.
Imperative Code Blocks
When receiving messages or actions, as described in the section on Messages and Actions it is possible to write imperative style code to describe the desired logic. In general code blocks exist within {}
brackets - within code blocks the following code constructs are available:
return
This simply exits whatever function the statement lies within
if-then-else
These have optional else
statements. If there is just one statement after the then
or else
then there is no need for {}
; otherwise this is necessary. Note that if-then-else
is valid in both Expressions and statement. The following are all valid examples of if-then-else
statements:
case
This allows imperative reasoning about case statements. This is in contrast to the functional style case statements used for example in validations described in the Optional Cases.
It is possible to exclude either the None
case or the Some
case, but if both are included, the None
case must come first. The following are valid examples of imperative case statements:
let
It is possible to define local variables in code blocks. These variables remain within scope of their respective block and are overridden by variable names with the same name in more nested blocks or case statements. Case capture variables such as x
above act as local variables in this sense. Types of local variables are not defined and are inferred from their assignment. A local variable must be assigned a value. Valid examples of local variable declarations are
assignFrom
This allows all of the fields from the state to be assigned to the fields of an incoming message. We introduced the concept of assignable in the State section. These fields correspond to those in messages, and assignFrom(msg, state)
assigns the intersection of the fields in the message msg
with those from the internal declaration state
.
send
It is possible to send an outbound message, as described in the Messages section, it is possible to use the send
statement to denote this being send from the venue. It is possible to send the outbound message with all fields explicitly set, or by incorporating the assignable section of an internal state declaration. All of the required fields of an outbound message must be assigned in a send
. For example, given an outbound message ExecutionReport
which has fields CumQty: float
and LeavesQty: float
the following are all valid send statements:
If any required fields are missing from the sent outbound message an error will be raised in IPL.