Home Articles

扩展签名和原子实例化

Asked
Viewed 1983 times
0

我使用的是Alloy 4.2,我使用继承有一个复杂性问题 . 显然,签名之间的继承不像我以前在面向对象编程中那样(或者至少像我期望的那样) .

显然,当在run命令中没有设置exact关键字时,即使根抽象类是抽象的,原子也会实例化为根抽象签名的原子 . 当exact关键字用于指定命令时,原子会在指定时被实例化:叶子具体类 .

我希望能够搜索具有从另一个抽象继承的集合的可变性的解决方案 . 它允许我在抽象签名中指定然后存在于叶签名中的关系 .

示例(详细程度需要设置为高):

abstract sig A {}

sig B extends A {}

sig C extends A {}

pred show {}

run show for 6 B, 6 C
run show for exactly 6 B, exactly  6 C

当我在这里运行2谓词时有以下痕迹:

Executing "Run show1 for 6 B, 6 C"
   Sig this/B scope <= 6
   Sig this/C scope <= 6
   Sig this/A scope <= 12
   Sig this/A in [[A$0], [A$1], [A$2], [A$3], [A$4], [A$5], [A$6], [A$7], [A$8], [A$9], [A$10], [A$11]]
   Sig this/B in [[A$0], [A$1], [A$2], [A$3], [A$4], [A$5], [A$6], [A$7], [A$8], [A$9], [A$10], [A$11]] with size<=6
   Sig this/C in [[A$0], [A$1], [A$2], [A$3], [A$4], [A$5], [A$6], [A$7], [A$8], [A$9], [A$10], [A$11]] with size<=6
   Solver=minisatprover(jni) Bitwidth=0 MaxSeq=0 SkolemDepth=4 Symmetry=20
   15152 vars. 24 primary vars. 55808 clauses. 55164ms.
   Instance found. Predicate is consistent. 225ms.

在这个执行跟踪中,我们可以看到,尽管A是抽象的,但所有B和C都被实例化为A原子 . 我们可以看到B和C在A元素集中挑选了6个不相交的元素 .

Executing "Run show2 for exactly 6 B, exactly 6 C"
   Sig this/B scope <= 6
   Sig this/C scope <= 6
   Sig this/A scope <= 12
   Sig this/A in [[B$0], [B$1], [B$2], [B$3], [B$4], [B$5], [C$0], [C$1], [C$2], [C$3], [C$4], [C$5]]
   Sig this/B == [[B$0], [B$1], [B$2], [B$3], [B$4], [B$5]]
   Sig this/C == [[C$0], [C$1], [C$2], [C$3], [C$4], [C$5]]
   Solver=minisatprover(jni) Bitwidth=0 MaxSeq=0 SkolemDepth=4 Symmetry=20
   0 vars. 0 primary vars. 0 clauses. 2ms.
   Instance found. Predicate is consistent. 14ms.

在此跟踪中,我们可以看到A集仅由B和C元素组成,而不是由A元素组成 . 我们还可以看到,由于组合爆炸,求解时间非常不同,即使第二个命令解决的问题比第一个命令更简单 .

为了最大限度地缩短求解时间,是否可以通过在签名上使用事实或设置约束来获得看起来像这样的跟踪?

Executing "Run show2 for 6 B, 6 C"
   Sig this/B scope <= 6
   Sig this/C scope <= 6
   Sig this/A scope <= 12
   Sig this/A in [[B$0], [B$1], [B$2], [B$3], [B$4], [B$5], [C$0], [C$1], [C$2], [C$3], [C$4], [C$5]]
   Sig this/B == [[B$0], [B$1], [B$2], [B$3], [B$4], [B$5]]
   Sig this/C == [[C$0], [C$1], [C$2], [C$3], [C$4], [C$5]]

1 Answer

  • 1

    如果未使用“exact”关键字,则在求解模型之前无法知道每个原子的实际类型 . 换句话说,范围

    run show for 6 B, 6 C
    

    仅指定上限,这意味着允许有效实例包含例如 B 的2个原子和 C 的1个原子(取决于模型中的实际约束) . 这就是为什么Alloy只能分配足够的原子来开始(给它们一些通用名称,在这种情况下,名称是从基类型的名称派生的),并且在找到实例之后,每个原子将被重命名(在可视化器中)到反映其实际类型 .

    只有在指定精确范围时,Alloy才能最小化边界(如您所注意到的),以便可能缩短解决时间 .

Related