Hi,

I am using Alloy to try and identify invalid instances of models. As such, I am translating a model into the Alloy format, adding the appropriate assertions, and executing them with Alloy to find problems.

Firstly, I am translating from Java models, which supports multiple inheritance (interfaces). As such I use the Variant pattern (inspired by [1]) to translate multiple inheritance into a single inheritance tree as per Alloy:

// emulate multiple inheritance through variant wrapper
abstract sig Wrapper {
  to : set Wrapper,
  children : set Wrapper,
  eventTriggers : set Wrapper,
  outEdges : set Wrapper,
  attr_name : one AString,

  // inferred
  redirectsTo : set Wrapper,

  /* types */
  types : set Type
}

// types
abstract sig Type { }
one sig Button extends Type { }
one sig Page extends Type { }
one sig NavigateWire extends Type { }
one sig EventTrigger extends Type { }
one sig Other extends Type { } // for other types

pred isButton(w : Wrapper) { Button in w.types }
pred isPage(w : Wrapper) { Page in w.types }
pred isNavigateWire(w : Wrapper) { NavigateWire in w.types }
pred isEventTrigger(w : Wrapper) { EventTrigger in w.types }
pred isOther(w : Wrapper) { Other in w.types } // for other types

I also have to identify strings, so I convert all strings in the universe into single instances of an abstract String type:

// define strings
abstract sig AString { }
one sig StringEmpty extends AString { }
one sig String_Home extends AString { }
one sig String_Navigate_sto_spage_s0 extends AString { }
one sig String_page_s0 extends AString { }
one sig String_Navigate_sto_spage_s1 extends AString { }
one sig String_navigate extends AString { }
one sig String_click extends AString { }
one sig String_page_s1 extends AString { }
one sig String_access extends AString { }
one sig String_run extends AString { }

I have found that for any model instance of any significant size, Alloy fails to generate a CNF in any reasonable time frame. My instance looks like a number of these generated blocks:

one sig model_d124985804ff_d1 extends Wrapper { }
fact {
  model_d124985804ff_d1.eventTriggers = none
  model_d124985804ff_d1.children = visual_d1249858055d_d1 + visual_d1249858055d_d2 + visual_d1249858055d_d4
  model_d124985804ff_d1.to = none
  model_d124985804ff_d1.outEdges = none
  model_d124985804ff_d1.attr_name = StringEmpty

  // types
  model_d124985804ff_d1.types = Other
}

one sig visual_d1249858055d_d1 extends Wrapper { }
fact {
  visual_d1249858055d_d1.eventTriggers = none
  visual_d1249858055d_d1.outEdges = none
  visual_d1249858055d_d1.children = visual_d1249858055d_d3 + visual_d1249858055d_d5
  visual_d1249858055d_d1.to = none
  visual_d1249858055d_d1.attr_name = String_Home

  // types
  visual_d1249858055d_d1.types = Page + Other
}

one sig visual_d1249858055d_d3 extends Wrapper { }
fact {
  visual_d1249858055d_d3.eventTriggers = model_d124985804ff_d2
  visual_d1249858055d_d3.outEdges = none
  visual_d1249858055d_d3.children = none
  visual_d1249858055d_d3.to = none
  visual_d1249858055d_d3.attr_name = String_Navigate_sto_spage_s0

  // types
  visual_d1249858055d_d3.types = Button + Other
}

// ... 11 other instances omitted

I then evaluate the following logic. In particular, I am trying to find infinite loops of (Page -> EventTrigger -> NavigateWire -> Page). Since Alloy cannot handle recursive functions, I define this as a predicate, using iff:

// logic
fact {
  all b : Wrapper, a : Wrapper |
    b in a.redirectsTo <=>
    (b.isPage and a.isPage and
      (
        some e : Wrapper, w : Wrapper |
        e.isEventTrigger and w.isNavigateWire and (
          e.attr_name = String_access and
          e in a.eventTriggers and w in e.outEdges and b = w.to
        )
      )
    )
}

I then check for loops by using transitive closure:

// check
assert myCheck {
  no p : Wrapper | p.isPage and p in p.^redirectsTo
}
check myCheck for 3

For a model of 14 Wrapper instances, most time is spent generating the CNF, and Alloy correctly identifies the two counterexamples that exist:

Executing "Check myCheck for 3"
   Solver=sat4j Bitwidth=4 MaxSeq=3 SkolemDepth=1 Symmetry=20
   64588 vars. 1204 primary vars. 216788 clauses. 5375ms.
   Counterexample found. Assertion is invalid. 250ms.

For a model of 26 Wrapper instances, it takes significantly longer time (suggesting a very exponential situation):

Executing "Check myCheck for 3"
   Solver=sat4j Bitwidth=4 MaxSeq=3 SkolemDepth=1 Symmetry=20
   629733 vars. 3900 primary vars. 2250612 clauses. 122079ms.
   Counterexample found. Assertion is invalid. 2063ms.

For a model of 62 Wrapper instances, generation of the CNF does not complete within 8 hours.

Perhaps there is a major problem in the way I have written my check, or the way I am emulating strings, or emulating multiple inheritance through the Variant pattern? If I reduce the checks to "check myCheck for 1", it still generates the same number of variables and the same result, so I don't think that will help. Since it doesn't get past the generation of CNF, changing the SAT solver doesn't seem to make any difference either.

This is with the Alloy 4.1.10. I also increased the memory available to Java through the command line, but it didn't seem to make any difference:

java -jar alloy4.jar -vmargs -Xms256m -Xmx512m

Any advice or suggestions would be appreciated :) Thanks!

[1]: Crespo, Y., Marques, J. M., Rodriguez, J., "On the Translation of Multiple Inheritance Hierarchies into Single Inheritance Hierarchies", Proceedings of ECOOP, 2002.