CODEWITHSUNDEEP
alloy
wxlfrank
wxlfrank

Reputation: 39

Keywords: some and one before higher-order quantification

I have an Alloy specification representing a model transformation rules.. In the specification, I use higher-order quantification to specify rule matching. One strange thing is the analyzer works differently with "some" and "one", which I cannot understand.

For example, in the pred rule_enter[trans:Trans](see line 240), I use two higher-order quantification to encoding matching of the left and right side of a graph transformation rule. *********************EXAMPLE**************************************

some e_check0:Acheck&trans.darrows, e_TP0:ATP&(trans.source.arrows-trans.darrows), e_PF10:APF1&trans.darrows, e_TR0:ATR&(trans.source.arrows-trans.darrows), e_F1R0:AF1R&trans.darrows |
let n_P0 = e_check0.src, n_T0 = e_TP0.src, n_R0 = e_TR0.trg, n_F10 = e_PF10.trg |
(n_P0 = e_check0.trg and n_P0 = e_TP0.trg and n_P0 = e_PF10.src and n_T0 = e_TR0.src and n_F10 = e_F1R0.src and n_R0 = e_F1R0.trg  and
n_F10 in NF1&trans.dnodes and
n_P0 in NP&(trans.source.nodes-trans.dnodes) and n_T0 in NT&(trans.source.nodes-trans.dnodes) and n_R0 in NR&(trans.source.nodes-trans.dnodes))

some e_crit0:Acrit&trans.aarrows, e_TP0:ATP&(trans.source.arrows-trans.darrows), e_PF20:APF2&trans.aarrows, e_TR0:ATR&(trans.source.arrows-trans.darrows), e_F2R0:AF2R&trans.aarrows |
let n_P0 = e_crit0.src, n_T0 = e_TP0.src, n_R0 = e_TR0.trg, n_F20 = e_PF20.trg |
(n_P0 = e_crit0.trg and n_P0 = e_TP0.trg and n_P0 = e_PF20.src and n_T0 = e_TR0.src and n_F20 = e_F2R0.src and n_R0 = e_F2R0.trg  and
n_F20 in NF2&trans.anodes and
n_P0 in NP&(trans.source.nodes-trans.dnodes) and n_T0 in NT&(trans.source.nodes-trans.dnodes) and n_R0 in NR&(trans.source.nodes-trans.dnodes))

Here I use the keyword "some". The Analyzer can work with a scope 10.

But if I use the keyword "one", the analyzer reports the following error with a scope 5: *********************EXAMPLE**************************************

Executing "Check check$1 for 5 but exactly 1 Trans, exactly 2 Graph, exactly 1 Rule"
  Solver=minisat(jni) Bitwidth=0 MaxSeq=0 SkolemDepth=1 Symmetry=20
  Generating CNF...
.
Translation capacity exceeded.
In this scope, universe contains 89 atoms
and relations of arity 5 cannot be represented.
Visit http://alloy.mit.edu/ for advice on refactoring.

MY QUESTION is why the two quantification have different performances?

Upvotes: 1

Views: 139

Answers (3)

Aleksandar Milicevic
Aleksandar Milicevic

Reputation: 3867

one in alloy is encoded using set comprehension and the cardinality operator, e.g., 

one s: S | p[s]

is transformed to

#{s: S | p[s]} = 1

Set comprehension cannot be skolemized, so when the quantifier in question is higher-order, Alloy simply gives up.

Upvotes: 2

Nuno Macedo
Nuno Macedo

Reputation: 124

Higher-order quantifications are in general not allowed in Alloy. However, some existential quantifications (i.e., some) can be converted into solvable procedures through a process known as skolemization, which I believe does not apply to uniqueness quantifications (i.e., one). The process is briefly explained here for a (first-order) Alloy example.

I wasn't able to process your example (sorry), but I would guess that is one such case.

Upvotes: 1

danielp
danielp

Reputation: 1187

I do not have a concrete answer for your example but generally it is more complex to encode one than some: Let's assume you have a set S that can maximally contain the elements a, b, c.

Alloy translates the problem to a SAT problem. You can encode S in a SAT problem with 3 Boolean variables xa, xb, xc where xa=TRUE (resp. FALSE) means that a is in S (resp. not in S).

The statement some S can now easily encoded as the formula

xa \/ xb \/ xc

(with \/ as logical or).

On the other hand, for one you need to encode additionally that if one of the variables xa, xb, xc is true, the others are false. E.g.

xa \/ xb \/ xc
xa => not( xb \/ xc )
xb => not( xa \/ xc )
xc => not( xa \/ xb )

In conjuctive normal form (CNF, that's what the SAT solver takes as input) you have the clauses:

xa \/ xb \/ xc
-xa \/ -xb
-xa \/ -xc
-xb \/ -xa
-xb \/ -xc
-xc \/ -xa
-xc \/ -xb

Maybe there are techniques to optimize that but you can see that one needs more clauses to be encoded than some.

Upvotes: 0

Related Questions