Trait stateright::Representative

pub trait Representative {
    // Required method
    fn representative(&self) -> Self;
}

This trait is used to reduce the state space when checking a model with CheckerBuilder::symmetry. The trait indicates the ability to generate a representative from a symmetry equivalence class for each state in Model::State.

Bošnački, Dams, and Holenderski provide a clarifying example in their paper “Symmetric Spin”:

“In order to grasp the idea of symmetry reduction, consider a mutual exclusion protocol based on on semaphores. The (im)possibility for processes to enter their critical sections will be similar regardless of their identities, since process identities (pids) play no role in the semaphore mechanism. More formally, the system state remains behaviorally equivalent under permutations of pids. During state-space exploration, when a state is visited that is the same, up to a permutation of pids, as some state that has already been visited, the search can be pruned.”

How to Implement

Here is an example implementation:

use stateright::{Representative, Rewrite, RewritePlan};
use stateright::util::DenseNatMap;

struct SystemState {
    process_states: DenseNatMap<Pid, ProcessState>,
    time_slice_sequence: Vec<Pid>,
    // ... etc ...
}
impl Representative for SystemState {
    fn representative(&self) -> Self {
        let plan = (&self.process_states).into();
        Self {
            process_states: self.process_states.rewrite(&plan),
            time_slice_sequence: self.time_slice_sequence.rewrite(&plan),
            // ... etc ...
        }
    }
}

#[derive(Clone, Eq, Ord, PartialEq, PartialOrd)]
struct ProcessState {
    program_counter: usize,
    parent: Pid,
    // ... etc ...
}
impl Rewrite<Pid> for ProcessState {
    fn rewrite<S>(&self, plan: &RewritePlan<Pid,S>) -> Self {
        Self {
            program_counter: self.program_counter.rewrite(plan), // no-op (cannot contain `Pid`)
            parent: self.parent.rewrite(plan),
            // ... etc ...
        }
    }
}

Required Methods

fn representative(&self) -> Self

Generates a representative value in an equivalence class for self.

Implementors

impl<A, H> Representative for ActorModelState<A, H>where A: Actor, A::Msg: Rewrite<Id>, A::State: Ord + Rewrite<Id>, H: Rewrite<Id>,