Imandra’s
Region Decomposition
Region Decomposition is a feature of Imandra inspired by Cylindrical Algebraic Decomposition (CAD) but lifted for algorithms at large. With Region Decomposition, Imandra can take a function (or a model) written in the "pure" subset of OCaml (or ReasonML) and describe its behavior with a finite number of regions of its state-space.
Each such region of the state-space contains:
● A set of symbolic constraints on the inputs
● A symbolic invariant describing expected output
Imandra can further synthesize concrete inputs into the model satisfying a particular region - these instances will then be printed as driving scenario descriptions (e.g., CARLA's Python Strategy Interface).
State-space Regions
of “Digital Twin” Models
state machine encoding particular geography (with physics, etc.), each region of its state-space represents a distinct symbolic driving scenario.
Generating Test Cases
Imandra is a cloud-native automated reasoning engine allowing you to:
• Encode "digital twin" models using OCaml or ReasonML
• Decompose their state-spaces to create quantitative coverage metrics (symbolic driving scenarios)
• Synthesize and print (in whatever format is best suited for your simulation environment) concrete driving scenarios
Quantifying Testing Coverage
You can actually map the driving data into regions to understand what subset of the state-space has been covered.
State Explorer
The following regions were decomposed from the simple intersection model.
Select a region below for details
- Steady
- Braking
- Accelerating
Velocity
- Green
- Yellow
- Red
- Yellow&Red
Lights
- Will pass
- Won't pass
Passing
Region Name
Constraints
Invariant