У меня есть две модели, как показано ниже. Первый описывает модель. Пол узла и связанные с ним ребра и ограничения удалены во второй модели. 
//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
Кто-нибудь может объяснить причину?
