Commit 57b04836 authored by Ballarini Paolo's avatar Ballarini Paolo

Update README.md

parent 4ff87f3b
# PRISM_ProductionLines
Generators of PRISM code for DTMC models of production line systems (blocking-after-service policy)
\ No newline at end of file
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.
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment