Class MethodesNonFonctionnelles

java.lang.Object
  ConfigurationGeneSyst
      MethodesNonFonctionnelles

Direct Known Subclasses:

geneSyst, GestionNettoyer, Nettoyer, PreuveAB_tmp

public class MethodesNonFonctionnelles
extends ConfigurationGeneSyst

Quelques méthodes Indépendantes du fonctionnement de genesyst et permettant d'alleger le fichier de cette dernière classe.

Version:

30/08/2007

Author:

Nicolas Stouls en Juillet 2002 à partir de 'systèmeTransitions' de smaine hamdane 13/03/2002
Révision Didier Bert Février 2002 pour enlever les simplifications
Révision de Nicolas Stouls en Mai 2003 pour introduire le parallèlisme de l'atelier et resoudre des problèmes sur gros fichiers Révision de Xavier MORSELLI en février 2004 : -> choix du nom du projet sous l'AB par recherche dans le dossier bdb. ->Mise en constante de certains chemins d'accès dépendant de l'installation de l'atelier B. -> création de 2 fonctions pour l'interfaceAB : nDispo(...) et nNonDispo(..)

Field Summary

static boolean	AffichageMinimum Vrai ssi l'utilisateur veut un affichage minimum des traces.
static int	CstImplementation
static int	CstMachine
static int	CstRefinement
static boolean	Debugage Vrai ssi on est en mode de débugage
static int	Force Définition du niveau de preuve par défaut
static int	NbPreuvesAvantRedemarrage Pour éviter les "Cpu Limit Exceeded" On limite le nombre de preuve avant de redémarrer l'atelier.
static int	NbPreuvesFaitesDepuisDemarrage Pour éviter les "Cpu Limit Exceeded" On limite le nombre de preuve avant de redémarrer l'atelier.
static int	NbPreuvesFaitesParBoB Pour les statistiques.
static int[]	NbPreuvesFaitesParTactiques Pour les statistiques.
static boolean	Nettoyer Par défaut, après toute exécution de GénéSyst, les éléments temporaires seront effacé du dossier de travail.
static java.lang.String	NomDossierCalcul Nom du dossier temporaire de travail
static java.lang.String	NomDuProjet Nom du projet utilisé dans l'atelierB
static boolean	parallele Par défaut, l'atelier B est relancé pour chacune des vérifications des obligations de preuve générées.
static java.lang.String	Path Définition du chemin pour vérifier si un nom de projet existe
static boolean	QueGenererOP Par défaut, les obligations de preuve générées sont soumises au prouveur.
static char	SymboleDefaut Définition du symboles de condition gardée apparaissant dans le graphique final
static char	SymboleNonPr Définition du symboles de condition Non prouvée apparaissant dans le graphique final
static char	SymboleProuve Définition du symboles de condition vraie apparaissant dans le graphique final
static java.lang.String[]	TabClauseNature
static java.lang.String[]	TabExtensions
static boolean	TactiquesInteractives Par défaut, les obligations de preuve générées sont soumises au prouveur.
static int	TempAttenteAuRedemarrage Pour éviter les "Cpu Limit Exceeded" On limite le nombre de preuve avant de redémarrer l'atelier.
static PrintWriterGeneSyst	terminal Terminal de sortie du texte
static boolean	VerifierOracle Par défaut, les orcales soumis ne sont pas vérifiés.

Fields inherited from class ConfigurationGeneSyst

AdresseDossierBDB, AppelAtelierB, Cst_FaireExistentielle, FormatDot, FormatGxl, FormatHtml, NbFormatsSortie, NomDossierDeBase, NomDossierResultat, NomFichierHtml, NomFichierTraces, NomProjetDeBase, PathDot, TabFormatsSortie, TabFormatsSortiePossibles, TactiquesUtilisateur

Constructor Summary

MethodesNonFonctionnelles()

Method Summary

