Dataset supporting the publication "Formal Language Semantics for Triggered Enable Statecharts with a Run-to-Completion Scheduling"

This dataset is supporting the paper titled "Formal Language Semantics for Triggered Enable Statecharts with a Run-to-Completion Scheduling" in Proceedings of the 20th International Colloquium on Theoretical Aspects of Computing (ICTAC2023). The data includes the Rodin Archive which can be imported into the Rodin Platform. It was developed using Rodin 3.6. The bundle (RL2112) can be downloaded from the following link https://github.com/eventB-Soton/Rodin-Bundles/releases/tag/v3.6.0-2112 Users need to install Atelier-B prover additionally. The instructions can be found on this page https://www.uml-b.org/Downloads.html The archive contains one project called "triggered_statechart". The readers are recommended to browse the model in Rodin together with the accompanying PDF. The PDF contains the listing of the model in the ordered of development. In Rodin, one can also browse to see the proof. The data is under the CC-BY-SA license