如何解释合金事实-Java 学习之路

我正在读an article that uses Alloy to model some safety and security requirements for aircraft avionics . 我正在努力理解文章中显示的一个"fact constraints" .

数据流入系统 . 数据由系统使用 . 该模型声明了一组Data，一组System和一个consumeBy关系（System使用Data）：

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

以下Alloy事实是否表达与评论相同的内容？

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

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

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

如果执行此操作，您将得到以下反例，显示两者之间的差异：

enter image description here

简而言之，纸质版本说两者都只有一个共同点;你的版本说基准和系统都与一个关键性相关联，并且它是相同的（更强） .

我不知道在这种情况下哪个是对的 .

“一个”量词，虽然有一个非常简单的语义（“一个x：S | P”意味着P对于集合S中的一个x是真的）可能会令人困惑，因为我们很想读自然语言中的量词 . 在第73页的软件抽象第3章的常见问题解答中有一个半页讨论 .

回复于 2024-04-26T20:16:01+08:00

如何解释合金事实

1 回答

相关问题