void	AfficheStatistiques(long HeureDepart)
static void	AfficheTabInt(int[] TabInt, java.io.PrintWriter terminal) Méthode utilisée pour la gestion des états atteignables.
static void	AfficheTabInt(int[] TabInt, java.io.PrintWriter terminal, java.lang.String EnteteLigne) Méthode utilisée pour la gestion des états atteignables.
static java.lang.String	AppelCommandeExterne(java.lang.String Commande, boolean Resultat) Exécute la commande donnée avec le shell SH et renvoie le résultat de la commande (si celui-ci a été demandé).
java.lang.String	AppelCommandeExterneAvecScript(java.lang.String Commande, java.lang.String Script) Exécute la commande donnée avec la méthode AppelCommandeExterne en lui donnant comme paramètre un fichier contenant le Script donné et renvoie le résultat de la commande.
java.util.Vector<bob.predicat.TPredicat>	Conjonction(bob.predicat.TPredicat pred) La méthode Conjonction decompose le predicat pred selon les 'et', en un vecteur de predicats.
java.util.Vector<bob.predicat.TPredicat>	Disjonction(bob.predicat.TPredicat pred) La méthode Disjonction decompose le predicat pred selon les 'ou', en un vecteur de predicats.
static java.lang.String	DonneExtension(java.lang.String Nom) La fonction DonneExtension prend un nom de fichier et renvoie une Chaine de caractères ne contenant que l'extension (sans le point).
java.util.Vector<java.lang.String>	Donner_Extension() Donne tous les extensions possibles au fichier NomDuProjet
static java.lang.String	EnleveExtension(java.lang.String Nom) La fonction EnleveExtension prend un nom de fichier et renvoie une Chaine de caractères ne contenant que le nom sans l'extension ni le point.
static int[]	FusionneTabOfInt(int[] tab1, int[] tab2) Méthode utilisée pour la gestion des états atteignables.
java.lang.String	GestionNomDeProjet(java.lang.String NomProjetBase) Méthode utilisée pour la gestion des noms de projet
static int[]	IntNonPresent(int[] Anciens, int[] Nouveaux) Méthode utilisée pour la gestion des états atteignables.
java.util.Vector<bob.predicat.TPredicat>	inverseVecteur(java.util.Vector<bob.predicat.TPredicat> V) Prend un vecteur V et renvoie un vecteur contenant les memes éléments que V, mais dans l'ordre inverse.
void	LanceScriptExterne(java.lang.String Script) Exécute la commande donnée avec la méthode AppelCommandeExterne en lui donnant comme paramètre un fichier contenant le Script donné et renvoie le résultat de la commande.
static java.lang.String	NouveauNomDeFichier(java.lang.String Dossier, java.lang.String Nom) Prend un nom de fichier et renvoie le meme nom avec éventuellement un suffixe, de telle sorte que ce nouveau nom soit inutilisé pour l'instant dans le dossier spécifié.
java.util.Vector<java.lang.String>	RechercheElement(java.lang.String L, java.lang.String Element, boolean fichier) Recherche toutes les sous-chaines de L ayant pour préfixe Element et comme suffixe un numéro.
static java.lang.String	replaceAll(java.lang.String Chaine, java.lang.String ChRecherchee, java.lang.String ChNouvelle)
static java.lang.String	replaceAll(java.lang.String Chaine, java.lang.String ChRecherchee, java.lang.String ChNouvelle, int Debut)
(package private) static java.lang.String	SansChemin(java.lang.String NomFich) Prend un nom de fichier avec son éventuel chemin d'accès et renvoie le nom seul, sans son chemin.
(package private) static void	SysAfficher(java.io.Writer flux_sortie, bob.predicat.TPredicat ex) Affiche un Prédicat avec une présentation particulière pour les bob.predicat.TPredConst

Methods inherited from class ConfigurationGeneSyst

initTactiquesInteractives

Methods inherited from class java.lang.Object

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

Field Detail

NbPreuvesFaitesDepuisDemarrage

public static int NbPreuvesFaitesDepuisDemarrage

Pour éviter les "Cpu Limit Exceeded" On limite le nombre de preuve avant de redémarrer l'atelier.
Cette variable compte le nombre de preuve effectuées depuis redémarrage de l'atelier B.

NbPreuvesAvantRedemarrage

public static final int NbPreuvesAvantRedemarrage

Pour éviter les "Cpu Limit Exceeded" On limite le nombre de preuve avant de redémarrer l'atelier.
Cette variable définit le nombre de preuve à effectuer avant redémarrage de l'atelier B.

See Also:

Constant Field Values

TempAttenteAuRedemarrage

public static final int TempAttenteAuRedemarrage

Pour éviter les "Cpu Limit Exceeded" On limite le nombre de preuve avant de redémarrer l'atelier.
Cette variable définit le temps à attendre au redémarrage de l'atelier B.

See Also:

Constant Field Values

NbPreuvesFaitesParBoB

public static int NbPreuvesFaitesParBoB

Pour les statistiques.

NbPreuvesFaitesParTactiques

public static int[] NbPreuvesFaitesParTactiques

Pour les statistiques.

terminal

public static PrintWriterGeneSyst terminal

Terminal de sortie du texte

Debugage

public static boolean Debugage

Vrai ssi on est en mode de débugage

NomDuProjet

public static java.lang.String NomDuProjet

Nom du projet utilisé dans l'atelierB

NomDossierCalcul

public static java.lang.String NomDossierCalcul

Nom du dossier temporaire de travail

parallele

public static boolean parallele

Par défaut, l'atelier B est relancé pour chacune des vérifications des obligations de preuve générées.

SymboleProuve

public static char SymboleProuve

