Is there a way to find out what is causing 'No Instance Found' on run in Alloy?

Question

I have written in model using Alloy. However for certain conditions running the predicate to find an instance is failing and it says that no instance can be found. I tried increasing the bound to about 16 instances, yet it does not find any instance.

Is there any way I can debug this so that I can see which facts are failing which is causing Alloy not being able to find an instance?

Thanks !

Answer 1

If you change the default sat solver to minisat with unsat core, then it will be possible to highlight the constraints that can't be satisfied in a same instance.

Another possible solution is to comment your constraints one by one until analysis yield an instance hence pinpointing which constraint might cause trouble.

For a more specific answer, please share your model.