Class GFI_Datas

java.lang.Object
  GFI_Datas

Direct Known Subclasses:

GFI_Parseur

public class GFI_Datas
extends java.lang.Object

Cette classe définie une structure de données pour la mise en mémoire des traces avec les méthodes KiVontBien pour sauvegarder ou lire les données depuis un fichier.

Version:

20/01/2004

Author:

Nicolas Stouls en Janvier 2004

Nested Class Summary

class

GFI_Datas.QuadrupletEntiers Sous classe permettant le stockage de données dans des vecteurs ou tableaux

Field Summary

GFI_Datas.QuadrupletEntiers[][][]	AttConnues Tableau décrivant l'ensemble des atteignabilités connues.
static int	Atteignable Constante utilisée lors de la construction inductive des différentes transitions.
static int	AvecG Constante définissant une condition Gardée
GFI_Datas.QuadrupletEntiers[][]	DeclConnues Tableau décrivant l'ensemble des déclenchabilités connues.
static int	Declenchable Constante utilisée lors de la construction inductive des différentes transitions.
static int	DejaEtudie Constante utilisée lors de la construction inductive des différentes transitions.
GFI_Datas.QuadrupletEntiers[]	EquivEtatsConnues Tableau décrivant l'ensemble des équivalences d'états connues.
int[]	EtatsEtudies Taleau Permettant de mémoriser les états ayant déjà été visités lors de la construction inductive des différentes transitions.
GFI_Datas.QuadrupletEntiers[]	EtatsInitiaux Tableau décrivant l'ensemble des états initiaux.
static int	FormatDot Definition des constantes correspondant aux formats
static int	FormatGxl
static int	FormatHtml
static int	Inconnu Constante définissant une condition inconnue (Non Calculée).
bob.predicat.TPredicat	Invariant Invariant du composant en cours, servant à la preuve existencielle de transitions
java.util.ArrayList<java.util.ArrayList<java.lang.Integer>>	ListeEtatsParCluster Tableau associant au numéro d'un cluster (d'une équivalence d'états lors du raffinement), un vecteur d'entiers qui représente l'ensemble des numéros d'état des états du cluster donné.
java.util.Vector<bob.expression.TExprIdentificateur>	ListeVariables Vecteur contenant les TExprIdentificateur, servant à la preuve existencielle de transitions
int	NbEtatsCharges Nombre d'états dans le STE courant
int	NbEvCharges Nombre d'événements dans le STE courant
static int	NonPr Constante définissant une condition Non prouvée
static char[]	RepresentationConstantesPlus1 Représentation textuelle des différentes constantes définies précédamment
static boolean[]	TabFormatsSortie tableau memorisant les formats de sortie demandé par l'utilisateur.
PrintWriterGeneSyst	terminal Variable pointant vers le flux de sortie courant pour l'affichage des messages
static int	TjrsF Constante définissant une condition à FAUX
static int	TjrsV Constante définissant une condition à VRAI

Constructor Summary

GFI_Datas(PrintWriterGeneSyst term)
Constructeur simplifié de la classe de gestion du format intermédiaire.

GFI_Datas(PrintWriterGeneSyst term, int NbEtats, int NbEvents)
Constructeur de la classe de gestion du format intermédiaire.

Method Summary

