I have added an option that generates the label, state, and transition files that can be used to build an explicit model. I am fairly confident that the transient and steady state analysis outputs give the the probability that the model is in a given at the end of the analysis where the given state is the one in parentheses. Currently the explicit states do not stop once the finish condition is reached because I thought it may be interesting to analyze the model when it starts in the all zero state and see the probability that it generates an error. I don't know if that will be useful or not, but I plan on adding an option that recognizes the finish condition tomorrow. The next thing that may be interesting that I noticed in the documentation is the -simpath tag. I am going to dig into that as well to see if it can more closely match NGDBF iterations since PRISM's iterations are different. I have also added more trapping sets to load_trapping_sets.m.
#^https://github.com/fluentverification/usu_stochastic_case_studies/tree/master/ngdbf_models
