mCRL2 models, requirements and test logs for the EULYNX Point interface case study

mCRL2 models and mu-calculus formulas for the EULYNX Point Interface. Models and requirements are made in the context of the FormaSig project. Data is made available for replication purposes. REQ_P_001, REQ_P_001_1 and REQ_P_002 are requirements for the point specific mCRL2 model point_spec.mcrl2 Remaining .mcf files are requirements for the generic PDI interface pdi_spec.mcrl2 Artifacts relating to testing are: An mCRL2 model, mbt.mcrl2 A rename file to rename internal actions to tau, rename_file.re Partial state space associated to mbt.mcrl2, partial_state_space.aut The weak-trace bisim reduced version of the state space, partial_state_space_reduced.aut Testing logs, test-logs.zip本数据集包含面向EULYNX点接口（EULYNX Point Interface）的mCRL2模型与μ演算（mu-calculus）公式。所有模型与需求均依托FormaSig项目构建，公开该数据集的目的是支持研究成果复现。REQ_P_001、REQ_P_001_1与REQ_P_002为专用mCRL2模型point_spec.mcrl2对应的需求；剩余的.mcf文件均为通用PDI接口pdi_spec.mcrl2的需求。与测试相关的工件包括：mCRL2模型mbt.mcrl2；用于将内部动作重命名为τ动作的重命名文件rename_file.re；关联至mbt.mcrl2的部分状态空间文件partial_state_space.aut；该状态空间经弱迹双模拟（weak-trace bisimulation）约简后的版本partial_state_space_reduced.aut；测试日志压缩包test-logs.zip。