Maria on rinnakkaisten järjestelmien saavutettavuusanalysaattori, joka perustuu algebrallisiin järjestelmäverkkoihin, jotka ovat korkean tason Petri-verkkoja. Se on kirjoitettu C++:lla, ja se on vapaasti hyödynnettävissä GNU General Public Licensen ehdoilla.
| 0.1 | 17. syyskuuta 1999 |
| 0.2 | 10. elokuuta 2001 |
| 1.0 | 1. marraskuuta 2001 |
| 1.0.1 | 5. helmikuuta 2002 |
| 1.1 | 23. huhtikuuta 2002 |
| 1.2 | 23. kesäkuuta 2002 |
| 1.3 | 4. syyskuuta 2002 |
| 1.3.1 | 15. marraskuuta 2002 |
| 1.3.2 | 5. joulukuuta 2002 |
| 1.3.3 | 9. joulukuuta 2002 |
| 1.3.4 | 20. kesäkuuta 2003 |
| 1.3.5 | 29. heinäkuuta 2005 |
Maria-työkaluun on erikseen saatavilla LTL-X-mallintarkistin modulaarisille tila-avaruuksille. Koska toteutus on puutteellinen, se jaetaan erillisinä muutoksina versiolle 1.3.4 ja muutoksina versiolle 1.3.5. Lue lisätietoja ja asennusohjeet.
Lue myös hankkeen taustasta ja tutustu julkaisuihimme.
Saavutettavuusanalysaattori, lennosta toimiva mallintarkistin ja graafityökalu ovat olleet toiminnassa vuodesta 1999, jolloin julkaistiin versio 0.1. Vuonna 2001 julkaistuissa versioissa 0.2 ja 1.0 on kehittyneempiä toimintoja kuten reiluusoletuksia hyödyntävä mallintarkistin, käännökset matalan tason verkoksi ja C-koodiksi sekä graafinen käyttöliittymä.
Saavutettavuusgraafin esitystyökalu perustuu GraphViz-ohjelmistoon, jonka AT&T on kehittänyt graafien esittämistä varten. Työkalusta on kaksi toteutusta:
lefty-kielellä kirjoitettuun
dotty-graafitoimittimeen. Se on suosittelemamme
toteutus. Se toimii vanhoissakin GraphVizin versioissa.tcldot-kirjastoon. Se
on kokeellinen toteutus, josta puuttuu ominaisuuksia. Se pystyy
näyttämään vain yhden graafin kerrallaan.Marko Mäkelä lopetti työkalun kehittämisen vuonna 2004. Versio 1.3.5 (jossa on vähäisiä siirrettävyyden ja tehokkuuden parannuksia) jäänee viimeiseksi hänen julkaisemakseen.
Ohjelmiston lähdekoodin jakelupaikka on http://www.tcs.hut.fi/Software/maria/src/. Ajettavaksi ohjelmaksi sen voi kääntää esimerkiksi GCC:llä.
Voit myös kokeilla uusinta kehitteillä olevaa lähdekoodia ja käyttöohjetta.
Windows-käyttäjien iloksi tarjoamme zip-pakkauksen mingw:n ristiinkääntäjäksi asennetulla gcc-2.95.2:lla käännetystä ajettavasta ohjelmasta. Tämä versio on alkutekijöissään: C-koodin tuottaminen ei toimi eikä graafien esittäminen kuvina onnistu.
Maria 1.3.4:n käyttöohje, joka on tuotettu GNU-hankkeen Texinfo-järjestelmällä, on saatavissa PDF-muodossa.
Marian saavutettavuusgraafitiedostojen rakenne ja tilakoneiden kielet on kuvattu erikseen.
Marian ohjelmointityyli perustuu Ellemtelin suosituksiin.
Tämä sivu on saatavissa myös seuraavilla kielillä:
English
Oletuskielen
asettamisohjeet