Example |

Here is an example of an AUTOC automaton specification, corresponding to the scheduler of [6].

-- channels are first declared channel I1(); channel I2(); channel start(); -- used to simulate an initial transition process I { -- Models a non-deterministic environment sync I1,I2,start; -- set of channels on which the process synchronizes var c1,c2 : real; -- set of variables of the process init pc=linit; -- initial condition, using the implictly declared -- pc variable, of enumerated type loc linit: continuous blocked; -- time is not allowed to elapse here when c1>=0 and c2>=0 sync start() goto l; -- guarded transition with synchronization loc l: continuous c1=1 and c2=1; -- defines the derivatives of c1 and c2 to be equal to 1 when c1>=10 sync I1() goto l assign { c1 := 0 }; when c2>=20 sync I2() goto l assign { c2 := 0 }; } process T { -- The scheduler itself sync E1, E2, I1, I2, start; var x1,x2 : real; k1,k2 : int; init pc=linit; loc linit: continuous blocked; when x1=0 and x2=0 and k1=0 and k2=0 sync start() goto Idle; loc Idle: continuous x1=0 and x2=0; when true sync I1() goto Task1 assign { k1:=1 }; when true sync I2() goto Task2 assign { k2:=1 }; loc Task1: continuous if x1<=4 then x1=1 and x2=0 else blocked; -- The guard "x1<=4" is here the ``invariant'' of the location. -- If it is not satisfied, the time is blocked. when x1<4 sync I1() goto Task1 assign { k1 := k1 + 1 }; when x1<4 sync I2() goto Task2 assign { k2 := 1 }; when x1=4 and k1<=1 goto Idle assign { k1 := k1-1; x1 := 0 }; when x1=4 and k1>=2 goto Task1 assign { k1 := k1-1; x1 := 0 }; loc Task2: continuous if x2<=8 then x1=0 and x2=1 else blocked; when x2<8 sync I1() goto Task2 assign { k1 := k1 + 1 }; when x2<8 sync I2() goto Task2 assign { k2 := k2 + 1 }; when x2=8 and k2<=1 and k1=0 goto Idle assign { k2 := k2-1; x2 := 0 }; when x2=8 and k2<=1 and k1>=1 goto Task1 assign { k2 := k2-1; x2 := 0 }; when x2=8 and k2>=2 goto Task2 assign { k2 := k2-1; x2 := 0 }; } system I,T; -- Specifies the set of processes in the system explicit T; -- Specifies the processes to be composed explicitly #pragma final "not (I.pc=I.linit) and T.k2>=2" -- pragma clause, to be transmitted unmodified

Assuming the previous file is named `scheduler.autc`, the command `autoc2auto scheduler.autc scheduler.aut`

or simply `autoc2auto scheduler.autc`

produces the following file `scheduler.aut`:

type I.pc_t = enum { I.linit, I.l }; type T.pc_t = enum { T.linit, T.Idle, T.Task1, T.Task2 }; channel I1(); channel I2(); channel start(); channel T.tau(); -- for internal transitions of T system (I,T) (T) { -- The pair "(I,T)" allows to interpret transition degrees (see below) -- "(T)" means that only T is explicit in the product, and allows to interpret location names sync I1, I2, start; var I.c1 : real; I.c2 : real; I.pc : I.pc_t; T.pc : T.pc_t; T.x1 : real; T.x2 : real; T.k1 : int; T.k2 : int; init I.pc = I.linit and T.pc = T.linit; loc (linit): continuous blocked; (0,0): -- Transition degree: this transition is the composition of -- the first transition of I starting from linit and synchronized on start -- with the first transition of T starting from linit synchronized on start when I.pc = I.linit and I.c1 >= 0 and I.c2 >= 0 and T.x1 = 0 and T.x2 = 0 and T.k1 = 0 and T.k2 = 0 sync start() goto (Idle) assign { I.pc := if I.pc = I.linit and I.c1 >= 0 and I.c2 >= 0 then I.l else I.pc }; loc (Idle): continuous (if (I.pc = I.linit) then blocked else if (I.pc = I.l) then I.c1 = 1 and I.c2 = 1 else blocked) and T.x1 = 0 and T.x2 = 0; (0,0): when I.pc = I.l and I.c1 - 10 >= 0 sync I1() goto (Task1) assign { I.c1 := if I.pc = I.l and I.c1 - 10 >= 0 then 0 else I.c1; I.pc := if I.pc = I.l and I.c1 - 10 >= 0 then I.l else I.pc; T.k1 := 1 }; (0,0): when I.pc = I.l and I.c2 - 20 >= 0 sync I2() goto (Task2) assign { I.c2 := if I.pc = I.l and I.c2 - 20 >= 0 then 0 else I.c2; I.pc := if I.pc = I.l and I.c2 - 20 >= 0 then I.l else I.pc; T.k2 := 1 }; loc (Task1): continuous (if (I.pc = I.linit) then blocked else if (I.pc = I.l) then I.c1 = 1 and I.c2 = 1 else blocked) and (if (4 - T.x1 >= 0) then T.x1 = 1 and T.x2 = 0 else blocked); (0,0): when I.pc = I.l and I.c1 - 10 >= 0 and 4 - T.x1 > 0 sync I1() goto (Task1) assign { I.c1 := if I.pc = I.l and I.c1 - 10 >= 0 then 0 else I.c1; I.pc := if I.pc = I.l and I.c1 - 10 >= 0 then I.l else I.pc; T.k1 := T.k1 + 1 }; (0,0): when I.pc = I.l and I.c2 - 20 >= 0 and 4 - T.x1 > 0 sync I2() goto (Task2) assign { I.c2 := if I.pc = I.l and I.c2 - 20 >= 0 then 0 else I.c2; I.pc := if I.pc = I.l and I.c2 - 20 >= 0 then I.l else I.pc; T.k2 := 1 }; (0,0): when T.x1 = 4 and 1 - T.k1 >= 0 sync T.tau() goto (Idle) assign { T.x1 := 0; T.k1 := T.k1 - 1 }; (0,1): when T.x1 = 4 and T.k1 - 2 >= 0 sync T?tau() goto (Task1) assign { T.x1 := 0; T.k1 := T.k1 - 1 }; loc (Task2): continuous (if (I.pc = I.linit) then blocked else if (I.pc = I.l) then I.c1 = 1 and I.c2 = 1 else blocked) and (if (8 - T.x2 >= 0) then T.x1 = 0 and T.x2 = 1 else blocked); (0,0): when I.pc = I.l and I.c1 - 10 >= 0 and 8 - T.x2 > 0 sync I1() goto (Task2) assign { I.c1 := if I.pc = I.l and I.c1 - 10 >= 0 then 0 else I.c1; I.pc := if I.pc = I.l and I.c1 - 10 >= 0 then I.l else I.pc; T.k1 := T.k1 + 1 }; (0,0): when I.pc = I.l and I.c2 - 20 >= 0 and 8 - T.x2 > 0 sync I2() goto (Task2) assign { I.c2 := if I.pc = I.l and I.c2 - 20 >= 0 then 0 else I.c2; I.pc := if I.pc = I.l and I.c2 - 20 >= 0 then I.l else I.pc; T.k2 := T.k2 + 1 }; (0,0): when T.x2 = 8 and 1 - T.k2 >= 0 and T.k1 = 0 sync T.tau() goto (Idle) assign { T.x2 := 0; T.k2 := T.k2 - 1 }; (0,1): when T.x2 = 8 and 1 - T.k2 >= 0 and T.k1 - 1 >= 0 sync T.tau() goto (Task1) assign { T.x2 := 0; T.k2 := T.k2 - 1 }; (0,2): when T.x2 = 8 and T.k2 - 2 >= 0 sync T.tau() goto (Task2) assign { T.x2 := 0; T.k2 := T.k2 - 1 }; } #pragma final "not (I.pc=I.linit) and T.k2>=2" -- pragma clause, to be transmitted unmodified

