salmans / aluminum Goto Github PK

Package names should be more idiomatic. E.g.

edu.wpi.alas.minsolver
etc.

(There is a question here about edu.wpi vs. edu.brown vs. edu.wpiandbrown; no I don't really support that last one, but we should discuss with the group.)

MinSolver.next()'s builds a mapping from prop. variables to relations via the call:

mapVarToRelation = MinTwoWayTranslator.buildVarToRelationMap(translation, bounds);

However, the "bounds" in this case is the pre-Skolem bounds object. We use MyReporter to capture the post-Skolemization bounds. So the line could be replaced with:

mapVarToRelation = MinTwoWayTranslator.buildVarToRelationMap(translation, ((MyReporter)options.reporter()).skolemBounds);

I am not sure what the impact of this bug is yet, but it is an easy fix. Given our recent issues with skolem vars, it is worthwhile to keep watch for similar bugs.

Is saying no augments are possible. This is likely because the iterators are currently designed to just stop yielding results after an unsat. For instance, look at how nonTrivialSolution() catches a ContradictionException when adding cone-restriction clauses...

This could lead to unreliable results if someone tries to augment a final model.

It should read that there are no more minimal solutions. (Found by Dan)

The Alloy translation can map two isomorphic models to the same Alloy model. This happens surprisingly frequently. It is not a bug in Kodkod but rather a feature of Alloy's translation process, where an atom (say) "Object$2" can be renamed "Conference$1".

Our theorems guarantee that we don't repeat Kodkod models.

We should insert a Set and make sure we don't repeat ALLOY models.

Let's label the Aluminum UI in some way that indicates it is different from the last one. Since we are rapidly sending out fresh builds, there could be confusion between different downloads in the same day.

Either a build-time indicator, or a minor version number. (Note we say "based on Alloy Analyzer 4.1.10" but not which version of Aluminum it is!)

Alloy renames atoms for "clarity". E.g. "Addr$0" may be renamed to "Addr0". Or "Addr1". Or "Addr3". This is more reasonable if we realize that atoms names may not contain the most-specific types an atom belongs to in a given model. For instance "Person$1" may be a Student, causing Alloy to rename it "Student0".

The problem is that our augmentation labels are given with Kodkod's names, not Alloy's names. Users see Alloy's names, and are expected to somehow know the Kodkod name underneath. That's silly. We should translate to/from Alloy's names when:
(a) displaying possible augmentations
(b) accepting an augmentation.

Risk for debugging: This will make it harder for us to debug, since the Kodkod atom names will be hidden by the interface. But surely a reasonable logging scheme can replace the loss?

Why do Aluminum and Alloy share an Open Recent fileset? Is anything else shared between them?

It looks like the only two methods (re: translation between FOL and prop) have been moved into MinSolver. Eclipse confirms that they are not called anywhere.

Can the module be removed entirely?

some-loop.als

2nd solution (the self-loop, not the non-loop edges)

Add e(2,2). Now ask for consistent facts. The set is EMPTY. Should not be empty.

In another run, add e(0, 1) instead. The set isn't empty. There is no reason for e(2,2) to close off all other possibilities. Perhaps there is a clause not being removed from the solver?

1st solution and 3rd solution work fine.

(1) The MailBug class currently handles uncaught exceptions, prompting the user to submit a bug report. Obviously we need to make certain that Aluminum sends bug reports to the appropriate place... and we need to do so without sending any bug reports accidentally!

(2) We need to make sure the correct contact info is shown in the help menus.

Tree view produces a blank screen. Confirmed on Akhawe et al.'s authn spec.

... or else it is "invisible" until you alt-tab. Leads to an impression of freezing.

Even if Kodkod's SBP rules them out?

We can see this occuring in Aluminum in my one-edge spec:

sig Node { e: set Node }
pred atLeastOneEdge {
some e
}
run atLeastOneEdge for exactly 3 Node

We want to test:

(a) Soundness of minimal models ("If we present a model, it is minimal for the spec.")
(b) Completeness of minimal models ("If a model is minimal for the spec, we provide it up to isomorphism.")

(c) Soundness of augmentation ("If we produce a model M' as an augment of M by F on A, M' is a minimal model in that category.")
(d) Completeness of augmentation ("If A is satisfiable by a model containing M+F, we produce a minimal such.")

On small specs, we can test these vs. the model-sets generated by Alloy. (There is a nice justification of this strategy: the small-model hypothesis!)

Example spec:

abstract sig Color{}
abstract sig Element { color: set Color }
one sig e1, e2 extends Element{}
one sig red, blue extends Color{}

fact fact1 {
  some e: Element | blue in e.color
}

run{}

If I run this spec in Alloy, I get a model with a node: "e1 ($e)" (or "e2 ($e)").
If I run the spec in Aluminum, I only get "e1" (or "e2").

I just confirmed that the Skolem relation $e is populated in the instance passed back by MinSolver.next(). So it is not a bug in minimization. It's important that Aluminum show Skolem annotations the same as Alloy, especially given our recent intuitive trouble with Skolem relations.

Is it because there are just so many CFs to check? Or something else?

If it is because there are too many CFs, for LATER: incremental construction of CFs. Start with:
(a) Which relations can have a fact added consistently?
(b) Which elements can be involved in a consistent addition?
and move on from there.

Either way, need to discuss the weakness of "eager" CF generation in the paper.

Since "bounds" is pre-Skolem, the result given will be -1 and the skolem variables will be omitted from allLifters. Current code:

            int index = MinTwoWayTranslator.getPropVariableForTuple(bounds, ((MinSolutionIterator)prevIterator).getTranslation(), r, t);

One possible fix:

            Bounds skBounds = ((MyReporter)options.reporter()).skolemBounds;
            int index = MinTwoWayTranslator.getPropVariableForTuple(skBounds, ((MinSolutionIterator)prevIterator).getTranslation(), r, t);

this eliminates at least one bizarre non-minimal-model result in the colors example. :-)

From an engineering perspective, this means that we probably need to make sure that only the post-Skolem bounds are available at all --- or that the pre-skolem bounds are named something appropriate (not "bounds").

Trivially satisfiable means that the formula (not the bounds!) was simplified to a constant true during translation. Aluminum doesn't allow exploration (or enumeration of augments) in such a case. E.g.:

abstract sig Color{}
abstract sig Element { color: set Color }
one sig e1, e2 extends Element{}
one sig red, blue extends Color{}
run{}

Will produce a minimal model with 4 elements, but no edges (as expected). However:

(a) Clicking Next causes an exception:
"Enumerating...
java.lang.IllegalArgumentException: Reference to the constraint to remove needed!"

(b) Clicking for consistent facts produces:
"Finding consistent facts...
No consistent facts found!"

(which is untrue!)

MinSolver.solve() catches the trivial exception around line 755.