ProFlo – a language for specifying control flows of processes

ProFlo expressions [1][2] can be used for writing behavioural specifications which can be translated to Petri nets or STGs. In some situations this may be faster than drawing a Petri net or STG in the visual editor. Moreover, there are situations when control flow expressions are straightforward to write but the equivalent Petri net is difficult to design manually (e.g. see Example 3 below).

Example 1: Specification of an inverter with input in and output out. It is assumed that the intial state of the signals is in=0, out=1, and that the environment is well-behaved, i.e. does not change the value of the input until the output changes:

.inputs in
.outputs out
.process
{ in+; out-; in+; out+ }

Here the interpretation of actions (like in) is as in STGs, operator {…} denotes iteration, i.e. the behavior in braces is repeated, and operator ; denotes sequential composition, i.e. the four actions inside {…} are executed sequentially, one after another.

The tool can automatically generate an STG from this expression:

• open Workcraft and create a new Signal Transition Graph (STG) model;
• click the Conversion→Translate ProFlo expression… menu item;
• copy and paste the above expression to the text box in the Control Flow Logic Translator dialog and click    OK   .

The sequential composition operator ; can be omitted:

.inputs in
.outputs out
.process
{ in+ out- in- out+ } // semicolons between the actions are implicit

Furthermore, spaces, tabs, new lines and comments can be arbitrarily added or removed (as long as adjacent identifiers are not glued together into one identifier), e.g. the following expressions are equivalent to the initial specification:

.inputs in
.outputs out
.process
{in+out-in-out+} // spacing is flexible as long as one can distinguish different actions

// this is a specification of an inverter with input in and output out,
// augmented with long-winded hair-splitting comments

.inputs in // declare 'in' as an input signal
.outputs out // declare 'out' as an output signal

// all the actions in the process below must refer to the declared signals,
// and any other actions (e.g. misspelled ones) will cause a syntax error
.process
  { // begin iteration - the following behaviour is repeated 0 or more times:
    in+  // the environment is allowed to switch in from 0 to 1
    out+ // in response, the circuit must eventually switch out from 1 to 0
    in-  // only after out+ has completed, the environment is allowed to switch in from 1 to 0
    out- // in response, the circuit must eventually switch out from 0 to 1
  } // end iteration

Example 2: Specification of a C-element with inputs in1 and in2 and output out:

.inputs in1 in2
.outputs out
.process
{ (in1+ | in2+) out+ (in1- | in2-) out- }

Here, parallel composition (or interleaving) operator | is used to express the concurrency between inputs, and parentheses are used to override the default precedence of operators. The tool generates the following STG:

Example 3: Choice between 10 pairs of concurrent events:

  (a0 | b0) # (a1 | b1) # (a2 | b2) # (a3 | b3) # (a4 | b4) #
  (a5 | b5) # (a6 | b6) # (a7 | b7) # (a8 | b8) # (a9 | b9)

Here, the choice composition operator # is used to express choices between pairs of concurrent events.

The resulting Petri net contains 20 transitions a0, …, a9, b0, …, b9 and several synthesised places to enforce the choices. Note that manually designing such a Petri net (if `silent' transitions are disallowed) would be very difficult. An optimal solution has six places, e.g.:

C++-style comments are supported:

• from // to the end of the line
• enclosed in /*…*/

For Petri net models, the action names are built of English letters (case sensitive), digits, and symbols _ and ., not starting with . or a digit. Workcraft uses . symbol as the hierarchy separator, so it is a good idea not to use this symbol for anything else.

For STG models, the action names are as for Petri net models, but can optionally be postfixed with the signal edge, i.e. one of +-~ symbols.

The same action can occur multiple times within an expression – different transitions with the same label will be created in such a case.

There is also a special “silent” action $, which in STG models is translated to a dummy transition.

The operators are as follows (A and B are arbitrary expressions):

• Sequential composition A ; B or just A B
• Choice A # B
• Concurrency (a.k.a Interleaving) A | B
• Iteration { A } There are a few pitfalls when using the iteration, see below.

The binary operators ;, #, and | are given in the order of decreasing precedences, and parentheses (…) can be used to override the default precedence. All binary operators are associative; moreover, # and | are commutative.

The translation of expressions (without iteration operator) to Petri nets is described in [1][2].

The translation creates one Petri net or STG transition for each occurrence of an atomic action in the expression, i.e. if there are several occurrences of the same atomic action in the expression, a separate transition is created for each occurrence. In particular, no “silent” transitions (a.k.a. dummy transitions or ε-transitions) are created by the translation except those declared as .dummy and used in the expression or corresponding to the special $ action.

Then a set of places is synthesised to enforce the necessary sequencing and choice. Typically, a heuristic algorithm is used for synthesis (as the exact algorithm may be computationally expensive); this does not affect the correctness, but may result in more places than in the optimal solution. It is guaranteed that the resulting net is polynomial in the length of ProFlo specification, even if a heuristic synthesis algorithm is used.

There are a number of known pitfalls associated with the iteration operator. They can be solved by prefixing and/or postfixing the iteration with extra actions, i.e. making sure that iteration {A} is used in a context like …;{A};…, i.e. surrounded by sequential composition.

The tool diagnoses these kinds of pitfalls and prints a (hopefully) meaningful error message, so that an STG or Petri net with unexpected behaviour is not generated.

Consider the Petri net for {a} # b (note that the tool will actually report an error for this ProFlo specification and refuse to generate this Petri net):

Unfortunately, this Petri net has illegal traces like a b. Intuitively, the Petri net lacks a separate marking indicating that the decision has been made to execute the branch of the choice containing the iteration – in the above Petri net this marking is confused with the initial marking. If `silent' transitions were allowed, one could model this as $ {a} # b which results in the following Petri net with the expected behaviour:

Note that a similar problem can occur when iteration is nested within another iteration – the initial state of the outer iteration is effectively a choice between executing its body and skipping it, e.g. the Petri net for {{a} b} c (that the tool will refuse to generate) would allow the illegal trace a c (without b).

To work around problem, one should separate iteration from choice (or from outer iteration) with some sequencing, e.g. the following expressions avoid the problem: $ {a} # b, {$ {a} b} c.

A similar problem occurs when the end of the iteration body interacts with the merge point of a choice (or the end of the outer iteration's body). For example, consider (s {a} # b) c. The corresponding Petri net (that the tool will refuse to generate) is as follows:

Note that it allows an illegal trace b a. Similarly, the Petri net for {s {a}} (that the tool will refuse to generate) allows the illegal trace a (without s).

Another pitfall is that concurrency in the body of iteration can result in unsafe Petri net or STG. For example, consider the Petri net for {a | b} (which the tool will refuse to generate):

Note that firing either a or b transition results in an unsafe (though 2-bounded) marking. Intuitively, the reason is that traces like a b b are possible, where the transition corresponding to b can fire twice (but not more) in a row – to model this without `silent' transitions one needs two tokens on some place. As many verification and synthesis tools in Workcraft can work only with safe Petri nets or STGs, constructions like this should be avoided. If dummies are allowed, the following expression that introduces sequencing in the iteration body and results in a safe Petri net can be used instead: { $ (a | b) }.