|
本文针对可用于建模、模型检测的工具Groove的一些内容。
鉴于csdn、百度、知乎等都没有很多相关内容，特记录一些学习过程中遇到问题，以便大家讨论。内容如有任何不当地方，请不吝赐教，万分感谢。
一、软件官网及下载问题
官网地址：https://groove.ewi.utwente.nl/
下载地址：https://sourceforge.net/projects/groove/
在几个同名软件的影响下没能第一时间顺利找到、下载这个软件。
在此贴出官网和下载界面，避免需要的小伙伴浪费时间。
二、Groove简介
groove介绍。可以不用在这第二部分浪费时间。
Groove工具集包括一个用于创建图生成规则的编辑器、一个用于可视化计算由一组图生成规则引起的图转换的模拟器、一个用于自动探索状态空间的生成器、一个支持 CTL 和 LTL 公式的模型检查器以及一个成像用于将图形转换为图像的工具。
组成部分：
- 模拟器。一个图形界面工具，允许对规则和图形进行图形编辑，并集成了生成器和模型检查器的功能（见下文）。此外，模拟器允许用户通过手动将规则应用于主机图来交互式探索 LTS。
- 发电机。生成 GPS 状态空间的命令行工具。状态空间存储为标记转换系统 (LTS)，其中每个状态都是一个图，转换由规则应用程序标记。
探索状态空间所依据的策略（例如，深度优先、广度优先等）可以设置为参数。 - 模型检查器。一个命令行工具，用于检查以 CTL 时间逻辑表示的属性是否在由 Generator 生成的状态空间模型中成立。
|