Tesi di laurea triennale sulla programmazione a vincoli

Panoramica

Da studente di informatica alla triennale, la mia ricerca è partita da una domanda pratica: quando un simulatore accumula molte condizioni possibili, come si fa a fargli smettere di riconsiderare quelle che non possono più verificarsi? Ho sviluppato e valutato per HydLa un metodo che sfrutta la direzione in cui un valore sta cambiando per togliere dalla ricerca le condizioni ormai inutili. Nel modello di riferimento il tempo totale di simulazione si è ridotto a circa la metà.

Questo lavoro è una delle prime fondamenta della mia filosofia progettuale. La programmazione a vincoli mi ha insegnato che i risultati complessi non vanno sempre specificati direttamente: possono emergere da uno spazio di regole, priorità e confini definito con cura. È quel modo di pensare a reggere oggi il mio modo di progettare a partire dai vincoli nell'era dell'IA: progettare le condizioni entro cui un sistema generativo è libero di agire.

Abstract

HydLa è un linguaggio di modellazione per sistemi ibridi: sistemi in cui il cambiamento continuo e gli eventi discreti interagiscono. La sua impostazione basata sui vincoli permette di descrivere questi sistemi in modo conciso e di simularli con grande precisione. Il prezzo è che, in un modello grande, il simulatore può continuare a controllare un numero enorme di regole condizionali anche quando alcune hanno smesso di avere senso.

Questa ricerca ha proposto di ridurre dinamicamente quei vincoli con guardia. Riconoscendo un comportamento monotono — un valore che continua a muoversi in una sola direzione — il simulatore può stabilire che certe guardie non diventeranno mai vere in futuro e smettere di controllarle senza rischi. L'approccio si è rivelato particolarmente efficace in un modello con molti oggetti sorvegliati allo stesso modo, dove il tempo di esecuzione misurato è sceso a circa la metà di quello originale.

1. Introduzione

Un sistema ibrido unisce comportamento continuo ed eventi discreti. Una pallina che rimbalza è un esempio semplice: posizione e velocità cambiano con continuità finché è in aria, ma l'istante in cui tocca una superficie crea un evento discreto che ne cambia la direzione. Termostati, veicoli e robot contengono versioni ben più gravide di conseguenze della stessa miscela.

HydLa consente di descrivere questi sistemi con vincoli matematici e logici, invece di scrivere un'unica sequenza procedurale. Il suo simulatore, HyLaGI, esegue calcoli simbolici senza errori di arrotondamento e sa lavorare con parametri incerti. Questa espressività crea però un problema di scala: quando un modello contiene molte regole che si attivano solo in condizioni particolari, il simulatore deve chiedersi in continuazione se ciascuna condizione possa essere la prossima a verificarsi.

2. Vincoli con guardia nella simulazione

Un vincolo con guardia è una regola che si attiva solo quando la sua condizione di guardia è soddisfatta. Nel modello di riferimento qui sopra ogni segmento della superficie ha la propria regola: se la pallina arriva a quota zero mentre la sua posizione orizzontale cade dentro quel segmento, si applica la regola del rimbalzo. Dividere la superficie in più parti dà quindi al simulatore più guardie da ispezionare.

L'esperimento ha fatto variare il numero di segmenti da 10 a 200. Il simulatore originale rallentava all'incirca come il quadrato di quel numero. La cosa conta al di là dell'esempio giocattolo: un modello più grande può rappresentare molti oggetti fisici, regioni di contatto o eventi possibili esattamente in questa forma sorvegliata.

3. Dove sta il collo di bottiglia

La profilazione ha mostrato che il rallentamento non era distribuito in modo uniforme nel simulatore. Con 100 segmenti di superficie, il 96% del tempo di esecuzione misurato veniva speso in FindMinTime, l'operazione che cerca il primo evento possibile successivo. Rivalutava di continuo le guardie di tutti i vincoli candidati.

Quel risultato ha reso specifico l'obiettivo dell'ottimizzazione: ridurre il numero di guardie che FindMinTime deve considerare, preservando esattamente lo stesso comportamento simulato.

4. Riduzione dei vincoli con guardia

Si immagini una pallina che scende rimbalzando una scala. Una volta che la pallina ha superato un gradino e prosegue in avanti, quel gradino non può più influenzarla. Chi guarda il disegno scarta subito i gradini rimasti indietro; l'algoritmo originale continuava a controllarli tutti, uno per uno.

La parte difficile è dimostrare che una guardia scartata non servirà più in seguito. Rimuoverla solo perché adesso è falsa potrebbe produrre in silenzio un risultato sbagliato qualora tornasse vera. La proposta si appoggia perciò alla monotonia: alla garanzia che una variabile continui a crescere, o continui a decrescere, lungo un intervallo di tempo.

4.1 Approccio alla monotonia uniforme

Il primo approccio vale quando una variabile si muove in una sola direzione per l'intera simulazione. Nel modello a superficie divisa la posizione orizzontale della pallina cresce sempre. Una volta superato un segmento, la condizione di quel segmento non può più essere soddisfatta. Le tecniche di model checking permettono di stabilire questa proprietà prima della simulazione, così le guardie ormai inutili possono essere rimosse senza rischi mentre l'esecuzione procede.

4.2 Approccio alla monotonia alternata

Molti sistemi reali non si muovono per sempre in una sola direzione. Una variabile può crescere, invertirsi e poi decrescere. L'articolo ha quindi delineato un secondo approccio: partire da una direzione ipotizzata, sorvegliare quell'ipotesi con delle asserzioni e far ripartire la logica di riduzione dal punto in cui la direzione cambia. Le guardie rimosse per un intervallo monotono vengono ripristinate quando comincia il successivo.

5. Risultati sperimentali

Ho implementato l'approccio della monotonia uniforme e l'ho valutato con il modello a superficie divisa. Sia l'algoritmo originale sia quello proposto impiegavano comunque più tempo al crescere del numero di segmenti, ma la versione proposta faceva sistematicamente meno lavoro. Confrontando le curve interpolate, il coefficiente di grado massimo è sceso da 1,1463 a 0,6083; per questo caso di riferimento il tempo totale di simulazione si è all'incirca dimezzato.

Il risultato non sostiene che ogni modello HydLa diventi due volte più veloce. Mostra dove il metodo aiuta: nei modelli con molti oggetti sorvegliati e una direzione di cambiamento dimostrabile, dove le guardie diventano definitivamente irrilevanti durante l'esecuzione.

6. Conclusioni e lavoro futuro

La ricerca ha mostrato che a rendere più efficiente una simulazione può essere la conoscenza del modello, non soltanto un calcolo di basso livello più veloce. Usando la monotonia per riconoscere quali possibilità sono ormai impossibili, HyLaGI può restringere l'insieme dei vincoli attivi senza cambiare il risultato.

L'esperimento realizzato copriva la monotonia uniforme. L'articolo ha lasciato due direzioni per il seguito: valutare il metodo basato sulle asserzioni per il comportamento alternato e usare invarianti diversi dalla monotonia per individuare altri vincoli rimovibili senza rischi.