package frama-c

You can search for identifiers within the package.

in-package search v0.2.0

On This Page

Parameters
Signature

Platform dedicated to the analysis of source code written in C

Install

dune-project

Dependency

frama-c.com Edit opam file Versions (30)

Authors

Maintainers

F

frama-ci-bot@frama-c.com

Sources

frama-c-33.0-Arsenic.tar.gz

sha256=9c1cbffd28bb33c17a668107e39c96e4ae7378a3d8249f69b47afc7ee964e9b8

doc/frama-c.kernel/Frama_c_kernel/Lti_system/Make/index.html

Module `Lti_system.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 = {

state_matrix : ('n, 'n) Linear.matrix;
input_matrix : ('n, 'm) Linear.matrix;
input_space : 'm box;
shift : 'n Linear.vector;
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 = {

transition : 'n box list;
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 optional 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 as a ratio between 0 and 1.

val pretty_behavior : 'n behavior option Pretty_utils.formatter

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