Integers in Kodkod ( IntConstant.constant (...) )

[chrissoalloyuser]

Hello,

i do not really understand the way, in which Kodkod works with Integers
and Integer Constants.
In the following example i dont know, why the first Formula in
"declarations()" evaluates too true...


public final class IntegerTest {
     private final Relation Human, rAge, rAllAges;

     public IntegerTest() {
         Human = Relation.unary("Human");
         rAge = Relation.binary("rAge");

         //Just for test purposes
         rAllAges = Relation.unary("rAllAges");
     }

     public Formula declarations() {
         //sum() of the two integers should be 3, but its 0 ???
         Formula f1 = Human.join(rAge).sum().eq(IntConstant.constant(0));
         //Just for test purposes
         Formula f2 = Human.join(rAge).in(rAllAges);
         return f1.and(f2);
     }


     public Bounds bounds(int human, int integers) {
         final List<Object> atoms = new LinkedList<Object>();
         for (int i = 0; i < human; i++) {
             atoms.add("Human" + i);
         }
         for (int i = 0; i < integers; i++) {
             atoms.add(IntConstant.constant(i));
         }
         final Universe universe = new Universe(atoms);
         final TupleFactory factory = universe.factory();
         final Bounds bounds = new Bounds(universe);

         bounds.boundExactly(Human, factory.setOf("Human0", "Human1"));
         bounds.boundExactly(rAge, factory.setOf(factory.tuple("Human0",
IntConstant.constant(2)),
                                             factory.tuple("Human1",
IntConstant.constant(1))));

         bounds.bound(rAllAges, factory.allOf(1));

         return bounds;
     }

     public static void main(String[] args) {

         final IntegerTest model = new IntegerTest();
         final Solver solver = new Solver();
         solver.options().setSolver(SATFactory.DefaultSAT4J);

         final Solution sol = solver.solve(model.declarations(),
model.bounds(3, 3));

         System.out.println(sol);
     }

}

Can anyone give me a hint ?

Thanks
     Christian

[Felix Chang-2]

Dear user:

I'm afraid you did not understand how primitive integers
and Int atoms work in Kodkod and Alloy.

Here I have repaired your code, and added comments where appropriate:

public final class Test {

   private final Relation Human, rAge, rAllAges;

   public Test() {
      Human = Relation.unary("Human");
      rAge = Relation.binary("rAge");
      rAllAges = Relation.unary("rAllAges");
   }

   public Formula declarations() {
      Formula f1 = Human.join(rAge).sum().eq(IntConstant.constant(3));
      Formula f2 = Human.join(rAge).in(rAllAges);
      return f1.and(f2);
   }

   public Bounds bounds(int human, int integers) {
      final List<Object> atoms = new LinkedList<Object>();
      for (int i = 0; i < human; i++) { atoms.add("Human" + i); }
      for (int i = 0; i < integers; i++) {
          // Here, you need to give it actual Objects that
          // you want to represent for each integer...
          // Not "IntConstant" which is usually used to represent AST nodes.
          // Granted, you could use AST nodes as atoms, which is why
          // the typechecker did not complain, but it can get very confusing
          atoms.add("" + i);
      }
      final Universe universe = new Universe(atoms);
      final TupleFactory factory = universe.factory();
      final Bounds bounds = new Bounds(universe);
      // You need to add the following loop, to bind each primitive integer
      // in your model to an appropriate Int atom
      for (int i = 0; i < integers; i++) {
          bounds.boundExactly(i, factory.setOf("" + i));
      }
      bounds.boundExactly(Human, factory.setOf("Human0", "Human1"));
      bounds.boundExactly(rAge,
          factory.setOf(factory.tuple("Human0", "2"), // Use "2", not IntConstant
                        factory.tuple("Human1", "1")  // Use "1", not IntConstant
          ));
      bounds.bound(rAllAges, factory.allOf(1));
      return bounds;
   }

   public static void main(String[] args) {
     final Test model = new Test();
     final Solver solver = new Solver();
     solver.options().setSolver(SATFactory.DefaultSAT4J);
     final Solution sol = solver.solve(model.declarations(), model.bounds(3,3));
     System.out.println(sol);
   }
}

--

The program now executes as expected: the formula is satisfiable
when you want the sum to be IntConstant(3), and unsatisfiable
when you want the sum to be IntConstant(0).

Please compare your previous code to this code, consult the Kodkod API java doc,
and post back if you have further questions. (In particular, notice that
for bounds, I use "0", "1", and "2" since we're talking about exact atoms,
but for the declaration formula I use IntConstant.constant(3) since we are
talking about a relation which shall evaluate to be 3 at that point).

Sincerely,
Felix Chang
Alloy4 Developer

[Felix Chang-2]

On Tue, 8 Apr 2008, Felix Chang wrote:
> (In particular, notice that
> for bounds, I use "0", "1", and "2" since we're talking about exact atoms,
> but for the declaration formula I use IntConstant.constant(3) since we are
> talking about a relation which shall evaluate to be 3 at that point).

Sorry, I meant to say IntConstant.constant(3) is a primitive integer expression
that evaluates to 3.

The thing to remember is that in Kodkod you have 3 type of expressions:
Expression which is a set or relation
IntExpression which is a primitive integer
Formula which is a primitive boolean

Everything in your model except that eq() line, you are talking about
sets and relations. But when you invoke the sum() method, you are
asking Kodkod to convert each Int atom in the left hand side into
its corresponding primitive integer number, and then perform
a 2's complement addition of all primitive numbers.

And that's why it's the only place in your model where you should
write IntConstant.constant(3) rather than "3".
Everywhere else, as your model currently stands,
you need to use "0", "1", "2"...
(or whatever Object you choose to use for Int atoms)

Sincerely,
Felix Chang
Alloy4 Developer

[chrissoalloyuser]

Dear Felix,

many thanks for your reply. I didn't understand how kodkod maps
arbitrary atoms to an primitive integer. Yeah, i have to bound them,
that's the point.

Regards
Christian

--- In alloy-discuss@..., Felix Chang <fschang@...> wrote:
>
> On Tue, 8 Apr 2008, Felix Chang wrote:
> > (In particular, notice that
> > for bounds, I use "0", "1", and "2" since we're talking about
exact atoms,
> > but for the declaration formula I use IntConstant.constant(3)
since we are
> > talking about a relation which shall evaluate to be 3 at that point).
>
> Sorry, I meant to say IntConstant.constant(3) is a primitive integer
expression

> that evaluates to 3.
>
> The thing to remember is that in Kodkod you have 3 type of expressions:
> Expression which is a set or relation
> IntExpression which is a primitive integer
> Formula which is a primitive boolean
>
> Everything in your model except that eq() line, you are talking about
> sets and relations. But when you invoke the sum() method, you are
> asking Kodkod to convert each Int atom in the left hand side into
> its corresponding primitive integer number, and then perform
> a 2's complement addition of all primitive numbers.
>
> And that's why it's the only place in your model where you should
> write IntConstant.constant(3) rather than "3".
> Everywhere else, as your model currently stands,
> you need to use "0", "1", "2"...
> (or whatever Object you choose to use for Int atoms)
>
> Sincerely,
> Felix Chang
> Alloy4 Developer
>