module Partition:sig
..end
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
module Key:sig
..end
type 'state
partition
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
type
rationing
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
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 |
(* | AutoUnroll(stmt, min, max) requests to find a "good" unrolling limit
between min and max for the loop stmt . | *) |
type
split_kind =
| |
Static |
| |
Dynamic |
type
split_monitor
val new_monitor : split_limit:int -> split_monitor
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
unroll_limit . Counters are incremented by the Incr_loop action. | *) |
| |
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
branch .
They will be kept separated from states coming from other branches.
The integer is the maximum number of successive branches kept in the keys:
this action also removes the oldest branches from the keys to meet this
constraint. | *) |
| |
Ration of |
(* |
Ensures that the first states encountered are kept separate, by creating a
unique ration stamp for each new state until the
limit is reached. The
same rationing can be used on multiple flows. Applying a new rationing
replaces the previous one.
If the rationing has been created with merge:true , all the states from
each flow receive the same stamp, but states from different flows receive
different stamps, until limit states have been tagged. | *) |
| |
Restrict of |
(* | Restrict (exp, list) restricts the rationing according to the evaluation
of the expression exp :
– for each integer i in list , states in which exp evaluates exactly
to the singleton i receive the same unique stamp, and will thus be
joined together but kept separate from other states;
– all other states are joined together.
Previous rationing is erased and replaced by this new stamping.
Implementation of the option -eva-split-return. | *) |
| |
Split of |
(* | Split (exp, kind, monitor) tries to separate states such as the exp
evaluates to a singleton value in each state in the flow. If necessary and
possible, splits states into multiple states. States in which the exp
evaluates to different values will be kept separate. Gives up the split
if exp evaluates to more than limit values, limit being the split
limit of the monitor . A same monitor can be used for successive splits
on different flows. | *) |
| |
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.
| *) |
exception InvalidAction
module MakeFlow: