State

An IPL model can define an set of global internal declarations which constitute the state of the model. Typically, we just define one state internal declaration, and use this to reason. The resulting IPL model then represents a state transition system which allows us to reason using Imandra.

Defining State

Declaration of the state is done by defining internal variables:

internal NAME {
 FIELD_NAME : [OPTIONAL] FIELD_TYPE [= INITIAL_VALUE;]
 ...
 ...
}

Here it is not necessary to define a field as optional, or to give an initial value. It is important to note that should an initial value not be given, a candidate is generated internally to calculate the initial state when analysing the model as state machine. This may provide unexpected results, so it is advised to give initial values where applicable.

In a typical use case, we would want to store the order, cumulative and leaves quantities, and the average executed price thus far, the side of an order (typically buy or sell), and the limit price, if present:

internal state {
 OrdQty      : Qty
 LeavesQty   : Qty
 CumQty      : Qty = 0.0;
 Side        : Side
 AvgPx       : Price
 Limit       :? Price 
}

In this case we explicitly initialise the CumQty field with the value 0.0.

One can define records in the internal state also, and give initial values. For example a user may wish to record the opening and closing times of the venue as a record:

record venue_times {
    opening_time : UTCTimeOnly 
    closing_time : UTCTimeOnly 
}

In order to import this into the state with initial values we extend our state by writing:

internal state {
 OrdQty      : Qty
 LeavesQty   : Qty
 CumQty      : Qty = 0.0;
 Side        : Side
 AvgPx       : Price
 Limit       :? Price 
 venue_times : venue_times = 
    {
    opening_time = UTCTimeOnly (8, 0, 0, None);
    closing_time = UTCTimeOnly (16, 0, 0, None);
    };
}

The meaning of UTCTimeOnly (8, 0, 0, None) is explained in greater detail in the Expressions.

Assignable Fields

Messages, both inbound and outgoing, contain many fields that can be saved into the state variable or, the opposite, set from the values of the state. To make this more straightforward, we have introduced the concept of assignable fields that may be automatically assigned from a message or assigned to an outbound message.

Let’s modify slightly the internal state definition from above by attributing four assignable fields. We’ll revisit this example when we come to discuss receiving and rejecting messages in the messages section, but for now let us assume that the optionality of each field in the assignable section of the state is shared between every message. We can then write :

internal state {
 assignable {
  OrdQty      : Qty 
  LeavesQty   : Qty 
  CumQty      : Qty = 0.0;
  Side        : Side 
 }
 Limit   :? Price 
 AvgPx   : Price 
 venue_times : venue_times = 
    {
    opening_time = UTCTimeOnly (8, 0, 0, None);
    closing_time = UTCTimeOnly (16, 0, 0, None);
    };
}

Now the fields in the assignable section are marked specifically to correspond to fields which will be sent or received from messages in the model. When sending a message one can, for example, write

send ExecutionReport { state with 
 ...
}

which automatically assigns the values of any fields in the outgoing ExecutionReport message, with the values from state. Equally it is possible to assign to the state from an incoming message. For example in the following excerpt, any fields from the state coinciding between those in the incoming NewOrderSingle message are automatically assigned to the values of the respective field in the message.

 assignFrom ( msg, state )

It is possible for the optionality of fields to differ and for them still to form part of the assignable section of state. We refer to this as ambiguous optionality and such fields are defined in the state using the :* notation in the field declaration. For example if the Side field was optional in the ExecutionReport, but required in the NewOrderSingle message the state would be defined as

internal state {
 assignable {
  OrdQty      : Qty 
  LeavesQty   : Qty 
  CumQty      : Qty = 0.0;
  Side        :* Side 
 }
 Limit   :? Price 
 AvgPx   : Price
 venue_times : venue_times = 
    {
    opening_time = UTCTimeOnly (8, 0, 0, None);
    closing_time = UTCTimeOnly (16, 0, 0, None);
    };
}

We will revisit this concept in the section of Messages and Actions.