smc_scan_core 0.2.0

Core module for the Scan model checker.
Documentation 
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34

use std::fs::File;

use flate2::write::GzEncoder;

use crate::{
    Time, Val,
    channel_system::{Action, Event},
};

/// A writer for traces
pub type TraceWriter = GzEncoder<File>;

/// Trait that handles streaming of traces,
/// e.g., to print them to file.
pub trait Tracer {
    /// The extension to use for files of traces produced by the [`Tracer`].
    const EXTENSION: &str;

    /// Underlying model data to be traced.
    type ModelData;

    /// Creates and initializes the Tracer
    fn init(writer: TraceWriter, data: &Self::ModelData) -> Self;

    /// Stream a new state of the trace.
    fn trace(
        &mut self,
        data: &Self::ModelData,
        action: Action,
        event: &Event,
        time: Time,
        ports: &[Vec<Val>],
    );
}