UniTO/todo.org

• VPC [21/23]
• Prog Mobile [2/5]
• Apprendimento Automatico [1/2]
• Tesi [3/9]

TODO VPC [21/23]

• Controlla good latex
• Uppaal muovi cartella file
• Rimuovi "Contents" da ogni .org
• chiedi della riduzione
• calcolo semiflussi come da mail
• chiedi dell'esame
• Es1: definizioni
• Rimuovi parte in cui parli di archi inibitori
• Chiedi a Daniel come da p-semiflows deadlock
• Chiedi a Daniel come da p-semiflows liveness
• spiega nelle relazioni che bounded se RS finito
• spiega nelle relazioni che bounded quando coperta da p-semiflows
• Vedi bisimulazione ed equivalenze in teoria analisi
• Che significa urgente in uppaal?
• Uppaal: x = 0 come guardia, non ==

• Teoria [1/13]

  • Hierarchy of equivalences
  • algebra.extra.lucca: internal/external choices
  • Observer e testing equivalence
  • Vedi bene legge conservazione token
  • Vedi bene fairness, liveness come formule?
  • Vedi da relazioni procedure dimostrazione deadlock
  • Impara equivalenze come le spiega lei
  • Formalizza algoritmo bisimulazione
  • Vedi slide 42 ltl: liveness, safety, fairness, anche in CTL
  • CTL e LTL: set operatori minimo per derivare altri
  • Manca CTL* ?
  • Pstate?
  • BDD e decision diagrams, tutto Amparore

• rete A, b, c, d [6/6]

  • Spiega p-t-semiflows analysis: deadlock e liveness, boundness
  • sulle slide, quando si chiede come deve decidere il master
  • Sistema screenshots di GSPN non tagliati
  • Controlla riduzione se hai fuso posti con archi uscenti
  • Rifai la riduzione e controlla fusione con archi uscenti
  • chiedi Daniel riduzione
• rete E, F -> Controlla sia finito

• Analisi [27/27]

  • clearpage su ultime immagini
  • Riduzione???
  • Inverti S14 e S13

  • Derivation graph errori [5/5]

    • Derivation graph 3.6: aggiungi label local_q R0
    • Derivation graph 3.6: aggiungi label tau R5
    • Derivation graph 3.6: aggiungi label critical_q R16
    • Derivation graph 3.6: aggiungi label local_q R20
    • Derivation graph 3.2: aggiungi label S14
  • Spiega perche` non hai usato process
  • Riguardo RGGMED4, non posso scrivere ltl equiparabile a ctl?
  • Specifica all'inizio che usi condizione piu` bassa per deadlock
  • Riformula liveness
  • Chiedi perche` non riesci a riprodurre i variable ordering mostrati da euristica

  • Algebra processi [3/3]

    • modellazione
    • rg vs dg
    • equivalenza e bisimulazione
  • 3.2, 3.5 rifai immagini e ctl con nuovi nomi spazi / transizioni
  • E` algebra CSP? Specifica
  • metti trace equivalence
  • Vedi necessita` di Sync e /
  • Controlla in 3.6 Starvation: nusmv no, greatspn si`
  • 3.6, deadlock: correttezza spiegazione della differenza greatspn nusmv?
  • 3.6, starvation: perche` nusmv con processi non ha starvation?
  • 3.6, inserisci controesempi dove necessario
  • 3.10: si puo` fare model checking senza unfolding?
  • 3.10: correggi GSPN: starvation false???
  • Correggi latex deadlock: G(wₚ|wp' → …)
  • Risolvi riduzione_eliminazione2.jpg
  • Risolvi \ttvar per #
  • non mette i file inclusi nel pdf :(
  • Cosa significa FAIRNESS running alla fine dei .smv
  • chiedi a lei di safety, liveness, fairness
  • mi sa non finito

• uppal, es 4 [4/4]

  • Galla`: su uppaal e` stato lui a scegliere i valori numerici_tempo
  • Come si prende intervallo attesa richiesto da Donatelli?
  • Fai intervallo attesa
  • Cambia nomi
• CSP: che significa sync?
• controlla esercizi nuovi
• Controlla bene e studia Symbolic Reachability Graph: perche` cosi` buono?
• Confrontare esercizi con Galla`

Prog Mobile [2/5]

• Api all songs
• relazione
• slides
• teoria
• account prof

Apprendimento Automatico [1/2]

• Scrivile per date di esame
• Richiedi date esame

Tesi [3/9]

• Rivedere inference rules di Gabriel e aggiustarle con le mie
• segreteria: tesi inglese
• Gatti: inglese
• Gatti: Coppo mio relatore

• correzioni Coppo [0/5]

  • esempi di esecuzione + test
  • esplicitare mio contributo a fine introduzione o abstract
  • spiegare meglio ruolo symbolic exec
  • Cosa manca per implementare al compilatore: passare da prototipo a cosa finita

  • Introduzione [2/4]

    • dovrebbe essere un po' ampliata e migliorata verso la fine
    • snellendo un po' la presentazione formale.
    • spiegando meglio il ruolo della symbolic interpretation
    • Perche' ci si concentra sulla traduzione dei pattern?
• riferimenti bibliografici
• paper pattern matching C++
• Gabriel: finisci
• SimpleEquiv Latex
• Boolean result o Yes|No? (Inference rules)
• Mostra altri casi per la empty rule
• Adatta i cambiamenti al paper
• Esempio trimming
• Trimming e resto: mi sa che usi left e right male
• Spiega perche` trimming non simmetrico
• Spiega meglio le guards on equivalence checking

HALP HALP!