HowTo define a new formalism

Ce tutoriel a pour but d'expliquer comment spécifier un formalisme en le langage FML (Formalism Markup Language). Ce langage va de pair avec le langage GrML (Graph Markup Language) qui lui permet de spécifier des modèles.

1. Définitions

1.1. Modèle GrML (Graph Markup Language)

Un modèle est une instance d'un formalisme. Il est représenté dans un format XML suivant la structure d'un graphe (figure 1). Un modèle contient donc des nœuds et des arcs, les arcs permettant de relier les nœuds. Des attributs sont attachés au modèle ainsi qu'à tous les éléments du modèle. Ces attributs permettent d'ajouter de l'information au modèle (titre, auteurs, …) ou aux éléments (nom, valuation, …). Pour plus de détail concernant les attributs, voir la page HowTo define a complex attribute.

L'élément ref permet de gérer les modèles hiérarchiques ainsi que les modèles composés. Un nœud peut référencer un modèle (cas le plus courant), un arc également (SDD/DDD) et la composition peut se faire à l'aide des références entre éléments.

Les attributs formalismUrl, nodeType et arcType permettent de spécifier indépendamment de la structure du modèle le formalisme utilisé ainsi que les différents types d'élément composant notre modèle.


Figure 1 — Diagramme de classes d'un modèle au format GrML

Un schéma Relax-NG est disponible (model.rng) pour valider qu'un modèle respecte bien la structure d'un graphe. Ce schéma ne gère pas la validation des url (formalismUrl et targetUrl), c'est à dire si la cible d'une url existe et est bien valide.

Voici un exemple de modèle (figure 2) dans un formalisme de réseau de Petri auquel on a ajouté des places virtuelles.


Figure 2 — Exemple de modèle

Et voici sa représentation XML :

<?xml version="1.0" encoding="UTF-8"?>

<model formalismUrl="ptnet++.fml" xmlns="http://cosyverif.org/ns/model">

  <node id="1" nodeType="place">
    <attribute name="name">Place</attribute>
    <attribute name="marking">1</attribute>
  </node>
  <node id="2" nodeType="virtualPlace">
    <attribute name="name">Ref</attribute>
    <ref href="?id=1"/>
  </node>
  <node id="3" nodeType="transition">
    <attribute name="name">Transition</attribute>
  </node>

  <arc id="4" arcType="arc" source="1" target="3"/>
  <arc id="5" arcType="arc" source="3" target="2"/>
</model>

1.2. Formalisme FML (Formalism Markup Language)

Dans notre contexte, un formalisme est un document structuré (XML) devant respecter une certaine syntaxe (figure 3) et permettant de spécifier les différents types d'élément (nœuds et arcs) supportés. Un formalisme permet également de spécifier les différents types d'attributs attachés au modèle et aux différents types d'éléments.

Un formalisme peut être abstrait. Aucun modèle ne peut être d'un type de formalisme abstrait ce qui permet de définir les formalismes par morceaux. Pour cela on permet d'inclure une définition de formalisme (abstrait ou non).

Les formalismes hiérarchiques peuvent spécifier les types de hiérarchies autorisées en spécifiant quels types de nœuds et/ou d'arcs peuvent contenir des références. Le type d'élément référencé est également spécifié à l'aide de l'attribut targetUrl.

Un mécanisme sera ajouté afin de permettre de spécifier des contraintes. Par exemple : interdire les arcs entre les nœuds de même type (place-place ou transition-transition) dans les réseaux de Petri.


Figure 3 — Diagramme de classes d'un formalisme au format FML

Un schéma Relax-NG est disponible (formalism.rng) pour valider qu'un formalisme respecte bien la syntaxe définie. Ce schéma ne gère pas la validation des url (formalismUrl et targetUrl), c'est à dire si la cible d'une url existe et est bien valide.

<?xml version="1.0" encoding="UTF-8"?>

<formalism name="Place/Transition Net" xmlns="http://cosyverif.org/ns/formalism">
  <nodeType name="place"/>
  <leafAttribute name="name" refType="place"/>
  <leafAttribute name="initialMarking" defaultValue="0" refType="place"/>

  <nodeType name="transition"/>
  <leafAttribute name="name" refType="transition"/>

  <arcType name="arc"/>
  <leafAttribute name="valuation" refType="arc"/>
