为什么Alloy中两种模型的一致性检查性能没有差异？答案

【问题标题】：Why does the peformance of consistency check of the two models in Alloy have no difference?为什么Alloy中两种模型的一致性检查性能没有差异？
【发布时间】：2015-03-27 13:35:55
【问题描述】：

我有以下两种型号。第一个描述模型。在第二个模型中删除了节点性别及其相关的边缘和约束。

//Signatures for nodes
sig NPerson{}
abstract sig NGender{}
abstract sig NCivilStatus{}
lone sig Nmale, Nfemale extends NGender{}
lone sig Nmarried, Nsingle, Ndivorced, Nwidowed extends NCivilStatus{}

//Signatures for edges
sig Ehusband{src:one NPerson, trg:one NPerson}
sig Ewife{src:one NPerson, trg:one NPerson}
sig EpGender{src:one NPerson, trg:one NGender}
sig EpCivstat{src:one NPerson, trg:one NCivilStatus}

//facts
fact HasHusbandIsMarried{
    all h:Ehusband|let P0=h.src,P1=h.trg|
    (P0=h.src and P1=h.trg) implies (some civstat0:EpCivstat|let married=civstat0.trg|
    (civstat0.src=P0 and married in Nmarried)) 
}

fact inv_Ewife_Ehusband{
    all x:NPerson, y:NPerson| (some xy:Ehusband| xy.src=x and xy.trg=y) <=>  (some yx:Ewife| yx.src=y and yx.trg=x) 
}

