Définition d'un réseau de Petri au format tina

pl debut (1)
tr cparti debut -> parallele1 parallele2
tr branche1 parallele1 -> finbranche1
tr branche2 parallele2 -> finbranche2
tr synchro finbranche1 fingranche2 ->

Plus d'infos ici: Formats TINA

Fichiers

Extension	Format
.net	réseau de Petri textuel
.ndr	réseau de Petri graphique
.aut	Automate textuel
.adr	Automate graphique

(dr = draw)

nd (net draw)

nd est installé avec tina, il vous suffit de lancer la commande nd.
Dès le lancement vous êtes en mode édition de réseaux de Petri.

Action	Bouton(s)
Création d'une place	souris milieu
Création d'une transition	Ctrl + souris milieu
Création d'un arc	souris milieu en restant appuyant entre la place et la transition, ou la transition et la place.
Édition d'une place, d'une transition, d'un arc, pour changer le nom, le poids ou le marquage	souris droit
Supprimer une place, transition, arc	touche suppr !

Pour faire une vérification faites :
tools -> reachability analysis : markings graph avec verbose ou automaton

SELT Model-Checker SE-LTL

Manuel SELT