module Partition:sig
..end
A partition is a collection of states, each identified by a unique key. The keys define the states partition: states with identical keys are joined together, while states with different keys are maintained separate. A key contains the reason for which a state must be kept separate from others, or joined with similar states.
Partitioning actions allow updating the keys or spliting some states to define or change the partition. Actions are applied to flows, in which states with the same key are *not* automatically joined. This allows applying mutliple actions before recomputing the partitions. Flows can then be converted into partitions, thus merging states with identical keys.
Flows are used to transfer states from one partition to another. Transfer functions can be applied to flows; keys are maintained through transfer functions, until partitioning actions update them.
type
key
Partitioning keys attached to states.
module Key:sig
..end
type 'state
partition
Collection of states, each identified by a unique key.
val empty : 'a partition
val is_empty : 'a partition -> bool
val size : 'a partition -> int
val to_list : 'a partition -> 'a list
val find : key -> 'a partition -> 'a
val replace : key -> 'a -> 'a partition -> 'a partition
val merge : (key -> 'a option -> 'b option -> 'c option) ->
'a partition -> 'b partition -> 'c partition
val iter : (key -> 'a -> unit) -> 'a partition -> unit
val filter : (key -> 'a -> bool) ->
'a partition -> 'a partition
val map : ('a -> 'a) -> 'a partition -> 'a partition
typebranch =
int
Junction branch id in the control flow
type
rationing
Rationing are used to keep separate the n
first states propagated at
a point, by creating unique stamp until the limit is reached.
Implementation of the option -eva-slevel.
val new_rationing : limit:int -> merge:bool -> rationing
Creates a new rationing, that can be used successively on several flows.
type
unroll_limit =
| |
ExpLimit of |
(* | Value of the expression for each incoming state. The expression must evaluate to a singleton integer in each state. | *) |
| |
IntLimit of |
(* | Integer limit. | *) |
| |
AutoUnroll of |
(* |
| *) |
The unroll limit of a loop.
type
split_kind =
| |
Static |
| |
Dynamic |
Splits on an expression can be static or dynamic:
type
split_monitor
Split monitor: prevents splits from generating too many states.
val new_monitor : split_limit:int -> split_monitor
Creates a new monitor that allows to split up to split_limit
states.
type
action =
| |
Enter_loop of |
(* | Enters a loop in which the n first iterations will be kept separate:
creates an iteration counter at 0 for each states in the flow; states at
different iterations will be kept separate, untill reaching the
| *) |
| |
Leave_loop |
(* | Leaves the current loop: removes its iteration counter. States that were kept separate only by this iteration counter will be joined together. | *) |
| |
Incr_loop |
(* | Increments the iteration counter of the current loop for all states in the flow. States with different iteration counter are kept separate. | *) |
| |
Branch of |
(* | Identifies all the states in the flow as coming from | *) |
| |
Ration of |
(* | Ensures that the first states encountered are kept separate, by creating a
unique ration stamp for each new state until the | *) |
| |
Restrict of |
(* |
| *) |
| |
Split of |
(* |
| *) |
| |
Merge of |
(* | Forgets the split of an expression: states that were kept separate only by the split of this expression will be joined together. | *) |
| |
Update_dynamic_splits |
(* | Updates dynamic splits by evaluating the expression and spliting the states accordingly. | *) |
These actions redefine the partitioning by updating keys or spliting states. They are applied to all the pair (key, state) in a flow.
exception InvalidAction
module MakeFlow:
Flows are used to transfer states from one partition to another, by applying transfer functions and partitioning actions.