Inductive Validity Core¶
The inductive validity core generation is a post-analysis treatement that computes a minimal subset of the model elements (assumptions, guarantees, stateful equations, or node calls) that are sufficient to prove all valid properties.
To enable inductive validity core generation, run
kind2 <lustre_file> --ivc true
Options¶
--ivc_category {node_calls|contracts|equations|assertions|annotations}
(default: all categories) – Minimize only a specific category of elements, repeat option to minimize multiple categories--ivc_only_main_node <bool>
(defaultfalse
) – Only elements of the main node are considered in the computation--ivc_all <bool>
(defaultfalse
) – Compute all the Minimal Inductive Validity Cores--ivc_approximate <bool>
(defaulttrue
) – Compute an approximation (superset) of a MIVC. Ignored if--ivc_all
or--ivc_must_set
istrue
--ivc_smallest_first <bool>
(defaultfalse
) – Compute a smallest IVC first. If--ivc_all
isfalse
, the computed IVC will be a smallest one--ivc_must_set <bool>
(defaultfalse
) – Compute the MUST set in addition to the IVCs--print_ivc <bool>
(defaulttrue
) – Print the inductive validity core computed--print_ivc_complement <bool>
(defaultfalse
) – Print the complement of the inductive validity core computed (= the elements that were not necessary to prove the properties)--minimize_program {no|valid_lustre|concise}
(defaultno
) – Minimize the source Lustre program according to the inductive validity core(s) computed--ivc_output_dir <string>
(default<INPUT_FILENAME>
) – Output directory for the minimized programs--ivc_uc_timeout <int>
(default0
) – Set a timeout for each unsat core check sent to the solver--ivc_precomputed_mcs <int>
(default0
) – When computing all MIVCs, set a cardinality upper bound for the precomputed MCSs (helps prune space of candidates)
Example¶
Let’s consider the following Lustre code:
contract fSpec(u,v: real) returns(r: real);
let
guarantee r >= 0.0;
guarantee true -> r >= pre(r);
guarantee r >= u;
guarantee r >= v;
tel;
node f(u, v : real) returns (r : real);
(*@contract import fSpec(u,v) returns (r) ; *)
var m1,m2: real;
let
m1 = if v > u then v else u;
m2 = if m1 > 0.0 then m1 else 0.0;
r = m2 -> if pre(r) > m1 then pre(r) else m1;
tel;
node main(x, y : real) returns (P : bool);
var a,b : real;
let
a = f(x,y);
b = f(y,x);
P = a >= x and a >= y and b >= x and b >= y;
--%PROPERTY P;
tel;
If we are interesting in determining which guarantees of the contract fSpec
of f
are needed to prove P
,
we should run this command:
kind2 <lustre_file> --ivc true --ivc_category contracts --ivc_only_main_node false --compositional true
--ivc_category contracts
: because we are only interested in minimizing the contractfSpec
--ivc_only_main_node false
: becausefSpec
is not the contract of the main node, so we need to consider all nodes--compositional true
: as we want to minimize the contract off
and not its implementation, we need to enable compositional analysis
We obtain the following inductive validity core:
IVC (2 elements):
Node f
Guarantee fSpec[l11c12].guarantee[l6c4][3] at position [l6c4]
Guarantee fSpec[l11c12].guarantee[l7c4][4] at position [l7c4]
Minimizing over a subset of the assumptions/guarantees¶
If you are interested in computing an IVC among a subset of the assumptions or guarantees, you can use the category annotations
.
The assumptions and guarantees that should be considered must be preceded by the keyword weakly
.
All the other assumptions and guarantees will be considered as always present when computing the IVCs.
For instance, we can modify the previous example as follows:
contract fSpec(u,v: real) returns(r: real);
let
weakly guarantee r >= 0.0;
guarantee true -> r >= pre(r);
weakly guarantee r >= u;
guarantee r >= v;
tel;
kind2 <lustre_file> --ivc true --ivc_category annotations --ivc_only_main_node false --compositional true
We obtain the following inductive validity core:
IVC (1 elements):
Node f
Guarantee fSpec[l11c12].weakly_guarantee[l6c4][3] at position [l6c4]
Computing all Inductive Validity Cores¶
If we want to compute ALL the minimal inductive validity cores, we can use the following flags:
kind2 <lustre_file> --ivc true --ivc_all true
--ivc_all true
: specify that we want to compute all the IVCs