關鍵詞：一些和一個更高階的量化前

我有一個合金規範代表模型轉換規則。在規範中，我使用高階量化來指定規則匹配。奇怪的是，分析儀與「一些」和「一個」的工作方式不同，這是我無法理解的。關鍵詞：一些和一個更高階的量化前

例如，在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

關鍵詞：一些和一個更高階的量化前

回答

相關問題