该程序使用FSMSpec中提供的输入(见下文)来构建FSM的底层图形，并使用idris-ct在其上生成免费类别。然后，它使用执行中提供的初始状态和路径(分别称为x和[x1，.，xn])来评估组合idx；x1；.；xn。它返回SUCCESS或ERROR，具体取决于这是否定义了FREE类别中的有效态射。
这将在ELBA的二进制文件夹中安装二进制文件。通常情况下，~/.elba/bin如果该文件夹在您的路径中，您可以简单地调用fsm-oracle来测试它。
您可以在官方资源库中找到有关如何安装的ELBA和说明。
只需将您的输入(如下所指定的)放入一个文件中，例如input.JSON，然后运行：
如果执行有效，Idris将返回以下形式的json输出：
输入必须作为JSON馈送，并通过使用Typedefs转换为Idris术语和类型。FSM执行的IDRIS类型在文件Traph.idr中定义。
内部输入格式是FSMExec类型的术语，格式为(FSMSpec，FSMState，FSMPath)。它由三部分组成：运行执行的FSM规范(FSMSpec)、初始状态(FSMState)和要评估的操作列表(FSMPath)。
FSMSpec的类型是(NAT，LIST(NAT NAT))：FSM被指定为一对，其中第一个分量表示FSM的状态(顶点)的数目，而第二个分量是表示可能的动作的顶点对(边列表)的列表。
例如，(5，[(2，1)，(4，2)，(0，3)])指定具有5个顶点(枚举为0，1，2，3，4)和三个可能动作的FSM：一个从2到1，一个从4到2，以及一个从0到3。
边列表必须在顶点数指定的范围内。因此，诸如(5，[(7，1)，(4，2)，(0，3)])或(5，[(5，5)])的规范被认为是无效的，并且将产生错误。
FSMState的类型为NAT。这指定必须从其开始计算的初始顶点。
初始状态必须在FSMSpec中的顶点数指定的范围内。因此，例如，4是FSM(5，[(2，1)，(4，2)，(0，3)])的有效状态，而5不是，并且将产生错误。
列表中的每个数字必须在由FSMSpec中的边列表长度指定的范围内。因此，[1，0]是FSM(5，[(2，1)，(4，2)，(0，3)])的有效路径(表示首先使用从4到2的动作，然后是从2到1的动作)，而[3]不是。
如上所述的FSMSpec类型的术语必须作为输入馈送，并以JSON格式编码。JSON编码的实现方式可以在文件JSONFormat.idr中找到。
对元组和列表的常用方括号表示法进行编码。定义边的对编码为：
递归地应用这些定义，可以对任何FSMExec类型的术语进行编码。例如，下面是输入执行的JSON编码((5，[(1，1)，(3，4)，(2，1)])，2，[2，0，0])：
{"；_0"；：{"；_0"；：5，"；_1"；：[{"；Input"；：1，"；Output"；：1}，{"；Input"；：3，"；Output"；：4}，{"；输入"；：2，"；输出"；：1}]}，"；_1"；：2，"；_2"；：[2，0，0]}。
除非另有明确说明，否则此存储库中的所有文件都在GNU Affero通用公共许可证下获得许可。