Very bad recursion performance when generating CNF

Questions
1

I am still working on the model I described here. I’m basically implementing something where there is a function f : A -> B list, and I want to compute List.flatten (List.map f list_of_as). Hopefully that OCaml pseudocode makes sense. Anyway, the important part is the list/sequence map and flatten.

I’ve found that my implementation of this has really bad performance when generating the CNF.

Here is a scaled down example of the problem:

module Test

sig A {}
sig B {}

sig As {
	s: seq A
}

sig Bs {
	s: seq B
}

// This maps from an A to a sequence of Bs
pred f (input: A, out: Bs) {
	out.s = 0->B
}

// This maps from a sequence of As to a sequence of Bs using f
pred f_seq (input: As, output: Bs) {
	As.s.isEmpty => Bs.s.isEmpty else
	(some convert_first: Bs,
	      others: As,
	      convert_others: Bs |
	 // Convert the first A
       f [As.s.first, convert_first] and
	 // Create a sequence for the other As
	 others.s = As.s.rest and
	 // Recurse on the other As
	 f_seq [others, convert_others] and
	 // Combine the two sequences
	 output.s = convert_first.s.append [convert_others.s])
}

pred test {
	some a: As, b: Bs | f_seq [a, b]
}
run test for 5 but 5 int, 5 seq

Recursion unroll level 0: <1 second
Recursion unroll level 1: 2 seconds
Recursion unroll level 2: 200 seconds
Recursion unroll level 3: Still running :rofl:

I expected this to scale exponentially, but this exceeded my expectations (in a negative way). The other odd thing is that Java is not using that much memory (about ~1GiB). If the problem was that unrolling was really blowing up that much, I would have expected more memory use.

Does this seem like expected behavior? Is this a sign that my problem domain might not be that well suited for Alloy?

Thanks in advance.

2

Alloy is indeed not suited to write recursive programs over lists. If you want to execute and verify the correctness of programs, I’d say Why3 or Dafny are a better match (or the B language, if you want a refinement-based approach).

3

Thanks. I was starting to independently lean towards formulating my model as a program even before this. It’s a shame because the rest of the model seems very well suited for Alloy.

I am familiar with Boogie and Dafny, but will look into Why3 and B. I was also considering writing in C and using a BMC.

4

I was looking some at the code that translates from Alloy to Kodkod and here is the code that handles recursive calls.

I haven’t spent too much time thinking about this, but I wonder if the translation of the recursive function could be cached with a “hole” for the result of the recursive call and the function arguments.

Update: After some debugging, I found that it is Kodkod “translating” slowly. I think it is translating from its AST to a Boolean formula? Anyway, the code I pointed to in Alloy is not the issue.