0

我想应用一个规则：

rule <k> __BETA__ => __PROCESS__ </k>
     <processes> S:Set </processes>

如果S不包含任何形式的项目SetItem( new X . P )or SetItem( P | Q )。

我在手册中读到存在一个:=和:/=模式匹配的运算符，但没有它的用​​法示例，我不知道它是否是我需要的。

我记得看到 K 对 Sets 没有负模式匹配，但有没有一些可以实现与:/=运算符等效的？

顺便说一句，K 是否可以同时匹配和修改一个集合中的两个项目？我尝试了规则：

  rule <k> __PROCESS__ => __BETA__ </k>
       <processes> 
         ... 
         ( SetItem( A:KVar < B:KVar > . P:Process ) => SetItem( P ) )
         ( SetItem( A:KVar [ X:KVar ] . Q:Process ) => SetItem( Q[B/X] ) )
         ... 
       </processes>

但语义卡住了。这是有效的语法吗？

4

1 回答 1

1

我必须查看您的语义才能提供更好的建议，但在我看来，您正在尝试使用Set集合来存储一堆进程，并且每个进程都有自己的代数项，表示当前进程状态。

在这种情况下，我建议使用 K 的 Cell 多重性功能而不是将其存储在 a 中Set，模式匹配在那里会更好地工作。我不确定，但我们可能不支持您在此处尝试的 Set 模式匹配。如果你能做一个最小的例子，请向https://github.com/kframework/k提交问题，我们会得到支持。

不过，使用 K 的单元多重性肯定会起作用，您可以执行以下操作：

    configuration <k> $PGM:Pgm </k>
                  <processes>
                    <process multiplicity="*" type="Set"> .Process </process>
                  </processes>

  rule <k> __PROCESS__ => __BETA__ </k>
       <processes>
         <process> A:KVar < B:KVar > . P:Process ) => P      </process>
         <process> A:KVar [ X:KVar ] . Q:Process ) => Q[B/X] </process>
         ...
       </processes>

为了说明当进程没有匹配其他模式时应该发生某些事情，我会推荐一个owise规则：

    rule <k> __BETA__ => __DO_SOMETHING__ </k>
         <process> new X . P </process>

    rule <k> __BETA__ => __DO_SOMETHING__ </k>
         <process> P | Q </process>

    rule <k> __BETA__ => __DO_SOMETHING_DIFFERENT__ </k> [owise]

如果Set出于其他原因必须保留它，仍然可以使用[owise]规则方法。或者，如果您不喜欢这种[owise]方法，您可能需要一个函数来告诉您是否有任何流程符合您的标准。

例如，使用 K 多重性方法：

    rule <k> __BETA__ => __DO_SOMETHING__ </k>
         <processes> PROCESSES </processes>
      requires shouldDoSomething?(<processes> PROCESSES </processes>)

    rule <k> __BETA__ => __DO_SOMETHING_DIFFERENT__ </k>
         <processes> PROCESSES </processes>
      requires notBool shouldDoSomething?(<processes> PROCESSES </processes>)

    syntax Bool ::= shouldDoSomething? ( ProcessesCell ) [function]

    rule shouldDoSomething?( _ ) => false [owise]
    rule shouldDoSomething?( <processes> <process> new X . P </process> ... </processes> ) => true
    rule shouldDoSomething?( <processes> <process> P | Q     </process> ... </processes> ) => true

您可以使用该Set方法做同样的事情，只需定义排序而不是shouldDoSomething?(_)排序。诚然，我仍然在 的定义中使用 an ，但是您可以通过显式枚举所有潜在模式并递归地从集合中删除不符合条件的进程来避免它，直到您到达空包：SetProcessesCellowiseshouldDoSomething?(_)

    rule shouldDoSomething?( <processes> .Bag </processes> ) => false
    rule shouldDoSomething?( <processes> (<process> P ; Q </process> => .Bag) ... </processes>
    rule shouldDoSomething?( <processes> <process> new X . P </process> ... </processes> ) => true
    rule shouldDoSomething?( <processes> <process> P | Q     </process> ... </processes> ) => true

在这个例子中，你可以看到我正在从进程P ; Q包中删除所有进程，但是如果我找到一个是new X . Por P | Q，我说的是true，并且如果我们到达空的进程包（所以没有其中有new X . P或P | Q) 然后我们说false。

于 2020-05-24T09:39:54.777 回答