Version du 26/08/2010 Fait par Nico-S * Correction de la tactique 'seulement les OP false' quand tactiques utilisateur choisies * Correction du bug de fermeture des fenetres SLTS via la croix. ------------------------------------------------------------------------- Version du 15/08/2009 Fait par Nico-S * Réalisation d'une nouvelle interface Graphique * Passage du développement sous NetBeans. ------------------------------------------------------------------------- Version du 11/08/2009 Fait par Nico-S * Prise en charge de l'atelierB Version 4 ------------------------------------------------------------------------- Version du 09/07/2009 Fait par Nico-S * simplification des OP générées si les états sont déclarés comme mutuellement disjoints * Non génération d'OP lorsque l'événement est syntaxiquement réductible à skip (Atteignabilité et Déclenchabilité) ou à G => skip (atteignabilité seulement) * Possibilité de ne générer que les OP False ------------------------------------------------------------------------- Version du 04/06/2009 Fait par Nico-S * Remplacement des vecteurs en ArrayList --> normalement plus efficace ------------------------------------------------------------------------- Version du 26/05/2009 Fait par Nico-S * Correction de la simplification skip et du comptage des OP + introduction de la tactique 'seulement les OP false' * Correction affichage version * Correction du jeu de test par rapport aux tactiques utilisateur. ------------------------------------------------------------------------- ************************************************************************* ******************** Mise sous SVN ********************** ************************************************************************* ------------------------------------------------------------------------- ************************************************************************* ******************** Version de diffusion V0.1.8 ********************** ************************************************************************* ------------------------------------------------------------------------- Version du 19/05/2007 Fait par Nico-S * Mise en Jar de l'application de toutes ses dépendances. ------------------------------------------------------------------------- ************************************************************************* ******************** Version de diffusion V0.1.7.2 ********************** ************************************************************************* ------------------------------------------------------------------------- Version du 30/08/2007 Fait par Nico-S * Ajout de la gestion des tactiques utilisateur si l'atelier B n'est pas en parallèle. ------------------------------------------------------------------------- Version du 19/08/2007 Fait par Nico-S * Génération de l'oracle AVANT les autres résultats pour ne pas risquer de tout perdre * Ajout de l'affichage du nombre de preuve durant l'exécution si le mode DEBUG est activé. ------------------------------------------------------------------------- Version du 14/07/2007 Fait par Nico-S * Calcul des déclenchabilité à false avant true * Sortie possible du nombre de preuve pour tests ------------------------------------------------------------------------- Version du 16/04/2007 Fait par Nico-S * Mise en place de scripts de lancement user-friendly * Dans les machines Crées pour la preuve de formules, les variables sont changées en constantes afin de diminuer le temps de génération d'obligations de preuve et le temps de preuve associés à l'initialisation. ------------------------------------------------------------------------- Version du 14/02/2007 Fait par Nico-S * Possibilité de ne pas exporter de commentaire dans les oracle, afin de faciliter le dépiotage automatique des tests de non régression * Mise en place d'une batterie de tests de non régression avec dépouillage automatique * Simplification de l'algo de calcul des atteignabilités * Prise en compte des simplifications par raffinement du calcul d'atteignabilité. * Par raffinement, les transitions ne peuvent pas faire plus que dans l'abstraction ------------------------------------------------------------------------- Version du 09/11/2005 à 10h30 Fait par Nico-S * Correction de l'appel au proveur fait lors de sa mise en parallèle ------------------------------------------------------------------------- Version du 08/11/2005 à 15h30 Fait par Nico-S * Correction de l'affichage de l'icone de GénéSyst ------------------------------------------------------------------------- ************************************************************************* ******************** Version de diffusion V0.1.7.1 ********************** ************************************************************************* ------------------------------------------------------------------------- Version du 08/11/2005 à 10h45 Fait par Nico-S * Possibilité d'affichage des 2 composants, dans le cas de la prise en compte d'un raffinement. * Correction de quelques problèmes d'affichage de l'interface graphique. * Correction de la prise en charge de B4free dans le "nettoyage" des projets ------------------------------------------------------------------------- ************************************************************************* ******************** Version de diffusion V0.1.7 ************************ ************************************************************************* ------------------------------------------------------------------------- Version du 04/11/2005 à 12h Fait par Nico-S * Prise en charge du prouveur de B4free en plus de celui de l'atelier B. ------------------------------------------------------------------------- Version du 02/11/2005 à 12h Fait par Nico-S * Ajout de la possibilité de visualiser le résultat produit directement au travers de l'interface graphique. ------------------------------------------------------------------------- ************************************************************************* ******************** Version de diffusion V0.1.6-a.3 ******************** ************************************************************************* ------------------------------------------------------------------------- Version du 11/10/2005 à 12h Fait par Nico-S * Correction de la prise en compte des oracles (Ils n'étaient plus pris en compte depuis les dernières modifications) ------------------------------------------------------------------------- ************************************************************************* ******************** Version de diffusion V0.1.6-a.2 ******************** ************************************************************************* ------------------------------------------------------------------------- Version du 27/05/2005 à 12h Fait par Nico-S * mettre les oracles dans le dossier résultat ------------------------------------------------------------------------- Version du 16/05/2005 à 17h Fait par Nico-S * Pas de calcul des OP existencielles si ce n'est pas demander ------------------------------------------------------------------------- Version du 03/03/2005 à 11h Fait par Nico-S * Intégration de la nouvelle BoB ------------------------------------------------------------------------- Version du 03/01/2005 à 11h Fait par Nico-S * Correction de la génération des fichiers HTML. ------------------------------------------------------------------------- ************************************************************************* ********************* Version de diffusion 0.1.6.1 ********************** ************************************************************************* ------------------------------------------------------------------------- Version du 27/12/2004 à 11h Fait par Nico-S * Correction de la recherche des états initiaux dans le cas de défaut de preuve. ------------------------------------------------------------------------- Version du 24/12/2004 à 14h Fait par Nico-S * Intégration de la nouvelle version de la BoB ------------------------------------------------------------------------- Version du 22/12/2004 à 14h Fait par Nico-S * GUI : Calculer la taille et la position de chaque fenêtre en fonction de celles de la fenêtre principale. * GUI : Affichage de la version de GénéSyst sur la fenêtre. * GUI : Optimisation et correction des effacages de dossiers et projets. ------------------------------------------------------------------------- Version du 21/12/2004 à 14h Fait par Nico-S * GUI : Activation des ascensseurs sur le panel "format de sortie" ------------------------------------------------------------------------- Version du 20/12/2004 à 12h Fait par Nico-S * Amélioration de la prise en des erreurs par exception. * Ajout des options de personnification de la condition existentielle dans l'interfaces GUI * Affichage du nom des dossiers résultats produits. * Ajout d'un message d'erreur si aucune variables dans la machine * GUI : Gestion des boutons de fermeture des fenêtre * GUI : Correction de l'affichage des listing trop longs de dossiers/projets à effacer. ------------------------------------------------------------------------- Version du 16/12/2004 à 10h Fait par Nico-S * Ajout du choix de l'OP existentielle sur l'interface texte. * Ajout du choix du charactère de l'OP exist. sur l'interface texte. * Débugage de la fonction d'exportation DOT (dans le cas sans HTML) ------------------------------------------------------------------------- Version du 15/12/2004 à 16h Fait par Nico-S * Récupération des erreurs si mode graphique * En cas d'erreur, rajout de la trace de la pile d'appel * Correction du BUG suivant : Dans certains cas Declenchabilité gardée -> pas de calcul de l'atteignabilité. * Améliorations subtiles de l'interface graphique. * Propagation et prise en compte du choix de faire ou non les OP existentielles ------------------------------------------------------------------------- Version du 14/12/2004 à 18h Fait par Nico-S * Passage au J2SDK 1.5.0 avec généricité des vecteurs * Ne pas mettre les variables et l'invariant lors d'un calcul de AvecG ------------------------------------------------------------------------- Version du 10/11/2004 à 12h Fait par Nico-S * Rajout du cas AvecG dans l'algo du calcul de la déclenchabilité. * Simplification du calcul de l'atteignabilité ------------------------------------------------------------------------- Version du 10/11/2004 à 12h Fait par Nico-S * Réécriture de l'algo de calcul de l'atteignabilité. * Intégration totale du status supplémentaire NonPr. * Ajout de la simplification automatique des atteignabilités. ------------------------------------------------------------------------- ************************************************************************* ********************* Version de diffusion 0.1.5.1 ********************** ************************************************************************* ------------------------------------------------------------------------- Version du 09/11/2004 à 10h Fait par Nico-S * Correction d'un gros bug de GFI entrainant un graphe faux lors de l'exportation. * Remise en place de commentaires et réindentation d'une grosse partie de GFI. ------------------------------------------------------------------------- ************************************************************************* ********************** Version de diffusion 0.1.5 *********************** ************************************************************************* ------------------------------------------------------------------------- Version du 30/09/2004 à 18h Fait par Nico-S * Correction de certains bug d'affichage. * Correction de commentaires. * Ajout d'une icone à GénéSyst en mode graphique :o) * Possibilité d'utiliser des fichiers qui ne sont pas dans le dossier courrant (prise en compte des chemins et recopie en local dans le dossier de travail) * Effacement du fichier de trace après exécution si nettoyer est à vrai. ------------------------------------------------------------------------- Version du 16/08/2004 à 15h30 Fait par Nico-S * Intégration complète de PrintWriterGeneSyst dans l'affichage des traces de GeneSyst. * Simplification de la trace d'exécution minimale (pour la rendre vraiment minimaliste) ------------------------------------------------------------------------- Version du 16/08/2004 à 12h Fait par Nico-S * Modification de l'indentation et des commentaires des méthodes de calcul de l'atteignabilité et de la déclenchabilité (geneSyst.java). * Intégration de StockDecl et StockAtt dans NouvDecl et NouvAtt (GFI_Datas.java). * Réalisation de la classe PrintWriterGeneSyst permettant de factoriser toute la gestion de la présentation. ------------------------------------------------------------------------- Version du 13/08/2004 Fait par Nico-S * Modification de l'indentation et des commentaires de la méthode de calcul de l'initialisation (geneSyst.java). * Intégration de StockInit dans NouvInit (GFI_Datas.java). ------------------------------------------------------------------------- version du 06/08/2004 à 10h30 Fait par Mohamed Hounayda * modification geneSyst.java pour pouvoir appeler GenerationGXL quand il le faut. * Modification du dernier parametre de GenerationDOT qui est desormais le nom du dossier resultat après calcul. ce qui permet de le mettre aussi en parametre pour GenerationGXL si jamais les deux formats sont demandés par l'utilisateur. ------------------------------------------------------------------------- version du 05/08/2004 à 16h Fait par Mohamed Hounayda * Creation Methode GenerationGXL qui permet de generer un fichier gxl * Ajout d'une variable static FormatGxl representant l'indice du format gxl du tableau TabFormatsSortie. * Ajout d'une case dans la fenetre AppliGene permettant de selectionner le format GXl ------------------------------------------------------------------------- version du 05/08/2004 à 13h Fait par Mohamed Hounayda * Ajout d'une methode ConvertDisjEtats qui a pour effet de convertir des disjonctions d'état en tableaux de chaines. Cette methode était faite entierement dan GenerationDOT,étant donné qu'on en a besoin pour GenerationGXL, on l'a sort de la methode comme ça elle est independante. ------------------------------------------------------------------------- version du 03/08/2004 à 15h Fait par Mohamed Hounayda * modification AppliGene : le format DOT est obligatoirement choisi avec le format html.Au moins un format de sortie doit être sélectionné au moment de lancer l'outil. * modification GFI_Exportation: - le fichier DOT qui est généré est mis desormais dans le dossier résultat - Si l'on ne génère pas d'html alors les dossiers "Etats", "Clusters" et "Transitions" ne doivent pas être crées ------------------------------------------------------------------------- version du 30/07/2004 Fait par Mohamed Hounayda * Ajout de commentaires: - Appligene - GestionAffichage - GestionNettoyer - gestionOnglet - ModeNettoyer - ModeNettoyerDossier - TextWriter - GFI_Datas - GFI_Exportation ------------------------------------------------------------------------- version du 29/07/2004 à 11h Fait par Mohamed Hounayda * Modification de GFI_Exportation.Ajout d'une function java replaceAll() permettant de remplacer les caracteres speciaux \n contenu dans les noms des etats d'un raffinement(pour qu'il ne s'affiche pas dans le fichier hml).Mais à revoir car la function ne marche pas.Elle ne change rien au string qui lui est donné. ------------------------------------------------------------------------- version du 27/07/2004 à 11h Fait par Mohamed Hounayda * creation d'un tableau TabFormatsSortie de boolean contenant des affirmations pour tel ou tel formats de sortie (dans GFI_datas).Cette variable est static.On le rempli grace aux ecouteurs evenements de la fenetre principale (dans AppliGene). * Ajout de deux constantes FormatDot et Formathtml dans GFI_datas correspondant a l'indice dans le tableau definit precedemment. ------------------------------------------------------------------------- version du 26/07/2004 à 14h Fait par Mohamed Hounayda * Ajout d'une varible dans ConfigurationGeneSyst fournissant le chemin d'acces de la commande dot (PathDot). * modification de la function AppelCommandeExterne de MethodesNonFonctionnelles. Elle est en static pour pouvoir l'utiliser afin d'executer la commande dot dans GFI_Exportation. ------------------------------------------------------------------------- version du 26/07/2004 à 10h30 Fait par Mohamed Hounayda * Ajout d'une variable static NomFichierHtml dans ConfigurationGeneSyst ------------------------------------------------------------------------- version du 23/07/2004 à 13h30 (Nico-S) * Les choix par défaut pour les paramètres étant déjà définis dans les classes ConfigurationGeneSyst et MéthodesNonFonctionnelles, L'interface graphique utilise maintenant les mêmes sources. ------------------------------------------------------------------------- version du 23/07/2004 à 12h40 (Nico-S) * Reprise de la gestion du dossier pour l'exportation du graphe au format HTML. * Modification des classes MethodesNonFonctionnelles, GFI_Exportation et geneSyst. ------------------------------------------------------------------------- Liste des classes de génésyst modifiées dans la version du 22/07/2004 de 11h30 * geneSyst * MethodeNonFonctionnelles * GFI_Datas * QuadrupletEntiers * GFI_Exportations * ConfigurationGeneSyst ------------------------------------------------------------------------- version du 22/07/2004 à 11h30 Fait par Mohamed Hounayda * Ajout dans la fonction RecherchePointArriveeDesTransition de geneSyst d'une variable locable TPredicat NonEvDeNonF qui correspond à la condition d'atteignabilité (non [ev] non F). ------------------------------------------------------------------------- version du 22/07/2004 Fait par Mohamed Hounayda Petit récapitulatif sur les nouvelles classes servant à l'interface * AppliGene: classe possedant le main.Elle affiche la premiere fenetre qui invite l'utilisateur à choisir les options et à lancer geneSyst. C'est dans cette classe que l'objet geneSyst a été crée.Et donc on y fait appel a la fonction GenerationDesSTE de geneSyst. - La case permettant de cocher une verification d'oracle ne sera activer que si un nom d'oracle sera spécifié. - Le bouton lancer permettant la GenerationDesSTE n'est aussi activé que si un nom de machine est donné. Ces verifications de noms se font grace a l'evenement creé par le mouvement du curseur de la zone de text TextField. - Enfin, lorsque la case QueGenererOP est cocher la spécification du niveau de force,des oracles et donc de verifier oracle sont désactivés. - Apres une selection de fichier grace au bouton parcourir,une verification sur l'extension du fichier est faite automatiquement et permet à l'utilisateur de choisir un autre fichier. - Apres le lancement de la generation une autre verification est faite car l'utilisateur peut avoir specifier lui meme ses fichiers. * GestionAffichage : Elle est appelé par AppliGene lors du lancement de geneSyst. Elle permet de visualiser toutes les informations qui étaient auparavant afficher sur le terminal. - la zone de text est rempli au fur est à mesure qu'un flush() est appelé - la barre de defilement se positionne au bas au textArea ce qui permet de toujours voir la dernier ligne inserée. - le bouton retour pemet de revenir à la premiere fenetre. * GestionNettoyer: Elle reprend la classe initiale Nettoyer en gardant toutes ces fonctions fonctions de nettoyage. Sachant qu'elle est en interaction avec la classe ModeNettoyer. - son constructeur definit les dossiers à nettoyer si c'est l'objet ModeNettoyerDossier qui l'appelle.sinon si ModeNettoyer alors,il definit les projets à nettoyer.Un message d'avertissement apparait lorsqu'il n'y a rien à nettoyer. Ensuite renvoie les dossiers à la classe appelant afin de pouvoir les afficher; - De plus il possede des fonctions de nettoyage totalité des projets (dossiers) et nettoyage cas par cas des projets(dossiers).ces fonctions s'inspire de la classe nettoyer initiale. * GestionOnglets : Celle ci est une fenetre qui ne sert qu'à contenir deux onglets offrant le nettoyage des projets et des dossiers. - creation des deux objets ModeNettoyer et ModeNettoyerDossier. * ModeNettoyer : cette classe est un panneau d'affichage permettant le gerer le nettoyage des projets. Cette classe est le premier onglet de la fenetre gerée par GestionOnglets. * ModeNettoyerDossier : celle ci herite de la classe ModeNettoyer et elle permet de gerer le nettoyage des dossiers.Cette classe est le premier onglet de la fenetre gerée par GestionOnglets. * TextWriter : classe heritant de PrintWriter et permet d'afficher le contenu de la variable terminal de geneSyst non plus dans le terminal mais dans le TextArea de la fenetre GestionAffichage.Donc redefinition des fonctions writer() et flush() de PrintWriter. -------------------------------------------------------------------------- version du 21/07/2004 Fait par Mohamed Hounayda * Apres avoir remarquer que les preuves sont réalisé avant que les listes des EtatsInitiaux, des evenements declanchables et atteignables ne soient initiés, l'appel des fonctions de stockage des assertions ne peut plus se faire dans PreuveAB_temp. * D'où le retablissement de la classe PreuveAB_temp comme elle était auparavant. * L'appel des fonctions de stockage des assertions se fait alors dans la classe geneSyst à chaque fois que l'on vient d'initialiser un etatInit, un evenementDecl ou un evenementAtt . ------------------------------------------------------------------------- version du 20/07/2004 à 10h00 Fait par Mohamed Hounayda * ajout d'une variable dans GFI_Datats public static final int Declenchable=0 - elle sert à savoir dans quelle table recuperer les informations (est ce dans DeclConnues,AttConnues ou EtatsInitiaux) - elle n'est utiliser que dans GFI_exporations dans les fonctions: GenerationTransitionHTML() et AffichageGarde() * Modification du constructeur de PreuveAB_temp, ajout d'un objet GestionFichierIntermediaire * Appel des fonctions de stockage des assertions dans CreationFichierAB de PreuveAB_temp * Modification de la classe QuadrupletEntiers: Ajout d'un objet TPredicat * Dans GFI_Datas, creation: - trois fonctions de stockage des predicats (EtatsInitiaux, Declanchable et Atteignable) - trois fonctions d'accessibilité des predicats * Dans GFI_Exportation: - ajout de trois fonctions pour la creation des fichiers HTML en fonction de Clusters, Etats, Transitions ------------------------------------------------------------------------- version du 16/07/2004 Fait par Mohamed Hounayda * Ajout d'une constante NomDossierResultat dans la classe ConfigurationGeneSyst pour la creation dossier Resultats * creation des dossiers - Resultats/Etats - Resultats/Transitions - Resultats/Clusters dans la classe geneSyst dans la fonction GenerationDesSTE * Modification de la classe GFI_Exportation - Ajout de trois fonctions permettant de creer les fichiers html - Modification du fichier .dot en introduisant les closes URL ------------------------------------------------------------------------- ************************************************************************* ********************** Version de diffusion 0.1.4 *********************** ************************************************************************* ------------------------------------------------------------------------- version du 13/07/2004 (Nico-S) * Relecture et corrections minimes diverses. ------------------------------------------------------------------------- version du 04/04/2004 (Nico-S) * supression du bug de "outOfBoundException" de la méthode NbCluster() ------------------------------------------------------------------------- version du 27/04/2004 (Nico-S) * PreuveAB_tmp : retrait des fichiers du projet après qu'ils aient été prvoués et que leur taux de preuve ait été lu (L:464) * GFI_Datas : Correction de la méthode NbClusters() qui peut aboutir dans un arrayoutofBoundexception Rajout d'un test sur la nullité de ListeEtatsParCluster * geneSyst : Génération des fichiers produit par l'analyse de la machine avant de commencer l'analyse du raffinement. * MéthodesNonFonctionnelles : L413 : changement d'un '&' en '&&' ------------------------------------------------------------------------- version du 22/04/2004 (Xavier) Etape 1 (Fini): Ajout d'un nouveau paramétre dans le main généSyst : Oui/Non faire la vérification de l'oracle .Dans la class geneSyst.java -> Dans la méthode "GenerationDesSTE" ajout du paramétre "VerifierOracle" -> Dans la méthode "TraitementSystemeAbstrait" ajout du paramétre "VerifierOracle" -> Dans la méthode "TraitementRaffinement" ajout du paramétre "VerifierOracle" -> Dans la méthode "RechercheEtatsInitiaux" ajout du paramétre "VerifierOracle" -> Dans la méthode "DeclenchabiliteDesTransitions" ajout du paramétre "VerifierOracle" Etape 2 (Fini) : Modification de l'initiabilité : ATTENTION : COMMENTAIRES NON FAITS. .Dans la classe geneSyst.java : -> Dans la methode "RechercheEtatsInitiaux" prise en compte de l'oracle. .Tests effectués : Pour : java geneSyst m.mch -OM OracleTest.Oracle -V false java geneSyst m.mch -OM OracleTest.Oracle -V false J'obtiens le meme état initial. Pour : java geneSyst parking_r1.mch java geneSyst parking_r1.mch -OM IndexMachinesAbstr.Oracle -V true java geneSyst parking_r1.mch -OM IndexMachinesAbstr.Oracle -V false J'obtiens le meme état initial. Etape 3 (Fini ) : Modification de la décidabilité: .Dans la classe GFI_DATA.java --> Ajout de la méthode : public int IndiceDansVector(Vector L,int Etat1, int Etat2, int Ev, int Pr) qui recherche de l'indice d'un élément particulier dans un vecteur de QuadrupletEntiers. --> Modification de la méthode : void NouvDecl(int Etat,int Ev,int Pr,String FT, String FF) Si un élément est déja présent dans le vector DeclConnues, on le modifie. * Tests effectués : java geneSyst m.mch java geneSyst MachineACafeClassique.mch ATTENTION : COMMENTAIRES NON FAITS. .Dans la classe geneSyst.java : -> Dans la methode "DeclenchabiliteDesTransitions " prise en compte de l'oracle. * Tests effectués : 1) java geneSyst parking_r1.mch -> 35 preuves. 2) java geneSyst parking_r1.mch -OM IndexMachinesAbstr.Oracle -V false -> Nombre de preuves réalisées : 9 3) java geneSyst parking_r1.mch -OM IndexMachinesAbstr.Oracle -V true -> Nombre de preuves réalisées : 13 --> Fichier dot du 1) différent des 2 autres et de celui de test. 1) java geneSyst m.mch ->Nombre de preuves réalisées : 25 2) java geneSyst m.mch -OM OracleTest.Oracle -V true -> Nombre de preuves réalisées : 10 3) java geneSyst m.mch -OM OracleTest.Oracle -V false -> Nombre de preuves réalisées : 17 ---> Fichier dot du 1) identique à celui du fichier de test "m.dot" ---> Fichier dot 2) et 3) identique mais différent du 1) et de celui du test Résultat à revérifier car l'ateignabilité na pas été faite. Etape 4 (Fini): Modification de l'atteignabilité : .Dans la class geneSyst.java -> Dans la méthode "RecherchePointArriveeDesTransition" ajout du paramétre "VerifierOracle" ATTENTION : COMMENTAIRES NON FAITS. .Dans la classe geneSyst.java : -> Dans la methode "DeclenchabiliteDesTransitions " prise en compte de l'oracle. . Tests effectués : 1) java geneSyst parking_r1.mch -> 35 preuves. 2) java geneSyst parking_r1.mch -OM IndexMachinesAbstr.Oracle -V false -> Nombre de preuves réalisées : 9 /** NOUVELLE VALEUR */ 3) java geneSyst parking_r1.mch -OM IndexMachinesAbstr.Oracle -V true -> Nombre depreuves réalisées : 22 --> Fichier dot du 1) différent des 2 autres et de celui de test. 1) java geneSyst m.mch ->Nombre de preuves réalisées : 25 /** NOUVELLE VALEUR */ 2) java geneSyst m.mch -OM OracleTest.Oracle -V true -> Nombre de preuves réalisées :19 3) java geneSyst m.mch -OM OracleTest.Oracle -V false -> Nombre de preuves réalisées : 17 ---> Fichier dot du 1) identique à celui du fichier de test "m.dot" ---> Fichier dot 2) et 3) identique mais différent du 1) et de celui du test Etape 5 (A faire) : Debugage --> Correction des erreurs. ------------------------------------------------------------------------- version du 19/04/2004 (Nicolas) * Intégration des modifications de Xavier * Simplification de la méthode DeclenchabiliteDesTransitions * Simplification de la preuve (si la simplification suffit alors on ne lance pas l'atelier B) * tests * !!!! BUG dans l'exemple DISTRI3 !!!! Ce bug est peut-être plutôt dû à la BoB ------------------------------------------------------------------------- version du 16/04/2004 (Xavier) * Modification de la classe MethodePMI.java --> Execution en paralléle des fichier pmi et po * Modification la fonction Get_AssertionLemmas_V2(String NomSansExt, String Chemin) {...} dans la class InterfaceAB pour prendre en compte le paramétre supplémentaire de la méthode PMI (MethodePMI.java) : le fichier po -- Le test contenu dans ExempleSimpleAvecOracle : m.mch Erreur dans le fichier m.dot. -- Idem pour la MachineASimple.mch -- Le test effectué sur parking.mch ne presente pas d'erreurs. ------------------------------------------------------------------------- version du 16/04/2004 (Xavier) * Lecture du code de l'atteignabilité * Simplification de la déclenchabilité dans genesyst.java * Test avec -> MachineACafe.mch --> Erreur d'execution. -> parking.mch --> parking.dot ------------------------------------------------------------------------- version du 15/04/2004 (Nicolas) : * Terminaison de tous les processus lancés. -> Cela permet de retrouver le prompt après la fin de l'exécution de l'outil. * Simplification de divers appels * Simplification de la méthode de calcul de l'atteignabilité et des états initiaux * Ajout du paramètre "AtelierB en Parallele" en ligne de commande ------------------------------------------------------------------------- version du 14/04/2004 (Nicolas) : * Création de la classe PreuveAB_tmp qui permet de centraliser la génération des OP en attendant que la classe TComposantGeneSyst.java soit prète. * Integration de cette classe, simplification des appels et debuggage * Integration de certaines parties de TComposantGeneSyst.java pour la simplification des calculs. ------------------------------------------------------------------------- version du 07/04/2004 (Nicolas) : * Debuggage de l'implantation de la génération des OP de l'atteignabilité. ------------------------------------------------------------------------- version du 06/04/2004 (Nicolas) : * Débuggage de la fonction de parsage d'un PMI -> Il y avait un Pb lorsque la clause lue contienait plusieurs OP * Simplification des transitions produites sur le fichier DOT par Extension du format des étiquettes. * Ajout d'une attente et d'un jeu d'essais supplémentaire pour l'accès au Fichier PMI. En effet, certaines latences font que le fichier peut mettre quelques centièmes de seconde à être ccessible. * Implantation par une variable "sale" de la possibilité de choix entre garder l'atelier dans un processus parallèle ou le relancer pour chaque résolution d'OP. ------------------------------------------------------------------------- version du 01/04/2004 soir (Xavier) : * Dans "TcomposantGenesyst" -> Dans le groupe 2 : Ajout de : . public Vector preds_disjonctif = new Vector(); // liste des prédicats disjonctifs La question est : est-ce vraiment utile de le rajouter? -> Fin du groupe 3 : ajout de . Tableau des représentations textuelles des états . Représentation textuelle des clauses non traitées . un codage simple de la nature du composant Voir : Est ce qu'on obtient le résultat que l'on attend?? pour le codage simple de la nature du composant, voir pour sa taille et pour les noms des variables attribuées. ------------------------------------------------------------------------- version du 01/04/2004 soir (Xavier) : * Installation de la nouvelle version de GénéSyst * Dans "TcomposantGenesyst" -> mise à jour du groupe 1 -> ajout du groupe 2 et -> une partie du groupe 3. ------------------------------------------------------------------------- version du 01/04/2004 midi (Nicolas) : * Intégration de la lecture du status par fichier PMI interposé * Débuggage, simplification et sécurisation de la classe "MethodesPMI" (1h30 !!!!! Ne t'avais-je pas demandé de la tester ?). -> Méthode PMI fausse car la théorie proof state doit se lire de bas en haut. -> Sécurisation de la méthode Donne_Resultat_Preuve * Simplification des appels de commandes extérieurs selon la technique de Xavier -> Plus rapide et plus sûr. -> Cas flagrant : Méthodes de nettoyage. * Sauvegarde dans un sous dossier de la classe en cours de développement : TComposantGeneSyst. Elle est encore loin d'être finie, je te laisse la continuer. * Mise en place d'un état initial unique dans le graphique généré et explicitation du niveau de preuve de l'atteignabilité des états par la transition Init. * Renommage de geneSyst_alpha en geneSyst (Depuis longtemps déjà ce n'est plus une version alpha ^_^) * Pas de distinction entre le fichier utilisé pour faire une preuve et celui qui est sauvegardé. -> Plus de Pb de nom dans les fichiers SVG -> Identification précise du fichier .PMI utilisé ------------------------------------------------------------------------- version du 29/03/2004 soir (Xavier) : * Modification de la recherche PMI avec le terme "unproved" et teste avec un fichier pmi. * Création de la class TComposantGeneSyst.java -> 1er groupe créé -> d'une méthode Affiche_GroupeA() pr le test * Création d'une class test.java ayant pour méthode main() celle de geneSyst.java excepté l'appel à la méthode GenerationDesSTE() * Resultat.txt contient le résultat de l'execution de : java test ../ExXavier/parking_r1.mch -R ../ExXavier/parking_r2.ref -OM ../ExXavier/IndexMachinesAbstr.Oracle -OR ../ExXavier/IndexMachinesRaff.Oracle ------------------------------------------------------------------------- version du 29/03/2004 (Nicolas) : * Privatisation des variables de "GestionFormatIntermediaire" pour éviter les accès sauvage depuis l'extérieur. * Décomposition de "GestionFormatIntermediaire" en 4 classes (1) GFI_Datas -> Introduction de la strcture de données (2) GFI_Parseur -> Hérite de (1) et introduit un parseur de fichier ".oracle" (3) GFI_Exporte -> Hérite de (2) et introduit différents formats de sortie du STE (oracle, textuel) (4) GestinFormatIntermediaire -> Hérite de (3) et introduit différentes méthodes diverses de haut niveau comme le calcul de la liste des transitions utilisées dans le STE commençant aux états initiaux trouvés. * Introduction de la gestion du nombre d'événements Objectif : Mettre des tableaux pour certaines structures de données de GFI ------------------------------------------------------------------------- version du 25/03/2004 : * Dans le cas du traitement d'un system raffiné, correction du calcul des états initiaux. * Correction de la méthode "RechercheEtatsInitiaux". * Premier débuggage des classe "PreuveAbstract.java" et "PreuveAB.java". * Dans GestionFormatIntermédiaire, modification des méthodes : public static int[] EtatToInt(GestionFormatIntermediaire STEInt) public int[] ArriveeFromTListeTransitionsToInt(GestionFormatIntermediaire STEInt) en public int[] DonneEtatsInit() public int[] DonneEtatsAtteignablesDepuis(int[] EtatsDepart) * Correction du calcul des prochains états à visiter lors de la construction d'un STE. * Correction, optimisation et remise en place de la méthode de génération de fichiers DOT (maintenant intégralement dans MéthodesNonFonctionnelles). ------------------------------------------------------------------------- version du 23/03/2004 : * Retrait des classes non utilisées (TEtats, TTransitions, TListeTransitions) et recompilation => Surprise : il y a des erreurs car ces classes étaient utilisées :o/ -> Retrait de la fonction GénérationBCG car elle n'a pas été mise à jour. -> Dans, GestionFormatIntermediaire, la méthode DonneListeTransition ne peut être statique. +> Retrait de l'argument "static" -> Dans GeneSyst_Alpha, "import java.lang.object.*;" +> Object n'est pas un package. +> Retrait de la clause. -> Dans GeneSyst_Alpha, "TEtat[] EtatsInit = new TEtat[0];" TEtat ne doit plus êtr eutilisé. +> Retrait de la clause. * Mise à 1 de la force de preuve par défaut * Débuggage de l'exportation de l'oracle. (Pb pour les équivalences d'états pour le raffinement datant d'un certain temps déjà) * Repassage des tests après corrections. => Ok. * Création d'un premier jet de la classe abstraite "PreuveAbstract.java" et de son implantation "PreuveAB.java" qui permet une interface plus conviviale avec l'AtelierB, et ouvre les possibilités de couplage à un autre prouveur. ------------------------------------------------------------------------- version du 22/03/2004 soir : * Affichage des états initaux pr le systeme raffiné : * Différents jeu de test dans Résulat_Xav. * Suppression des divers commentaires, * Tar du répertoire Class : Class2203 ------------------------------------------------------------------------- version du 19/03/2004 soir : Fait par XM : * correction du pb lors du traitement d'un système raffiné par GénéSyst sans oracle. * rajout d'un paramétre STEIntermediaireAbstrait dans la méthode TransitionRaffinement(...) de la class geneSyst_alpha.java * test ok pr le raffinement avec ou sans oracle. A faire pr lundi 22 mars 2004 * voir pourquoi l'état initial ne s'affiche pas pr le systeme raffiné : // Liste des états initiaux : * Suppression des divers commentaires, * Réagencement de la class GestionFormatIntermediaire et voir pr la création d'une class MethodesNonFonctionnellesGIF ------------------------------------------------------------------------- version du 08/03/2004 soir : Fait par XM : * Dans la class GestionFormatIntermediaire ajout de méthodes pour le raffinement : -> public static int DonneEtatDepart(Vector Trans,int i) qui donne le numéro de l'état de départ, -> public static int DonneEtatArrivee(Vector Trans,int i) qui donne le numéro de l'état d'arrivée, ->public static int DonneEvenement(Vector Trans,int i) qui donne l'évenement. * Effacement de tous les TlisteTransition,TTransition et TTetat dans la class généSyst. * De meme dans la class ResultatAnalyse. * Test avec Parking_r1.mch avec le raffinement parking_r2.mch avec oracle. --> Pas de probleme Sans oracle il manque les transitions * Création d'une sauvegarde nommé Class040312.tar.gz A VOIR POUR LUNDI 15/03 Pourquoi les transitions dans le fichier.dot ne s'affichent pas lors du test sans oracles ? ------------------------------------------------------------------------- version du 08/03/2004 soir : Fait par XM : PARTIE 1 : * Suppression d'un vector Init dans la class GestionFormatIntermediaire qui contient l'ensemble des états initiaux de la machine * Création d'une methode Afficher dans la class GestionFormatIntermediaire qui permet d'afficher le résultats des transitions. * Création d'une méthode qui retourne la liste des Opération dans GestionFormatIntermédiare. public boolean[] DonneListeOpPresentes(int NbOps){} * Instantiation de 3 nouvelles méthodes non fonctionnelles dans la class GestionFormatIntermédiare: --> public static String StrMoins(int l) {} --> public static String intToStr(int i,int l){ --> public static String strToStr(String Str,int l){ Test effectué sur parking_r1.mch avec et sans oracle. PARTIE 2 : * Dans la méthode GenerateDot(...) de la class MethodeNonFonctionnel, correction d'une erreur lors de la recherche des états initiaux. * Instanciation de la méthode EtatToInt(...) dans la class GestionFormatIntermédiare qui permet de retourner sous forme d'un tableau d'entier, les états initiaux. Test effectué sur parking_r1.mch avec Oracle PARTIE 3 : * Nouveaux Tests : --> parking_r1.mch sans oracle. OK --> MachineACafeClassique.mch OK ------------------------------------------------------------------------- version du 04/03/2004 soir : Fait par XM : * Création d'un vector Init dans la class GestionFormatIntermediaire qui contient l'ensemble des états initiaux de la machine * Dans la methode public void RechercheEtatsInitiaux(...) suppression des TEtat au profit de GestionFormatIntermediaire. * Suppression d'une méthode NouvTransition(int Etat1,int Etat2,int Ev,int Pr,String FT, String FF) qui permet d'inserer dans le vector ListeTransition le quadruplet utilisé pour la transition. * Suppression d'une méthode void DonneListeTransition() qui permet d'inserer dans le vector Transition tous les * Dans la methode public void TraitementSystemeAbstrait(...) suppression des TEtat au profit de GestionFormatIntermediaire. * Dans la methode public void TraitementRaffinement(...) suppression des TEtat au profit de GestionFormatIntermediaire. Test effectué sur parking_r1.mch avec et sans oracle. ------------------------------------------------------------------------- version du 01/03/2004 soir : Fait par XM : * Création d'un vector ListeTransition dans la class GestionFormatIntermediaire qui contient l'ensemble des transitions de la machine * Création d'une méthode NouvTransition(int Etat1,int Etat2,int Ev,int Pr,String FT, String FF) qui permet d'inserer dans le vector ListeTransition le quadruplet utilisé pour la transition. * Création d'une méthode void DonneListeTransition() qui permet d'inserer dans le vector Transition tous les transition. * Création d'une méthode int[] ArriveeFromTListeTransitionsToInt(GestionFormatIntermediaire STEInt) * Dans la methode public void RecherchePointArriveeDesTransition(...) suppression des TListeTransition au profit de GestionFormatIntermediaire. * Dans la methode public void DeclenchabiliteDesTransitions(...) suppression des TListeTransition au profit de GestionFormatIntermediaire. * Dans la methode public void TraitementSystemeAbstrait(...) suppression des TListeTransition au profit de GestionFormatIntermediaire. * Dans la methode public void TraitementRaffinement(...) suppression des TListeTransition au profit de GestionFormatIntermediaire. Test effectué sur parking_r1.mch avec et sans oracle. --------------------------------------------------------------------------------- * Suppression le vector ListeTransition de la class GestionFormatIntermédiaire. Test effectué sur parking_r1.mch avec Oracle ------------------------------------------------------------------------- version du 27/02/2004 soir : Fait par XM * Retrait des classes TEtat dans la procedure :public void GenerationDOT(...) de la class MethodesNonFonctionnelle. * Réalisation de tests : parking_r1.mch et MachineACafeClassique.mch et comparaison des fichiers .dot avec ceux sauvegarder avant la modification. idem avec les .ps * Retrait retrait des commentaires d'affichage dans public void GenerationDOT(...) de la class MethodesNonFonctionnelle. * commenter la procédure écrire de la class GestionIntermediare. * Tar du répertoire Class : Class2702 A faire par XM : * Retrait des classes TEtat dans la procedure :public void GenerationBCG(...) de la class MethodesNonFonctionnelle. * Retrait des TTransition dans la procedure :public void GenerationBCG(...) de la class MethodesNonFonctionnelle. * Elimination progressive des TEtat,TTransition,Transition, en fonction du schéma défini au départ. ------------------------------------------------------------------------- version du 26/02/2004 soir : Fait par XM * Retrait des TTransition dans la procedure :public void GenerationDOT(...) de la class MethodesNonFonctionnelle. A faire par XM : * Retrait des classes TEtat dans la procedure :public void GenerationDOT(...) de la class MethodesNonFonctionnelle. Pb sur l'etat initial. * Retrait retrait des commentaires d'affichage dans public void GenerationDOT(...) de la class MethodesNonFonctionnelle. * commenter la procédure écrire de la class GestionIntermediare. * Retrait des classes TEtat dans la procedure :public void GenerationBCG(...) de la class MethodesNonFonctionnelle. * Retrait des TTransition dans la procedure :public void GenerationBCG(...) de la class MethodesNonFonctionnelle. * Elimination progressiv des TEtat,TTransition,Transition, en fonction du schéma défini au départ. ------------------------------------------------------------------------- version du 23/02/2004 soir : En cours par XM : * Retrait des classes TEtat dans la procedure :public void GenerationDOT(...) de la class MethodesNonFonctionnelle réalisé pb ac les etats initiaux, variable inconnu à testé * Retrait des TTransition dans la procedure :public void GenerationDOT(...) de la class MethodesNonFonctionnelle : Pour cela, création dans GestionFormatIntermédaire d'une procédure écrire() qui écrit dans le fichier dot tous les Transitions possibles entre les états. Affichage des nom des transition ----> ok affichage du nom de chaque état ----> ok PB : ->Problème sur l'écriture de condition de la transition par ex [ ][G] ou [] [] -> utiliser la méthode DonnerDecl(...) pour l'état d'arrivé -> Pb ds la parcours du vector AttConnues ------------------------------------------------------------------------- version du 13/02/2004 soir : Fait par XM : * Retrait des classes TEtat dans la procedure :public void GenerationDOT(...) de la class MethodesNonFonctionnelle réalisé En cours par XM : * Retrait des TTransition dans la procedure :public void GenerationDOT(...) de la class MethodesNonFonctionnelle : Pour cela, création dans GestionFormatIntermédaire d'une procédure écrire() qui écrit dans le fichier dot tous les Transitions possibles entre les états. Affichage des nom des transition ----> ok affichage du nom de chaque état ----> ok PB : ->Problème sur la l'écriture de condition de la transition par [ ][G] ou [] [] ->Problème sur l'ateignabilité des transitions, j'ai toutes les transitions à partir d'un état: cause mauvaise utilisation de la fonction recherche2(..) ------------------------------------------------------------------------- version du 07/02/2004 soir : * Retrait des classes TEtat, TTransition et TListeTransition dans la procedure :public void GenerationDOT(...) de la class MethodesNonFonctionnelle (en cours de réalisation). ------------------------------------------------------------------------- version du 07/02/2004 soir : Fait par NS : * Remise en place de l'ancien InterfacageAB * Retrait des méthode nDipos et nNonDipos * Retrait des classes TEtat, TTransition et TListeTransition de la classe GestionFormatIntermediaire * Retrait des ".simplifier()" intempestifs qui sont la cause de l'erreur sur l'exemple. (Laquelle est maintenant détectée contrairement à quand on utilisait nDipos) ------------------------------------------------------------------------- version du 07/02/2004 12h : Fait par NS : * Remise en place des paramètres d'appel de la méthode CreationDeFichierB. La modification qui avait été faite ne changeait que le nom du fichier et absolument pas l'obligation de preuve. * Mise en place d'un script d'installation qui génère automatiquement la classe ConfigurationGeneSyst.java * Débuggage du fichier UPDATES.txt et créatoion du fichier TODO.txt * sur l'exemple : java genesyst MachineACafeClassique.mch détection de l'erreur suivante : java.lang.OutOfMemoryError at java.lang.StringBuffer.ensureCapacity(StringBuffer.java:162) at java.lang.StringBuffer.append(StringBuffer.java:68) at java.lang.StringBuffer.append(StringBuffer.java:46) at MethodesNonFonctionnelles.nDipos(MethodesNonFonctionnelles.java:1055) at interfacageAB.TraiterCommande(interfacageAB.java:507) at interfacageAB.TraiterCommande(interfacageAB.java:436) at interfacageAB.Get_Status_Machine(interfacageAB.java:57) at interfacageAB.Get_AssertionLemmas(interfacageAB.java:1338) at geneSyst_alpha.ProuveMachine(geneSyst_alpha.java:469) at geneSyst_alpha.RecherchePointArriveeDesTransition(geneSyst_alpha.java:902) at geneSyst_alpha.DeclenchabiliteDesTransitions(geneSyst_alpha.java:1275) at geneSyst_alpha.TraitementSystemeAbstrait(geneSyst_alpha.java:1625) at geneSyst_alpha.GenerationDesSTE(geneSyst_alpha.java:2390) at geneSyst_alpha.main(geneSyst_alpha.java:2940) Afin de faciliter le contournement de ce problème, j'ai fait en sorte que la chaine de caractère soit vidée à chaque itération de la boucle de purge des tampons au début de TraiterCommande. * Visiblement, celle-ci vient de la nouvelle méthode nDipos. A ce sujet, un commentaire sert à ce qu'un relecteur extérieur comprenne ce que fait la méthode. En l'occurence : "Méthode qui teste si quelque chose est arrivée" ne m'indique pas grand chose. De plus, "@param InputStream out" n'est pas correct, il faut mettre : "@param out et un commentaire qui décrit ce à quoi sert ce paramètre." Question : ne voulais tu pas nommer ta méthode "nDispo" plutôt que "nDipos" ? Si la réponse est non, alors j'aurais juste voulu comprendre ce que cela voulait dire :o/ ------------------------------------------------------------------------- version du 06/02/2004 soir : Fait par Xavier Morselli: Etape 3 (En cours) : Incorporation de TListreTransition.java dans GestionFormatIntermédiaire.java: + problème de fonctionnement pour geneSyst.java Création de 2 fonction nDipos(...) et nNondipos(...) dans MethodeNonFonctionnelles .java. Ces 2 méthodes sont utilisées dans LancerAB()et ReLancerAB(), pour l'instant, dans le but d'alléger le code mais aussi pour une utilisation ultérieure dans TraiterCommande(..); Test : java genesyst MachineACafeClassique.mch -->OK java genesyst parking_r1.mch -->OK java genesyst parking_r1.mch -r parking_r2.ref -->OK java geneSyst_alpha parking_r1.mch -OR IndexMachinesAbstr.Oracle --> OK <---- ??? Si tu ne sais pas utiliser les oracles, dis le moi et je t'expliquerais :o/ java geneSyst_alpha parking_r1.mch -r parking_r2.ref -OR IndexMachinesRaff.Oracle -->OK ------------------------------------------------------------------------- version du 02/02/2004 soir : Fait par Xavier Morselli: Fichier geneSyst.java ->CreationDeFichierB([...]) Tout d'abord , nous mettons OPDefaut = false (on ne cherche pas à prouver la non propriété d'abord) puis on la mets à true... Ceci dans les classes : [...]DonneEtatAbstraitCorrespondant(), [...]RechercheEtatsInitiaux () et [...]RecherchePointArriveeDesTransition() ->>>>>>>>> C'est limpide .... Mais à part le "comment", si tu décrivait le "quoi" de ce que tu as fait ? Etape 1 (Réalisé) : Incorporation de TEtat.java dans GestionFormatIntermédiaire.java: + pas de problème de fonctionnement pour geneSyst.java Etape 2 (Réalisé) : Incorporation de TTransition.java dans GestionFormatIntermédiaire.java: + pas de problème de fonctionnement pour geneSyst.java Etape 3 (en cours) : Incorporation de TListreTransition.java dans GestionFormatIntermédiaire.java: + pas de problème de fonctionnement pour geneSyst.java ------------------------------------------------------------------------- version du 29/01/2004 soir : Fait par Xavier Morselli: Fichier MethodesNonFonctionelles.java * Création du Vector : Vector Extension qui contient toutes les extensions possibles pour un NomDeProjet. ------------------------------------------------------------------------- version du 28/01/2004 soir : Fait par Nicolas Stouls: * Modification des traces générées lors du chargement d'un oracle * Correction d'une intervertion de paramètre pour toutes les méthodes ayant attrait à l'équivalence des états par raffinement dans la classe de gestion du format intermediaire * Correction du calcul du déclenchement dans le cas d'un raffinement * Correction de la simplification par raffinement du calcul des états initiaux * Correction de la formule implantée pour calculer le déclenchement et retrait de la simplification => Elle est buguée Le bug a été soumis à Didier. * Correction de la terminologie employée dans les traces pour les conditions réductibles ou non à true. ------------------------------------------------------------------------- version du 28/01/2004 midi : Fait par Xavier Morselli: * Choix du nom du projet sous l'AB par recherche dans le dossier bdb. -> Gain de temps -> Plus stable * Mise en constante de certains chemins d'accès dépendant de l'installation de l'atelier B.