Class GFI_Exportation

java.lang.Object
  GFI_Datas
      GFI_Parseur
          GFI_Exportation

Direct Known Subclasses:

GestionFormatIntermediaire

public class GFI_Exportation
extends GFI_Parseur

Cette classe définie une structure de données pour la mise en mémoire des traces avec les méthodes KiVontBien pour exporter les données vers un fichier graphique ou de format intermédiaire.

Version:

20/01/2004

Author:

Nicolas Stouls en Janvier 2004

Nested Class Summary

Nested classes/interfaces inherited from class GFI_Datas

GFI_Datas.QuadrupletEntiers

Field Summary

static boolean	ExporterCommentaire
(package private) java.lang.String[]	ListeEtats
(package private) java.lang.String[]	ListeEtatsAbstraits
(package private) static java.lang.String	NomInit Constante définissant le nom de l'événement étiquetant les transitions partant de QInit
(package private) static java.lang.String	NomQInit Constante définissant le nom de l'état initial

Fields inherited from class GFI_Parseur

DernierCarLuInutilise, FinChargementEtats, FinChargementEv

Fields inherited from class GFI_Datas

AttConnues, Atteignable, AvecG, DeclConnues, Declenchable, DejaEtudie, EquivEtatsConnues, EtatsEtudies, EtatsInitiaux, FormatDot, FormatGxl, FormatHtml, Inconnu, Invariant, ListeEtatsParCluster, ListeVariables, NbEtatsCharges, NbEvCharges, NonPr, RepresentationConstantesPlus1, TabFormatsSortie, terminal, TjrsF, TjrsV

Constructor Summary

GFI_Exportation(PrintWriterGeneSyst term, java.lang.String NomFichierOracle)

GFI_Exportation(PrintWriterGeneSyst term, java.lang.String NomFichierOracle, int NbEtats, int NbEvents)

Method Summary

java.lang.String	AffichageGarde(int indice, int nature, int etat1, int etat2) Methodes permettant d'afficher les renseignements sur declanchabilité, atteignabilité et etats initiaux
void	Afficher(java.io.PrintWriter FluxSortie, java.util.Vector<bob.composant.TOperation> ops, java.lang.String EnteteLigne) Méthode permettant d'afficher, sur le flux de sortie précisé, une représentation textuelle du STE courant.
private java.lang.String[]	ConvertDisjEtats(java.util.Vector<bob.predicat.TPredicat> preds_disj) Convertie le vecteurs de disjonctions d'états donnés en paramètre en un tableau de String.
(package private) void	ExporteFichier(java.lang.String NomFichier, java.util.Vector<bob.composant.TOperation> ops, java.util.Vector<bob.predicat.TPredicat> Etats) Méthode permettant d'exporter les informations en mémoire vers un fichier d'oracle.
void	GenerationDOT(java.lang.String NomMachine, java.lang.String[] ListeNomOps, java.util.Vector<bob.predicat.TPredicat> preds_disj, char SymboleProuve, char SymboleDefaut, char SymboleNonPr, java.lang.String NomResultatCalcul) Génère un fichier .dot, traduisible avec l'outil dot de GRAPHVIZ de AT&T, en une image de différents formats.
void	GenerationDOT(java.lang.String NomMachine, java.lang.String[] ListeNomOps, java.util.Vector<bob.predicat.TPredicat> preds_disj, java.util.Vector<bob.predicat.TPredicat> preds_disj_abstraite, int[] EquivalenceEtats, char SymboleProuve, char SymboleDefaut, char SymboleNonPr, java.lang.String NomResultatCalcul) Génère un fichier .dot, traduisible avec l'outil dot de GRAPHVIZ de AT&T, en une image de différents formats.
void	GenerationFichierClusterHTML(int i, java.lang.String nomCl, java.util.Vector<java.lang.String> etats, java.lang.String NomResultatCalcul) Methodes permettant de generer les fichiers HTML fournissant les renseignements des CLUSTERS
void	GenerationFichiersEtatHTML(int i, java.lang.String nomEtat, int CondInit, java.lang.String NomResultatCalcul) Methodes permettant de generer les fichiers HTML fournissant les renseignements des ETATS
void	GenerationFichierTransitionHTML(int i, java.util.ArrayList<GFI_Datas.QuadrupletEntiers> nomEv, int dep, int arr, java.lang.String NomResultatCalcul) Methodes permettant de generer les fichiers HTML fournissant les renseignements des TRANSITIONS
void	GenerationGXL(java.lang.String NomMachine, java.lang.String[] ListeNomOps, java.util.Vector<bob.predicat.TPredicat> preds_disj, char SymboleProuve, char SymboleDefaut, char SymboleNonPr, java.lang.String NomResultatCalcul) Generation du fichier Gxl: NomMachine.gxl cas des machines
void	GenerationGXL(java.lang.String NomMachine, java.lang.String[] ListeNomOps, java.util.Vector<bob.predicat.TPredicat> preds_disj, java.util.Vector<bob.predicat.TPredicat> preds_disj_abstraite, int[] EquivalenceEtats, char SymboleProuve, char SymboleDefaut, char SymboleNonPr, java.lang.String NomResultatCalcul) Generation du fichier Gxl: NomMachine.gxl
void	GenerationIndexHtml(java.lang.String NomMachine, java.lang.String NomResultatCalcul) Generation du fichier html:index.html
static java.lang.String	intToStr(int i, int l)
(package private) static java.lang.String	NomFichierSVGMachine(java.lang.String Prefixe, int NumOp, int NumEtat1, int NumEtat2, int TypeOP) Méthode calculant le nom d'une machine de sauvegarde d'une obligation de preuve SANS SON EXTENSION !!!
static java.lang.String	StrMoins(int l)
static java.lang.String	strToStr(java.lang.String Str, int l)

