The formulation of Turan's theorem states that a
`k+1`

-free graph with `n`

nodes can maximally
have `(k-1)n`

edges. A graph
is ^{2}/(2k)`k+1`

-free if it contains no clique
with `k+1`

nodes (a clique is a subset of nodes in which
every two nodes are connected by an edge); this is equivalent to
saying that its maximum clique has exactly `k`

nodes. A
formalization of Turan's theorem in Alloy is given in the figure on
the right.

The formalization of the `maxClique`

property is
**higher-order**, because it quantifies over all possible
sets of `Node`

s to assert that there does not exist another
set of nodes which is a `clique`

and has more nodes than
the max-clique. Higher-order specifications are expressible in Alloy,
but the official Alloy Analyzer is not powerful enough to analyze
them. In **Alloy***, in contrast, this check can be
automatically performed to confirm that no counterexample can be found
within the specified scope.

There are two ways to now formalize Turan's theorem
(the `Turan_dom_constr`

and `Turan_classical`

commands). In both cases, the idea is to asserts that for all
possible `edge`

relations (from `Node`

to `Node`

) that are symmetric and irreflexive, if the
max-clique in that graph has `k`

nodes
(`k=#mClq`

), the number of selected edges
(`e=(#edges).div[2]`

) must be at
most `(k-1)n`

(the number of tuples in
^{2}/(2k)`edges`

is divided by `2`

because the graph in
setup of the theorem in undirected). The differences, although
syntactic, have significant impact on performance:

- classical
- the classical way to constrain the domain of
a universal quantifier (e.g.,
*all edges that are symmetric and irreflexive*) is to use an implication in the quantifier body; similarly, to constraint the domain of an existential quantifier (e.g.,*some set of nodes that is max-clique*), a conjunction in the body is used. - with domain

constraints - for an efficient CEGIS
implementation, we prefer domain constraints to be given explicitly
(as opposed to merged and inlined in the quantifier body) using the
newly introduced

clause (not available in standard Alloy).**when**

_{command}\^{scope} | 5 | 6 | 7 | 8 | 9 | 10 |

`Turan_classical` | 4s | 10s | 43s | to | to | to |

`Turan_dom_constr` | 0.3s | 3s | 6s | 10s | 44s | 170s |

comparison of analysis times for various scopes |

some sig Node {} // between every two nodes there is an edge pred clique[edges: Node -> Node, clq: set Node] { all disj n1, n2: clq | n1 -> n2 in edges } // no other clique with more nodes pred maxClique[edges: Node -> Node, clq: set Node] { clique[edges, clq] no cq2: set Node | cq2!=clq && clique[edges,cq2] && #cq2>#clq } // symmetric and irreflexive pred edgeProps[edges: Node -> Node] { (~edges in edges) and (no edges & iden) } // max number of edges in a (k+1)-free graph with n // nodes is (k-1)n^2/(2k) check Turan_dom_constr { all edges: Node -> Node when edgeProps[edges] | some mClq: set Node when maxClique[edges, mClq] | let n = #Node, k = #mClq, e = (#edges).div[2] | e <= k.minus[1].mul[n].mul[n].div[2].div[k] }for 7 but 0..294 Int -- checks in ~6s // same as above, but with inlined domain constraints check Turan_classical { all edges: Node -> Node | edgeProps[edges] implies { some mClq: set Node { maxClique[edges, mClq] let n = #Node, k = #mClq, e = (#edges).div[2] | e <= k.minus[1].mul[n].mul[n].div[2].div[k] } } } for 7 but 0..294 Int -- checks in ~43s