6.1. Sarežģītības apakšējais novērtējums - EXPTIME
Tas pierādīts rakstā:
Daniela Berardi, Diego Calvanese, Giuseppe De Giacomo. Reasoning on UML class diagrams is EXPTIME-hard. Proceedings of International Workshop on Description Logics (DL03), September 5-7, 2003, Roma, Italy (online copy: PDF).
Vispārīgajā gadījumā, UML klašu diagramma sastāv no grafiska attēla un OCL valodā pierakstītu ierobežojumu kopas (constraints). Grafiskais attēls definē diagrammas primitīvus (jeb atomāros jēdzienus), kā arī uzdod daļu no ierobežojumiem (tikai vienkāršākos no tiem, piemēram, disjointness un covering).
UML klašu diagrammai var risināt šādus secināšanas uzdevumus:
- (diagram consistency) noteikt, vai diagramma ir saderīga vai pretrunīga (t.i. vai eksistē modelis - intepretācija, kurā izpildās visi diagrammas ierobežojumi),
- (class consistency) noteikt, vai diagrammā dotā klase ir vai nav tukša (t.i. vai eksistē modelis, kurā izpildās visi diagrammas ierobežojumi, un dotā klase nav tukša),
- (class equivalence) noteikt, vai diagrammā divas klases ir vai nav ekvivalentas.
Viegli parādīt, ka jebkuru no šiem uzdevumiem ir viegli reducēt uz jebkuru citu (citai diagrammai, protams), tāpēc no algroritmu sarežģītības viedokļa mēs varam aplūkot tikai vienu uzdevumu - piemēram, class consistency.
Otrkārt, ja atļaujam izmantot valodas OCL iespējas pilnā apjomā, tad klašu diagrammā var iekodēt jebkuru pirmās pakāpes teoriju, t.i. šai gadījumā visi secināšanas uzdevumi ir algoritmiski neatrisināmi.
Tāpēc raksta autori pētī secināšanas sarežģītību gadījumā, ja valodu OCL neizmanto vispār, t.i. visi ierobežojumi tiek fiksēti tikai ar klašu diagrammas grafisko līdzekļu palīdzību.
Algoritma sarežģītību mērī kā funkciju no "diagrammas izmēra" (to var definēt, piemēram, kā tā XML faila garumu, kas glabā diagrammas saturu).
Teorēma. Ja UML klašu diagrammās izmanto tikai zemāk minētos līdzekļus, tad class consistency uzdevums tām ir EXPTIME-hard: klases (bez atribūtiem un metodēm), binārās asociācijas bez multiplicitātes ierobežojumiem vai ar ierobežojumu 1..* vienā no galiem, apakšklases un apakšasociācijas ar disjointness un covering ierobežojumiem.
Pierādījums. Sākam ar loģiku ALC, atļaujot jebkuras T-kastes aksiomas C1<=C2, arī cikliskās (A-kaste var palikt tukša). Kā var noskaidrot, piemēram, J.Zoļina navigatorā, šādā gadījumā class consistency uzdevums ir EXPTIME-hard.
Ideja: loģiku ALC reducēsim uz šaurākām loģikām, ko būs vieglāk "ielikt" klašu diagrammā.
1. Vispirms jebkuru zināšanu bāzi loģikā ALC reducēsim uz zināšanu bāzi K' šaurākā loģikā ALC', kur aksiomās C1<=C2 jēdziens C1 drīkst būt tikai atomārs, bet C2 - jebkura izteiksme.
Precīzāk, aplūkosim zināšanu bāzi K loģikā ALC un jēdzienu-izteiksmi C, kura saderību ar K gribam noskaidrot. Šo uzdevumu reducēsim uz jēdziena atomāra jēdziena C^X saderību ar zināšanu bāzi K', kurā ir tikai viena aksioma:
X <= šķēlums {-C1 v C2 | C1<=C2 ir bāzes K aksioma} ^ šķēlums {Ap.X | p ir loma no K vai C }.
C sader ar K tad un tikai tad, ja C^X sader ar K' (pārliecināsimies). Tiešām, pirmkārt, ja eksistē modelis, kurā izpildās visas K aksiomas un C ir netukša klase, tad šajā modelī X var interpretēt kā visu objektu klasi (to dažreiz apzīmē ar T). Tad aksioma būs patiesa un C^X būs netukša klase. Otrkārt, ja eksistē modelis, kurā ir patiesa K' aksioma un C^X ir netukša klase, tad šajā modelī arī X ir netukša klase, kura ir slēgta pret visām lomām p (no K un C), un kurā ir patiesas visas K aksiomas. Q.E.D.
2. Nākošais solis - zināšanu bāzi K' loģikā ALC' reducēsim uz zināšanu bāzi K'' loģikā ALC'', kurā atļauti tikai šādi līdzekļi:
- negācija atļauta tikai pie atomāriem jēdzieniem,
- apvienojuma operācija ir atļauta tikai atomāriem jēdzieniem, bet šķēlums - nav atļauts nemaz,
- kvantori Er.C un Ar.C ir atļauti tikai atomāriem jēdzieniem C;
- aksiomās C1<=C2 jēdziens C1 drīkst būt tikai atomārs, C2 - atomārs jēdziens, tā negācija vai divu atomāru jēdzienu apvienojums.
Vispirms K' aksiomu labās puses reducēsim negāciju normālformā (tas prasa lineāru laiku). Pēc tam taisīsim rekursiju:
- aksiomu A<=C1^C2 aizvietosim ar A<=C1 un A<=C2;
- aksiomu A<=C1 v C2 aizvietosim ar A<=A1 v A2, A1<=C1, A2<=C2, kur A1 un A2 ir jauni atomāri jēdzieni;
- aksiomu A <= Ap.C1 aizvietosim ar A<=Ap.A1, A1<=C1, kur A1 ir jauns atomārs jēdziens;
- aksiomu A <= Ep.C1 aizvietosim ar A<=Ep.A1, A1<=C1, kur A1 ir jauns atomārs jēdziens;
Rekursijas rezultātā tiek iegūta zināšanu bāze K'' loģikā ALC''. Izdarīto aizvietošanu skaits ir lineārs, jo katru ALC operāciju K' aksiomās mēs aizvietojam tikai vienreiz. Tāpēc gan redukcijas laiks, gan bāzes K'' izmērs būs lineāri atkarīgi no bāzes K' izmēra (un tāpēc - arī no K+C izmēra).
3. Zināšanu bāzi K'' jau var samērā viegli "ielikt" UML klašu diagrammā.
Veidosim diagrammu K''', iekļaujot tajā kā klašu simbolus visus K'' jēdzienus. Iezīmēsim arī klasi T, kura būs augsšklase visām K''' klasēm.
Visas K'' lomas p zīmēsim kā asociācijas no T uz T (t.i. nekādi neierobežojot, kuru klašu instances var šo lomu attiecības atrasties).
Un beidzot, K'' aksiomas attēlosim kā apakšklašu attiecības (B un D ir atomāri jēdzieni):
- Aksiomu B<=D attēlosim, atzīmējot B kā D apakšklasi.
- Aksioma B<= ~D nozīmē, ka B un D ir disjoint, tāpēc to attēlosim kā: "B and D are disjoint subclasses of T" (grafisko attēlu sk. rakstā).
- Aksiomas B <= D1 v D2 attēlošanai ievedīsim palīgklasi D3=D1 v D2, un diagramma zīmēsim: "B is subclass of D3", "D1 and D2 are covering subclasses of D3" (grafisko attēlu sk. rakstā).
- Aksioma B <= Ap.D nozīmē asociācijā p klases B instances var saistīties tikai ar klases D instancēm. Tās attēlošanai (grafisko attēlu sk. rakstā) var ievest: a) asociācijas p apakšasociācijas p' un p'' (ar piebildi covering), b) klases T apakšklasi B' (ar piebildi disjoint with B), c) p' savienot ar B (kā domain) un D (kā range), d) p'' savienot ar B' (kā domain) un T (kā range).
- Aksioma B <= Ep.D nozīmē, ka katrai klases B instancei ir asociācija p ar vismaz vienu klases D instanci. Tās attēlošanai (grafisko attēlu sk. rakstā) var ievest asociācijas p apakšasociāciju p', savienojot to ar klasi B (kā domain) un ar klasi D (kā range), pie tam D galā ir jāuzliek multiplicity constraint 1..*.
Uzdevums. Pārliecinieties, ka bāzei K'' eksistē modelis tad un tikai tad, ja eksistē modelis diagrammai K'''.
Tā kā viss redukcijas process no zināšanu bāzes K+C līdz diagrammai K''' ir izpildāms lineārā laikā, un K''' izmērs ir lineāri atkarīgs no K+C, tad līdz ar to esam pierādījuši, ka UML klašu diagrammām, kurās izmanto tikai teorēmas formulējumā minētos līdzekļus, class consistency uzdevums ir EXPTIME-hard. Q.E.D.
Problēma (vizmaz maģistra darba tēma). Vai secinājums par EXPTIME-hardness paliks spēkā arī tad, ja diagrammās atļausim lietot ne visus līdzekļus, kas minēti teorēmas formulējumā? Piemēram, neļausim izmantot apakšasociācijas? Vai neļausim izmantot disjointness un/vai covering nosacījumus?
6.2. Sarežģītības augšējais novērtējums
Daniela Berardi, Andrea Cali, Giuseppe De Giacomo. Reasoning on UML class diagrams. Technical Report 11-03, Dipartimento di Informatica e Sistemistica, Universit? di Roma "La Sapienza", 2003 (online copy: PDF).
Ja atļaujam UML klašu diagrammās izmantot valodas OCL iespējas pilnā apjomā, tad klašu diagrammā var iekodēt jebkuru pirmās pakāpes teoriju, t.i. šai gadījumā visi secināšanas uzdevumi ir algoritmiski neatrisināmi.
Tāpēc raksta autori pētī secināšanas sarežģītību gadījumā, ja valodu OCL neizmanto vispār, t.i. visi ierobežojumi tiek fiksēti tikai ar klašu diagrammas grafisko līdzekļu palīdzību.
Šajā rakstā autori parāda, ka ja UML klašu diagrammās neizmanto OCL valodā rakstītus ierobežojumus, tad secināšanas uzdevums (piemēram, class consistency) tajās ir EXPTIME-complete.
Pirmo pusi - apakšējo novērtējumu sk. iepriekšējā sadaļā 6.1.
Augšējo novērtējumu autori pierāda, definējot polinomiālu algoritmu, kas reducē class consistency uzdevumu UML klašu diagrammās (bez OCL) uz class consistency uzdevumu zināšanu bāzei loģikā ALCIQ. Kā var noskaidrot, piemēram, J.Zoļina navigatorā, šī pēdējā uzdevuma sarežģītība ir EXPTIME (sk. ALCIQ ar general T-Box).
Redukcijas algoritms
Klases
Mums te ir jātiek galā ar ar klasēm, to atribūtiem un metodēm (jeb operācijām).
Diagrammas klasi B attēlojam kā atomāru jēdzienu ar to pašu vārdu B.
Klases B atribūtu a attēlojam kā atomāru lomu ar vārdu a un aksiomu B<=Aa.T (kāpēc tā vajadzīga?). Ja atribūtam ir multiplicity constraint i..j, tad to pierakstām kā aksiomu B <= (>=i)a.T ^ (<=j)a.T. Protams, i=0 gadījumā nav vajadzīgs konjunkcijas pirmais loceklis, bet j=* gadījumā nav vajadzīgs konjunkcijas otrais loceklis (un ja i..j ir 0..*, tad šāda aksioma vispār nav vajadzīga).
Klases B operāciju (metodi)
f(): D, ja tai nav parametru, attēlojam kā atomāru lomu f un
aksiomu
B <= Af.D ^ (<=1)f.T,
kas nozīmē, ka katrai klases B instancei lomas f galā ir tikai
klases D instances, un pie tam ne vairāk kā viena.
Klases B operācija (metode) f(p1:P1,..., pn:Pn): D, ja tai ir n parametri, būtu jāmodelē kā "atribūts" f, kura vērtība ir n argumentu funkcija. Tāpēc f varam attēlot kā lomu f, kas B instances saista ar jauna jēdziena F instancēm, kurām ir n+1 loma p1, ..., pn, q (q attiecas uz funkcijas f vērtību). Utt. To sauc par "reifikāciju" (reification - asociācijas modelēšanu ar klasi).
Asociācijas
Bināru asociāciju p starp klasēm C1 un C2 var attēlot kā lomu p ar aksiomu T <= Ap.C2 ^ Ap-1.C1. Ja C2 galā ir multiplicitātes ierobežojums i..j, tad to var pierakstīt ar aksiomu C1 <= (>=i)p.T ^ (<=j)p.T. Ja tāds ierobežojums ir C1 galā, tad jāraksta aksioma C2 <= (>=i)p-1.T ^ (<=j)p-1.T.
Nebināru asociāciju attēlošanai atkal jāizmanto
reifikācija. Piemēram, 3-vietīgu asociāciju p starp klasēm
C1, C2, C3, kuras komponentu lomas ir p1, p2, p3 attēlojam kā
jēdzienu P un 3 lomas p1, p2, p3, kā arī aksiomu:
P <= Ep1.C1 ^ (<=1)p1 ^ Ep2.C2 ^ (<=1)p2 ^ Ep3.C3 ^
(<=1)p3.
Multiplicitātes ierobežojumus attēlojam tāpat kā binārajām
asociācijām.
Apakšklases
Ja mūsu diagrammā klase C1 ir klases C2 apakšklase, tad to mēs varam attēlot kā aksiomu C1<=C2.
Ja C1 un C2 ir klases C3 disjoint apakšklases, tad to var attēlot ar aksiomas C1<=C3, C2 <=C3 un C1 <= -C2.
Ja C1 un C2 ir klases C3 covering apakšklases, tad to var attēlot ar aksiomas C1<=C3, C2 <=C3 un C3 <= C1 v C2.
Turpinājums sekos.