Master d’informatique 2008 2009
sacc
Mini-projet SACC 2008

Voici le cahier des charges du mini-projet pour l’UE SACC session automne 2008

Objectif

Le but du projet est de réaliser un outil genlts permettant de caculer un automate de transitions étiquetées (labelled transition system LTS) à partir d’un processus CCS.

Les contraintes sont les suivantes :

- au minimum, le LTS généré est fini si le système fourni en entrée est lui-même fini
- au mieux, le LTS généré doit être minimal (au sens de la bisimilarité)
- dans le cas d’un système infini, on indiquera un critère de terminaison de l’analyse (taille du LTS, mémoire occupée, nombre d’itérations, etc.).
- on pourra choisir un sous-ensemble du langage puis l’augmenter au fur et à mesure
- la phase de parsing est recommandée (facilite le test) mais non obligatoire

Le choix du langage d’implémentation est libre

Syntaxe des processus

La syntaxe BNF utilisée est une variante ASCII de la syntaxe formelle vue en cours. Cette syntaxe est donnée à titre indicatif, et pourra être adaptée ou corrigée si nécessaire. Il est bien sûr possible d’étendre le langage.

Les commentaires "à la C" sont autorisés

{letter} ::= 'a'..'z' | 'A'..'Z'
{digit} ::= '0'..'9'
{idletter} ::= {letter} | {digit} | '_'

{ident} ::= {letter} {idletter}*
{integer} ::= '0' | '1'..'9' {digit}*
{boolean} ::= 'true' | 'false'

{constant} ::= {integer} | {boolean}

{prog} ::= {process} | {definition} {prog}

{definition} ::= {header} '=' {process}

{header} ::= {ident} | {ident} '(' {params} ')'
{params} ::= {param} | {param} ',' {params}
{param} ::= {constant} | {ident}

{process} ::= '0'
                    | '(' {process} ')'
                    | '[' {process} ']'
                    | {prefix} '.' {process}
                    | {process} '||' {process}
                    | {process} '+' {process}
                    | 'new(' {names} ')'  {process}
                    | {ident} '(' {args} ')'
                    | {ident} '(' ')'

{prefix} ::=  'tau'
                  | {ident} '!'
                  | {ident} '?'

{names} ::= {ident} | {ident} ',' {names}

{args} ::= {expr} | {expr} ',' {args}

{expr} ::= {constant}
                  | {ident}
                  | '(' {expr} ')'
                  | 'not' {expr}
                  | {expr} 'and' {expr}
                  | {expr} 'or' {expr}
                   | {expr} '+' {expr}
                   | {expr} '-' {expr}

Remarques :

Les espaces ne sont pas pris en compte

Les préfixes et le new sont prioritaires sur le parallèle et la somme

 a!.b?.0 + a?.b!.0 = (a!.b?.0) + (a?.b!.0)

 new(a,b) a!.b?.0 || b?.a?.0  = new(a.b) [ a!.b?.0 ] || b?.a?.0

La somme est prioritaire sur le parallèle

 P + Q || R + M  =  (P + Q) || (R + M)

Format du fichier de sortie

Le LTS généré doit être au format suivant :

{lts} ::= {trans} | {trans} {lts}

{trans} ::= {ident} '--[' {prefix} ']--> {ident}

Encore une fois, les commentaires "à la C" sont autorisés.

Exemple

Voici un exemple simple :

Sem2(p,v,0) = p!.Sem2(p,v,1)
Sem2(p,v,1) = p!.Sem2(p,v,2) + v?.Sem2(p,v,0)
Sem2(p,v,2) = v?.Sem2(p,v,1)

new(p,v) [  p?.a!.b!.v!.0 || p?.a!.b!.v!.0 || Sem2(p,v,0) ]

Et le LTS généré sera :

S1 --[tau]--> S2
S2 --[a!]--> S3
S3 --[b!]--> S4
S1 --[tau]--> S6

... etc ...

Algorithme de minimsation

Pour la partie minimisation, le premier critère concerne le partionnement des états dans des "blocs grossiers" discriminés par les ensembles d’action en sortie des états, selon les principes vus en cours.

Au niveau des blocs fin, à l’intérieur des blocs grossiers, il nous manque un algorithme pour comprendre s’il faut séparer (split) ou au contraire rassembler (merge) les états qu’ils contiennent.

L’algorithme de Lee et Yannakakis est un algorithme simple et relativemement efficace permettant de vérifier si deux états sont bisimilaires ou non, le voici en pseudo-code.

Entrée:  
 - un système de transition LTS partitionné en blocs grossiers et blocs fins
 - une liste L de blocks fin potentiellement instables (i.e. les états qu'ils contiennent ne sont pas forcément bisimilaire.)

Algorithme:
 tant que L est non-vide :
     retirer un bloc (fin) B de L
     pour tout bloc fin C dont certains états conduisent en B :
         pour toute action alpha telle que alpha-1(B) est non-vide
         (B possède au moins un prédécesseur via une transition alpha) :
               calculer  C'  =   C  intersection  alpha-1(B)
               si C' est non vide et C' est différent de C alors :
                   retirer le bloc fin C de la partition
                   retirer le bloc fin C de la liste L (s'il est présent)
                   calculer C'' = C - C'    (différence d'ensembles)
                   ajouter C' et C''  (blocs fin) dans la partition (choisir le bon bloc grossier)
                   ajouter C' et C'' à la liste L   (blocs instables)
               fin si
           fin pour
     fin pour
  fin tant que

Remarque : la notation alpha-1(B) signifie l’ensemble des états qui ont une transition avec le label alpha vers B

Conditions de rendu

Archive ltsgen-NOM1-NOM2.zipau format zip

- répertoire principal : ltsgen-NOM1-NOM2/
- sous-répertoire des sources dans src/
- Fichier de construction src/Makefile ou src/build.xml
- documentation dans doc/

Pour la soumission aller sur cette page

Poster un message sur le forum de cette page

13 Messages de forum