Methods inherited from class GFI_Parseur

CaptureAssocNumEtat_Etat, CaptureAssocNumEv_Ev, CaptureAtt, CaptureDecl, CaptureEqu, CaptureInit, CaptureInstruction, CaptureInt, CaptureNomIdf, CapturePr, CaptureStr, chargeOracle, EstAlphaNum, EstInt, FermeParenthese, OuvreParenthese, PasseEspaces, Virgule

Methods inherited from class GFI_Datas

AfficheTout, CommentaireDebugage, DonneAtt, DonneDecl, DonneEquiv, DonneEquiv, DonneEtatArrivee, DonneEtatDepart, DonneEtatNDuCluster, DonneEtatsAVisiter, DonneEtatsInit, DonneEvenement, DonneListeTransitions, DonneNbEtats, DonneNumClusterFromEtat, DonnePredAtt, DonnePredDecl, DonnePredInit, EstInitial, InitialiseNbEtats, InitialiseNbEvents, NbCluster, NbEtatDansCluster, NouvAtt, NouvDecl, NouvEquiv, NouvEtatDansCluster, NouvInit

Methods inherited from class java.lang.Object

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

Field Detail

ExporterCommentaire

public static boolean ExporterCommentaire

NomQInit

static final java.lang.String NomQInit

Constante définissant le nom de l'état initial

See Also:

Constant Field Values

NomInit

static final java.lang.String NomInit

Constante définissant le nom de l'événement étiquetant les transitions partant de QInit

See Also:

Constant Field Values

ListeEtats

java.lang.String[] ListeEtats

ListeEtatsAbstraits

java.lang.String[] ListeEtatsAbstraits

Constructor Detail

GFI_Exportation

GFI_Exportation(PrintWriterGeneSyst term,
                java.lang.String NomFichierOracle)

GFI_Exportation

GFI_Exportation(PrintWriterGeneSyst term,
                java.lang.String NomFichierOracle,
                int NbEtats,
                int NbEvents)

