我想正式确定从应用程序访问其他应用程序的数据部分的权限。首先，我创建请求签名（例如APP1想读APP2的DATASECTION）和权限（请求A是MAY_PREVENT） sig request{
from: OS_App,
to: Memory,
act: action
}
sig permission{
req: request,
per: status
}
我在Alloy中编写了下面的代码。我想知道为什么它没有找到一个实例，因为在代码中根本没有任何事实。 abstract sig TaskStatus {}
one sig Completed extends TaskStatus {}
one sig Waiting extends TaskStatus {}
one sig OnGoing extends TaskStatus {}
si
下午好， 我在处理无界通用量词时遇到了Alloy问题。正如丹尼尔杰克逊的“软件抽象”一书（第5.3节“无界通用量词”）中所解释的，Alloy在通用量词和断言检查方面有一个细微的限制。合金产生在某些情况下的寄生反例，例如下一个检查集合下联盟（在前述书示出）封闭： sig Set {
elements: set Element
}
sig Element {}
assert Clos
以下合金代码说，每间客房都有一组键： sig Key {}
sig Room {
keys: set Key
}
的keys关系需要被约束。就目前而言，它允许这样的实例：密钥K1用于一堆房间。哎哟!我们不希望这样。我们希望每个密钥只能与一个房间一起使用。下面是说明有效的情况下，宇宙的图形（和我们实际要允许情况下的子集）： 集，我们其实是想用这种合金代码是很好的表达实例： Roo
请考虑下面的Alloy模型，这是一个剥离的学生提交的本质版本。这个问题是一个排课系统，学生想说没有冲突（在同一时间在同一个地方的两个不同的课程会）： abstract sig Room{}
one sig S20, S30, S50 extends Room{}
abstract sig Period{}
one sig Mon, Tue, Wed, Thu, Fri extends Pe
我正在学习Alloy，我试图指定一个简单的数组列表。我的规范基于Alloy的书籍和在线教程的第一个例子。我只是试图测试它的基本特征，而我想要做的事情非常简单，但不起作用，我不知道为什么，因为它与示例非常相似。这是我的规格： module FileSystem/Lists[A]
open util/ordering[List]
sig List {
content: Int ->on