Struct ChannelSystemBuilder 

pub struct ChannelSystemBuilder { /* private fields */ }

The object used to define and build a CS.

Implementations

impl ChannelSystemBuilder

pub fn new() -> Self

Create a new ProgramGraphBuilder with the given RNG (see also ChannelSystemBuilder::new). At creation, this will be completely empty.

pub fn new_program_graph(&mut self) -> PgId

Add a new PG to the CS.

pub fn new_var(&mut self, pg_id: PgId, val: Val) -> Result<Var, CsError>

Add a new variable of the given type to the given PG.

It fails if the CS contains no such PG, or if the expression is badly-typed.

See ProgramGraphBuilder::new_var for more info.

pub fn new_clock(&mut self, pg_id: PgId) -> Result<Clock, CsError>

Adds a new clock to the given PG and returns a Clock id object.

It fails if the CS contains no such PG.

See also ProgramGraphBuilder::new_clock.

pub fn new_action(&mut self, pg_id: PgId) -> Result<Action, CsError>

Adds a new action to the given PG.

It fails if the CS contains no such PG.

See also ProgramGraphBuilder::new_action.

pub fn add_reset( &mut self, pg_id: PgId, action: Action, clock: Clock, ) -> Result<(), CsError>

Adds resetting the clock as an effect of the given action.

Fails if either the PG does not belong to the CS, or either the action or the clock do not belong to the PG.

See also ProgramGraphBuilder::add_reset.

pub fn add_effect( &mut self, pg_id: PgId, action: Action, var: Var, effect: CsExpression, ) -> Result<(), CsError>

Add an effect to the given action of the given PG. It fails if:

• the CS contains no such PG;
• the given action does not belong to it;
• the given variable does not belong to it;
• trying to add an effect to a communication action.

// Create a new CS builder
let mut cs_builder = ChannelSystemBuilder::new();

// Add a new PG to the CS
let pg = cs_builder.new_program_graph();

// Create new channel
let chn = cs_builder.new_channel(vec![Type::Integer], Some(1));

// Create new send communication action
let send = cs_builder
    .new_send(pg, chn, vec![CsExpression::from(1i64)])
    .expect("always possible to add new actions");

// Add new variable to pg
let var = cs_builder
    .new_var(pg, Val::from(0i64))
    .expect("always possible to add new variable");

// It is not allowed to associate effects to communication actions
cs_builder.add_effect(pg, send, var, Expression::from(1i64))
    .expect_err("cannot add effect to receive, which is a communication");

See ProgramGraphBuilder::add_effect for more info.

pub fn new_location(&mut self, pg_id: PgId) -> Result<Location, CsError>

Adds a new location to the given PG.

It fails if the CS contains no such PG.

See also ProgramGraphBuilder::new_location.

pub fn new_timed_location( &mut self, pg_id: PgId, invariants: &[(Clock, Option<Time>, Option<Time>)], ) -> Result<Location, CsError>

Adds a new location to the given PG with the given time invariants, and returns its Location indexing object.

It fails if the CS contains no such PG.

See also ProgramGraphBuilder::new_timed_location.

pub fn new_process( &mut self, pg_id: PgId, location: Location, ) -> Result<(), CsError>

Adds a new process to the given PG starting at the given location.

It fails if the CS contains no such PG, or if the PG does not contain such location.

See also ProgramGraphBuilder::new_process.

pub fn new_initial_location(&mut self, pg_id: PgId) -> Result<Location, CsError>

Adds a new initial location to the given PG.

It fails if the CS contains no such PG.

See also ProgramGraphBuilder::new_initial_location.

pub fn new_initial_timed_location( &mut self, pg_id: PgId, invariants: &[(Clock, Option<Time>, Option<Time>)], ) -> Result<Location, CsError>

Adds a new initial location to the given PG with the given time invariants, and returns its Location indexing object.

It fails if the CS contains no such PG.

See also ProgramGraphBuilder::new_initial_timed_location.

pub fn add_transition( &mut self, pg_id: PgId, pre: Location, action: Action, post: Location, guard: Option<CsGuard>, ) -> Result<(), CsError>

Adds a transition to the PG.

Fails if the CS contains no such PG, or if the given action, variable or locations do not belong to it.

See also ProgramGraphBuilder::add_transition.

pub fn add_timed_transition( &mut self, pg_id: PgId, pre: Location, action: Action, post: Location, guard: Option<CsGuard>, constraints: &[(Clock, Option<Time>, Option<Time>)], ) -> Result<(), CsError>

Adds a timed transition to the PG with the given time constraints.

Fails if the CS contains no such PG, or if the given action, variable or locations do not belong to it.

See also ProgramGraphBuilder::add_timed_transition.

pub fn add_autonomous_transition( &mut self, pg_id: PgId, pre: Location, post: Location, guard: Option<CsGuard>, ) -> Result<(), CsError>

Adds an autonomous transition to the PG.

Fails if the CS contains no such PG, or if the given variable or locations do not belong to it.

See also ProgramGraphBuilder::add_autonomous_transition.

pub fn add_autonomous_timed_transition( &mut self, pg_id: PgId, pre: Location, post: Location, guard: Option<CsGuard>, constraints: &[(Clock, Option<Time>, Option<Time>)], ) -> Result<(), CsError>

Adds an autonomous timed transition to the PG with the given time constraints.

Fails if the CS contains no such PG, or if the given variable or locations do not belong to it.

See also ProgramGraphBuilder::add_autonomous_timed_transition.

pub fn new_channel( &mut self, var_types: Vec<Type>, capacity: Option<usize>, ) -> Channel

Adds a new channel of the given type and capacity to the CS.

• None capacity means that the channel’s capacity is unlimited.
• [Some(0)] capacity means the channel uses the handshake protocol (NOT YET IMPLEMENTED!)

pub fn new_send( &mut self, pg_id: PgId, channel: Channel, msgs: Vec<CsExpression>, ) -> Result<Action, CsError>

Adds a new Send communication action to the given PG.

Fails if the channel and message types do not match.

pub fn new_receive( &mut self, pg_id: PgId, channel: Channel, vars: Vec<Var>, ) -> Result<Action, CsError>

Adds a new Receive communication action to the given PG.

Fails if the channel and message types do not match.

pub fn new_probe_empty_queue( &mut self, pg_id: PgId, channel: Channel, ) -> Result<Action, CsError>

Adds a new ProbeEmptyQueue communication action to the given PG.

Fails if the queue uses the handshake protocol.

pub fn new_probe_full_queue( &mut self, pg_id: PgId, channel: Channel, ) -> Result<Action, CsError>

Adds a new ProbeFullQueue communication action to the given PG.

Fails if the queue uses the handshake protocol or it has infinite capacity.

pub fn build(self) -> ChannelSystem

Produces a ChannelSystem defined by the ChannelSystemBuilder’s data and consuming it.

Trait Implementations

impl Default for ChannelSystemBuilder

fn default() -> Self

Returns the “default value” for a type.