Class geneSyst

java.lang.Object
  ConfigurationGeneSyst
      MethodesNonFonctionnelles
          geneSyst

public class geneSyst
extends MethodesNonFonctionnelles

La classe geneSyst permet de générer l'automate comportemental exacte d'une spécification B événementielle et de son premier raffinement.

Pour toute information, se référer au site :
http://www-lsr.imag.fr/Les.Personnes/Nicolas.Stouls/
Ou par E-mail à nicolas.stouls@imag.fr

Version:

V0.1.7.2 20/04/2007

Author:

V0.0.1 : smaine hamdane 13/03/2002
V0.1 : Reprise de Nicolas Stouls en Juillet 2002.
V0.1.1 : Révision Didier Bert Février 2002 pour enlever les simplifications
V0.1.2 : Révision de Nicolas Stouls en Mai 2003 pour introduire le parallèlisme de l'atelier et resoudre des problèmes sur gros fichiers
V0.1.3 : Révision en Janvier 2004 par Nicolas Stouls pour introduire la gestion d'un format intermédiaire
V0.1.4 : Révision en aout 2004 par Hounayda Mohamed pour ajouter une interface graphique et différents formats de sortie
V0.1.5 : Révision en Octobre 2004 par Nicolas Stouls pour corriger quelques petits bugs
V0.1.5.1 : Révision en Novembre 2004 par Nicolas Stouls pour corriger un gros bug de génération de résultats
V0.1.6-a : Révision en Novembre 2004 par Nicolas Stouls pour ajouter l'OP du cas par défaut
V0.1.6-a.1 : Révision en Décembre 2004 par Nicolas Stouls pour renforcer l'implantation de l'OP du cas par défaut et passage à java 1.5.0
V0.1.6-a.2 : Révision en mars 2005 par Nicolas Stouls pour intégrer la nouvelle BoB.
V0.1.6-a.3 : Révision 11 octobre 2005 par Nicolas Stouls pour corriger un problème d'utilisation des oracles.
V0.1.7 : Révision le 4 novembre 2005 par Nicolas Stouls pour supporter la prouveur B4free
V0.1.7.1 : Révision le 8 novembre 2005 par Nicolas Stouls pour avoir la visualisation des 2 composants lorsque un raffinement est pris en compte
V0.1.7.2 : Révision le 20 avril 2007 par Nicolas Stouls pour pouvoir ne pas exporter de commentaire dans les oracle, afin de faciliter le dépiotage automatique des tests de non régression
+ simplification de l'algo de calcul des atteignabilités
+ prise en compte des simplifications par raffinement du calcul d'atteignabilité. + Correction des bugs avec prouveur en parallèle + Calcul des déclenchabilité à false avant true + Sortie possible du nombre de preuve pour tests

Field Summary

static java.lang.String	CheminEtNomFichierAbstrProduitAuFormatDot
static java.lang.String	CheminEtNomFichierRaffProduitAuFormatDot
static boolean	DonnerNombreDePreuves
static boolean	ExporterCommentaire
private boolean	FaireOPExistentielle
PreuveAB_tmp	IAB
static java.lang.String	VersionGS

Fields inherited from class MethodesNonFonctionnelles

AffichageMinimum, CstImplementation, CstMachine, CstRefinement, Debugage, Force, NbPreuvesAvantRedemarrage, NbPreuvesFaitesDepuisDemarrage, NbPreuvesFaitesParBoB, NbPreuvesFaitesParTactiques, Nettoyer, NomDossierCalcul, NomDuProjet, parallele, Path, QueGenererOP, SymboleDefaut, SymboleNonPr, SymboleProuve, TabClauseNature, TabExtensions, TactiquesInteractives, TempAttenteAuRedemarrage, terminal, VerifierOracle

Fields inherited from class ConfigurationGeneSyst

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

Constructor Summary

geneSyst()

Method Summary

