在 K 中操纵全局状态的有状态规则?

Question

K 是否有规则可以访问的全局状态的概念？ 例如 说一个配置C => C'。我想转换一组探索状态中不存在C'然后通过向其添加C'来更新全局探索状态集。

我正在尝试不确定地探索程序的所有可访问状态(使用 --search 选项(。但是，探索的每条路径都是独立的，这意味着如果我在配置本身中传递探索集，则每条路径都不会知道在其他路径中看到的配置。

如果没有全局状态，这种行为的最佳实践是什么？有没有办法在每个独立路径能够访问的更大环境中不确定地探索转换？

Answer 1

如果需要，您始终可以自己模拟此行为，但它非常麻烦且容易出错：

configuration <myConfig>
<k> $PGM:Pgm </k>
<someOtherCells> .SomeOtherSort </someOtherCells>
</myConfig>
<states> .List </states>
syntax Pgm ::= "saveConfig" | "loadConfig" Int | "isExplored?"
syntax Bool ::= "#isExplored?" "(" MyConfigCell "," List ")"
rule <myConfig> <k> saveConfig => . ... </k> ... </myConfig> #as CONFIGURATION
<states> ... (.List(CONFIGURATION)) </states>
rule (<myConfig> <k> loadConfig IDX ~> REST </k> ... </myConfig> => STATES[IDX])
<states> STATES </states>
requires IDX <Int size(STATES)
rule <myConfig> <k> isExplored? => #isExplored?(CONFIGURATION, STATES) ... </k> ... </myConfig> #as CONFIGURATION
<states> STATES </states>

然后，您需要提供是否已通过#isExplored?函数探索状态的定义。直接平等可能有效(使用==K(，但可能不行。您可能只想实际比较那里的某些单元格子集。

不幸的是，这种状态折叠功能尚未内置于Haskell后端中。当然，它可以自动检查每个新访问的状态，以查看它是否是以前探索过的状态，如果是，请停止在该执行路径上进行搜索。如果您需要此功能，请在 https://github.com/kframework/kore 存储库中提出问题，并解释您的用例。没有关于它很快实施的承诺，但对我们来说，了解人们希望如何使用该工具会很好。