Method Detail

NomFichierSVGMachine

static java.lang.String NomFichierSVGMachine(java.lang.String Prefixe,
                                             int NumOp,
                                             int NumEtat1,
                                             int NumEtat2,
                                             int TypeOP)

Méthode calculant le nom d'une machine de sauvegarde d'une obligation de preuve SANS SON EXTENSION !!! A DEPLACER DANS UNE AUTRE CLASSE !!!!!

Parameters:

Prefixe - Préfixe à rajouter en entete du nom de fichier

NumOp - le numéro de l'opération (>=0 ou =-1 si initialisation)

NumEtat1 - >=0, un numéro d'état.

NumEtat2 - >=0, un numéro d'état ou -1 sinon. // * @param OPDefaut faux ssi on cherche à prouver que la transition est toujours vrai

TypeOP - Donne le type d'OP contenu dans le fichier pour savoir quel suffixe mettre au fichier.

Returns:

nom à utiliser pour le fichier contenant l'obligation de preuve décrite.

ExporteFichier

void ExporteFichier(java.lang.String NomFichier,
                    java.util.Vector<bob.composant.TOperation> ops,
                    java.util.Vector<bob.predicat.TPredicat> Etats)
              throws java.io.IOException

Méthode permettant d'exporter les informations en mémoire vers un fichier d'oracle.

Parameters:

NomFichier - Nom du fichier où écrire l'oracle

ops - Vecteur contenant le nom de chacune des opérations

Etats - Vecteur contenant le predicat de chacun des états

Throws:

java.io.IOException

Afficher

public void Afficher(java.io.PrintWriter FluxSortie,
                     java.util.Vector<bob.composant.TOperation> ops,
                     java.lang.String EnteteLigne)

Méthode permettant d'afficher, sur le flux de sortie précisé, une représentation textuelle du STE courant.

Parameters:

FluxSortie - Pointeur vers le flux de sortie dans lequel sera écrit l'orcale.

ops - Vecteur contenant le nom de chacune des opérations.

EnteteLigne - Chaine de caractère à mettre en debut de chacune des lignes.

StrMoins

public static java.lang.String StrMoins(int l)

intToStr

public static java.lang.String intToStr(int i,
                                        int l)

strToStr

public static java.lang.String strToStr(java.lang.String Str,
                                        int l)

GenerationDOT

public void GenerationDOT(java.lang.String NomMachine,
                          java.lang.String[] ListeNomOps,
                          java.util.Vector<bob.predicat.TPredicat> preds_disj,
                          char SymboleProuve,
                          char SymboleDefaut,
                          char SymboleNonPr,
                          java.lang.String NomResultatCalcul)
                   throws java.io.IOException,
                          ErreurException

Génère un fichier .dot, traduisible avec l'outil dot de GRAPHVIZ de AT&T, en une image de différents formats.

Entete simplifiée pour ne pas changer les méthoe y faisant référence.

Parameters:

NomMachine - Nom de la machine originale à partir du quel va-t-etre dériver le nim du fichier généré.

ListeNomOps - Liste des opérations (et donc de leurs noms)

preds_disj - description des différents états

SymboleProuve - Carractère à affiché sur le graphique produit en tant que condition si celle-ci est réductible à true.

SymboleDefaut - Carractère à affiché sur le graphique produit en tant que condition si celle-ci n'est pas réductible à true.

SymboleNonPr - Carractère à affiché sur le graphique produit en tant que condition si celle-ci n'est pas prouvé.

NomResultatCalcul - Nom du dossier à utiliser pour créer le résultat de la génération HTML

Throws:

java.io.IOException

ErreurException

ConvertDisjEtats

private java.lang.String[] ConvertDisjEtats(java.util.Vector<bob.predicat.TPredicat> preds_disj)
                                     throws java.io.IOException,
                                            ErreurException

