AGAVE是一种用于验证不断发展的软件规格的敏捷迭代和增量工具。 AGAVE可以应用于不同的建模语言，但是到目前为止，已经实现了针对Path-CTL属性验证Statechart的功能。 该工具将两个XML文件作为输入，一个XML文件表示系统模型（状态图），另一个XML文件表示要验证的属性（在Path-qCTL中）。 该属性被指定到txt文件中。 该工具返回“ true”，“ false”或“ conditional”。 在条件情况下，还会报告一组对透明状态的约束。 AGAVE将三个文件作为输入：Example1.xml包含要分析的Statechart Example1Property.txt包含要验证的属性Example1InitialState.txt包含原子命题的初始值。要运行AGAVE，请在同一目录中下载这三个文件以及AGAVE.jar。文件夹 。 然后，从命令行键入：java -jar AGAVE.jar
