如何解释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章常见问题解答中，有半页讨论了这个例子。