A few explanations about how AUTOC2AUTO works:

- it introduces enumerated types for program counter variables, with the naming scheme
`P.pc_t`. - it possibly makes explicit the internal channel of each process (if there are internal transitions), with the naming scheme
`P.tau`; - it introduces new names for communication parameters;
- it labels the transitions of each process with a "degree", which is just an integer, the purpose of which is to resolve explicit non-determinism of transitions. For each location and each synchronization channel, the degree allows to distinguish the different transitions starting from this location and synchronized on the channel. This notion of degree can be useful for automatic tools, and is needed for the translation to NBAC which accepts only deterministic systems (with inputs).
- The product is then performed: locations of the result are
the product of the explicitly composed process (
`explicit`declaration in AUTOC format). The state and behaviour of other processes are encoded with their "pc" variables.

When one specifies a system directly with the AUTO format, degrees may be omitted.

Assuming the previous file is named `scheduler.aut`, the command `auto2nbac scheduler.aut scheduler.ba`

or simply `auto2nbac scheduler.aut`

produces the file `scheduler.ba`. We
display only parts of it:

typedef I.pc_t = enum { I.linit, I.l }; T.pc_t = enum { T.linit, T.Idle, T.Task1, T.Task2 }; channel_t = enum { I1, I2, start, T.tau }; -- type of the "channel" variable state I.c1 : real; I.c2 : real; I.pc : I.pc_t; T.pc : T.pc_t; T.x1 : real; T.x2 : real; T.k1 : int; T.k2 : int; input channel : channel_t; -- used to encode synchronization channel aux0 : uint[0]; -- used to encode the degree of process I aux1 : uint[2]; -- used to encode the degree of process T ... initial I.pc = I.linit and T.pc = T.linit; space true; final not I.pc = pc.linit and T.k1 - 3 >= 0; -- Content of the "final" pragma in Auto file automaton -- initial control structure: the one defined by the Auto system location Task2_ : T.pc = T.Task2; -- definition of the location (a state formula) location Task1_ : T.pc = T.Task1; location Idle_ : T.pc = T.Idle; location linit_ : T.pc = T.linit; edge (Task2_,Task2_) : channel = T.tau and T.x2 = 8 and T.k2 - 2 >= 0 and aux0 = uint[0](0) and aux1 = uint[2](2) or channel = I2 and I.pc = I.l and I.c2 - 20 >= 0 and 8 - T.x2 > 0 and aux0 = uint[0](0) and aux1 = uint[2](0) or channel = I1 and I.pc = I.l and I.c1 - 10 >= 0 and 8 - T.x2 > 0 and aux0 = uint[0](0) and aux1 = uint[2](0) -- first condition: necessary condition for a discrete transition to be fired , true -- second condition: necessary condition for a continuous transition to be fired ; edge (Task2_,Task1_) : ...

Let us perform a reachability analysis, trying to prove the property (that the final condition is not reachable) and outputting the set of reachable state to `scheduler.aut.ba`: `nbacg.opt -analysis 0 +success +valid -o scheduler.aut.ba
scheduler.ba`

and then annotate the result on the initial AUTO automaton by generating `scheduler.aut.aut` as follows: `nbac2auto -bdd scheduler.aut scheduler.aut.ba scheduler.aut.aut`

We get this, that we may display with DOT by typing `auto2dot scheduler.aut.aut scheduler.dot` `dot -Tps scheduler.dot >scheduler.ps`

and we obtain this file.

Bertrand Jeannet, February 10, 2011

Example |