syksy 1997
Harjoitustyöohje
I. YLEISTÄ
Kukin kurssilainen saa oman tehtävän.
Annettu tehtävä ratkaistaan kahdella tavalla:
- lauselogiikan toteutuvuusongelmana ja
- logiikkaohjelman stabiilin mallien löytämisongelmana.
Tätä varten tehdään käännös tehtävästä
- toisaalta lauselogiikkaan siten, että käännöksen mallit vastaavat
hyväksyttäviä ratkaisuja tehtävälle ja
- toisaalta logiikkaohjelmiin siten, että logiikkaohjelman stabiilit
mallit vastaavat hyväksyttäviä ratkaisuja
Sitten haetaan tehtävään ratkaisu käyttäen lauselogiikan ja logiikkaohjelmien
toteutuksia. Käännettäessä tehtävää lauselogiikan lauseiksi voi apuna
käyttää satplan-ohjelmisto.
Kukin kurssilainen pitää lyhyen (15min) esityksen harjoitustyöstään ti
2.12.1997 klo 14-17.
Hyväksytty harjoitustyö edellyttää kirjallista työselostusta, jossa kuvataan
laaditut käännökset ja löydetyt ratkaisut sekä annetaan ajoesimerkit
niin, että on periaatteessa mahdollista toistaa tehty ratkaisu.
Ratkaisuna tehdyt ajoesimerkit palautetaan myös sähköisessä muodossa
siten, että tehtävien tarkastuksen yhteydessä on mahdollista suorittaa
tietokoneajoja.
Arvosanaan nostavasti vaikuttavat esim.
- perustehtävää hankalamman ongelman ratkaiseminen (saatavissa on sarja
vaikeutuvia tehtäviä, joiden avulla voi osoittaa mihin asti laadittu
ratkaisutekniikkaa pystyy).
- löydetyn ratkaisun optimaalisuuden osoittaminen,
- tulokset käytetyn käännöksen laajennettavuudesta ja muunneltavuudesta sekä
- tulokset käytetyn ratkaisumenetelmän herkkyydestä esim. esitystavalle,
ylimääräiselle/redundantille informaatiolle, ja tehtävän koon muutoksille.
Harjoitustyön viimeinen palautuspäivä on pe 12.12.1997.
Harjoitustyö arvostellaan kirjallisen työselostuksen pohjalta.
Harjoitustyön arvosanalla voi olla korottava vaikutus kurssin arvosanaa:
jos harjoitustyön arvosana on korkeampi kuin tentistä saatu,
opintojakson arvosanaksi tulee tentinarvosana korotettuna yhdellä (ei
kuitenkaan koske tentin arvosanoja 0 ja 5).
II. TARJOLLA OLEVIA OHJELMISTOJA
Olemme asentaneet harjoitustyön tekemiseen riittävän ohjelmiston LK:n
hp-työasemiin ("puut": palisanteri, palmu, pihlaja, ...)
Tarjolla on
- satplan, walksat ja ntab -ohjelmistot,
joiden avulla voi tehdä lauselogiikkaa koskevan puolen
harjoitustyöstä ja
- smodels-ohjelmisto logiikkaohjelmia koskevaan osuuteen
Binaarit löytyvät hakemistosta ~psimons/satplan/system/bin ja
käyttöohjeita hakemistosta ~psimons/satplan/doc
Ohjelmistojen käyttö edellyttää polkunimien hoitamista kuntoon. Esim.
bash:ia käytettäessä tarvitaan määrittelyt:
SATPLAN=~psimons/satplan/system
export SATPLAN
PATH=$SATPLAN/bin:$PATH
Muille komentotulkeille löytyy ohjeita tiedostosta
~psimons/satplan/README.
III. HARJOITUSTYÖN TEKEMINEN MUILLA KONEILLA
satplan, walksat, ntab ja smodels -ohjelmistoista on käytössä
lähdekoodi, joten niiden asentaminen periaatteessa ei ole kovin vaikeaa
jos käytössä on normaalit Unix-työkalut: make, gcc, awk, perl, ...
(Huom! ntab ei ole kirjoitettu kovin kannettavasti ja sen
asentaminen 64-bittiseen arkkitehtuuriin näyttää hankalalta).
Seuraavassa ohjeita ohjelmien asentamiseen (kun käytössä on normaalit
gnu-työkalut).
- satplan ja walksat
- hae
satplan.tar.gz
- pura tar-tiedosto ja toimi system/README.install ohjeiden mukaan.
- ntab
- hae
ntab.tar.gz
- pura tar-tiedosto ja aja make hakemistossa tableau
- ohjeita tableau/REAME
- Huom! Kopio binaari (ntab) tiedostoksi $SATPLAN/bin/tableau, niin
voit käyttää ntab:a satplan:ssa.
- smodels
- hae tältä kotisivulta
smodels 1.9
- pura tar-tiedosto ja aja make (binaari on nimeltään smodels)
- samoin hae
parse 1.2
- pura tar-tiedosto ja aja make (binaari on nimeltään parse)
- Käyttöohjeita README
ja
manual;
Ota yhteyttä
Ilkka.Niemela@hut.fi
tai
Patrik.Simons@hut.fi,
jos eteen tulee ongelmia tai kysymyksiä.