在合金中将一个单独的属性设置为空答案

【问题标题】：Impose a lone attribute to be empty in Alloy在合金中将一个单独的属性设置为空
【发布时间】：2016-11-10 12:27:57
【问题描述】：

我想知道实际上是否有办法强制签名的属性为空。我尝试过这种方式，但它似乎不起作用：

sig C {
 myattribute: lone Type
}

信号类型 { att1：诠释 att2：……等等…… }

fact {
    all c: C| 
        (my condition) 
        <=>
        (
            no c.myattribute
        )
}

至于现在我们可以考虑这样定义一个带有抽象签名的结构：

abstract sig GeneralType {}
one sig Empty extends GeneralType {}
sig NotEmpty extends GeneralType {...arguments (att1,2....}

【问题讨论】：

实际上，您的代码应该可以正常工作。也许“我的状况”发生了一些意想不到的事情？尝试将“我的状况”替换为“1=1”之类的内容进行测试。

标签： alloy

【解决方案1】：

在my condition 的权限下，现有代码应该已经可以工作了。（wmeyer 的建议确实是正确的。）

您可以测试您的约束以确保其行为符合您的预期：

sig Type { }

sig C {
    myattribute: lone Type
}

fact {
    all c: C | no c.myattribute
}

run { } for 5

check {
    all c: C | no c.myattribute
} for 5

【讨论】：