README.md 1.06 KB
Newer Older
Ballarini Paolo's avatar
Ballarini Paolo committed
1 2
# PRISM_ProductionLines

Ballarini Paolo's avatar
Ballarini Paolo committed
3 4 5 6 7 8 9 10 11 12
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.