The Refinement Calculus of Reactive Systems Toolset - Feb 2018

Distribution of the Refinement Calculus of Reactive Systems (RCRS) Toolset. Includes full RCRS formalization in the Isabelle proof assistant, Formal Analyzer implemented on top of Isabelle, Translator of Simulink models to RCRS, sample Simulink models, and demonstration files with instructions.<br>RCRS is fully implemented in the Isabelle theorem prover. The RCRS implementation currently consists of 22 Isabelle theories (.thy files).<br>This dataset is in .zip archive format and can be uncompressed using standard compression software. This dataset consists of:<br><b>- instructions-figshare.txt - </b>Step-by-step instructions on how to use this artifact to replicate the results in the TACAS 2018 paper: "The Refinement Calculus of Reactive Systems Toolset" in openly accessible .txt format.<b>- RCRS_Demo.thy - </b>a demo file for RCRS in openly-accessible Isabelle <b>.thy</b> format. <b>- Documentation/ - </b>guidance documents in openly accessible <b>.pdf </b>format on RCRS and a theory dependency graph.<b>- RCRS/ - </b>data are in either openly-accessible Python language <b>.py</b> format or Isabelle theorem <b>.thy</b> format. RCRS contains two subfolders: I. The "Isabelle" folder contains the implementation of RCRS into the Isabelle proof assistant. See file "document.pdf" for documentation on the subfolders. II. The "Simulink2Isabelle" folder contains the "simulink2isabelle.py" translator: it translates Simulink models into RCRS/Isabelle theories.<br><b>- Simulink_models/ </b> - data are in <b>.slx</b> format, accessible via MathWorks Matlab/Simulink. These form the Translator inputs.<br>The instructions allow to reproduce in full the results reported in the paper "The Refinement Calculus of Reactive Systems Toolset", TACAS 2018.<br>

反应式系统精化演算（Refinement Calculus of Reactive Systems, RCRS）工具集的分发资源。包含完整的RCRS形式化规约（基于Isabelle证明助手（Isabelle proof assistant）实现）、基于Isabelle开发的形式化分析器、Simulink模型到RCRS的转换器、示例Simulink模型，以及附带使用说明的演示文件。
RCRS完全基于Isabelle定理证明器（Isabelle theorem prover）实现，当前的RCRS实现包含22个Isabelle理论文件（.thy格式）。
本数据集采用.zip压缩归档格式，可通过标准解压软件进行解压。数据集具体组成如下：
- instructions-figshare.txt：以开放可获取的纯文本（.txt）格式提供的分步操作指南，可用于复现TACAS 2018论文《反应式系统精化演算工具集》（原英文标题：*The Refinement Calculus of Reactive Systems Toolset*）中的实验结果。
- RCRS_Demo.thy：以开放可获取的Isabelle理论（.thy）格式提供的RCRS演示文件。
- Documentation/：以开放可获取的便携式文档格式（.pdf）提供的RCRS相关指导文档与理论依赖关系图。
- RCRS/：数据文件分为开放可获取的Python语言脚本（.py格式）与Isabelle定理证明理论（.thy格式）两类。该目录包含两个子文件夹：
I. “Isabelle”子文件夹：实现了RCRS到Isabelle定理证明器的集成。可通过文件“document.pdf”查阅该子文件夹的相关文档说明。
II. “Simulink2Isabelle”子文件夹：包含转换器工具“simulink2isabelle.py”，可将Simulink模型转换为RCRS/Isabelle理论文件。
- Simulink_models/：数据采用MathWorks Matlab/Simulink支持的.slx格式，作为转换器的输入样本。
本分步操作指南可完整复现TACAS 2018论文《反应式系统精化演算工具集》（原英文标题：*The Refinement Calculus of Reactive Systems Toolset*）中报告的全部实验结果。