违反 alloy 中的事实

Question

我正在创建 bell lapadula，这是我的代码。

abstract sig classificaion{}
one sig classified extends classification{}
one sig unclassified extends classification{}
sig user{ level: one classification,
    r,w: set object}
sig object{ sec: one classification}
fact policy1{no((classified.~sec).~r & unclassidied.~level)}
fact policy2{no((unclassified.~sec).~w & classifed.~level)}

我想测试策略 1。所以我在我的代码中添加了这个来检查它是否会违反 policy1。但我一直在“级别：”

中收到错误

one sig usera extends user{}{
level: one classified,
r: set objecta
}
one sig objecta extends object{}{
sec: one unclassified
}

Answer 1

你可能想写：

one sig usera extends user{}{
level= classified
r=objecta
}
one sig objecta extends object{}{
sec= unclassified
}

请注意，签名事实包含公式（由 true 或 false 计算的表达式），需要对对象的任何实例都适用。

从这个意义上说，写level = classified 意味着每个usera atom（必然只有一个）的level是分类的。

违反 alloy 中的事实

Violate fact in alloy

alloy