State annotations

> > >

A state annotation adds state information to a location in an automaton. States consist of the current locations of automata and the 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 CIF explorer may generate CIF models with state spaces represented as automata. For the example from the lesson on synchronizing events, it may generate the following model:

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 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 reference manual.