private void	DeclenchabiliteDesTransitions(int[] ListeEtatsDepart, java.util.Vector<bob.predicat.TPredicat> preds_disj, java.util.Vector<bob.composant.TOperation> ops, boolean[][][] ListeTransitionsEffectuables, boolean[][] ListeTransitionsDeclenchables, GestionFormatIntermediaire STEInt, boolean QueGenererOP, boolean VerifierOracle) DeclenchabiliteDesTransitions recherche quels sont les couples d'états (E1,E2) possibles tels que pour un événement Ev donné on ait : E1 - Ev -> E2 Le calcul de l'état d'arrivé est déporté dans la méthode RecherchePointArriveeDesTransition.
private int	DonneEtatAbstraitCorrespondant(bob.predicat.TPredicat EtatR, int NumEtatR, java.util.Vector<bob.predicat.TPredicat> preds_disjA, GestionFormatIntermediaire STEInt, boolean QueGenererOP) DonneEtatAbstraitCorrespondant recherche, par la preuve quel état du vector preds_disjA est équivalent au prédicat EtatR.
boolean	GenerationDesSTE(java.lang.String NomFichierAbstraitAvecExtensionEtChemin, java.lang.String NomFichierRaffinementAvecExtensionEtChemin, int Force, boolean Nettoyer, char SDefaut, char SProuve, char SNonPr, boolean QueGenererOP, boolean VerifierOracle, java.lang.String NomFichierOracleMch, java.lang.String NomFichierOracleRaff, boolean FaireExistentielle) GenerationDesSTE réalise les Systèmes de Transitions Etiquetés (STE) du raffinement et de la machine B précisés.
static void	main(java.lang.String[] args) Procédure principale.
private java.lang.String	PointArriveeTransitionNonAtteignable(int Etati, int Evenementj, int Etatk, GestionFormatIntermediaire STEInt, bob.predicat.TPredicat NonAtt, java.lang.String NMT, java.lang.String NMG)
private java.lang.String	PointArriveeTransitionPossibAtteignable(int Etati, int Evenementj, int Etatk, GestionFormatIntermediaire STEInt, bob.predicat.TPredicat PossAtt, bob.predicat.TPredicat NonEvDeNonF, java.lang.String NMT, java.lang.String NMF)
private java.lang.String	PointArriveeTransitionTjrsAtteignable(int Etati, int Evenementj, int Etatk, GestionFormatIntermediaire STEInt, bob.predicat.TPredicat AttSansCond, java.lang.String NMF, java.lang.String NMG)
private void	RechercheEtatsInitiaux(bob.substitution.TSubstitution Initialisation, java.util.Vector<bob.predicat.TPredicat> preds_disj, int[] AssociationEquivalenceEtats, GestionFormatIntermediaire STEInt, GestionFormatIntermediaire STEAbstrait, boolean QueGenererOP, boolean VerifierOracle) RechercheEtatsInitiaux recherche la liste des état initiaux du ststème de transitions et renvoie son résultat sous forme d'uin vercteur de TEtats.
private void	RecherchePointArriveeDesTransition(int Etati, int Evenementj, java.util.Vector<bob.predicat.TPredicat> preds_disj, java.util.Vector<bob.composant.TOperation> ops, boolean[][][] ListeTransitionsEffectuables, GestionFormatIntermediaire STEInt, boolean QueGenererOP, boolean VerifierOracle) RecherchePointArriveeDesTransition recherche quels sont les conditions d'atteignabilité de chacun des états de preds_disj par l'événement Evenementj depuis l'état Etati.
private ResultatAnalyse	TraitementRaffinement(java.lang.String NomFichierAvecExtensionEtChemin, ResultatAnalyse ResultatAnalyseSystemeAbstrait, int Force, boolean Nettoyer, GestionFormatIntermediaire STEIntermediaireAbstrait, GestionFormatIntermediaire STEInt, boolean QueGenererOP, boolean VerifierOracle) TraitementRaffinement réalise le Système de Transitions étiquetées du raffinement B précisé par NomFichierAvecExtension.
private ResultatAnalyse	TraitementSystemeAbstrait(java.lang.String NomFichierAvecExtensionEtChemin, int Force, boolean Nettoyer, GestionFormatIntermediaire STEInt, boolean QueGenererOP, boolean VerifierOracle) TraitementSystemeAbstrait réalise le Système de Transitions étiquetées de la machine B précisée par NomFichierAvecExtension.

Methods inherited from class MethodesNonFonctionnelles

AfficheStatistiques, AfficheTabInt, AfficheTabInt, AppelCommandeExterne, AppelCommandeExterneAvecScript, Conjonction, Disjonction, DonneExtension, Donner_Extension, EnleveExtension, FusionneTabOfInt, GestionNomDeProjet, IntNonPresent, inverseVecteur, LanceScriptExterne, NouveauNomDeFichier, RechercheElement, replaceAll, replaceAll, SansChemin, SysAfficher

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

VersionGS

public static final java.lang.String VersionGS

See Also:

Constant Field Values

FaireOPExistentielle

private boolean FaireOPExistentielle

CheminEtNomFichierAbstrProduitAuFormatDot

public static java.lang.String CheminEtNomFichierAbstrProduitAuFormatDot

CheminEtNomFichierRaffProduitAuFormatDot

