Recently I downloaded PIPE2 which is the Platform Independent Petri Net editor written in Java. It's an impressive open source and FREE tool to that allows you to model Generalized Stochastic Petri Nets (GSPNs).
So I fired it up and decided to build a simple Producer / Consumer model, aka the "bounded buffer problem". Here's the GSPN I drew with the PIPE2 editor.
Notice that the highest firing rate for the producer is 100 times that of the consumer (on both timed transitions). This means we would mostly expect the input buffers to be highly utilized and the PIPE2 analysis shows this.
Here is PIPE's classification of the above GSPN.
Petri net classification results
State Machine  false 
Marked Graph  true 
Free Choice Net  true 
Extended Free Choice Net  true 
Simple Net  true 
Extended Simple Net  true 
Here is PIPE2's GSPN analysis of the Petri Net.
GSPN Steady State Analysis Results
Steady State Distribution of Tangible States  

Average Number of Tokens on a Place  

Token Probability Density  

Throughput of Timed Transitions  

Sojourn times for tangible states  

State space exploration took 0.051s
Solving the steady state distribution took 0.015s
Total time was 0.747s
Finally here is the reachability graph produced PIPE2.
The file format of the saved GSPNs is in an XML dialect. As you can see PIPE to is more than just a graphical GSPN editor it also does some heavy lifting with the analysis.
I have been able to import the above GSPN into Mathematica but I haven't done much with it in there yet. That's for tomorrow!
Phil