nomoSDK : les formalismes

Dans le cadre de la conception dirigé par modèle, un modèle correspond à une description expliquant la relation entre les entrées et les sorties d'un système.

Un formalisme (ou méta-modèle) correspond aux concepts et leurs relations utiliser pour exprimer un modèle.

Pour chaque problème, le formalisme le plus adapté est utilisé facilitant ainsi la conception et la vérification.

Une solution réalisée à l'aide d'un formalisme se traduit ensuite en un programme nomo qui pourra être instancier au sein d'un programme principal. La traduction automatique en langage nomo assure l'interopérabilité des solutions développées.

Le logiciel nomoSDK offre deux formalismes : les automates à états finis et l'algèbre booléenne mais offre également la possibilité d'en ajouter de nouveaux formalismes.

Le formalisme des automates à états finis repose sur la notion d'état et de transition. Un automate possède un état. Le passage d'un état à un autre s'effectue via un événement. Une transition décrit le changement d'état de l'automate en fonction de l'arrivé d'un événement et de l'état courant.

Le langage choisi pour traduire ce formalisme des automates à états finis repose sur la syntaxe XML. L'élément automaton défini un automate en contenant des éléments state représentant les états de l'automate. Le premier élément state de l’élément automaton correspond à l'état initiale. Un élément state possède obligatoirement l'attribut name qui nomme l'état. Les transitions d'un état vers un autre sont décrit par les éléments transition contenu dans les éléments state. Les éléments transition possède obligatoirement deux attributs : event correspondant au nom de l'événement et target correspondant au nouvel état.

Lorsqu'un événement survient et que l'état courant ne possède aucune transition lié à cet évènement, l'automate reste à l'état courant.

L’illustration ci-dessous décrit graphiquement un exemple d'automate dont la description XML suit.

<program name="exemple" xmlns="http://www.nomoseed.org/program">
  <sdk>
    <formalism xmlns="http://www.nomoseed.org/sdk"
               xmlns:xsi="http://www.w3.org/2001/XMLSchema-instance"
               xsi:type="automaton">
      <automaton xmlns="http://www.nomoseed.org/automaton">
        <state name="S1">
          <transition event="E1" target="S2"/>
          <transition event="E3" target="S2"/>
        </state>
        <state name="S2">
          <transition event="E1" target="S2"/>
          <transition event="E3" target="S1"/>
          <transition event="E2" target="S1"/>
        </state>
      </automaton>  
    </formalism>
  </sdk>
</program>

La génération du code en nomo s'effectue au moment de l'édition des liens.

En langage nomo, l'état de l'automate correspond à la valeur de l'évènement de type de conception appelé state dont l'indice temporel est soit négatif soit nul. Dans le second cas, cela signifie que cette valeur d'état vient d'être affecté.

Aucune règle à l'extérieur du programme nomo décrivant l'automate doit être du type de conception appelé state défini dans le modèle nomo de l'automate qui a été généré automatiquement.

Les évènements proviennent des règles de conception type event défini dans le modèle nomo de l'automate appartenant à un programme contenant le programme décrivant l'automate, comme le montre la troisième partie du tutoriel.

À noter, dans l'exemple la différence entre l'implication de E1 lors de l'état S2 et de E2 lors de l'état S1. E1 entraine une nouvelle affectation de l'automate à l'état S2 alors que E2 laisse inchangé l'état courant. Autrement dit, E1 pendant S2 entraine une conclusion S2 avec un délai nul alors que E2 pendant S2 n'entraine rien. Mais dans les deux cas l'état de l'automate est logiquement inchangé.

Le modèle nomo généré a pour base le modèle suivant :

<model xmlns="http://www.nomoseed.org/model" name="automaton">
  <header xmlns="http://www.nomoseed.org/project">...</header>
  <definition>
    <conception_type name="state"/>
    <conception_type name="event"/>
  </definition>
</model>

L'algèbre booléennes repose d'une part sur un ensemble de deux valeurs de vérité {VRAI, FAUX} et d'autre part trois opérateurs : la conjonction (ET) , la disjonction (OU) et la négation (NON).

