* Corrections de la liste d’adjacence.

Fri, 20 May 2011 01:03:01 +0200

author
Vincent Duvert <vincent.duvert@etu.enseeiht.fr>
date
Fri, 20 May 2011 01:03:01 +0200
changeset 7
1b4b2a8fbc1b
parent 6
ccee2034ba11
child 9
484282a8bc80

* Corrections de la liste d’adjacence.
* Rapport: introduction et quelques références bibliographiques.
* Améliorations du Makefile.
* Complétion du .hgignore.

.hgignore file | annotate | diff | revisions
adj_list/adj_list.tla file | annotate | diff | revisions
adj_list/run_tree_adj_list.tla file | annotate | diff | revisions
rapport/Makefile file | annotate | diff | revisions
rapport/rapport.tex file | annotate | diff | revisions
     1.1 --- a/.hgignore	Thu May 19 22:17:39 2011 +0200
     1.2 +++ b/.hgignore	Fri May 20 01:03:01 2011 +0200
     1.3 @@ -1,3 +1,11 @@
     1.4  syntax:glob
     1.5  .DS_Store
     1.6  memory/*
     1.7 +states/*
     1.8 +rapport/*.pdf
     1.9 +rapport/rapport.aux
    1.10 +rapport/rapport.log
    1.11 +rapport/rapport.toc
    1.12 +rapport/rapport.bib
    1.13 +rapport/*.pyg
    1.14 +
     2.1 --- a/adj_list/adj_list.tla	Thu May 19 22:17:39 2011 +0200
     2.2 +++ b/adj_list/adj_list.tla	Fri May 20 01:03:01 2011 +0200
     2.3 @@ -16,13 +16,16 @@
     2.4  UNIT == "<NO_DATA>"
     2.5  ITEM == NODES \cup { UNDEF }
     2.6  
     2.7 +NULL == 0
     2.8 +
     2.9  \* Une liste d’adjacence décrit les arêtes orientées entre les nœuds du graphe via des couples :
    2.10  \* <<a, b>> indique une arête allant de a à b.
    2.11 -ETAT == NODES \X ITEM
    2.12 +EstElementAdjacence(e) ==
    2.13 +	e[1] \in NODES /\ e[2] \in ITEM
    2.14  
    2.15  \* Invariant: état correct
    2.16  TypeEtat(etat) ==
    2.17 - /\ etat \subseteq ETAT
    2.18 +  etat = SelectSeq(etat, EstElementAdjacence)
    2.19  
    2.20  \* INVARIANT
    2.21  
    2.22 @@ -40,22 +43,31 @@
    2.23  
    2.24  \* PROCEDURE CREATE
    2.25  
    2.26 +RECURSIVE ObtenirNoeudsAdjacence(_, _)
    2.27 +ObtenirNoeudsAdjacence(etat, src) ==
    2.28 +  IF etat = << >> THEN
    2.29 +    << >>
    2.30 +  ELSE
    2.31 +    IF Head(etat)[1] = src THEN
    2.32 +      << Head(etat) >> \o ObtenirNoeudsAdjacence(Tail(etat), src)
    2.33 +    ELSE
    2.34 +      ObtenirNoeudsAdjacence(Tail(etat), src)
    2.35 +
    2.36  \* on choisit un emplacement libre du graphe (indéfini)
    2.37  \* pour y insérer un nouveau noeud d'arité quelconque
    2.38  Pre_create(param, etat) ==
    2.39   /\ \E src \in NODES :
    2.40 -    LET EstPointe(e) == e[1] = src IN
    2.41 -    LET pointes == SelectSeq(etat, EstPointes) IN
    2.42 +    LET pointes == ObtenirNoeudsAdjacence(etat, src) IN
    2.43       /\ pointes /= << >>
    2.44       /\ \E o \in 1..Len(pointes) :
    2.45 -      pointes[o] = UNDEF
    2.46 - /\ \E dst \in NODES :
    2.47 -    LET EstPointe(e) == e[1] = dst IN
    2.48 -    SelectSeq(etat, EstPointes) = << >>
    2.49 - /\ a \in Naturals
    2.50 - /\ param = [ source |-> src, offset |-> o, target |-> dst, arity |-> a ]
    2.51 +      /\ pointes[o][1] = UNDEF
    2.52 +      /\ \E dst \in NODES :
    2.53 +        /\ ObtenirNoeudsAdjacence(etat, dst) = << >>
    2.54 +        /\ \E a \in Nat :
    2.55 +            param = [ source |-> src, offset |-> o, target |-> dst, arity |-> a ]
    2.56  
    2.57  \* Fonction créant la liste d’adjacence originale d’un nœud d’arité donnée
    2.58 +RECURSIVE CreerNoeud(_, _, _)
    2.59  CreerNoeud(etat, noeud, arite) ==
    2.60   IF arite = 1 THEN
    2.61    Append(etat, << noeud, UNDEF >>)
    2.62 @@ -64,6 +76,7 @@
    2.63  
    2.64  \* Fonction modifiant la liste d’adjacence pour remplacer l’adjacence d’un nœud donné, de position
    2.65  \* donnée, par un autre nœud.
    2.66 +RECURSIVE RemplacerAdjacence(_, _, _, _)
    2.67  RemplacerAdjacence(etat, src, offset, dst) ==
    2.68   IF Head(etat)[1] = src THEN
    2.69    IF offset = 1 THEN
    2.70 @@ -84,14 +97,14 @@
    2.71  
    2.72  Pre_get(param, etat) ==
    2.73   /\ \E src \in NODES :
    2.74 -    LET EstPointe(e) == e[1] = src IN
    2.75 -    LET pointes == SelectSeq(etat, EstPointes) IN
    2.76 +    LET pointes == ObtenirNoeudsAdjacence(etat, src) IN
    2.77       /\ pointes /= << >>
    2.78       /\ \E o \in 1..Len(pointes) :
    2.79 -      pointes[o] /= UNDEF
    2.80 - /\ param = [ source |-> src, offset |-> o ]
    2.81 +       /\ pointes[o][1] /= UNDEF
    2.82 +       /\ param = [ source |-> src, offset |-> o ]
    2.83  
    2.84  \* Récupération de l’adjacence d’offset donné d’un nœud
    2.85 +RECURSIVE ObtenirAdjacence(_, _, _)
    2.86  ObtenirAdjacence(etat, src, offset) ==
    2.87   IF Head(etat)[1] = src THEN
    2.88    IF offset = 1 THEN
    2.89 @@ -101,7 +114,7 @@
    2.90   ELSE
    2.91    ObtenirAdjacence(Tail(etat), src, offset)
    2.92  
    2.93 -Act_get(param, etat) ==
    2.94 +Act_get(param, etat, etat_p, result) ==
    2.95   /\ etat_p = etat
    2.96   /\ result = ObtenirAdjacence(etat, param.source, param.offset)
    2.97  
    2.98 @@ -110,14 +123,14 @@
    2.99  \* PROCEDURE SET
   2.100  Pre_set(param, etat) ==
   2.101   /\ \E src \in NODES :
   2.102 -    LET EstPointe(e) == e[1] = src IN
   2.103 -    LET pointes == SelectSeq(etat, EstPointes) IN
   2.104 -     /\ pointes /= << >>
   2.105 -     /\ \E o \in 1..Len(pointes) :
   2.106 -      pointes[o] = UNDEF
   2.107 - /\ param = [ source |-> src, offset |-> o, target |-> dst ]
   2.108 +      \E dst \in NODES :
   2.109 +        LET pointes == ObtenirNoeudsAdjacence(etat, src) IN
   2.110 +         /\ pointes /= << >>
   2.111 +         /\ \E o \in 1..Len(pointes) :
   2.112 +           /\ pointes[o][1] = UNDEF
   2.113 +           /\ param = [ source |-> src, offset |-> o, target |-> dst ]
   2.114   
   2.115 -Act_get(param, etat) ==
   2.116 +Act_set(param, etat, etat_p, result) ==
   2.117   /\ etat_p = RemplacerAdjacence(etat, param.source, param.offset, param.target)
   2.118   /\ result = UNIT
   2.119  
     3.1 --- a/adj_list/run_tree_adj_list.tla	Thu May 19 22:17:39 2011 +0200
     3.2 +++ b/adj_list/run_tree_adj_list.tla	Fri May 20 01:03:01 2011 +0200
     3.3 @@ -1,9 +1,8 @@
     3.4  ---------------- MODULE run_tree_adj_list ----------------
     3.5  
     3.6 -EXTENDS Naturals, FiniteSets, Sequences, TLC, var_raffinement
     3.7 +EXTENDS Naturals, FiniteSets, Sequences, var_raffinement
     3.8  
     3.9  CONSTANT
    3.10 -    MEM,
    3.11      UNDEF,
    3.12      ROOT,
    3.13      NODES,
    3.14 @@ -11,36 +10,9 @@
    3.15  
    3.16  A == INSTANCE tree
    3.17  
    3.18 -C == INSTANCE memory
    3.19 +C == INSTANCE adj_list
    3.20  
    3.21 -\* ensemble de fonction de type dépendent de la forme : (x:X) -> Y(x)
    3.22 -\* X représente le type d'entrée
    3.23 -\* Y(_) représente les types de sortie dépendant du paramètre d'entrée x
    3.24 -DependentFunction(X, Y(_)) ==
    3.25 - LET DependentFunctionRec[sx\in SUBSET X] ==
    3.26 -  IF (sx = {}) THEN { << >> } ELSE
    3.27 -  LET b == Print(sx, TRUE) IN
    3.28 -  LET x == CHOOSE x \in sx : TRUE IN
    3.29 -   { (x :> Yx)@@Rec : Yx \in Y(x), Rec \in DependentFunctionRec[sx \ { x }] }
    3.30 - IN DependentFunctionRec[X]
    3.31 -
    3.32 -\* ensemble des noeuds attachés à une adresse donnée (normalement un seul)
    3.33 -NodesAt(etatC, adr) ==
    3.34 - IF (adr=C!NULL) THEN { UNDEF } ELSE { n \in NODES : etatC.store[n] = adr }
    3.35 -
    3.36 -\* Ici, un seul état abstrait peut correspondre à un état concret donné
    3.37 -Liaison(etatC) ==
    3.38 - \* l'ensemble des noeuds alloués/utilisés
    3.39 - LET noeuds == { n \in NODES : etatC.store[n] /= C!NULL } IN
    3.40 -  \* l'ensemble des liens possibles pour chaque noeud
    3.41 -  LET liens(noeud) ==
    3.42 -  LET nadr == etatC.store[noeud] IN
    3.43 -  IF (nadr=C!NULL) THEN { << >> }
    3.44 -                   ELSE \* l'ensemble des noeuds (normalement un seul)
    3.45 -                        \* attachés au 'o'-ème fils de 'noeud'
    3.46 -                        LET nodesAt(o) == NodesAt(etatC, etatC.heap[nadr+o])
    3.47 -                        IN DependentFunction(1..etatC.heap[nadr], nodesAt)
    3.48 - IN { [nodes |-> noeuds, links |-> lnk] : lnk \in DependentFunction(NODES, liens) }
    3.49 +Liaison(etatC) == { etatC }
    3.50  
    3.51  INSTANCE run_raffinement WITH InitA <- A!Init, ContratClientA <- A!ContratClient, ContratModuleA <- A!ContratModule,
    3.52                                InitC <- C!Init, ContratClientC <- C!ContratClient, ContratModuleC <- C!ContratModule
     4.1 --- a/rapport/Makefile	Thu May 19 22:17:39 2011 +0200
     4.2 +++ b/rapport/Makefile	Fri May 20 01:03:01 2011 +0200
     4.3 @@ -8,7 +8,7 @@
     4.4  liste-fils.pdf: liste-fils.dot
     4.5  
     4.6  %.pdf: %.tex
     4.7 -	xelatex -shell-escape $<
     4.8 +	(xelatex -shell-escape $< || (rm -f $@ && false))
     4.9  	xelatex -shell-escape $<
    4.10  
    4.11  %.pdf: %.dot
    4.12 @@ -22,3 +22,5 @@
    4.13  
    4.14  mrproper: clean
    4.15  	rm -f *.pdf
    4.16 +
    4.17 +.PHONY: clean mrproper
    4.18 \ No newline at end of file
     5.1 --- a/rapport/rapport.tex	Thu May 19 22:17:39 2011 +0200
     5.2 +++ b/rapport/rapport.tex	Fri May 20 01:03:01 2011 +0200
     5.3 @@ -28,6 +28,7 @@
     5.4  \usepackage{textcomp}
     5.5  \usepackage{amsmath}
     5.6  \usepackage{tikz}
     5.7 +\usepackage{url}
     5.8  
     5.9  \title{{\itshape\large Spécification formelle et validation}\\ Sérialisation de structures de données}
    5.10  \author{Vincent \textsc{Duvert} \and Sanaa \textsc{Essaid} \and Antoine \textsc{Lubineau}}
    5.11 @@ -38,7 +39,8 @@
    5.12  	\maketitle
    5.13  	
    5.14  	\begin{abstract}
    5.15 -		
    5.16 +		Ce projet est consacré à l’étude des différentes méthodes permettant
    5.17 +		de sérialiser une structure de données.
    5.18  	\end{abstract}
    5.19  
    5.20  	\vfill
    5.21 @@ -50,8 +52,12 @@
    5.22  	\section{Introduction}
    5.23  
    5.24  		\subsection{Méthodes de sérialisation}
    5.25 -
    5.26 -
    5.27 +		Lors de leur fonctionnement, les programmes informatiques manipulent		des données généralement très structurées, par l’utilisation notamment		de pointeurs. Ces pointeurs ne conservant leur validité que durant		l’exécution du programme, il est nécessaire de transformer les données		pour les placer sous une forme plus adaptée au stockage dans un fichier		ou au transfert par le réseau. Ce processus est nommé  \emph{sérialisation} \cite{serialisation}.
    5.28 +		
    5.29 +		Il existe plusieurs méthodes de sérialisation; il est possible de les étudier de manière générique, en représentant les structures de données des programmes par des modèles algorithmiques. Dans certains cas, on peut utiliser des \emph{arbres enracinés} \cite{arbres_enracines} pour représenter l’imbrication des structures. Mais, certains langages de programmations autorisant les structures \emph{récursives} (où un élément d’une structure peut faire référence à l’ensemble de la structure), il est nécessaire d’utiliser un \emph{graphe orienté} \cite{graphes_orientes}.
    5.30 +		
    5.31 +		Ce projet a pour but de présenter diverses manières d’effectuer la sérialisation d’un arbre ou d’un graphe, et d’implémenter l’une d’entre elles en TLA.
    5.32 +		
    5.33  		\subsection{Notations}
    5.34  
    5.35  	\newpage
    5.36 @@ -59,8 +65,8 @@
    5.37  	\section{Recherche bibliographique}
    5.38  
    5.39  		\subsection{Matrice d'adjacence}
    5.40 -
    5.41 -		À tout graphe, orienté ou non, on peut associer une matrice d'adjacence qui décrit complètement les \emph{relations} entre les nœuds (à condition qu'il n'y ait pas plus d'une arête orientée ayant les mêmes extrémités). On ne spécifie pas comment désigner la données associée à chaque nœud, mais $1$ peut être un pointeur sur celle-ci.
    5.42 +		
    5.43 +		À tout graphe, orienté ou non, on peut associer une matrice d'adjacence qui décrit complètement les \emph{relations} entre les nœuds (à condition qu'il n'y ait pas plus d'une arête orientée ayant les mêmes extrémités). On ne spécifie pas comment désigner la données associée à chaque nœud, mais $1$ peut être un pointeur sur celle-ci. \cite{mat_adj}
    5.44  
    5.45  		\begin{multicols}{2}
    5.46  
    5.47 @@ -101,7 +107,7 @@
    5.48  
    5.49  		\subsection{Liste de paires d'adjacence}
    5.50  
    5.51 -		Cette méthode de sérialisation est très simple: on liste toutes les relations du graphe, et on écrit pour chacune les deux sommets associés (on peut se baser sur l'ordre pour indiquer le sens d'une relation).
    5.52 +		Cette méthode de sérialisation est très simple: on liste toutes les relations du graphe, et on écrit pour chacune les deux sommets associés (on peut se baser sur l'ordre pour indiquer le sens d'une relation). \cite{liste_adj}
    5.53  
    5.54  		Avec le même exemple que précédemment, on obtient
    5.55  		\begin{verbatim}
    5.56 @@ -212,4 +218,10 @@
    5.57  	
    5.58  	\section{Conclusion}
    5.59  
    5.60 +	\begin{thebibliography}{9}
    5.61 +	\bibitem{serialisation} \url{http://fr.wikipedia.org/wiki/Sérialisation}
    5.62 +	\bibitem{graphes_orientes} \url{http://fr.wikipedia.org/wiki/Graphe_orienté}
    5.63 +	\bibitem{mat_adj} \url{http://fr.wikipedia.org/wiki/Matrice_d%27adjacence}
    5.64 +	\bibitem{liste_adj} \url{http://en.wikipedia.org/wiki/Adjacency_list}
    5.65 +	\end{thebibliography}
    5.66  \end{document}

mercurial