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.