</formalism>

1.3. URL

Dans les documents GrML et FML, certains attributs (formalismeUrl, href) utilise des données du type URL. Ces URLs permettent de lier nos documents avec d'autres documents. On peut par exemple lier un élément de notre document avec un autre élément au sein du même document (lien local). Une URL est également utilisée pour spécifier le formalisme utilisé par un modèle (attribut formalismUrl de l'élement model).

Il existe deux types d'URL :
  • URL absolue, par exemple http://alligator.lip6.fr/pt-net.fml. Ce type d'URL dans la forme la plus complète ressemble à ça : protocol :// hostname / path/filename #id.
    • protocol : protocole de communication (ex: http, file, …)
    • hostname : nom de domaine ou adresse IP
    • path/filename : chemin absolu pour atteindre le fichier
    • #id : paramètre optionnel permettant de spécifier un élément cible dans le document.
  • URL relative : par exemple ./filename équivalent à filename. Ce type d'URL est similaire aux URLs absolues sauf que les 3 premiers paramètres sont déduis en fonction du document contenant l'URL.
Exemples d'URL :

2. Tutoriel

2.1. Définition d'un formalisme

Le formalisme «_Petri Net_» n'étant pas un véritable formalisme on va le définir comme formalisme abstrait à l'aide de l'attribut abstract="true". Un modèle ne peut pas être du type d'un formalisme abstrait (analogie avec les classes abstraites non instanciable).

<?xml version="1.0" encoding="UTF-8"?>

<!-- file: petrinet.fml -->
<formalism abstract="true" name="Petri Net" xmlns="http://cosyverif.org/ns/formalism">
</formalism>

Un réseau de Petri est composé de places et de transitions reliées par des arcs :

<?xml version="1.0" encoding="UTF-8"?>

<!-- file: petrinet.fml -->
<formalism abstract="true" name="Petri Net" xmlns="http://cosyverif.org/ns/formalism">
  <nodeType name="place"/>
  <nodeType name="transition"/>
  <arcType name="arc"/>
</formalism>

On peut également rajouter que les places et les transitions ont des noms :

<?xml version="1.0" encoding="UTF-8"?>

<!-- file: petrinet.fml -->
<formalism abstract="true" name="Petri Net" xmlns="http://cosyverif.org/ns/formalism">
  <nodeType name="place"/>
  <nodeType name="transition"/>
  <arcType name="arc"/>

  <leafAttribute name="name" refType="place"/>
  <leafAttribute name="name" refType="transition"/>
</formalism>

2.2. Composition de formalismes

On va maintenant définir le formalisme «_Place/Transition Net_» en réutilisant le formalisme abstrait «_Petri Net_».

<?xml version="1.0" encoding="UTF-8"?>

<!-- file: ptnet.fml -->
<formalism name="Place/Transition Net" xmlns="http://cosyverif.org/ns/formalism" xmlns:xi="http://www.w3.org/2001/XInclude">
  <xi:include formalismUrl="petrinet.fml"/>
</formalism>

Le mot clé xi:include permet d'insérer le contenu d'un formalisme ou d'un formalisme abstrait. Attention, pour pouvoir utiliser l'inclusion de formalisme, il faut déclarer l'espace de nom xi à l'aide de la définition xmlns:xi="http://www.w3.org/2001/XInclude". Au final ce formalisme est équivalent à ce formalisme :

<?xml version="1.0" encoding="UTF-8"?>

<!-- file: ptnet.fml -->
<formalism name="Place/Transition Net" xmlns="http://cosyverif.org/ns/formalism">
  <nodeType name="place"/>
  <nodeType name="transition"/>
  <arcType name="arc"/>

  <leafAttribute name="name" refType="place"/>
  <leafAttribute name="name" refType="transition"/>
</formalism>

On peut maintenant ajouter les informations nécessaires à un réseau de Petri Place/Transition.

<?xml version="1.0" encoding="UTF-8"?>