Convertie le vecteurs de disjonctions d'états donnés en paramètre en un tableau de String.

Parameters:

preds_disj - description des différents états.

Returns:

Version textuelle de chacun des états décrits dans le vecteur paramètre.

Throws:

java.io.IOException

ErreurException

GenerationDOT

public void GenerationDOT(java.lang.String NomMachine,
                          java.lang.String[] ListeNomOps,
                          java.util.Vector<bob.predicat.TPredicat> preds_disj,
                          java.util.Vector<bob.predicat.TPredicat> preds_disj_abstraite,
                          int[] EquivalenceEtats,
                          char SymboleProuve,
                          char SymboleDefaut,
                          char SymboleNonPr,
                          java.lang.String NomResultatCalcul)
                   throws java.io.IOException,
                          ErreurException

Génère un fichier .dot, traduisible avec l'outil dot de GRAPHVIZ de AT&T, en une image de différents formats.

Parameters:

NomMachine - Nom de la machine originale à partir du quel va-t-etre dériver le nim du fichier généré.

ListeNomOps - Liste des opérations (et donc de leurs noms)

preds_disj - description des différents états

preds_disj_abstraite - description des différents états de l'abstraction

EquivalenceEtats - Equivalence des états entre les abstraits et les raffinés.

SymboleProuve - Carractère à affiché sur le graphique produit en tant que condition si celle-ci est réductible à true.

SymboleDefaut - Carractère à affiché sur le graphique produit en tant que condition si celle-ci n'est pas réductible à true.

SymboleNonPr - Carractère à affiché sur le graphique produit en tant que condition si celle-ci n'est pas prouvé.

NomResultatCalcul - Nom du dossier à utiliser pour créer le résultat de la génération HTML

Throws:

java.io.IOException

ErreurException

GenerationFichiersEtatHTML

public void GenerationFichiersEtatHTML(int i,
                                       java.lang.String nomEtat,
                                       int CondInit,
                                       java.lang.String NomResultatCalcul)

Methodes permettant de generer les fichiers HTML fournissant les renseignements des ETATS

Parameters:

i - indique le numero que le fichier devra avoir comme nom il permet de faire la correspondance entre le fichier et l'état concerné.

nomEtat - le nom de l'état // * @param initG boolean indiquant si l'état est gardé ou pas // * @param initT boolean indiquant si l'état est toujours initial ou pas

CondInit - Entier indiquant le nouveau de preuve de l'"initiabilité" de l'état

NomResultatCalcul - represente le nom du dossier principal où le fichier va etre créer

GenerationFichierClusterHTML

public void GenerationFichierClusterHTML(int i,
                                         java.lang.String nomCl,
                                         java.util.Vector<java.lang.String> etats,
                                         java.lang.String NomResultatCalcul)

Methodes permettant de generer les fichiers HTML fournissant les renseignements des CLUSTERS

Parameters:

i - indique le numero que le fichier devra avoir comme nom il permet de faire la correspondance entre le fichier et le cluster concerné.

nomCl - le nom du cluster

etats - vecteur detenant le nom des états le composant

NomResultatCalcul - represente le nom du dossier principal où le fichier va etre créer

GenerationFichierTransitionHTML

public void GenerationFichierTransitionHTML(int i,
                                            java.util.ArrayList<GFI_Datas.QuadrupletEntiers> nomEv,
                                            int dep,
                                            int arr,
                                            java.lang.String NomResultatCalcul)

Methodes permettant de generer les fichiers HTML fournissant les renseignements des TRANSITIONS

Parameters:

i - indique le numero que le fichier devra avoir comme nom. Il permet de faire la correspondance entre le fichier et la transition concernée.

nomEv - vecteur memorisant le nom des evenements contenu dans une transitions.

dep - designe l'etat de depart

arr - designe l'etat d'arrivée

NomResultatCalcul - represente le nom du dossier principal où le fichier va etre créer

AffichageGarde

