Tina version 3.4.4 -- 01/05/16 -- LAAS/CNRS

mode -R

INPUT NET ------------------------------------------------------- 

parsed net interblocage

## Description textuelle du reseau (voi FAQ) 

7 places, 6 transitions

net interblocage
tr FreeAB WorkAB -> A B idle 
tr FreeBA WorkBA -> A B 
tr OqpA A idle -> WaitB 
tr OqpAB B WaitB -> WorkAB 
tr OqpB B idle -> WaitA 
tr OqpBA A WaitA -> WorkBA idle 
pl A (1)
pl B (1)
pl idle (2)

0.000s

REACHABILITY ANALYSIS ------------------------------------------- 

bounded
## Reseau Borne


6 marking(s), 8 transition(s)
## Le graphe des marquages est constitué
## par 6 marquages et 8 transitions

MARKINGS:
## Liste des marquages

0 : A B idle*2
1 : B WaitB idle
2 : A WaitA idle
3 : WorkAB idle
4 : WaitA WaitB
5 : WorkBA idle*2

REACHABILITY GRAPH:
## Liste des transitions

0 -> OqpA/1, OqpB/2
1 -> OqpAB/3, OqpB/4
2 -> OqpA/4, OqpBA/5
3 -> FreeAB/0
4 -> 
5 -> FreeBA/0

0.000s

LIVENESS ANALYSIS ----------------------------------------------- 

not live
## reseau non vivant

not reversible
## reseau non réinitialisable 

1 dead marking(s),1 live marking(s)
0 dead transition(s), 0 live transition(s)

## 1     etat de blocage 
## 0 transitions mortes (non quasi vivantes)

dead marking(s): 4
# Liste des marquages morts (1 seul ici) 

STRONG CONNECTED COMPONENTS:

## Liste des composantes fortements connexes

0 : 4
1 : 5 3 2 1 0

## Quotient du graphe des marquages par les composantes fortements connexes

SCC GRAPH:

0 ->
1 -> FreeBA/1, FreeAB/1, OqpA/0, OqpBA/1, OqpAB/1, OqpB/0, OqpA/1, OqpB/1

0.000s

ANALYSIS COMPLETED ----------------------------------------------