1)Prima di tutto è necessario installare TLV:
il link da cui scaricare TLV è il seguente:
http://www.wisdom.weizmann.ac.il/~verify/tlv/
non posso mandarle il file perché dipende dalla piattaforma che usa.
2)Installarlo ed aggiungere una variabile d'ambiente TLV_RULES e farla puntare al file delle regole (rules) in allegato (solitamente si mette la cartella rules nella directory di installazione di TLV).
3)Scrivere i file XML dei servizi che compongono la community e l'XML del target service (dei file di prova sono già nella cartella tesina_Java/services, ed è lo stesso esempio presentato in tesina.pdf) in accordo alle regole in tesina_Java/assunzioni.txt.
4)Far partire il programma java lanciando il comando java Client.
5)Immettere, come suggerisce l'interfaccia grafica, il numero di servizi, il numero di azioni, il path degli XML dei servizi della community, il path del target service, ed il path di dove si vuole che il programmi salvi il file .smv risultato della computazione.
6)Dare a TLV come input il file .smv generato dal programma Java, lanciando il seguente comando dalla shell dei comandi:

path_installazione_TLV$ ./tlv comp-inv.pf percorso_file.smv

Nel file tesina.pdf ci sono gli output relativi alla composizione avvenuta con successo e a quella fallita.