Fogalmi modell helyességvizsgálata

Mitől lesz helyes a fogalmi modellünk? Mit is értünk modell helyesség alatt? Hogyan tudjuk a modell helyességvizsgálatot arra használni, hogy jobban, pontosabban, formális módon fogalmazzuk meg a fogalmi modellünkkel kapcsolatos elvárásokat. A most következő cikkben ezt a kérdéskört járjuk körül.

Komplex szabályok a fogalmi modellezésben

Ahogy egyre komplexebb fogalmi modellekkel dolgozunk, hamar rájövünk arra, hogy a korábban bemutatott eszköztárunknak vannak korlátai: gyakran bonyolultabb szabályokat szeretnénk megkövetelni a rendszerünkkel kapcsolatban, mint egy egyszerű kapcsolat számosságot.

Nézzünk pár példát fogalmi modellekhez kapcsolódó komplex szabályokra:

Egy munkatárs nyilvántartó rendszerben csak olyan munkatárs szerepelhet, aki felnőtt. Egy tengeri fúrótornyokat menedzselő rendszerben csak olyan dolgozókat küldhetnek fel egy toronyra, melyek rendelkeznek a megfelelő tanúsítványokkal, és biztosítani kell azt, hogy minimum két ember legyen egy toronyba (ennek az oka egyébként az, hogy ha valaki mondjuk szívrohamot kap, akkor a másik tudjon segítséget hívni). Egy digitális tanúsítványokkal foglalkozó rendszerben csak olyan felhasználó írhat alá egy dokumentumot, amely nincs letiltva. Egy motorbérlő rendszerben egy adott motort egy adott idősávban egyszerre csak egy személy bérelhet ki, de az is csak akkor, ha a motor éppen elérhető (nincs szervizben, nincs töltés alatt, nem lopták el, stb.).

Ezeket a szabályokat invariánsnak nevezzük, és a rendszer minden állapotában teljesülniük kell.

Példa feladat

Ebben a cikkben egy példa feladatot – illetve annak egy részét – fogunk közösen megoldani, melyet a letscode.hu csapata mutatott be az egyik podcast-jük alkalmával.

Letscode.hu · Foglalórendszerterv

A feladat nagy vonalakban a következő:

Egy elektromos robogó bérléssel foglalkozó cég megbíz minket, hogy segítsünk nekik egy szoftver elkészítésében, mely a meglévő papír alapú folyamatukat gépesítené. Eddig egy kockás papíron vezették azt az információt, hogy ki, mikor, melyik robogót bérelte ki és mekkora idősávra. Külön vezették, hogy melyik robogót mikor kell szervizelni, esetleg ellopták-e, vagy összetörték-e.

Ez egy viszonylag egyszerű, jól definiált feladat, nézzük meg, hogy ezt hogyan is tudjuk iteratívan modellezni majd formálisan ellenőrizni. Ehhez a feladathoz most az Alloy nyílt forráskódú programot fogjuk használni.

Alloy nyelv és analizátor

Az Alloy egy nyílt forráskódú, bárki számára ingyenesen elérhető nyelv és analizátor, mely a következőképpen működik: a felhasználó megadja az egyes fogalmait, azok kapcsolatait, illetve az egyes szabályokat. Az Alloy képes arra, hogy az adott szabályok alapján példákat generáljon (ez lényegében megfelel az UML Object diagramjának). Az Alloy ennél azonban többet is tud: lehetőséget biztosít arra, hogy kérdéseket tegyünk fel: például van-e a szabályhalmaznak megfelelő példa, amely esetén egy robogót ketten is bérelnek. Az Alloy ilyenkor végigmegy az összes lehetőségen, és amennyiben talál egy ilyen példát, akkor azt megmutatja.

Az Alloy telepítése

Az alloytool-t a https://alloytools.org/download.html oldalról telepíthetjük, a telepítéséhez Java környezet szükséges. Az ingyenes Visual Studio Code-hoz létezik plugin, amely az Alloy letöltését és telepítését megoldja, első körben ezt az irányt javaslom a kedves olvasónak. A Visual Studio Code telepítése és elindítása után a plugins ikonra kattintva a keresőben írjuk be az alloy kulcsszót majd az első találnál nyomjunk rá az Install gombra.

Alloy fájl létrehozása