Définition du symboles de condition vraie apparaissant dans le graphique final

SymboleDefaut

public static char SymboleDefaut

Définition du symboles de condition gardée apparaissant dans le graphique final

SymboleNonPr

public static char SymboleNonPr

Définition du symboles de condition Non prouvée apparaissant dans le graphique final

Force

public static int Force

Définition du niveau de preuve par défaut

Nettoyer

public static boolean Nettoyer

Par défaut, après toute exécution de GénéSyst, les éléments temporaires seront effacé du dossier de travail.

QueGenererOP

public static boolean QueGenererOP

Par défaut, les obligations de preuve générées sont soumises au prouveur.

VerifierOracle

public static boolean VerifierOracle

Par défaut, les orcales soumis ne sont pas vérifiés.

AffichageMinimum

public static boolean AffichageMinimum

Vrai ssi l'utilisateur veut un affichage minimum des traces.

Path

public static java.lang.String Path

Définition du chemin pour vérifier si un nom de projet existe

TactiquesInteractives

public static boolean TactiquesInteractives

Par défaut, les obligations de preuve générées sont soumises au prouveur.

CstMachine

public static final int CstMachine

See Also:

Constant Field Values

CstRefinement

public static final int CstRefinement

See Also:

Constant Field Values

CstImplementation

public static final int CstImplementation

See Also:

Constant Field Values

TabExtensions

public static final java.lang.String[] TabExtensions

TabClauseNature

public static final java.lang.String[] TabClauseNature

Constructor Detail

MethodesNonFonctionnelles

public MethodesNonFonctionnelles()

Method Detail

replaceAll

public static java.lang.String replaceAll(java.lang.String Chaine,
                                          java.lang.String ChRecherchee,
                                          java.lang.String ChNouvelle)

replaceAll

public static java.lang.String replaceAll(java.lang.String Chaine,
                                          java.lang.String ChRecherchee,
                                          java.lang.String ChNouvelle,
                                          int Debut)

AppelCommandeExterne

public static java.lang.String AppelCommandeExterne(java.lang.String Commande,
                                                    boolean Resultat)
                                             throws java.io.IOException,
                                                    ErreurException

Exécute la commande donnée avec le shell SH et renvoie le résultat de la commande (si celui-ci a été demandé).

Parameters:

Commande - La commande à passer

Resultat - Si vrai alors on atend un résultat à cette commande.

Returns:

Le resultat de la commande

Throws:

java.io.IOException

ErreurException

AppelCommandeExterneAvecScript

public java.lang.String AppelCommandeExterneAvecScript(java.lang.String Commande,
                                                       java.lang.String Script)
                                                throws java.io.IOException,
                                                       ErreurException

Exécute la commande donnée avec la méthode AppelCommandeExterne en lui donnant comme paramètre un fichier contenant le Script donné et renvoie le résultat de la commande.

Parameters:

Commande - La commande à passer

Script - Le scipt d'exécution

Returns:

Le resultat de la commande

Throws:

java.io.IOException

ErreurException

LanceScriptExterne

public void LanceScriptExterne(java.lang.String Script)
                        throws java.io.IOException,
                               ErreurException

Exécute la commande donnée avec la méthode AppelCommandeExterne en lui donnant comme paramètre un fichier contenant le Script donné et renvoie le résultat de la commande.

Parameters:

Commande - La commande à passer

Script - Le scipt d'exécution

Throws:

java.io.IOException

ErreurException

SansChemin

static java.lang.String SansChemin(java.lang.String NomFich)

Prend un nom de fichier avec son éventuel chemin d'accès et renvoie le nom seul, sans son chemin.

Parameters:

NomFich - Le nom du fichier avec son éventuel chemin.

Returns:

Le nom du fichier sans son chemin.

SysAfficher

static void SysAfficher(java.io.Writer flux_sortie,
                        bob.predicat.TPredicat ex)
                 throws java.io.IOException,
                        java.io.FileNotFoundException

Affiche un Prédicat avec une présentation particulière pour les bob.predicat.TPredConst

Parameters:

flux_sortie - Flux de sortie: fichier de type Writer ou terminal(new PrintWriter(System.out)).

ex - prédicat à représenter.

Throws:

java.io.IOException

java.io.FileNotFoundException

NouveauNomDeFichier

public static java.lang.String NouveauNomDeFichier(java.lang.String Dossier,
                                                   java.lang.String Nom)
                                            throws java.io.IOException

Prend un nom de fichier et renvoie le meme nom avec éventuellement un suffixe, de telle sorte que ce nouveau nom soit inutilisé pour l'instant dans le dossier spécifié.

Parameters:

Dossier - Le dossier de recherche

Nom - Le nom voulu

Returns:

un nom de fichier non utilisé

Throws:

java.io.IOException

GestionNomDeProjet

