Frama-C:
Plug-ins:
Libraries:

Frama-C API - Make

Parameters

module K : Field.S

Signature

module Linear : sig ... end

The linear space in which the systems are defined.

module Box : sig ... end
type 'n box = 'n Box.t
type ('n, 'm) system = {
  1. state_matrix : ('n, 'n) Linear.matrix;
  2. input_matrix : ('n, 'm) Linear.matrix;
  3. input_space : 'm box;
  4. shift : 'n Linear.vector;
  5. initial_state : 'n Linear.vector;
}

A LTI system full specification. The fields are as follows:

  • state_matrix: the system's state matrix A;
  • input_matrix: the system's input matrix B;
  • input_space: the box containing all input vectors;
  • shift: the system's shift vector S;
  • initial_state: the system's initial state X[0].
type 'n behavior = {
  1. transition : 'n box list;
  2. permanent : 'n box;
}

Representation of a LTI system's behavior. The fields are as follows:

  • transition represents the transition phase as a list of boxes, one for each iteration that cannot be proven contained in the permanent phase. The length of the list, i.e the number of unrolled iterations, depends on the system's parameters and on the precision of the permanent phase's abstraction.
  • permanent represents the permanent phase as a unique box, which is an invariant for the filter for all iterations after the ones unrolled through the transition phase.
val behavior : ?timeout:float -> completion_target:float -> ('n Nat.succ, 'm Nat.succ) system -> 'n Nat.succ behavior option

Behavior computation. See module-level documentation for a general overview and a link to the underlying theory. The optionnal parameters are as follows:

  • timeout specifies the maximum analysis duration. It is expressed in seconds, and its default value is one second.
  • completion_target specifies the relative completion of the permanent phase that must be achieved, i.e how much of the permanent box is proven to be a valid and reachable state of the system. It is expressed in percentage between 0 and 100.
val pretty_behavior : 'n behavior option Pretty_utils.formatter

Pretty print a behavior. Used for test and debug purposes.