=====  S3 - Progetto finale =====

=== Testo  e norme ===
Il documento //aggiornato// si trova {{:magistralesicurezza:sss:requisiti_1_.pdf|qui}}.

=== FAQ ===

== C'è altro materiale didattico? ==

Sì, una versione aggiornata (in inglese) di parte dei lucidi è disponibile  
[[http://correctnessbycconstruction.wikispaces.com/|qui]]. 

Tutta la documentazione SPARK può essere scaricata da 
{{http://www2.adacore.com/wp-content/files/auto_update/sparkdocs-docs/index.html|qui}}, compreso il SImplifierManual, che è molto utile e ricco di esempi.


== Il numero di appartamenti e termosifoni è fissato a priori? ==

Sì, e conviene limitarsi a poche unità. 

== Conviene realizzare il codice per iterazioni? ==

Sì. Dato che il concentratore deve agire ogni ora, conviene prima risolvere il problema del singolo passo, e in un secondo tempo introdurre il ciclo. 

== 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ì:

{{:magistralesicurezza:sss:figura_faq.jpg|}}

== 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 [[http://www.valentiniweb.com/piermo/meccanica/mat/Impianti_di_climatizzazione_1.pdf|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. 
----