如何解釋Alloy事實

Question

我正在閱讀an article that uses Alloy to model some safety and security requirements for aircraft avionics。我正在努力理解文章中顯示的「事實約束」之一。

數據流入系統。數據被系統消耗。該模型聲明的一組數據，一組系統，和一個consumedBy關係（數據由系統消耗的）：

sig Data { 
    consumedBy: some System 
} 

sig System {} 

然後，該模型聲明瞭一套「臨界值」。關係將關鍵性映射到數據。另一個關係將關鍵性映射到系統：

sig Criticality { 
    concernedData: one Data, 
    concernedSystem: one System 
} 

接下來，模型表達兩個事實。這是我掙扎的第二個事實。

第一個事實說，每個系統消耗的至少一個數據：

all s: System | some consumedBy.s 

文章有關於第二個事實此評論：

// for any system which consumes a given datum, 
    // the said datum and system should belong to 
    // a same unique criticality 

我覺得評論是這樣說：如果一個系統消耗一個數據，那麼數據和系統必須具有相同的關鍵性。例如，如果數據D1被系統S1消耗並且數據D1具有關鍵性C1，那麼系統S1也必須具有關鍵性C1。你是否同意對評論的解釋？

現在，這裏的事實是如何在合金表示：

all d: Data | all s: System | one c: Criticality | 
     c.concernedData = d and c.concernedSystem = s 

我怎麼讀這個事實的理解是這樣的：

The following constraint holds for exactly one c in Criticality: 
    For every d in Data and every s in System: 
     c.concernedData = d and c.concernedSystem = s 

是這樣的事實，一個正確的認識？如果是這樣，我不認爲這個事實表達了與評論中的描述相同的內容。

所以我的問題是：

一：評論這樣說：

// for any system which consumes a given datum, 
    // the said datum and system should belong to 
    // a same unique criticality 

執行以下合金事實表達了同樣的事情有何評論？

all d: Data | all s: System | one c: Criticality | 
     c.concernedData = d and c.concernedSystem = s 

二：如果評論和合金其實是不一樣的，又是什麼來表達合金的評論的正確方法？

Answer 1

這裏要說的是事實的文件的版本進行比較，以我所認爲的合金模型捕捉你想表達什麼：

sig Data {consumedBy: some System} 
sig Criticality { 
    concernedData: one Data, 
    concernedSystem: one System 
} 
sig System {} 

// the paper's statement: 
// for any system which consumes a given datum, 
// there is one criticality that has that data and system 
// as its concernedData and concernedSystem 
pred Paper { 
    all d: Data | all s: d.consumedBy | one c: Criticality | 
     c.concernedData = d and c.concernedSystem = s 
    } 

// your interpretation: 
// If a system consumes a datum, then the datum and the system 
// must have the same (single) criticality 
pred You { 
    all d: Data | all s: d.consumedBy | 
    concernedData.d = concernedSystem.s and one concernedSystem.s 
    } 

check {Paper implies You} for 2 

如果執行此，您會收到以下反顯示的區別兩個：

總之，紙質版本說只有一個雙方共享臨界;你的版本說基準和系統每個都與一個關鍵性相關聯，並且它是相同的（這是更強的）。

我不知道在這種情況下哪個是正確的。

「一個」量詞雖然有一個非常簡單的語義（「one x：S | P」意味着P對於集合S中的一個x是真實的）可能會令人困惑，因爲我們如何試圖讀取量詞以自然語言。在第73頁的軟件抽象第3章常見問題解答中，有半頁討論了這個例子。