生產基於另一子集的原子的子集

我有以下模式：生產基於另一子集的原子的子集

sig A1 { 
// ... 
} 
sig A2 { 
// ... 
} 

sig S { 
    s_a1: one A1, 
    s_a2: one A2 
}

我想「生產」的子集S1：基於S0的元件S：S受以下約束：

S1具有相同數目的原子作爲S0
那些原子在S0滿足條件C1 [s_valid.s_a1] s_valid還必須包含在S1
每個這些原子s_invalid我ÑS0不滿足C1 [s_invalid.s_a1]必須有在S1中的原子與相同的S_A1但不同s_a2關聯

目的是模擬的一些集合中的項的修改。我試圖用理解表達式來解決這個問題，但我找不到在s_a2關聯中表達變化的正確方法。

來源

2017-06-23 Attila Karoly

這樣的事情？

-- s1 has the same number of atoms as s0 
#s1 = #s2 
-- those atoms s_valid in s0 that meet condition c1[s_valid.s_a1] must also be contained in s1 
{x: s0 | c1[x.s_a1]} in s1 
-- for each of those atoms s_invalid in s0 that does not meet c1[s_invalid.s_a1] there must be an atom in s1 with the same s_a1 but a different s_a2 association 
all x: s0 | not c1[x.s_a1] implies some y: s1 | y.s_a1 = x.s_a1 and y.s_a2 != x.s_a2

來源

2017-06-25 01:37:42

一個最有用的答案。我仍然需要做一些工作，因爲我的問題陳述不夠精確。通過類推，s0和s1是記錄集，s0包含一些帶有無效字段值的記錄，s1是糾正的記錄集，其中包含s0中的有效條目和s0中的無效條目的糾正版本。無論如何，這種方式更具有教育意義。 –

學習合金是一段美好的旅程。我發現它的確經常引發新的想法，而不僅僅是軟件，而且也是邏輯和物理世界的建模。謝謝教授。 –

生產基於另一子集的原子的子集

回答

相關問題