Prise en mains | Exemples | Exos Struct | Exos LTL | Exos CTL | TP Atemporel | TP Temporel | |||||||||||
Pour permettre la vérification de propriétés spécifiques, TINA
dispose d'un model-checker pour la logique temporelle CTL (Conditional
Time Logic ou encore Computation Tree Logic). Cette logique permet
d'exprimer des propriétés caractéristiques du système que vous
modélisez et de les vérifier.
Les formules de CTL s'évaluent sur l'ensemble des
états du système (ici du graphe de marquages associé au
réseau que vous analysez).
Une formule f est vraie si elle est satisfaite par toutes
les états du système S. On le note S |= f.
Les formules de CTL contiennent les formules habituelles
du calcul propositionnel construites avec les connecteurs classiques
négation (-), conjonction (/\) disjonction (\/) et implication (=>).
En plus des connecteurs propositionnels, on trouve deux opérateurs temporels binaires utilisés en notation infixe:
|
|