关键词：一些和一个更高阶的量化前

我有一个合金规范代表模型转换规则。在规范中，我使用高阶量化来指定规则匹配。奇怪的是，分析仪与“一些”和“一个”的工作方式不同，这是我无法理解的。关键词：一些和一个更高阶的量化前

例如，在pred rule_enter [trans：Trans]（请参见第240行）中，我使用两个更高阶的量化来编码图转换规则的左侧和右侧的匹配。 *********************示例************************** ************

some e_check0:Acheck&trans.darrows, e_TP0:ATP&(trans.source.arrows-trans.darrows), e_PF10:APF1&trans.darrows, e_TR0:ATR&(trans.source.arrows-trans.darrows), e_F1R0:AF1R&trans.darrows | 
let n_P0 = e_check0.src, n_T0 = e_TP0.src, n_R0 = e_TR0.trg, n_F10 = e_PF10.trg | 
(n_P0 = e_check0.trg and n_P0 = e_TP0.trg and n_P0 = e_PF10.src and n_T0 = e_TR0.src and n_F10 = e_F1R0.src and n_R0 = e_F1R0.trg and 
n_F10 in NF1&trans.dnodes and 
n_P0 in NP&(trans.source.nodes-trans.dnodes) and n_T0 in NT&(trans.source.nodes-trans.dnodes) and n_R0 in NR&(trans.source.nodes-trans.dnodes)) 

some e_crit0:Acrit&trans.aarrows, e_TP0:ATP&(trans.source.arrows-trans.darrows), e_PF20:APF2&trans.aarrows, e_TR0:ATR&(trans.source.arrows-trans.darrows), e_F2R0:AF2R&trans.aarrows | 
let n_P0 = e_crit0.src, n_T0 = e_TP0.src, n_R0 = e_TR0.trg, n_F20 = e_PF20.trg | 
(n_P0 = e_crit0.trg and n_P0 = e_TP0.trg and n_P0 = e_PF20.src and n_T0 = e_TR0.src and n_F20 = e_F2R0.src and n_R0 = e_F2R0.trg and 
n_F20 in NF2&trans.anodes and 
n_P0 in NP&(trans.source.nodes-trans.dnodes) and n_T0 in NT&(trans.source.nodes-trans.dnodes) and n_R0 in NR&(trans.source.nodes-trans.dnodes))

这里我使用了关键字 “一些”。分析仪可以使用示波器10.

但是，如果使用关键字“one”，分析仪会报告示波器5的以下错误： ************** *******示例**************************************

Executing "Check check$1 for 5 but exactly 1 Trans, exactly 2 Graph, exactly 1 Rule" 
    Solver=minisat(jni) Bitwidth=0 MaxSeq=0 SkolemDepth=1 Symmetry=20 
    Generating CNF... 
. 
Translation capacity exceeded. 
In this scope, universe contains 89 atoms 
and relations of arity 5 cannot be represented. 
Visit http://alloy.mit.edu/ for advice on refactoring.

我的问题就是为什么两个量化有不同的表现？

来源

2014-06-23 wxlfrank

对于您的示例，我没有具体的答案，但通常编码one要比some更复杂：假设您有一个可最大限度地包含元素a，b，c的集合S.

合金将问题转化为SAT问题。您可以使用3个布尔变量xa,xb,xc对SAT进行编码，其中xa=TRUE（或FALSE）表示a在S（而不在S中）。

语句some S现在可以容易地编码为式

xa \/ xb \/ xc

（与\/作为逻辑或）。

在另一方面，为one需要额外编码，如果变量xa，xb之一，xc是真的，其他都是假的。例如。

xa \/ xb \/ xc 
xa => not(xb \/ xc) 
xb => not(xa \/ xc) 
xc => not(xa \/ xb)

在conjuctive范式（CNF，这就是国家税务总局解算器作为输入），你有条款：

xa \/ xb \/ xc 
-xa \/ -xb 
-xa \/ -xc 
-xb \/ -xa 
-xb \/ -xc 
-xc \/ -xa 
-xc \/ -xb

或许有一些技术来优化，但你可以看到，one需要更多子句编码比some。

来源

2014-06-24 08:38:37 danielp

合金中一般不允许高阶定量。然而，一些存在的量化（即，，一些）可通过称为skolemization一个过程，这相信不适用于唯一的量化（转换成可解程序即一个）。对于（一阶）合金实例，该过程被简要地解释为here。

我无法处理你的例子（对不起），但我想这是一个这样的例子。

来源

2014-06-24 09:18:43

在合金one使用集理解和基数操作者，例如编码，

one s: S | p[s]

转化为

#{s: S | p[s]} = 1

集理解不能skolemized，所以当所讨论的量词较高顺序，合金简单地放弃。

来源

2014-06-24 17:14:11

关键词：一些和一个更高阶的量化前

回答

相关问题