如何解释 Alloy 个事实

Question

我正在阅读an article that uses Alloy to model some safety and security requirements for aircraft avionics。我很难理解文章中显示的 "fact constraints" 之一。

数据流入系统。数据由系统消耗。该模型声明了一组Data、一组System和一个consumedBy关系（Data is consumed by System）：

sig Data {
   consumedBy: some System
} 

sig System {}

模型然后声明一组 "criticality values." 关系将关键性映射到数据。另一个关系将关键性映射到系统：

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。您同意评论的这种解释吗？

现在，事实在 Alloy 中是这样表达的：

   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

以下Alloy事实与评论所表达的意思相同吗？

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

二：如果评论和Alloy事实不一样，那么Alloy中评论的正确表达方式是什么？

Answer 1

这是一个 Alloy 模型，它将论文的事实版本与我认为捕捉到你想要表达的内容进行比较：

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" 量词虽然具有非常简单的语义（"one x: S | P" 意味着 P 对于集合 S 中的一个 x 为真）可能会造成混淆，因为我们很想阅读量词在自然语言中。在 Software Abstractions 第 3 章的常见问题解答中，有半页讨论了这个示例，第 73 页。

如何解释 Alloy 个事实

How to interpret an Alloy fact

alloy