# Model Checking

Caesar has some support to export probabilistic programs written in (an executable fragment of) HeyVL to the *jani-model* format.
The JANI project defines exchange formats for quantitative model checking problems (and more).

Executable HeyVL programs are essentially programs without verification statements, where therefore the Markov chain semantics is clearly defined and the program can be executed forwards in a step-by-step fashion.

After exporting HeyVL programs to JANI, we can use our favorite probabilistic model checkers to calculate and/or verify expected rewards.
For now, we have only tested with the model checker *Storm*.

This feature is still under development. There are sure to be bugs and missing functionality. The encoding is sure to change in the near future.

## Usage

For a simple example, consider the HeyVL program below.

`@wp`

proc geo_mc(init_c: UInt) -> (c: UInt, cont: Bool)

post [!cont]

{

c = init_c

cont = true

while cont && c <= 20 {

var prob_choice: Bool = flip(0.5)

if prob_choice { cont = false } else { c = c + 1 }

}

}

To export JANI files for the model checker, simply run Caesar with the `--jani-dir DIR`

option to instruct it to save all translateable (co)procs to `.jani`

files in the directory `DIR`

:

`caesar example.heyvl --jani-dir DIR`

We use the probabilistic model checker Storm.
Running Storm on the produced file gives us the optimal value.^{1}
Procedure inputs to are translated to JANI's *constants*, and must be given to Storm via the flag `--constants init_c=0`

(any other initial value can be chosen).

`$ storm --jani DIR/FILE.jani -jprop reward --exact --sound --constants init_c=0`

Part of the output:

`Model checking property "reward": R[exp]{"reward"}min=? [C] ...`

Result (for initial states): 2097151/2097152 (approx. 0.9999995232)

In this particular case, we can obtain the optimal lower bound in Caesar by using the unrolling proof rule.
The annotation `@unroll(22, 0)`

for unrolling depth 22 finds the fixpoint in this case.
But this is only exact if we can bound the number of loop iterations statically.

## Supported Programs

The currently implemented translation only supports a subset of the executable fragment of HeyVL.

### Supported Declarations

`proc`

and`coproc`

specifications with:- Inputs and output declarations,
`pre`

declarations that are only Boolean conditions of the form`?(b)`

.`post`

declarations (arbitrary operands).

### Supported Statements

In the body, statements:

- Blocks,
- Variable declarations with initializers,
- Assignments with pure expressions,
- Sampling from distributions,
`reward`

statements,- In
`proc`

s:`assert`

statements with Boolean condition of the form`assert ?(b)`

,- Binary demonic choices,

- In
`coproc`

s: - If-then-else statements,
- While loops (with least-fixed point semantics — see below for semantics details),
- Annotations, in particular proof rule annotations, will be ignored.

#### Loop Semantics

In the JANI translation, while loops are always assumed to have **least fixed-point semantics** when model-checking.^{2}
That means we just accumulate total expected rewards over all terminating executions in the Markov chain.
This corresponds to wp/ert semantics.

Notice that in `proc`

s, this is different from the default behavior of Caesar's proof rules such as induction.
They would assume greatest fixed-point (wlp) semantics in `proc`

s.
We recommend always adding the `@wp`

or `@ert`

annotations to your `proc`

/`coproc`

.
They instruct Caesar to enforce that sound proof rules for least fixed-point semantics are being used.

If you want one-bounded wlp semantics (greatest fixed-points), then you can use the generated property `diverge_prob`

to obtain the probability of divergence.
Then the result should be the sum of the `reward`

and `diverge_prob`

properties (Storm: `-jprop reward,diverge_prob`

).^{3}

If you want *unbounded* greatest fixed-point semantics, then you can use the generated property `can_diverge`

to check whether there is a diverging path.
Then the result is `\infty`

if `can_diverge`

is `true`

, otherwise the result is `reward`

.^{4}
This property is currently not supported by Storm.^{5}

We intentionally avoid using the *reachability reward* properties (i.e. setting the `reach`

property of `ExpectedValueExpression`

in JANI) as it will assign the expected reward `\infty`

to any state from which goal states are not reachable with probability 1.
If the program is not AST, then this does not correspond to either least or greatest fixpoint semantics weakest pre-expectation style semantics that we know of.

### Supported Types

The supported types of values are:

Make sure to check in your model checker's documentation how these types are realized. For example, Storm assumes 32-bit numbers by default for unbounded integer types.

`EUReal`

values are currently only supported as values in `pre`

/`post`

declarations and in `assert`

statements.
The value `\infty`

cannot be explicitly represented in JANI, therefore `EUReal`

expressions that go beyond the specific supported verification constructs are not supported.

### Not Supported

In particular, the following constructs are *not* supported:

- Calls to uninterpreted functions or to
`proc`

s/`coproc`

s, - Uninitialized variable declarations or
`havoc`

/`cohavoc`

statements, - Quantitative verification statements such as
`assume`

/`assert`

in arbitrary locations. - User-defined domains, axioms will be ignored.

- We use the
`--exact`

and`--sound`

flags to ensure that Storm is forced to use exact arithmetic and only sound algorithms to produce the solution. Consult your chosen model checker's documentation to see which guarantees they give.↩ - We always use least-fixed point semantics because encoding greatest fixpoint/weakest
*liberal*pre-expectation semantics seems to be impossible with a single JANI property right now.↩ - Corollary 4.26 of Benjamin Kaminski's PhD thesis states that (one-bounded)
`wlp`

can be computed via`wp`

plus the probability of divergence.↩ - This is similar to the qualitative wlp, which evaluates to the top element of the Boolean lattice (
`true`

) if the loop has a possibility of nontermination. In the quantitative setting, we have`\infty`

as our top element of the`EUReal`

lattice.↩ - Storm currently does not support the qualitative analysis required for the
`can_diverge`

property and will throw an error. The feature is tracked in the issue moves-rwth/storm#529.↩