WhyMon: explanations as verdicts

Getting Started

To execute the project on your local machine, follow the instructions below.

Prerequisites

We recommend that you install a recent verion of the OCaml compiler (>= 4.11) and necessary dependencies with opam.

In particular, if you are a Debian/Ubuntu user

# apt-get install opam

or if you are an Arch Linux user

# pacman -S opam

and then

$ opam switch 4.13.1
$ eval $(opam config env)
$ opam install dune core_kernel base zarith menhir js_of_ocaml js_of_ocaml-ppx zarith_stubs_js

should be enough.

Running

From the root folder, you can compile the code with

$ dune build

to obtain the executable whymon.exe inside the folder bin. Moreover,

$ ./bin/whymon.exe --help

will print the usage statement. For instance, you can run one of our predefined examples with our output checker:

$ ./bin/whymon.exe -mode verified -sig examples/paper/publish_approve_manager.sig -formula examples/paper/publish_approve_manager.mfotl -log examples/paper/publish_approve_manager.log

You can remove the binary and clean the working directory with

$ dune clean

Formalization

The file src/checker.ml corresponds to the code extracted from the Isabelle formalization.

You can also extract this code on your local machine.

The formalization is compatible with Isabelle 2022, and depends on the corresponding Archive of Formal Proofs (AFP) version.

After setting up the AFP locally (by following these instructions), you can run

$ isabelle build -vd thys -eD code

from inside the formalization folder to produce the file formalization/code/checker.ocaml.

Syntax

Metric First-Order Temporal Logic

{PRED} ::= string

{VAR} ::= string

{VARS} ::=   {VAR}
           | {VAR}, {VARS}

{CONST} ::= quoted string

{I}  ::= [{NAT}, {UPPERBOUND}]

{UPPERBOUND} ::=   {NAT}
                 | INFINITY   (∞)

{f} ::=   {PRED}({VARS})
        | true                  (⊤)
        | false                 (⊥)
        | {VAR} EQCONST {CONST} (=)
        | NOT {f}               (¬)
        | {f} AND {f}           (∧)
        | {f} OR  {f}           (∨)
        | {f} IMPLIES {f}       (→)
        | {f} IFF {f}           (↔)
        | EXISTS {VAR}. {f}     (∃)
        | FORALL {VAR}. {f}     {∀}
        | PREV{I} {f}           (●)
        | NEXT{I} {f}           (○)
        | ONCE{I} {f}           (⧫)
        | EVENTUALLY{I} {f}     (◊)
        | HISTORICALLY{I} {f}   (■)
        | ALWAYS{I} {f}         (□)
        | {f} SINCE{I} {f}      (S)
        | {f} UNTIL{I} {f}      (U)
        | {f} TRIGGER{I} {f}    (T)
        | {f} RELEASE{I} {f}    (R)

Note that this tool also supports the equivalent Unicode characters (on the right).

Signature

{TYPE} ::= string | int

{VARTYPES} ::=   {VAR}:{TYPE}
               | {VAR}:{TYPE}, {VARTYPES}

{SIG} ::=   {PRED}({VARTYPES})
          | {PRED}({VARTYPES}) \n {SIG}

Trace

{VALUES} ::=   string
             | string, {VALUES}

{TRACE} :=   @{NAT} {PREDICATE}(VALUES)*
           | @{NAT} {PREDICATE}()* \n {TRACE}

where 0 <= {NAT} <= 2147483647.

License

This project is licensed under the GNU Lesser GPL-3.0 license - see LICENSE for details.