合金 - 如何为签名设置值

Question

我想将一个应用程序对其他应用程序数据部分的访问形式化。首先，我为请求（例如 APP1 想要读取 APP2 的 DATASECTION）和权限（请求 A 为 MAY_PREVENT）创建签名

sig request{
 from: OS_App,
 to: Memory,
 act: action
}

sig permission{
    req: request,
    per: status
}

我为我的想法写了两个函数，但它不起作用。有人可以帮帮我吗？

//Assign a request 
pred P_026 [asc: request, app1: NonTrusted, app2: OS_App, ds: app2.ownDS]{
    asc.from = app1
    asc.to = ds
    asc.act = read
}

//If the Request is A then status is may_prevent
fun F_026[s: status, requ: request, app1: NonTrusted, app2: OS_App, ds: app2.ownDS]: set may_prevent{
    {s : requ.per | requ in P_026[requ,app1,app2,ds]} 
}

Answer 1

我不知道你是否还在为这个问题而苦苦挣扎！！我不完全理解你的问题，因为我们没有看到所有签名的定义：“NonTrusted”、“action”......

但是我可以看到这里有一个问题：“requ in P_026[requ,app1,app2,ds]”你不能写这个“谓词中的原子”是荒谬的..