(package private) void	AfficheTout() Méthode de Débug.
(package private) java.lang.String	CommentaireDebugage() Calcule le commentaire de fin de ligne en mode débugage.
(package private) int	DonneAtt(int Etat1, int Etat2, int Ev) Renvoie le niveau de preuve de l'atteignabilité depuis l'état précisé pour l'événement Donné vers l'état donné.
(package private) int	DonneDecl(int Etat, int Ev) Renvoie le niveau de preuve de la déclenchabilité de l'état précisé pour l'événement Donné.
(package private) int	DonneEquiv(int EtatR) Renvoie le numéro de la disjonction d'états équivalente à Etat1.
(package private) int	DonneEquiv(int EtatR, int EtatA) Renvoie le niveau de preuve de l'équivalence entre l'état abstrait Etat1 et la disjonction d'états Etat2 précisée.
static int	DonneEtatArrivee(java.util.Vector<GFI_Datas.QuadrupletEntiers> Trans, int i)
static int	DonneEtatDepart(java.util.Vector<GFI_Datas.QuadrupletEntiers> Trans, int i) Méthode permettant d'accèder au champs Etat de départ d'une transition issue de la méthode DonneListeTransitions.
(package private) int	DonneEtatNDuCluster(int Cluster, int NumEtat) Donne le NumEtat-ième état du regroupement d'états Cluster lors d'un raffinement.
int[]	DonneEtatsAVisiter() La méthode DonneEtatsAVisiter renvoie un tableau d'entiers dont chacun des éléments est le numéro d'un état atteind n'ayant pas encore été observé du point de vue de la déclenchabilité des événements
int[]	DonneEtatsInit() La méthode DonneEtatsInit renvoie un tableau d'entiers contenant l'ensemble des numéros des états initiaux.
static int	DonneEvenement(java.util.Vector<GFI_Datas.QuadrupletEntiers> Trans, int i)
java.util.Vector<GFI_Datas.QuadrupletEntiers>	DonneListeTransitions() Méthode permettant de lister toutes les transitions réalisables par un système.
(package private) int	DonneNbEtats() Renvoie le nombre d'états présents dans le STE.
(package private) int	DonneNumClusterFromEtat(int Etat) Donne le numéro du cluster dans lequel se trouve l'état précisé.
(package private) bob.predicat.TPredicat	DonnePredAtt(int Etat1, int Etat2, int Ev) Donne la condition pour l'evenement atteignable
(package private) bob.predicat.TPredicat	DonnePredDecl(int Etat, int Ev) Donne la condition pour l'evenement declenchable
(package private) bob.predicat.TPredicat	DonnePredInit(int Etat) Donne la condition pour l'etat initial
(package private) int	EstInitial(int Etat) Renvoie le niveau de preuve de l'initiabilité de l'état précisé.
(package private) void	InitialiseNbEtats(int NbEtats)
(package private) void	InitialiseNbEvents(int NbEvents)
(package private) int	NbCluster() Donne le nombre de cluster en mémoire.
(package private) int	NbEtatDansCluster(int Cluster) Donne le nombre d'états contenus dans le regroupement d'états Cluster lors d'un raffinement.
(package private) void	NouvAtt(int Etat1, int Etat2, int Ev, int Pr, java.lang.String FT, java.lang.String FF, java.lang.String FG, bob.predicat.TPredicat Assertion) Ajoute une nouvelle information d'atteignabilité d'état
(package private) void	NouvDecl(int Etat, int Ev, int Pr, java.lang.String FT, java.lang.String FF, java.lang.String FG, bob.predicat.TPredicat Assertion) Ajoute une nouvelle information de déclenchabilité d'événement
(package private) void	NouvEquiv(int EtatR, int EtatA, int Pr, java.lang.String FT) Ajoute une nouvelle information d'équivalence d'états
(package private) void	NouvEtatDansCluster(int Cluster, int Etat) Permet d'ajouter un état dans un regroupement d'états lors d'un raffinement.
(package private) void	NouvInit(int Etat, int Pr, java.lang.String FT, java.lang.String FF, java.lang.String FG, bob.predicat.TPredicat Assertion) Ajoute une nouvelle information d'initialité d'état

Methods inherited from class java.lang.Object

clone, equals, finalize, getClass, hashCode, notify, notifyAll, toString, wait, wait, wait

Field Detail

NonPr

public static final int NonPr

Constante définissant une condition Non prouvée

See Also:

Constant Field Values

TjrsV

public static final int TjrsV

Constante définissant une condition à VRAI

See Also:

Constant Field Values

AvecG

public static final int AvecG

Constante définissant une condition Gardée

See Also:

Constant Field Values

TjrsF

public static final int TjrsF

Constante définissant une condition à FAUX

See Also:

Constant Field Values

Inconnu

public static final int Inconnu

Constante définissant une condition inconnue (Non Calculée).

See Also:

Constant Field Values

RepresentationConstantesPlus1

public static final char[] RepresentationConstantesPlus1

Représentation textuelle des différentes constantes définies précédamment

terminal

public PrintWriterGeneSyst terminal

Variable pointant vers le flux de sortie courant pour l'affichage des messages

EtatsInitiaux

public GFI_Datas.QuadrupletEntiers[] EtatsInitiaux

Tableau décrivant l'ensemble des états initiaux.
Le numéro d'index est le numéro de l'état et le contenu du tableau : (-1,-1,-1,Pr,FT,FF)
où Pr est l'une des trois constantes de preuve TjrsV/TjrsF/AvecG

DeclConnues

public GFI_Datas.QuadrupletEntiers[][] DeclConnues