public java.lang.String AffichageGarde(int indice,
                                       int nature,
                                       int etat1,
                                       int etat2)
                                throws java.io.IOException

Methodes permettant d'afficher les renseignements sur declanchabilité, atteignabilité et etats initiaux

Parameters:

indice - designe le numero de l'evenement pour Declenchable et Atteignable

nature - entier permettant de savoir s'il sagit de Declenchable,Atteignable ou etatsinitiaux

etat1 - correspondant au numero de l'etat concerné pour EtatsInitiaux et Declenchable et correspondant à l'etat de depart pour Atteignable.

etat2 - correspondant à l'etat d'arrivée pour Atteignable

Returns:

String la chaine de caractere en html qui permet d'afficher les conditions dans un textArea.

Throws:

java.io.IOException

GenerationIndexHtml

public void GenerationIndexHtml(java.lang.String NomMachine,
                                java.lang.String NomResultatCalcul)
                         throws ErreurException,
                                java.io.IOException

Generation du fichier html:index.html

Parameters:

NomMachine - est le nom de la machine,ce nom permet de manipuler le fichier NomMachine.dot generé precedemment.

NomResultatCalcul - permet de creer le fichier index.html dans le bon bon repertoire.

Throws:

ErreurException

java.io.IOException

GenerationGXL

public void GenerationGXL(java.lang.String NomMachine,
                          java.lang.String[] ListeNomOps,
                          java.util.Vector<bob.predicat.TPredicat> preds_disj,
                          char SymboleProuve,
                          char SymboleDefaut,
                          char SymboleNonPr,
                          java.lang.String NomResultatCalcul)
                   throws java.io.IOException,
                          ErreurException

Generation du fichier Gxl: NomMachine.gxl cas des machines

Parameters:

NomMachine - Nom de la machine originale à partir du quel va-t-etre dériver le nim du fichier généré.

ListeNomOps - Liste des opérations (et donc de leurs noms)

preds_disj - description des différents états

SymboleProuve - Carractère à affiché sur le graphique produit en tant que condition si celle-ci est réductible à true.

SymboleDefaut - Carractère à affiché sur le graphique produit en tant que condition si celle-ci n'est pas réductible à true.

SymboleNonPr - Carractère à affiché sur le graphique produit en tant que condition si celle-ci n'est pas prouvée.

NomResultatCalcul - Nom du dossier à utiliser pour créer le résultat de la génération HTML

Throws:

java.io.IOException

ErreurException

GenerationGXL

public void GenerationGXL(java.lang.String NomMachine,
                          java.lang.String[] ListeNomOps,
                          java.util.Vector<bob.predicat.TPredicat> preds_disj,
                          java.util.Vector<bob.predicat.TPredicat> preds_disj_abstraite,
                          int[] EquivalenceEtats,
                          char SymboleProuve,
                          char SymboleDefaut,
                          char SymboleNonPr,
                          java.lang.String NomResultatCalcul)
                   throws java.io.IOException,
                          ErreurException

Generation du fichier Gxl: NomMachine.gxl

Parameters:

NomMachine - Nom de la machine originale à partir du quel va-t-etre dériver le nim du fichier généré.

ListeNomOps - Liste des opérations (et donc de leurs noms)

preds_disj - description des différents états

preds_disj_abstraite - description des différents états de l'abstraction

EquivalenceEtats - Equivalence des états entre les abstraits et les raffinés.

SymboleProuve - Carractère à affiché sur le graphique produit en tant que condition si celle-ci est réductible à true.

SymboleDefaut - Carractère à affiché sur le graphique produit en tant que condition si celle-ci n'est pas réductible à true.

SymboleNonPr - Carractère à affiché sur le graphique produit en tant que condition si celle-ci n'est pas prouvée.

NomResultatCalcul - Nom du dossier à utiliser pour créer le résultat de la génération HTML

Throws:

java.io.IOException

ErreurException