# Module Splitting::SuccSplits

Provides a predicate for the successor relation with split information,
as well as logic used to construct the type `TSplits`

representing sets
of splits. Only sets of splits that can be reached are constructed, hence
the predicates are mutually recursive.

For the successor relation

```
succSplits(ControlFlowElement pred, Splits predSplits, ControlFlowElement succ, Splits succSplits, Completion c)
```

the following invariants are maintained:

`pred`

is reachable with split set`predSplits`

.- For all
`split`

in`predSplits`

:- If
`split.hasSuccessor(pred, succ, c)`

then`split`

in`succSplits`

.

- If
- For all
`split`

in`predSplits`

:- If
`split.hasExit(pred, succ, c)`

then`split`

not in`succSplits`

.

- If
- For all
`split`

not in`predSplits`

:- If
`split.hasEntry(pred, succ, c)`

then`split`

in`succSplits`

.

- If
- For all
`split`

in`succSplits`

:`split.hasSuccessor(pred, succ, c)`

and`split`

in`predSplits`

, or`split.hasEntry(pred, succ, c)`

and`split`

not in`predSplits`

.

The algorithm divides into four cases:

- The set of splits for the successor is the same as the set of splits
for the predecessor:
a) The successor is in the same
`SameSplitsBlock`

as the predecessor. b) The successor is*not*in the same`SameSplitsBlock`

as the predecessor. - The set of splits for the successor is different from the set of splits
for the predecessor:
a) The set of splits for the successor is
*maybe*non-empty. b) The set of splits for the successor is*always*empty.

Only case 2a may introduce new sets of splits, so only predicates from
this case are used in the definition of `TSplits`

.

The predicates in this module are named after the cases above.

## Predicates

case2aFromRank | Case 2a. |

case2aSomeAtRank | Gets a split that should be in |

succSplits | Holds if |