Promela代在 AnyMath
运行代码生成器
从模型文件生成Promela代码 AnyMath 通过访问API执行 AnyMath 例如，从窗口 命令行 
:
engee.generate_code(source, destination, target="promela")哪里
-
资料来源--string，模型文件的路径。工程师; -
目的地--string，将放置生成文件的目录的路径。
API使用模型文件名作为生成文件的名称（后缀"。engee"排除在外），以新后缀"结尾。pml"。
例如，如果模型文件的路径为 资料来源 — "/user/models/large_model。工程师"，以及生成文件的目录 目的地 — "/用户/旋转"，然后用Promela语言生成的代码将被放置在一个文件中，其路径 — "/user/spin/large_model。pml".
正式核实程序 AnyMath
-
创建有限状态机模型（块内 Chart)在 AnyMath .
-
使用函数生成正式的Promela模型
generate_code指定目标语言:恩吉。generate_code(source,destination,target="promela").
-
以LTL公式的形式添加正式属性。
-
使用自旋工具检查模型。
-
结果分析：成功证明、反例、执行路径。
→ 
模型的局限性
如果模型包含不在列表中的块或类型，则调用API以生成Promela代码的尝试将失败。
不支持:
多重采样步骤;
*图表*区块的时间运算符(t, 以前, 之后…);
*图表块的操作员 计数 和 持续时间;
*Julia库函数，如 战俘, 楼层, 齐尔… .
数据类型支持
此外，仅支持由Promela中具有类似物的这些类型的元素组成的那些数据类型和数组。:
朱莉娅型 |
普罗梅拉型 |
|---|---|
|
|
|
|
|
|
|
|
Julia语法支持
Promela代码生成器支持在*Chart*块的代码插入中找到的几乎所有Julia语法和 支持C语言代码生成器。
许多设计在Promela中没有直接类似物，因此不支持。:
*操作员 继续;
*嵌套循环 为 （或具有复杂条件的循环）;
*周期 为 以1以外的增量计算;
*操作员 ,.
附加语法实现:
-
@后藤 -
@标签