Module program_graph 

Implementation of the PG model of computation.

A Program Graph is given by:

• a finite set L of locations;
• a finite set A of actions;
• a finite set V of typed variables;
• a transition relation that associates pairs of locations (pre-location and post-location) and an action with a Boolean expression (the guard of the transition);
• for each actions, a set of effects, i.e., a variable x from V and an expression in the variables of V of the same type as x.

The state of a PG is given by its current location and the value assigned to each variable. The PG’s state evolves by non-deterministically choosing a transition whose pre-state is the current state, and whose guard expression evaluates to true. Then, the post-state of the chosen transition becomes the current state of the PG. Finally, the effects of the transition’s associated action are applied in order, by assigning each effect’s variable the value of the effect’s expression evaluation.

A PG is represented by a ProgramGraph and defined through a ProgramGraphBuilder, by adding, one at a time, new locations, actions, effects, guards and transitions. Then, the ProgramGraph is built from the ProgramGraphBuilder and can be executed by performing transitions, though the structure of the PG itself can no longer be altered.

// Create a new PG builder
let mut pg_builder = ProgramGraphBuilder::new();

// 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();

// Create a new location
let post_loc = pg_builder.new_location();

// Add a transition (the guard is optional, and None is equivalent to the guard always being true)
let result = pg_builder.add_transition(initial_loc, action, post_loc, None);

// This can only fail if the builder does not recognize either the locations
// or the action defining the transition
result.expect("both the initial location and the action belong to the PG");

// Build the PG from its builder
// The builder is always guaranteed to build a well-defined PG and building cannot fail
let pg = pg_builder.build();
let mut instance = pg.new_instance();

// Execution starts in the initial location
assert_eq!(instance.current_states().as_slice(), &[initial_loc]);

// Compute the possible transitions on the PG
{
    let mut iter = instance .possible_transitions();
    let (act, mut trans) = iter.next().unwrap();
    assert_eq!(act, action);
    let post_locs: Vec<Location> = trans.next().unwrap().collect();
    assert_eq!(post_locs, vec![post_loc]);
    assert!(iter.next().is_none());
}

// Perform a transition
let mut rng: SmallRng = rand::make_rng();
let result = instance .transition(action, &[post_loc], &mut rng);

// Performing a transition can fail, in particular, if the transition was not allowed
result.expect("The transition from the initial location onto itself is possible");

// There are no more possible transitions
assert!(instance.possible_transitions().next().is_none());

// Attempting to transition results in an error
instance.transition(action, &[post_loc], &mut rng).expect_err("The transition is not possible");

Structs

Action

An indexing object for actions in a PG.

Clock

An indexing object for clocks in a PG.

Location

An indexing object for locations in a PG.

ProgramGraph

A definition object for a PG. It represents the abstract definition of a PG.

ProgramGraphBuilder

Defines and builds a PG.

ProgramGraphRun

Representation of a PG that can be executed transition-by-transition.

Var

An indexing object for typed variables in a PG.

Enums

PgError

The error type for operations with ProgramGraphBuilders and ProgramGraphs.

Type Aliases

ActionIdx

The index for Actions in a ProgramGraph.

LocationIdx

The index for Locations in a ProgramGraph.

PgExpression

An expression using PG’s Var as variables.

PgGuard

A Boolean expression over Var variables.

TimeConstraint

A time constraint given by a clock and, optionally, a lower bound and/or an upper bound.