Initialization predicates

Initialization predicates can be used to specify the allowed initial locations of automata, as well as to restrict the allowed initial values of variables and initial states in general.

Initial locations of automata

Initialization predicates can be used to specify the allowed initial locations of automata:

automaton a:
  location loc1:
    initial;

  location loc2:
    initial true;

  location loc3;

  location loc4:
    initial false;
end

Automaton a has four locations. Location loc1 has the initial keyword, and is thus allowed to be the initial location. Location loc2 also uses the initial keyword, but additionally specifies a predicate that indicates under which conditions the location may be the initial location. Since it is true, which always holds, it does not impose any additional restrictions, and can thus always be the initial location. In fact, this is identical to location loc1, which did not specify a predicate, in which case it default to true as well.

Location loc3 does not specify anything about initialization, and thus can never be the initial location. Location loc4 can only be the initial location if false holds. Since false never holds, location loc4 can never be the initial location. In fact, this is identical to location loc3, which did not specify any initialization at all, in which case it default to false as well.

Locations loc1 and loc2 are the potential initial locations, while locations loc3 and loc4 can not be chosen as initial locations of automaton a. Since an automaton can only have one current location, an initial location has to be chosen from the potential initial locations. In other words, the initial location of automaton a is either location loc1 or location loc2.

Consistency between initial locations and initial values

Consider the following CIF specification:

automaton odd_even:
  event inc, dec;
  disc int n = 5;

  location odd:
    initial;
    edge inc do n := n + 1 goto even;
    edge dec do n := n - 1 goto even;

  location even:
    edge inc do n := n + 1 goto odd;
    edge dec do n := n - 1 goto odd;
end

Automaton odd_even keeps track of a value (n) that can constantly be incremented (event inc) and decremented (event dec) by one. It has two locations, that keep track of the odd/even status of value n. Currently, the initial value is 5, which is odd. Therefore, the initial keyword is specified in the odd location. However, if we change the initial value of variable n to 6, we have to change the initial location as well, to ensure consistent initialization. To automatically keep the initial location consistent with the initial value of variable n, we can change the specification to the following:

automaton odd_even:
  event inc, dec;
  disc int n = 5;

  location odd:
    initial n mod 2 = 1; // Initial location if 'n' is odd.
    edge inc do n := n + 1 goto even;
    edge dec do n := n - 1 goto even;

  location even:
    initial n mod 2 = 0; // Initial location if 'n' is even.
    edge inc do n := n + 1 goto odd;
    edge dec do n := n - 1 goto odd;
end

In this specification, location odd can only be the initial location if the value is odd (the value modulo two is equal to one), and location even can only be the initial location if the value is even. Changing the initial value of variable n then also changes the potential initial locations. Since the value is always odd or even, and can’t be both odd and even, automaton odd_even always has exactly one potential initial location.

Restricting initialization

Initialization predicates can also be used to restrict the initial values of variables. And more generally, they restrict the possible initial states. It is for instance also possible to specify which combinations of locations of automata and values of variables are allowed as initial states.

As an example of restricting the allowed initial values of variables, consider the following CIF specification:

automaton a:
  disc int x in any;

  initial x mod 2 = 1;

  location ...
end

In this partial automaton, variable x can be initialized to any integer value, as indicated by its int type and the any keyword. However, the initialization predicate states that initially, the value of x module two must be equal to one. That is, the value of variable x must initially be odd.

It is allowed to specify initialization predicates inside automata, but it is also allowed to place them outside the automata:

automaton a:
  disc int x in any;

  location ...
end

automaton b:
  disc int x in any;

  location ...
end

initial a.x = 2 * b.x;

Here, two automata each declare a variable that can have arbitrary initial values. The initialization predicate specifies that the initial value of variable x from automaton b must be twice the initial value of variable x from automaton a.

Similarly, the initial locations of two automata can be restricted using additional initialization predicates:

automaton a:
  location a1:
    initial;
    ...

  location a2:
    initial;
    ...
end

automaton b:
  location b1:
    initial;
    ...

  location b2:
    initial;
    ...
end

initial (a.a1 and b.b1) or (a.a2 and b.b2);

The two automata, a and b, each have two potential initial locations. The initialization predicate outside the automata only allows certain combinations of initial locations of the two automata. It specifies that if automaton a starts in location a1, then automaton b must start in b1. Alternatively, if automaton a starts in location a2, then b must start in b2.

Note that locations of automata that are not indicated as being potentially initial are never initial locations. The initialization predicates outside the automata further restrict initialization, but can never make locations initial that were not already indicated as such.

This last example can however be more simply specified using only initialization predicates in locations:

automaton a:
  location a1:
    initial;
    ...

  location a2:
    initial;
    ...
end

automaton b:
  location b1:
    initial a.a1;
    ...

  location b2:
    initial a.a2;
    ...
end

The initialization for automaton a1 remains as it was before. Instead of restricting the initialization combinations of the two automata using an extra initialization predicate, these restrictions are not put in the initialization predicates of the locations of automaton b. Location b1 can only be the initial location of automaton b if automaton a is in location a1. And similarly, location b2 can only be its initial location if automaton a starts in a2.

It is generally recommended to use initialization predicates in locations, where possible. If initialization must be further restricted by an initialization predicates outside locations, it is recommended to place it inside an automaton if the condition only applies to declarations from that automaton, and to place it outside of the automata if the condition applies to declarations of multiple automata.