Tableau décrivant l'ensemble des déclenchabilités connues.
Le format de chaque élément est : (Etat,Ev,-1,Pr,FT,FF)
où Etat est le numéro de l'état considéré, Ev le numéro de l'événement et Pr l'une des trois constantes de preuve TjrsV/TjrsF/AvecG

AttConnues

public GFI_Datas.QuadrupletEntiers[][][] AttConnues

Tableau décrivant l'ensemble des atteignabilités connues.
Le format de chaque élément est : (EtatD,EtatA,Ev,Pr,FT,FF)
où EtatD est le numéro de l'état de départ considéré, EtatA le numéro de l'état d'arrivée, Ev le numéro de l'événement et Pr l'une des trois constantes de preuve TjrsV/TjrsF/AvecG

EquivEtatsConnues

public GFI_Datas.QuadrupletEntiers[] EquivEtatsConnues

Tableau décrivant l'ensemble des équivalences d'états connues.
Le format de chaque élément est : (NumEquiv,Pr,EtatA,EtatA)
où EtatA est le numéro de l'état abstrait considéré, Pr l'une des deux constantes de preuve TjrsV/TjrsF, et NumEquiv le numéro de l'a disjonction d'états qui est équivalente à EtatA. Notons Que ce dernier paramètre est doublé pour une question de réutilisabilité des fonctions existantes dans les différents modes de recherche.

Ce cas là n'est utile que pour une machine de raffinement

ListeEtatsParCluster

public java.util.ArrayList<java.util.ArrayList<java.lang.Integer>> ListeEtatsParCluster

Tableau associant au numéro d'un cluster (d'une équivalence d'états lors du raffinement), un vecteur d'entiers qui représente l'ensemble des numéros d'état des états du cluster donné.

NbEtatsCharges

public int NbEtatsCharges

Nombre d'états dans le STE courant

NbEvCharges

public int NbEvCharges

Nombre d'événements dans le STE courant

EtatsEtudies

public int[] EtatsEtudies

Taleau Permettant de mémoriser les états ayant déjà été visités lors de la construction inductive des différentes transitions.

Declenchable

public static final int Declenchable

Constante utilisée lors de la construction inductive des différentes transitions.

See Also:

Constant Field Values

Atteignable

public static final int Atteignable

Constante utilisée lors de la construction inductive des différentes transitions.

See Also:

Constant Field Values

DejaEtudie

public static final int DejaEtudie

Constante utilisée lors de la construction inductive des différentes transitions.

See Also:

Constant Field Values

TabFormatsSortie

public static boolean[] TabFormatsSortie

tableau memorisant les formats de sortie demandé par l'utilisateur.

FormatDot

public static final int FormatDot

Definition des constantes correspondant aux formats

FormatHtml

public static final int FormatHtml

FormatGxl

public static final int FormatGxl

ListeVariables

public java.util.Vector<bob.expression.TExprIdentificateur> ListeVariables

Vecteur contenant les TExprIdentificateur, servant à la preuve existencielle de transitions

Invariant

public bob.predicat.TPredicat Invariant

Invariant du composant en cours, servant à la preuve existencielle de transitions

Constructor Detail

GFI_Datas

GFI_Datas(PrintWriterGeneSyst term)

Constructeur simplifié de la classe de gestion du format intermédiaire.

Parameters:

term - C'est un pointeur vers un flux de sortie pour l'affichage des messages

GFI_Datas

GFI_Datas(PrintWriterGeneSyst term,
          int NbEtats,
          int NbEvents)

Constructeur de la classe de gestion du format intermédiaire.

Parameters:

term - C'est un pointeur vers un flux de sortie pour l'affichage des messages

NbEtats - Indique le nombre d'états contenus dans le système courant. Cette information est précieuse pour créer les tableaux d'états initiaux notamment.

NbEvents - Indique le nombre d'événements contenus dans le système courant. Cette information est précieuse pour créer les tableaux d'événements initiaux notamment.

Method Detail

InitialiseNbEtats

void InitialiseNbEtats(int NbEtats)

InitialiseNbEvents

void InitialiseNbEvents(int NbEvents)

DonneNbEtats

int DonneNbEtats()

Renvoie le nombre d'états présents dans le STE.

Returns:

le nombre d'états

EstInitial

int EstInitial(int Etat)

Renvoie le niveau de preuve de l'initiabilité de l'état précisé.

Parameters:

Etat - Numéro de l'état dont on veut savoir sont initiabilité

Returns:

le niveau de la preuve de l'initiabilité de Etat

DonneDecl

int DonneDecl(int Etat,
              int Ev)

Renvoie le niveau de preuve de la déclenchabilité de l'état précisé pour l'événement Donné.

Parameters:

Etat - Numéro de l'état de départ

Ev - Numéro de l'événement dont on veut savoir sa déclenchabilité

Returns:

le niveau de la preuve de la déclenchabilité de Ev depuis Etat

DonneAtt

int DonneAtt(int Etat1,
             int Etat2,
             int Ev)

Renvoie le niveau de preuve de l'atteignabilité depuis l'état précisé pour l'événement Donné vers l'état donné.

Parameters:

Etat1 - Numéro de l'état de départ

Etat2 - Numéro de l'état d'arrivée

Ev - Numéro de l'événement dont on veut savoir son atteignabilité

Returns:

le niveau de la preuve de l'atteignabilité de Ev depuis Etat1 vers Etat2

DonneEquiv

int DonneEquiv(int EtatR)

Renvoie le numéro de la disjonction d'états équivalente à Etat1. Si aucun élément ne match alors on renvoi la constante Inconnu.

Parameters:

EtatR - Numéro de la disjonction d'états Raffinés

Returns:

le numéro de la disjonction d'états équivalente à Etat1.

DonneEquiv

int DonneEquiv(int EtatR,
               int EtatA)

Renvoie le niveau de preuve de l'équivalence entre l'état abstrait Etat1 et la disjonction d'états Etat2 précisée.

Parameters:

EtatR - Numéro de la disjonction d'états Raffinés

EtatA - Numéro de l'état Abstrait

Returns:

le niveau de preuve de l'équivalence entre Etat1 et Etat2.

CommentaireDebugage

java.lang.String CommentaireDebugage()

Calcule le commentaire de fin de ligne en mode débugage.

NouvInit

void NouvInit(int Etat,
              int Pr,
              java.lang.String FT,
              java.lang.String FF,
              java.lang.String FG,
              bob.predicat.TPredicat Assertion)

Ajoute une nouvelle information d'initialité d'état

Parameters:

Etat - numéro de l'état considéré

Pr - Niveau de la preuve de son initiabilité

FT - Nom du fichier contenant l'obligation de preuve pour la condition TjrsV

FF - Nom du fichier contenant l'obligation de preuve pour la condition TjrsF

FG - Nom du fichier contenant l'obligation de preuve pour la condition AvecG

Assertion - le predicat à memoriser

NouvDecl

void NouvDecl(int Etat,
              int Ev,
              int Pr,
              java.lang.String FT,
              java.lang.String FF,
              java.lang.String FG,
              bob.predicat.TPredicat Assertion)

Ajoute une nouvelle information de déclenchabilité d'événement

Parameters:

Etat - numéro de l'état considéré

Ev - numéro de l'événement considéré

Pr - Niveau de la preuve de sa déclenchabilité

FT - Nom du fichier contenant l'obligation de preuve pour la condition TjrsV

FF - Nom du fichier contenant l'obligation de preuve pour la condition TjrsF

FG - Nom du fichier contenant l'obligation de preuve pour la condition AvecG

Assertion - le predicat à memoriser

NouvAtt

void NouvAtt(int Etat1,
             int Etat2,
             int Ev,
             int Pr,
             java.lang.String FT,
             java.lang.String FF,
             java.lang.String FG,
             bob.predicat.TPredicat Assertion)

Ajoute une nouvelle information d'atteignabilité d'état

Parameters:

Etat1 - numéro de l'état de départ considéré

Etat2 - numéro de l'état d'arrivé considéré

Ev - numéro de l'événement considéré

Pr - Niveau de la preuve de son atteignabilité

FT - Nom du fichier contenant l'obligation de preuve pour la condition TjrsV

FF - Nom du fichier contenant l'obligation de preuve pour la condition TjrsF

FG - Nom du fichier contenant l'obligation de preuve pour la condition AvecG

Assertion - le predicat à memoriser

NouvEquiv

void NouvEquiv(int EtatR,
               int EtatA,
               int Pr,
               java.lang.String FT)

Ajoute une nouvelle information d'équivalence d'états

Parameters:

EtatR - numéro de la disjonction d'états raffiné

EtatA - numéro de l'état abstrait

Pr - Etat de la preuve de l'obligation de preuve.

FT - Nom du fichier contenant l'obligation de preuve pour la condition TjrsV

NouvEtatDansCluster

