ByMC Specification Syntax

TACO mainly works on .ta or .eta files, which are very close to the actual threshold automata model. You can find a full formal definition of the accepted syntax in the parser crate of TACO.

This section will give you an introduction to the format by encoding the threshold automaton depicted in Figure 2. If you want to find out more about the purpose of the individual components you can refer to the Theoretical Background section.

Skeleton¶

Every threshold automaton starts with an outer skeleton block which begins with ta (or skel or thresholdAutomaton) followed by the name of the threshold automaton.

For example, if we want to encode Figure 2 and name it SRB, we would start by using:

// Outer Skeleton of the threshold automaton named `SRB`. ta SRB { ... }

Declaration of Shared Variables¶

Next, we need to declare the components of the threshold automaton, starting with the shared variables. In this case, our threshold automaton has two nsnt and rec, which are declared using:

// shared variable declaration shared nsnt, rec;

Declaration of Parameters¶

Afterward, we can declare the parameters of the threshold automaton similarly:

// parameter declaration parameters n, t, f;

(Optional) Declaration of Macros¶

Even though not included in the official grammar, ByMC and many of the benchmarks written for ByMC use macros for frequently used expressions. They can be defined inside a define block:

define THRESH_0 == n - f; define THRESH_1 == t + 1 - f;

Instead of writing n - f or t + 1 - f in the specification file, you can now use THRESH_0 or THRESH_1 respectively.

Assumptions / Resilience Condition¶

After the parameters have been declared, we need to specify the resilience conditions ( $RC$ in the formal definitions see).

In this case, we have the resilience conditions

n > 3 \cdot t \\ t \geq f \\ f \geq 0

(1)

which are translated into individual statements separated by a ;:

// Encoding of resilience conditions assumptions (3) { n > 3 * t; t >= f; f >= 0; }

Declaring Locations¶

After the shared variables and parameters, as well as the resilience conditions have been defined, we still have to declare the locations exist, which is done in a locations block.

// Declaration of locations of the threshold automaton locations (5) { V0: [0]; V1: [1]; RV0: [2]; SE: [3]; AC: [4]; }

Note that TACO does neither use the number of locations (i.e., the n in locations (n) {) nor the indices of locations (i.e., the numbers in the [] brackets). You could also just write 0 for TACO. However, we decided to keep them to maintain compatibility with ByMC.

Initial Conditions¶

The inits block in a .ta file has two main purposes:

it declares the initial conditions on variables, and
it declares which locations are initial

Initial Variable Conditions¶

The initial variable conditions define with what values the variables start. In most cases, we do assume that initially the variables are set to 0, which is achieved for a variable nsnt by specifying

nsnt == 0;

Initial Location Constraints¶

The inits block also allows you to define which locations of a threshold automaton can be initial. When using the name of a location in the inits block, you refer to the number of processes that are allowed in that initial state.

Additionally, the inits block also defines the relation between the parameters and the processes, which we model explicitly. A threshold automaton only models the correct processes explicitly (see Theoretical Background). In our case, the number of correct processes is given by $n - f$ , and we now want these $n - f$ processes to start in one of the initial states.

Since the initial states in Figure 2 are V1 and V0 we can achieve this with the constraint:

V1 + V0 == n - f; /* n-f correct processes in initial states */

or using the previously defined macro:

V1 + V0 == THRESH_0; /* n-f correct processes in initial states */

Additionally, you have to define that all other locations, for example AC, cannot have any process starting in it, by writing:

// No process is in location `AC` AC == 0;

The Full `inits` Block¶

For Figure 2, the full inits block is then given by:

inits(6) { nsnt == 0; rec == 0; RV0 == 0; SE == 0; AC == 0; V1 + V0 == THRESH_0; /* n-f correct processes in initial states */ }

Defining Rules¶

Next, we have to define how processes can move from one location to the other, i.e., we need to declare the rules of the threshold automaton. This is done inside a rules block.

Example Rule¶

Let’s, for example, define the rule from location SE to V1 with the guard

(rec \geq n - f) \wedge (nsnt > t + 1 - f)

(2)

that resets the variables rec and nsnt. In a .ta file we first have to give the rule a unique id (lets say 6) then the rule is specified as:

6: SE -> V1 when ((rec >= n - f) && (nsnt > t + 1 - f)) do { rec' := 0; nsnt' := 0; };

where when contains the rule guard and do specifies the update. Note that the variable to be updated has an additional ' and we use the assignment operator :=.

Alternatively, the rule can be specified with the previously defined macros:

6: SE -> V1 when ((rec >= THRESH_0) && (nsnt > THRESH_1)) do { rec' := 0; nsnt' := 0; };

To specify an update like an increment, you can also refer to the old variable value in the condition after the assignment. For example:

rec' := rec + 1;

specifies an increment of variable rec by one. You can find an encoding of all the rules of Figure 2 in section Full Specification.

Correctness Property¶

After having specified the full automaton, we also have to specify its correctness properties. This is done inside a specifications block. To specify a property validity in $ELTL_{FT}$ of the form

(V1 == 0) \Rightarrow \square( AC == 0)

(3)

we simply write:

validity: V1 == 0 -> [](AC == 0);

Full Specification¶

If we put everything together, we get the full encoding of Figure 2 as:

1ta SRB {

2 shared nsnt, rec;

4 parameters n, t, f;

6 define THRESH_0 == n - f;

7 define THRESH_1 == t + 1 - f;

9 assumptions (3) {

10 n > 3 * t;

11 t >= f;

12 f >= 0;

13 }

15 locations (5) {

16 V0: [0];

17 V1: [1];

18 RV0: [2];

19 SE: [3];

20 AC: [4];

21 }

23 inits(6) {

24 nsnt == 0;

25 rec == 0;

26 RV0 == 0;

27 SE == 0;

28 AC == 0;

29 V1 + V0 == THRESH_0; /* n-f correct processes in initial states */

30 }

32 rules (8) {

33 0: V0 -> RV0

34 when (true)

35 do { rec' := rec + 1; };

36 1: V1 -> SE

37 when (true)

38 do { nsnt' := nsnt + 1; rec' := rec + 1; };

39 2: RV0 -> SE

40 when (nsnt >= THRESH_1)

41 do {};

42 3: SE -> AC

43 when (nsnt >= n - t - f)

44 do {};

45 4: RV0 -> V0

46 /* when ((rec >= n - f) && (nsnt > t + 1 - f)) */

47 when ((rec >= THRESH_0) && (nsnt > THRESH_1))

48 do {};

49 5: RV0 -> V0

50 when (rec == 0)

51 do {};

52 6: SE -> V1

53 /* when ((rec >= n - f) && (nsnt > t + 1 - f)) */

54 when ((rec >= THRESH_0) && (nsnt > THRESH_1))

55 do { rec' := 0; nsnt' := 0; };

56 7: SE -> V1

57 when (rec == 0)

58 do {};

59 }

61 specifications (1) {

62 validity: V1 == 0 -> [](AC == 0);

63 }

64}

Full ByMC specification for threshold automaton depicted in Figure 2

Skeleton¶

Declaration of Shared Variables¶

Declaration of Parameters¶

(Optional) Declaration of Macros¶

Assumptions / Resilience Condition¶

Declaring Locations¶

Initial Conditions¶

Initial Variable Conditions¶

Initial Location Constraints¶

The Full inits Block¶

Defining Rules¶

Example Rule¶

Correctness Property¶

Full Specification¶

The Full `inits` Block¶