时间戳

首页 > 解决方案 > 在 K 中操纵全局状态的有状态规则？

kframework - 在 K 中操纵全局状态的有状态规则？

问题描述

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

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

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

标签： kframework

解决方案

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

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存储库中打开一个问题，并说明您的用例。没有承诺很快就会实施，但我们很高兴知道人们希望如何使用该工具。

推荐阅读