Running

Running#

These instructions are for using the provided R2U2 CLI example; to use R2U2 as a library, see embedding R2U2.

Prerequisites#

  1. Build r2u2_cli crate

  2. A C2PO specification file

Note

If r2u2_cli was built locally, run the r2u2_cli with following command: ./target/release/r2u2_cli. If r2u2_cli was installed from crates.io, run by simply calling r2u2_cli.

Use r2u2_cli to compile only#

Usage: r2u2_cli compile [OPTIONS] <SPEC> <MAP>

Arguments:

       <SPEC> Sets a specification .c2po or .mltl file or spec.bin

       <MAP> Sets a trace .csv or a map .map file

Options:

      -o, --output <PATH> Sets location to save output in a file (default = current directory)

            --disable-booleanizer Disables booleanizer (default = booleanizer enabled)

            --disable-aux Disable Assume-Guarantee Contract (AGC) and auxiliary specification logging

            --disable-rewrite Disables rewrite rules (default = rewrite rules enabled)

            --disable-cse Disables common subexpression elimination (CSE) (default = CSE enabled)

            --enable-sat Enables SAT checking through Z3 -> Z3 must be installed (default = SAT disabled)

            --timeout-sat <TIMEOUT_SAT> Set the timeout of SAT calls in seconds (default: 3600)

      -h, --help Print help

Use r2u2_cli to run R2U2#

Usage: r2u2_cli run [OPTIONS] <SPEC> <TRACE>

Arguments:

       <SPEC> Sets a specification .c2po or .mltl file or spec.bin

       <TRACE> Sets a trace .csv file

Options:

      -o, --output <PATH> Sets location to save output in a file (default = print to terminal)

            --disable-contracts Disable assume-guarantee contract status logging

            --enable-aux Enable auxiliary specification logging

      -h, --help Print help

Contents