Crate scan_core 

Implementation of program graphs (PG) and channel systems (CS) formalisms¹ for use in the SCAN model checker.

---

1. Baier, C., & Katoen, J. (2008). Principles of model checking. MIT Press. ↩

Modules

channel_system

Implementation of the CS model of computation.

program_graph

Implementation of the PG model of computation.

Structs

CsModel

A definition type that instances new CsModelRun.

CsModelRun

Transition system model based on a ChannelSystem.

MtlOracle

An oracle for (simple) Mtl properties.

PgModel

A ProgramGraph-based model implementing TransitionSystem with synchronous concurrency.

PgModelRun

A model based on a single ProgramGraph, with predicates over the PG’s variables.

PmtlOracle

An oracle for PMTL properties over timed, dense traces.

Scan

The main type to interface with the verification capabilities of SCAN. Scan holds the model, properties and other data necessary to run the verification process. The type of models and properties is abstracted through the TransitionSystem and Oracle traits, to provide a unified interface.

Enums

Atom

An atomic variable for crate::Pmtl formulae.

BooleanExpr

Boolean expressions.

Expression

Expressions for the language internally used by PGs and CSs.

FloatExpr

Floating-point numerical expression.

IntegerExpr

Integer expressions.

Mtl

An Metric Temporal Logic (MTL) formula.

NaturalExpr

A Natural number expression

Pmtl

A Past-time Metric Temporal Logic (PMTL) formula.

RunOutcome

The possible outcomes of a model execution.

Type

The types supported by the language internally used by PGs and CSs.

TypeError

The error type for operations with Type.

Val

Possible values for each Type.

Traits

Oracle

Implementators are induced by a temporal property. They can update their internal state when fed a new state of a trace, and establish whether their corresponding property holds on such trace.

Tracer

Trait that handles streaming of traces, e.g., to print them to file.

TransitionSystem

Trait for types that can execute like a transition system.

TransitionSystemGenerator

A type that can generate instances of a TransitionSystem.

Functions

adaptive_bound

Computes adaptive bound for given confidence, precision and (partial) experimental results.

derive_precision

Computes precision for given experimental results and confidence deriving it from adaptive bound through quadratic equation.

okamoto_bound

Computes Okamoto bound for given confidence and precision.

Type Aliases

Float

Floating-point values.

Integer

Integer values.

Natural

Natural (unsigned) values.

Time

The type that represents time.