Skip to main content

Crate scan_core

Crate scan_core 

Source
Expand description

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

This crate is part of the SCAN statistical 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§

Report
Final report for a verification run.
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 properties is abstracted through the Oracle trait, to provide a unified interface.
TimeRange
A time constraint given by lower bound and upper bounds.
TransitionSystem
A definition type that instances new [CsModelRun].
TransitionSystemRun
Transition system model based on a ChannelSystem.

Enums§

Atom
An atomic variable exposed by the [ChannelSystem to the TransitionSystem].
BooleanExpr
Boolean expressions.
Expression
Expressions for the language internally used by PGs and CSs.
FloatExpr
Floating-point numerical expression.
IntegerExpr
Integer expressions.
NaturalExpr
A Natural number expression
ScanError
Errors that can be returned by a [Scan] method
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.

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.
TraceWriter
A writer for traces