如何解释合金事实

Question

我正在阅读an article that uses Alloy to model some safety and security requirements for aircraft avionics。我很难理解文章中显示的“事实限制”之一。

数据流入系统。数据由系统使用。该模型声明了一组Data，一组System，以及一个consumedBy关系（Data被System消费）：

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

二：如果comment和Alloy fact不一样，那么Alloy中comment的正确表达方式是什么？

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”量词虽然具有非常简单的语义（“one x: S | P”意味着 P 对于集合 S 中的一个 x 为真）可能会令人困惑，因为我们很想在自然语言。在第 73 页的软件抽象第 3 章的常见问题解答中有一个半页的示例讨论。