Impose a lone attribute to be empty in Alloy

Question

I was wondering if there's a way, in a fact, to force an attribute of a signature be empty. I tried this way but it seems not work:

sig C {
 myattribute: lone Type
}

sig Type { att1: Int att2: ..... etc.. }

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

As for now we can just think about defing a structure with an abstract signature this way:

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

Actually, your code should work as it is. Maybe there is something unexpected going on with "my condition"? Try tor replace "my condition" with something like "1=1" for testing. — wmeyer

ivcha ivcha · Accepted Answer · 2016-11-13T23:40:29

The existing code should already work given the right my condition. (wmeyer is indeed correct in suggesting that.)

You can test your constraint to make sure it is behaving as you would expect:

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

Impose a lone attribute to be empty in Alloy

1 Answers