2

I'm using Alloy using its API as explained in Alloy - Generate .xml instance from .als.

I want to iterate over all solutions.

How to do this?

Community
  • 1
  • 1
Martin Monperrus
  • 1,845
  • 2
  • 19
  • 28

1 Answers1

4

In order to iterate over all the satisfiable solutions, you can simply loop over calls of the next() method on your A4Solution object, until the solution obtained is unsatisfiable (check with the satisfiable() method).

You will have something like :

A4Solution mySolution = TranslateAlloyToKodkod.execute_command(null, model.getAllReachableSigs(), cmd, new A4Options());

while(mySolution.satisfiable()){
    mySolution=mySolution.next();
    //...
}
Loïc Gammaitoni
  • 4,173
  • 16
  • 39