Generators of PRISM code for DTMC models of production line systems (blocking-after-service policy)- directory 1_slot_models/ contains PRISM files for DTMC models of the 1-slot type. PRISM models of this kind consist of single module with no synchronisation. The resulting DTMC has reduced state-space (compared to modles of 2-alot type) at the cost of a much larger PRISM code. - directory 2_slot_models/ contains PRISM files for DTMC models of the 2-slot type. PRISM models of this kind consist of several synchronising modules and exploit PRISM module replication. The resulting DTMC has larger state-space (because of extra fictitious states being added) but PRISM code is shorter (hence allowing a better scaling w.r.t. the number of machines of the production line). - directory Generators contains the generators for automatically creating the PRISM models, based on a configuration file. - directo Generators/configFiles contains a few examples of configuration files used to generate the PRISM models in 1_slot_models and 2_slot_models.