Un esecutore di specifiche logiche in tempo reale

Nei capitoli precedenti è stato mostrato come si possa applicare l'algoritmo di chiusura progressiva alle reti di inferenza temporale ottenendo, nel caso di inferenza causale, garanzia di tempo reale per una scelta opportuna del passo di discretizzazione. Punto debole di questo approccio risulta certamente la scelta di una funzione inferenza incompleta, scelta peraltro resa necessaria dalla complessità esponenziale di un qualunque algoritmo che aspiri alla completezza. Per superare questo problema si può tentare di caratterizzare l'insieme delle specifiche eseguibili, per cui cioè è garantita la produzione dell'intera storia di tutte le uscite per qualunque combinazione di storie di ingressi e condizioni iniziali, ma questa strada è ricca di difficoltà teoriche. Si possono individuare condizioni sufficienti per l'eseguibilità, ma quelle fino ad oggi trovate risultano molto restrittive e molte specifiche in e.etti eseguibili non le soddisfano. In mancanza di strumenti teorici adeguati, la sperimentazione può comunque fornire l'evidenza di un insieme di specifiche eseguibili sufficientemente ampio. Una volta completata la specifica del sistema desiderato, tecniche di dimostrazione automatica possono essere impiegate per verificare l'appartenenza delle uscite alla chiusura delle possibili combinazioni di ingressi e condizioni iniziali rispetto alle regole di inferenza implementate. Questo secondo problema è evidentemente pi`u semplice del precedente, in quanto non prescinde dalla struttura della particolare specifica.
La strada che è stata in e.etti percorsa ha richiesto l'implementazione di un esecutore di specifiche logiche conforme all'algoritmo teorico e la creazione di alcune reti di prova che si sono mostrate sempre capaci di produrre le uscite richieste a partire da segnali di ingresso casuali. Per la codifica è stato scelto il linguaggio C ANSI e tutte le funzioni esterne al programma appartengono alla libreria standard. Questo, assieme ad opportuni accorgimenti progettuali come la scelta del compilatore GNU, garantisce un'ottima portabilità sulle piattaforme pi`u diverse attraverso la semplice ricompilazione. La piattaforma preferita per lo sviluppo è stato un computer compatibile Intel con sistema operativo Linux, quest'ultimo scelto per le sue caratteristiche di robustezza e velocità che risultano fattori critici in molte applicazioni tempo reale. Per compiere i test necessari sono stati realizzati altri programmi di corredo, tra cui un generatore/visualizzatore di segnali casuali ed un compilatore da BTL al formato di descrizione della rete accettato dall'esecutore.
L'esecutore effettivamente implementato ha corrisposto alle attese. Può acquisire ingressi da file predeterminati al momento del lancio o progressivamente costruiti da altre applicazioni, man.tenendosi in attesa di nuova informazione sulla fine dei file medesimi e registrando in altri file le uscite inferibili a mano a mano che queste vengono determinate dall'algoritmo di chiusura progressiva. In particolare, i file di ingresso ed uscita hanno lo stesso formato e questo permette il lancio di pi`u esecutori in parallelo che si scambiano conoscenza in tempo reale. Dato che non è evidente in quale misura l'ipotesi di inferenza causale sia restrittiva ai fini dell'esecuzione di una specifica generica, il programma consente di scegliere se operare o meno sotto questa ipotesi.