A complex synchronisation between modules can be more flexibly defined using protocols. A protocol keeps the agent's state variables hidden, but allows the agent to talk to the external world about the actions it performs. Let us look again at the FTC model, but with its modules synchronised by the protocols, or rather, unsynchronised, as the protocols exlude certain sets of statements from being synchronised.

The environment now talks to the trains 1 and 2 through its protocol:

    protocol {
        in1, in2 := lights == GREEN;
        out1, out2 := lights == RED;
    };

ignoring the 3rd train as usual. The way of synchronisation is realised explicitly by using guards:

    [] lights == GREEN && (${$rpt("(in$ && train$.in)", " || ", 1, .NUM - 1)}) ->
                   lights := RED;
    [] lights == RED && (${$rpt("(out$ && train$.out)", " || ", 1, .NUM - 1)}) ->
                   lights := GREEN;

As seen, there is a built-in function $rpt(String operand, String operator, Z min, Z max), which is handy if an expression of the form operand1 operator operand2 operator operand3 is needed. The function is written in the Verics language and the user can similarly define other string–processing functions as needed. In this case, the function is expanded by the preprocessor as follows:

    [] lights == GREEN && ((in1 && train1.in) || (in2 && train2.in)) ->
                   lights := RED; 
    [] lights == RED && ((out1 && train1.out) || (out2 && train2.out)) ->
                   lights := GREEN; 

The expressivity of boolean equations like that is what makes the protocols verbose, yet flexible.

Let us look into the 1st train, as expanded by the preprocessor:

agent train1 { 
    Z{WAIT, TUNNEL, AWAY} phase := AWAY;

    protocol {
        in, none := phase == WAIT;
        out, none := phase == TUNNEL;
        approach, none := phase == AWAY;
    }; 

    []  phase == AWAY && approach -> phase := WAIT;
    // the train NUM is faulty 
    []  phase == WAIT && in && environment.in1 -> phase := TUNNEL;
    []  phase == TUNNEL && out && environment.out1 -> phase := AWAY; 
}; 

We allow a none action, i.e. the train can be idle while the other parts of the system run.

Files:

• FTCp.vxs: the source of the model;
• FTCp.ispl: the resulting ISPL file.

Command line:

• veric -oi FTCp.vxs