Aldebaran-pikaohje

Asetukset

CADP=/home/group/bisim/cadplinux ; export CADP
export PATH=$PATH:/home/group/bisim/cadplinux/com
export PATH=$PATH:/home/group/bisim/cadplinux/bin.iX86
export MANPATH=$MANPATH:/usr/man:/usr/local/man:$CADP/man

Käyttö

Graafinen käyttöliittymä käynnistyy komennolla 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 Aldebaran 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.

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 _omin.aut /_omin.bcg (esim. testi_omin.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ää edellyttää vastaavan kirjaston esittelyä library - endlib -määreillä (ks. esimerkki lopusta).

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

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