Struct PgModel 

pub struct PgModel { /* private fields */ }

A ProgramGraph-based model implementing TransitionSystem with synchronous concurrency.

Implementations

impl PgModel

pub fn new( pg: ProgramGraphBuilder, global_vars: Vec<Var>, predicates: Vec<PgExpression>, ) -> Self

Create a new PgModel from the given ProgramGraph and predicates over its internal state.

Trait Implementations

impl Clone for PgModel

fn clone(&self) -> PgModel

Returns a duplicate of the value.

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

Performs copy-assignment from source.

impl Debug for PgModel

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

Formats the value using the given formatter.

impl TransitionSystemGenerator for PgModel

type Ts<'a> = PgModelRun<'a> where Self: 'a

The type of TransitionSystem to be generated.

fn generate<'a>(&'a self) -> Self::Ts<'a>

Generate a new instance of the TransitionSystem.