CADP-pikaohje

CADP ("Construction and Analysis of Distributed Processes", formerly known as "CAESAR/ALDEBARAN Development Package"):n kotisivu löytyy osoitteesta http://www.inrialpes.fr/vasy/cadp/. Ohjelmisto toimii Linuxissa ja se on kevään 2007 kurssilla käytössä koneessa melkinkari.

Asetukset

Lisää .profile-tiedostoon seuraavat rivit: 
CADP=/opt/cadp ; export CADP
export PATH=$PATH:/opt/cadp/com
export PATH=$PATH:/opt/cadp/bin.iX86
export MANPATH=$MANPATH:/usr/man:/usr/local/man:$CADP/man

Käyttö

Graafinen käyttöliittymä käynnistyy komennolla xeuca. (Huom! .profile komennot saat ainakin voimaan loggaamalla ulos melkinkarista ja kirjoittautumalla uudelleen sisään.) Xeucan voi käynnistää myös /opt/cadp/com/xeuca. Lotos-ohjelmat (tiedostonimessä pääte .lot tai .lotos) näkyvät kukkaikoneina. Muodostetaan siirtymäsysteemi: Generate labelled transition system (ikonista hiirellä aukeava valikko). Mikäli ohjelma on virheellinen, tulostuu lista virheilmoituksista. Muuten ohjelmisto luo .aut tai .bcg -päätteisen tiedoston (esim. testi.lotos -> testi.aut/testi.bcg), jonka ikonissa on siirtymäsysteemi. Pääte riippuu siitä mikä optio generate:ssa valitaan. Jos testi.lotos tiedostosta generoidaan siirtymäsysteemi ja valitaan siirtymäsysteemin formaatiksi BCG tuloksena on tiedosto testi.bcg. jos taas valitaan siirtymäsysteemin formaatiksi Aldebaran, niin tuloksena on tiedosto testi.aut.

Siirtymäsysteemitiedosto testi.aut on ascii-esitys ja testi.bcg on binääriesitys vastaavan siirtymäsysteemin rakenteesta. Graafisen esityksen voi tulostaa valitsemalla ikonin hiirivalikosta Visualize ja Edit. Joskus kaaret menevät päällekkäin ja niitä kannattaa siirrellä.

Systeemin voi minimoida valitsemalla komennon Reduce ja vaihtoehdon "using Aldebaran" sekä "observational equivalence". Tuloksena syntyy tiedosto, jonka pääte on _o.aut /_o.bcg (esim. testi_o.aut).

Kahta prosessia (joita vastaavat siirt. systeemit esim: a.aut b.aut) voi vertailla komennolla Compare (valinta observation equivalence).

Siirtymäsysteemin deadlockit selviävät .aut tai .bcg -tiedoston komennolla information. Deadlockiin johtavan polun saa komennolla Find deadlocks.

Jos ohjelmasi ei käänny, niin

  1. Tarkista, että kaikki porttinimet on mainittu kyseisen prosessin parametreina
  2. Kaikki ulos näkyvät portit on annettu ohjelman parametreina (kaikki portit, jos et ole käyttänyt kätkentää)
  3. Muistathan, että puolipistettä edeltävä etutoiminto voi olla vain toiminto (a;P a on toiminto ja P prosessi)!
  4. Tietotyyppien käyttäminen edellyttää vastaavan kirjaston esittelyä library - endlib -määreillä (ks. esimerkki lopusta).
Esimerkki 
specification testi [a, b, c] : noexit behaviour

        P[a,b,c]
         |[b]|
        Q[a,b,c]

where

process P [a,b,c] : noexit :=
        b; P[a,b,c]   
         []
        b; a; stop
endproc

process Q [a,b,c] : noexit :=
        b; c;  stop
endproc

endspec
Esimerkki tietotyyppien käytöstä 
specification test[a]:exit

library
	BOOLEAN,
	NATURAL
endlib


behavior

(t1[a](1) |[a]| t2[a])

where

process t1[a](n:Nat):exit:=
a!n; exit
endproc

process t2[a]:exit:=
a?n:Nat; exit
endproc

endspec
Lisää esimerkkejä hakemistossa /opt/cadp/demos