Testing framework: Aluminum vs. Alloy

[tnelson]

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

[tnelson]

Salman introduced AluminumTester for (a), (b); need to see if it addresses (c), (d) as well.

[tnelson]

Does not address (c) and (d). This is an open question re: methods of testing, since order of model enumeration can change across versions and platforms...

[tnelson]

Soundness of consistent-fact set is easy to test (does there exist some Alloy model containing p(min)+F for each F?)

Completeness is harder. Must check all models in cone to make sure none of them contain F. But can still be done, right?