## Trace errors?

Moderator: Automated Software Engineering

Toobee
Sonntagsinformatiker
Beiträge: 225
Registriert: 7. Apr 2011 12:58

### Trace errors?

Is there any way, except wasting more time and start every time from zero, to find over-specification errors?

Once I specify this line

//every company has some employee
fact f1b2 { all c : Company | some e: Employee | c in e.worksfor }

no model is generated where a company has a subcontractor - I have no clue why and it makes no sense to proceed with the chinese wall task if there are no subcontractors. And I think task 2 will generate even more nonsense without the first one working?

(at least the reason for annoy no being used is straight forward)

tgp
Sonntagsinformatiker
Beiträge: 268
Registriert: 15. Nov 2006 21:41

### Re: Trace errors?

If you do not want to start the solutions from zero, specify something like

Code: Alles auswählen

run {
#Company > 1
#conflictWith > 0
}

Perhaps there are more sensible minimum constraints on the relations and types/sets?

(the constraint on #Company is obviously not needed if the one for conflictWith is there...)

ericbodden
Sonntagsinformatiker
Beiträge: 243
Registriert: 5. Apr 2010 19:06

### Re: Trace errors?

Hi Toobee.

I am afraid I also don't have a better answer. Over-specification is really kind of hard to debug in Alloy.

-- Eric

Toobee
Sonntagsinformatiker
Beiträge: 225
Registriert: 7. Apr 2011 12:58

### Re: Trace errors?

Maybe I understood something wrong.

Code: Alles auswählen

all a, b: Company | a in b.isSubContractorFor implies b.isSubContractorFor.conflictWith & a == none

What does that mean? I intended to express that each a which works for b is not in conflict with the sub contractors of b. I think that might be the line that causes the absence of any subcontractors in the later task? Did I express what I intended or are there any other implications I missed?