//////////////////////////////////////////////////////////////////////////////
// Copyright (c) 2023, 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[]

:leveloffset: -2

[[lang-tut-annotations-state]]
== State annotations

A state <<lang-tut-annotations,annotation>> adds <<lang-tut-basics-chapter-synchronizing-events-statespace,state>> information to a location in an automaton.
States consist of the <<lang-tut-basics-chapter-synchronizing-events-statespace,current locations of automata>> and the <<lang-tut-data-chapter-discrete-variables-state-space,current values of variables>>.
The typical use of state annotations is for generated models that contain an automaton representing a state space of another model, where each location of that automaton represents a state of the state space.
For instance, the <<tools-chapter-cif-explorer,CIF explorer>> may <<tools-chapter-cif-explorer-output-cif,generate CIF models>> with state spaces represented as automata.
For the example from the lesson on <<lang-tut-basics-chapter-synchronizing-events,synchronizing events>>, it may generate the following model:

[source, cif]
----
group producer:
  event produce;
  event provide;
end

group consumer:
  event consume;
end

automaton statespace:
  alphabet producer.produce, producer.provide, consumer.consume;

  @state(consumer: "idle", producer: "producing")
  location loc1:
    initial;
    edge producer.produce goto loc2;

  @state(consumer: "idle", producer: "idle")
  location loc2:
    edge producer.provide goto loc3;

  @state(consumer: "consuming", producer: "producing")
  location loc3:
    edge producer.produce goto loc4;
    edge consumer.consume goto loc1;

  @state(consumer: "consuming", producer: "idle")
  location loc4:
    edge consumer.consume goto loc2;
end
----

This state space consists of four states, each represented by a location of the `statespace` automaton.
For instance, the first state is represented by location `loc1`, which corresponds to the state where the `consumer` is `idle` and the `producer` is `producing`.

A location may have multiple state annotations in case it represents multiple states.
For instance, the <<tools-eventbased-chapter-dfa-minimization,event-based DFA minimization>> tool may merge locations representing different states to a single location representing multiple states.

For more detailed information on state annotations, see the <<lang-ref-annotations-state,reference manual>>.