public java.lang.String GestionNomDeProjet(java.lang.String NomProjetBase)
                                    throws java.lang.InterruptedException

Méthode utilisée pour la gestion des noms de projet

Parameters:

NomProjetBase - Nom de projet de base

Returns:

Renvoie le nom du projet

Throws:

java.lang.InterruptedException

RechercheElement

public java.util.Vector<java.lang.String> RechercheElement(java.lang.String L,
                                                           java.lang.String Element,
                                                           boolean fichier)

Recherche toutes les sous-chaines de L ayant pour préfixe Element et comme suffixe un numéro. Si fichier est vrai, alors chaque chaine trouvée sera considérée comme un nom de fichier et leur existence serra vérifiée.

Parameters:

L - une chaine de recherche

Element - la chaine à chercher

fichier - vrai ssi on cherche des noms de fichiers

Returns:

la liste de toutes les sous-chaines trouvées.

EnleveExtension

public static java.lang.String EnleveExtension(java.lang.String Nom)

La fonction EnleveExtension prend un nom de fichier et renvoie une Chaine de caractères ne contenant que le nom sans l'extension ni le point.

Parameters:

Nom - nom dont on veut enlever l'extension

Returns:

le Nom sans l'extension ni le point

DonneExtension

public static java.lang.String DonneExtension(java.lang.String Nom)

La fonction DonneExtension prend un nom de fichier et renvoie une Chaine de caractères ne contenant que l'extension (sans le point).

Parameters:

Nom - nom dont en veut l'extension

Returns:

l'extension (sans le point)

Donner_Extension

public java.util.Vector<java.lang.String> Donner_Extension()

Donne tous les extensions possibles au fichier NomDuProjet

Returns:

le Vector de toutes les extensions possibles.

Disjonction

public java.util.Vector<bob.predicat.TPredicat> Disjonction(bob.predicat.TPredicat pred)

La méthode Disjonction decompose le predicat pred selon les 'ou', en un vecteur de predicats.

Parameters:

pred - prédicat à décomposer

Conjonction

public java.util.Vector<bob.predicat.TPredicat> Conjonction(bob.predicat.TPredicat pred)

La méthode Conjonction decompose le predicat pred selon les 'et', en un vecteur de predicats.

Parameters:

pred - prédicat à décomposer

inverseVecteur

public java.util.Vector<bob.predicat.TPredicat> inverseVecteur(java.util.Vector<bob.predicat.TPredicat> V)

Prend un vecteur V et renvoie un vecteur contenant les memes éléments que V, mais dans l'ordre inverse.

Parameters:

V - Vecteur initial

Returns:

Vecteur inversé

FusionneTabOfInt

public static int[] FusionneTabOfInt(int[] tab1,
                                     int[] tab2)

Méthode utilisée pour la gestion des états atteignables.

Celle-ci permet de fusionner deux tableaux d'entier dans une troisième en évitant les doublons à la condition initiale que tab1 ne contienne pas de doublons.

Parameters:

tab1 - Tableau d'entiers ne contenant pas 2 valeurs identiques

tab2 - Tableau d'entiers

Returns:

Un pointeur vers un nouveau tableau contenant une et une seule fois chacunes des valeurs contenues dans les tableaux tab1 et tab2.

IntNonPresent

public static int[] IntNonPresent(int[] Anciens,
                                  int[] Nouveaux)

Méthode utilisée pour la gestion des états atteignables.

Celle-ci permet de définir l'ensemble des entiers présent dans le tableau Nouveaux mais n'étant pas dans le tableau Anciens.

Parameters:

Anciens - Tableau d'entiers

Nouveaux - Tableau d'entiers

Returns:

Un pointeur vers un nouveau tableau contenant une et une seule fois chacunes des valeurs contenues dans Nouveaux mais n'étant pas dans Anciens.

AfficheTabInt

public static void AfficheTabInt(int[] TabInt,
                                 java.io.PrintWriter terminal)

Méthode utilisée pour la gestion des états atteignables.

Celle-ci permet d'afficher le contenu de TabInt sur le flux terminal sur plusieurs lignes sous la forme d'une liste.

Parameters:

TabInt - Tableau d'entiers

terminal - flux de sortie

AfficheTabInt

public static void AfficheTabInt(int[] TabInt,
                                 java.io.PrintWriter terminal,
                                 java.lang.String EnteteLigne)

Méthode utilisée pour la gestion des états atteignables.

Celle-ci permet d'afficher le contenu de TabInt sur le flux terminal sur plusieurs lignes sous la forme d'une liste dont l'entete de la ligne peut etre paramètrée.

Parameters:

TabInt - Tableau d'entiers

terminal - flux de sortie

EnteteLigne - entete de chacune des lignes

AfficheStatistiques

public void AfficheStatistiques(long HeureDepart)