合金 - 如何设置签名的值

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 [热曲，APP1，APP2，DS]”你可以不写这个‘原子在谓语’是absurde ..