## 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.