Questa è una vecchia versione del documento!
Indice
S3 - Progetto finale
Testo e norme
Si trovano qui
FAQ
E' opportuno prevedere più sistemi SPARK?
Sì, almeno perché la parte di aggiornamento del codice di controllo non può aggiornare se stessa, per via della natura fortemente statica del linguaggio.
Come si crea una matrice di variabili di confine?
Dato che i package non sono oggetti di prim'ordine in SPARK, bisogna simulare la matrice con una funzione che mappa gli indici su uno specifico package. Per esempio, per le temperature, il secondo sensore del quarto appartamento sarà rappresentato da
package Temp_4_2; –# own in T; end package Temp_4_2;
e il package Edificio avrà una funzione getTemp(noSensore : … ; noAppartamento : … ) return Temperatura;
che conterrà un mostruoso case (peraltro generabile automaticamente), tra cui
… if noAppartamento = 4 and noSensore = 2 then ret := Temp_4_2.T else …
Dal punto di vista INFORMED, la situazione si presenta così:
Qual è il tipo dei consumi? Ovvero, qual è la dimensione del parametro teta?
Trattandosi di un sistema termodinamico, conviene misurare il consumo (cioè il lavoro fatto) in kilo-calorie (kcal). Si veda ad esempio la scheda 9 di questi appunti di fisica tecnica.
Quindi la dimensione di teta è kcal/Celsius. Il tipo, per semplificare, può essere un semplice intero. Il tipo dei consumi avrà quindi un'operazione di moltiplicazione per un intero che produce una temperatura (purché Celsius esporti un'operazione di creazione di una temperatura da un tipo primitivo opportuno).
Alternativamente, si può pensare a un solo package per tutte le dimensioni fisiche, in modo che le operazioni miste possano sfruttare la conoscenza comune delle rappresentazioni.