Changes from Fiacre V2 to Fiacre V3

Shared variables

Shared variables may be read in any statement in a process (including init statements and those performing communications).

Example (assuming v1 and v2 are shared variables):

   from S
      if v2 > v1 then V1 := V2 else p!V1 end;
      to S'

As of frac-1.4.0, shared variables may be written in any statement (including those performing communications) except init statements. frac checks absence of write conflicts on shared variables at compile time.

Guarded commands

The on statement, made of keyword on followed by a boolean expression, is a derived notation for guarded commands. A computation path may include any number of "on" statements, at any place.

Semantically, the following statements are equivalent:

	      
   on e; s
   case e of true -> s end
   true := e; s

loop statements

In a transition from state s, the statement (to s) may be replaced by loop. In untimed transitions, these two statements behave identically. In timed transition, (to s) resets the clocks of all enabled interactions rooted at state s, while loop does not. Example:

	      
   from S
      if e then p!4; to S' else x := 3; loop end

wait statements

Process transitions may include wait statements, made of keyword wait followed by a time interval (with the same syntax as time intervals in local port declarations in components).

Only one wait statement may appear on any computation path of a transition, and only in silent paths (not using any port).

Example:

   from s
      if e then x := 0; wait [3,4[ else p!56 end;
      to s'

unless clauses in select statements

In a select statement, the separator "[]" may be replaced by unless. unless clauses specify priorities between groups of alternants of a select statement. Only one select statement with unless clause may appear on any computation path of a transition. All statements under unless must be silent (may not use any port).

Example:

   from s
      select s1
      []	    s2
      unless s3
      []	    s4
      unless s5
      end;
      to s'

In this example, statement s5 has priority over s1 to s4 and statements s3 and s4 have priority over s1 and s2.

Constraints on priorities

In a priority specification "a1 | ... | an > b1 | ... | bm" ports ai must be locally defined in the component or of profile closed. This restriction is essential for maintaining compositionality of fiacre components.

frac also checks that the priority relation is cycle-free.

Syntax revisions

Access expressions (a[x] or a.f) are now considered atomic expressions. As a consequence, the following expresions, for instance, are grammatically correct:

   not a[3]          instead of        not (a[3])
   S (X r.f.[2])     instead of        S (X (r.f.[2]))

length primitive for queues

A length primitive is added for queues.

Native fiacre functions: (as of frac-1.6.0)

As of frac-1.6.0, fiacre supports functions. Functions come in two forms: native (defined in fiacre) or extern (defined in C with their profile declared in fiacre).

The native Fiacre functions reuse most of the control structures of processes, but with a "functional" semantics (e.g. "case" dynamically fails if no pattern matches). Fiacre functions do not allow side-effects (no shared variables as arguments). Fiacre functions may be recursive.

The following example defines a "reorder" function taking a queue as argument and returning the queue in which the urgent elements occur first:

   type msg is p1 | p2 of int | p3 of 0..4 end

   function urgent (m : msg) : bool is return m=p1

   type mbuff is queue 7 of msg

   function reorder (q: mbuff) : mbuff is
      var u: mbuff := {||}, n: mbuff := {||}, h: msg
      begin
         while not (empty q) do
	    h := first q;
	    q := dequeue q;
            if urgent h then
	       u := enqueue (u,h)
	    else
               n := enqueue (n,h)
	    end
         end;
         while not (empty n) do
	    u := enqueue (u,first n);
	    n := dequeue n
         end;
      return u
      end

If the body resumes to a return statement then the enclosing begin and end may be omitted.

Properties declarations and assert directives

As of frac-1.7.0, fiacre descriptions may include property declarations and assert directives. These features do not belong to the Fiacre language but are features of the frac compiler easying expression of correctness requirements and verification. The language of properties is described in a separate properties page.