The Wolf, Goat and Cabbage Exchange

Our last article introduced the notion of Machine Reasonable APIs and Regulations. Here, we give an example of such an API and regulation in the context of the FIX protocol. In order to demonstrate what we mean, we encode a fictional exchange which accepts FIX messages and analyse its functionality using the Imandra Protocol Language.

In our exchange, we want to be able to trade with three objects — a wolf, a cabbage and a goat. Initially, the exchange has all three. Let us assume it is a regulatory requirement that no client can be in ownership of all three objects.

The exchange implements a trading logic which attempts to provide functionality to trade in these objects while adhering to the regulatory requirement. In order to trade a client can

1. send a message asking to pick up or drop an object belonging to the client;
2. explicitly do nothing and wait for an action from the exchange;
3. send an object to the exchange.

The exchange performs fill actions, which can

1. pick up or drop an object belonging to the exchange;
2. explicitly do nothing and wait for another message;
3. send an object to the client.

The exchange explicitly forbids the following pairs of objects from existing alone either at the exchange when it is the client’s turn to send a message, or with a client when it is the exchange’s turn to send a message:

Wolf and Goat or Goat and Cabbage prohibited from being alone together

Note that it is valid for all three to exist together at the exchange. The exchange thinks that this constraint is enough to satisfy the regulatory requirement and has conducted some testing with hundreds of thousands of test cases, none of which break the regulatory requirement, which gives some confidence that the requirement will not be broken.

Let us now describe this venue using the Imandra Protocol Language (IPL). We begin by defining the types of messages that the exchange accepts and sends out. We are notionally importing the FIX 4.4 dictionary here, but we want to add our own special fields and associated enumeration types, which we can do using the custom functionality in IPL:

import FIX_4_4

@encoding: char
enum act {
    Pick        "p"
    Drop        "d"
    SwapTransit "s"
}

@encoding: char
enum obj {
    Cabbage     "c"
    Goat        "g"
    Wolf        "w"
}

extend message NewOrderSingle {
    obj        "2001" :? obj
    act        "2002" : act
}

extend message ExecutionReport {
    obj        "2001" :? obj
    act        "2002" : act
}

message NewOrderSingle {
	opt obj
	req act
} 

outbound message ExecutionReport {
	opt obj
	req act
}

What this means is that the exchange accepts a NewOrderSingle message with an optional field obj with given field tag “2001”, and a field act with given field tag “2002”. The exchange also sends out an ExecutionReport message with the same fields. The acceptable values are given by the associated enumeration types.

Now we have defined a message interface for the exchange we can consider adding some validation requirements, which dictate the acceptable behaviour of the fields of the incoming messages. In order to do this let us first introduce a new local enumeration type named location, and the notion of a state — a ubiquitous and canonical notion in any IPL model:

enum location {
   Exchange
   Client
   Transit
   Eaten
}
internal state {
   assignable{
      act : act
      obj :? obj
   }
   cabbage : location = Exchange;
   goat : location = Exchange;
   wolf : location = Exchange;
   transit : location = Client;
}

The state records the location of the objects, and where the objects can be picked up or dropped off — represented by the transit field.

We refer to messages as “events”. We can add a constrained event called an action, which we name fill that records any objects transferred from the exchange to the client. We can also add validation statements to events which ensure specified properties are true when receiving an event. These validation statements ensure that should an object be eaten an event is not accepted, and that should the event be to simply move the transit element then there should be no object contained therein. We also ensure that the transit element is at the correct location to pick or drop at the client.

action fill {
   obj :?obj
   act : act
   validate{!state.cabbage == Eaten && !state.goat == Eaten}
   validate{this.act == SwapTransit <==> !present(this.obj)}
   validate{state.transit == Exchange}
}

Now we can write logic which acts upon the state when a message or an action is received:

