# SCAN
SCAN (StatistiCal ANalyzer) is a statistical model checker
designed to verify large concurrent systems
for which standard verification techniques do not scale.
## Development status
SCAN is currently under development at DIBRIS, University of Genoa (UniGe)
in the context of the [CONVINCE project](https://convince-project.eu/).
## Documentation
User documentation: [The SCAN Book](https://convince-project.github.io/scan).
API docs for the library crates:
- [`smc_scan_core`](https://docs.rs/smc_scan_core/latest/scan_core/)
- [`smc_scan_scxml`](https://docs.rs/smc_scan_scxml/latest/scan_scxml/)
- [`smc_scan_jani`](https://docs.rs/smc_scan_jani/latest/scan_jani/)
- [`smc_scan_promela`](https://docs.rs/smc_scan_promela/latest/scan_promela/)
- [`smc_scan_pmtl`](https://docs.rs/smc_scan_pmtl/latest/scan_pmtl/)
- [`smc_scan_mtl`](https://docs.rs/smc_scan_mtl/latest/scan_mtl/)
- [`smc_scan`](https://docs.rs/smc_scan/latest/scan/)
## Formalism
Internally, SCAN uses Channel Systems (CS) as models,[^1]
and past Metric Temporal Logic (pMTL) as property specification language.
SCAN is being developed to accept models specified in multiple, rich modeling languages.
At the moment the following languages are planned or (partially) implemented:
- [x] State Charts specified in [SCXML format](https://www.w3.org/TR/scxml/).
- [ ] [Promela](https://spinroot.com/spin/Man/Manual.html)
- [x] [JANI](https://jani-spec.org/)
## Installation
Currently, the only way to obtain SCAN is to build it from sources.
### Build prerequisites
SCAN is entirely written in [Rust](https://www.rust-lang.org/),
so, to build it, you need to install a recent version of the Rust toolchain.
The easiest and recommended way to do so is by installing [rustup](https://rustup.rs/)
either following the instructions on its homepage or through your OS's package manager.
Do not forget to set your `PATH` correctly, if required.
### Installing with Cargo
To install and use SCAN on your system,
the easiest way is to use the `cargo install` command.
Follow the instructions from the [Build prerequisites](#build-prerequisites) section to install the required build dependencies.
Then, install SCAN directly from `crates.io` with:
```console
cargo install smc_scan --locked
```
Cargo will build and install SCAN on your system
(the `--locked` option is not required,
but it is recommended as it improves build reproducibility
by enforcing the use of specified versions for dependencies).
For advanced installation options, refer to the [Install](https://convince-project.github.io/scan/manual/install.html) section of the SCAN Book.
## Usage
After installation, SCAN can be used as a CLI tool.
To print the help screen, use
```console
scan --help
```
which will show the available functionalities and commands' syntax.
To verify all specified properties over a model, for example, use:
```console
scan <MODEL> verify --all
```
where `MODEL` is the path to your model file or folder.
For an in-depth documentation of the user interface, refer to the [Interface](https://convince-project.github.io/scan/manual/interface.html) section of the SCAN Book.
## Development
For development's purposes, you will want to build and run SCAN from source code.
Use Cargo's usual `build` and `run` commands for that.
For example, from the repo's root folder, build SCAN with
```console
cargo build
```
Cargo, Rust's build manager, will take care of importing the required dependencies.
Run SCAN via Cargo with
```console
cargo run -- [ARGS]
```
or by running the executable file directly, with
```console
target/debug/scan [ARGS]
```
Install your local version of Scan on your system for more ease of use, with:
```console
cargo install --path <SCAN_REPO_PATH>
```
To build SCAN's documentation API (with suggested flags) and have it open in a browser tab, run:
```console
cargo doc --no-deps --workspace --open
```
Run all unit and integration tests with:
```console
cargo test --workspace
```