Advanced Features

This tutorial covers advanced IPL behavior in larger models.

Ambiguous optionality

When a field is optional in one message and required in another, use :* in state:

internal state {
  assignable{
    ExecInst :* ExecInst
  }
}

For such fields, optional imports generally need defaults:

message NewOrderSingle {
  opt ExecInst default = Some Held
}

Verification packs

You can enable built-in verification goals:

VerificationPacks[EmptyString,Venue]

• EmptyString checks outbound string values are not empty.
• Venue checks OrdStatus transitions are valid.

This page builds on the complete model from previous tutorials with actions, custom fields/cases, and repeating groups.