Struct ProgramGraphBuilder 

pub struct ProgramGraphBuilder { /* private fields */ }

Defines and builds a PG.

Implementations

impl ProgramGraphBuilder

pub fn new() -> Self

Creates a new ProgramGraphBuilder. At creation, this will only have the initial location with no variables, no actions and no transitions.

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

Adds a new variable with the given initial value (and the inferred type) to the PG. It creates and uses a default RNG for probabilistic expressions.

It fails if the expression giving the initial value of the variable is not well-typed.

// Create a new action
let action = pg_builder.new_action();

// Create a value to assign the expression.
let val = (PgExpression::from(40i64) + PgExpression::from(40i64)).unwrap().eval_constant().unwrap();

// Create a new variable
let var = pg_builder
    .new_var(val)
    .unwrap();

pub fn new_clock(&mut self) -> Clock

Adds a new clock and returns a Clock id object.

See also crate::channel_system::ChannelSystemBuilder::new_clock.

pub fn new_action(&mut self) -> Action

Adds a new action to the PG.

// Create a new action
let action: Action = pg_builder.new_action();

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

Associates a clock reset to an action.

Returns an error if the clock to be reset does not belong to the Program Graph.

let action = pg_builder.new_action();
let clock = other_pg_builder.new_clock();
// Associate action with clock reset
pg_builder
    .add_reset(action, clock)
    .expect_err("the clock does not belong to this PG");

pub fn add_effect( &mut self, action: Action, var: Var, effect: PgExpression, ) -> Result<(), PgError>

Adds an effect to the given action. Requires specifying which variable is assigned the value of which expression whenever the action triggers a transition.

It fails if the type of the variable and that of the expression do not match.

// Create a new action
let action: Action = pg_builder.new_action();

// Create a new variable
let var: Var = pg_builder.new_var(Val::from(true)).expect("expression is well-typed");

// Add an effect to the action
pg_builder
    .add_effect(action, var, PgExpression::from(1i64))
    .expect_err("var is of type bool but expression is of type integer");
pg_builder
    .add_effect(action, var, PgExpression::from(false))
    .expect("var and expression type match");

pub fn new_location(&mut self) -> Location

Adds a new location to the PG and returns its Location indexing object.

pub fn new_timed_location( &mut self, invariants: Vec<TimeConstraint>, ) -> Result<Location, PgError>

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

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

Adds a new (synchronous) process to the PG starting from the given Location.

pub fn new_initial_location(&mut self) -> Location

Adds a new process starting at a new location to the PG and returns the Location indexing object.

pub fn new_initial_timed_location( &mut self, invariants: Vec<TimeConstraint>, ) -> Result<Location, PgError>

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

pub fn add_transition( &mut self, pre: Location, action: Action, post: Location, guard: Option<PgGuard>, ) -> Result<(), PgError>

Adds a transition to the PG. Requires specifying:

• state pre-transition,
• action triggering the transition,
• state post-transition, and
• (optionally) boolean expression guarding the transition.

Fails if the provided guard is not a boolean expression.

// The builder is initialized with an initial location
let initial_loc = pg_builder.new_initial_location();

// Create a new action
let action = pg_builder.new_action();

// Add a transition
pg_builder
    .add_transition(initial_loc, action, initial_loc, None)
    .expect("this transition can be added");
pg_builder
    .add_transition(initial_loc, action, initial_loc, Some(BooleanExpr::from(false)))
    .expect("this one too");

pub fn add_timed_transition( &mut self, pre: Location, action: Action, post: Location, guard: Option<PgGuard>, constraints: Vec<TimeConstraint>, ) -> Result<(), PgError>

Adds a timed transition to the PG under timed constraints. Requires specifying the same data as ProgramGraphBuilder::add_transition, plus a slice of time constraints.

Fails if the provided guard is not a boolean expression.

// The builder is initialized with an initial location
let initial_loc = pg_builder.new_initial_location();

// Create a new action
let action = pg_builder.new_action();

// Add a new clock
let clock = pg_builder.new_clock();

// Add a timed transition
pg_builder
    .add_timed_transition(initial_loc, action, initial_loc, None, vec![(clock, None, Some(1))])
    .expect("this transition can be added");
pg_builder
    .add_timed_transition(initial_loc, action, initial_loc, Some(BooleanExpr::from(false)), vec![(clock, Some(1), None)])
    .expect("this one too");

pub fn add_autonomous_transition( &mut self, pre: Location, post: Location, guard: Option<PgGuard>, ) -> Result<(), PgError>

Adds an autonomous transition to the PG, i.e., a transition enabled by the epsilon action. Requires specifying:

• state pre-transition,
• state post-transition, and
• (optionally) boolean expression guarding the transition.

Fails if the provided guard is not a boolean expression.

// The builder is initialized with an initial location
let initial_loc = pg_builder.new_initial_location();

// Add a transition
pg_builder
    .add_autonomous_transition(initial_loc, initial_loc, None)
    .expect("this autonomous transition can be added");
pg_builder
    .add_autonomous_transition(initial_loc, initial_loc, Some(BooleanExpr::from(false)))
    .expect("this one too");

pub fn add_autonomous_timed_transition( &mut self, pre: Location, post: Location, guard: Option<PgGuard>, constraints: Vec<TimeConstraint>, ) -> Result<(), PgError>

Adds an autonomous timed transition to the PG, i.e., a transition enabled by the epsilon action under time constraints. Requires specifying the same data as ProgramGraphBuilder::add_autonomous_transition, plus a slice of time constraints.

Fails if the provided guard is not a boolean expression.

// The builder is initialized with an initial location
let initial_loc = pg_builder.new_initial_location();

// Add a new clock
let clock = pg_builder.new_clock();

// Add an autonomous timed transition
pg_builder
    .add_autonomous_timed_transition(initial_loc, initial_loc, None, vec![(clock, None, Some(1))])
    .expect("this transition can be added");
pg_builder
    .add_autonomous_timed_transition(initial_loc, initial_loc, Some(BooleanExpr::from(false)), vec![(clock, Some(1), None)])
    .expect("this one too");

pub fn build(self) -> ProgramGraph

Produces a ProgramGraph defined by the ProgramGraphBuilder’s data and consuming it.

Since the construction of the builder is already checked ad every step, this method cannot fail.

Trait Implementations

impl Clone for ProgramGraphBuilder

fn clone(&self) -> ProgramGraphBuilder

Returns a duplicate of the value.

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

Performs copy-assignment from source.

impl Debug for ProgramGraphBuilder

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

Formats the value using the given formatter.

impl Default for ProgramGraphBuilder

fn default() -> Self

Returns the “default value” for a type.