Newer
Older
COSMOS_ProductionLines
Generators of .gspn files (for COSMOS model checker) corresponding to DTMC models of production line systems (blocking-after-service policy) consisting of an arbitrary number N of machines
directory gspn_prodLines/ contains COSMOS .gspn files for DTMC models of production lines with different number of machines and generated through the Java generator (contained in directory Generators) using different configFiles
directory GSPN_Generator contains the generator (written in Java) for automatically creating the .gspn file, based on a configuration file.
directory GSPN_Generator/configFiles contains a few examples of configuration files used to generate the COSMOS .gspn models
How to generate a COSMOS .gspn from a productionLine configFile:
- javac CosmosGenerator_2phases.java
- java CosmosGenerator_2phases configFileName (e.g. java CosmosGenerator_2phases 5M)