Writing assertions in alloy

Question

I'm modelling cardinality based feature models in Alloy, that allow to create multiple instances of Features.

So my Alloy-Model has signatures for the Feature-Model itself, the Features and the Instances. The Feature-Model has a set of Features and a set of Instances (the configuration, containing all Instances of all Features). A Feature has a set of Instances and an interval which contains the allowed multiplicities of the Feature (using a lower and an upper bound). Now i'm trying to find Integers in the intervals of the features, that are never satisfied by any configuration.

I've tried many different solutions, but none of them worked for now. For example this assertion:

assert featureInstanceCardinality{
    all f: Feature, d: Int - 0 | some c: FM.config | IsPossibleCardinality[f, d] => (#(f.instances & c) = d)
}

should in my opinion lead to the right solution (For every Feature f and every Integer d, if d is a possible multiplicity of f, there is at least one configuration c, where f has d instances). Unfortunately this returns counterexamples for every possible amount of Instances for every feature.

Can anybody explain why this is happening, or if it is even possible what I'm trying to do? I would really appreciate some help in this case.

This question IMHO remains unanswered as you don't provide enough of your model for us to know what's going on. Please edit your question if you're still looking for help :-) — Loïc Gammaitoni

C. M. Sperberg-McQueen C. M. Sperberg-McQueen · Accepted Answer · 2016-02-29T03:23:13

One obvious problem is that the signature Int includes negative numbers, so your assertion

assert featureInstanceCardinality{
  all f: Feature, d: Int - 0 | 
    some c: FM.config | 
      IsPossibleCardinality[f, d] 
      => (#(f.instances & c) = d)
}

seems to be claiming that the number of atoms in (f.instances & c) could be -2, if IsPossibleCardinality[f,-2] is true. So if IsPossibleCardinality erroneously held for some negative numbers, that would lead to the failure of the assertion.

A fuller answer would be possible only if you gave a complete working example of the problem you are encountering.

Writing assertions in alloy

1 Answers