Supponiamo di avere un'azione "a". Allora a-negato è il complementare di "a".

In altre parole, (esempio stupido) se io ti stringo la mano (chiamiamo questa azione "a" tu ti fai stringere la mano, e quindi fai ¬a (con ¬a indico a negato).

In realtà la situazione è un po' diversa in CCS: (esempio meno stupido)

supponiamo di avere due termini CCS, A e B.
Supponiamo di avere un'azione "a", e che la situazione sia:

a.A | ¬a.B

cioè A compie "a" e B compie "¬a", in parallelo.
Allora puoi avere 3 situazioni:
1) A compie "a": a.A | ¬a.B --> A | ¬a.B
2) B compie "¬a": a.A | ¬a.B --> a.A | B
3) A compie "a" e B compie "¬a" contemporaneamente: allora si dice che i due processi si stringono la mano (si parla in effetti di handshaking), e compiono un tau. Il punto 3 quindi diventa: a.A | ¬a.B --> A | B.

Spero di essere stato chiaro e soprattutto di non aver fatto errori.
Se ci sono errori ditelo, senò magari li rifaccio al compito!

[size=2]PS: quello che ho scritto è trattato a pag. 60 delle dispense di Pettorossi "Elements of concurrent programming".[/size]

Ok Nash, quello che dici tu è sicuramente giusto.
La situazione è un po' meno ovvia quando dobbiamo scrivere in CCS processi un po' più complessi, vedi per esempio la dimostrazione di correttezza dell'Alternating Bit Protocol.
Considera la descrizione del Receiver B(b) nello schema semplificato:
B(b)=Mam.if m2=b then (¬outC)m1.B'(¬b) else B'(b)
B'(b)=(¬Mb)¬b.B(b)+(¬Mb)error.B(b)
Il ¬ si dovrebbe riferire solo al bit, ma per capirci ¬Mb = Mb "negato";
La seconda equazione dovrebbe indicare il fatto che il canale può trasmettere il messaggio giusto oppure un errore.
Ora, (¬Mb)¬b significa: "¬b viene spedito tramite il canale Mb" giusto?
Ho cercato un po' in giro su google, quando c'è la barra si parla di sincronizzazione dell'input, forse mi sono confuso un po' con questo.
Speriamo di arrivare a una conclusione prima di Martedì!

un'azione diretta (senza barra) indica un'azione che il processo riceve dall'esterno (la ricezione di un input, e infatti nel value passing CCS
a?x->p che indica proprio la ricezione di un input dal canale a viene anche scritto come ax.p) mentre l'azione con la barra indica un'azione che il processo compie sul mondo esterno (scrittura di un output, ed infatti
a!x->p è scritto come ¬ax.p); ¬(Mb)b significa quindi "scrivi b in Mb" e (Mb)b è invece "leggi b da Mb"; questo dovrebbe spiegare anche il tau, che indica la coppia di azioni input-output: se ho un processo A=¬(Mb)b.A1 e un processo B=(Mb)b.B1 allora ho che il loro paralleo A|B fa tau e va in A1|B1 cioè A e B si parlano e cambiano stato (in questo senso tau sincronizza i processi ed è un'azione interna).. questo è quello che ho capito io

avete studiato ciò sulle sue dispense in english?

Si, sembra che qualcosa di buono sia uscito fuori

Decifrazione di dispense+sue spiegazioni

ma dite che può bastare quello che sta sulle sue dispense?
Nn sono proprio chiarissime.. cioè,io penso di aver più o meno capito ma mi rimane tutto così astratto.. bhò!!
Cambiando argomento: ma l'UML dove cavolo si deve studiare?!?
Thanks

Si, la maggior parte degli argomenti di esame sono nelle dispense.
Se le hai scaricate appena il prof le ha messe sul sito, riscaricale, c'erano un po' di errori che sono stati corretti.
In effetti la trattazione è molto formale quindi non facilmente digeribile, ma se ti ci metti e le rileggi un po' di volte alla fine si capisce.
Per l'UML ci sono le dispense sulla lezione di Fabio Lecca sul sito del prof, anche se pure quelle un po' confusionarie, e cmq Google vince sempre
Che Dio ce la mandi buona Mercoledì, se il compito rimane più o meno quello dell'altro appello è abbastanza fattibile.

Grazie Arbal
Ora vado a fare una ricerca in rete..