# Assumption Generation¶

In the early stages of model development and analysis, properties of system components often fail to hold because the assumptions made about a component’s environment are insufficient to guarantee these properties, even when component’s behavior is correctly specified. When this happens, the system designer must study the counterexample provided by Kind 2, pinpoint the cause, and identify possible restrictions on the environment that the properties need in order to hold — which were perhaps assumed by the designer but were not made explicit.

For instance, consider the following Lustre program:

```
node Arbiter (s1,s2: bool; e1,e2:int) returns(o: int);
(*@contract
guarantee "G1" s1 => o=e1;
guarantee "G2" s2 => o=e2;
*)
let
if s1 and s2 then
o = any { o:int | o = e1 or o = e2 };
elsif s1 then
o = e1;
else
o = e2;
fi
tel
```

If we run Kind 2 to check guarantees `G1`

and `G2`

, Kind 2 determines
the properties are invalid, providing a counterexample for each of them.
In the first counterexample, `s1`

and `s2`

are true initially, and
the output is equal to the value of `e2`

, which falsifies `G1`

.
In the second counterexample, `s1`

and `s2`

are true initially, and
the output is equal to the value of `e1`

, which falsifies `G2`

.

From the description of the counterexamples,
it is evident that one potential missing assumption is that
`s1`

and `s2`

are never simultaneously true.
If that is indeed the case, explicitly stating this assumption
in the contract of the node,
allows Kind 2 to prove both properties valid.

Generating the missing assumptions for straightforward examples like the one
above is not very difficult. However, in more realistic scenarios,
this task can become quite challenging.
To help system designers in those situations,
Kind 2 offers a post-analysis that can be enabled by
passing the command-line option `--assumption_gen true`

.
When this option is enabled, Kind 2 will automatically generate assumptions
that are strong enough to prove the set of falsified properties
in the verification analysis while not being overly restrictive.
Note that just finding sufficient assumptions is not challenging.
The challenge is to find minimally restrictive assumptions
which can then be recognized as realistic by the designer.

For the example above, Kind 2 generates the assumption:
`(not s2) or (not s1) or (e1 = e2)`

.
Notice that this assumption is a weaker version of the one mentioned above,
as it considers a third case where the inputs `e1`

and
`e2`

equal.

The functionality generates one-state constraints on a node’s environment, but it currently lacks the capability to generate two-state properties, which presents a significantly more complex challenge.