Error evaluating skolem

[awwx]

Alloy 6.1.0, SAT4J openjdk version "11.0.13" 2021-10-19 Ubuntu 21.04

This example might not make much sense as a model since I was just playing around while learning Alloy and then I cut it down to a minimal test case, but since it causes a crash I thought I'd pass it along for you...

var sig Item {}

fact {
  no Item
}

pred add_item_enabled {
  #Item < 3
}

pred item_added [item: Item'] {
  item not in Item
  Item' = Item + item
}

pred some_item_added {
  some item: Item' | item_added [item]
}

fun added_item : Item {
  Item' - Item
}

fact {
  (eventually always add_item_enabled) implies (always eventually some_item_added)
}

Executing "Run Default for 4 but 4 int, 4 seq expect 1"
   Solver=sat4j Steps=1..10 Bitwidth=4 MaxSeq=4 SkolemDepth=1 Symmetry=OFF Mode=batch
   1..2 steps. 159 vars. 15 primary vars. 351 clauses. 61ms.
   Writing the XML file...
Fatal error:
Error evaluating skolem $this/added_item
StackTrace:
class edu.mit.csail.sdg.alloy4.ErrorFatal: Error evaluating skolem $this/added_item
edu.mit.csail.sdg.translator.A4SolutionWriter.<init>(A4SolutionWriter.java:312)
edu.mit.csail.sdg.translator.A4SolutionWriter.writeInstance(A4SolutionWriter.java:330)
edu.mit.csail.sdg.translator.A4Solution.writeXML(A4Solution.java:1979)
edu.mit.csail.sdg.translator.A4Solution.writeXML(A4Solution.java:1962)
edu.mit.csail.sdg.alloy4whole.SimpleReporter.writeXML(SimpleReporter.java:596)
edu.mit.csail.sdg.alloy4whole.SimpleReporter.resultSAT(SimpleReporter.java:431)
edu.mit.csail.sdg.translator.A4Solution.solve(A4Solution.java:1744)
edu.mit.csail.sdg.translator.TranslateAlloyToKodkod.execute_commandFromBook(TranslateAlloyToKodkod.java:610)
edu.mit.csail.sdg.alloy4whole.SimpleReporter$SimpleTask1.run(SimpleReporter.java:742)
edu.mit.csail.sdg.alloy4.WorkerEngine$6.run(WorkerEngine.java:485)
java.base/java.lang.Thread.run(Thread.java:829)
caused by...
class edu.mit.csail.sdg.alloy4.ErrorFatal: An internal error occurred in the evaluator.
edu.mit.csail.sdg.translator.A4SolutionWriter.writeExpr(A4SolutionWriter.java:118)
edu.mit.csail.sdg.translator.A4SolutionWriter.<init>(A4SolutionWriter.java:307)
edu.mit.csail.sdg.translator.A4SolutionWriter.writeInstance(A4SolutionWriter.java:330)
edu.mit.csail.sdg.translator.A4Solution.writeXML(A4Solution.java:1979)
edu.mit.csail.sdg.translator.A4Solution.writeXML(A4Solution.java:1962)
edu.mit.csail.sdg.alloy4whole.SimpleReporter.writeXML(SimpleReporter.java:596)
edu.mit.csail.sdg.alloy4whole.SimpleReporter.resultSAT(SimpleReporter.java:431)
edu.mit.csail.sdg.translator.A4Solution.solve(A4Solution.java:1744)
edu.mit.csail.sdg.translator.TranslateAlloyToKodkod.execute_commandFromBook(TranslateAlloyToKodkod.java:610)
edu.mit.csail.sdg.alloy4whole.SimpleReporter$SimpleTask1.run(SimpleReporter.java:742)
edu.mit.csail.sdg.alloy4.WorkerEngine$6.run(WorkerEngine.java:485)
java.base/java.lang.Thread.run(Thread.java:829)

[grayswandyr]

Thanks for the report, I can reproduce the bug too, even without the unusually-placed prime symbols.

[dkasak]

Incidentally, I just stumbled on this bug while trying almost exactly the same thing as above, namely an "add item" predicate for a top-level var sig. It doesn't seem to behave sensibly, so is this kind of thing even supported?

[grayswandyr]

Incidentally, I just stumbled on this bug while trying almost exactly the same thing as above, namely an "add item" predicate for a top-level var sig. It doesn't seem to behave sensibly, so is this kind of thing even supported?

Not enough information to answer... Here @awwx ' issue is not related to item_added, witness:

var sig Item {}

fact {
  no Item
}

pred add_item_enabled {
  #Item < 3
}

pred some_item_added {
    one Item' - Item
}

fun added_item : Item {
  Item' - Item
}

fact {
  (eventually always add_item_enabled) implies (always eventually some_item_added)
}

[grayswandyr]

Pinging @nmacedo

[alcinocunha]

A simpler example where the problem still occurs:

var sig Item {}

fact {
    no Item and some Item'
}

fun added_item : Item {
  Item'
}

[nmacedo]

Fixed for 6.2.