receive (f:fill) {
 if (state.cabbage == Client  && state.goat == Client)  then 
 {
  state.cabbage = Eaten    
  return
 }
 if (state.goat    == Client  && state.wolf == Client)  then
 { 
  state.goat = Eaten
  return
 }

 state.act = f.act
 state.obj = f.obj

 if f.act == SwapTransit then state.transit = Client
 else if f.act == Pick then
 {
  if (state.cabbage == Transit || state.goat == Transit || state.wolf == Transit) then return

  let thisObjVal = if f.obj == (Some Cabbage) then state.cabbage 
    else if f.obj == (Some Wolf) then state.wolf else state.goat

   if thisObjVal == Exchange  then 
   {              
     if f.obj == (Some Cabbage) then state.cabbage = Transit else
     if f.obj == (Some Wolf)    then state.wolf    = Transit else
     state.goat  = Transit 
   }
 }
 else 
 {
   let thisObjVal = if f.obj == (Some Cabbage) then state.cabbage 
     else if f.obj == (Some Wolf) then state.wolf else state.goat

   if thisObjVal == Transit then 
   {                
     if f.obj == (Some Cabbage) then state.cabbage = Exchange
     else if f.obj == (Some Wolf)    then state.wolf    = Exchange 
     else state.goat    = Exchange 
   }
 }
 send ExecutionReport state
}

receive (m:NewOrderSingle){
 if (state.cabbage == Exchange && state.goat == Exchange) then 
  {
    state.cabbage = Eaten
    return
  }
  if (state.goat    == Exchange && state.wolf == Exchange) then 
  {
    state.goat = Eaten
    return
  }
  assignFrom(m,state)

  if m.act == SwapTransit then state.transit = Exchange
  else if m.act == Pick then
  {
    if (state.cabbage == Transit || state.goat == Transit || state.wolf == Transit) then return

    let thisObjVal = if m.obj == (Some Cabbage) then state.cabbage 
      else if m.obj == (Some Wolf) then state.wolf else state.goat

    if thisObjVal == Client then 
    {              
      if m.obj == (Some Cabbage)   then state.cabbage = Transit
      else if m.obj == (Some Wolf) then state.wolf    = Transit 
      else if m.obj == (Some Goat) then state.goat    = Transit
    }
  }
  else 
  {
    let thisObjVal = if m.obj == (Some Cabbage) then state.cabbage 
      else if m.obj == (Some Wolf) then state.wolf else state.goat

    if thisObjVal == Transit then 
    {                
      if m.obj == (Some Cabbage)   then state.cabbage = Client 
      else if m.obj == (Some Wolf) then state.wolf    = Client
      else state.goat    = Client
    }
  }
}

As this full model is machine reasonable we can now set about analysing the possible states. We can try to determine if the model satisfies the regulation by writing a verification goal. In this case, because this is a demonstration example, we tailor the verification goal to the problem, but in general verification goals can be automatically generated.

In IPL we can define the machine reasonable regulation, by writing for example:

validate {
 !(state.cabbage = Client &&
   state.goat    = Client &&
   state.wolf    = Client)
}

then use Imandra to verify whether this regulation holds. In this case, Imandra quickly discovers that the regulation is broken giving back an example FIX log of NewOrderSingle and ExecutionReport messages:

This log can be validated by pasting the contents here for example, and corresponds to the following sequence of messages and actions:

The regulatory requirement of this problem — that no client should be in the possession of all three objects — is only broken at message sequence lengths of 18 or greater. The number of possible paths that can be found with message sequences of length 18 is 3,200,668. The total number of paths at less than or equal to 18 is 5,816,112. Out of all of these possible sequences of events, there are only 2 sequences which break the regulatory requirement.

Even with a bounded message sequence length for testing, and tens of thousands of tests, the probability that one of the 2 sequences is found via classical testing techniques is extremely low. This is why formal analysis of the model is so vital. Imandra can not only find the sequence where the regulatory requirement is broken but can also perform a region decomposition which provides a static analysis of all the feasible paths through the model. For example below is a graph showing the distinct paths through the model sufficient to cover all possible scenarios in this model — please click on the image to see the full decomposition graph.

This decomposition of the state-space is automatically produced by Imandra, and produces a set of possible regions which we can explore and use both in formal verification and in the automatic creation of high-coverage test suites. Below is an image of the generated interactive region explorer — soon publicly available for browsing!

We’re very excited to bring the rigour of machine reasonable APIs and regulations to finance, significantly upping the game when it comes to algorithm governance and transparency.

Join us at www.imandra.ai to learn more!