Почему производительность проверки согласованности двух моделей в Alloy не имеет различий?

Question

У меня есть две модели, как следующие. Первый описывает модель. Пол узла и связанные с ним ребра и ограничения удаляются во второй модели.

//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

Может кто-нибудь объяснить причину?

Answer 1

На очень высоком уровне абстракции, я думаю, что ответ на вашу загадку лежит в обсуждении в разделе 2.2 программных абстракций Джексона:

Конечно, анализатор не создает и не проверяет каждый случай в отдельности; даже если он использовал только один процессорный цикл на случай, 10³⁰ случаев [как в примере, приведенном ранее в с. 2.2] все равно займет больше времени, чем возраст вселенной. Сокращая дерево возможностей, оно может исключить большие подпространства, не изучая их полностью.

Можно предположить (но я не измерял это!), Что, когда вторая модель устраняет некоторые ограничения, это затрудняет сокращение пространства поиска. (Чтобы измерить это, я хотел бы посмотреть, смогу ли я построить третью модель, которая сохраняет дополнительные сигнатуры, но не ограничения, и посмотреть, как сравниваются ее времена.)

Производительность почти всегда сложный вопрос; Вы сделали правильный первый шаг, измеряя, а не просто размышляя.

[Постскриптум] На более низком уровне абстракции я добавил пустые предикаты и 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

И, снова обращая внимание на сроки, о которых вы сообщаете, я не вижу никаких признаков того состояния, которое вы описываете:

Но производительность для второй модели даже хуже, чем для первой модели.

Напротив, в 16 из 21 областей, по которым вы сообщаете время, модель 2 работает быстрее, а не медленнее. И в любом случае разница не особенно значительна: время, которое вы сообщаете для двух моделей, находится в пределах десяти или пятнадцати процентов для большинства областей и в одинаковом порядке для почти всех областей. (Поэтому, если вы сейчас скажете мне, что столбцы были перевернуты для некоторых или всех строк, мой ответ все равно будет: "Скажите, почему вы думаете, что это указывает на удивительную разницу в производительности".)