public static java.lang.String CheminEtNomFichierRaffProduitAuFormatDot

IAB

public PreuveAB_tmp IAB

ExporterCommentaire

public static boolean ExporterCommentaire

DonnerNombreDePreuves

public static boolean DonnerNombreDePreuves

Constructor Detail

geneSyst

public geneSyst()

Method Detail

DonneEtatAbstraitCorrespondant

private int DonneEtatAbstraitCorrespondant(bob.predicat.TPredicat EtatR,
                                           int NumEtatR,
                                           java.util.Vector<bob.predicat.TPredicat> preds_disjA,
                                           GestionFormatIntermediaire STEInt,
                                           boolean QueGenererOP)
                                    throws java.io.FileNotFoundException,
                                           java.io.IOException,
                                           ErreurException

DonneEtatAbstraitCorrespondant recherche, par la preuve quel état du vector preds_disjA est équivalent au prédicat EtatR.

Parameters:

EtatR - Etat raffiné

NumEtatR - Numéro de l'état Raffiné

preds_disjA - Ensemble des états abstraits

STEInt - Structure de donnée représentant toute les connaissances que l'on a du graphe comportementale à ce niveau là.

QueGenererOP - Vrai si et seulement si l'on veut générer l'ensemble des obligations de preuve sans pour autant les prouver. Dans le cas particulier de cette méthode, les preuves ont quand même lieu car si ce n'était pas le cas alors on ne connaitrait pas l'association des états par là même ont ne pourrais rien faire par la suite.

Returns:

numéro, dans la disjonction abstraite, de l'état équivalent ou -1.

Throws:

java.io.FileNotFoundException

java.io.IOException

ErreurException

RechercheEtatsInitiaux

private void RechercheEtatsInitiaux(bob.substitution.TSubstitution Initialisation,
                                    java.util.Vector<bob.predicat.TPredicat> preds_disj,
                                    int[] AssociationEquivalenceEtats,
                                    GestionFormatIntermediaire STEInt,
                                    GestionFormatIntermediaire STEAbstrait,
                                    boolean QueGenererOP,
                                    boolean VerifierOracle)
                             throws java.io.IOException,
                                    ErreurException

RechercheEtatsInitiaux recherche la liste des état initiaux du ststème de transitions et renvoie son résultat sous forme d'uin vercteur de TEtats.

Parameters:

Initialisation - la substitution du fichier original

preds_disj - Ensemble des états

AssociationEquivalenceEtats - Liste des équivalences entre les états abstraits et les états raffinés

STEInt - informations connues du STE sous la forme du format intermédiaire utilisé

STEAbstrait - informations connues du STE de la machine abstraite associée

QueGenererOP - Si vrai alors on ne fait que générer les obligations de preuves. On n'effectue aucune preuve.

VerifierOracle - Si vrai alors l'oracle est utiliser pour diriger la génération des obligations de preuve. Sinon, il est pris comme étant correct et aucune OP n'est vérifiée.

Throws:

java.io.IOException

ErreurException

PointArriveeTransitionTjrsAtteignable

private java.lang.String PointArriveeTransitionTjrsAtteignable(int Etati,
                                                               int Evenementj,
                                                               int Etatk,
                                                               GestionFormatIntermediaire STEInt,
                                                               bob.predicat.TPredicat AttSansCond,
                                                               java.lang.String NMF,
                                                               java.lang.String NMG)
                                                        throws java.io.IOException,
                                                               ErreurException

Throws:

java.io.IOException

ErreurException

PointArriveeTransitionNonAtteignable

private java.lang.String PointArriveeTransitionNonAtteignable(int Etati,
                                                              int Evenementj,
                                                              int Etatk,
                                                              GestionFormatIntermediaire STEInt,
                                                              bob.predicat.TPredicat NonAtt,
                                                              java.lang.String NMT,
                                                              java.lang.String NMG)
                                                       throws java.io.IOException,
                                                              ErreurException

Throws:

java.io.IOException

ErreurException

PointArriveeTransitionPossibAtteignable

private java.lang.String PointArriveeTransitionPossibAtteignable(int Etati,
                                                                 int Evenementj,
                                                                 int Etatk,
                                                                 GestionFormatIntermediaire STEInt,
                                                                 bob.predicat.TPredicat PossAtt,
                                                                 bob.predicat.TPredicat NonEvDeNonF,
                                                                 java.lang.String NMT,
                                                                 java.lang.String NMF)
                                                          throws java.io.IOException,
                                                                 ErreurException

Throws:

java.io.IOException

ErreurException

RecherchePointArriveeDesTransition

