Function chaining seems broken

[EugeneWagner]

The "add" function in the following simple model doesn't work consistently if it's chained (see assertion "addWorksFluently") but works fine without chaining (see assertion "addWorks")

sig IntSet{
   values: set Int
}

fun IntSet.add(value: Int): IntSet {
   { result: one IntSet | result.values = this.values + value }
}

fun emptySet: IntSet {
   { result: IntSet | no result.values }
}

assert emptySetWorks{
   all myIntSet: IntSet |
      myIntSet = emptySet implies no myIntSet.values and myIntSet.values = none
}
check emptySetWorks

assert addWorks {
   all disj s1, s2: IntSet |
      s1 = emptySet.add[0] and
      s2 = s1.add[1]
      implies
      s1.values = 0 and
      s2.values = 0 + 1
}
check addWorks

assert addWorksFluently {
   all disj s: IntSet |
      s = emptySet.add[0].add[1]
      implies
      s.values = 0 + 1
}
check addWorksFluently

[pkriens]

I think this is one of the nasty dark corners of Alloy that we need to make more clear.

Functions in Alloy are partial, even if you specify total (i.e. fun foo : one Foo {}). So a function like emptySet can return an IntSet.values = {} or none! The same is unfortunately true for your add function.

An instance of a model can have any number of IntSet atoms, including 0 or max scope. However, each instance contains all IntSet atoms that are allowed by the facts. You do not constrain the solution anywhere so some Instances will have no {}, {0}, or {0,1}. An instance that lacks the proper IntSet will return none for add or emptySet …

So in addWorks works because you test the intermediate result. If either {}, {0}, {0,1} are not in the instance you will detect it by the equality check for s1 and s2. If one of them fails, the overall condition is true. So it works but likely for different reasons than you thought.

However, in the fluently check you chain the calculations. So if any ‘returns’ none then the results is different than you think. For example, an instance like

┌───────────┬──────┐ │this/IntSet│values│ ├───────────┼──────┤ │IntSet⁰ │1 │ └───────────┴──────┘

s       = emptySet.add[0].add[1]
IntSet⁰     = emptySet.add[0].add[1]
IntSet⁰     = {}.add[0].add[1]
IntSet⁰     = {}.{}.add[1]

So looking at {}.add[1]

none.add[ 1 ] : IntSet { { result: one IntSet | result.values = {}.values + 1 } }
none.add[ 1 ] : IntSet { { result: one IntSet | result.values = {} + 1 } }
none.add[ 1 ] : IntSet { { result: one IntSet | result.values = 1 } }
none.add[ 1 ] : IntSet { IntSet⁰ }}
IntSet⁰

So the condition is true, which means we need to look at the consequence. IntSet⁰.values = {1}, and it must be {0+1} … BOOM!

I find these problem the most nasty problems in Alloy and they’ve cost me many hours. It is one of the primary reasons I hardly use functions, only predicates and macros. With functions, you can always get none back and that quite often destroys the intuition what you specify.

I answered it here because I think it is an important topic (there is a Github issue on this.) However, these question belong on StackOverflow.

Kind regards,

Peter Kriens

Let’s assume Alloy tests a solution that has no empty IntSet. In that case your emptySet return a none. In Alloy all functions are partial, even if you specify they are total, so emptySet returns none instead of an empty IntSet. However, adding a fact that requires the emptySet would not suffice because also the add function can be partial if the required set is not of the solution.

So any solution that does not contain {}, {0}, and {0,2} will fail as a counterexample.

On 12 Apr 2018, at 12:33, EugeneWagner notifications@github.com wrote:

The "add" function in the following simple model doesn't work consistently if it's chained (see assertion "addWorksFluently") but works fine without chaining (see assertion "addWorks")

sig IntSet{ values: set Int }

fun IntSet.add(value: Int): IntSet { { result: one IntSet | result.values = this.values + value } }

fun emptySet: IntSet { { result: IntSet | no result.values } }

assert emptySetWorks{ all myIntSet: IntSet | myIntSet = emptySet implies no myIntSet.values and myIntSet.values = none } check emptySetWorks

assert addWorks { all disj s1, s2: IntSet | s1 = emptySet.add[0] and s2 = s1.add[1] implies s1.values = 0 and s2.values = 0 + 1 } check addWorks

assert addWorksFluently { all disj s: IntSet | s = emptySet.add[0].add[1] implies s.values = 0 + 1 } check addWorksFluently

— You are receiving this because you are subscribed to this thread. Reply to this email directly, view it on GitHub https://github.com/AlloyTools/org.alloytools.alloy/issues/47, or mute the thread https://github.com/notifications/unsubscribe-auth/AAMPLs434YbSAWUq7D-HRYHxNlZ9dha7ks5tny15gaJpZM4TRifB.

[aleksandarmilicevic]

I wanted to clarify one point: this behavior has absolutely nothing to do with functions in Alloy.

To prove it, you can rewrite your addWorksFluently to not use functions at all (by manually inlining them, which is what Alloy does behind the scenes anyway), and you'll get exactly the same behavior:

check addWorksFluently {
  all s: IntSet |
    s = {result2: IntSet | result2.values = {result1: IntSet | result1.values = { result0: one IntSet | no result0.values }.values + 0}.values + 1}
    implies
    s.values = 0 + 1
}

This has everything to do with set comprehension. Set comprehension, by definition, evaluates to a set of atoms/tuples that satisfy a given predicate. The add function uses set comprehension to compute all IntSet atoms whose values field contains all values in this plus a given integer: if there is no such IntSet atom in the universe, the result will be an empty set. There is no Alloy black magic going on there. So far, this is just the most fundamental, unaltered predicate logic.

What can be confusing is the meaning of all s: IntSet | .... It's very intuitive to think that this must mean "for all integer sets" just because the name says so. But in fact, IntSet is defined as a sig, so it is treated just like any other set. Since your check command doesn't specify a scope, the default scope of 3 is used, meaning that Alloy will consider all possible IntSet sets of up to only 3 elements. Since there are no additional facts specified in the model, there are no restrictions for the values field, so Alloy can consider an instance consisting of, say, 2 IntSet atoms, both having their values field set to {2, 4}. Against that instance, emptySet evaluates to none, emptySet.add[0] also evaluates to none, and emptySet.add[2] evaluates to none too.

To check that chaining function calls indeed works, you could add a fact like this to your model:

fact { 
  some s0, s1, s2: IntSet | no s0.values && s1.values = 0 && s2.values = 1
}

which would make your addWorksFluently true.

More generally, you could add a fact to ensure that there exists an IntSet atom corresponding to every possible int set, and then check a more general version of addWorksFluently:

fact ensureIntSetAtoms {
  all setOfInts: set Int | some is: IntSet | is.values = setOfInts
}

check addWorksFluently {
  all s: IntSet |
    all i, j: Int |
      s = emptySet.add[i].add[j]
      iff
      s.values = i + j
} for 0 but 2 Int, exactly 16 IntSet

This model, however, is higher-order, so you'd have to use Alloy* to check that this assertion is indeed true.

Yes, this is an important topic and a common pitfall, but it is not an issue in the sense that Alloy can be changed in any way that would help accommodate it.

[aleksandarmilicevic]

We could, however, create a section in our Wiki and move this example there.