构造一个 graph

In this workshop we are going to use Alloy to model graphs. Mathematically, recall that a graph is just a pair ⟨V, E⟩ where V is a set of vertices (aka nodes) and E is a set of edges. Each member of E is a pair (v, u) 1 where each of v and u are vertices from V . (v, u) is in E if and only if the graph has an edge from vertex v to vertex u.
We will model this in Alloy using the following signature declaration.
在这里插入图片描述

The first part declares a set Node which will be the set of possible nodes in the graph. The second part
declares a binary relation edges on Nodes. Technically it declares a set Graph of graphs that has only
“one” element (i.e. our model is talking about just a single graph). For any graph g, g.edges is then the
edge relation for that graph. Since the set Graph has only one element in it, to refer to the set of edges in
the graph in our model we can just write Graph.edges.

谓词

Enter the following predicate definition, which specifies when a graph g has exactly two edges.
在这里插入图片描述

谓词的作用简单：给定一个 graph 实例，当这个 graph 满足谓词的定义的时候，谓词就 hold 了，或者说 pred 结果就为 true

We can use the run command to view satisfying instances of this predicate, i.e. to get Alloy to show us
graphs that have exactly two edges. Add the following run command and then choose Execute → Run
has two edges from the menu.

undirected 无向图

Write a predicate is undirected that holds for a graph g when that graph is undirected. Recall an
undirected graph is one such that whenever it contains an edge (v, u) it also contains the symmetric edge (u, v).
Use the run command to view instances of your predicate.

sig Node{}

one sig Graph{
	edges: Node -> Node
}

//
//pred hasTwoEdges{
//	all g: Graph | #g.edges = 2
//}

pred hasTwoEdges[g: Graph]{
	#g.edges = 2
}

pred is_undirected[g: Graph]{
// 错误写法：
// all u, v : Node | (g.edges[u] <=> g.edges[v])
// 因为 g.edges[u] 返回的不是布尔类型
//	all u, v : Node | (v in g.edges[u] <=> u in g.edges[v])
	all u, v : Node | (v in g.edges[u] => u in g.edges[v] and u in g.edges[v] =>v in g.edges[u] )
}

一定注意的是错误的写法：

pred is_undirected[g: Graph]{
// 错误写法：
// all u, v : Node | (g.edges[u] <=> g.edges[v])
// 因为 g.edges[u] 返回的不是布尔类型
}

g.edges[u] 返回的根本就不是 bool 类型，因此与 <=> 这种逻辑符号进行连接是肯定不对的

undirected2 无向图的第二种写法

The following two functions are shorthand respectively that given a graph g and node v, return the set of nodes with edges to v, and those with edges from v respectively.
在这里插入图片描述
Using these functions, write a predicate is undirected2 that holds for a graph g precisely when g is
undirected.


fun edges_to[g: Graph, v: Node]: set Node {
	//given a graph g and node v, return the set of nodes with edges to v,
	g.edges.v
}

fun edges_from[g: Graph, v: Node]: set Node {
	//given a graph g and node v, return the set of nodes with edges from v,
	g.edges[v]
}

pred is_undirected2[g:Graph]{
	all u: Node | edges_to[g, u] = edges_from[g, u]
}

run is_undirected2 for 3 but 5 Node

assert

The following assertion asserts that the two definitions is undirected and is undirected2 are logically equivalent.
在这里插入图片描述

Here we are instructing Alloy to check it for modes of size up to 20 members of each signature, i.e. graphs that have at most 20 nodes. Enter this command and then execute the check by choosing Execute → Check is undirected equiv for 20 from the menu. Alloy should not find any counter-example (i.e. any model in which this assertion is false), and should produce output like the following:

Fact

Alloy fact declarations declare axioms, i.e. assumptions that Alloy will assume are always true. When generating instances of a model or searching for counter-examples to an assertion, Alloy will only consider ones that satisfy the assumptions stated in fact declarations.

在这里插入图片描述

What does this fact say? Modify this fact to instead say that every graph has exactly three (3) edges. Then re-run the has two edges predicate. What happens? Why?

fact 的意思就是，强制只考虑符合 fact 定义的情况，其他不符合的自动被过滤了

fact at_least_one_edge{
	all g:Graph | #g.edges=3
}

pred hasTwoEdges[g: Graph]{
	#g.edges = 2
}
run hasTwoEdges

这里的 run 一定找不到任何符合要求的 instance
因为在 run 的时候假定所有的 instance 都有 3 个 edge，但是 hasTwoEdge 只要刚好有 2 条 edge 的实例，所以没有任何符合条件的实例

扩展

If you have time: What do the following predicates mean? Enter each and use Alloy’s run command to help work out what they are saying logically. Write down your answer as comments in your Alloy file.
在这里插入图片描述

这两个pred定义都试图描述图中的某种关系，但它们的含义是不同的：

what_does_this_mean1[g: Graph]： 这个谓词表示在图 g 中，对于所有的节点 u 和 v，都存在从u到v的边，并且从v到u的边。这个谓词实际上在描述一个无向图，因为无向图的特性就是如果存在一个从u到v的边，那么必须存在一个从v到u的边。
what_does_this_mean2[g: Graph]： 这个谓词表示在图g中，对于所有的节点u和v，要么存在从u到v的边，要么存在从v到u的边，或者两者都存在。 这个谓词的含义更为广泛，它实际上描述的是一个连通图，连通图的特性就是对于所有的节点对，至少存在一条边使得这两个节点是连通的。注意，这并不意味着图是无向的，因为它并未要求如果存在从u到v的边，那么必须存在从v到u的边。
但当我认为 what_does_this_mean1[g: Graph] 与 is_undirected 以及 is_undirected2 是等价的时候，我发现其实并不是：


pred what_does_this_mean1[g: Graph] {
all u, v: Node | (u -> v) in g.edges and (v -> u) in g.edges
}
pred what_does_this_mean2[g: Graph] {
all u, v: Node | (u -> v) in g.edges or (v -> u) in g.edges
}

assert isEqual{
	all g:Graph | what_does_this_mean1[g] <=> is_undirected2[g]
}

//run hasTwoEdges
//check is_undirected_equiv for 20

check isEqual