haslab / pardinus Goto Github PK

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).

Clean up electrod files after solving not in debug mode.

Compile and package Electrod automatically during Pardinus installation.

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

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

Test whether Electrod failed and handle the solving process accordingly.

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

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

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

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?

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

Integer operations on Electrod are not bounded, unlike Kodkod.

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.

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

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).

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

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).

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.

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)

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.

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

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

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

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

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

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

Electrod no longer uses instance declarations.