<!-- file: ptnet.fml -->
<formalism name="Place/Transition Net" xmlns="http://cosyverif.org/ns/formalism" xmlns:xi="http://www.w3.org/2001/XInclude">
  <xi:include formalismUrl="petrinet.fml"/>
  <leafAttribut name="initialMarking" default="0" refType="place"/>
  <leafAttribut name="valuation" default="1" refType="arc"/>
</formalism>

2.3. Formalismes hiérarchiques

Nous allons maintenant définir un formalisme exploitant la hiérarchie : les réseaux de Petri d' Evinrude. La figure 4 présente un exemple de modèle hiérarchique respectant ce formalisme.


Figure 4 — Exemple de model hiérarchique

Ce formalisme permet d'attacher des sous-modèles à des places. Dans notre exemple la place echo-server référence deux sous-modèles. Les places dans les sous-modèles peuvent être de type input-place et/ou output-place. Dernier point particulier, le formalisme permet de définir des places virtuelles référençant des places pouvant se trouver n'importe où dans le modèle. Dans notre exemple, les places bleues sont des places virtuelles et le lien est déterminé par les arcs bleus.

Tout d'abord, on va définir les différents types de notre formalisme en ce basant sur notre définition de réseau de Petri précédente :

<?xml version="1.0" encoding="UTF-8"?>

<!-- file: evinrudenet.fml -->
<formalism name="Evinrude Net" xmlns="http://cosyverif.org/ns/formalism" xmlns:xi="http://www.w3.org/2001/XInclude">
  <xi:include formalismUrl="petrinet.fml"/>
  <nodeType name="virtualPlace"/>
</formalism>

Rajoutons quelques attributs pour gérer les input-place et output-place.

<?xml version="1.0" encoding="UTF-8"?>

<!-- file: evinrudenet.fml -->
<formalism name="Evinrude Net" xmlns="http://cosyverif.org/ns/formalism">
  <include formalismUrl="petrinet.fml"/>
  <nodeType name="virtualPlace"/>
  <leafAttribut name="isInput" default="false" refType="place"/>
  <leafAttribut name="isOutput" default="false" refType="place"/>
</formalism>

Maintenant pour gérer la hiérarchie et les places virtuelles nous devons autoriser les références vers les places pour les places virtuelles et vers des Evinrude Net pour les places :

<?xml version="1.0" encoding="UTF-8"?>

<nodeType name="place">
  <ref href="evinrudenet.fml"/>
</nodeType>

<nodeType name="virtualPlace">
  <ref href="#place" maxOccurs="1"/>
</nodeType>

L'attribut multiplicity permet de spécifier la multiplicité des références. La valeur par défaut est celle définie par le graphe c'est à dire «*». En spécifiant «1», on rend donc la référence obligatoire pour les places virtuelles.

Pour autoriser les références vers des modèles pour une place on doit redéfinir le type «place» défini dans petrinet.fml. La redéfinition écrase simplement l'ancienne sans conséquences sur les attributs, une place aura encore un nom.

On obtient donc au final cette spécification :

<?xml version="1.0" encoding="UTF-8"?>

<!-- file: evinrudenet.fml -->
<formalism name="Evinrude Net" xmlns="http://cosyverif.org/ns/formalism" xmlns:xi="http://www.w3.org/2001/XInclude">
  <xi:include formalismUrl="petrinet.fml"/>

  <nodeType name="place">
    <ref href="evinrudenet.fml"/>
  </nodeType>
  <nodeType name="virtualPlace">
    <ref href="#place" maxOccurs="1"/>
  </nodeType>

  <leafAttribut name="isInput" default="false" refType="place"/>
  <leafAttribut name="isOutput" default="false" refType="place"/>
</formalism>

FML_Diagram.png (71.9 KB) Clément Démoulins, 09/13/2012 11:48 am

exemple_model_1.png (8.61 KB) Clément Démoulins, 09/13/2012 11:48 am

exemple_model_2.png (60.4 KB) Clément Démoulins, 09/13/2012 11:48 am

GrML_Diagram.png (39.1 KB) Clément Démoulins, 10/04/2012 04:54 pm