private void RecherchePointArriveeDesTransition(int Etati,
                                                int Evenementj,
                                                java.util.Vector<bob.predicat.TPredicat> preds_disj,
                                                java.util.Vector<bob.composant.TOperation> ops,
                                                boolean[][][] ListeTransitionsEffectuables,
                                                GestionFormatIntermediaire STEInt,
                                                boolean QueGenererOP,
                                                boolean VerifierOracle)
                                         throws java.io.IOException,
                                                ErreurException

RecherchePointArriveeDesTransition recherche quels sont les conditions d'atteignabilité de chacun des états de preds_disj par l'événement Evenementj depuis l'état Etati. Cette procédure utilise les sous procédures PointArriveeTransitionPossibAtteignable, PointArriveeTransitionNonAtteignable et PointArriveeTransitionTjrsAtteignable pour determiner ces conditions.

Si une condition est fausse alors la transition n'existe pas.

Parameters:

Etati - Etat de départ traité

Evenementj - Evénement traité

preds_disj - Ensemble des états

ops - Liste des événements. Seul Evenementj nous intéresse dans cette liste.

ListeTransitionsEffectuables - ensemble des transitions effectuables dans l'abstraction

STEInt - informations connues du STE sous la forme du format intermédiaire utilisé

QueGenererOP - Si vrai alors on ne fait que générer les obligations de preuves. On n'effectue aucune preuve.

VerifierOracle - Si vrai alors l'oracle est utiliser pour diriger la génération des obligations de preuve. Sinon, il est pris comme étant correct et aucune OP n'est vérifiée.

Throws:

java.io.IOException

ErreurException

DeclenchabiliteDesTransitions

private void DeclenchabiliteDesTransitions(int[] ListeEtatsDepart,
                                           java.util.Vector<bob.predicat.TPredicat> preds_disj,
                                           java.util.Vector<bob.composant.TOperation> ops,
                                           boolean[][][] ListeTransitionsEffectuables,
                                           boolean[][] ListeTransitionsDeclenchables,
                                           GestionFormatIntermediaire STEInt,
                                           boolean QueGenererOP,
                                           boolean VerifierOracle)
                                    throws java.io.IOException,
                                           ErreurException

DeclenchabiliteDesTransitions recherche quels sont les couples d'états (E1,E2) possibles tels que pour un événement Ev donné on ait : E1 - Ev -> E2 Le calcul de l'état d'arrivé est déporté dans la méthode RecherchePointArriveeDesTransition.

Cette méthode calcule également la condition sous laquelle chaque transition est déclenchable depuis l'état de départ donné.

Parameters:

ListeEtatsDepart - etats de départ traités

preds_disj - Ensemble des états

ops - Liste ds opérations

ListeTransitionsEffectuables - ensemble des transitions effectuables dans l'abstraction

ListeTransitionsDeclenchables - ensemble des transitions déclenchables dans l'abstraction

STEInt - informations connues du STE sous la forme du format intermédiaire utilisé

QueGenererOP - Si vrai alors on ne fait que générer les obligations de preuves. On n'effectue aucune preuve.

VerifierOracle - Si vrai alors l'oracle est utiliser pour diriger la génération des obligations de preuve. Sinon, il est pris comme étant correct et aucune OP n'est vérifiée.

Throws:

java.io.IOException

ErreurException

TraitementSystemeAbstrait

private ResultatAnalyse TraitementSystemeAbstrait(java.lang.String NomFichierAvecExtensionEtChemin,
                                                  int Force,
                                                  boolean Nettoyer,
                                                  GestionFormatIntermediaire STEInt,
                                                  boolean QueGenererOP,
                                                  boolean VerifierOracle)
                                           throws tatibouet.bparser.ParseException,
                                                  tatibouet.bparser.AfterParserException,
                                                  java.io.FileNotFoundException,
                                                  java.io.IOException,
                                                  ErreurException

TraitementSystemeAbstrait réalise le Système de Transitions étiquetées de la machine B précisée par NomFichierAvecExtension.

Parameters:

NomFichierAvecExtensionEtChemin - Nom du fichier source avec son extension

Force - Niveau de force à utiliser pour les preuves

Nettoyer - Si vrai alors on efface tous les fichiers temporaires à la fin des calculs

SDefaut - Symbole pour le graph final pour le cas de transitions conditionnées

SProuve - Symbole pour le graph final pour le cas de transitions non conditionnées

STEInt - informations connues du STE sous la forme du format intermédiaire utilisé

QueGenererOP - Si vrai alors on ne fait que générer les obligations de preuves. On n'effectue aucune preuve.