Toute variable ou composition de variable via les opérateurs et les parenthèses possède une valeur de vérité soit VRAI, soit FAUSSE.

La conjonction correspond à l’évaluation de la relation entre deux opérandes dont le résultat est VRAI si et seulement si la première opérande est à VRAI ET la seconde opérande est à VRAI, et FAUX dans les autres cas.

La disjonction correspond également à l’évaluation de la relation entre deux opérandes dont le résultat est VRAI si et seulement si la première opérande est à VRAI OU la seconde opérande est à VRAI, et FAUX dans les autres cas.

La négation possède une opérande et renvoie VRAI si et seulement si cette opérande est à FAUX, et FAUX dans l'autre cas.

Une opérande peut être soit une variable soit une composition de variable.

Le formalisme de l'algèbre booléenne dans le cadre du logiciel nomoSDK vise définir les implications de la véracité d'une composition de variables sur la valeur d'une variable. Par exemple, SI (a ET b) ALORS NON(c). L'évaluation de ces implications s'effectue à chaque interprétation.

Toutefois, la cohérence des implications logiques n'est pas vérifié, c'est-dire que SI a alors NON(b) et SI a alors b ne sera pas relevé comme une erreur. La première implication définie aura priorité.

De même SI a alors NON(a) se comprendra comme la variable a à VRAI à cette interprétation conduira à son affectation à FAUX pour l'interprétation suivante. Dans le cas de la présence l'implication symétrique SI NON(a) alors a, il y aura donc une oscillation de la valeur de vérité de la variable a.

L'expression de ce formalisme prend la syntaxe suivante :

• le symbole '.' correspond à l'opérateur de conjonction (a ET b ⇒ a.b),
• le symbole '+' correspond à l'opérateur de disjonction (a OU b ⇒ a+b),
• le symbole '^' correspond à la négation (NON(a) ⇒ a^),
• le symbole '*' correspond au ou-exclusif (a XOR b ⇒ a*b),
• le symbole ':' correspond à l'implication, à droite une fonction booléenne, à gauche, la liste des variables à affecter séparer par une virgule, la présence du nom d'une variable l'affecte à VRAI, le nom d'une variable suivie de l'opérateur de négation l'affecte à FAUX. (SI a ET b ALORS c ainsi que NON(b) ⇒ a.b : c, b^)
• ce qui suit le symbole '//' jusqu'à la fin de ligne est considéré comme du commentaire,
• les variables doivent respecter l'expression régulière [a-zA-Z]+[a-zA-Z0-9_]* à l'exception de i[0-9]* (voir plus bas)

Soit l'exemple suivant :

<program name="exemple" xmlns="http://www.nomoseed.org/program">
  <sdk xmlns:sdk="http://www.nomoseed.org/sdk">
    <formalism xmlns="http://www.nomoseed.org/sdk"
               xmlns:xsi="http://www.w3.org/2001/XMLSchema-instance"
               xsi:type="boolean_logic">
      <boolean_logic xmlns="http://www.nomoseed.org/boolean_logic">
        a + (c + d)^.b : c^
        c + d : a
        : c, d
      </boolean_logic>
    </sdk:formalism>
  </sdk>
</program>

Autrement-dit, les implications logiques suivantes :