fact multi_EpCivstat{
    //mulitplicity on pCivstat:Person->CivilStatusmin:1;max:1
    all n:(NPerson)| let count = #{e:(EpCivstat)| e.src = n}| count>=1 and count <=1}

fact MarriedWithoutHusband{
    all civstat0:EpCivstat|let P0=civstat0.src,married=civstat0.trg|
    married in Nmarried and not (some h:Ehusband|let P2=h.trg|
    h.src=P0) implies (some w:Ewife|let P1=w.trg|
    w.src=P0) 
}

fact HasWifeIsMarried{
    all wife0:Ewife|let P1=wife0.src,Person1=wife0.trg|
    (P1=wife0.src and Person1=wife0.trg) implies (some civstat0:EpCivstat|let married=civstat0.trg|
    (civstat0.src=P1 and married in Nmarried)) 
}

fact multi_EpGender{
    //mulitplicity on pGender:Person->Gendermin:1;max:1
    all n:(NPerson)| let count = #{e:(EpGender)| e.src = n}| count>=1 and count <=1}

fact mult1_Ehusband{
    //mulitplicity on husband:Person->Person[0,1]
    all n:(NPerson)| lone e:(Ehusband)|e.src=n
}

fact mult1_Ewife{
    //mulitplicity on wife:Person->Person[0,1]
    all n:(NPerson)| lone e:(Ewife)|e.src=n
}

fact xor_Ewife_Ehusband{
    //XOR constraint between wife:Person->Person and husband:Person->Person
    all n:(NPerson) | let e1 = (some e : Ewife | e.src = n), e2=(some e : Ehusband | e.src = n)|(e1 or e2) and not(e1 and e2)
}

fact MarriedWithoutWife{
    all s:EpCivstat|let p1=s.src,married=s.trg|
    married in Nmarried and not (some w:Ewife|let p3=w.trg|
    w.src=p1) implies (some h:Ehusband|let p2=h.trg|
    h.src=p1) 
}

fact surj_EpGender{
    //surjective on pGender:Person->Gender
    all n:(NGender)| some e:(EpGender)| e.trg = n
}

fact irr_Ehusband{
    //reflexive on husband:Person->Person
    no e:(Ehusband)| e.src = e.trg
}

fact AtLeastOneSingle{
    some civstat0:EpCivstat|let P0=civstat0.src,single=civstat0.trg|
    single in Nsingle
}

fact surj_EpCivstat{
    //surjective on pCivstat:Person->CivilStatus
    all n:(NCivilStatus)| some e:(EpCivstat)| e.trg = n
}

fact irr_Ewife{
    //reflexive on wife:Person->Person
    no e:(Ewife)| e.src = e.trg
}

合金中的第二个模型

//Signatures for edges
sig Ehusband{src:one NPerson, trg:one NPerson}
sig Ewife{src:one NPerson, trg:one NPerson}
sig EpCivstat{src:one NPerson, trg:one NCivilStatus}

//facts
fact HasHusbandIsMarried{
    all h:Ehusband|let P0=h.src,P1=h.trg|
    (P0=h.src and P1=h.trg) implies (some civstat0:EpCivstat|let married=civstat0.trg|
    (civstat0.src=P0 and married in Nmarried)) 
}

fact inv_Ewife_Ehusband{
    all x:NPerson, y:NPerson| (some xy:Ehusband| xy.src=x and xy.trg=y) <=>  (some yx:Ewife| yx.src=y and yx.trg=x) 
}

fact multi_EpCivstat{
    //mulitplicity on pCivstat:Person->CivilStatusmin:1;max:1
    all n:(NPerson)| let count = #{e:(EpCivstat)| e.src = n}| count>=1 and count <=1}

fact MarriedWithoutHusband{
    all civstat0:EpCivstat|let P0=civstat0.src,married=civstat0.trg|
    married in Nmarried and not (some h:Ehusband|let P2=h.trg|
    h.src=P0) implies (some w:Ewife|let P1=w.trg|
    w.src=P0) 
}

fact HasWifeIsMarried{
    all wife0:Ewife|let P1=wife0.src,Person1=wife0.trg|
    (P1=wife0.src and Person1=wife0.trg) implies (some civstat0:EpCivstat|let married=civstat0.trg|
    (civstat0.src=P1 and married in Nmarried)) 
}

fact mult1_Ehusband{
    //mulitplicity on husband:Person->Person[0,1]
    all n:(NPerson)| lone e:(Ehusband)|e.src=n
}

fact mult1_Ewife{
    //mulitplicity on wife:Person->Person[0,1]
    all n:(NPerson)| lone e:(Ewife)|e.src=n
}

fact xor_Ewife_Ehusband{
    //XOR constraint between wife:Person->Person and husband:Person->Person
    all n:(NPerson) | let e1 = (some e : Ewife | e.src = n), e2=(some e : Ehusband | e.src = n)|(e1 or e2) and not(e1 and e2)
}

fact MarriedWithoutWife{
    all s:EpCivstat|let p1=s.src,married=s.trg|
    married in Nmarried and not (some w:Ewife|let p3=w.trg|
    w.src=p1) implies (some h:Ehusband|let p2=h.trg|
    h.src=p1) 
}

fact irr_Ehusband{
    //reflexive on husband:Person->Person
    no e:(Ehusband)| e.src = e.trg
}

fact AtLeastOneSingle{
    some civstat0:EpCivstat|let P0=civstat0.src,single=civstat0.trg|
    single in Nsingle
}

fact surj_EpCivstat{
    //surjective on pCivstat:Person->CivilStatus
    all n:(NCivilStatus)| some e:(EpCivstat)| e.trg = n
}

fact irr_Ewife{
    //reflexive on wife:Person->Person
    no e:(Ewife)| e.src = e.trg
}

我使用 run{} 来检查两个模型的一致性。这两个模型没有实例。我想看看性能差异。所以我使用范围直到 23。但结果不是我所期望的。

模型不一致。因此，要找到模型的有效实例，或确定没有实例，我希望分析器需要检查模型的每个可能实例。直观地说，如果我们删除结构的一部分，需要检查的可能实例应该更少，这意味着更少的检查应该花费更少的时间。

但第二次的表现模型甚至比第一个模型更差。以下是两种模型的验证时间，单位为毫秒。

Scope m1    m2
3   158     11
4   95      59
5   109     105
6   245     157
7   364     256
8   871     402
9   1652    646
10  1861    1479
11  1406    2418
12  5421    4343
13  6886    2609
14  10425   6553
15  13081   5871
16  19731   19453
17  16491   22249
18  21984   18191
19  39671   45510
20  60001   49958
21  67709   67892
22  101256  97801
23  135082  168585

谁能解释一下原因？

【问题讨论】：

标签： alloy

【解决方案1】：

在非常高的抽象层次上，我认为您的难题的答案在于杰克逊的软件抽象第 2.2 节中的讨论：

当然，分析器不会单独构建和检查每个案例；即使每个案例只使用一个处理器周期，10³⁰ 个案例 [如 sec 前面给出的示例所示。 2.2]仍然需要比宇宙年龄更长的时间。通过修剪可能性树，它可以在不完全检查的情况下排除大型子空间。

有人可能会猜想（但我没有测量过这个！），当第二个模型消除了一些约束时，它会使搜索空间更难修剪。（为了衡量这一点，我会看看我是否可以构建第三个模型，保留额外的签名但不保留约束，并看看它的时间比较。）

性能几乎总是一件复杂的事情；通过衡量而不是仅仅推测，您迈出了正确的第一步。

[Postscript] 在较低的抽象级别上，我为问题中包含的两个模型中的每一个添加了一个空谓词和一个run 命令，将一些丢失的签名声明恢复到第二个，并比较了在默认范围内搜索实例所花费的时间。我不清楚这两种模型在性能方面是否存在一致的差异。乍一看，同一模型在同一范围内的运行之间的差异有时似乎比模型 1 和模型 2 之间的差异更大。

Scope  Model 1...............  Model 2...............
       Trans.   Solve   Total  Trans.   Solve   Total

    3     132      32     164      17      11      28
           68      13      81      12      15      27 
           31      13      44      14       6      20
           23      12      35      10      47      57 
           13      16      29       9      15      24

    5      59      86     145      38     180     218
           37      88     125      54     103     157
           45      95     140      51     106     157
           31      89     120      24      89     113
           58      93     151      24      91     115

   10     640    6997    7637     140   13746   13886
          169    7237    7406     214   13717   13931
          189    6704    6893     188   15107   15295

   15     592   82872   83464     472   15522   15994
          543   78690   79233     574   16396   16970

   20    2701  840961  843662    1179 1082708 1083887

再看看你报告的时间，我看不出你描述的任何事态的迹象：

但第二个模型的性能比第一个模型的性能还要差。

相反，在您报告时间的 21 个范围中有 16 个，模型 2 更快，而不是更慢。无论哪种方式，差异都不是特别显着：对于大多数示波器，您报告两个模型的时间在 10% 或 15% 之内，几乎所有示波器的报告时间都在相同的数量级。（因此，如果您现在告诉我某些或所有行的列颠倒了，我的回答仍然是“告诉我为什么您认为这表明性能存在令人费解的差异”。）

【讨论】：

第二个模型不仅删除了约束，还删除了部分结构：两个签名。
是的，确实如此。（实际上，更像是八个签名，从您上面显示的两个文件之间的差异来看，但似乎其中一些在您在此处粘贴的版本中被意外删除了。）但这似乎是一个经验问题，是否与删除约束相比，删除两个签名对速度的影响更大。你说第二种模式比较慢；如果是这样，您就知道哪个变化更重要。但您报告的数据却恰恰相反。
但理论上，如果我们将 Alloy 中的分析视为检查可能性树。对于每个范围，M2 的可能性树包含在 M1 的树中。结构 M1-M2 及其相关约束不影响 M2 的可能性树。想想看。由于 M2 的每个测试用例都不是 M2 的实例，因此无论何时添加由 Gender 或 gGender (M1-M2) 类型的元素，它都不会成为 M1 的实例。
表示M2的一致性测试用例少于M1一致性测试的测试用例。因此，M2 的性能应始终优于 M1，尤其是当范围扩大时。但是，您的报告也显示出与预期相反的结果。
两点。 (1) 您似乎假设当可能实例的空间较大时，分析器将不得不检查更多的案例以耗尽空间。但是分析器将检查的案例数量不仅取决于可能性空间的大小，还取决于分析器通过修剪树可以排除的可能性的数量，这取决于大小以外的很多东西树的。 (2) 您似乎认为这里的性能存在显着且一致的差异；为什么？数字似乎没有显示。