-
Notifications
You must be signed in to change notification settings - Fork 0
/
Copy pathTODO
62 lines (40 loc) · 2.43 KB
/
TODO
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
# Todos
## List
- aggiungere tutto neldàla label così si feedback all'utente e comunque usare le additional info nelle gv
- unbounded send (*stella di klene nei cicli di send)
- fare il filtro solo sulle send e azzerarlo quando avviene una receive (tutte le receive e tutti i processi) -> fatto ma implementando la unbounded send dovrei poter eliminare questa cosa
- lasciare numerini nelle lv -> fare check nelle gv quando si ripassa dalla stessa spawn
- dividere localview data from wip_lv data
- se c'è un loop che cambia variabili -> perdere la variabile (unknown) così alla secoda receive matcha più (o tutte) branch (hello.erl example)
## appunti temi diversi
### Spawn in global view
Nella add global state fare andare avanti i processi spawnati! dare errore ma comunque provare a produrre qualcosa
(fare un test con due processi paralleli, uno che registra un processo e uno che invia un messaggio a quello registrato)
### fsa minimize
prima: nella gv fare la valutazione del ptmt su i dati passati nella additional_info
- usare nella gv le versioni non minimizzate delle lv
- chiedere all'utente se salvare la totale o la minimizzata
-> aggiungere valutazione nella gv di tutti i possibili edge
## fix mutual recurtion
aggiungere una stack di chiamate alla struct wip_lv
se si aggiungono le variabili locali si implementa anche una sorta di scope
## Notes 8/5
show one possible execution -> creare una cartella con tutte le possibili singole esecuzioni
preserve orders of messages in gv
mutual recursion will diverge (we needs to at least detect it -> keep a trace of the function call and stop)
controllare minimizzazione e informazioni negli edge (attaccarli agli id e non alle label, come? si uniscono le informazioni in fase minimizzazione)
x prox volta
tabella dei simboli con le funzioni poi variabili
missmatch sulla ricezione nella coreografia globale
? quando non conosco a chi inviare un dato
se dichiaro come partecipante non posso usarlo come funziona normale (dare warning).
## Label global view
Migliorare le label della global view:
- visualizzare meglio i dati inviati
- usare le additional info
## Mettere come opzione la history dei messaggi
Inserire un config file?
fare il sito come https://soter.mpi-sws.org/
se non vengono fatte overapprossimazioni -> allora abbiamo una coreografia esatta
se abbiamo fatto delle overapprossiamzioni -> allora non siamo sicuri di niente
idea: aggiungere transizione erronea verso un nuovo stato.