CODEWITHSUNDEEP
alloy
Dirk-Jan Swagerman
Dirk-Jan Swagerman

Reputation: 11

No more satisfying instances

No examples generated for my alloy model with the error message: 'No more satisfying instances' (see image attached)

I have created the following small model in Alloy:

sig System 
{
    subSystem : System
}

// Prevent a subsystem from directly including itself
fact noDirectInclusion
{
    no s : System | s in s.subSystem
}

// Prevent a subsystem from transitivelyincluding itself
fact noTransitiveInclusion
{
    no s : System | s in s.^subSystem
}

pred show {}

run show for 5

The fact 'noDirectInclusion' nicely prevents the generation of examples where a subsystem is a subsystem of itself.

I am probably missing something trivial, but When I also use the fact 'noTransitiveInclusion' there are no longer any examples generated with the error message: 'No more satisfying instances' (see image attached)

What am I missing?

Upvotes: 0

Views: 45

Answers (1)

Peter Kriens
Peter Kriens

Reputation: 15372

What am I missing?

Try to make your graph by hand for only 2 System sigs ...

You will see that with the constraints you specified in the System sig you can only make a cycle ... You force a System to have 1 and exactly 1 subSystem, i.e. the default for a field is one. Therefore, the transitive graph can only be a cycle with a finite set of objects and that invalidates your fact.

Either make subSystem a lone or set.

Upvotes: 0

Related Questions