SI (a OU (NON (c OU d) ET b) = VRAI ALORS c = FAUX SI (c OU d) = VRAI ALORS a = VRAI c = VRAI d = VRAI

Par défaut, aucune les variables n'est initialisé et aucune conjonction atomique possédant une variable non initialiser n'est évaluable.

Pour les initialisés à VRAI lors de la première interprétation, il faut utiliser l'opérateur d'affectation sans qu'il soit précédé par une quelconque fonction booléenne. Ainsi la troisième formule de l'exemple ci-dessus correspond à l'initialisation des variables c et d à VRAI.

A l'édition des liens, le code nomo est généré et la liste des conjonctions atomiques est inséré à la suite des formules booléennes. L'exemple ci-dessus devient alors :

<program name="exemple" xmlns="http://www.nomoseed.org/program">
  <sdk xmlns:sdk="http://www.nomoseed.org/sdk">
    <sdk:formalism xsi:type="sdk:boolean_logic">
      <boolean_logic xmlns="http://www.nomoseed.org/boolean_logic">
        a + (c + d)^.b : c^
        c + d : a
        : c, d^
 
        // Atomic conjunctions
        // a:c^
        // b.c^.d^:c^
        // c:a
        // d:a
        // :c
        // :d
      </boolean_logic>
    </sdk:formalism>
  </sdk>
</program>

À noter que par souci de simplification d'écriture des règles, il a été introduit les crochets ('[' et ']') afin de définir implicitement des variables intermédiaires sans nuire à la conception des implications booléennes. Soit l'exemple suivant qui permet de simplifier les conjonctions atomiques avec la création d'une variable intermédiaire i0 :

<program name="exemple" xmlns="http://www.nomoseed.org/program">
  <sdk xmlns:sdk="http://www.nomoseed.org/sdk">
    <sdk:formalism xsi:type="sdk:boolean_logic">
      <boolean_logic xmlns="http://www.nomoseed.org/boolean_logic">
        a + [(c + d)^.b] : c^
        b + [(c + d)^.b] : b^
        c + [(c + d)^.b] : a
        c + d : a
        : c, d^
 
        // Atomic conjunctions
        // a:c^
        // i0:c^
        // b:b^
        // i0:b^
        // c:a
        // i0:a
        // d:a
        // :c
        // :d^
        // b.c^.d^:i0
      </boolean_logic>
    </sdk:formalism>
  </sdk>
</program>

À chaque variable correspond un type de conception de même nom. Chacun de ces types possède deux items : true et false.

Lorsqu'une implication conduit à mettre une variable booléen à VRAI ou à FAUX, cela se traduit par l'introduction d'un évènement du type idoine avec la valeur correspondante et un indice temporel nul, cela peut être comme le front d'un signal. Une fois cette évènement produit un second de même type viendra mais avec un indice temporel négatif minimal ('MIN').

En dehors des implications booléennes, l'affectation d'une variable booléenne s'effectue simplement par la conclusion du type correspondant à la variable avec la valeur voulu et délai nul. La production du second évènement si il y a lieu est généré par les règles générées automatiquement du formalisme booléen.

L'ajout d'un nouvel formalisme s'effectue en créant dans le répertoire “nomoSDK/formalisms” un répertoire avec pour nom celui du nouveau formalisme “nom_du_formalisme” respectant l'expression régulière [a-zA-Z]+[a-zA-Z0-9_]*

Ce nouveau répertoire doit contenir au minimum trois fichiers : “name.csv”, “nom_du_formalisme.dll”, “nom_du_formalisme.xsd”

Le fichier “name.csv” sert à l’internationalisation du logiciel nomoSDK, il contient le nom du formalisme utilisé dans l'onglet accueil du logiciel en fonction de la langue codé selon la norme ISO 639 avec deux caractères en minuscule. Par exemple, celui du formalisme des automates à états finis contient les informations suivantes :

language,name
en,Automaton
fr,Automate

Le fichier “nom_du_formalisme.xsd” définit la grammaire du langage utilisé dans l'élément formalism d'un programme nomo. L'espace de nom cible de la grammaire (targetNamespace et xmlns) doit suivre la forme "http://www.nomoseed.org/nom_du_formalisme".

Le fichier “nom_du_formalisme.dll” correspond à la bibliothèque dynamique avec pour interface une fonction convention C dont le seul argument correspond au nom du fichier contenant le programme nomo à traiter :

 void formalismActualize(const char* file);

L'opération conduit à la création d'un fichier “formalism.log” contenant les erreurs relevées.

Si aucune erreur s'est produite, autrement dit si le fichier “formalism.log” est vide, alors le résultat de l'opération est sauvegardé dans file.