Struct Timeline 

pub struct Timeline { /* private fields */ }

The instants each clock of a multiclock assertion ticks at (16.13), over ONE shared axis of positions (the simulation’s time steps, or the trace’s rows). Position p is a tick of clock c when p is in c’s list.

Positions 0..real are the trace’s real steps. From real on, a word is the constant ⊤/⊥ tail of TailWord, which is a letter at EVERY position, so every position past real is a tick of every clock: the tail neither adds nor removes obligations clock by clock, it simply continues the verdict word. A clock with no list at all ticks at every position (the single-clock case, where a timeline is not needed).

Implementations

impl Timeline

pub fn new(real: u32, ticks: Vec<Vec<u32>>) -> Result<Self, TraceError>

ticks[c] is the sorted tick list of ClockId(c); every entry must be below real.

pub fn from_rows(rows: &[&[bool]]) -> Self

One tick list per row of rows: step t is a tick of clock c when rows[c][t]. The timeline is as long as the longest row.

pub fn real(&self) -> u32

The number of real steps.

pub fn truncated(&self, n: u32) -> Timeline

The first n real steps: the timeline of a word cut to n letters, whose later positions are the constant tail (a tick of every clock). A cut longer than the trace is the trace.

pub fn is_tick(&self, c: ClockId, p: u32) -> bool

Is p a tick of c?

pub fn next_tick(&self, c: ClockId, p: u32) -> u32

The first tick of c at or after p (p itself when it is one).

pub fn kth_after(&self, c: ClockId, p: u32, k: u32) -> u32

The k-th tick of c strictly after p (k == 0 is p itself: the caller is already standing on a tick). ##1 is k == 1: “the nearest strictly subsequent tick” (16.13.1).

Trait Implementations

impl Clone for Timeline

fn clone(&self) -> Self

Returns a duplicate of the value.

fn clone_from(&mut self, source: &Self)

Performs copy-assignment from source.

impl Debug for Timeline

fn fmt(&self, f: &mut Formatter<'_>) -> Result

Formats the value using the given formatter.

impl Eq for Timeline

impl PartialEq for Timeline

fn eq(&self, other: &Self) -> bool

Equality operator ==.

fn ne(&self, other: &Rhs) -> bool

Inequality operator !=.

impl StructuralPartialEq for Timeline