Skip to content

Commit

Permalink
website: add comment about --no-verify option
Browse files Browse the repository at this point in the history
  • Loading branch information
Philipp15b committed Dec 21, 2024
1 parent 3ae2ff5 commit 09b349e
Showing 1 changed file with 3 additions and 1 deletion.
4 changes: 3 additions & 1 deletion website/docs/model-checking.md
Original file line number Diff line number Diff line change
Expand Up @@ -54,9 +54,11 @@ proc geo_mc(init_c: UInt) -> (c: UInt, cont: Bool)
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`:

```bash
caesar example.heyvl --jani-dir DIR
caesar example.heyvl --jani-dir DIR --no-verify
```

The `--no-verify` option tells Caesar to skip the actual verification because it is not needed for the JANI output.

The output JANI files will have the following structure that you can use:
* Properties:
* `reward`: This is the expected value of the verification conditions (cf. [Statements](./heyvl/statements.md)).
Expand Down

0 comments on commit 09b349e

Please sign in to comment.