Model Library

This is a collection of Supremica models used as benchmarks in research papers, and for education. To download, just right-click the links and choose “Save link as…” or similar. If you want to have your specific model published here, contact fabian at chalmers dot se.

Cluster Tool, untimed versions of the model from R. Su, J. H. van Schuppen and J. E. Rooda, The Synthesis of Time Optimal Supervisors by Using Heaps-of-Pieces, in IEEE Transactions on Automatic Control, vol. 57, no. 1, pp. 105-118, Jan. 2012. The different models have been extended with additional tools, for CTx the x denotes the number of tools. These models were generated by UltraDES. See also Lucas V. R. Alves, Lucas R. R. Martins, Patricia N. Pena, UltraDES – A Library for Modeling, Analysis, and Control of Discrete Event Systems, 20th World Congress The International Federation of Automatic Control Toulouse, France, July 9-14, 2017.

CT7 CT10 CT11 CT12 CT15 CT17

Benchmark files for Mohammad Reza Shoaei, Laura Kovács, Bengt Lennartson. Supervisory Control of Discrete-Event Systems via IC3, Haifa Verification Conference HVC 2014: Hardware and Software: Verification and Testing pp 252-266:

CMT1_5 CMT3_3 CMT5_5 CMT7_7 EDP5_10 EDP5_50 EDP5_100 EDP5_200 EDP5_500 EDP5_1000 PME Production_cell_complete_BDD

Cat and mouse model from the original R&W papers but with the forbidden states where the cat and the mouse are simultaneously in the same room specified in a “modular” fashion, as described by Patrik Magnusson, Martin Fabian, Knut Åkesson. Modular specification of forbidden states for supervisory control IFAC Proceedings Volumes. 10th International Workshop on Discrete Event Systems (WODES), Berlin, 30 August – 1 September 2010. Vol. 10, p. 412-417 See the model comments for details.

CatMouse_ForbiddenStates