Describir: Hybrid State Petri Nets which Have the Analysis Power of Stochastic Hybrid Systems and the Formal Verification Power of Automata