Constant expression "UNIV" cannot be directly expanded to "UNIV" during translation since this will always contain the state atoms, so will never be true.

Evaluator requires temporal instances to be converted back into a single static instance in a state idiom. Convert sequence traces (e.g., from Electrod) back to static instance so that they can be evaluated.

Test whether Electrod failed and handle the solving process accordingly.

Electrod no longer uses instance declarations.

hasNext test freezes in decomposed model finding (at least with electrod) once no more solutions.

Allow solution to be iterated by converting instances to a formula, for engines without incremental solving.

Clean up electrod files after solving not in debug mode.

Assume that traces are always infinite through looping, simplify all translations accordingly.

Integer operations on Electrod are not bounded, unlike Kodkod.

When resolving bounds with difference the upper bound cannot be used directly; any other problematic operators?

The bounds of relations over which a total ordering is imposed are not being correctly bound at the configuration stage.

The bounded temporal expansion converts eventually into an existential quantification, which will often be skolemized; alternative solutions will be returned depending on the value of that skolemized value, but in the perspective of the user, these all represent the same temporal instance (since temporal expansion is opaque).

Iteration of trivial configurations introduces new variables that are not being bound in Electrod problems.

Create a proper toggleable debug mode and adapt all output accordingly.

Compile and package Electrod automatically during Pardinus installation.

To allow easier experiments with Pardinus, we could add a human-friendly concrete syntax, thus removing the obligation to use the Java API. I am advocating a syntax akin to that of E. Torlak's PhD thesis and articles. The electrod input syntax (example) roughly follows these lines and could serve as an inspiration. The corresponding grammar should belong to a nice grammar class. ANTLR seems to be the way to go these days.

Seems like a good student project.

In decomposed problems, the no overflows option is not being applying to the partial problem.

Get the solving statistics from the Electrod output (#variables, solving and translation time).

Currently opening util/ordering on a variable sig is buggy (the system will crash due to too many configurations being generated). But what would be the expected meaning anyway?

Pretty-printing should parenthesize every kind of term (expressions, formulas, integer expressions). This is to ensure that Electrod parses the generated models consistently (spoiler: as of now, there are cases where it does not and where the fix will not be trivial; besides these problems, this will also ensure that things such as inconsistent operator precedences will not create "artificial" problems).

upperBounds() should be a shallow embedding, is causing new skolem variables to not be detected when skolemizing.

It would be nice to generate all .elo files corresponding to a given analysis in a directory, the name of which would depend on the name of the original Electrum file. It would also be nice if this name contained the name of the executed command. E.g. command check foo of file bar.ele should produce a directory named bar-check-foo-date-time-NNNN/ (NNNN being a fresh id).

next is protected in electrod and throws a syntax error; which other keywords must be renamed?

In kodkod, when a relation is not referred in the formulas, it is always assigned the lower bound. By creating a formula for the temporal instance, every relation is referred, making iteration inconsistent.

Often Pardinus attempts to parse the XML file before it is available (even though it waits for Electrod to terminate).

Electrod does not support relations with integer fields, test this before launching the problem.

In the latest version of Alloy, attempting to use metafacility via the following code:

sig A {
   x: Int,
   y: Int,
   z: Int
}

pred eq[a1, a2 : A] { all f:A$.fields | a1.(f.value)=a2.(f.value) }

pred show {
   eq[A, A]
}

run show

Cause a stack overflow error in Pardinus:

java.lang.StackOverflowError
	at java.util.HashMap.putVal(HashMap.java:629)
	at java.util.HashMap.put(HashMap.java:612)
	at java.util.HashSet.add(HashSet.java:220)
	at java.util.AbstractCollection.addAll(AbstractCollection.java:344)
	at java.util.HashSet.<init>(HashSet.java:120)
	at kodkod.instance.PardinusBounds$SymbolicStructures.transitiveDeps(PardinusBounds.java:800)
	at kodkod.instance.PardinusBounds$SymbolicStructures.transitiveDeps(PardinusBounds.java:805)
	at kodkod.instance.PardinusBounds$SymbolicStructures.transitiveDeps(PardinusBounds.java:805)
	at kodkod.instance.PardinusBounds$SymbolicStructures.transitiveDeps(PardinusBounds.java:805)
	at kodkod.instance.PardinusBounds$SymbolicStructures.transitiveDeps(PardinusBounds.java:805)