首页 文章

合金:这个合金代码有什么问题?

提问于
浏览
-1

如何解决这个合金代码执行的问题?用合金v 4.1测试给我们一个错误:

.error类型这不能是一个合法的关系连接,左边是t(type = {this / Target})右边是this / subject(type = {this / subjects})

sig Element{}
sig policy extends Element{}
sig Target extends Element{}
sig Targets extends Target{}
abstract sig subjects,Request,Action extends Targets{}
sig Rule{}
sig Attribute{}
sig Value{}
sig Effect{}
sig T1,T2,T3 extends Target{}
sig SUB1,SUB2,SUB3 extends subjects{}
sig elementMatch{}
abstract sig Policy{
policyTarget : one Target ,
rules : set Rule ,
}
abstract sig Elements{
attributes : Attribute -> Value}
{attributes in values}

pred targetMatch[t:Target,r:Request]
{
some s:t.subjects | elementMatch[s, r.subject]
some s:t. resources| elementMatch[s,r.resource]
some s:t. actions| elementMatch[s,r.action]
}
fun ruleResponse [r:Rule,req:Request]
:Effect{
if targetMatch[r.ruleTarget,req]
then r.ruleEffect
}
assert permitforprofessor{
all q : Request{
{~(q.subject.attributes).Attribute=professor}
=> policyResponse[p,q] = permit}
}
run targetMatch

1 回答

  • 3

    我没有那么深入到你的代码的细节,但我可以看到许多缺陷 .

    您收到的错误是由于您在targetMatch谓词中编写的 t.subject .

    一切都写在错误消息中 . 这不是合法的关系加入 .

    在其他错误中,elementMatch [s,r.subject]在知道elementMatch被声明为签名时也看起来非常可疑 .

    我建议你通过在线Alloy课程来更熟悉这门语言:

    http://alloy.mit.edu/alloy/tutorials/online/frame-FS-1.html

相关问题