- 2.3 Transformation de l'AltaRica au réseau de Petri.
- Dépliage de réseau de Petri ...16.
- Figure 2.1 : Réseau de Petri.
- Figure 2.2 : Réseau de Petri de SG(3).
- Figure 2.3 : Macro-transition et des transitions correspondantes Figure 2.4 : SG(3) en langage AltaRica.
- Figure 3.1 : Réseau d'ocurrence Figure 3.2a : Algorithme de dépliage Figure 3.2b : Génération des transitions Figure 3.3 : Préfixe fini.
- Figure 3.4 : Préfixe du dépliage de SG(3) Figure 3.5a : Composant s 0 de SG(3) Figure 3.5b : Composant s 1 de SG(3) Figure 3.5c : Composant s 2 de SG(3).
- Figure 3.6a : Processus arborescent dans le composant s 0 de SG(3) Figure 3.6b : Processus arborescent dans le composant s 1 de SG(3) Figure 3.6c : Processus arborescent dans le composant s 2 de SG(3) Figure 3.7 : Processus arborescent global.
- Figure 5.1 : Graphe des sous-préfixes.
- Figure 5.2 : Les sous-préfixes Q, R et P de SG(3) Figure 5.3 : Graphe des sous-préfixes de SG(3).
- Figure 5.4 : L'arbre Cartsian du composant s 1 de SG(3) Figure 5.5 : RMQ rapide.
- Figure 5.6 : La construction du graphe des sous-préfixes Figure 5.7 : Construction de matrice A.
- Figure 5.8 : Arbre AVL dans le RMQ dynamique.
- De nos jours, pour éviter l'explosion combinatoire du nombre d'états d'un système compliqué, la vérification basée sur des préfixes finis est une bonne solution, mais le dépliage n'est développé que sur le réseau de Petri, un langage de modélisation en bas niveau.
- Mots clés: Dépliage, Altarica, réseau de Petri, modélisation, vérification, préfixe, Dernière Ancêtre Commun (LCA), Requête Minimale du Rang (RMQ), RMQ dynamique.
- Né de la volonté d'industriels et de chercheurs, le langage de modélisation en haut niveau AltaRica [Arnold03] a beaucoup d'avantages tels qu'il est utilisé plus facilement que des langages de modélisation en bas niveau comme le réseau de Petri ou il est naturel de pouvoir décrire par de nombreuses façons différentes un système donné..
- La vérification basée sur des préfixes finis [Esparza01, Couvreur04] est une nouvelle approche pour éviter l'explosion combinatoire de nombre d'états du système compliqué, mais ces techniques ne sont développées que sur le réseau de Petri, un langage de modélisation en bas niveau..
- L'objectif de mon stage est de réaliser un dépliage sur le langage AltaRica: pas seulement de construire un outil de tranformation de l'AltaRica au réseau de Petri, mais aussi de chercher des algorithmes plus efficaces pour déplier un modèle en AltaRica..
- Langage AltaRica est un langage de modélisation en haut niveau ayant des avantages tels que la construction des systèmes complexes plus facile que des langages de modélisation en bas niveau comme le réseau de Petri.
- Tout d'abord, on concerne le réseau de Petri, étant un des langages de modélisation en bas niveau.
- Un réseau de Petri R est une structure <P, T, Pre, Post>.
- est la donnée d'un réseau de Petri R et d'un marquage initial m 0.
- est la donnée d'un réseau de Petri R, d'un alphabet fini Σ et d'une fonction d'étiquetage sur les transitions λ: T → Σ..
- Exemple 2.1 Réseau de Petri:.
- Figure 2.1: Réseau de Petri.
- un réseau de Petri.
- SG(3) en langage réseau de Petri:.
- Figure 2.2: Réseau de Petri de SG(3).
- Réseau de Petri est facile à utiliser mais est difficile concevable de modéliser des systèmes très complexes [Pagetti04]..
- Figure 2.3: Macro-transition et des transitions correspondantes.
- SG(3) en langage AltaRica dans la figure 2.4..
- <t1, s0.b0, s1.b1, s2.e >;.
- <t4, s0.w1, s1.w0, s2.e >;.
- Figure 2.4: SG(3) en langage AltaRica.
- On transforme le système modélisé en langage AltaRica au système représenté par le réseau de Petri.
- Le format de transformation de l'AltaRica au réseau de Petri est présenté dans la section 4.1..
- En suite, on peut utiliser le dépliage normal sur ce réseau de Petri (dans la section 3.2).
- Dépliage de réseau de Petri.
- Depuis longtemps, on cherche une structure plus simple pour présenter un réseau de Petri, en conçervant leurs caractéristiques, c'est le réseau d'occurrence.
- McMillan a proposé un algorithme de base pour déplier un réseau de Petri en 1995.
- Le réseau d'occurrence est une structure plus simple pour présenter un réseau de Petri, en conçervant leurs caractéristiques..
- Soit h un homomorphisme de réseau de S dans <R, m 0 >.
- Le réseau d'ocurrence correspondant du réseau de Petri dans l'exemple 2.1.
- Figure 3.1: Réseau d'ocurrence.
- McMillan a proposé un algorithme de base [McMillan95] pour déplier un réseau de Petri en 1995.
- Figure 3.2a: Algorithme de dépliage.
- Figure 3.2b: Génération des transitions.
- Le préfixe fini du réseau de Petri dans l'exemple 2.1..
- Figure 3.3: Préfixe fini.
- Figure 3.4: Préfixe du dépliage de SG(3).
- On peut appliquer cet algorithme pour déplier un réseau de Petri transformé à partir du langage AltaRica.
- Figure 3.5a: Composant s 0 de SG(3).
- Figure 3.5b: Composant s 1 de SG(3).
- Figure 3.5c: Composant s 2 de SG(3).
- Figure 3.6a: Processus arborescent dans le composant s 0 de SG(3).
- Figure 3.6b: Processus arborescent dans le composant s 1 de SG(3).
- Figure 3.6c: Processus arborescent dans le composant s 2 de SG(3).
- Figure 3.7: Processus arborescent global.
- On crée un outil alta2net pour le transformer au format de réseau de Petri (fichier .net)..
- #place s0_s__B mk(<..>).
- #place s1_s__E mk(<..>).
- #place s2_s__W mk(<..>).
- in {s0_s__B:<..>;s1_s__E:<..>;}.
- out {s0_s__E:<..>;s1_s__B:<..>;}.
- in {s1_s__B:<..>;s2_s__E:<..>;}.
- out {s1_s__E:<..>;s2_s__B:<..>;}.
- in {s0_s__B:<..>;s1_s__W:<..>;s2_s__E:<..>;}.
- out {s0_s__E:<..>;s1_s__W:<..>;s2_s__B:<..>;}.
- in {s0_s__E:<..>;s1_s__W:<..>;}.
- out {s0_s__W:<..>;s1_s__E:<..>;}.
- in {s1_s__E:<..>;s2_s__W:<..>;}.
- out {s1_s__W:<..>;s2_s__E:<..>;}.
- in {s0_s__E:<..>;s1_s__B:<..>;s2_s__W:<..>;}.
- out {s0_s__W:<..>;s1_s__B:<..>;s2_s__E:<..>;}.
- En suite, on peut utiliser des algorithmes de dépliage pour le réseau de Petri (On utilise un ordre adéquat SizeParikhLex) ainsi que l’algorithme supplémentaire en tenant compte des connaissances des composants (les produit d’automates)..
- Par exemple, concernons le réseau de Petri dans l'exemple 2.1 et la figure 2.1, nous avons un sous-préfixe P comme dans la figure 3.3.
- On a donc que le processus arborescent dans la figure 3.1 est très simple comme le suivant:.
- On a un graphe des sous-préfixes comme dans la figure 5.1..
- Figure 5.1: Graphe des sous-préfixes.
- Figure 5.2: Les sous-préfixes Q (2), R (1) et P (0) de SG(3).
- Figure 5.3: Graphe des sous-préfixes de SG(3).
- On trouve qu’on ne doit que déterminer le conflit entre r 1 et r 2 quand r 1 ≠ r 2 (On a O(H.
- Figure 5.4: L'arbre Cartsian du composant s 1 de SG(3).
- Concernons LCA(u, v) comme dans la figure 5.4 où b = 2 et n = 7..
- j) dans le groupe de j..
- Figure 5.5: RMQ rapide.
- Dans la matrice B, avec m = 2 b max .n / lg(b max .n), on a une complexité d'espace: O(m.lg(m.
- T B est calculé comme dans la section 5.2..
- Figure 5.6: La construction du graphe des sous-préfixes.
- Figure 5.7: Construction de matrice A.
- L'arbre AVL dans le RMQ dynamique:.
- Figure 5.8: Arbre AVL dans le RMQ dynamique.
- Durant mon stage, j'ai déjà construit un outil alta2net pour transformer de l'AltaRica au réseau de Petri.
- Entrées : La liste des transitions, des places du réseau de Petri Sorties : Les premiers événements a partir du marquage initial La raison de mon choix.
- Entrées : La liste des transitions, des places du réseau de Petri,.
- Entrées : La liste des transitions, des places du réseau de Petri Sorties : Le préfix de dépliage du réseau de Petri.
- Le but de cette fonction : Déplier un réseau de Petri La raison de mon choix.
- On crée cette fonction pour déplier un réseau de Petri en utilisant des connaissances des composants pour économiser le mémoire et pour que le programme fonctionne très vite.
- Réseau de Petri et son préfixe de SG(5).
- Réseau de Petri et son préfixe de SG(7)