Struct version 2.9.0 -- 02/12/08 -- LAAS/CNRS

parsed net bdd0

7 places, 6 transitions

net bdd0
tr arrivee_ecrivains writers -> wait_writers 
tr arrivee_lecteurs readers -> wait_readers 
tr debut_ecriture lock*5 wait_writers -> writting 
tr debut_lecture lock wait_readers -> reading 
tr fin_ecriture writting -> lock*5 writers 
tr fin_lecture reading -> lock readers 
pl lock (5)
pl readers (6)
pl writers (3)

0.002s

P-SEMI-FLOWS GENERATING SET ------------------------------------- 

invariant

wait_writers writers writting
lock reading writting*5
readers reading wait_readers

0.000s

T-SEMI-FLOWS GENERATING SET ------------------------------------- 

consistent

arrivee_lecteurs debut_lecture fin_lecture
arrivee_ecrivains debut_ecriture fin_ecriture

0.000s

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