Struct CsModel 

pub struct CsModel { /* private fields */ }

A definition type that instances new CsModelRun.

Implementations

impl CsModel

pub fn new(cs: ChannelSystemBuilder) -> Self

Creates a new CsModel from a ChannelSystemBuilder.

pub fn add_port(&mut self, channel: Channel, idx: usize, default: Val)

Adds a new port to the CsModel, which is given by an Channel and a default Val value.

pub fn add_predicate(&mut self, predicate: Expression<Atom>) -> usize

Adds a new predicate to the CsModel, which is an expression over the CS’s channels.

Trait Implementations

impl Clone for CsModel

fn clone(&self) -> CsModel

Returns a duplicate of the value.

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

Performs copy-assignment from source.

impl Debug for CsModel

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

Formats the value using the given formatter.

impl TransitionSystemGenerator for CsModel

type Ts<'a> = CsModelRun<'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.