This is the documentation for PRISM's Java code: for the discrete-event simulation engine, see {@link simulator.SimulatorEngine}; for the explicit-state probabilistic model checking and abstraction-refinement, see package {@link explicit}.