Aller au contenu

Sémantique d'exécution

Toute la sémantique est dans Internal.StateLogic (états) et Transition.

Activité d'un état

active = pre(newActive);
reenter = anySet and anyReset;
newActive = initialState and initial()
            or pre(reenter)
            or anySet and not anyReset
            or active and not anyReset;
  • anySet / anyReset : une transition entrante / sortante franchit, sur l'un quelconque des quatre côtés.
  • pre() coupe la boucle état → transition → état : une décision prise à une itération d'événement n'est visible qu'à l'itération suivante.
  • Auto-transition (set et reset vrais ensemble) : l'état devient inactif à l'itération suivante (exit), puis actif à celle d'après grâce à pre(reenter) (entry), au même instant. Faire la ré-entrée dans la même itération créerait une boucle algébrique entre entryTime et la condition after() des transitions sortantes (rencontrée puis corrigée).

État initial

initial equation pre(newActive) = false; : tous les états sont inactifs pendant l'initialisation. Pour le pseudo-état initial, newActive vaut true pendant l'initialisation (terme initialState and initial()) ; à la première itération d'événement qui suit, au temps de départ, active = pre(newActive) devient vrai, puis sa transition de complétion franchit.

Raison : une clause when n'est pas évaluée pendant l'initialisation. Si un état était actif dès l'initialisation, when active ne se déclencherait pas pour lui : pas de entryTime, pas de entryCount, pas d'impulsion entry. Vérifié sous omc 1.27.1 et 1.24.4 (verify_01 : cycles = 1 dès t = 0).

Entrées, sorties, impulsions

when active then entryTime = time; entryCount = pre(entryCount) + 1; end when;
when not active then exitTime = time; exitCount = pre(exitCount) + 1; end when;
// State :
entry = if pulseDuration > 0 then entryCount > 0 and time < entryTime + pulseDuration
        else change(entryCount);

Une impulsion de durée finie est une relation sur time : le solveur place un événement à sa fin. Avec pulseDuration = 0, change() n'est vrai qu'à l'itération où le compteur change. Même principe pour exit et pour l'effect d'une transition (fireTime, fireCount).

Priorités

Internal.availability(active, enabled, priority) : la transition k est disponible si l'état est actif et qu'aucune autre transition j n'est franchissable (enabled[j]) avec un numéro de priorité plus petit, ou égal et un indice plus petit (ordre des côtés haut, droite, bas, gauche, puis indice). enabled ne dépend que du déclencheur et de la garde, jamais de available : pas de boucle algébrique. Une extrémité cible envoie enabled = false et ne bloque donc rien.

Franchissement d'une transition

triggered = edge(localSignal)                                // Signal
          | source.active and time >= source.entryTime + delay  // After
          | edge(changeValue)                               // When
          | true;                                           // Completion
enabled = triggered and localGuard;
fire = source.available and enabled;
source.reset = fire;  target.set = fire;
  • Signal et When sont des événements : edge() n'est vrai qu'à la première itération de l'instant où le signal ou l'expression devient vrai. Si l'état source n'est pas disponible à cette itération, ou si la garde est fausse, l'événement est perdu. initial equation pre(x) = x : pas d'événement au démarrage, même si l'expression est vraie à t = 0.
  • After mesure le temps depuis source.entryTime (remis à jour à chaque entrée, y compris par une auto-transition). La relation time >= entryTime + delay est localisée par le solveur. Le déclencheur reste vrai après le délai : une garde qui devient vraie ensuite fait franchir.
  • Completion : franchit dès que l'état source est disponible et la garde vraie, y compris plus tard si la garde le devient (écart assumé avec SysML strict, cf. requirements.md).
  • La garde vient de l'input Boolean guard (modificateur, comme Modelica.StateGraph.Transition.condition) ou de l'entrée conditionnelle guardPort.

Déroulé d'un franchissement

À l'instant t où la transition A → B devient franchissable :

  1. itération 1 : A.available et enabled vrais → fire ; A.newActive = false, B.newActive = true ;
  2. itération 2 : A.active = false (exit de A), B.active = true (entry de B, entryTime de B = t) ; si une transition sortante de B est déjà franchissable (complétion avec garde vraie, cas du Choice), elle franchit à son tour (itération 3…).

Les enchaînements à un même instant se font donc par itération d'événements. Une boucle de transitions toujours franchissables ne converge pas : le solveur s'arrête sur le nombre maximal d'itérations d'événements (cf. Limites).