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:
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
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:
Here Imandra will examine the logic and produce regions for all valid messages or actions that could logically take the place of the wildcard.
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
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.
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.
We can also constrain the expanded values using
This will produce a region for each of the OrdType values
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:
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:
This will create a region tagged
big and a region tagged
big region’s constraints will state that the OrderQty has to be
> 100, and the
small region will be constrained to