Region Decomposition

The term Region Decomposition refers to a (geometrically inspired) "slicing" of an algorithm’s state-space into distinct regions where the behavior of the algorithm is invariant, i.e., where it behaves "the same."

Each "slice" or region of the state-space describes a family of inputs and the output of the algorithm upon them, both of which may be symbolic and represent (potentially infinitely) many concrete instances.

The entrypoint to decomposition is the Modular_decomp.top function, here's a quick basic example of how it can be used:

In [1]:
let f x =
  if x > 0 then
    1
  else
    -1
;;

let d = Modular_decomp.top "f" [@@program]
Out[1]:
val f : int -> int = <fun>
val d : Top_result.modular_decomposition =
  {Imandra_interactive.Modular_decomp.MD.md_session = 1i;
   md_f =
    {Imandra_surface.Uid.name = "f"; id = <abstr>; special_tag = <abstr>;
     namespace = <abstr>;
     chash = Some PJgo2DFsoBguzbl73toT4qEHddvTtETrZBGCibHbAsE;
     depth = (3i, 1i)};
   md_args = [(x : int)]; md_regions = <abstr>}
Regions details

No group selected.

  • Concrete regions are numbered
  • Unnumbered regions are groups whose children share a particular constraint
  • Click on a region to view its details
  • Double click on a region to zoom in on it
  • Shift+double click to zoom out
  • Hit escape to reset back to the top
decomp of (f x
Reg_idConstraintsInvariant
1
  • not (x > 0)
-1
0
  • x > 0
1

Imandra decomposed the function "f" into 2 regions: the first region tells us that whenever the input argument x is less than or equal to 0, then the value returned by the function will be -1, the second region tells us that whenever x is positive, the output will be 1.

When using Region Decomposition from a REPL instead of from the jupyter notebook, we recommend installing the vornoi printer (producing the above diagram) via the Imandra_voronoi.Voronoi.print printer

Advanced Usage