A plugin telepítése után válasszunk egy könyvtárat amibe dolgozni fogunk a File -> Open Folder menüben, majd hozzunk létre egy új file-t .als kiterjesztéssel:

Modellezés

Az első modell

Kezdjünk is neki a feladatnak, nézzük először a fogalmainkat. A következő fogalmak biztos hogy szerepelnek a rendszerben:

Ügyfél: aki bérelni akar
Robogó: a robogó, amit bérelni akar
Foglalás: annak a ténye, hogy egy ügyfél, egy robogót kibérelt

Nézzük meg, hogy ezt hogyan is tudjuk az Alloy-ban leírni:

module modeldriven/robogo

sig Robogo {
}

sig Ugyfel {
}

sig Foglalas {
}

run {} for 3

A program lehetőséget biztosít arra, hogy a modelljeinket modulokba szervezzük, az első sorban tehát definiálunk egy modul-t modeldriven/robogo néven.

A sig kulcsszóval tudunk fogalmat definiálni. Láthatjuk, hogy van három fogalmunk: Robogo, Ugyfel, illetve Foglalas. Szándékosan magyarul neveztem el a dolgokat, hogy jobban érthető legyen a példa azoknak is, akik nem beszélnek angolul.

A run sor arra kéri az Alloy-t hogy az egyes fogalmakból generáljon maximum 3-3 példányt, és mutassa meg. A kapcsos zárójellel egyelőre nem foglalkozunk.

Mentsük el a fájlt a CTRL + s gombbal, majd pedig vigyük az egeret a run fölé. Az így megjelenő Execute parancsra kattintva azt láthatjuk, hogy az Alloy talált a szabályoknak megfelelő példát vagy példákat.

A jobb oldali instance found-ra kattintva pedig megnyílik a program egy külön ablakban, és mutat egy példát (nem feltétlenül ezt):

Mit látunk a képen? Azt, hogy van egy Robogónk (egy példányunk a robogó fogalomból).

A Next gombra kattintva megkérhetjük az Alloy-t hogy mutasson egy másik példát.

Mit látunk a képen? Van egy Robogónk, van egy Ügyfelünk, és van egy Foglalásunk, de a foglalás önmagában áll, nem tartozik hozzá sem Robogó, sem pedig ügyfél.

Ezt szeretnénk? Nem, azt szeretnénk, hogy ha létrejön egy Foglalás, akkor ahhoz mindig tartozzon Robogó és Ügyfél is. Bővítsük tehát ezzel a relációval a modellünket.

Relációk használata

module modeldriven/robogo

sig Robogo {
}

sig Ugyfel {
}

sig Foglalas {
    ugyfel: one Ugyfel,
    robogo: one Robogo
}

run {} for 3

A Foglalas fogalom alá felvettünk két mezőt, az egyiket ugyfel, a másikat pedig robogo néven. A kapcsolatnak egy a számossága, ezt a one kulcsszóval jelöljük. Ezt azt jelenti hogy egy Foglalás példányhoz pontosan egy Ügyfél illetve pontosan egy Robogó tartozhat.

A következő táblázat segítséget nyújt a számosság meghatározásában:

Számosság	Jelentése
one	pontosan egy
lone	nulla vagy egy
set	nulla vagy több
some	egy vagy több

Generáljunk egy példát a megadott specifikációból:

Megszorítások használata

Az Alloy generált egy példát, ahol az egyes kapcsolatokat élekkel jelölte. Minden egyes példa egy beszélgetést indukál, melynek során feltesszük azt a kérdést, hogy az által kitalált szabályokból generált példák vajon helyesek-e, ezt szeretnénk-e látni? Ha nem, akkor bizony szabályokat kell meghatároznunk. Ezt egészen addig folytatjuk, amíg az összes példa, amit az Alloy generál, megfelelő nem lesz.

A fenti képen egy hibás példát láthatunk, mégpedig azért, mert az a szabályunk, hogy két foglalás nem tartozhat egyazon robogóhoz.

Ezért egy invariánst kell létrehoznunk, amely biztosítani fogja, hogy ilyen eset ne állhasson elő. Ezt a fact kulcsszó segítségével tudjuk megtenni:

module modeldriven/robogo

sig Robogo {
}

sig Ugyfel {
}

sig Foglalas {
    ugyfel: one Ugyfel,
    robogo: one Robogo
}

