The Description of The Input File

The fault-intolerant agreement program consists of four non-general processes i, j, k, l and a general g. Each non-general process has four variables d, f, b, and up. Variable di represents the decision of a non-general process i, fi denotes whether i has finalized its decision, bi denotes whether i is Byzantine or not, and upi states whether i has failed or not. Process g also has variables dg and bg. We assume that the process g never fails. Thus, the variables of the agreement program are as shown in the var section (cf. lines 2-23). Transitions of the fault-intolerant program. If process i has not copied a value from the general and i has not failed (i.e., upi = 1) then i copies the decision of the general (first action in the body of process i (cf. line 28)). If i has copied a decision and as a result di is different from -1 then i can finalize its decision if it has not failed (second action in the body of process i (cf. line 30)). Other non-general processes (j, k, and l) have a similar structure as shown in the input file (cf. lines 37-67). Read/Write restrictions. Each non-general process i is allowed to read the following set of variables: $\{ di, dj, dk, dl, dg, fi, upi, bi \}$. Thus, i can read the d values of other processes and all its variables. The set of variables that i can write is $\{ di, fi \}$. Read/write restrictions of each process are specified in its body after the program actions (using read and write keywords (e.g., lines 32-33)). Faults. A Byzantine fault transition can cause a process to become Byzantine if no process is initially Byzantine. A Byzantine process can arbitrarily change its decision (i.e., the value of d). Moreover, the program is subject to failstop faults such that at most one of the non-general processes can be failed, and as a result, it will stop executing any action. The developers of fault-tolerance should specify the faults similar to an independent process that can perturb program variables (cf. lines 71-86). Invariant. The users of our framework should represent the invariant of the program as a state predicate. In particular, the invariant is a Boolean function (over program variables) that takes a state s and identifies whether s is an invariant state or not. In the agreement program, the bg variable partitions the invariant into two parts: the set of states s₁ where g is non-Byzantine (cf. line 91), and the set of states s₂ where g is Byzantine (cf. line 106). When g is non-Byzantine, at most one of the non-generals could be Byzantine (cf. lines 92-96). Also, for every non-general process i that is non-Byzantine (i) i has not yet decided or it has copied the value of dg (cf. lines 97-100), and (ii) i has not yet finalized or i has decided (cf. lines 101-104). When g becomes Byzantine, all the non-general processes are non-Byzantine and all the processes that have not failed agree on the same decision (cf. lines 106-116). The invariant of the agreement program stipulates the above conditions on the states in which at most one non-general process has failed (cf. lines 121-125). Safety specification. The safety specification requires that if g is Byzantine, all the non-general non-Byzantine processes that have not failed should finalize with the same decision (agreement). If g is not Byzantine, then the decision of every finalized non-general non-Byzantine process should be the same as dg (validity). Thus, safety is violated if the program executes a transition that satisfies at least one of the conditions specified in the specification section of the input file (cf. lines 129-168). When g is not Byzantine, at most one of the non-general processes is Byzantine. In this case, the program should satisfy its validity requirement; i.e., all the non-Byzantine processes finalize with the same decision as dg. If g is Byzantine then the program should satisfy its agreement requirement; i.e., all the non-general non-Byzantine processes, that are not failed, finalize with the same decision. The specification section is divided into three parts: source, destination, and relation parts. Intuitively, in the source part (cf. line 133), we specify a condition that identifies a set of states s_source, where if a transition t originates at s_source then t violates the safety of the specification. In the destination part (cf. lines 137-156), we write a state predicate that identifies a set of states s_destination, where if a transition t reaches s_destination then t violates safety. In the relation part (cf. lines 160-168), we specify a condition that identifies a set of transitions that should not be executed by the program. Note, that we have added a suffix ``s" (respectively, suffix ``d") to the variable names in the specification section that stands for source (respectively, destination). Since the relation condition specifies a set of transitions t_spec using their source and destination states, we need to distinguish between the value of a specific variable x in the source state of t_spec (i.e., xs means the value of x in the source state of t_spec) and in the destination state of t_spec (i.e., xd means the value of x in the destination state of t_spec). In the case that the program specification does not stipulate any source condition on safety-violating transitions, we leave the source section empty with the keyword noSource (cf. line 133). (We use similar keywords noDestination and noRelation for the cases where we do not have destination or relation conditions in the specification, respectively.) Initial states. The keyword init (cf. line 172) identifies the section of the input file where the user has to specify some initial states. These initial states should belong to the invariant. For each initial state, the user should use the reserved word state (cf. line 176). In the state section (cf. lines 176-178 and 181-183), the user should assign some values to the program variables that belong to their corresponding domain.