//////////////////////////////////////////////////////////////////////////////
// Copyright (c) 2010, 2026 Contributors to the Eclipse Foundation
//
// See the NOTICE file(s) distributed with this work for additional
// information regarding copyright ownership.
//
// This program and the accompanying materials are made available
// under the terms of the MIT License which is available at
// https://opensource.org/licenses/MIT
//
// SPDX-License-Identifier: MIT
//////////////////////////////////////////////////////////////////////////////

include::../_part_attributes.asciidoc[]

indexterm:[marking]
indexterm:[marker,predicate]

:leveloffset: -2

[[lang-tut-synthesis-marked]]
== Marker predicates

Marking is very weak form of liveness, and is used by <<lang-tut-synthesis-intro,supervisory controller synthesis>> to prevent livelocks, to ensure progress.
It is also used to prevent deadlocks.
A supervisor per definition ensures that a marked state can always be reached, for the entire system.
A system is marked if all its automata are marked.
An automaton is marked if its active location is a marked location.
In literature, marked location are also called _safe_ locations.
Note that deadlock in marked states is not prevented, as a marker state (the state itself) can be reached by not taking any transition.
In literature, marked deadlock states are also called _final_ states.

Marking can be specified using _marker predicates_.
Locations can be marked using the `marked` keyword, as follows:

[source, cif]
----
plant lamp:
  controllable c_turn_on, c_turn_off;

  location off:
    initial;
    marked;
    edge c_turn_on goto on;

  location on:
    edge c_turn_off goto off;
end
----

In this example location `off` is both initial and marked, while location `on` is neither initial nor marked.

Marker predicates are very similar to <<lang-tut-data-chapter-init-preds,initialization predicates>>, as by default, locations are not marked, similar to how by default locations are not initial.
Marker predicates can be specified in locations, automata, <<lang-tut-reuse2-chapter-groups,groups>>, and the top level of the specification (which can be seen as a group), similar to initialization predicates.

The following specification shows an example of a variable that is only marked for a certain value:

[source, cif]
----
plant counter:
  controllable c_increment, c_decrement;
  disc int[0..10] count = 0;

  marked count = 0;

  location:
    initial;
    marked;
    edge c_increment do count := count + 1;
    edge c_decrement do count := count - 1;
end
----

Variable `count` of plant automaton `counter` is only marked if it has value zero.
That is, the entire system can only be marked if `count` is zero.
Supervisor synthesis will ensure that it is always possible to get back to a state where `count` is zero.
