Trait SessionLaws 

pub trait SessionLaws<This>
where
    This: UndertakingAlg + RunReadAlg + RunHoldAlg + AttentionAlg + ClockAlg + SessionLawFixture,
    This::Id: Clone + Eq + Debug,
{
    // Required methods
    fn session_laws(&mut self) -> Result<()>;
    fn check_beginning_laws(&mut self) -> Result<()>;
    fn check_saying_laws(&mut self) -> Result<()>;
    fn check_unwanted_laws(&mut self) -> Result<()>;
    fn check_holding_laws(&mut self) -> Result<()>;
}

Authors the attendance laws.

Required Methods

fn session_laws(&mut self) -> Result<()>

Checks that one pass reconciles what is wanted with what is happening.

The laws checked are:

1. one pass begins every request wanting work, and no other;
2. a request whose work has begun is not begun again, however many passes run;
3. everything a run said is told before how it ended, and nothing is told after;
4. work refusing to begin ends once and is not begun again;
5. a run nobody wants is told to end on every pass until it is over, and ends once;
6. time a run is held still is not counted as time it was running;
7. attending to no runs tells nothing.

Errors

Returns the first violated law.

fn check_beginning_laws(&mut self) -> Result<()>

Checks what one pass begins, and what it declines to begin twice.

Errors

Returns the first violated law.

fn check_saying_laws(&mut self) -> Result<()>

Checks that what a run said reaches the request before how it ended.

Errors

Returns the first violated law.

fn check_unwanted_laws(&mut self) -> Result<()>

Checks how a run nobody wants any more is ended.

Errors

Returns the first violated law.

fn check_holding_laws(&mut self) -> Result<()>

Checks that time a run is held still is not time it was running.

Errors

Returns the first violated law.

Dyn Compatibility

This trait is dyn compatible.

In older versions of Rust, dyn compatibility was called "object safety".

Implementors

impl<This> SessionLaws<This> for This

where This: UndertakingAlg + RunReadAlg + RunHoldAlg + AttentionAlg + ClockAlg + SessionLawFixture, This::Id: Clone + Eq + Debug,

Authors the attendance laws.