void NouvEtatDansCluster(int Cluster,
                         int Etat)

Permet d'ajouter un état dans un regroupement d'états lors d'un raffinement.

Parameters:

Cluster - Numéro du regroupement d'états.

Etat - numéro de l'état à ajouter.

NbEtatDansCluster

int NbEtatDansCluster(int Cluster)

Donne le nombre d'états contenus dans le regroupement d'états Cluster lors d'un raffinement.

Parameters:

Cluster - Numéro du regroupement d'états.

Returns:

Nombre d'états contenus dans le regroupement précisé.

NbCluster

int NbCluster()

Donne le nombre de cluster en mémoire.
Attention : une hypothèse forte a été faite ici. Les clusters doivent tous avoir été rentrés en mémoire avec des numéros contigüs en partant de 0.
Ex : si les clusters 0, 1, 2, 3, 4, 6, et 7 sont définis alors seuls le résultat sera 5 et non 7 car les deux derniers seront ignorer à cause de la rupture de continuité de la suite. Normalement, cette contrainte ne devrait poser aucun problème dans notre cas.

Returns:

Nombre de clusters définis en mémoire.

DonneEtatNDuCluster

int DonneEtatNDuCluster(int Cluster,
                        int NumEtat)

Donne le NumEtat-ième état du regroupement d'états Cluster lors d'un raffinement.

Parameters:

Cluster - Numéro du regroupement d'états.

NumEtat - Indice de l'état dont on veut le numéro.

Returns:

Numéro de l'état d'indice NumEtat dans le regroupement numéro Cluster.

DonneNumClusterFromEtat

int DonneNumClusterFromEtat(int Etat)

Donne le numéro du cluster dans lequel se trouve l'état précisé.

Parameters:

Etat - Numéro de l'état dont un veut savoir dans quel cluster il est.

Returns:

Numéro du cluster contenant l'état et -1 sinon.

DonnePredInit

bob.predicat.TPredicat DonnePredInit(int Etat)

Donne la condition pour l'etat initial

Returns:

le predicat associé a l'etat

DonnePredDecl

bob.predicat.TPredicat DonnePredDecl(int Etat,
                                     int Ev)

Donne la condition pour l'evenement declenchable

Returns:

le predicat associé a l'evenement declenchable

DonnePredAtt

bob.predicat.TPredicat DonnePredAtt(int Etat1,
                                    int Etat2,
                                    int Ev)

Donne la condition pour l'evenement atteignable

Returns:

le predicat associé a l'evenement atteignable

AfficheTout

void AfficheTout()

Méthode de Débug. Elle affiche sur le terminal courant la totalité des inforamtions contenue dans l'instance courante de GestionFormatIntermediaire.

DonneEtatsAVisiter

public int[] DonneEtatsAVisiter()

La méthode DonneEtatsAVisiter renvoie un tableau d'entiers dont chacun des éléments est le numéro d'un état atteind n'ayant pas encore été observé du point de vue de la déclenchabilité des événements

Returns:

un tableau d'entiers représentant les états nouvellement atteinds.

DonneEtatsInit

public int[] DonneEtatsInit()

La méthode DonneEtatsInit renvoie un tableau d'entiers contenant l'ensemble des numéros des états initiaux.

Returns:

l'ensemble des numéros des états initiaux.

DonneListeTransitions

public java.util.Vector<GFI_Datas.QuadrupletEntiers> DonneListeTransitions()

Méthode permettant de lister toutes les transitions réalisables par un système.

Returns:

Vecteur de QuadrupletEntiers. Les 3 champs de chacune des transitions sont accessibles par les trois méthodes DonneEtatDepart, DonneEtatArrivee et DonneEvenement.

DonneEtatDepart

public static int DonneEtatDepart(java.util.Vector<GFI_Datas.QuadrupletEntiers> Trans,
                                  int i)

Méthode permettant d'accèder au champs Etat de départ d'une transition issue de la méthode DonneListeTransitions.

Returns:

Vecteur de QuadrupletEntiers. Les 3 champs de chacune des transitions sont accessibles par les trois méthodes DonneEtatDepart, DonneEtatArrivee et DonneEvenement.

DonneEtatArrivee

public static int DonneEtatArrivee(java.util.Vector<GFI_Datas.QuadrupletEntiers> Trans,
                                   int i)

DonneEvenement

public static int DonneEvenement(java.util.Vector<GFI_Datas.QuadrupletEntiers> Trans,
                                 int i)