Message Flows

MessageFlows

Message flows are used to guide Imandra’s analysis when decomposing your IPL model into its distinct regions of behavior - this can be done by submitting your model to the Imandra API - see API and Web Services.

The way to define a message flow in your IPL model is as follows:

messageFlows {
  NewOrderFill {
	  name "NewOrder Fill"
	  description "Send NewOrderSingle Message then receive a fill action"
	  template [NewOrderSingle, fill]
  }
}

The name and description here are optional and are used for documentation purposes - the name at the start of the messageflow block (e.g. NewOrderFill) is the unique ID for the messageFlow.

Imandra’s decomposition will then produce regions from the initial state of the model where a valid NewOrderSingle message was received, followed by a fill.

You can define multiple messageFlows in a single messageFlows block:

messageFlows {
  NewOrderFill {
	  name "NewOrder Fill"
	  description "Send NewOrderSingle message then receive a fill action"
	  template [NewOrderSingle, fill]
  }

  NewOrderCancel {
	  name "NewOrder Cancel"
	  description "Send NewOrderSingle message, then OrderCancelRequest, then receive a fill action"
	  template [NewOrderSingle, OrderCancelRequest, cancel]
  }
}

Wildcard events

If you’re not sure what messages and events may or may not be logically valid for the spec you’ve written, you can use the wildcard template event:

messageFlows {
  NewOrderWildcard {
	  name "NewOrder wildcard"
	  description "Send NewOrderSingle message then any possible message or action"
	  template [NewOrderSingle, _]
  }
}

Here Imandra will examine the logic and produce regions for all valid messages or actions that could logically take the place of the wildcard.

Attributes

By default Imandra will only produce regions for valid states of the model (i.e. regions where the validate statements in your model are true). If you’re interested in looking at rejection behavior for particular steps, you can use the @@includeInvalid or @@invalidOnly attributes:

messageFlows {
  NewOrderRejections {
	  name "NewOrder rejections"
	  description "Send NewOrderSingle messages that do not satisfy the model's validate statements"
	  template [NewOrderSingle @@invalidOnly]
  }

  NewOrderAll {
	  name "NewOrder all"
	  description "Send NewOrderSingle messages that are both valid and invalid"
	  template [NewOrderSingle @@includeInvalid]
  }
}

It is also possible to add a special @@minimalInvalid attribute to messageFlows which will produce a cases for each validation statement, where the validation statement in question fails, but all other validations are true. This can produce a lot of regions, but is useful for picking out specific failures which are required for testing.

messageFlows {
  NewOrderRejections {
	  name "NewOrder minimal rejections"
	  description "Send NewOrderSingle messages that minimally do not satisfy the model's validate statements"
	  template [NewOrderSingle @@minimalInvalid]
  }
}

Expanders

In some situations the logic of your model may not care about what value a particular field takes, but you may still wish to produce regions for the different possible values.

For example your model may not care about the OrderQty of a NewOrderSingle, but you may be producing test cases to run against the real implementation of your system, and you may know that a certain size of order triggers additional behaviors that you want to test.

messageFlows {
  NewOrderFill {
    name "NewOrderFill"
    description "Send NewOrderSingle message then receive a fill action"
    template [
      NewOrderSingle expanding { OrdType },
      fill
    ]
  }
}

Here we’re asking Imandra to expand the OrdType field and produce a region for each of the logically valid values of that field. Each of these regions can then be transformed into a test case we can run against our real system.

Constraining with `when`

We can also constrain the expanded values using when:

messageFlows {
  NewOrderFill {
    name "NewOrderFill"
    description "Send NewOrderSingle message then receive a fill action"
    template [
      NewOrderSingle expanding { OrdType when it in {|OrdType.Market, Limit, StopLimit|}},
      fill
    ]
  }
}

This will produce a region for each of the OrdType values Market, Limit, and StopLimit. Note that if the logic of the model dictates that one of these values is not allowed, a region will not be produced for that value.

Expanding on multiple fields

We can expand on multiple fields in a message in two ways:

enum a {
  a1
  a2
  a3
}

enum b {
  b1
  b2
  b3
}

action act {
  a : a
  b : b
}

receive (act: act) {
}

messageFlows {
  ExpandAdd {
    name "Expand additive"
    description "Send Act action with additive expansion on fields A and B"
    template [
      act expanding { a, b }
    ]
  }

  ExpandMul {
    name "Expand multiplicative"
    description "Send Act action with multiplicative expansion on fields A and B"
    template [
      act expanding { a } { b }
    ]
  }
}

ExpandAdd will produce one region for each of the unique values of a, and one region for each of the unique values of b treated separately.

ExpandMul will produce one region for each of the unique values of a, for each of the unique values of b.

We can see the difference in the IPL cases list:

Expanding using a function

We can also expand based on a function that we’ve defined:

import FIX_4_4

message NewOrderSingle {
  req OrderQtyData.OrderQty
}

enum bigAndSmall {
  big
  small
}

function bigAndSmallQty(m: NewOrderSingle) : bigAndSmall {
  return if m.OrderQtyData.OrderQty > 100.0 then big else small
}

messageFlows {
  NewOrderSizes {
    name "NewOrderSizes"
    description "Send NewOrderSingle message expanding big and small order quantity"
    template [
      NewOrderSingle expanding {fun bigAndSmallQty}
    ]
  }
}

This will create a region tagged big and a region tagged small:

The big region’s constraints will state that the OrderQty has to be > 100, and the small region will be constrained to <= 100.