![](https://csdnimg.cn/release/download_crawler_static/88749734/bg4.jpg)
X. Li
等人
/
理论计算机科学电子笔记
164
(
2006
)
3
E是一个对称关系,可以用转置运算符' ~ '表示
fact UndirectedGraph {
E = ~E
}
//
E
是
对称的
fact
NonEmpty
{ some
V
}
//
考虑非空图
事实
引入了模型的任何
实例都
必须满足的约束,即,集合和关系的任何令人满
意的赋值。事实
NonEmpty
要求实例至少有一个顶点
2
。如果表达式
e
计算为非空集,
则公式
some e
计算为true。(类似地,当
e
求值为空集时
,没有e
求值为true
我们使用
谓词来
表达语句1,即,一个可以在其他地方
调用
的参数化公式:
pred Statement1(){ Connected()
&&
无环()}
pred Connected(){
all disj
v1,v2:
V
| v2
中的
v1
。E } predAcyclic(){
all
v:
V
|(
v,E){
predInCycle(v:
V,
c:
V
->
V)
{
v
in v. c
||
some
v':v.c.
|
设
c
' = c -(v -> v')-(v' -> v)
|
v
' in v.
* c '
}
所有的
o
y
p
r o
vides
通常的逻辑
运算
符:
&&
' ' ( 和) ,
'
||
’
(
or
)
,
not
,
‘
=>
’
(implication),
and‘
<=>
’(bi-implication). 关键字
disj
要求
v1
和
v2
是不同的(更
准确地说,是不相
交的单例集);
all
和
some
分别表示泛量化和存在量化;
in
表示子集(每个表达式在语
义上都是一个集合[5],因此
in
不表示集合成员);
'^ '表示传递闭包,'* '表示自反
传递闭包。v2表达式
。因此,E
表示
沿着E中的边进行一次或多次遍历
之后从v2可到达的
所有顶点的集合
,并且
Connected
表示任何两个不同的顶点之间存在路径。 谓词
InCycle
表示顶点
v
是一个循环的一部分,根据边关系
c
i,在v处有一个自循环,或者
v
有一些邻居
v
',使得即使我们删除连接v和v'的边,这两个顶点仍然是连接的。运
算符
' -> '和' - '分别表示配对(更一般地,笛卡尔积)和集合差异。
我们的问题集要求学生扩展上述Alloy模型,以表示语句2-5中的每一个。
3
学生
们还必须用Alloy表达五个语句的等价性,并使用Alloy Analyzer进行检查。 接下来
我们介绍 学生与分析仪之间的交互,以解决上述问题。 我们选择这个特定的交
互作为用户在使用Alloy Analyzer时通常执行的步骤的代表,通过修改Alloy模型并执
行它的循环。
用户首先检查提供的模型是否一致:
test {!Statement 1()}检查
测试3
Alloy
断言
引入了一个应该检查的公式,在这种情况下,
Statement1
不成立。命令
check
指示分析器
使用指定的作用域(特别是3)查找给定断言的反例。安-
[2
]这一条件是声明1-5的等价性所必需的
3
更准确地说,这道题还要求学生写出谓语Connected。