CFA is an abbreviation for Communicating Finite Automata. The idea of this concept is that the user can model a system and its parallel components as finite automata communicating with each other. The automata run in parallel, but each individual automaton runs sequentially. They can communicate via shared variables, channels or stacks. Channels act as FIFO buffer (First In First Out), and stacks act as LIFO buffer (Last In First Out). The buffer size can be fixed for each channel or stack individually.

In this section we will show which basic steps one has to do in order to specify a CFA correctly.

• At the beginning of the file one special keyword is expected:
  CFA

• Then global variables, channels and stacks can be defined. The definitions must have the following form (keywords are set in boldface):
  @global
var x:{0..5} init 0;
var ch: chan 1 of {0..5};
var st: stack 3 of {1..4};

  First we have defined a global variable x whose values range from 0 to 5. The initial value of x is set to 0. Setting an initial value is optional and can be omitted (in which case the variabe will be initialized to a random value in its domain). ch is a channel of capacity 1 and can contain values ranging from 0 to 5, and st is a stack of capacity 3 whose values range from 1 to 4. The capacity of a channel or stack determines how many values can be held by them at the same time.

  Automata can communicate via global variables, channels and stacks.

• At this point we can define the automaton:

  • First you have to type the line:
    @automaton auto1

    where @automaton is a keyword and auto1 is an arbitrary name for the automaton.

  • Now you can specify the behaviour of the automaton:
    • Defining the initial state of the automaton:
      A1 {@start}.

      where @start is a keyword and A1 is an identifier for the state.

    • Labelling states:
      A2 {@label "incs1"}.

      This line means that the state A2 is labelled with incs1. Labels do not have to be unique, and therefore two states can take the same label. Setting labels is useful for increasing the readability of a program. Moreover, labels can be used in formulae as atomic propositions.

    • Transitions from one state to another have the following form:
      A3 [pred] A4

      where A3 and A4 are state identifiers, and pred is a predicate (see below). A transition can be executed if there exists a binding for the variables that makes the predicate true.

• Now we describe how the predicate pred mentioned above looks like.
  • 'x=1
    This means that this transition can be executed if the variable x is set to 1 before the execution of this transition ('x is also referred to as the pre-value of x). We do not know anything about the value of x after execution of this transition. Maybe the value has been changed.
  • x'=1
    This means that the variable x is set to 1 after execution of this transition (x' is the post-value of x). In traditional programming languages, this would correspond to a value assignment x:=1.
  • x=1
    This means that the transition can be executed if the variable x has the value 1 before the execution of this transition. It corresponds to x==1 (test of equality) in C. The value of x will not be changed.
  • x'=ch?
    This means that the variable x reads a value from the channel ch if the channel is not empty. The value is deleted from the channel.
  • x=ch!
    This means that the variable x writes a value to the channel ch if the capacity value allows it.
  • ch??
    This expression is true if the channel ch is empty.
  • ch!!
    This expression is true if the channel ch is at full capacity.
  • You can join the notations mentioned above with logical operators, for example:
    x=2 & y'=1 (Conjunction)
    x=1 | y=3 (Disjunction)
    
  • The notation for stacks is the same as for channels. The only difference between stacks and channels is that stacks act as LIFO buffers and channels as FIFO buffers.

An example for a CFA specification can be seen here.

Atomic propositions in formulae

Atomic propositions can consist of ...

• State identifiers
  A state identifier can be an atomic proposition, for example A1, A2, A3.
• Labels of states
  One can use the label of a state as atomic proposition, for example "incs1".

• Expressions
  of the form "x=val", "x#val", "x<val", "x>val", "x>=val", "x<=val" (# denotes inequality).
  For a channel ch or a stack st one can type, e.g., "c[1]=val", "st[2]=val", "st[3]=val", .... The number in square brackets denotes the buffer position of the channel or the stack. It must not be greater than the capacity value defined for them.

Labels and expressions must be typed in quotes.