Tutoriel sur Roméo

imt

1. Objectif

Nous allons ici apprendre les bases de l’utilisation du logiciel Roméo.

2. Installation

Voici le lien à suivre : http://romeo.rts-software.org/

Suivre les instructions d’installation pour votre OS : Windows, MacOS ou Linux

3. Lancement de Roméo

Lancez Roméo et vous devriez voir ceci

romeo

4. Design d’un premier réseau de Petri

Roméo est assez intuitif. Sur la gauche vous avez les éléments de votre réseau de Petri, à savoir des places et des transitions, et certains types particuliers de transitions dont nous parlerons plus tardivement.

Dessinons ce réseau de Petri qui représente la synchronisation de deux feux de circulation:

romeo2

5. Simulation

Nous allons maintenant pouvoir exécuter le simulateur de Roméo. C’est le même principe qeu ce que vous avez pu voir dans PIPE dans le précédent module.

  • on lance la simulation

  • on clique sur les transitions à exécuter

  • on observe l’évolution de nos tokens et de nos transitions pouvant être exécutées

romeo3

6. Model checker

Bien évidemment aucun intérêt à utiliser Roméo plutôt que PIPE si on se limite a dessiner et simuler des réseaux de Petri. L’intérêt de Roméo se trouve dans le fait qu’il contient un model-checker qui interprète une version allégée de la logique CTL vue en cours.

6.1. Lancer le model-checker

Cliquez sur le bouton Checker

romeo4

La fenêtre du model-checker s’ouvre. Dans Property nous allons pouvoir écrire les propriétés CTL à vérifier. Nous pourrons ensuite cliquer sur Check property.

Dans la sous-fenêtre d’affichage vous pouvez voir une espèce de documentation de l’utilisation de Roméo avec la syntaxe GMEC vue en cours et les propriétés temporelles suportées par Roméo (une sous partie de CTL). Vous y voyez également des exemples.

Comme vu dans les cours les propriétés du type EX et AX n’existe pas en Roméo.

6.2. Première propriété

Nous allons vérifier que pour toutes les branches (dans tous les cas) on atteint finalement un état où le feu 1 est vert :

AF(M(Vert1)==1)

Vous devriez observer le résultat suivant :

romeo5

La propriété est vraie.

6.3. Propriété fausse et trace du contre exemple

Testons cette propriété :

AG(M(Vert1)+M(Vert2)==1)

Vous devriez observer le message suivant

Checking property AG(M(Vert1)+M(Vert2)==1) on TPN: /home/hcoullon/Documents/TEACHINGS/FIT/simulation/mon_cours/feux_circulation.xml
Waiting for response (kill the romeo-cli process to interrupt)...
false

Trace: T7

Vous pouvez alors jouer la trace donnée en contre-exemple (ici simplement exécuter la transition T7) pour observer pourquoi votre propriété n’est pas vrai dans tous les cas.

Comment rendre cette propriété vraie ?

6.4. Tester d’autres propriétés

Trouvez d’autres propriétés à vérifier sur les feux de circulation et en trouver une signification en langage naturel.