VerifierOracle - Si vrai alors l'oracle est utiliser pour diriger la génération des obligations de preuve. Sinon, il est pris comme étant correct et aucune OP n'est vérifiée.

Returns:

L'ensemble des données nécessaires pour réaliser le STE

Throws:

tatibouet.bparser.ParseException

tatibouet.bparser.AfterParserException

java.io.FileNotFoundException

java.io.IOException

ErreurException

TraitementRaffinement

private ResultatAnalyse TraitementRaffinement(java.lang.String NomFichierAvecExtensionEtChemin,
                                              ResultatAnalyse ResultatAnalyseSystemeAbstrait,
                                              int Force,
                                              boolean Nettoyer,
                                              GestionFormatIntermediaire STEIntermediaireAbstrait,
                                              GestionFormatIntermediaire STEInt,
                                              boolean QueGenererOP,
                                              boolean VerifierOracle)
                                       throws tatibouet.bparser.ParseException,
                                              tatibouet.bparser.AfterParserException,
                                              java.io.FileNotFoundException,
                                              java.io.IOException,
                                              ErreurException

TraitementRaffinement réalise le Système de Transitions étiquetées du raffinement B précisé par NomFichierAvecExtension.

Parameters:

NomFichierAvecExtensionEtChemin - Nom du fichier source avec son extension

ResultatAnalyseSystemeAbstrait - Résultat de l'analyse de l'abstraction

Force - Niveau de force à utiliser pour les preuves

Nettoyer - Si vrai alors on efface tous les fichiers temporaires à la fin des calculs

SDefaut - Symbole pour le graph final pour le cas de transitions conditionnées

SProuve - Symbole pour le graph final pour le cas de transitions non conditionnées

STEIntermediaireAbstrait - informations connues du STE sous la forme du format intermédiaire utilisé

STEInt - informations connues du STE sous la forme du format intermédiaire utilisé

QueGenererOP - Si vrai alors on ne fait que générer les obligations de preuves. On n'effectue aucune preuve.

VerifierOracle - Si vrai alors l'oracle est utiliser pour diriger la génération des obligations de preuve. Sinon, il est pris comme étant correct et aucune OP n'est vérifiée.

Returns:

ResultatAnalyse L'ensemble des données nécessaires pour réaliser le STE

Throws:

tatibouet.bparser.ParseException

tatibouet.bparser.AfterParserException

java.io.FileNotFoundException

java.io.IOException

ErreurException

GenerationDesSTE

public boolean GenerationDesSTE(java.lang.String NomFichierAbstraitAvecExtensionEtChemin,
                                java.lang.String NomFichierRaffinementAvecExtensionEtChemin,
                                int Force,
                                boolean Nettoyer,
                                char SDefaut,
                                char SProuve,
                                char SNonPr,
                                boolean QueGenererOP,
                                boolean VerifierOracle,
                                java.lang.String NomFichierOracleMch,
                                java.lang.String NomFichierOracleRaff,
                                boolean FaireExistentielle)

GenerationDesSTE réalise les Systèmes de Transitions Etiquetés (STE) du raffinement et de la machine B précisés.

Parameters:

NomFichierAbstraitAvecExtensionEtChemin - Nom du fichier source de l'abstraction avec son extension

NomFichierRaffinementAvecExtensionEtChemin - Nom du fichier source du raffinement avec son extension

Force - Niveau de force à utiliser pour les preuves

Nettoyer - Si vrai alors on efface tous les fichiers temporaires à la fin des calculs

SDefaut - Symbole pour le graph final pour le cas de transitions conditionnées

SProuve - Symbole pour le graph final pour le cas de transitions non conditionnées

QueGenererOP - Si vrai alors on ne fait que générer les obligations de preuves. On n'effectue aucune preuve.

VerifierOracle - Si vrai alors l'oracle est utiliser pour diriger la génération des obligations de preuve. Sinon, il est pris comme étant correct et aucune OP n'est vérifiée.

NomFichierOracleMch - Nom du fichier d'oracle pour l'abstraction

NomFichierOracleRaff - Nom du fichier d'oracle pour le raffinement

FaireExistentielle - Si vrai, alors les obligations de preuve existentielles seront produites et, le cas échéant, prouvées.

Returns:

Renvoie faux ssi la génération a été annulée.

main

public static void main(java.lang.String[] args)

Procédure principale. Elle traite les informations données en ligne de commande et lance le traitement.

Note : Cette procédure n'est pas appelée si l'interface graphique est utilisée.

Parameters:

args - les paramètres passés en ligne de commande