fact egyRobogoEgyFoglalashozTartozik {
    no disj f1, f2: Foglalas | f1.robogo = f2.robogo
}

run {} for 3

Mit is jelent ez a szabály? Ez a szabály azt jelenti hogy nincs (no) két (f1, f2: Foglalas) tetszőleges egymással nem megegyező (disj) Foglalás amely esetén igaz az hogy az elsőhöz tartozó robogó megegyezik a másodikhoz tartozó robogóval (f1.robogo = f2.robogo).

Nézzük meg, hogy ebből milyen példát generálunk:

Ez már megfelel annak, amit látni szeretnénk.

Feltétel vizsgálat

Amikor egy modellen dolgozunk, akkor nem csak szabályokat adhatunk meg, hanem kérdéseket is feltehetünk: vajon van-e olyan példa, amely bizonyos szabályoknak nem felel meg, és ha igen, akkor pontosan mi is ez. Vegyük az előző szabályunkat, de ne invariánsként, hanem feltételként.

module modeldriven/robogo

sig Robogo {
}

sig Ugyfel {
}

sig Foglalas {
    ugyfel: one Ugyfel,
    robogo: one Robogo
}

assert egyRobogoEgyFoglalashozTartozik {
    no disj f1, f2: Foglalas | f1.robogo = f2.robogo
}

check egyRobogoEgyFoglalashozTartozik for 3

Ehhez csak annyit kell tennünk hogy lecseréljük az fact kulcsszavunkat assert-re, majd pedig hozzáadunk egy új sort:

check egyRobogoEgyFoglalashozTartozik for 2

Ez arra utasítja az Alloy-t hogy az általa generált összes példára futtassa le a feltételt, és szóljon, ha talál olyat, amelyre ez nem igaz. Ahogy vártuk, a modell ellenőrző talál is ilyen példát, pontosabban ellenpéldát:

A linkre kattintva megnézhetjük az ellenpéldát, illetve a Next gombra kattintva további ellenpéldákat is láthatunk.

A teljes példa

Az eddig tanultak és némi dokumentáció olvasás alapján most már bárki képes lesz megoldani a korábban említett feladatot. Az én megoldásom a következő, kíváncsi vagyok, hogy ti mire juttok.

module modeldriven/robogo

sig Robogo, Ugyfel, IdoSzelet {   
}

enum Statusz {
    TOLTES_ALATT,
    SZERVIZ_ALATT,
    OSSZETORT,
    ELLOPOTT
}

sig RobogoEsemeny {
    robogo: one Robogo,
    statusz: one Statusz,
    idoszelet: one IdoSzelet
}

sig Foglalas {
    ugyfel: one Ugyfel,
    robogo: one Robogo,
    idoszelet: one IdoSzelet
}

fact statuszNemLebeg {
    all s: Statusz | some r: RobogoEsemeny | r.statusz = s
}

fact idoszeletNemLebeg {
    all i: IdoSzelet | i in (RobogoEsemeny.idoszelet + Foglalas.idoszelet)
}

fact nincsKetFoglalasUgyanarraARobogoraEsIdoszeletre {
    no disj f1, f2: Foglalas | 
    f1.robogo = f2.robogo and f1.idoszelet = f2.idoszelet
}

fact robogoNemFoglalhatoHaEsemenyVan {
    no f: Foglalas | some r: RobogoEsemeny | 
    f.idoszelet = r.idoszelet
}

fact egyIdoszeletbenCsakEgyEsemenyEgyRobogohoz {
    no disj e1, e2: RobogoEsemeny | 
    e1.robogo = e2.robogo and e1.idoszelet = e2.idoszelet
}

run {} for 4

Összefoglaló

Ebben a cikkben bemutattam az Alloy nevű modellező és ellenőrző rendszer funkcióinak egy apró szeletét, mely segítségével fogalmi modelleket tudunk definiálni és ellenőrizni. Maga a rendszer nagyon sok mindent tud, de ennek bemutatása túlmutat egy rövid bemutatás keretein: a téma iránt érdeklődők számára több leírást illetve videó anyagot is belinkeltem.

Azt gondolom, hogy ez az eszköz nagyon hasznos a fogalmi modellezés során és megfelelő helyen és időben alkalmazva komoly segítséget tud nyújtani abban, hogy a fogalmi modellünk helyes és konzisztens legyen.