FORMAALIT MENTELMÄT                                  Jyväskylän yliopisto
Kevät 2005                                          Tietotekniikan laitos

Luentomateriaali saatavilla Korpin kautta.

DEMOT 8 (23.3.2005) - Tehtävät

Lukuläksy: Luentomonisteen luvut 4.2.4, 4.2.5 ja 14.

1-2.
   Internet-sähköpostijärjestelmä koostuu prosesseista, jotka
   välittävät erityisellä tavalla muotoiltuja viestejä toisilleen.
   Osa näistä prosesseista on niinsanottuja käyttäjäagentteja (MUA,
   Mail User Agent), jotka ihmiskäyttäjän puolesta ottavat vastaan ja
   lähettävät viestejä; loput ovat välittäjäagentteja (MTA, Mail
   Transfer Agent).  Ne kaikki kuitenkin puhuvat samaa protokollaa,
   SMTP:tä (Simple Mail Transfer Protocol).

   Tehdään seuraavat yksinkertaistukset:
   - Kukin prosessi juttelee kerrallaan vain yhden prosessin kanssa;
     juttelu tapahtuu CSP-kanavan PEER kautta.

   - Kullakin prosessilla on oma uniikki tunnuksensa, joka on
     luonnollinen luku ja jonka prosessi itse tietää.

   - Juttelu muodostuu viesteistä, jotka ovat luonnollisia lukuja.

   - Juttelu alkaa, kun jompi kumpi ("lähettäjä") lähettää toiselle
     ("vastaanottaja") oman tunnuksensa.  Vastaanottaja vastaa siihen
     joko hyväksymis- tai hylkäysviestillä.  Jos vastaus on hylkäävä,
     juttelu päättyy siihen.  Muuten lähettäjä lähettää
     järjestyksessä
      1. sen prosessin tunnuksen, jolta viesti on alunperin peräisin,
      2. sen prosessin tunnuksen, jolle viesti on tarkoitettu,
      3. viestin koon (viestiin kuuluvien luonnollisten lukujen
         lukumäärä), sekä
      4. viestin sisällön (jono luonnollisia lukuja, joiden lukumäärä
         lähetettiin kolmantena tietona).
     Tämän jälkeen vastaanottaja vastaa joko hyväksymis- tai
     hylkäysviestillä.  Jos vastaus on hyväksyvä, vastaanottaja ottaa
     vastuun viestin välittämisestä perille, muuten viesti jää
     lähettäjän vastuulle.  Juttelu päättyy tähän vastaukseen.

   - Käytettävät viestikoodit:
          0 hylkäävä vastaus
          1 hyväksyvä vastaus

   - Yhteys haluttuun prosessiin syntyy kirjoittamalla CTL-kanavaan
     halutun juttelukumppanin tunnus ja lukemalla sieltä vastaus, 0
     tai 1.  Jos vastaus on 0, sellaista prosessia ei ole eikä
     jutteluyhteys synny.  Jos vastaus on 1, jutteluyhteys on syntynyt
     ja juttelun voi aloittaa PEER-kanavalla.  Jos tätä yritetään, kun
     joku juttelu on jo käynnissä, CTL-kanava vastaa aina 0.

   Tehtävänäsi on kirjoittaa maanantain luennon CSP-kielellä MTA.
   Prosessisi siis välittää muiden viestejä, se ei itse luo niitä eikä
   se myöskään ota vastaan itselleen tarkoitettuja viestejä.
   Käytännössä siis prosessisi tulee odottaa, kunnes joku yrittää
   tarjota sille viestiä, jolloin prosessisi tulee ottaa se vastaan.
   Sitten prosessisi tulee yrittää välittää viesti muuttamattomana
   vastaanottajalleen.  Jos se tässä epäonnistuu, sen tulee yrittää
   lähettää alkuperäisen viestin lähettäjälle (jos sen tunnus ei ole 0
   eli "ei lähettäjää") virheilmoitusviesti (tämän lähettäjäkoodiksi
   laitetaan sitten 0 eli "ei lähettäjää").  Viestin sisällöksi
   laitetaan alkuperäisen viestin lähettäjän ja vastaanottajan
   tunnukset sekä alkuperäisen viestin sisältö.  Jos virheviestiä ei
   saada lähetettyä, voidaan viesti unohtaa.


Demossa läsnäolijoiden yhteinen, paikanpäällä kirjoitettu vastaus:

uid <- getUid();

(
PEER?remote_uid;
PEER!1;
PEER?from;
PEER?to;
PEER?length;
i <- 0;
(i<length -> (PEER?numbers[i]; i <- i+1))*;
PEER!1;
/* edelleenlähetys */
CTL!to;
CTL?ok;
if ok = 1 then 
    PEER!uid;
    PEER?ok;
    if ok = 1 then
        PEER!from
        PEER!to
        PEER!length
        i <- 0;
        (i<length -> (PEER!numbers[i]; i <- i+1))*;
        PEER?ok;
        ret <- ok;
    else
        ret <- 0;
    fi
else 
    ret <- 0
fi
/* virheilmoituksen palautus */
if ret = 0 then
    CTL!from
    CTL?ok
    if ok = 1 then 
        PEER!uid;
        PEER?ok;
        if ok = 1 then
            PEER!0
            PEER!from
            PEER!length+2
            PEER!from
            PEER!to
            i <- 0;
            (i<length -> (PEER!numbers[i]; i <- i+1))*;
            PEER?ok;
        fi
    fi
fi
)*


3. Tehtävänäsi on kirjoittaa Join Calculus Remix -kielellä (torstain
   luento) ns. printer spooler -ohjelma (portti), joka toimii
   seuraavasti:

     - Printteri prn lähettää porttiisi asynkronisen viestin
       printerReady(prn), kun se on valmis ottamaan vastaan uuden
       työn.

     - Käyttäjä usr lähettää porttiisi asynkronisen viestin
       job(usr, file), kun hän haluaa saada tiedoston file tulostettua.

     - Ohjelmasi tulee välittää tulostettava tiedosto jollekin
       vapaalle printterille prn synkronisella viestillä
       prn.print(file); jos vapaita printtereitä ei ole, joudutaan
       printterien vapautumista tietenkin odottamaan.

     - Kun tulostus on valmis, käyttäjälle usr tulee kertoa, että
       tiedosto file on tulostettu printeerillä prn käyttäen
       asynkronista viestiä usr.jobDone(file,prn)

   Rajapinnat:

    interface Printer:
       print(file : File)

    interface Spooler:
       async printerReady(printer : Printer)
       async job(usr : User, file : File)

    interface User:
       async jobDone(file : File, prn : Printer)


Oma vastaukseni (liian simppeli, koska tulostusjärjestystä ei päätetä):

SpoolerProgram implements Spooler:
    async job(usr : User, file : File) 
        | async printerReady(printer : Printer) ->
        printer.print(file);
        usr.jobDone(file, printer)