diff --git a/Makefile b/Makefile new file mode 100644 index 0000000..6669418 --- /dev/null +++ b/Makefile @@ -0,0 +1,45 @@ +## Makefile + +CC = gcc +FLAGS = -Wall -Werror -m64 -DNDEBUG +FLAGS_F = -m64 +OPTFLAGS = -O2 + +all: verifier + +makefile.dep: *.[ch] + for i in *.c; do gcc -MM "$${i}"; done > $@ + +include makefile.dep + +%.o: %.c Makefile + $(CC) $(FLAGS) $(OPTFLAGS) -c $< + +verifier: anread.o anproc.o antclass.o anpsmod.o y.tab.o lex.yy.o dbm.o + $(CC) $(FLAGS) $(OPTFLAGS) anread.o anproc.o antclass.o anpsmod.o lex.yy.o y.tab.o dbm.o -o verifier + +lex.yy.o: lex.yy.c + $(CC) $(FLAGS_F) $(OPTFLAGS) -c lex.yy.c + +lex.yy.c: verifier.l y.tab.c + lex verifier.l + +y.tab.o: y.tab.c + $(CC) $(FLAGS_F) $(OPTFLAGS) -c y.tab.c + +y.tab.c: verifier.y + yacc -d verifier.y + +dbm_testing: + $(CC) $(FLAGS) $(OPTFLAGS) -o dbm_testing dbm_testing.c dbm.o + +# clean lex&yacc +cleanly: + rm -f lex.yy.c y.tab.c y.tab.h y.output + +clean: cleanly + rm -f *.o verifier dbm_testing + +test: verifier + ./verifier < netfiles/tgc.aut + diff --git a/TODO b/TODO new file mode 100644 index 0000000..62604c6 --- /dev/null +++ b/TODO @@ -0,0 +1,25 @@ +Do poprawy (optymalizacje): +- sposob zwracania przez f-cje prod_loc_acts akcji wykonalnych z okr. + lokacji jest tragiczny i jest paskudna strata pamieci i czasu ;) + +- z kazda aktualizacja DBM przeliczam PK, co moze sie okazac bez sensu + +- przy obliczaniu pre_e wystepuje powtarzajace sie guard(e) n I(s), + ktore jest niezmienne dla dodanego przejscia. Mozna zapisac + obliczony wynik wraz z zapisanym przejsciem e. Dodatkowo mozna + traktowac NULL jak strefe bez ograniczen, co pozwoli nam + przyspieszyc obliczenia i jednoczesnie nie zuzyje zbyt wiele pamieci + (zakladajac ze nie wszedzie sa okreslone niezmienniki/guardy). + +- sprawdzanie pustosci przeciecia dwoch stref bez alokowania zadnych + DBM-ow, np. wykorzystywac zawsze ten sam tymczasowy DBM + +- tam gdzie przekazujemy argument do funkcji wskazujacy na zbior + reachstable, moze warto wprowadzic zmienne globalne? Z punktu + widzenia zlozonosci rozni sie to tylko o pewna stala. + +- Sprawdzanie czy Z n Z' = Z mozna zrealizowac w wydajniejszy sposob, bo + nie potrzeba obliczac dokladnego wyniku, tylko sprawdzac czy minimum + jest rowne temu co jest w Z. Odpada wtedy alokowanie dodatkowych DBM-ow + i zwalnianie ich. + diff --git a/anmacro.h b/anmacro.h new file mode 100644 index 0000000..003f0d3 --- /dev/null +++ b/anmacro.h @@ -0,0 +1,34 @@ +#ifndef _INC_ANMACRO_H_ +#define _INC_ANMACRO_H_ + +#include +#include +#include + +#define FERROR(s) \ +{ \ + printf("%s (function %s), line %d: %s\n", __FILE__, __func__, __LINE__, s); \ + exit(1); \ +} + +#define CLOCK_0_NAME "0" + +#define CONSTR_LT 0 +#define CONSTR_LE 1 +#define CONSTR_MARK_TERM(a) ((a)->l_clk = -1) /* oznaczanie ograniczenia jako terminujace liste */ +#define CONSTR_IS_TERM(a) ((a)->l_clk == -1) /* sprawdzanie czy org. jest terminujace */ + +#define LOC_INITIAL (1 << 0) +#define LOC_COMMITED (1 << 1) +#define LOC_URGENT (1 << 2) +#define LOC_IS_INITIAL(a) ((a).type & LOC_INITIAL) +#define LOC_IS_COMMITED(a) ((a).type & LOC_COMMITED) +#define LOC_IS_URGENT(a) ((a).type & LOC_URGENT) + +#define ACT_URGENT (1 << 0) +#define ACT_IS_URGENT(a) ((a).type & ACT_URGENT) + +#define TRANS_P(x, y, a, b) &(x)[((a)*(y)+(b))] /* pobieranie listy przejsc z lokacji a do b */ +#define TRANS(x, y, a, b) (x)[((a)*(y)+(b))] + +#endif /* !_INC_ANMACRO_H_ */ diff --git a/anproc.c b/anproc.c new file mode 100644 index 0000000..87e1df3 --- /dev/null +++ b/anproc.c @@ -0,0 +1,892 @@ +/** anproc.c **/ + +/* + * Przetwarzanie struktur stworzonych podczas wczytywania sieci automatow, + * tworzenie produktu na podstawie sieci automatow. + */ + +#include +#include +#include +#include +#include "anproc.h" +#include "antypes.h" +#include "anmacro.h" +#include "macro.h" +#include "dbm.h" + +static Aut *aut = NULL; +static Aut_idx naut = 0; + +static Clock_idx pclocks_cnt = 0; /* zegary w automacie produktowym */ +static ProdClock *pclocks_map; +static Clock_idx **rpclocks_map; + +static Act *act = NULL; +Act_idx nact = 0; + +DBM_idx dbm_size = 0; +DBM_elem *zeroDBM = NULL; +ProdLoc_set *init_loc_set = NULL; + +Property_set *ppts = NULL; + +/* + * Inicjalizacja przetwarzania sieci + * + * F-cja ustawia wartosci zmiennych globalnych, zeby uniknac przekazywania niektorych argumentow + */ +void +net_init(AutNet *an) +{ + idx_t i; + + /* automaty */ + aut = an->aut; + naut = an->naut; + + /* akcje */ + act = an->act; + nact = an->nact; + + ppts = an->ppts; + + /* zliczamy zegary ze wszystkich automatow skladowych */ + for (i = 0; i < naut; i++) + { + pclocks_cnt += aut[i].nclks; + } + dbm_size = pclocks_cnt+1; + + zeroDBM = dbm_init_zero(dbm_size); + + prod_clocks_mkmap(); + +#ifdef VERBOSE + printf("Liczba zegarow w automacie produktowym = %d\n", pclocks_cnt); +#endif +} + +void +prod_clocks_mkmap(void) +{ + Clock_idx i, j, k; + + pclocks_map = smalloc(sizeof(ProdClock)*pclocks_cnt); /* produktowy -> skladowy */ + rpclocks_map = smalloc(sizeof(Clock_idx *)*naut); /* skladowy -> produktowy */ + + k = 0; + for (i = 0; i < naut; i++) + { + rpclocks_map[i] = smalloc(sizeof(Clock_idx)*aut[i].nclks); + for (j = 0; j < aut[i].nclks; j++) + { + pclocks_map[k].par_aut = i; + pclocks_map[k].par_idx = j+1; /* ze wzgledu na x_0 */ + rpclocks_map[i][j] = k+1; + k++; + } + } +} + +void +prod_clock_maps_free(void) +{ + idx_t i; + + free(pclocks_map); + + for (i = 0; i < naut; i++) + { + free(rpclocks_map[i]); + } + free(rpclocks_map); +} + +/* + * Konwersja indeksu zegara z automatu skladowego + * do indeksu zegara z automatu produktoweg + */ +Clock_idx +prod_clock_idx2pidx(Aut_idx ai, Clock_idx ci) +{ + assert(ai < naut); + assert(ci-1 < aut[ai].nclks); + + if (ci == 0) + return 0; + else + { + assert(rpclocks_map[ai][ci-1] < dbm_size); + return rpclocks_map[ai][ci-1]; + } +} + +/* + * Indeks produktowego zegara -> indeks skladowego + */ +ProdClock +prod_clock_pidx2idx(Clock_idx ci) +{ + if (ci == 0) + { + ProdClock r; + r.par_aut = 0; + r.par_idx = 0; + return r; + } + else + { + return pclocks_map[ci-1]; + } +} + + +/* + * Okreslanie poczatkowej lokacji produktowej + */ +Loc_idx * +prod_loc_initial(void) +{ + idx_t i; + Loc_idx *initial; + + initial = smalloc(sizeof(Loc_idx)*naut); + + for (i = 0; i < naut; i++) + initial[i] = aut[i].init_loc; + + return initial; +} + +/* + * Kopiowanie okreslonej lokacji produktowej + */ +Loc_idx * +prod_loc_copy(Loc_idx *prod_loc) +{ + Loc_idx *copy; + + copy = smalloc(sizeof(Loc_idx)*naut); + (void)memcpy(copy, prod_loc, sizeof(Loc_idx)*naut); + + return copy; +} + +/* + * Pobieranie listy akcji POTENCJALNIE wykonalnych z lokacji produktowej + */ +bool * +prod_loc_acts(Loc_idx *prod_loc) +{ + idx_t i, j; + Trans_set *t; + bool *used_acts; + + used_acts = smalloc_zero(sizeof(bool)*nact); + + for (i = 0; i < naut; i++) + { + for (j = 0; j < aut[i].nloc; j++) + { + for (t = TRANS(aut[i].trans, aut[i].nloc, prod_loc[i], j); + t != NULL; + t = t->next) + { + used_acts[t->act] = true; + } + } + } + + return used_acts; +} + +/* + * Wyswietlanie lokacji produktowej + */ +void +prod_loc_show(Loc_idx *prod_loc) +{ + idx_t i; + + printf("( "); + for (i = 0; i < naut; i++) + printf("%s ", get_loc_name(aut[i].loc, prod_loc[i])); + printf(")"); +} + +/* + * Dodawanie lokacji produktowej do zbioru + */ +ProdLoc_set * +prod_loc_set_add(Loc_idx *prod_loc, DBM_elem *inv, ProdLoc_set **root, ProdLoc_set **cur) +{ + ProdLoc_set *new; + + new = smalloc(sizeof(ProdLoc_set)); + new->loc = prod_loc; + new->inv = inv; + new->src_locs = NULL; + new->dst_locs = NULL; + new->classes = NULL; + new->trans_complete = false; + + prod_loc_set_raw_add(new, root, cur); + + return new; +} + +/* + * Dodawanie lokacji produktowej do zbioru w postaci surowej + */ +void +prod_loc_set_raw_add(ProdLoc_set *new, ProdLoc_set **root, ProdLoc_set **cur) +{ + new->next = NULL; /* nie wiadomo co tam bylo, a dodajemy na koncu */ + + if (!*root) + *root = new; + else + (*cur)->next = new; + *cur = new; +} + +/* + * Sprawdzanie zawierania lokacji produktowej przez zbior + */ +bool +prod_loc_set_is_in(Loc_idx *prod_loc, ProdLoc_set *root) +{ + ProdLoc_set *cur; + + for (cur = root; cur; cur = cur->next) + { + if (memcmp(cur->loc, prod_loc, sizeof(Loc_idx)*naut) == 0) return true; /* znaleziono */ + } + + return false; /* nie znaleziono */ +} + +/* + * Sprawdzanie zawierania lokacji produktowej przez zbior + */ +ProdLoc_set * +prod_loc_set_getp(Loc_idx *prod_loc, ProdLoc_set *root) +{ + ProdLoc_set *cur; + + for (cur = root; cur; cur = cur->next) + { + if (memcmp(cur->loc, prod_loc, sizeof(Loc_idx)*naut) == 0) return cur; + } + + return NULL; +} + +/* + * Wyciaganie (wybieranie i usuwanie) elementu ze zbioru + */ +ProdLoc_set * +prod_loc_set_raw_pick(ProdLoc_set **root) +{ + ProdLoc_set *picked; + + picked = *root; /* bierzemy korzen */ + + /* jesli byl korzen, to mial ustawione pole next, ktore wskazuje na nowy korzen */ + if (*root) + *root = picked->next; + + return picked; +} + +/* + * Wyswietlanie zbioru lokacji produktowych + */ +void +prod_loc_set_show(ProdLoc_set *root) +{ + ProdLoc_set *cur; + + for (cur = root; cur; cur = cur->next) + { + prod_loc_show(cur->loc); + printf("\ninv:\n"); + dbm_print(cur->inv, dbm_size); + } + printf("\n"); +} + +/* + * Pelne zwalnianie pamieci przydzielonej na zbior lokacji produktowych + * (pelne - wraz z lokacjami produktowymi). + */ +void +prod_loc_set_free(ProdLoc_set *root) +{ + ProdLoc_set *cur; + + for (cur = root; cur; ) + { + ProdLoc_set *tmp = cur; + + cur = cur->next; + free(tmp->loc); + dbm_destroy(tmp->inv); + free(tmp); + } +} + +/* + * Dodawanie przejscia do lokacji + */ +void +trans_add(ProdLoc_set *src_loc, ProdLoc_set *dst_loc, ProdTrLoc_set *prtl) +{ + ProdTrans_set *new_trans; + DstLoc_set *cur_dst_loc; + DstLoc_set *dst_group = NULL; + + new_trans = smalloc(sizeof(ProdTrans_set)); + new_trans->act = prtl->act; + new_trans->guard = prtl->guard; + new_trans->clocks = prtl->clocks; + new_trans->next = NULL; + + /* + - zgrupowane wszystkie przejscia do jednej lokacji docelowej + - dodajac nowe przejscie szukamy grupy do ktorej nalezy okreslone + przejscie dodac + - jesli nie ma jeszcze takiej grupy, to ja tworzymy + - z grupa zwiazany jest wskaznik na lokacje docelowa + (dokladnie, element zbioru lokacji ja przetrzymujacy) + */ + + /* szukamy grupy przejsc prowadzacych do dst_loc */ + cur_dst_loc = src_loc->dst_locs; + while (cur_dst_loc) + { + /* sprawdzamy czy znalezlismy cur_dst_loc == dst_loc */ + if (cur_dst_loc->loc_set == dst_loc) + { + dst_group = cur_dst_loc; + break; + } + + if (!cur_dst_loc->next) + break; + else + cur_dst_loc = cur_dst_loc->next; + } + + /* + * jesli dst_group jest nieustawione, to nie ma jeszcze takiej + * lokacji docelowej i trzeba ja dodac + */ + if (!dst_group) + { + SrcLoc_set *new_src_loc; + + dst_group = smalloc(sizeof(DstLoc_set)); + dst_group->loc_set = dst_loc; + dst_group->trans = NULL; + dst_group->last_trans = NULL; + dst_group->next = NULL; + + /* + * naszym dst_locs_LAST jest cur_dst_loc (gdy dst_group == NULL) + */ + if (!src_loc->dst_locs) + src_loc->dst_locs = dst_group; + else + { + assert(cur_dst_loc != NULL); + cur_dst_loc->next = dst_group; /* Segfault! */ + } + + new_src_loc = smalloc(sizeof(SrcLoc_set)); + new_src_loc->loc_set = src_loc; + new_src_loc->trans = new_trans; /* zapisujemy tylko raz (i tylko pierwszy element) */ + new_src_loc->next = NULL; + + /* + * zakladamy ze jesli nie udalo sie znalezc istniejacej grupy to + * w lokacji docelowej tez nie ma informacji o tej lokacji zrodlowej + */ + if(!dst_loc->src_locs) + dst_loc->src_locs = new_src_loc; + else + dst_loc->last_src_loc->next = new_src_loc; + dst_loc->last_src_loc = new_src_loc; + + } + + if (!dst_group->trans) + dst_group->trans = new_trans; + else + dst_group->last_trans->next = new_trans; + dst_group->last_trans = new_trans; + +} + + +/* + * Pobieranie wskaznika na przejscia z lokacji src do lokacji dst + */ +ProdTrans_set * +trans_get(ProdLoc_set *src, ProdLoc_set *dst) +{ + DstLoc_set *cur_dstloc; + + for (cur_dstloc = src->dst_locs; cur_dstloc; cur_dstloc = cur_dstloc->next) + { + if (cur_dstloc->loc_set == dst) + { + return cur_dstloc->trans; + } + } + + return NULL; +} + +/* + * Sprawdzanie zawierania elementu zbioru lokacji produktowych + * przez zbior lokacji zrodlowych + */ +bool +ploc_in_src_locs(ProdLoc_set *prod_loc, SrcLoc_set *root) +{ + SrcLoc_set *cur; + + for (cur = root; cur; cur = cur->next) + { + if (cur->loc_set == prod_loc) return true; /* znaleziono */ + } + + return false; /* nie znaleziono */ +} + +void +trloc_set_free(TrLoc_set **trloc) +{ + idx_t i; + TrLoc_set *tmp; + + for (i = 0; i < naut; i++) + for (tmp = trloc[i]; tmp != NULL; tmp = tmp->next) + free(tmp); + + free(trloc); +} + +/* + * Sprawdzanie czy lista ograniczen zawiera jakies rzeczywiste ograniczenia + */ +bool +constr_nonempty(Constr *c) +{ + if (c) + /* lista jest niepusta */ + if (CONSTR_IS_TERM(c)) + /* pierwsze ogr. jest terminujace, czyli nic nie ma */ + return false; + else + /* jest przynajmniej jedno ogr. */ + return true; + else + return false; +} + +/* + * Wprowadzanie ograniczen z listy c do DBM-a p + */ +void +constr2dbm(Aut_idx ai, DBM_elem *p, Constr *c) +{ + if (!c) return; + + for (; !CONSTR_IS_TERM(c); c++) + { + DBM_idx i, j; + + i = prod_clock_idx2pidx(ai, c->l_clk); + j = prod_clock_idx2pidx(ai, c->r_clk); + + switch (c->rel) + { + case CONSTR_LE: + dbm_constr_le(p, dbm_size, i, j, c->val); + break; + + case CONSTR_LT: + dbm_constr_lt(p, dbm_size, i, j, c->val); + break; + + default: + FERROR("Unknown relation"); + break; + } + + dbm_canon1(p, dbm_size, i, j); + } +} + +/* + * Zbieranie z automatow skladowych zegarow z indeksami automatu produktowego + */ +void +clocks_collect(ClockIdx_set **root, ClockIdx_set **cur, Aut_idx ai, Clock_idx *clks, Clock_idx nclks) +{ + idx_t i; + + for (i = 0; i < nclks; i++, clks++) + { + ClockIdx_set *n = smalloc(sizeof(ClockIdx_set)); + + n->idx = prod_clock_idx2pidx(ai, *clks); + assert(n->idx > 0); + n->next = NULL; + + if (!*root) + *root = n; + else + (*cur)->next = n; + *cur = n; + } +} + +/* + * Zwalnianie pamieci zaalokowanej przez clocks_collect + */ +void +colclocks_free(ClockIdx_set *elem) +{ + ClockIdx_set *next; + + while (elem) + { + next = elem->next; + free(elem); + elem = next; + } +} + +/* + * Pobieranie niezmiennika dla okreslonej lokacji produktowej w post. DBM. + */ +DBM_elem * +prod_loc_inv(Loc_idx *ploc) +{ + DBM_elem *p = NULL; + idx_t i; + + p = dbm_init(dbm_size); + + for (i = 0; i < naut; i++) + { + constr2dbm(i, p, aut[i].loc[ploc[i]].inv); + } + + return p; +} + +/* + * Pobieranie niezmiennika dla okreslonej lokacji produktowej w post. DBM. + * Jesli nie ma ograniczen, to DBM == NULL. + */ +DBM_elem * +prod_loc_inv0(Loc_idx *ploc) +{ + DBM_elem *p = NULL; + idx_t i; + + for (i = 0; i < naut; i++) + { + Constr *cinv; + + cinv = aut[i].loc[ploc[i]].inv; + + /* DBM alokowany tylko jak jest co do niego wrzucic */ + if (!p && constr_nonempty(cinv)) p = dbm_init(dbm_size); + + constr2dbm(i, p, cinv); + } + + return p; /* p == NULL jesli nie ma ograniczen */ +} + +/* + * Znajdowanie przejsc z okreslona akcja mozliwych z danej lokacji + * produktowej wraz z lokacjami produktowymi do ktorych prowadza. + */ +ProdTrLoc_set * +prod_loc_succ(Loc_idx *src_ploc, Act_idx a) +{ + idx_t i, j; + Trans_set *t; + + TrLoc_set **trloc; /* posrednia struktura do ktorej bedziemy zbierac przejscia i lokacje docelowe */ + idx_t *ntrloc; /* liczniki odnalezionych przejsc w poszczegolnych automatach */ + + trloc = smalloc_zero(sizeof(TrLoc_set *)*naut); + ntrloc = smalloc_zero(sizeof(idx_t)*naut); + + for (i = 0; i < naut; i++) + { + if (aut[i].uact[a]) /* jesli akcja jest w zbiorze akcji automatu, to idziemy dalej */ + { + + for (j = 0; j < aut[i].nloc; j++) + { + for (t = TRANS(aut[i].trans, aut[i].nloc, src_ploc[i], j); + t != NULL; t = t->next) + { + + if (t->act == a) /* znalezlismy przejscie z poszukiwana akcja */ + { + TrLoc_set *n; + + ntrloc[i]++; /* znaleziono przejscie */ + + n = smalloc(sizeof(TrLoc_set)); + n->loc = j; + n->trans = t; + n->next = NULL; + + if (!trloc[i]) + trloc[i] = n; + else + { + TrLoc_set *last; + for (last = trloc[i]; last->next != NULL; last = last->next); + last->next = n; + } + + } + + } + } + + if (!ntrloc[i]) + { + /* akcja jest niewykonalna, poniewaz i-ty automat ma ta akcje + * w zbiorze swoich akcji, ale nie jest ona w nim umozliwiona. + */ + trloc_set_free(trloc); + free(ntrloc); + return NULL; + } + } + } + + { + ProdTrLoc_set *r = NULL, *r_cur = NULL; + idx_t *idcs = smalloc(sizeof(idx_t)*naut); + int k = 0; + + for (i = 0; i < naut; i++) + { + if (ntrloc[i] > 0) idcs[i] = 1; + else idcs[i] = 0; + } + + while (k >= 0) + { + Loc_idx *dst_ploc = prod_loc_copy(src_ploc); + ProdTrLoc_set *n = smalloc(sizeof(ProdTrLoc_set)); + ClockIdx_set *clocks_cur = NULL; + + n->act = a; + n->guard = dbm_init(dbm_size); + n->clocks = NULL; /* musi byc, bo inaczej clocks_cur bedzie brany pod uwage w clocks_collect */ + + for (i = 0; i < naut; i++) + { + + int depth = 0; + TrLoc_set *trloc_tmp; + + for (trloc_tmp = trloc[i]; trloc_tmp; trloc_tmp = trloc_tmp->next) + { + /* ten for wykonuje sie tylko jak cos sie zmienilo w i-tym automacie */ + + depth++; + if (depth == idcs[i]) + { + dst_ploc[i] = trloc_tmp->loc; + constr2dbm(i, n->guard, trloc_tmp->trans->guard); /* wystarczy tylko dla trloc[i]? */ + /* optymalniej byloby dokonac kanonizacji po wniesieniu zmian do DBM z uwzglednieniem + * ile zostalo zmodyfikowanych elementow (czasami dbm_canon1 nie oplaca sie), poniewaz + * obecnie constr2dbm oblicza za kazdym razem PK co na pewno nie jest oplacalne jesli + * modyfikacji jest tyle co dbm_size. + */ + clocks_collect(&(n->clocks), &clocks_cur, i, trloc_tmp->trans->clocks, trloc_tmp->trans->nclocks); + } + } + + } + + n->loc = dst_ploc; + n->next = NULL; + + if (!r) + r = n; + else + r_cur->next = n; + r_cur = n; + + for (k = naut - 1; k >= 0 && idcs[k] == ntrloc[k]; k--) + { + if (ntrloc[k] > 0) idcs[k] = 1; + } + + if (k >= 0) idcs[k]++; + + } + + free(idcs); + trloc_set_free(trloc); + free(ntrloc); + + return r; + } +} + +/* + * Zwalniamy pamiec prtl i zwracamy kolejny element + * (do wykorzystywania w petlach) + * + */ +ProdTrLoc_set * +prtl_free_getNext(ProdTrLoc_set *prtl) +{ + ProdTrLoc_set *next; + + next = prtl->next; + free(prtl); + + return next; +} + +/* + * Generowanie automatu pseudoproduktowego (do testow). Troche nasmiecone. Jesli ma zostac w kodzie, to + * trzeba dokonac doglebnego przegladu. + */ +void +prod_show(AutNet *an) +{ + ProdLoc_set *waiting_root = NULL, *waiting_cur = NULL; /* _cur nie musi byc NULL (ale kompilator...) */ + ProdLoc_set *visited_root = NULL, *visited_cur = NULL; + + Loc_idx *ploc_init; + DBM_elem *ploc_init_inv; + + net_init(an); + + ploc_init = prod_loc_initial(); + ploc_init_inv = prod_loc_inv(ploc_init); + + prod_loc_set_add(ploc_init, ploc_init_inv, &waiting_root, &waiting_cur); + + while (waiting_root) + { + + ProdLoc_set *processed; + bool *actions; + idx_t i; + + processed = prod_loc_set_raw_pick(&waiting_root); + prod_loc_set_raw_add(processed, &visited_root, &visited_cur); + + actions = prod_loc_acts(processed->loc); + + printf("-------------------------------------------------------------\n"); + printf("Przejscia mozliwe z lokacji produktowej "); + prod_loc_show(processed->loc); printf("\n"); + + for (i = 0; i < nact; i++) + { + if (actions[i]) + { + ProdTrLoc_set *prtl, *prtl_tmp; + prtl = prod_loc_succ(processed->loc, i); + + for (prtl_tmp = prtl; prtl_tmp;) + { + printf("\n"); + printf("Akcja %s\n", get_act_name(act, i)); + printf("Guard:\n"); + dbm_print(prtl_tmp->guard, dbm_size); + printf("Zegary do zresetowania: "); + { + ClockIdx_set *cur; + for (cur = prtl_tmp->clocks; cur; cur = cur->next) + { + ProdClock pc; + pc = prod_clock_pidx2idx(cur->idx); + printf("%s(%s,%d) ", aut[pc.par_aut].name, get_clock_name(aut[pc.par_aut].clks, pc.par_idx), cur->idx); + } + printf("\n"); + } + printf("Do lokacji: "); + prod_loc_show(prtl_tmp->loc); printf("\n"); + + if (!prod_loc_set_is_in(prtl_tmp->loc, waiting_root) && !prod_loc_set_is_in(prtl_tmp->loc, visited_root)) + { + /* lokacji nie ma jeszcze ani w WAITING ani w VISITED, wiec moze ja dodamy... */ + DBM_elem *inv_guard; + + inv_guard = dbm_intersection_cf(processed->inv, prtl_tmp->guard, dbm_size); + if (!dbm_empty(inv_guard, dbm_size)) + { + ClockIdx_set *cur; + DBM_elem *prtl_tmp_locInv; + + for (cur = prtl_tmp->clocks; cur; cur = cur->next) + { + dbm_reset(inv_guard, dbm_size, cur->idx); + } + /* przeciecie inv_guard (po resetach) z niezmiennikiem lokacji docelowej */ + prtl_tmp_locInv = prod_loc_inv(prtl_tmp->loc); + dbm_intersection_cf_ip(inv_guard, prtl_tmp_locInv, dbm_size); + if (!dbm_empty(inv_guard, dbm_size)) + { + prod_loc_set_add(prtl_tmp->loc, prtl_tmp_locInv, &waiting_root, &waiting_cur); + } + else + { + dbm_destroy(prtl_tmp_locInv); + } + } + } + else + { + /* mamy juz ta lokacje, wiec zwalniamy pamiec */ + free(prtl_tmp->loc); + } + + /* informacje z prod_loc_succ zostaly wykorzystane - zwalniamy pamiec */ + dbm_destroy(prtl_tmp->guard); + colclocks_free(prtl_tmp->clocks); + { + ProdTrLoc_set *next; + + next = prtl_tmp->next; + free(prtl_tmp); + prtl_tmp = next; + } + + } + } + + } + free(actions); /* moze lepiej byloby pomyslec nad czyms wielokrotnego uzytku...? + albo zastapic jakas lepsza struktura danych? */ + } + + printf("------\n"); + prod_loc_set_show(visited_root); + prod_loc_set_free(visited_root); + +} + diff --git a/anproc.h b/anproc.h new file mode 100644 index 0000000..bfa4dc2 --- /dev/null +++ b/anproc.h @@ -0,0 +1,49 @@ +#ifndef _INC_ANPROC_H_ +#define _INC_ANPROC_H_ + +#include +#include +#include "anread.h" +#include "antypes.h" + +#ifndef NDEBUG + #define VERBOSE +#endif + +/** prototypy **/ +void net_init(AutNet *); +void prod_clocks_mkmap(void); +void prod_clock_maps_free(void); +Clock_idx prod_clock_idx2pidx(Aut_idx, Clock_idx); +ProdClock prod_clock_pidx2idx(Clock_idx); +Loc_idx *prod_loc_initial(void); +Loc_idx *prod_loc_copy(Loc_idx *); +bool *prod_loc_acts(Loc_idx *); +void prod_loc_show(Loc_idx *prod_loc); +ProdLoc_set *prod_loc_set_add(Loc_idx *, DBM_elem *, ProdLoc_set **, ProdLoc_set **); +void prod_loc_set_raw_add(ProdLoc_set *, ProdLoc_set **, ProdLoc_set **); +bool prod_loc_set_is_in(Loc_idx *, ProdLoc_set *); +ProdLoc_set *prod_loc_set_getp(Loc_idx *, ProdLoc_set *); +ProdLoc_set *prod_loc_set_raw_pick(ProdLoc_set **); +void prod_loc_set_show(ProdLoc_set *); +void prod_loc_set_free(ProdLoc_set *); +void trans_add(ProdLoc_set *, ProdLoc_set *, ProdTrLoc_set *); +bool ploc_in_src_locs(ProdLoc_set *, SrcLoc_set *); +void trloc_set_free(TrLoc_set **); +bool constr_nonempty(Constr *); +void constr2dbm(Aut_idx, DBM_elem *, Constr *); +void clocks_collect(ClockIdx_set **, ClockIdx_set **, Aut_idx, Clock_idx *, Clock_idx); +void colclocks_free(ClockIdx_set *); +DBM_elem *prod_loc_inv(Loc_idx *); +DBM_elem *prod_loc_inv0(Loc_idx *); +ProdTrLoc_set *prod_loc_succ(Loc_idx *, Act_idx); +ProdTrLoc_set *prtl_free_getNext(ProdTrLoc_set *); +void prod_show(AutNet *); + +extern Act_idx nact; +extern DBM_idx dbm_size; +extern DBM_elem *zeroDBM; +extern ProdLoc_set *init_loc_set; +extern Property_set *ppts; + +#endif /* !_INC_ANPROC_H_ */ diff --git a/anpsmod.c b/anpsmod.c new file mode 100644 index 0000000..d48af0e --- /dev/null +++ b/anpsmod.c @@ -0,0 +1,824 @@ +/** anpsmod.c **/ + +/* + * Tutaj jest splitting. Zaczyna sie od psmodel_builder. + */ + +#include +#include +#include +#include +#include "anpsmod.h" +#include "antclass.h" +#include "anproc.h" +#include "antypes.h" +#include "anmacro.h" +#include "macro.h" +#include "dbm.h" + +#ifdef PSM_VERBOSE +static unsigned int stTests; +static unsigned int skip_stTests; +#endif + +/* + * Obliczanie pre_e. + * + * (nie ma sprawdzania zgodnosci przejscia miedzy lokacjami, bo to powinno byc wiadomo + * zanim zostanie wywolana funkcja) + * + * Z n time_pre( [Y:=0]( time_pre(Z') n I(s') ) n guard(e) n I(s) ) + */ +DBM_elem * +psmodel_pre(ProdTrans_set *trans, ProdLoc_set *loc_src, ProdLoc_set *loc_dst, DBM_elem *z_src, DBM_elem *z_dst) +{ + DBM_elem *guard_inv, *tmp_dbm; + + guard_inv = dbm_intersection_cf(trans->guard, loc_src->inv, dbm_size); + if (dbm_empty(guard_inv, dbm_size)) + { + tmp_dbm = guard_inv; + } + else + { + tmp_dbm = dbm_copy(z_dst, dbm_size); + dbm_time_predecessor(tmp_dbm, dbm_size); + dbm_intersection_cf_ip(tmp_dbm, loc_dst->inv, dbm_size); /* modyfikacja w miejscu tmp_dbm */ + if (!dbm_empty(tmp_dbm, dbm_size)) + { + /* tmp_dbm := [reset(trans) := 0]tmp_dbm */ + ClockIdx_set *cur_clock; + + for (cur_clock = trans->clocks; cur_clock; cur_clock = cur_clock->next) + dbm_invreset(tmp_dbm, dbm_size, cur_clock->idx); + + dbm_intersection_cf_ip(tmp_dbm, guard_inv, dbm_size); + if (!dbm_empty(tmp_dbm, dbm_size)) + { + dbm_time_predecessor(tmp_dbm, dbm_size); + dbm_intersection_cf_ip(tmp_dbm, z_src, dbm_size); + } + } + dbm_destroy(guard_inv); + } + + return tmp_dbm; +} + +/* + * Porownywanie wyniku pre_e z konkretna strefa + */ +bool +psmodel_pre_eq(DBM_elem *z_cmp, ProdTrans_set *trans, ProdLoc_set *loc_src, ProdLoc_set *loc_dst, + DBM_elem *z_src, DBM_elem *z_dst) +{ + bool are_equal; + DBM_elem *rlt; + + rlt = psmodel_pre(trans, loc_src, loc_dst, z_src, z_dst); + + are_equal = dbm_equal(rlt, z_cmp, dbm_size); + dbm_destroy(rlt); + + return are_equal; +} + +/* + * Sprawdzanie pustosci wyniku operacji pre_e + */ +bool +psmodel_pre_empty(ProdTrans_set *trans, ProdLoc_set *loc_src, ProdLoc_set *loc_dst, + DBM_elem *z_src, DBM_elem *z_dst) +{ + bool is_empty; + DBM_elem *rlt; + + rlt = psmodel_pre(trans, loc_src, loc_dst, z_src, z_dst); + + is_empty = dbm_empty(rlt, dbm_size); + dbm_destroy(rlt); + + return is_empty; +} + +/* + * Funkcja wykorzystywana przy Post + */ +DBM_elem * +psmodel_post(ProdTrans_set *trans, ProdLoc_set *loc_src, DBM_elem *z_src, DBM_elem *z_dst) +{ + DBM_elem *tmp_dbm; + + tmp_dbm = dbm_copy(z_src, dbm_size); + dbm_time_successor(tmp_dbm, dbm_size); + dbm_intersection_cf_ip(tmp_dbm, loc_src->inv, dbm_size); + if (!dbm_empty(tmp_dbm, dbm_size)) + { + dbm_intersection_cf_ip(tmp_dbm, trans->guard, dbm_size); + if (!dbm_empty(tmp_dbm, dbm_size)) + { + ClockIdx_set *cur_clock; + + for (cur_clock = trans->clocks; cur_clock; cur_clock = cur_clock->next) + dbm_reset(tmp_dbm, dbm_size, cur_clock->idx); + + dbm_time_successor(tmp_dbm, dbm_size); + dbm_intersection_cf_ip(tmp_dbm, z_dst, dbm_size); + } + } + + return tmp_dbm; +} + +bool +psmodel_post_empty(ProdTrans_set *trans, ProdLoc_set *loc_src, DBM_elem *z_src, DBM_elem *z_dst) +{ + bool is_empty; + DBM_elem *rlt; + + rlt = psmodel_post(trans, loc_src, z_src, z_dst); + + is_empty = dbm_empty(rlt, dbm_size); + dbm_destroy(rlt); + + return is_empty; +} + +/* + * Sprawdzanie stabilnosci danej klasy ze wzgledu na mozliwe nastepniki, + * a nastepnie ewentualna stabilizacja. + */ +void +psmodel_split(TimedClass_set *tcX, TimedClassRS_set **reach_stable, TimedClassRS_set **reach_stable_cur) +{ + TimedClass_set *tcY; + DstLoc_set *tcY_dstloc; + ProdLoc_set *tcX_prodloc; + DBM_elem *tcX_dbm, *tcY_dbm; + ProdTrans_set *trans_e; + + tcX_prodloc = tcX->loc_set; + tcX_dbm = tclass_readZoneDBM(tcX); + + assert(tcX->depth != DEPTH_INF); + + /* + * Biore wszystkie klasy Y t.z. da sie do nich przejsc z X (potencjalnie), a nastepnie + * szukam przejsc e \in E t.z. pre_e(X,Y) != 0. + * + * Dla przyspieszenia bierzemy pod uwage potencjalna mozliwosc przejscia. Wystepuje ona dla + * klas zwiazanych z lokacja do ktorych prowadzi przejscie z lokacji zwiazanej z aktualnie + * przetwarzana klasa. + */ + + /** SZUKAMY WSZYSTKICH MOZLIWYCH NASTEPNIKOW KLASY X **/ + /* Przechodzimy przez wszystkie lokacje (docelowe - dst_locs) z location(X) */ + for (tcY_dstloc = tcX_prodloc->dst_locs; tcY_dstloc; tcY_dstloc = tcY_dstloc->next) + { + /* + * Bierzemy po kolei wszystkie klasy zwiazane z location(Y), + * ktore sa potencjalnymi klasami docelowymi + */ + for (tcY = tcY_dstloc->loc_set->classes; tcY; tcY = tcY->next) + { + tcY_dbm = tclass_readZoneDBM(tcY); + + /* Bierzemy wszystkie przejscia mozliwe DO location(Y)... */ + for (trans_e = tcY_dstloc->trans; trans_e; trans_e = trans_e->next) + { + /* ...i dla kazdego e (= trans_e) sprawdzamy czy pre_e(X,Y) != 0 */ + if (!psmodel_pre_empty(trans_e, tcX_prodloc, tcY_dstloc->loc_set, tcX_dbm, tcY_dbm)) + { +#ifdef PSM_VERBOSE + printf("\nSprawdzam stabilnosc klasy (%p) ", tcX); tclass_print(tcX); + printf("\n\tze wzgledu na klase "); tclass_print(tcY); printf("\n\n"); +#endif + assert(tcX->depth != DEPTH_INF); + + if (!psmodel_stabilityCheck(tcY, *reach_stable)) + { + assert(tcY->depth >= tcX->depth+1); + + /* stabilizujemy klase tcX ze wzgl. na tcY oraz przejscie trans_e */ + psmodel_realSplit(tcX, tcY, trans_e, reach_stable, reach_stable_cur); + + return; + } + } + } + + } + } + + /* jak jestesmy tutaj, to stabilne (Split (X,Pi) = {X}): */ + psmodel_stableHandler(tcX, reach_stable, reach_stable_cur); +} + +/* + * Sprawdzanie stabilnosci wzgledem klasy Y + * + * szukamy klasy X1 o minimalnej glebokosci z ktorej istnieje przejscie do klasy Y + * + * z klasy X1 do Y istnieje przejscie jak istnieje przejscie e miedzy location(X1) i location(Y) + * oraz pre_e(X1,Y) != 0 + * + * location(X1) moze byc ktoras z lokacji nalezacych do zbioru lokacji z ktorych + * osiagalna jest location(Y) + * + * jak znajdziemy takie przejscie to sprawdzamy stabilnosc + */ +bool +psmodel_stabilityCheck(TimedClass_set *tcY, TimedClassRS_set *reach_stable) +{ + TimedClassRS_set *curRS; + dpt_t min_depth = DEPTH_INF; + DBM_elem *tcY_dbm = NULL; + + assert(tclass_ReachStable_is_sorted(reach_stable)); /* polegamy na tym ze reach_stable jest posortowane */ + +#ifdef PSM_VERBOSE + stTests++; +#endif + + /* zakladamy ze klasa ([q0], {q0}, 0) ma petle wlasna, wiec bedzie stabilna */ + if (tcY->depth == 0 && tclass_hasInit(tcY)) + { + return true; + } + + /* Bierzemy kolejne klasy X1 do sprawdzenia */ + for (curRS = reach_stable; curRS; curRS = curRS->next) + { + TimedClass_set *tcX1 = curRS->tclass; + /* do sprawdzenia para lokacji i wszystkie przejscia miedzy nimi: */ + + if (tcX1->depth > min_depth) + { + return false; /* nie ma co dalej szukac, bo juz nie ma "minimalnych" */ + } + + /* Jesli znalazlo sie stabilne przejscie z wybranej klasy, to: + * - istnieje przejscie (z jakim h \in E) + * - zachodzi AE na rdzeniach + * - klasa ma minimalna glebokosc bo wybralismy ja z RS (sortowanie) + */ +#ifndef NO_STCACHE + if (tclass_isStableSucc(tcX1, tcY)) + { +#ifdef PSM_VERBOSE + printf("Pominiety test stabilnosci\n"); + skip_stTests++; +#endif + return true; + } +#endif + + if (ploc_in_src_locs(tcX1->loc_set, tcY->loc_set->src_locs)) + { + ProdTrans_set *trans_h; + + if (!tcY_dbm) tcY_dbm = tclass_readZoneDBM(tcY); + + /* Bierzemy kazde mozliwe przejscie z location(X1) do location(Y) */ + for (trans_h = trans_get(tcX1->loc_set, tcY->loc_set); trans_h; trans_h = trans_h->next) + { + if (!psmodel_pre_empty(trans_h, tcX1->loc_set, tcY->loc_set, + tclass_readZoneDBM(tcX1), tcY_dbm)) + { + /* znaleziono mozliwe przejscie z X1 do Y */ + DBM_elem *tcX1_corDBM; + + tcX1_corDBM = tclass_readCorDBM(tcX1); + + /* aktualizujemy min_depth, bo to bedzie nasze minimum */ + if (min_depth != tcX1->depth) + min_depth = tcX1->depth; + + /* Znalazlo sie przejscie! */ +#ifdef PSM_VERBOSE + printf("Mamy przejscie z klasy (%p) ", tcX1); tclass_print(tcX1); + printf("\n\tdo klasy "); tclass_print(tcY); +#endif + if (psmodel_pre_eq(tcX1_corDBM, trans_h, tcX1->loc_set, tcY->loc_set, + tcX1_corDBM, tclass_readCorDBM(tcY))) + { +#ifdef PSM_VERBOSE + printf("stabilna\n"); +#endif + +#ifndef NO_STCACHE + /* zapamietujemy stabilnosc */ + tclass_saveStable(tcX1, tcY); +#endif + return true; + } + } + + } + + } + + } + + return false; +} + +/* + * Obsluga przypadku, gdy split nie mial co robic + */ +void +psmodel_stableHandler(TimedClass_set *tcX, TimedClassRS_set **reach_stable, TimedClassRS_set **reach_stable_cur) +{ + DstLoc_set *dst_loc; + TimedClass_set *tcY; + ProdTrans_set *trans_e; + + /* oznaczanie klasy tcX jako stabilna */ + tclass_mark_stable(tcX); + + /* znajdowanie wszystkich nastepnikow klasy tcX */ + for (dst_loc = tcX->loc_set->dst_locs; dst_loc; dst_loc = dst_loc->next) + { + for (tcY = dst_loc->loc_set->classes; tcY; tcY = tcY->next) + { + for (trans_e = dst_loc->trans; trans_e; trans_e = trans_e->next) + { + if (!psmodel_post_empty(trans_e, tcX->loc_set, tclass_readZoneDBM(tcX), tclass_readZoneDBM(tcY))) + { + /* ustawianie dpt dla kazdego odnalezionego nastepnika */ + tclass_depthUpdateIncr(tcY, tcX); + + /* dodawanie do reachable */ + tclass_ReachStable_add(tcY, reach_stable, reach_stable_cur); +#ifdef PSM_VERBOSE + printf("dodaje klase do reachable %p [%d]: ", trans_e, trans_e->act); tclass_print(tcY); printf("\n"); +#endif + /* TODO: tutaj testowanie spelniania wlasnosci - to sie zrobi ;) */ + if (ppty_check(tcY->loc_set->loc)) + { + tclass_ReachStable_print(*reach_stable); + exit(0); + } + } + } + } + } +} + +/* + * Sprawdzenie warunku funkcji Sp na potrzeby asercji + * + * Powinno zachodzic pre_e(X,Y) != 0 oraz pre_e(Xcor, Ycor) != Xcor + */ +bool +psmodel_realSplit_isDefined(TimedClass_set *tcX, TimedClass_set *tcY, ProdTrans_set *trans_e) +{ + if (psmodel_pre_empty(trans_e, tcX->loc_set, tcY->loc_set, tclass_readZoneDBM(tcX), tclass_readZoneDBM(tcY))) + { + printf("pre_e(X,Y) = 0\n"); + return false; + } + if (psmodel_pre_eq(tclass_readCorDBM(tcX), trans_e, tcX->loc_set, tcY->loc_set, tclass_readCorDBM(tcX), tclass_readCorDBM(tcY))) + { + printf("pre_e(Xcor, Ycor) = Xcor\n"); + return false; + } + + return true; +} + +/* + * Split z rozpatrywaniem 4 przypadkow niestabilnosci + */ +void +psmodel_realSplit(TimedClass_set *tcX, TimedClass_set *tcY, ProdTrans_set *trans_e, + TimedClassRS_set **reach_stable, TimedClassRS_set **reach_stable_cur) +{ + DBM_elem *pre_e_Xcor_Ycor; + DBM_elem *tcX_corDBM, *tcY_corDBM; + + assert(psmodel_realSplit_isDefined(tcX, tcY, trans_e)); /* bardzo wdzieczna assercja */ + + tcX_corDBM = tclass_readCorDBM(tcX); + tcY_corDBM = tclass_readCorDBM(tcY); + + pre_e_Xcor_Ycor = psmodel_pre(trans_e, tcX->loc_set, tcY->loc_set, tcX_corDBM, tcY_corDBM); + + if (!dbm_empty(pre_e_Xcor_Ycor, dbm_size)) + { + /* jesli pre_e(Xcor,Ycor) != 0 to pseudo e-stabilny */ +#ifdef PSM_VERBOSE + printf("pseudo stable\n"); +#endif + /* + * Przed aktualizacja stable aktualizujemy reachable, bo dzieki temu + * przeszukiwac bedziemy mniejszy zbior (stabilnosc oznaczamy na elementach + * reachable). Pi nie aktualizujemy, bo podmieniamy tylko cor klasy. + */ + tclass_ReachStable_delete(tcX, reach_stable, reach_stable_cur); /* usuwanie tcX z reachable i ze stable */ + tclass_mark_preds_unstable(tcX); + /* tutaj tclass_mark_unstable(tcX, *reach_stable) nie mialoby sensu bo tcX juz jest wyrzucone */ + +#ifndef NO_STCACHE + tclass_forgetPreStability(tcX); +#endif + tclass_replaceCorDBM(tcX, pre_e_Xcor_Ycor); /* nowa klasa */ + tclass_depthUpdateInf(tcX); /* jesli nie zawiera q0 ustawiamy dpt(tcX) := inf */ + if (tclass_hasInit(tcX)) /* jesli zawiera q0, to dodajemy do reachable */ + { + tclass_ReachStable_addInit(tcX, reach_stable, reach_stable_cur); + } + /* Nie zwalniamy pre_e_Xcor_Ycor - wykorzystane jako cor! */ + } + else + { + /* pre_e(Xcor,Ycor) = 0 */ + DBM_elem *pre_e_X_Ycor, *tcX_zoneDBM; + TimedClass_set *tcN; + + tcX_zoneDBM = tclass_readZoneDBM(tcX); + pre_e_X_Ycor = psmodel_pre(trans_e, tcX->loc_set, tcY->loc_set, tcX_zoneDBM, tcY_corDBM); + if (!dbm_empty(pre_e_X_Ycor, dbm_size)) + { + DBMset_elem *dbms, *dbms_elem; + + /* jesli pre_e(X,Ycor) != 0 to pseudo e-niestabilny */ +#ifdef PSM_VERBOSE + printf("pseudo unstable\n"); +#endif + /* na podstawie zbioru tworzymy klasy Zone = X\Xcor, Cor = pre_e_X_Ycor */ + dbms = dbm_diff(tcX_zoneDBM, tcX_corDBM, dbm_size); + for (dbms_elem = dbms; dbms_elem; dbms_elem = dbms_elem->next) + { + DBM_elem *new_cor; + + new_cor = dbm_intersection_cf(pre_e_X_Ycor, dbms_elem->dbm, dbm_size); + if (dbm_empty(new_cor, dbm_size)) + { + /* + * Jesli cor (pre_e_X_Ycor) nie zawiera sie w zone to ustawiamy, + * ze cor = zone (jak cor = NULL, to cor = zone). + */ + dbm_destroy(new_cor); + new_cor = NULL; + } + + tcN = tclass_create_nd(tcX->loc_set, dbms_elem->dbm, new_cor); + tclass_depthUpdateInf(tcN); + if (tclass_hasInit(tcN)) + { + tclass_ReachStable_addInit(tcN, reach_stable, reach_stable_cur); + } + tclass_add(tcN); + } + dbmset_scaffoldDestroy(dbms); + + tclass_ReachStable_delete(tcX, reach_stable, reach_stable_cur); + tclass_mark_preds_unstable(tcX); +#ifndef NO_STCACHE + tclass_forgetPreStability(tcX); +#endif + tclass_replaceZoneDBM(tcX, tcX_corDBM); /* nowa klasa; cor rowny calej nowej klasie, tzn. cor == NULL */ + tclass_depthUpdateInf(tcX); + if (tclass_hasInit(tcX)) + { + tclass_ReachStable_addInit(tcX, reach_stable, reach_stable_cur); + } + } + else + { + /* pre_e(X,Ycor) = 0 */ + DBM_elem *pre_e_Xcor_Y, *tcY_zoneDBM; + + tcY_zoneDBM = tclass_readZoneDBM(tcY); + pre_e_Xcor_Y = psmodel_pre(trans_e, tcX->loc_set, tcY->loc_set, tcX_corDBM, tcY_zoneDBM); + if (!dbm_empty(pre_e_Xcor_Y, dbm_size)) + { + DBMset_elem *dbms, *dbms_elem; + + /* jesli pre_e(Xcor,Y) != 0 to semi e-niestabilny */ +#ifdef PSM_VERBOSE + printf("semi unstable\n"); +#endif + /* (X, pre_e_Xcor_Y, dpt), robimy podmiane i aktualizujemy */ + tclass_ReachStable_delete(tcX, reach_stable, reach_stable_cur); + tclass_mark_preds_unstable(tcX); +#ifndef NO_STCACHE + tclass_forgetPreStability(tcX); +#endif + tclass_replaceCorDBM(tcX, pre_e_Xcor_Y); /* dalej zwolnic pre_e_Xcor_Y */ + tclass_depthUpdateInf(tcX); + if (tclass_hasInit(tcX)) + { + tclass_ReachStable_addInit(tcX, reach_stable, reach_stable_cur); + } + + /* (Y\Ycor, Y\Ycor, dpt) */ + dbms = dbm_diff(tcY_zoneDBM, tcY_corDBM, dbm_size); + for (dbms_elem = dbms; dbms_elem; dbms_elem = dbms_elem->next) + { + tcN = tclass_create_nd(tcY->loc_set, dbms_elem->dbm, NULL); /* NULL, bo cor = zone */ + tclass_depthUpdateInf(tcN); + if (tclass_hasInit(tcN)) + { + tclass_ReachStable_addInit(tcN, reach_stable, reach_stable_cur); + } + tclass_add(tcN); + } + dbmset_scaffoldDestroy(dbms); + + /* (Ycor, Ycor, dpt) */ + tclass_ReachStable_delete(tcY, reach_stable, reach_stable_cur); + tclass_mark_preds_unstable(tcY); +#ifndef NO_STCACHE + tclass_forgetPreStability(tcY); +#endif + tclass_replaceZoneDBM(tcY, tcY_corDBM); /* cor domyslnie rowny calej klasie */ + tclass_depthUpdateInf(tcY); + if (tclass_hasInit(tcY)) + { + tclass_ReachStable_addInit(tcY, reach_stable, reach_stable_cur); + } + } + else + { + DBM_elem *pre_e_X_Y; + DBMset_elem *dbms, *dbms_elem; + /* pre_e(Xcor,Y) = 0 */ + +#ifdef PSM_VERBOSE + printf("unstable\n"); +#endif + /* TODO: czasem niestety to obliczane jest dwa razy (wczesniej przy spr. mozliwosci przejscia) */ + pre_e_X_Y = psmodel_pre(trans_e, tcX->loc_set, tcY->loc_set, tcX_zoneDBM, tcY_zoneDBM); + + /* (X\pre_e_X_Y, Xcor, dpt) - uwaga podwojne wykorzystanie pre_e_X_Y - napisac komentarz! */ + dbms = dbm_diff(tcX_zoneDBM, pre_e_X_Y, dbm_size); + for (dbms_elem = dbms; dbms_elem; dbms_elem = dbms_elem->next) + { + DBM_elem *new_cor; + + new_cor = dbm_intersection_cf(tcX_corDBM, dbms->dbm, dbm_size); + if (dbm_empty(new_cor, dbm_size)) + { + dbm_destroy(new_cor); + new_cor = NULL; + } + tcN = tclass_create_nd(tcX->loc_set, dbms_elem->dbm, new_cor); + tclass_depthUpdateInf(tcN); + if (tclass_hasInit(tcN)) + { + tclass_ReachStable_addInit(tcN, reach_stable, reach_stable_cur); + } + tclass_add(tcN); + } + dbmset_scaffoldDestroy(dbms); + + /* (pre_e_X_Y, pre_e_X_Y, dpt) */ + tclass_ReachStable_delete(tcX, reach_stable, reach_stable_cur); + tclass_mark_preds_unstable(tcX); +#ifndef NO_STCACHE + tclass_forgetSuccStability(tcX); + tclass_forgetPreStability(tcX); +#endif + tclass_replaceZoneDBM(tcX, pre_e_X_Y); /* nowa klasa; cor zostaje rowny zone, tzn. cor == NULL */ + dbm_destroy(pre_e_X_Y); + tclass_depthUpdateInf(tcX); + if (tclass_hasInit(tcX)) + { + tclass_ReachStable_addInit(tcX, reach_stable, reach_stable_cur); + } + + /* (Y\Ycor, Y\Ycor, dpt) */ + dbms = dbm_diff(tcY_zoneDBM, tcY_corDBM, dbm_size); + for (dbms_elem = dbms; dbms_elem; dbms_elem = dbms_elem->next) + { + tcN = tclass_create_nd(tcY->loc_set, dbms_elem->dbm, NULL); /* NULL, bo cor = zone */ + tclass_depthUpdateInf(tcN); + if (tclass_hasInit(tcN)) + { + tclass_ReachStable_addInit(tcN, reach_stable, reach_stable_cur); + } + tclass_add(tcN); + } + dbmset_scaffoldDestroy(dbms); + + /* (Ycor, Ycor, dpt) */ + tclass_ReachStable_delete(tcY, reach_stable, reach_stable_cur); + tclass_mark_preds_unstable(tcY); +#ifndef NO_STCACHE + tclass_forgetPreStability(tcY); +#endif + tclass_replaceZoneDBM(tcY, tcY_corDBM); /* nowy cor domyslnie rowny calej klasie */ + tclass_depthUpdateInf(tcY); + if (tclass_hasInit(tcY)) + { + tclass_ReachStable_addInit(tcY, reach_stable, reach_stable_cur); + } + } + dbm_destroy(pre_e_Xcor_Y); + } + dbm_destroy(pre_e_X_Ycor); + } + dbm_destroy(pre_e_Xcor_Ycor); + +} + +/* + * Inicjalizacja potrzebnych struktur danych do zbudowania ps-modelu: + * + * - poczatkowy podzial + * - zbior lokacji odwiedzonych + * - zbior klas osiagalnych (reachable), zbior klas stabilnych (stable) + */ +void +psmodel_init(ProdLoc_set **visited_root, ProdLoc_set **visited_cur, + TimedClassRS_set **reach_stable_root, TimedClassRS_set **reach_stable_cur) +{ + Loc_idx *ploc_init; /* lokacja poczatkowa */ + DBM_elem *ploc_init_inv; /* jej niezmiennik */ + TimedClass_set *init_tclass; + + /* zbieramy informacje o lokacji poczatkowej */ + ploc_init = prod_loc_initial(); /* lokacje skladowe */ + ploc_init_inv = prod_loc_inv(ploc_init); /* niezmiennik (koniunkcja niezm. skladowych) */ + + init_loc_set = prod_loc_set_add(ploc_init, ploc_init_inv, visited_root, visited_cur); + + init_tclass = tclass_create(init_loc_set, NULL, dbm_copy(zeroDBM, dbm_size), 0); + tclass_add(init_tclass); + tclass_mark_reach_unst(init_tclass, reach_stable_root, reach_stable_cur); +} + +/* + * Konstruowanie pseudosymulacyjnego modelu abstrakcyjnego + */ +void +psmodel_builder(AutNet *an) +{ + ProdLoc_set *visited_locs_root = NULL, *visited_locs_cur; + + TimedClassRS_set *reach_stable_root = NULL, *reach_stable_cur, *picked_tclass_rs; + + net_init(an); /* inicjalizujemy siec */ + + psmodel_init(&visited_locs_root, &visited_locs_cur, &reach_stable_root, &reach_stable_cur); + +#ifdef PSM_VERBOSE + stTests = 0; + skip_stTests = 0; +#endif + + /* + * Na razie stosujemy zbior zawierajacy klasy osiagalne i oznaczamy te ktore sa w stable, + * opierajac sie na obserwacji, ze stable zawsze zawiera sie w reachable. + * W przyszlosci mozna sprobowac rozbic reachable na reachable_stable (stable) i reachable_unstable. + * Dzieki temu uniknie sie przegladania zbioru w poszukiwaniu pierwszej niestabilnej klasy. + */ + + while ((picked_tclass_rs = tclass_pickReachUnst(reach_stable_root)) != NULL) + { + TimedClass_set *tc; /* rozwazana klasa Y */ + bool *actions; + idx_t i; + ProdLoc_set *cur_loc; + + tc = picked_tclass_rs->tclass; + cur_loc = tc->loc_set; + +#ifdef PSM_VERBOSE + printf("Przetwarzana klasa "); tclass_print(tc); printf("\n"); +#endif + + if (!cur_loc->trans_complete) + { + /**** okreslamy new_locs, visited_locs i rozszerzamy zbior Pi ****/ + actions = prod_loc_acts(tc->loc_set->loc); /* akcje wykonalne z lokacji zwiazanej z biezaca klasa */ + for (i = 0; i < nact; i++) + { + if (actions[i]) + { + ProdTrLoc_set *prtl, *prtl_tmp; + prtl = prod_loc_succ(cur_loc->loc, i); /* pobieramy mozliwe przejscia dla akcji i */ + + for (prtl_tmp = prtl; prtl_tmp; prtl_tmp = prtl_free_getNext(prtl_tmp)) + { + DBM_elem *inv_guard; + bool transition_added = false; + + /* + * UWAGA: + * Zanim dodamy lokacje lub przejscie do niej prowadzace, sprawdzamy warunek + * na guardy i niezmienniki. Przejscia rowniez nie sa zapisywane jesli nie jest + * spelniony ten warunek (linia 6 i 7). + */ + + inv_guard = dbm_intersection_cf(cur_loc->inv, prtl_tmp->guard, dbm_size); + if (!dbm_empty(inv_guard, dbm_size)) + { + /* niepuste przeciecie niezmiennika lokacji zrodlowej z guardem */ + ClockIdx_set *cur_clock; + DBM_elem *dst_locInv; + ProdLoc_set *dst_loc; + + /* inv_guard := inv_guard[reset(prtl_tmp) := 0] */ + for (cur_clock = prtl_tmp->clocks; cur_clock; cur_clock = cur_clock->next) + dbm_reset(inv_guard, dbm_size, cur_clock->idx); + + /* pobieramy adres struktury z lokacja docelowa dla przetwarzanego przejscia + * jesli nie ma, to dst_loc == NULL + * + * dst_loc jest wykorzystywane jako warunek czy lokacja jest w visited_locs + */ + dst_loc = prod_loc_set_getp(prtl_tmp->loc, visited_locs_root); + + /* niezmiennik produktowy obliczamy tylko gdy jeszcze nie zrobilismy tego wczesniej */ + if (!dst_loc) + dst_locInv = prod_loc_inv(prtl_tmp->loc); + else + dst_locInv = dst_loc->inv; + + dbm_intersection_cf_ip(inv_guard, dst_locInv, dbm_size); + if (!dbm_empty(inv_guard, dbm_size)) + { + /* dodajemy lokacje do visited_locs? */ + if (!dst_loc) + { + /* dst_loc == NULL */ + dst_loc = prod_loc_set_add(prtl_tmp->loc, dst_locInv, &visited_locs_root, &visited_locs_cur); + tclass_add(tclass_create_base(dst_loc)); /* dodajemy nowa klase do Pi */ + } + else + { + /* juz mamy ta lokacje, wiec zwalniamy pamiec (juz znamy ta konfiguracje lokacji skladowych) */ + free(prtl_tmp->loc); + /* dst_locInv: niezmiennika nigdy nie zwalniamy, bo albo jest pobrany + * istniejacy albo dodajemy nowa lokacje + */ + } + + /* dopisujemy odkryte przejscie do zbioru przejsc lokacji zrodlowej (aktualnie przetwarzana) */ + trans_add(cur_loc, dst_loc, prtl_tmp); + transition_added = true; + } + } + + dbm_destroy(inv_guard); + + /* DBM z guardem i liste zegarow (reset) zwalniamy tylko jesli nie dodalismy tranzycji */ + if (!transition_added) + { + dbm_destroy(prtl_tmp->guard); + colclocks_free(prtl_tmp->clocks); + } + + } + } + } + free(actions); + cur_loc->trans_complete = true; /* przejscia z tej lokacji zostaly skompletowane */ + } + psmodel_split(tc, &reach_stable_root, &reach_stable_cur); + + } + + tclass_ReachStable_print(reach_stable_root); +#ifdef PSM_VERBOSE + printf("\nPominietych testow stabilnosci (cache): %u/%u\n", skip_stTests, stTests); + printf("Utworzonych rzeczywistych klas: %u\n", tclass_count(visited_locs_root)); +#endif + +} + +bool +ppty_check(Loc_idx *prodloc) +{ + Property_set *ppty; + + for (ppty = ppts; ppty; ppty = ppty->next) + { + ProdConf_set *w; + bool sat = false; + + for (w = ppty->prop; w; w = w->next) + { + if (prodloc[w->aut] == w->loc) + { + sat = true; + } + else + { + sat = false; + break; + } + } + + if (sat) + { + printf("Property \"%s\" satisfied!\n", ppty->name); + return true; + } + } + + return false; +} diff --git a/anpsmod.h b/anpsmod.h new file mode 100644 index 0000000..7ae8f29 --- /dev/null +++ b/anpsmod.h @@ -0,0 +1,34 @@ +#ifndef _INC_ANPSMOD_H_ +#define _INC_ANPSMOD_H_ + +#include +#include "antypes.h" + +#ifndef NDEBUG + #define PSM_VERBOSE +#endif + +/* wylaczanie cache'u stabilnosci */ +/* +#define NO_STCACHE +*/ + +DBM_elem *psmodel_pre(ProdTrans_set *, ProdLoc_set *, ProdLoc_set *, DBM_elem *, DBM_elem *); +bool psmodel_pre_eq(DBM_elem *, ProdTrans_set *, ProdLoc_set *, ProdLoc_set *, DBM_elem *, DBM_elem *); +bool psmodel_pre_empty(ProdTrans_set *, ProdLoc_set *, ProdLoc_set *, DBM_elem *, DBM_elem *); +DBM_elem *psmodel_post(ProdTrans_set *, ProdLoc_set *, DBM_elem *, DBM_elem *); +bool psmodel_post_empty(ProdTrans_set *, ProdLoc_set *, DBM_elem *, DBM_elem *); + +void psmodel_split(TimedClass_set *, TimedClassRS_set **, TimedClassRS_set **); +bool psmodel_stabilityCheck(TimedClass_set *, TimedClassRS_set *); +void psmodel_stableHandler(TimedClass_set *, TimedClassRS_set **, TimedClassRS_set **); +bool psmodel_realSplit_isDefined(TimedClass_set *, TimedClass_set *, ProdTrans_set *); +void psmodel_realSplit(TimedClass_set *, TimedClass_set *, ProdTrans_set *, TimedClassRS_set **, TimedClassRS_set **); + +void psmodel_init(ProdLoc_set **, ProdLoc_set **, TimedClassRS_set **, TimedClassRS_set **); +void psmodel_builder(AutNet *); + +bool ppty_check(Loc_idx *); + + +#endif /* !_INC_ANPSMOD_H_ */ diff --git a/anread.c b/anread.c new file mode 100644 index 0000000..5820d57 --- /dev/null +++ b/anread.c @@ -0,0 +1,862 @@ +/** anread.c **/ + +/* + * Konstruowanie struktury danych przetrzymujacej cala wczytana siec. + * + * Nie okreslam ktore argumenty sa const, bo to juz nie te czasy. ;) + */ + +#include +#include +#include +#include +#include "anread.h" +#include "antypes.h" +#include "anmacro.h" +#include "macro.h" + +/* lokacje */ +static Loc_set *loc_root = NULL; +static Loc_set *loc_cur = NULL; +static Loc_idx loc_cnt = 0; +static Loc *loc_map = NULL; +static Loc_type loc_type = 0; + +static Loc_idx init_loc; /* indeks lok. poczatkowej */ +static bool got_initial_loc = false; /* czy juz mamy lok. poczatkowa */ + +/* akcje */ +static Act_set *act_root = NULL; +static Act_set *act_cur = NULL; +static Act_idx act_cnt = 0; +static Act *act_map = NULL; +static Act_type act_type = 0; +static bool *uact = NULL; + +/* zegary */ +static Clock_set *clocks_root = NULL; /* korzen zegarowego stosu */ +static Clock_set *clocks_cur = NULL; /* biezacy element (ostatni) zegarowego stosu */ +static Clock_idx clocks_cnt = 0; /* liczba aktualnie zapmietanych zegarow na zegarowym stosie */ +static Clock *clocks_map = NULL; /* mapowanie indeksow zegarow na ich nazwy */ +static Clock_idx aut_clocks_cnt = 0; + +/* ograniczenia */ +static Constr_set *constr_root = NULL; +static Constr_set *constr_cur = NULL; +static Constr_idx constr_cnt = 0; + +/* macierz przejsc */ +static Trans_set **trs = NULL; + +/* automaty */ +static Aut_set *aut_root = NULL; +static Aut_set *aut_cur = NULL; +static Aut_idx aut_cnt = 0; + +/* wlasnosci sieci */ +static ProdConf_set *prodconf_root = NULL; +static ProdConf_set *prodconf_cur = NULL; +static Property_set *properties_root = NULL; +static Property_set *properties_cur = NULL; + +/* siec automatow */ +static AutNet autnet; + +/**************/ +/*** ZEGARY ***/ +/**************/ + +/* + * Dodawanie zegarow do listy + */ +void +clocks_append(Clock new_clock) +{ + Clock_set *n, *cur = clocks_root, *next; + + /* sprawdzamy czy dodawany zegar juz nie znajduje sie na liscie */ + while (cur) + { + next = cur->next; + if(strcmp(cur->clock, new_clock) == 0) + { + printf("Duplicated clock %s. Not adding!\n", new_clock); + return; + } + cur = next; + } + + n = smalloc(sizeof(Clock_set)); + + n->clock = new_clock; + n->next = NULL; + + if (!clocks_cur) + clocks_root = n; + else + clocks_cur->next = n; + clocks_cur = n; + + clocks_cnt++; +} + +/* + * Tworzenie mapy zegarow systemowych +*/ +void +clocks_mkmap(void) +{ + Clock_set *cur = clocks_root, *next; + Clock *map = NULL; + + if (clocks_map) + { + FERROR("Clocks already mapped"); + } + + aut_clocks_cnt = clocks_cnt; + map = clocks_map = smalloc(sizeof(Clock) * aut_clocks_cnt); + + while (cur) + { + next = cur->next; + *map = cur->clock; + map++; + free(cur); + cur = next; + } + + clocks_root = clocks_cur = NULL; + clocks_cnt = 0; +} + +/* + * Konsumowanie zapamietanych zegarow i zwracanie + * ich indeksow w postaci tablicy + * + * UWAGA: clocks_cnt jest resetowany, wiec + * ewentualnie trzeba wczesniej go zapamietac + */ +Clock_idx * +clocks_mkarr(void) +{ + Clock_set *cur = clocks_root, *next; + Clock_idx *r, *arr; + + if (!clocks_root) return NULL; + + arr = r = smalloc(sizeof(Clock_idx) * clocks_cnt); + + while (cur) + { + next = cur->next; + *(arr++) = get_cur_clock_idx(cur->clock); + free(cur->clock); + free(cur); + cur = next; + } + + clocks_root = clocks_cur = NULL; + clocks_cnt = 0; + + return r; +} + +/* + * Znajdowanie indeksu zegara na podstawie jego nazwy + */ +Clock_idx +get_clock_idx(Clock *cm, Clock_idx cc, char *name) +{ + int i; + + if (!cm) + { + FERROR("Clocks map is empty!"); + } + + for (i = 0; i < cc; i++) + if (!strcmp(*(cm++), name)) return i+1; + + printf("Clock %s undeclared. ", name); + FERROR("Unknown clock!"); + /* return -1; */ +} + +Clock_idx +get_cur_clock_idx(char *name) +{ + return get_clock_idx(clocks_map, aut_clocks_cnt, name); +} + +char * +get_clock_name(Clock *cm, Clock_idx i) +{ + assert(i >= 0); + + if (!cm) + { + FERROR("Clocks map is empty!"); + } + + if (i == 0) return CLOCK_0_NAME; + else return cm[i-1]; +} + +char * +get_cur_clock_name(Clock_idx i) +{ + return get_clock_name(clocks_map, i); +} + +void +clocks_show(Clock *cm, Clock_idx cc) +{ + int i; + + if (!cm) + { + FERROR("Clocks map is empty!"); + } + + for (i = 0; i < cc+1; i++) + printf("cm[%d] = %s\n", i, get_clock_name(cm, i)); +} + +/*****************************/ +/*** OGRANICZENIA ZEGAROWE ***/ +/*****************************/ + +void +constr_append(Clock_idx i, Clock_idx j, Constr_rel r, int val) +{ + Constr_set *n; + + n = smalloc(sizeof(Constr_set)); + + n->constr.l_clk = i; + n->constr.r_clk = j; + n->constr.rel = r; + n->constr.val = val; + n->next = NULL; + + if (!constr_root) + constr_root = n; + else + constr_cur->next = n; + constr_cur = n; + + constr_cnt++; +} + +Constr * +constrs_mkarr(void) +{ + Constr_set *cur = constr_root, *next; + Constr *r, *arr; + + if (!constr_root) return NULL; + + r = smalloc(sizeof(Constr) * (constr_cnt+1)); + arr = r; + + while (cur) + { + next = cur->next; + *(arr++) = cur->constr; + free(cur); + cur = next; + } + + CONSTR_MARK_TERM(arr); /* ostatnie ograniczenie terminuje tablice */ + + constr_root = constr_cur = NULL; + constr_cnt = 0; + + return r; +} + +/* + * Wyswietlanie ograniczen + */ +void +constrs_show(Constr *c, Clock *cm) +{ + if (!c) return; + + while (!CONSTR_IS_TERM(c)) + { + printf("(%s - %s ", get_clock_name(cm, c->l_clk), get_clock_name(cm, c->r_clk)); + switch (c->rel) + { + case CONSTR_LE: + printf("<= "); + break; + case CONSTR_LT: + printf("< "); + break; + } + printf("%d) ", c->val); + c++; + } +} + +/***************/ +/*** LOKACJE ***/ +/***************/ + +void +locations_append(char *name) +{ + Loc_set *n, *cur = loc_root, *next; + + /* sprawdzamy czy dodawana lokacja juz nie znajduje sie na liscie */ + while (cur) + { + next = cur->next; + if(strcmp(cur->loc.name, name) == 0) + { + printf("Duplicated location %s. Not adding!\n", name); + return; + } + cur = next; + } + + n = smalloc(sizeof(Loc_set)); + + n->loc.name = name; + n->loc.inv = constrs_mkarr(); + n->loc.type = loc_type; loc_type = 0; + n->next = NULL; + + if (!loc_cur) + loc_root = n; + else + loc_cur->next = n; + loc_cur = n; + + loc_cnt++; +} + +/* + * Okresla typ aktualnej lokacji do dodania + */ +void +set_loc_type(Loc_type t) +{ + loc_type |= t; +} + +/* + * Tworzenie mapy lokacji + */ +void +locations_mkmap(void) +{ + Loc_set *cur = loc_root, *next; + Loc *map = NULL; + int i; + + if (loc_map) + { + FERROR("Locations already mapped"); + } + + loc_map = smalloc(sizeof(Loc)*loc_cnt); + + map = loc_map; + + for (i = 0; cur; i++) + { + next = cur->next; + *map = cur->loc; + if (LOC_IS_INITIAL(cur->loc)) + { + if (got_initial_loc) + { + FERROR("Multiple initial locations not allowed."); + } + else + { + init_loc = i; + got_initial_loc = true; + } + } + map++; + free(cur); + cur = next; + } + + loc_root = loc_cur = NULL; +} + +Loc_idx +get_loc_idx(Loc *lm, Loc_idx lc, char *name) +{ + int i; + + if (!lm) + { + FERROR("Locations map is empty!"); + } + + for (i = 0; i < lc; i++) + if (!strcmp((lm++)->name, name)) return i; + + printf("Location %s undeclared\n", name); + FERROR("Unknown location!"); + /* return -1; */ +} + +Loc_idx +get_cur_loc_idx(char *name) +{ + return get_loc_idx(loc_map, loc_cnt, name); +} + +char * +get_loc_name(Loc *lm, Loc_idx i) +{ + return lm[i].name; +} + +char * +get_cur_loc_name(Loc_idx i) +{ + return get_loc_name(loc_map, i); +} + +void +locations_show(Loc *lm, Loc_idx lc, Clock *cm) +{ + int i; + + if (!lm) + { + FERROR("Locations map is empty!"); + } + + printf("Locations:\n"); + + for (i = 0; i < lc; i++) + { + printf("%d - %s ", i, lm[i].name); + if (LOC_IS_INITIAL(lm[i])) printf("initial "); + if (LOC_IS_URGENT(lm[i])) printf("urgent "); + if (LOC_IS_COMMITED(lm[i])) printf("commited "); + if (lm[i].inv) + { + printf("with invariant: "); + constrs_show(lm[i].inv, cm); + } + printf("\n"); + } +} + +/*************/ +/*** AKCJE ***/ +/*************/ + +void +actions_append(char *name) +{ + Act_set *n, *cur = act_root, *next; + + /* sprawdzamy czy dodawana akcja juz nie znajduje sie na liscie */ + while (cur) + { + next = cur->next; + if(!strcmp(cur->act.name, name)) + { + printf("Duplicated action %s. Not adding!\n", name); + return; + } + cur = next; + } + + n = smalloc(sizeof(Act_set)); + + n->act.name = name; + n->act.type = act_type; act_type = 0; + n->next = NULL; + + if (!act_cur) + act_root = n; + else + act_cur->next = n; + act_cur = n; + + act_cnt++; +} + +/* + * Okresla typ aktualnej akcji do dodania + */ +void +set_act_type(Act_type t) +{ + act_type |= t; +} + +/* + * Tworzenie mapy akcji + */ +void +actions_mkmap(void) +{ + Act_set *cur = act_root, *next; + Act *map = NULL; + + if (act_map) + { + FERROR("Actions already mapped"); + } + + act_map = smalloc(sizeof(Act)*act_cnt); + + map = act_map; + + while (cur) + { + next = cur->next; + *map = cur->act; + map++; + free(cur); + cur = next; + } + + act_root = act_cur = NULL; + +#ifdef VERBOSE + printf("Got all actions\n"); + actions_show(act_map, act_cnt); +#endif +} + +Act_idx +get_act_idx(Act *am, Act_idx ac, char *name) +{ + int i; + + if (!am) + { + FERROR("Actions map is empty!"); + /* TODO: czy to faktycznie jest nie do przelkniecia? + czy zakladamy ze jak jest automat to musi miec jakies akcje? */ + } + + for (i = 0; i < ac; i++) + if (!strcmp((am++)->name, name)) return i; + + printf("Action %s undeclared. ", name); + FERROR("Unknown action!"); + + /* return -1; */ +} + +Loc_idx +get_cur_act_idx(char *name) +{ + return get_act_idx(act_map, act_cnt, name); +} + +char * +get_act_name(Act *am, Act_idx i) +{ + return am[i].name; +} + +char * +get_cur_act_name(Act_idx i) +{ + return get_act_name(act_map, i); +} + +void +actions_show(Act *am, Act_idx ac) +{ + int i; + + if (!am) + { + FERROR("Actions map is empty!"); + } + + printf("Actions:\n"); + + for (i = 0; i < ac; i++) + { + printf("%d - %s ", i, am[i].name); + if (ACT_IS_URGENT(am[i])) printf("urgent "); + printf("\n"); + } +} + +void +act_mark_used(Act_idx i) +{ +#ifdef VERBOSE + printf("Marking action %d as used\n", i); +#endif + if (!uact) + uact = smalloc_zero(sizeof(bool)*act_cnt); + + uact[i] = true; +} + +/*****************/ +/*** PRZEJSCIA ***/ +/*****************/ + +void +trans_append(Loc_idx src, Loc_idx dst, Act_idx action) +{ + Trans_set **ts; + Trans_set *new_trans; + Trans_set *cur; + + if (!trs) /* jesli nie ma tablicy tranzycji, to ja tworzymy */ + trs = smalloc_zero(sizeof(Trans_set *)*loc_cnt*loc_cnt); + + act_mark_used(action); + + new_trans = smalloc(sizeof(Trans_set)); + new_trans->act = action; + new_trans->guard = constrs_mkarr(); + new_trans->nclocks = clocks_cnt; /* clocks_mkarr() zeruje clocks_cnt, dlatego najpierw zapisujemy _cnt */ + new_trans->clocks = clocks_mkarr(); + new_trans->next = NULL; + + ts = TRANS_P(trs, loc_cnt, src, dst); /* bierzemy odpowiedni wskaznik do wskaznika na pierwsza tranzycje */ + if (!*ts) + *ts = new_trans; + else + { + cur = *ts; + while (cur->next) cur = cur->next; + cur->next = new_trans; + } + +} + +void +trans_show(Trans_set **t, Loc *lm, Loc_idx nl, Clock *cm, Act *am) +{ + Loc_idx i, j; + Trans_set **ts; + Trans_set *cur; /* mozna pozbyc sie tej zmiennej ;) */ + + if (!t) + { + FERROR("No transitions recorded!"); + } + + printf("Transitions:\n"); + + for (i = 0; i < nl; i++) + { + for (j = 0; j < nl; j++) + { + + ts = TRANS_P(t, nl, i, j); + + if (*ts) + { + cur = *ts; + do { + printf("Action: %s ", get_act_name(am, cur->act)); + if (ACT_IS_URGENT(am[cur->act])) printf("(urgent)"); + printf("\n"); + printf("%s -> %s\n", get_loc_name(lm, i), get_loc_name(lm, j)); + printf("Guard: "); + constrs_show(cur->guard, cm); + printf("\n"); + printf("Reset clocks: "); + trans_clocks_show(cur, cm); + cur = cur->next; + } while (cur); + + } + + } + } +} + +/* + * Wyswietlanie zegarow do zresetowania ze wskazana tranzycja + */ +void +trans_clocks_show(Trans_set *t, Clock *cm) +{ + int i; + Clock_idx *c = t->clocks; + + for (i = 0; i < t->nclocks; i++) { + printf("%s ", get_clock_name(cm, c[i])); + } + printf("\n"); +} + +void +cur_trans_show(void) +{ + trans_show(trs, loc_map, loc_cnt, clocks_map, act_map); +} + +/*****************/ +/*** Wlasnosci ***/ +/*****************/ + +/* + * tutaj powinien byc tworzony element Property_set z powstalej + * listy tymczasowej elementow ProdConf_set. + */ +void +property_got_one(char *name) +{ + Property_set *new; + + new = smalloc(sizeof(Property_set)); + new->prop = prodconf_root; prodconf_root = NULL; + new->name = name; + new->next = NULL; + + if (!properties_root) + properties_root = new; + else + properties_cur->next = new; + properties_cur = new; +} + +/* + * tutaj powinien byc tworzony element ProdConf_set + * i dodawany do listy tych elementow + */ +void +property_append_loc(char *loc, char *aut) +{ + Aut_idx ai; + ProdConf_set *new; + + if (!autnet.aut) FERROR("Define network first!"); + + ai = get_aut_idx(aut); + + new = smalloc(sizeof(ProdConf_set)); + new->aut = ai; + new->loc = get_loc_idx(autnet.aut[ai].loc, autnet.aut[ai].nloc, loc); + new->next = NULL; + + if (!prodconf_root) + prodconf_root = new; + else + prodconf_cur->next = new; + prodconf_cur = new; + + free(loc); + free(aut); +} + +/***************/ +/*** AUTOMAT ***/ +/***************/ + +Aut_idx +get_aut_idx(char *name) +{ + Aut_idx i; + + assert(autnet.aut != NULL); + + for (i = 0; i < autnet.naut; i++) + { + if (!strcmp(autnet.aut[i].name, name)) return i; + } + + printf("Automaton %s not found\n", name); + FERROR("Unknown automaton!"); +} + +void +complete_automaton(char *name) +{ + Aut_set *n; + + n = smalloc(sizeof(Aut_set)); + + n->name = name; + n->nclks = aut_clocks_cnt; aut_clocks_cnt = 0; + n->clks = clocks_map; clocks_map = NULL; + n->nloc = loc_cnt; loc_cnt = 0; + n->loc = loc_map; loc_map = NULL; + if (!got_initial_loc) /* brak lokacji poczatkowej! */ + { + FERROR("Initial location not defined!"); + } + else + { + n->init_loc = init_loc; + got_initial_loc = false; + } + n->trans = trs; trs = NULL; + n->uact = uact; uact = NULL; + n->next = NULL; + + if (!aut_cur) + aut_root = n; + else + aut_cur->next = n; + aut_cur = n; + + aut_cnt++; + +#ifdef VERBOSE + printf("Got complete automaton %s.\n", name); + clocks_show(n->clks, n->nclks); + locations_show(n->loc, n->nloc, n->clks); + trans_show(n->trans, n->loc, n->nloc, n->clks, act_map); +#endif +} + +void +complete_net(void) +{ + Aut_set *cur = aut_root, *next; + Aut *map = NULL; + + autnet.aut = smalloc(sizeof(Aut) * aut_cnt); + autnet.naut = aut_cnt; + autnet.act = act_map; act_map = NULL; + autnet.nact = act_cnt; act_cnt = 0; + + map = autnet.aut; + while (cur) + { + next = cur->next; + map->name = cur->name; + map->nclks = cur->nclks; + map->clks = cur->clks; + map->nloc = cur->nloc; + map->loc = cur->loc; + map->init_loc = cur->init_loc; + map->trans = cur->trans; + map->uact = cur->uact; + map++; + free(cur); /* TODO: co jeszcze zwalniac? */ + cur = next; + } + + aut_root = aut_cur = NULL; + +#ifdef VERBOSE + printf("Read complete network!\n"); +#endif +} + +AutNet +get_autnet(void) +{ + autnet.ppts = properties_root; /* zwracamy dodatkowo wlasnosci do zweryfikowania */ + return autnet; +} + diff --git a/anread.h b/anread.h new file mode 100644 index 0000000..fb2d645 --- /dev/null +++ b/anread.h @@ -0,0 +1,52 @@ +#ifndef _INC_ANREAD_H_ +#define _INC_ANREAD_H_ + +#include "antypes.h" +#include + +// #define VERBOSE /* brzydko ;) */ + +/** prototypy **/ + +void clocks_append(char *); +void clocks_mkmap(void); +Clock_idx *clocks_mkarr(void); +/*void clocks_free(void);*/ +void constr_append(Clock_idx, Clock_idx, Constr_rel, int); +Constr *constrs_mkarr(void); +Clock_idx get_clock_idx(Clock *, Clock_idx, char *); +Clock_idx get_cur_clock_idx(char *); +char *get_clock_name(Clock *, Clock_idx); +char *get_cur_clock_name(Clock_idx); +void clocks_show(Clock *, Clock_idx); +void constrs_show(Constr *, Clock *); +void trans_append(Loc_idx, Loc_idx, Act_idx); +void trans_show(Trans_set **, Loc *, Loc_idx, Clock *, Act *); +void trans_clocks_show(Trans_set *, Clock *); +void cur_trans_show(void); +Loc_idx get_loc_idx(Loc *, Loc_idx, char *); +Loc_idx get_cur_loc_idx(char *); +char *get_loc_name(Loc *, Loc_idx); +char *get_cur_loc_name(Loc_idx); +void locations_append(char *); +void set_loc_type(Loc_type); +void locations_mkmap(void); +void locations_show(Loc *, Loc_idx, Clock *); +void actions_append(char *); +void set_act_type(Act_type); +void actions_mkmap(void); +Act_idx get_act_idx(Act *, Act_idx, char *); +Loc_idx get_cur_act_idx(char *); +char *get_act_name(Act *, Act_idx); +char *get_cur_act_name(Act_idx); +void actions_show(Act *, Act_idx); +void act_mark_used(Act_idx); +void property_got_one(char *); +void property_append_loc(char *, char *); +Property_set *get_properties(void); +Aut_idx get_aut_idx(char *); +void complete_automaton(char *); +void complete_net(void); +AutNet get_autnet(void); + +#endif /* !_INC_ANREAD_H_*/ diff --git a/antclass.c b/antclass.c new file mode 100644 index 0000000..0cf7a0b --- /dev/null +++ b/antclass.c @@ -0,0 +1,755 @@ +/** antclass.c **/ + +/* + * Manipulacje klasami abstrakcyjnymi, tworzenie nowych, + * modyfikowanie ich parametrow, sprawdzanie, etc. + */ + +#include +#include +#include +#include +#include "antclass.h" +#include "anpsmod.h" +#include "anproc.h" +#include "antypes.h" +#include "anmacro.h" +#include "macro.h" +#include "dbm.h" + +/* + * Tworzenie klasy + */ +TimedClass_set * +tclass_create(ProdLoc_set *loc, DBM_elem *zone, DBM_elem *cor, dpt_t depth) +{ + TimedClass_set *new_tclass; + + new_tclass = tclass_create_nd(loc, zone, cor); + new_tclass->depth = depth; + + return new_tclass; +} + +/* + * Tworzenie klasy bez okreslania glebokosci + */ +TimedClass_set * +tclass_create_nd(ProdLoc_set *loc, DBM_elem *zone, DBM_elem *cor) +{ + TimedClass_set *new_tclass; + + new_tclass = smalloc(sizeof(TimedClass_set)); + new_tclass->dbm = zone; + new_tclass->cor_dbm = cor; + /*new_tclass->depth = depth;*/ + new_tclass->loc_set = loc; + new_tclass->rs = NULL; + new_tclass->stable_pre = NULL; + new_tclass->stable_succ = NULL; + new_tclass->next = NULL; + + return new_tclass; +} + +/* + * Tworzenie domyslnej klasy wyjsciowej dla odkrytej lokacji + */ +TimedClass_set * +tclass_create_base(ProdLoc_set *loc) +{ + /* Nowa klasa rowna niezmiennikowi (z cor rownym rowniez niezmiennikowi) */ + return tclass_create(loc, NULL, NULL, DEPTH_INF); +} + +/* + * Dodawanie klasy do zbioru klas (przyczepianie do odpowiedniej lokacji) + */ +void +tclass_add(TimedClass_set *tclass) +{ + ProdLoc_set *loc; + +#ifdef TC_VERBOSE + printf("tclass_add (%p): ", tclass); tclass_print(tclass); printf("\n"); +#endif + + loc = tclass->loc_set; + + if (!loc->classes) + loc->classes = tclass; + else + loc->last_class->next = tclass; + loc->last_class = tclass; +} + +/* + * Usuwanie klasy ze zbioru wszystkich klas nalezacych do podzialu + * + * przez koniecznosc szukania poprzedniego elementu listy moze byc + * nieco bolesne, ale oszczedzamy troche pamieci ;) + * + * W praktyce na razie funkcja okazuje sie raczej nieprzydatna, bo + * wykorzystujemy istniejace klasy i zmieniamy w nich strefy. + * + * UWAGA: brakuje usuwania informacji o klasach stabilnych (trzeba + * zwolnic pamiec). + */ +// void +// tclass_del(TimedClass_set *tclass) +// { +// ProdLoc_set *loc; +// TimedClass_set *tmp, *prev = NULL; +// +// loc = tclass->loc_set; +// +// for (tmp = loc->classes; tmp; prev = tmp, tmp = tmp->next) +// { +// if (tmp == tclass) +// { +// if (prev) /* usuwamy dalej niz z poczatku */ +// { +// prev->next = tmp->next; +// +// /* usuwamy z konca */ +// if (tmp == loc->last_class) +// loc->last_class = prev; +// } +// else /* usuwamy z poczatku */ +// { +// loc->classes = tmp->next; +// /* tutaj nie aktualizujemy last_class, bo jak korzen +// * bedzie NULL, to nie patrzymy na last_class. +// */ +// } +// +// if (tmp->dbm) dbm_destroy(tmp->dbm); +// if (tmp->cor_dbm) dbm_destroy(tmp->cor_dbm); +// free(tmp); +// +// return; +// } +// } +// +// assert(0); /* jesli jestesmy tutaj, to nie znalezlismy klasy do usuniecia */ +// } + +void +tclass_print(TimedClass_set *tc) +{ + printf("{"); prod_loc_show(tc->loc_set->loc); + printf(" Z="); + dbm_xprint(tclass_readZoneDBM(tc), dbm_size); + if (!tc->dbm) printf("=(inv)"); + printf(" Cor="); + if (tc->cor_dbm) + dbm_xprint(tc->cor_dbm, dbm_size); + else + printf("(zone)"); + printf(" dpt="); + if (tc->depth != DEPTH_INF) + printf("%u", tc->depth); + else + printf("inf"); + printf("} "); +} + +/* + * Funkcja zwracajaca adres DBM ze strefa klasy w celu jego ODCZYTANIA + * UWAGA: nie jest tworzona kopia, uwazac zeby nie zmodyfikowac! + */ +DBM_elem * +tclass_readZoneDBM(TimedClass_set *tclass) +{ + if (!tclass->dbm) return tclass->loc_set->inv; + else return tclass->dbm; +} + +/* + * Funkcja zwracajaca adres DBM z cor klasy w celu jego ODCZYTANIA + * UWAGA: nie jest tworzona kopia, uwazac zeby nie zmodyfikowac! + */ +DBM_elem * +tclass_readCorDBM(TimedClass_set *tclass) +{ + /* jesli cor == NULL, to jest taki sam jak zone */ + if (!tclass->cor_dbm) return tclass_readZoneDBM(tclass); + else return tclass->cor_dbm; /* cor ustawiony jawnie (niedomyslny) */ +} + +/* + * Funkcja zwracajaca strefe klasy gotowa do modyfikowania + */ +DBM_elem * +tclass_writeZoneDBM(TimedClass_set *tclass) +{ + if (!tclass->dbm) tclass->dbm = dbm_copy(tclass->loc_set->inv, dbm_size); + + return tclass->dbm; +} + +/* + * Funkcja zwracajaca cor klasy gotowy do modyfikowania + */ +DBM_elem * +tclass_writeCorDBM(TimedClass_set *tclass) +{ + if (!tclass->cor_dbm) tclass->cor_dbm = dbm_copy(tclass_readZoneDBM(tclass), dbm_size); + + return tclass->cor_dbm; +} + +/* + * Funkcje pomocnicze do przenoszenia DBM-ow do nowych klas + * (unikanie kopiowania) + * + * Po uzyciu ktorejs z nich klasa jest zdegenerowana, + * tzn. cor i zone moga nie odpowiadac wlasciwej klasie. + */ +/* +DBM_elem * +tclass_consumeZoneDBM(TimedClass_set *tclass) +{ + DBM_elem *rlt; + + rlt = tclass_writeZoneDBM(tclass); + tclass->dbm = NULL; + + return rlt; +} + +DBM_elem * +tclass_consumeCorDBM(TimedClass_set *tclass) +{ + DBM_elem *rlt; + + rlt = tclass_writeCorDBM(tclass); + tclass->cor_dbm = NULL; + + return rlt; +} +*/ + +/* + * Podmienianie strefy klasy, cor domyslnie taki sam jak calosc klasy + */ +void +tclass_replaceZoneDBM(TimedClass_set *tclass, DBM_elem *new_dbm) +{ + DBM_elem *tmp; + + assert(!dbm_empty(new_dbm, dbm_size)); + +#ifdef TC_VERBOSE + printf("tclass_replaceZoneDBM: nowy zone dla klasy (%p) ", tclass); tclass_print(tclass); + printf("; nowy zone: "); dbm_xprint(new_dbm, dbm_size); printf("\n"); +#endif + + tmp = tclass->dbm; + tclass->dbm = dbm_copy(new_dbm, dbm_size); + if (tmp) dbm_destroy(tmp); + + if (tclass->cor_dbm) dbm_destroy(tclass->cor_dbm); + tclass->cor_dbm = NULL; +} + +/* + * Podmienianie cor klasy + */ +void +tclass_replaceCorDBM(TimedClass_set *tclass, DBM_elem *new_cor) +{ + DBM_elem *tmp; + + assert(!dbm_empty(new_cor, dbm_size)); + + tmp = tclass->cor_dbm; + tclass->cor_dbm = dbm_copy(new_cor, dbm_size); + + if (tmp) dbm_destroy(tmp); +} + +void +tclass_depthUpdateIncr(TimedClass_set *tclass, TimedClass_set *pre_tclass) +{ + dpt_t new_depth; + + if (pre_tclass->depth < DEPTH_INF-1) + { + new_depth = pre_tclass->depth+1; + if (new_depth < tclass->depth) + { + tclass->depth = new_depth; + } + } + else + { + FERROR("Depth overflow!"); + } +} + +/* + * Ustawianie glebokosci klasy na inf jesli nie zawiera + * ona stanu poczatkowego q0 + */ +void +tclass_depthUpdateInf(TimedClass_set *tclass) +{ + if (!tclass_hasInit(tclass)) + { + assert(!tclass->rs); /* jak inf, to nie moze byc w RS */ + tclass->depth = DEPTH_INF; + } +} + +/* + * Sprawdzanie czy klasa zawiera stan poczatkowy q0 + */ +bool +tclass_hasInit(TimedClass_set *tclass) +{ + DBM_elem *tmp; + bool has_init = false; + + if (tclass->loc_set == init_loc_set) /* zgodnosc lokacji */ + { + /*dbm_print(tclass_readZoneDBM(tclass), dbm_size);*/ + + assert(dbm_is_canonical(tclass_readZoneDBM(tclass), dbm_size)); + + tmp = dbm_intersection_cf(tclass_readZoneDBM(tclass), zeroDBM, dbm_size); + if (!dbm_empty(tmp, dbm_size)) has_init = true; + dbm_destroy(tmp); + } + + return has_init; +} + +/* + * Do poprawy. Trzeba troche zmienic struktury danych, bo to szukanie jest mordercze. + */ +bool +tclass_is_in_ReachStable(TimedClass_set *tclass) +{ + if (tclass->rs) return true; + else return false; +} + +/* + * Dodawanie klasy do zbioru reachable+stable klas + */ +void +tclass_ReachStable_add(TimedClass_set *new_class, TimedClassRS_set **root, TimedClassRS_set **cur) +{ + assert(new_class->depth != DEPTH_INF); + assert(tclass_ReachStable_is_sorted(*root)); + + if (!tclass_is_in_ReachStable(new_class)) + { + TimedClassRS_set *new, *pred; + + new = smalloc(sizeof(TimedClassRS_set)); + new->tclass = new_class; + new->stable = false; + + new_class->rs = new; + + if (!*root) + { + new->prev = NULL; + new->next = NULL; + *root = *cur = new; + } + else + { + /* cofamy sie do elementu o glebokosci nie wiekszej od naszej (po ktorym chcemy dodac nowy element) > */ + for (pred = *cur; pred->tclass->depth > new_class->depth; pred = pred->prev); + + new->next = pred->next; + new->prev = pred; /* poprzedni element to ostatnio dodany */ + if (pred->next) { + pred->next->prev = new; + } + pred->next = new; + + if (pred == *cur) *cur = new; + } + + } + + assert(tclass_ReachStable_is_sorted(*root)); +} + +/* + * Dodawanie klasy zawierajacej stan q0 do zbioru + */ +void +tclass_ReachStable_addInit(TimedClass_set *new_class, TimedClassRS_set **root, TimedClassRS_set **cur) +{ + TimedClassRS_set *new; + + if (!tclass_is_in_ReachStable(new_class)) + { + assert(new_class->depth != DEPTH_INF); + + new = smalloc(sizeof(TimedClassRS_set)); + new->tclass = new_class; + new->stable = false; + new->next = *root; /* pod nowy element podczepiamy korzen */ + new->prev = NULL; /* bo dodajemy na poczatku */ + + new_class->rs = new; + + if (!*root) /* jesli lista byla pusta, to trzeba zaktualizowac cur, bo nowy bedzie ostatni */ + { + *cur = new; + } + else + { + assert(*root != NULL); + (*root)->prev = new; + } + *root = new; /* lista zaczyna sie od nowego elementu */ + + assert(tclass_ReachStable_is_sorted(*root)); + } +} + +/* + * Usuwanie klasy ze zbioru klas + */ +void +tclass_ReachStable_delete(TimedClass_set *del_class, TimedClassRS_set **root, TimedClassRS_set **cur) +{ +#ifdef TC_VERBOSE + printf("Usuwam klase (%p) ze zbioru ReachStable: ", del_class); + tclass_print(del_class); +#endif + + if (tclass_is_in_ReachStable(del_class)) + { + TimedClassRS_set *tmpRS; + + tmpRS = del_class->rs; + + if (tmpRS->next) + tmpRS->next->prev = tmpRS->prev; + if (tmpRS->prev) + tmpRS->prev->next = tmpRS->next; + + if (tmpRS == *root) + *root = NULL; + else + if (tmpRS == *cur) *cur = tmpRS->prev; + + free(tmpRS); + del_class->rs = NULL; + +#ifdef TC_VERBOSE + printf("faktycznie usuwana\n"); + tclass_ReachStable_print(*root); +#endif + + } +#ifdef TC_VERBOSE + else + { + printf("nie bylo co usuwac\n"); + } +#endif +} + +/* + * Zwalnianie pamieci przydzielonej na strukture zbioru (bez faktycznych klas) + */ +/*void +tclass_ReachStable_free(TimedClassRS_set **root) +{ +}*/ + +/* + * Oznaczanie klasy jako osiagalna i niestabilna (czyli dodawanie do zbioru) + */ +void +tclass_mark_reach_unst(TimedClass_set *tclass, TimedClassRS_set **root, TimedClassRS_set **cur) +{ + tclass_ReachStable_add(tclass, root, cur); +} + +/* + * Oznaczanie klasy jako osiagalna (dodawanie klasy do zbioru reachable) + */ +void +tclass_rs_mark_stable(TimedClassRS_set *tclass_rs) +{ + tclass_rs->stable = true; +} + +/* + * Znajdowanie klasy tclass i oznaczanie jako stabilna + */ +void +tclass_mark_stable(TimedClass_set *tclass) +{ + assert(tclass->rs != NULL); + + tclass->rs->stable = true; +} + +/* + * Znajdowanie klasy tclass i oznaczanie jako niestabilna + */ +void +tclass_mark_unstable(TimedClass_set *tclass) +{ + if (tclass->rs) + tclass->rs->stable = false; +} + +/* + * Oznaczanie wszystkich poprzednikow danej klasy jako niestabilne + */ +void +tclass_mark_preds_unstable(TimedClass_set *tclass) +{ + SrcLoc_set *src_loc; + TimedClass_set *tclass_src; + ProdTrans_set *trans_e; + + for (src_loc = tclass->loc_set->src_locs; src_loc; src_loc = src_loc->next) + { + for (tclass_src = src_loc->loc_set->classes; tclass_src; tclass_src = tclass_src->next) + { + for (trans_e = src_loc->trans; trans_e; trans_e = trans_e->next) + { + if (!psmodel_pre_empty(trans_e, src_loc->loc_set, tclass->loc_set, + tclass_readZoneDBM(tclass_src), tclass_readZoneDBM(tclass))) + { + tclass_mark_unstable(tclass_src); + } + } + } + } +} + +TimedClassRS_set * +tclass_pickReachUnst(TimedClassRS_set *root) +{ + TimedClassRS_set *curRS; + + assert(tclass_ReachStable_is_sorted(root)); + + /* szukamy pierwszego niestabilnego elementu (od korzenia) */ + for (curRS = root; curRS; curRS = curRS->next) + { + if (curRS->stable == false) + { + return curRS; + } + } + + return NULL; +} + +/* + * Sprawdzanie czy lista ReachStable jest posortowana + */ +bool +tclass_ReachStable_is_sorted(TimedClassRS_set *root) +{ + TimedClassRS_set *curRS; + dpt_t min_depth = 0; + + for (curRS = root; curRS; curRS = curRS->next) + { + if (curRS->tclass->depth < min_depth) + return false; + + min_depth = curRS->tclass->depth; + } + + return true; +} + +/* + * Wyswietlanie wszystkich stabilnych klas nalezacych do zbioru RS + */ +void +tclass_ReachStable_print(TimedClassRS_set *root) +{ + TimedClassRS_set *curRS; + idx_t i; + + for (curRS = root, i = 1; curRS; curRS = curRS->next, i++) + { + printf("(%u) (%p) ", i, curRS->tclass); tclass_print(curRS->tclass); + if (!curRS->stable) printf("UNSTABLE!!!"); + printf("\n"); + } +} + +/* + * Zapamietywanie stabilnego nastepnika + */ +void +tclass_saveStable(TimedClass_set *tcX, TimedClass_set *tcY) +{ + TClassPtr_set *new; + + assert(tclass_isReallyStableSucc(tcX, tcY)); + + if (!tclass_is_in_tcPtrs(tcY, tcX->stable_succ)) + { + new = smalloc(sizeof(TClassPtr_set)); + new->tclass = tcY; + new->next = tcX->stable_succ; + tcX->stable_succ = new; + } + + if (!tclass_is_in_tcPtrs(tcX, tcY->stable_pre)) + { + new = smalloc(sizeof(TClassPtr_set)); + new->tclass = tcX; + new->next = tcY->stable_pre; + tcY->stable_pre = new; + } +} + +/* + * Usuwanie informacji o poprzednikach stabilnych + * wzgledem danej klasy tcY. + */ +void +tclass_forgetPreStability(TimedClass_set *tcY) +{ + TClassPtr_set *tcptr; + + if (tcY->stable_pre) + { + for (tcptr = tcY->stable_pre; tcptr; ) + { + TClassPtr_set *tmp; + + /* zagladamy do kazdego poprzednika i usuwamy sie z jego stable_succ */ + tclass_tcPtrDel(tcY, &tcptr->tclass->stable_succ); + + tmp = tcptr; + tcptr = tcptr->next; + free(tmp); + } + tcY->stable_pre = NULL; + } +} + +/* + * Usuwanie informacji o nastepnikach wzgledem + * ktorych jest stabilna dana klasa tcX. + */ +void +tclass_forgetSuccStability(TimedClass_set *tcX) +{ + TClassPtr_set *tcptr; + + if (tcX->stable_succ) + { + for (tcptr = tcX->stable_succ; tcptr; ) + { + TClassPtr_set *tmp; + + /* zagladamy do kazdego nastepnika i usuwamy sie z jego stable_pre */ + tclass_tcPtrDel(tcX, &tcptr->tclass->stable_pre); + + tmp = tcptr; + tcptr = tcptr->next; + free(tmp); + } + tcX->stable_succ = NULL; + } +} + +void +tclass_tcPtrDel(TimedClass_set *tc, TClassPtr_set **tcptr) +{ + TClassPtr_set *tmp, *prev = NULL; + + for (tmp = *tcptr; tmp; prev = tmp, tmp = tmp->next) + { + if (tmp->tclass == tc) + { + if (prev) + prev->next = tmp->next; + else + *tcptr = tmp->next; + + free(tmp); + + return; + } + } +} + +bool +tclass_is_in_tcPtrs(TimedClass_set *tc, TClassPtr_set *tcptr) +{ + TClassPtr_set *tmp; + + for (tmp = tcptr; tmp; tmp = tmp->next) + if (tmp->tclass == tc) return true; + + return false; +} + +/* + * Sprawdzanie czy klasa tcY jest stabilnym nastepnikiem tcX + */ +bool +tclass_isStableSucc(TimedClass_set *tcX, TimedClass_set *tcY) +{ + if(tclass_is_in_tcPtrs(tcY, tcX->stable_succ)) + { + assert(tclass_isReallyStableSucc(tcX, tcY)); + return true; + } + else + { + return false; + } +} + +/* + * Sprawdzanie czy faktycznie mamy wlasciwie zapamietana stabilnosc + */ +bool +tclass_isReallyStableSucc(TimedClass_set *tcX, TimedClass_set *tcY) +{ + ProdTrans_set *trans_h; + + /* W rzeczywistosci interesuje nas tylko istnienie jakiegos przejscia dla ktorego jest AE */ + for (trans_h = trans_get(tcX->loc_set, tcY->loc_set); trans_h; trans_h = trans_h->next) + { + if (psmodel_pre_eq(tclass_readCorDBM(tcX), trans_h, tcX->loc_set, tcY->loc_set, + tclass_readCorDBM(tcX), tclass_readCorDBM(tcY))) + return true; + } + + return true; +} + +unsigned int +tclass_count(ProdLoc_set *locs) +{ + ProdLoc_set *loc; + unsigned int nclasses = 0; + + for (loc = locs; loc; loc = loc->next) + { + TimedClass_set *tclass; + + for (tclass = loc->classes; tclass; tclass = tclass->next) + { + nclasses++; + } + } + + return nclasses; +} diff --git a/antclass.h b/antclass.h new file mode 100644 index 0000000..5a7a689 --- /dev/null +++ b/antclass.h @@ -0,0 +1,54 @@ +#ifndef _INC_ANTCLASS_H_ +#define _INC_ANTCLASS_H_ + +#include +#include +#include "antypes.h" + +#ifndef NDEBUG + #define TC_VERBOSE +#endif + +#define DEPTH_INF UINT_MAX + +TimedClass_set *tclass_create(ProdLoc_set *, DBM_elem *, DBM_elem *, dpt_t); +TimedClass_set *tclass_create_nd(ProdLoc_set *, DBM_elem *, DBM_elem *); +TimedClass_set *tclass_create_base(ProdLoc_set *); +void tclass_print(TimedClass_set *); +void tclass_add(TimedClass_set *); +void tclass_del(TimedClass_set *); +ProdTrans_set *trans_get(ProdLoc_set *, ProdLoc_set *); +DBM_elem *tclass_readZoneDBM(TimedClass_set *); +DBM_elem *tclass_readCorDBM(TimedClass_set *); +DBM_elem *tclass_writeZoneDBM(TimedClass_set *); +DBM_elem *tclass_writeCorDBM(TimedClass_set *); +/*DBM_elem *tclass_consumeZoneDBM(TimedClass_set *); +DBM_elem *tclass_consumeCorDBM(TimedClass_set *);*/ +void tclass_replaceCorDBM(TimedClass_set *, DBM_elem *); +void tclass_replaceZoneDBM(TimedClass_set *, DBM_elem *); +void tclass_depthUpdateInf(TimedClass_set *); +void tclass_depthUpdateIncr(TimedClass_set *, TimedClass_set *); +bool tclass_hasInit(TimedClass_set *); +bool tclass_is_in_ReachStable(TimedClass_set *); +void tclass_ReachStable_add(TimedClass_set *, TimedClassRS_set **, TimedClassRS_set **); +void tclass_ReachStable_addInit(TimedClass_set *, TimedClassRS_set **, TimedClassRS_set **); +void tclass_ReachStable_delete(TimedClass_set *, TimedClassRS_set **, TimedClassRS_set **); +void tclass_ReachStable_free(TimedClassRS_set **); +void tclass_mark_reach_unst(TimedClass_set *, TimedClassRS_set **, TimedClassRS_set **); +void tclass_rs_mark_stable(TimedClassRS_set *); +void tclass_mark_stable(TimedClass_set *); +void tclass_mark_unstable(TimedClass_set *); +void tclass_mark_preds_unstable(TimedClass_set *); +TimedClassRS_set *tclass_pickReachUnst(TimedClassRS_set *); +bool tclass_ReachStable_is_sorted(TimedClassRS_set *); +void tclass_ReachStable_print(TimedClassRS_set *); +void tclass_saveStable(TimedClass_set *, TimedClass_set *); +void tclass_forgetPreStability(TimedClass_set *); +void tclass_forgetSuccStability(TimedClass_set *); +void tclass_tcPtrDel(TimedClass_set *, TClassPtr_set **); +bool tclass_is_in_tcPtrs(TimedClass_set *, TClassPtr_set *); +bool tclass_isStableSucc(TimedClass_set *, TimedClass_set *); +bool tclass_isReallyStableSucc(TimedClass_set *, TimedClass_set *); +unsigned int tclass_count(ProdLoc_set *); + +#endif /* !_INC_ANTCLASS_H_ */ diff --git a/antypes.h b/antypes.h new file mode 100644 index 0000000..2a81725 --- /dev/null +++ b/antypes.h @@ -0,0 +1,212 @@ +#ifndef _INC_ANTYPES_H_ +#define _INC_ANTYPES_H_ + +#include +#include "dbm.h" + +typedef unsigned int idx_t; + +typedef idx_t Aut_idx; +typedef idx_t Loc_idx; +typedef idx_t Act_idx; +typedef idx_t Constr_idx; + +/* Clock_idx nie jest unsigned, bo ujemne wartosci uzywane jako oznaczenie konca listy */ +typedef int Clock_idx; + +typedef unsigned int dpt_t; + +typedef unsigned int Constr_rel; +typedef char *Clock; +typedef unsigned int Loc_type; + +typedef struct constr { + Clock_idx l_clk; + Clock_idx r_clk; + Constr_rel rel; + int val; +} Constr; + +typedef struct constr_set { + Constr constr; + struct constr_set *next; +} Constr_set; + +typedef struct loc { + char *name; + Constr *inv; + Loc_type type; +} Loc; + +typedef struct loc_set { + Loc loc; + struct loc_set *next; +} Loc_set; + +typedef unsigned int Act_type; + +typedef struct act { + char *name; + Act_type type; +} Act; + +/* zbior akcji */ +typedef struct act_set { + Act act; + struct act_set *next; +} Act_set; + +/* zbior zegarow */ +typedef struct clock_set { + Clock clock; + struct clock_set *next; +} Clock_set; + +/* zbior przejsc */ +typedef struct transition_set { + Act_idx act; + Constr *guard; + Clock_idx *clocks; + Clock_idx nclocks; + struct transition_set *next; +} Trans_set; + +/* automat */ +typedef struct automaton { + char *name; /* nazwa automatu */ + Clock_idx nclks; /* liczba zegarow */ + Clock *clks; /* zegary */ + Loc_idx nloc; /* liczba lokacji */ + Loc *loc; /* lokacje */ + Loc_idx init_loc; /* lokacja poczatkowa */ + Trans_set **trans; /* tranzycje */ + bool *uact; /* akcje uzywane w automacie */ +} Aut; + +/* zbior automatow */ +typedef struct automaton_set { + char *name; /* nazwa automatu */ + Clock_idx nclks; /* liczba zegarow */ + Clock *clks; /* zegary */ + Loc_idx nloc; /* liczba lokacji */ + Loc *loc; /* lokacje */ + Loc_idx init_loc; /* lokacja poczatkowa */ + Trans_set **trans; /* tranzycje */ + bool *uact; /* akcje uzywane w automacie */ + struct automaton_set *next; +} Aut_set; + +/* wlasnosci: konfiguracja lokacji */ +typedef struct prod_conf_set { + Aut_idx aut; + Loc_idx loc; + struct prod_conf_set *next; +} ProdConf_set; + +/* wlasnosci: szukane konfiguracje lokacji */ +typedef struct property_set { + ProdConf_set *prop; + char *name; + struct property_set *next; +} Property_set; + +/* siec automatow */ +typedef struct autnet { + Aut *aut; + Aut_idx naut; + Act *act; + Act_idx nact; + Property_set *ppts; /* wlasnosci sieci */ +} AutNet; + +/* zbior lokacji produktowych */ +typedef struct prod_loc_set { + Loc_idx *loc; + DBM_elem *inv; + struct src_ploc_set *src_locs; /* lokacje z ktorych ta lokacja jest osiagalna (+przejscia) */ + struct src_ploc_set *last_src_loc; /* zapisujemy ostatnio dodana lokacje zrodlowa */ + struct dst_ploc_set *dst_locs; /* lokacje docelowe osiagalne przez przejscia z tej lokacji */ + bool trans_complete; + struct timed_class_set *classes; + struct timed_class_set *last_class; + struct prod_loc_set *next; +} ProdLoc_set; + +/* struktura do grupowania przejsc ze wzgledu na lokacje docelowa (wiazana z lokacja zrodlowa) */ +typedef struct dst_ploc_set { + struct prod_trans_set *trans; /* struktura z odkrytymi przejsciami */ + struct prod_trans_set *last_trans; /* ostatnio dodane przejscie */ + struct prod_loc_set *loc_set; /* lokacja docelowa */ + struct dst_ploc_set *next; +} DstLoc_set; + +/* + * struktura do zapisu lokacji z ktorych mozna sie dostac do biezacej; dodatkowo zawiera + * wskaznik na pierwszy element listy przejsc do niej prowadzacych. + */ +typedef struct src_ploc_set { + struct prod_loc_set *loc_set; /* lokacja zrodlowa */ + struct prod_trans_set *trans; /* lista przejsc (ten sam kawalek pamieci co w dst_ploc_set) */ + struct src_ploc_set *next; +} SrcLoc_set; + +typedef struct clock_idx_set { + Clock_idx idx; + struct clock_idx_set *next; +} ClockIdx_set; + +typedef struct prod_trans_set { + Act_idx act; + DBM_elem *guard; + ClockIdx_set *clocks; /* zegary do zresetowania */ + struct prod_trans_set *next; +} ProdTrans_set; + +typedef struct prod_trans_loc_set { + Act_idx act; + DBM_elem *guard; + ClockIdx_set *clocks; /* zegary do zresetowania */ + Loc_idx *loc; /* docelowa lokacja */ + struct prod_trans_loc_set *next; +} ProdTrLoc_set; + +typedef struct trans_loc_set { + Trans_set *trans; + Loc_idx loc; + struct trans_loc_set *next; +} TrLoc_set; + +typedef struct prod_clock { + Aut_idx par_aut; /* automat-rodzic (skladowy) */ + Clock_idx par_idx; /* index zegara u rodzica */ +} ProdClock; + +/* Zbior reachable-stable */ +struct timed_class_rs_set { + struct timed_class_set *tclass; + bool stable; /* czy klasa nalezy do zbioru stable */ + struct timed_class_rs_set *next; + struct timed_class_rs_set *prev; +}; +typedef struct timed_class_rs_set TimedClassRS_set; + +struct timed_class_set { + DBM_elem *dbm; /* strefa */ + DBM_elem *cor_dbm; /* cor klasy */ + unsigned int depth; + ProdLoc_set *loc_set; /* wskaznik na element zbioru z lokacjami (wraz z niezmiennikami) */ + struct timed_class_rs_set *rs; + struct timed_class_ptr_set *stable_pre; /* poprzedniki ktore sa stabilne ze wzgledu na ta klase */ + struct timed_class_ptr_set *stable_succ; /* nastepniki ze wzgledu na ktore ta klasa jest stabilna */ + struct timed_class_set *next; +}; +typedef struct timed_class_set TimedClass_set; + +struct timed_class_ptr_set { + struct timed_class_set *tclass; + struct timed_class_ptr_set *next; +}; +typedef struct timed_class_ptr_set TClassPtr_set; + +#endif /* !_INC_ANTYPES_H_ */ + diff --git a/dbm.c b/dbm.c new file mode 100644 index 0000000..372328a --- /dev/null +++ b/dbm.c @@ -0,0 +1,1348 @@ +/** dbm.c **/ + +/* + * Operacje na macierzach ograniczen roznic + */ + +#include +#include +#include +#include "dbm.h" +#include "dbm_macro.h" +#include "macro.h" + +DBM_elem * +dbm_init(DBM_idx dim) +{ + DBM_elem *p; + DBM_idx i, j; + + p = dbm_rawinit(dim); + + /* Poczatkowe wypelnianie macierzy */ + for (i = 0; i < dim; i++) + { + for (j = 0; j < dim; j++) + { + if (i == j || i == 0) /* pierwszy wiersz macierzy i przekatna: (0, <=) */ + { + DBM(p, dim, i, j) = DBM_E_0LE; + } + else /* pozostale: nieograniczone */ + { + DBM(p, dim, i, j) = INF; + } + } + } + + assert(dbm_is_sane(p, dim)); + + return p; +} + +DBM_elem * +dbm_init_zero(DBM_idx dim) +{ + DBM_elem *p; + DBM_idx i, j; + + p = dbm_rawinit(dim); + + for (i = 0; i < dim; i++) + { + for (j = 0; j < dim; j++) + { + DBM(p, dim, i, j) = DBM_E_0LE; + } + } + + assert(dbm_is_sane(p, dim)); + + return p; +} + +DBM_elem * +dbm_init_empty(DBM_idx dim) +{ + DBM_elem *p; + + p = dbm_init(dim); + DBM_MARK_EMPTY(p); + + return p; +} + +DBM_elem * +dbm_rawinit(DBM_idx dim) +{ + return (DBM_elem *)smalloc((dim*dim)*sizeof(DBM_elem)); +} + +DBM_elem * +dbm_copy(DBM_elem *p, DBM_idx dim) +{ + DBM_elem *r; + + assert(p && dim); + + r = dbm_rawinit(dim); + memcpy(r, p, sizeof(DBM_elem)*dim*dim); + + return r; +} + +void +dbm_print_elem(DBM_elem e) +{ + if (e == INF) + printf("inf "); + else + { + printf("(%d,", e >> 1); + switch (e & 1) + { + case REL_LE: /* najmniej znaczacy bit - 1 */ + printf("<=) "); + break; + case REL_LT: /* najmniej znaczacy bit - 0 */ + printf(" <) "); + break; + } + } + + return; +} + + +void +dbm_print(DBM_elem *p, DBM_idx dim) +{ + DBM_idx i, j; + + if (!p) + { + FERROR("dbm_print: p == NULL"); + } + + for (i = 0; i < dim; i++) + { + printf("[ "); + for (j = 0; j < dim; j++) + { + dbm_print_elem(DBM(p, dim, i, j)); + } + printf("]\n"); + } + + return; +} + +/* + * Wyswietlanie elementow w zhumanizowanej postaci ;) + * + * Pisane na kolanie, wiec mozna byloby to przemyslec... + */ +void +dbm_xprint_elem(DBM_elem *p, DBM_idx dim, DBM_idx i, DBM_idx j) +{ + DBM_elem e; + + e = DBM(p, dim, i, j); + + if (j == 0) { + printf("[x%d%s%d]", i, (e==INF?"inf":((e&1)==REL_LE?"<=":"<")), e >> 1); + + } + else + { + if (i == 0) + { + printf("[x%d%s%d]", j, (e==INF?"inf":((e&1)==REL_LE?">=":">")), -(e >> 1)); + } + else + { + printf("[x%d-x%d%s%d]", i, j, (e==INF?"inf":((e&1)==REL_LE?"<=":"<")), e >> 1); + } + } + + return; +} + +/* + * Wyswietlanie kanonicznych DBM-ow + */ +void +dbm_xprint(DBM_elem *p, DBM_idx dim) +{ + DBM_idx i, j; + bool f = false; + + if (dbm_empty(p, dim)) + printf("Empty"); + + for (i = 0; i < dim; i++) + { + for (j = 0; j < dim; j++) + { + if (i == j || i == 0) + { + if (DBM(p, dim, i, j) != DBM_E_0LE) + { + f = true; + dbm_xprint_elem(p, dim, i, j); + } + } + else + { + if (DBM(p, dim, i, j) != INF) + { + f = true; + dbm_xprint_elem(p, dim, i, j); + } + } + } + } + if (!f) printf("Default"); +} + +/* Ustawianie ograniczen */ +void +dbm_constr_le(DBM_elem *p, DBM_idx dim, DBM_idx i, DBM_idx j, int val) +{ + assert(i < dim && j < dim); + assert(i != j); /* nie wolno modyfikowac przekatnej */ + + DBM(p, dim, i, j) = DBM_VSC(DBM_ELEM(val, REL_LE)); + + return; +} + +void +dbm_constr_lt(DBM_elem *p, DBM_idx dim, DBM_idx i, DBM_idx j, int val) +{ + assert(i < dim && j < dim); + assert(i != j); /* nie wolno modyfikowac przekatnej */ + + DBM(p, dim, i, j) = DBM_VSC(DBM_ELEM(val, REL_LT)); + + return; +} + +/* Uwalnianie ograniczenia */ +void +dbm_rls_constr(DBM_elem *p, DBM_idx dim, DBM_idx i, DBM_idx j) +{ + assert(i < dim && j < dim); + assert(i != j); /* nie wolno modyfikowac przekatnej */ + + DBM(p, dim, i, j) = INF; + + assert(dbm_is_sane(p, dim)); + + return; +} + + +/* + * Sprowadzamy DBM do postaci kanonicznej (Floyd-Warshall) + * + * p = {0, 1, 2, ..., dim-1} + * + * for (k in p) + * for (i in p) + * for (j in p) + * if (a[i,j] > a[i,k] + a[k,j]) then + * a[i,j] = a[i,k] + a[k,j] + * + */ +void +dbm_canonicalize(DBM_elem *p, DBM_idx dim) +{ + DBM_idx k, i, j; + DBM_elem *e, sum; + + assert(p != NULL); + assert(dbm_valid_val(p, dim)); + + for (k = 0; k < dim; k++) + { + for (i = 0; i < dim; i++) + { + for (j = 0; j < dim; j++) + { + e = DBM_P(p, dim, i, j); + sum = DBM_SUM(DBM(p, dim, i, k), DBM(p, dim, k, j)); + if (*e > sum) + { + *e = DBM_LVSC(sum); + } + + if (i == j && *e < DBM_E_0LE) + { + /* + * Nie obliczamy do konca post. kanonicznej jesli pojawia element ujemny na przekatnej, + * bo i tak mozna to robic w nieskonczonosc. Wtedy natychmiast oznaczamy strefe jako + * pusta. Dzieki temu strefy ktorych DBM-y sprowadzalismy do post. kanonicznej szybko + * sprawdza sie pod katem pustosci. + */ + DBM_MARK_EMPTY(p); + return; + } + + } + } + } + + assert(dbm_valid_val(p, dim)); + + return; +} + +/* + * Specjalizowany Floyd-Warshal Rokickiego do obliczania + * postaci kanonicznej DBM po wniesieniu jednej zmiany + * do kanonicznego DBM, ktora zaciesnia ograniczenie. + * + * a[x,y] - zmodyfikowany element + * p = {0, 1, 2, ..., dim-1} + * + * for (j in p) + * if (a[x,j] > a[x,y] + a[y,j]) then + * a[x,j] = a[x,y] + a[y,j] + * for (i in p) + * if (a[i,y] > a[i,x] + a[x,y]) then + * a[i,y] = a[i,x] + a[x,y] + * for (j in p) + * if (a[i,j] > a[i,y] + a[y,j]) then + * a[i,j] = a[i,y] + a[y,j] + * + * Odwolanie do pracy Rokickiego odnalezione w kodzie biblioteki DBM Uppaala. + * Stad tez pomysl dobierania sposobu kanonizacji. Metoda przekazywania + * zbioru indeksow elementow zmodyfikowanych jest silnie zainspirowana Uppaalem. + * + * Funkcja zwraca prawde jesli strefa nie jest pusta, w przeciwnym wypadku falsz. + */ +bool +dbm_canon1(DBM_elem *p, DBM_idx dim, DBM_idx x, DBM_idx y) +{ + DBM_idx i, j; + DBM_elem *e, sum; + + assert(p != NULL); + assert(dbm_valid_val(p, dim)); + + for (j = 0; j < dim; j++) + { + e = DBM_P(p, dim, x, j); + sum = DBM_SUM(DBM(p, dim, x, y), DBM(p, dim, y, j)); + if (*e > sum) + { + *e = DBM_LVSC(sum); + } + } + if (DBM(p, dim, x, x) < DBM_E_0LE) /* strefa pusta? */ + { + DBM_MARK_EMPTY(p); + return false; + } + + for (i = 0; i < dim; i++) + { + e = DBM_P(p, dim, i, y); + sum = DBM_SUM(DBM(p,dim, i, x), DBM(p, dim, x, y)); + if (*e > sum) + { + *e = DBM_LVSC(sum); + + for (j = 0; j < dim; j++) + { + e = DBM_P(p, dim, i, j); + sum = DBM_SUM(DBM(p,dim, i, y), DBM(p, dim, y, j)); + if (*e > sum) { + *e = DBM_LVSC(sum); + } + } + } + if (DBM(p, dim, i, i) < DBM_E_0LE) /* strefa pusta? */ + { + DBM_MARK_EMPTY(p); + return false; + } + } + + assert(dbm_valid_val(p, dim)); + assert(dbm_is_canonical(p, dim)); + + return true; +} + + +/* + * Specjalizowany Floyd-Warshall do obliczania postaci + * kanonicznej po wniesieniu kliku zmian do kanonicznego DBM, + * ktore zaciesniaja ograniczenia. + * + * p = {0, 1, 2, ..., dim-1} + * f - zbior indeksow elementow zmodyfikowanych + * + * for (k in f) + * for (i in p) + * for (j in p) + * if (a[i,j] > a[i,k] + a[k,j]) then + * a[i,j] = a[i,k] + a[k,j] + * + */ +void +dbm_scanon(DBM_elem *p, DBM_idx dim, DBM_idx_flags *f) +{ + DBM_idx i, j, k; + DBM_elem *e, sum; + + assert(p != NULL); + assert(dbm_valid_val(p, dim)); + + for (k = 0; k < dim; k++) + { + if (IS_FLAGGED(f, k)) + { + + for (i = 0; i < dim; i++) + { + for (j = 0; j < dim; j++) + { + + e = DBM_P(p, dim, i, j); + + sum = DBM_SUM(DBM(p, dim, i, k), DBM(p, dim, k, j)); + if (*e > sum) + { + *e = DBM_LVSC(sum); + } + + if (i == j && *e < DBM_E_0LE) /* strefa pusta? */ + { + DBM_MARK_EMPTY(p); + return; + } + + } + } + + } + } + + assert(dbm_valid_val(p, dim)); + assert(dbm_is_canonical(p, dim)); + + return; +} + +bool +dbm_is_canonical(DBM_elem *p, DBM_idx dim) +{ + DBM_idx k, i, j; + DBM_elem *e; + + assert(p != NULL); + /* + * Jesli strefa ma element ujemny na przekatnej, to uznajemy, ze mamy postac kanoniczna. + * W przeciwnym wypadku nie bylibysmy w stanie tego stwierdzic badajac czy algorytm + * obliczajacy postac kanoniczna nanosi jakies zmiany, poniewaz nanosilby je do + * nieskonczonosci (teoretycznie). + */ + for (i = 0; i < dim; i++) + { + if (DBM(p, dim, i, i) < DBM_E_0LE) + return true; + } + + for (k = 0; k < dim; k++) + { + for (i = 0; i < dim; i++) + { + for (j = 0; j < dim; j++) + { + + e = DBM_P(p, dim, i, j); + + /* sprawdzamy czy algorytm wprowadzilby jakas zmiane w DBM */ + if (*e > DBM_SUM(DBM(p, dim, i, k), DBM(p, dim, k, j))) + return false; + + } + } + } + + return true; +} + +/* + * Porownywanie stref w postaciach kanonicznych + */ +bool +dbm_equal(DBM_elem *p, DBM_elem *q, DBM_idx dim) +{ + assert(dbm_is_canonical(p, dim)); + assert(dbm_is_canonical(q, dim)); + + if (dbm_empty(p, dim) && dbm_empty(q, dim)) + return true; /* obie strefy puste */ + /* Jesli chcemy pominac sprawdzenia dbm_empty, to trzeba byloby + * zmienic zalozenie o PK (komentarz w dbm_empty). + */ + + if (memcmp(p, q, sizeof(DBM_elem)*dim*dim) == 0) + return true; + else + return false; +} + +/* + * Sprawdzanie pustosci DBM w postaci kanonicznej + */ +bool +dbm_empty(DBM_elem *p, DBM_idx dim) +{ + int i; + + assert(p != NULL); + assert(dbm_is_canonical(p, dim)); + + if (*p < DBM_E_0LE) return true; + + /* + * Jesli dalej nie chcemy sprawdzac calej przekatnej, musielibysmy + * zmienic zalozenie dot. postaci kanonicznej. DBM bylby w postaci + * kanonicznej wtw gdy jesli strefa jest pusta, to DBM(0,0) < DBM_E_0LE + * (czyli jesli gdzies na przekatnej jest element < DBM_E_0LE, to + * wtedy rowniez DBM(0,0) < DBM_E_0LE). + */ + for (i = 1; i < dim; i++) + { + + if (DBM(p, dim, i, i) < DBM_E_0LE) + { + DBM_MARK_EMPTY(p); /* oznaczamy strefe aby kolejne sprawdzenia byly szybsze */ + return true; + } + + } + + return false; +} + +/* + * Obliczanie przeciecia dwoch stref + */ +DBM_elem * +dbm_intersection(DBM_elem *p, DBM_elem *q, DBM_idx dim) +{ + DBM_elem *r, *e; + DBM_idx i, j; + + assert(p != NULL && q != NULL); + + r = dbm_rawinit(dim); + + for (i = 0; i < dim; i++) + { + for (j = 0; j < dim; j++) + { + + e = DBM_P(r, dim, i, j); + *e = DBM_MIN(DBM(p, dim, i, j), DBM(q, dim, i, j)); + + if (i == j && *e < DBM_E_0LE) + { + /* + * Jesli gdzies na przekatnej pojawi sie liczba ujemna, + * wtedy strefe oznaczamy jako pusta i nic wiecej z nia + * nie robimy, bo i tak pozostanie pusta. + */ + DBM_MARK_EMPTY(r); + return r; + } + } + } + + dbm_canonicalize(r, dim); + + return r; +} + +/* + * Obliczanie liczby elementow tablicy mieszczacej bity odpowiadajace zegarom + */ +DBM_idx_flags * +get_flags_array(DBM_idx dim) +{ + return (DBM_idx_flags *)smalloc_zero(sizeof(DBM_idx_flags) * GET_ASIZE(dim)); +} + +/* + * Obliczanie przeciecia dwoch stref (w miejscu, modyfikuje p) + * + * p - DBM w postaci kanonicznej (z tym zalozeniem jest szybciej, + * a w praktyce nie jest ono trudne do spelnienia) + */ +void +dbm_intersection_cf_ip(DBM_elem *p, DBM_elem *q, DBM_idx dim) +{ + DBM_elem *e_p, *e_q; + DBM_idx i, j; + DBM_idx_flags *flags; + DBM_idx chg_i = 0, chg_j = 0; + unsigned int chg_cnt = 0; + + assert(p != NULL && q != NULL); + assert(dbm_valid_val(p, dim)); + assert(dbm_valid_val(q, dim)); + assert(dbm_is_canonical(p, dim)); + + e_p = p; + e_q = q; + + /* tablica do flagowania zmodyfikowanych indeksow */ + flags = get_flags_array(dim); + + for (i = 0; i < dim; i++) + { + for (j = 0; j < dim; j++) + { + + assert(e_p == DBM_P(p, dim, i, j)); /* czy na pewno biezacy element odpowiada temu, czego sie spodziewamy */ + assert(e_q == DBM_P(q, dim, i, j)); + + if (*e_p > *e_q) + { + + *e_p = *e_q; + + SET_FLAG(flags, i); /* flagujemy indeksy modyfikacji */ + SET_FLAG(flags, j); + + /* jesli jest szansa, ze bedzie to jedyna modyfikacja, to zapisujemy co zmodyfikowano */ + if (chg_cnt < 1) + { + chg_i = i; + chg_j = j; + } + chg_cnt++; /* zwiekszamy licznik modyfikacji */ + + } + + if (i == j && *e_p < DBM_E_0LE) + { + free(flags); + DBM_MARK_EMPTY(p); + return; + } + + e_p++; /* przechodzimy do kolejnych elementow */ + e_q++; + + } + } + + if (chg_cnt == 1) + { + dbm_canon1(p, dim, chg_i, chg_j); + } + else if (chg_cnt > 1) + { + dbm_scanon(p, dim, flags); + } + + free(flags); /* tablica flag juz jest zbedna */ + + assert(dbm_is_canonical(p, dim)); + + return; +} + +/* + * Obliczanie przeciecia dwoch stref, wejsciowy DBM p w postaci kanonicznej. + * + * W niektorych zastosowaniach jest to szybka metoda. Wystarczyloby udowodnic, + * ze zachowywanie postaci kanonicznej po kazdej najmniejszej zmianie w niczym + * nie przeszkadza. + * + * W praktyce weryfikacji niekoniecznie ma sens ;) + * + * (prototypowo) + */ +void +dbm_intersection_cfX_ip(DBM_elem *p, DBM_elem *q, DBM_idx dim) +{ + DBM_elem *e_p, *e_q; + DBM_idx i, j; + + assert(dbm_valid_val(p, dim)); + assert(dbm_valid_val(q, dim)); + assert(dbm_is_canonical(p, dim)); + + e_p = p; + e_q = q; + + for (i = 0; i < dim; i++) { + for (j = 0; j < dim; j++) { + + assert(e_p == DBM_P(p, dim, i, j)); /* czy na pewno biezacy element odpowiada temu, czego sie spodziewamy */ + assert(e_q == DBM_P(q, dim, i, j)); + + if (*e_p > *e_q) { + + *e_p = *e_q; + + if(!dbm_canon1(p, dim, i, j)) { + return; /* dbm_canon1 oznaczyl strefe jako pusta */ + } + + } + + /* Moze nie jest to oplacalne jednak? + * Jesli mamy p w PK i jesli nie jest oznaczona jako pusta to daje nam to tyle, ze + * zostanie oznaczona, ale wczesniej moze to zrobic tez dbm_canon1. + */ + if (i == j && *e_p < 0) { + *p = DBM_E_NEG; + return; + } + + e_p++; /* przechodzimy do kolejnych elementow */ + e_q++; + + } + } + + assert(dbm_is_canonical(p, dim)); + + return; +} + +/* + * Obliczanie przeciecia dwoch stref + * + * p - DBM w postaci kanonicznej (pozostaje nienaruszony) + */ +DBM_elem * +dbm_intersection_cf(DBM_elem *p, DBM_elem *q, DBM_idx dim) +{ + DBM_elem *x; + + assert(p != NULL && q != NULL); + + x = dbm_copy(p, dim); + dbm_intersection_cf_ip(x, q, dim); + + return x; +} + +/* + * Z[x:=0] + * Resetowanie zegara z zachowaniem postaci kanonicznej + * + * c - resetowany zegar + */ +void +dbm_reset(DBM_elem *p, DBM_idx dim, DBM_idx c) +{ + DBM_idx i; + + assert(p != NULL); + assert(dbm_is_canonical(p, dim)); + + for (i = 0; i < dim; i++) + { + + if (i != c) /* pomijamy DBM(i,i) */ + { + DBM(p, dim, c, i) = DBM(p, dim, 0, i); + DBM(p, dim, i, c) = DBM(p, dim, i, 0); + } + + } + + assert(dbm_is_canonical(p, dim)); + + return; +} + +/* + * [x:=0]Z + * + * c - resetowany zegar + */ +void +dbm_invreset(DBM_elem *p, DBM_idx dim, DBM_idx c) +{ + DBM_idx i; +#ifndef NDEBUG + DBM_elem *p_orig; +#endif + + assert(p != NULL); + assert(dbm_is_canonical(p, dim)); + +#ifndef NDEBUG + p_orig = dbm_copy(p, dim); +#endif + + if (DBM(p, dim, 0, c) == DBM_E_0LE) + { + /* + * Pomijamy: DBM(p, dim, c, 0) = DBM_E_0LE; + * bo zawiera sie to w nastepnym kroku. + * + * Zamiast obliczania postaci kanonicznej, + * poprawiamy tylko to co trzeba: + */ + for (i = 1; i < dim; i++) + DBM(p, dim, i, 0) = DBM(p, dim, i, c); + + for (i = 0; i < dim; i++) + if (i != c) DBM(p, dim, c, i) = INF; + + dbm_canonicalize(p, dim); + + } + else /* wynikiem operacji jest pusta strefa */ + { + DBM_MARK_EMPTY(p); + } + + assert(dbm_is_canonical(p, dim)); + +#ifndef NDEBUG + assert(dbm_check_invreset(p_orig, p, dim, c)); + dbm_destroy(p_orig); +#endif + + return; +} + +/* + * Sprawdzanie poprawnosci obliczania [x:=0]Z wzgledem pierwotnego algorytmu z AinV + * + * p - nienaruszony DBM (do obliczenia) + * q - wynikowy DBM do porownania + */ +bool +dbm_check_invreset(DBM_elem *p, DBM_elem *q, DBM_idx dim, DBM_idx c) +{ + DBM_idx i; + + assert(p != NULL && q != NULL); + + if (DBM(p, dim, 0, c) == DBM_E_0LE) + { + + DBM(p, dim, c, 0) = DBM_E_0LE; + dbm_canonicalize(p, dim); + + for (i = 0; i < dim; i++) + { + if (i != c) DBM(p, dim, c, i) = INF; + } + + dbm_canonicalize(p, dim); + + } + else + { + DBM_MARK_EMPTY(p); + } + + if (dbm_equal(p, q, dim)) + { + return true; + } + + printf("Inconsistency detected!\nExpected result:\n"); + dbm_print(p, dim); + printf("\nIncorrect result:\n"); + dbm_print(q, dim); + + return false; +} + +/* + * Obliczanie nastepnika czasowego (zachowuje postac kanoniczna) + */ +void +dbm_time_successor(DBM_elem *p, DBM_idx dim) +{ + int i; + + assert(p != NULL); + assert(dbm_is_canonical(p, dim)); + + for (i = 1; i < dim; i++) + { + DBM(p, dim, i, 0) = INF; + } + + assert(dbm_is_canonical(p, dim)); + + return; +} + +/* + * Obliczanie poprzednika czasowego (zachowuje postac kanoniczna) + */ +void +dbm_time_predecessor(DBM_elem *p, DBM_idx dim) +{ + int i, j; + DBM_elem *e1, *e2; + + assert(p != NULL); + assert(dbm_is_canonical(p, dim)); + + for (j = 1; j < dim; j++) + { + e1 = DBM_P(p, dim, 0, j); + *e1 = DBM_E_0LE; /* DBM(0,j) := (0, <=) */ + + for (i = 1; i < dim; i++) + { + e2 = DBM_P(p, dim, i, j); + + if (*e2 < *e1) /* DBM(i,j) < DBM(0,j) */ + { + *e1 = *e2; + } + } + + } + + assert(dbm_is_canonical(p, dim)); + + return; +} + + +/* + * Obliczanie poprzednika czasowego (nie zachowuje postaci kanonicznej) + */ +void +dbm_time_predecessor_nc(DBM_elem *p, DBM_idx dim) +{ + int j; + + assert(p != NULL); + assert(dbm_is_canonical(p, dim)); /* wejsciowy DBM musi byc w PK */ + + for (j = 1; j < dim; j++) + { + DBM(p, dim, 0, j) = DBM_E_0LE; /* DBM(0,j) := (0, <=) */ + } + + return; +} + + +/* + * Makro do rozluzniania ograniczen (zamiana < na <=) + * + * Dzialamy tylko jezeli DBM(i,j) != inf oraz DBM(i,j) z ograniczeniem <. + * Mimo ze obecnosc tego warunku nie jest konieczna, jest on oplacalny. + */ +#define DBM_RELAX_REL(i, j) \ +{ \ + DBM_elem *e; \ + e = DBM_P(p, dim, i, j); \ + if (*e != INF && (*e & 1) == REL_LT) *e |= 1; \ +} + +/* + * Domkniecie strefy (nie mylic z postacia kanoniczna) + */ +void +dbm_closure(DBM_elem *p, DBM_idx dim) +{ + DBM_idx i, j; + + assert(p != NULL); + assert(dbm_is_canonical(p, dim)); + + for (i = 0; i < dim; i++) + { + for (j = 0; j < dim; j++) + { + DBM_RELAX_REL(i, j); + } + } + + assert(dbm_is_canonical(p, dim)); + + return; +} + +void +dbm_fill(DBM_elem *p, DBM_idx dim) +{ + DBM_idx i; + + assert(p != NULL); + assert(dbm_is_canonical(p, dim)); + + /* zaczynamy od 1, bo DBM(0,0) nie potrzeba poprawiac */ + for (i = 1; i < dim; i++) + { + DBM_RELAX_REL(i, 0); + DBM_RELAX_REL(0, i); + } + + assert(dbm_is_canonical(p, dim)); + + return; +} + +/* wynik w PK */ +DBM_elem * +dbm_border(DBM_elem *p, DBM_elem *q, DBM_idx dim) +{ + DBM_elem *r; + + assert(p != NULL && q != NULL); + assert(dbm_is_canonical(p, dim)); + assert(dbm_is_canonical(q, dim)); + + r = dbm_intersection(p, q, dim); + if (!dbm_empty(r, dim)) + { + + /* strefy nie sa rozlaczne; wynik: domkniecie przeciecia */ + /* dbm_closure(r, dim); */ /* DO SPRAWDZENIA: hm, w rzeczywistosci to wcale nie closure? */ + return r; + + } + else + { + + DBM_idx i, j; + DBM_elem pe, qe; + + dbm_destroy(r); /* nie potrzebujemy juz przeciecia stref */ + + for (i = 1; i < dim; i++) + { + /* (1) szukamy: DBMp(i,0) = (c, <) i DBMq(0,i) = (-c, <=) */ + pe = DBM(p, dim, i, 0); + qe = DBM(q, dim, 0, i); + if (DBM_V(pe) == -DBM_V(qe) && DBM_R(pe) == REL_LT && DBM_R(qe) == REL_LE) + { + + for (j = 1; j < dim; j++) + { + /* (2) szukamy: DBMp(j,0) = (c, <=) i DBMq(0,j) = (-c, <), j != i*/ + pe = DBM(p, dim, j, 0); + qe = DBM(q, dim, 0, j); + if (j != i && DBM_V(pe) == -DBM_V(qe) && DBM_R(pe) == REL_LE && DBM_R(qe) == REL_LT) + { + /* wynik: pusta strefa */ + r = dbm_init(dim); + DBM_MARK_EMPTY(r); + return r; + } + } /* nie znalezlismy (2) */ + + /* wynik: Fill(Z) n Z' */ + dbm_fill(p, dim); + r = dbm_intersection(p, q, dim); + return r; + } + + } /* nie znalezlismy (1) */ + + for (i = 1; i < dim; i++) + { + /* (3) szukamy: DBMp(i,0) = (c, <=) i DBMq(0,i) = (-c, <) */ + pe = DBM(p, dim, i, 0); + qe = DBM(q, dim, 0, i); + if (DBM_V(pe) == -DBM_V(qe) && DBM_R(pe) == REL_LE && DBM_R(qe) == REL_LT) + { + /* wynik: Z n Fill(Z') */ + dbm_fill(q, dim); + r = dbm_intersection(p, q, dim); + return r; + } + } /* nie znalezlismy (3) */ + + /* wynik: pusta strefa */ + r = dbm_init(dim); + DBM_MARK_EMPTY(r); + return r; + } + +} + +/* Natychmiastowy poprzednik czasowy (w PK) */ +DBM_elem * +dbm_imm_time_predecessor(DBM_elem *p, DBM_elem *q, DBM_idx dim) +{ + DBM_elem *r, *t; + + assert(p != NULL && q != NULL); + assert(dbm_is_canonical(p, dim)); + assert(dbm_is_canonical(q, dim)); + + t = dbm_border(p, q, dim); + dbm_time_predecessor_nc(t, dim); + + r = dbm_intersection(p, t, dim); + + return r; +} + +/* + * Dodawanie kolejnych DBM-ow do zbioru + */ +void +dbmset_add(DBMset_elem **root, DBMset_elem **last, DBM_elem *dbm) +{ + DBMset_elem *new; + + new = (DBMset_elem *)smalloc(sizeof(DBMset_elem)); + + new->dbm = dbm; + new->next = NULL; + + if (*root == NULL) + *root = new; + else + (*last)->next = new; + *last = new; + + return; +} + +/* + * Odalokowywanie zbioru DBM-ow (lacznie z elementami zbioru) + */ +void +dbmset_destroy(DBMset_elem *root) +{ + DBMset_elem *cur, *tmp; + + cur = root; + while (cur != NULL) + { + assert(cur->dbm != NULL); + free(cur->dbm); + + tmp = cur; + cur = cur->next; + free(tmp); + } + + return; +} + +/* + * Odalokowywanie samej struktury zbioru DBM-ow + */ +void +dbmset_scaffoldDestroy(DBMset_elem *root) +{ + DBMset_elem *cur, *tmp; + + cur = root; + while (cur != NULL) + { + tmp = cur; + cur = cur->next; + free(tmp); + } + + return; +} + +/* + * Wyswietlanie DBM-ow nalezacych do zbioru + */ +void +dbmset_print(DBMset_elem *root, DBM_idx dim) +{ + DBMset_elem *cur; + unsigned int i = 1; + + cur = root; + while (cur != NULL) + { + printf("DBM %d:\n", i++); + dbm_print(cur->dbm, dim); + cur = cur->next; + } + + return; +} + +/* + * Obliczanie roznicy stref + */ +DBMset_elem * +dbm_diff(DBM_elem *p_orig, DBM_elem *q, DBM_idx dim) +{ + DBM_idx i, j; + DBMset_elem *r = NULL, *last = NULL; /* zbior stref */ + bool done = false, p_used = false; + DBM_elem *p, *q_c, *t, *z, w; + + assert(p_orig != NULL && q != NULL); + assert(dbm_is_canonical(p_orig, dim)); + assert(dbm_is_canonical(q, dim)); + + p = dbm_copy(p_orig, dim); /* p bedziemy modyfikowac */ + + q_c = dbm_copy(q, dim); + dbm_closure(q_c, dim); + + for (i = 0; i < dim && !done; i++) + { + for (j = 0; j < dim && !done; j++) + { + /* dodatkowe sprawdzanie != INF (dodane na szybko dla pewnosci, TODO: upewnic sie czy potrzebne) */ + if (i != j && DBM(q, dim, i, j) != INF) + { + + /* sprawdzamy przeciecie obu stref */ + t = dbm_intersection_cf(p, q, dim); /* t jest w PK */ + + if (dbm_empty(t, dim)) + { /* aktualne Z i Z' sa rozlaczne */ + + dbm_destroy(t); + + assert(dbm_is_canonical(p, dim)); + if (!dbm_empty(p, dim)) /* nie dodajemy pustych DBM-ow */ + { + dbmset_add(&r, &last, p); + p_used = true; /* p zostalo wykorzystane */ + assert(r != NULL); + } + /* nie trzeba zwalniac, bo !p_used (zwolni sie dalej) */ + + done = true; + + } + else if (dbm_equal(t, p, dim)) /* Z n Z' jest rowne aktualnemu Z */ + { + + dbm_destroy(t); + done = true; + + } + else + { + + dbm_destroy(t); + + t = dbm_copy(q_c, dim); + w = DBM_V(DBM(q, dim, i, j)); + DBM(t, dim, i, j) = DBM_ELEM(w, REL_LE); + DBM(t, dim, j, i) = DBM_ELEM(-w, REL_LE); + + z = dbm_intersection_cf(p, t, dim); /* z jest w PK */ + dbm_destroy(t); + + if (!dbm_empty(z, dim)) + { + + t = dbm_copy(p, dim); + w = DBM(q, dim, i, j); + DBM(t, dim, j, i) = DBM_ELEM(-DBM_V(w), DBM_INV_R(w)); + dbm_canonicalize(t, dim); /* przed dodaniem obliczamy PK, TODO: zastanowic sie czy + * nie mozna zoptymalizowac (to jest poprawka na szybko) + */ + if (!dbm_empty(t, dim)) /* nie dodajemy pustych DBM-ow */ + { + dbmset_add(&r, &last, t); /* potem nie zwalniamy t, bo juz zostalo "oddane" (inaczej bysmy je utracili) */ + assert(r != NULL); + } + else + { + dbm_destroy(t); + } + assert(w <= DBM(p, dim, i, j)); /* zawezanie ograniczenia */ + DBM(p, dim, i, j) = w; + dbm_canon1(p, dim, i, j); /* postac kanoniczna p potrzebna jest na wejsciu dbm_equal() */ + + } + + dbm_destroy(z); + + } + + } + } + } + + dbm_destroy(q_c); + if (!p_used) dbm_destroy(p); /* zwalniamy p tylko jesli nie jest uzywane: TODO moze lepiej operowac na 'if (p != NULL)'? */ + + return r; +} + +/* + * Sprawdzanie czy wartosci elementow zawieraja sie w dopuszczalnym przedziale. + */ +bool +dbm_valid_val(DBM_elem *p, DBM_idx dim) +{ + assert(p != NULL); + + while (dim-- != 0) + { + if ((*p < DBM_RAW_MIN || *p > DBM_RAW_MAX) && *p != INF) + { + return false; + } + p++; + } + + return true; +} + +/* + * Sprawdzanie czy DBM jest "zdrowy". + */ +bool +dbm_is_sane(DBM_elem *p, DBM_idx dim) +{ + DBM_idx i; + + assert(p != NULL); + + for (i = 0; i < dim; i++) + { + + /* Element > (0, <=) w pierwszym wierszu macierzy */ + if (DBM(p, dim, 0, i) > DBM_E_0LE) + { + printf("Negative clock valuation allowed!\n"); + return false; + } + + /* czy (0, <=) na calej przekatnej */ + if (DBM(p, dim, i, i) != DBM_E_0LE) + { + printf("Invalid element on a diagonal!\n"); + return false; + } + + } + + if (dbm_valid_val(p, dim)) + { + return true; + } + else + { + printf("Not allowed value found (dbm_valid_val check failed)!\n"); + return false; + } + + return true; +} diff --git a/dbm.h b/dbm.h new file mode 100644 index 0000000..d519dc9 --- /dev/null +++ b/dbm.h @@ -0,0 +1,76 @@ +#ifndef _INC_DBM_H_ +#define _INC_DBM_H_ + +#include +#include /* troche elegancji ;-) */ +#include +/* + * Asercje miejscami sa mocno naciagane, ale moga nas zabezpieczac + * przed samymi soba, wiec nie krepuje sie z ich stosowaniem. + */ + +typedef int DBM_elem; +typedef int DBM_val; +typedef int DBM_rel; +typedef unsigned int DBM_idx; +typedef unsigned int DBM_idx_flags; /* unsigned! */ + +typedef struct dbmset_elem { + DBM_elem *dbm; + struct dbmset_elem *next; +} DBMset_elem; + +/** prototypy **/ +DBM_elem *dbm_init(DBM_idx); +DBM_elem *dbm_init_zero(DBM_idx); +DBM_elem *dbm_init_empty(DBM_idx); +DBM_elem *dbm_rawinit(DBM_idx); +DBM_elem *dbm_copy(DBM_elem *, DBM_idx); +void dbm_print_elem(DBM_elem); +void dbm_xprint_elem(DBM_elem *, DBM_idx, DBM_idx, DBM_idx); +void dbm_print(DBM_elem *, DBM_idx); +void dbm_xprint(DBM_elem *, DBM_idx); +void dbm_constr_le(DBM_elem *, DBM_idx, DBM_idx, DBM_idx, int); +void dbm_constr_lt(DBM_elem *, DBM_idx, DBM_idx, DBM_idx, int); +void dbm_rls_constr(DBM_elem *, DBM_idx, DBM_idx, DBM_idx); +void dbm_canonicalize(DBM_elem *, DBM_idx); +bool dbm_canon1(DBM_elem *, DBM_idx, DBM_idx, DBM_idx); +void dbm_scanon(DBM_elem *, DBM_idx, DBM_idx_flags *); +bool dbm_is_canonical(DBM_elem *, DBM_idx); +bool dbm_equal(DBM_elem *, DBM_elem *, DBM_idx); +DBM_elem *dbm_intersection(DBM_elem *, DBM_elem *, DBM_idx); +DBM_idx_flags *get_flags_array(DBM_idx); +void dbm_intersection_cfX_ip(DBM_elem *p, DBM_elem *q, DBM_idx dim); +void dbm_intersection_cf_ip(DBM_elem *p, DBM_elem *q, DBM_idx dim); +DBM_elem *dbm_intersection_cf(DBM_elem *, DBM_elem *, DBM_idx); +bool dbm_empty(DBM_elem *, DBM_idx); +void dbm_reset(DBM_elem *, DBM_idx, DBM_idx); +void dbm_invreset(DBM_elem *, DBM_idx, DBM_idx); +bool dbm_check_invreset(DBM_elem *, DBM_elem *, DBM_idx, DBM_idx); +void dbm_time_successor(DBM_elem *, DBM_idx); +void dbm_time_predecessor(DBM_elem *, DBM_idx); +void dbm_time_predecessor_nc(DBM_elem *, DBM_idx); +void dbm_closure(DBM_elem *, DBM_idx); +void dbm_fill(DBM_elem *, DBM_idx); +DBM_elem *dbm_border(DBM_elem *, DBM_elem *, DBM_idx); +DBM_elem *dbm_imm_time_predecessor(DBM_elem *, DBM_elem *, DBM_idx); +void dbmset_add(DBMset_elem **, DBMset_elem **, DBM_elem *); +void dbmset_destroy(DBMset_elem *); +void dbmset_scaffoldDestroy(DBMset_elem *); +void dbmset_print(DBMset_elem *, DBM_idx); +DBMset_elem *dbm_diff(DBM_elem *, DBM_elem *, DBM_idx); +bool dbm_valid_val(DBM_elem *, DBM_idx); +bool dbm_is_sane(DBM_elem *, DBM_idx); + +/* + * Zwalnianie pamieci przydzielonej na DBM + */ +static inline void +dbm_destroy(DBM_elem *p) +{ + free(p); + + return; +} + +#endif /* !_INC_DBM_H_ */ diff --git a/dbm_macro.h b/dbm_macro.h new file mode 100644 index 0000000..cdbcda6 --- /dev/null +++ b/dbm_macro.h @@ -0,0 +1,82 @@ +#ifndef _INC_DBM_MACRO_H_ +#define _INC_DBM_MACRO_H_ + +#include + +/* + * Definicje dla czytelnosci, a nie dla elastycznosci. + * Zmiana wplywa na porzadek zbioru. + */ +#define REL_LT 0 /* < */ +#define REL_LE 1 /* <= */ +#define INF INT_MAX /* nieskonczonosc */ + +#define DBM_RAW_MAX (INT_MAX >> 1) /* co z nieskonczonoscia? */ +#define DBM_RAW_MIN (INT_MIN >> 1) +#define DBM_VAL_MAX (DBM_RAW_MAX >> 1) +/* + * Jak abs(DBM_VAL_MIN) jest takie samo jak _MAX, to nie trzeba sprawdzac + * wartosci po zmianie znaku. + */ +#define DBM_VAL_MIN ((DBM_RAW_MIN+2) >> 1) + +/* Z makrami jest o wieeeeele szybciej... */ +#define DBM(a, b, c, d) a[((c)*(b)+(d))] +#define DBM_P(a, b, c, d) &a[((c)*(b)+(d))] +#define DBM_MIN(a,b) ( (a) < (b) ? (a) : (b) ) +#define DBM_SUM(a, b) ( ((a) == INF || (b) == INF) ? INF : ((a) + (b) - ( ( ((a) | (b)) & 1 ) )) ) +#define DBM_ELEM(a, b) ( ((a) << 1) | (b) ) /* tworzenie elementu */ +#define DBM_E_0LE 1 /* (0, <=) */ +#define DBM_E_0LT 0 /* (0, <) */ +#define DBM_E_NEG -1 /* (-1, <=) */ +#define DBM_V(a) ( (a) >> 1 ) /* pobieranie wartosci z elementu */ +#define DBM_R(a) ( (a) & 1 ) /* pobieranie rodzaju relacji */ +#define DBM_INV_R(a) ( ((a) & 1) ^ 1 ) /* pobieranie odwrotnej relacji (<= daje <, a < daje <=) */ +#define DBM_MARK_EMPTY(a) ( *(a) = DBM_E_NEG ) + +#define GET_ASIZE(a) ( ((a) + (sizeof(DBM_idx_flags)*8 - 1)) >> 5 ) /* sprytny pomysl z ">> 5" wziety z Uppaala */ +#define GET_IDX(a) ( (((a) + (sizeof(DBM_idx_flags)*8)) >> 5) - 1 ) +#define GET_BIT_IDX(a) ( (a) % (sizeof(DBM_idx_flags)*8) ) +#define SET_FLAG(f, a) \ +{ \ + DBM_idx_flags *t; \ + t = &f[GET_IDX(a)]; \ + *t = ( *t | (1 << GET_BIT_IDX(a)) ); \ +} +#define IS_FLAGGED(f, a) ( (f[GET_IDX(a)] >> GET_BIT_IDX(a)) & 1 ) + +#define FERROR(s) \ +{ \ + printf("%s, line %d: %s\n", __FILE__, __LINE__, s); \ + exit(1); \ +} + +#define DBM_VSC(a) dbm_sval((a), __FILE__, __LINE__) /* value sanity check */ +#define DBM_LVSC(a) dbm_lsval((a), __FILE__, __LINE__) /* min. value sanity check */ + +/* Moze zabieg ze zwracaniem wartosci jest przesadzony...? + * Moze lepiej przejsc na sprawdzanie "przed" uzyciem a nie "w momencie" uzycia? + */ +static inline DBM_elem dbm_sval(DBM_elem e, char *fname, int line) +{ + if (e < DBM_RAW_MIN || e > DBM_RAW_MAX) { + if (e != INF) { + printf("DBM value overflow, %s:%d\n", fname, line); + exit(1); + } + } + + return e; +} + +static inline DBM_elem dbm_lsval(DBM_elem e, char *fname, int line) +{ + if (e < DBM_RAW_MIN) { + printf("DBM value overflow, %s:%d\n", fname, line); + exit(1); + } + + return e; +} + +#endif /* !_INC_DBM_MACRO_H_ */ diff --git a/dbm_testing.c b/dbm_testing.c new file mode 100644 index 0000000..9d7c766 --- /dev/null +++ b/dbm_testing.c @@ -0,0 +1,475 @@ +#include +#include +#include +#include "dbm.h" +#include "dbm_macro.h" + +/* + * Testowanie funkcji dbm_imm_time_predecessor + */ +void test_itp(void) +{ + DBM_elem *a, *b, *c, *c_exp; + DBM_idx dim; + + /* przypadki 2-wymiarowe */ + dim = 3; + + /* (a) Z */ + a = dbm_init(dim); + DBM(a, dim, 0, 1) = DBM_ELEM(0, REL_LE); + DBM(a, dim, 0, 2) = DBM_ELEM(0, REL_LE); + DBM(a, dim, 1, 0) = DBM_ELEM(5, REL_LT); + DBM(a, dim, 1, 2) = DBM_ELEM(5, REL_LT); + DBM(a, dim, 2, 0) = DBM_ELEM(5, REL_LT); + DBM(a, dim, 2, 1) = DBM_ELEM(5, REL_LT); + assert(dbm_is_canonical(a, dim)); + + /* (b) Z' */ + b = dbm_init(dim); + DBM(b, dim, 0, 1) = DBM_ELEM(-2, REL_LT); + DBM(b, dim, 0, 2) = DBM_ELEM(-2, REL_LT); + DBM(b, dim, 1, 0) = DBM_ELEM(6, REL_LT); + DBM(b, dim, 1, 2) = DBM_ELEM(4, REL_LT); + DBM(b, dim, 2, 0) = DBM_ELEM(7, REL_LT); + DBM(b, dim, 2, 1) = DBM_ELEM(5, REL_LT); + assert(dbm_is_canonical(b, dim)); + + /* spodziewany wynik */ + c_exp = dbm_init(dim); + DBM(c_exp, dim, 0, 1) = DBM_ELEM(0, REL_LE); + DBM(c_exp, dim, 0, 2) = DBM_ELEM(0, REL_LE); + DBM(c_exp, dim, 1, 0) = DBM_ELEM(5, REL_LT); + DBM(c_exp, dim, 1, 2) = DBM_ELEM(3, REL_LT); + DBM(c_exp, dim, 2, 0) = DBM_ELEM(5, REL_LT); + DBM(c_exp, dim, 2, 1) = DBM_ELEM(3, REL_LT); + assert(dbm_is_canonical(c_exp, dim)); + + printf("Z = \n"); + dbm_print(a, dim); printf("\n"); + + printf("Z' = \n"); + dbm_print(b, dim); printf("\n"); + + printf("spodziewany Z /||\\ Z' = \n"); + dbm_print(c_exp, dim); printf("\n"); + + c = dbm_imm_time_predecessor(a, b, dim); + printf("otrzymany Z /||\\ Z' = \n"); + dbm_print(c, dim); + + dbm_destroy(a); + dbm_destroy(b); + dbm_destroy(c); + dbm_destroy(c_exp); + printf("---------------------------\n"); + + return; +} + +/* + * Testowanie obliczania roznicy stref + */ +void test_diff(void) +{ + DBM_elem *a, *b; + DBM_idx dim = 3; + DBMset_elem *x; + + a = dbm_init(dim); + DBM(a, dim, 0, 1) = DBM_ELEM(-2, REL_LE); + DBM(a, dim, 0, 2) = DBM_ELEM(-2, REL_LE); + DBM(a, dim, 1, 0) = DBM_ELEM(4, REL_LT); + DBM(a, dim, 1, 2) = DBM_ELEM(2, REL_LT); + DBM(a, dim, 2, 0) = DBM_ELEM(4, REL_LE); + DBM(a, dim, 2, 1) = DBM_ELEM(2, REL_LE); + + b = dbm_init(dim); + DBM(b, dim, 0, 1) = DBM_ELEM(-3, REL_LT); + DBM(b, dim, 0, 2) = DBM_ELEM(-3, REL_LE); + DBM(b, dim, 1, 0) = DBM_ELEM(5, REL_LE); + DBM(b, dim, 1, 2) = DBM_ELEM(2, REL_LE); + DBM(b, dim, 2, 0) = DBM_ELEM(5, REL_LE); + DBM(b, dim, 2, 1) = DBM_ELEM(2, REL_LT); + + x = dbm_diff(a, b, dim); + + dbm_destroy(a); + dbm_destroy(b); + + dbmset_print(x, dim); + dbmset_destroy(x); + + return; +} + +/* + * Testowanie szybkosci obliczania roznicy stref + */ +void test_speed_diff(void) +{ + DBM_elem *a, *b; + DBM_idx dim = 6; + DBMset_elem *x; + + a = dbm_init(dim); + DBM(a, dim, 0, 1) = DBM_ELEM(-2, REL_LE); + DBM(a, dim, 0, 2) = DBM_ELEM(-2, REL_LE); + DBM(a, dim, 1, 0) = DBM_ELEM(4, REL_LT); + DBM(a, dim, 1, 2) = DBM_ELEM(2, REL_LT); + DBM(a, dim, 2, 0) = DBM_ELEM(4, REL_LE); + DBM(a, dim, 2, 1) = DBM_ELEM(2, REL_LE); + + b = dbm_init(dim); + DBM(b, dim, 0, 1) = DBM_ELEM(-3, REL_LT); + DBM(b, dim, 0, 2) = DBM_ELEM(-3, REL_LE); + DBM(b, dim, 1, 0) = DBM_ELEM(5, REL_LE); + DBM(b, dim, 1, 2) = DBM_ELEM(2, REL_LE); + DBM(b, dim, 2, 0) = DBM_ELEM(5, REL_LE); + DBM(b, dim, 2, 1) = DBM_ELEM(2, REL_LT); + + dbm_canonicalize(a, dim); + dbm_canonicalize(b, dim); + + { + unsigned int i; + + printf("\n"); + for (i = 0; i < 10000000; i++) { + if ((i+1) % 10 == 0) + printf("\r%d", i+1); + fflush(stdout); + + x = dbm_diff(a, b, dim); + dbmset_destroy(x); + + } + printf("\n"); + } + + dbm_destroy(a); + dbm_destroy(b); + + return; +} + +/* + * Testowanie obliczania przeciecia stref + */ +void test_intersection(void) +{ + DBM_elem *a, *b; + DBM_idx dim = 3; + DBM_elem *x1, *x2; + + a = dbm_init(dim); + DBM(a, dim, 0, 1) = DBM_ELEM(-2, REL_LE); + DBM(a, dim, 0, 2) = DBM_ELEM(-2, REL_LE); + DBM(a, dim, 1, 0) = DBM_ELEM(4, REL_LT); + DBM(a, dim, 1, 2) = DBM_ELEM(2, REL_LT); + DBM(a, dim, 2, 0) = DBM_ELEM(4, REL_LE); + DBM(a, dim, 2, 1) = DBM_ELEM(2, REL_LE); + + b = dbm_init(dim); + DBM(b, dim, 0, 1) = DBM_ELEM(-3, REL_LT); + DBM(b, dim, 0, 2) = DBM_ELEM(-3, REL_LE); + DBM(b, dim, 1, 0) = DBM_ELEM(5, REL_LE); + DBM(b, dim, 1, 2) = DBM_ELEM(2, REL_LE); + DBM(b, dim, 2, 0) = DBM_ELEM(5, REL_LE); + DBM(b, dim, 2, 1) = DBM_ELEM(2, REL_LT); + + x1 = dbm_intersection(a, b, dim); + dbm_print(x1, dim); + + x2 = dbm_intersection_cf(a, b, dim); + dbm_print(x2, dim); + + if (dbm_equal(x1, x2, dim)) + printf("Oba identyczne\n"); + else + printf("ROZNE, BLAD\n"); + + dbm_destroy(x1); + dbm_destroy(x2); + + dbm_destroy(a); + dbm_destroy(b); + + return; +} + +/* +void test_speed_isect(void) +{ + DBM_elem *a, *b; + DBM_idx dim = 6; + DBM_elem *x1, *x2; + + a = dbm_init(dim); + DBM(a, dim, 0, 1) = DBM_ELEM(-2, REL_LE); + DBM(a, dim, 0, 2) = DBM_ELEM(-2, REL_LE); + DBM(a, dim, 1, 0) = DBM_ELEM(4, REL_LT); + DBM(a, dim, 1, 2) = DBM_ELEM(2, REL_LT); + DBM(a, dim, 2, 0) = DBM_ELEM(4, REL_LE); + DBM(a, dim, 2, 1) = DBM_ELEM(2, REL_LE); + + b = dbm_init(dim); + DBM(b, dim, 0, 1) = DBM_ELEM(-3, REL_LT); + DBM(b, dim, 0, 2) = DBM_ELEM(-3, REL_LE); + DBM(b, dim, 1, 0) = DBM_ELEM(5, REL_LE); + DBM(b, dim, 1, 2) = DBM_ELEM(2, REL_LE); + DBM(b, dim, 2, 0) = DBM_ELEM(5, REL_LE); + DBM(b, dim, 2, 1) = DBM_ELEM(2, REL_LT); + + dbm_canonicalize(a, dim); + dbm_canonicalize(b, dim); + + x1 = dbm_intersection(a, b, dim); + + { + unsigned int i; + + printf("\n"); + for (i = 0; i < 10000000; i++) { + if ((i+1) % 10 == 0) + printf("\r%d", i+1); + fflush(stdout); + + x2 = dbm_intersection_cf(a, b, dim); + dbm_destroy(x2); + + } + printf("\n"); + } + + x2 = dbm_intersection_cf2(a, b, dim); + if (dbm_equal(x1, x2, dim)) + printf("Oba identyczne\n"); + else + printf("ROZNE, BLAD\n"); + + dbm_destroy(x1); + dbm_destroy(x2); + dbm_destroy(a); + dbm_destroy(b); + + return; +} +*/ + +/* + * Testowanie obliczania postaci kanonicznej + */ +void test_c14n(void) +{ + DBM_elem *a; + + DBM_idx dim = 3; + + a = dbm_init(dim); + DBM(a, dim, 0, 1) = DBM_ELEM(-2, REL_LE); + DBM(a, dim, 0, 2) = DBM_ELEM(-2, REL_LE); + DBM(a, dim, 1, 0) = DBM_ELEM(4, REL_LE); + DBM(a, dim, 1, 2) = DBM_ELEM(2, REL_LE); + DBM(a, dim, 2, 0) = DBM_ELEM(4, REL_LE); + DBM(a, dim, 2, 1) = DBM_ELEM(2, REL_LE); + + assert(dbm_is_canonical(a, dim)); + /* zaciesniamy x2 - x0 <= 4 do 3 */ + DBM(a, dim, 2, 0) = DBM_ELEM(3, REL_LE); + /* obliczamy postac kanoniczna po ZACIESNIENIU ograniczenia */ + dbm_canon1(a, dim, 2, 0); + assert(dbm_is_canonical(a, dim)); + + dbm_destroy(a); + + return; +} + +void test_closure_speed(void) +{ + DBM_elem *a; + DBM_idx dim = 1000; + + a = dbm_init(dim); + + DBM(a, dim, 0, 1) = DBM_ELEM(-2, REL_LE); + DBM(a, dim, 0, 2) = DBM_ELEM(-2, REL_LE); + DBM(a, dim, 1, 0) = DBM_ELEM(4, REL_LE); + DBM(a, dim, 1, 2) = DBM_ELEM(2, REL_LE); + DBM(a, dim, 2, 0) = DBM_ELEM(4, REL_LE); + DBM(a, dim, 2, 1) = DBM_ELEM(2, REL_LE); + + dbm_canonicalize(a, dim); + + dbm_closure(a, dim); + + return; +} + +void pbs(int n) { + unsigned int i; + i = 1<<(sizeof(n) * 8 - 1); while (i > 0) { if (n & i) printf("1"); else printf("0"); i >>= 1; } + printf("\n"); +} + + +int +main(void) +{ + + assert(printf("assertions are enabled!\n")); + + /* Macierz od Bengtssona (w jego publikacji jest najprawdopodobniej blad) + DBM(a, dim, 1, 0) = DBM_ELEM(20, REL_LT); + DBM(a, dim, 1, 2) = DBM_ELEM(-10, REL_LE); + DBM(a, dim, 2, 0) = DBM_ELEM(20, REL_LE); + DBM(a, dim, 2, 1) = DBM_ELEM(10, REL_LE); + */ + /* Macierz z Clarke MC + DBM(a, dim, 0, 1) = DBM_ELEM(-1, REL_LE); + DBM(a, dim, 0, 2) = DBM_ELEM(0, REL_LT); + DBM(a, dim, 1, 0) = INF; + DBM(a, dim, 1, 2) = DBM_ELEM(2, REL_LT); + DBM(a, dim, 2, 0) = DBM_ELEM(2, REL_LE); + DBM(a, dim, 2, 1) = INF; + */ + /* Testowanie Bengtssonowego down(D) z jego przykladem (w efekcie powinno byc DBM(0,1) = (-1, <=)): + DBM(a, dim, 0, 1) = DBM_ELEM(-4, REL_LE); + DBM(a, dim, 0, 2) = DBM_ELEM(-1, REL_LE); + DBM(a, dim, 1, 0) = DBM_ELEM(5, REL_LE); + DBM(a, dim, 1, 2) = DBM_ELEM(4, REL_LE); + DBM(a, dim, 2, 0) = DBM_ELEM(2, REL_LE); + DBM(a, dim, 2, 1) = DBM_ELEM(-1, REL_LE); + */ + /*dbm_print(a, dim); + dbm_time_successor(a, dim); + dbm_time_predecessor(a, dim); + dbm_canonicalize(a, dim); + */ + /* + { + + DBM(a, dim, 0, 2) = DBM_ELEM(-3, REL_LE); + DBM(a, dim, 1, 0) = DBM_ELEM(4, REL_LE); + DBM(a, dim, 1, 2) = DBM_ELEM(1, REL_LE); + DBM(a, dim, 2, 0) = DBM_ELEM(7, REL_LE); + DBM(a, dim, 2, 1) = DBM_ELEM(5, REL_LE); + + dbm_print(a, dim); + dbm_reset(a, dim, 1); + dbm_print(a, dim); + } + */ + + /* + { + unsigned int i; + DBM_elem *c; + + printf("\n"); + for (i = 0; i < 1000; i++) { + if ((i+1) % 10 == 0) + printf("\r%d", i+1); + fflush(stdout); + + c = dbm_intersection(a,b, dim); + free(c); + + } + printf("\n"); + } + */ + + /* odwrotny reset */ + /*{ + DBM_elem *a; + DBM_idx dim; + + dim = 4; + a = dbm_init(dim); + + assert(dbm_is_sane(a, dim)); + DBM(a, dim, 0, 1) = DBM_ELEM(0, REL_LE); + DBM(a, dim, 0, 2) = DBM_ELEM(-2, REL_LE); + DBM(a, dim, 1, 0) = DBM_ELEM(7, REL_LE); + DBM(a, dim, 1, 2) = DBM_ELEM(1, REL_LE); + DBM(a, dim, 2, 0) = DBM_ELEM(7, REL_LE); + DBM(a, dim, 2, 1) = DBM_ELEM(5, REL_LE); + DBM(a, dim, 0, 3) = DBM_ELEM(-1, REL_LE); + DBM(a, dim, 3, 0) = DBM_ELEM(3, REL_LE); + DBM(a, dim, 3, 2) = DBM_ELEM(-1, REL_LE); + DBM(a, dim, 2, 3) = DBM_ELEM(1, REL_LE); + DBM(a, dim, 1, 3) = DBM_ELEM(-1, REL_LE); + DBM(a, dim, 3, 1) = DBM_ELEM(2, REL_LE); + dbm_canonicalize(a, dim); + + dbm_print(a, dim); + dbm_invreset(a, dim, 1); + printf("\n"); + dbm_print(a, dim); + + dbm_destroy(a); + }*/ + + //test_intersection(); + //test_speed_isect(); + //test_diff(); + //test_speed_diff(); + //test_itp(); + //test_closure_speed(); + + /*{ + int i; + DBM_idx dim = 10; + DBM_elem *a = dbm_init(dim); + + for (i = 0; i < 1000000; i++) { + DBM(a, dim, 0, 1) = DBM_ELEM(0, REL_LE); + DBM(a, dim, 0, 2) = DBM_ELEM(-2, REL_LE); + DBM(a, dim, 1, 0) = DBM_ELEM(7, REL_LE); + DBM(a, dim, 1, 2) = DBM_ELEM(1, REL_LE); + DBM(a, dim, 2, 0) = DBM_ELEM(7, REL_LE); + DBM(a, dim, 2, 1) = DBM_ELEM(5, REL_LE); + DBM(a, dim, 0, 3) = DBM_ELEM(-1, REL_LE); + DBM(a, dim, 3, 0) = DBM_ELEM(3, REL_LE); + DBM(a, dim, 3, 2) = DBM_ELEM(-1, REL_LE); + DBM(a, dim, 2, 3) = DBM_ELEM(1, REL_LE); + DBM(a, dim, 1, 3) = DBM_ELEM(-1, REL_LE); + DBM(a, dim, 3, 1) = DBM_ELEM(2, REL_LE); + dbm_canonicalize(a, dim); + } + }*/ + + // { + // DBM_elem *a; + // + // DBM_idx dim = 2; + // a = dbm_init(dim); + // dbm_constr_lt(a, dim, 0, 1, -5); + // dbm_constr_lt(a, dim, 1, 0, 5); + // dbm_canonicalize(a, dim); + // //pbs(DBM_VAL_MIN); + // dbm_print(a, dim); + // + // } + + { + DBM_elem *a; + DBM_idx dim = 3; + a = dbm_init(dim); + + DBM(a, dim, 0, 1) = DBM_ELEM(-1, REL_LE); + DBM(a, dim, 0, 2) = DBM_ELEM(0, REL_LT); + DBM(a, dim, 1, 0) = INF; + DBM(a, dim, 1, 2) = DBM_ELEM(2, REL_LT); + DBM(a, dim, 2, 0) = DBM_ELEM(2, REL_LE); + DBM(a, dim, 2, 1) = INF; + dbm_canonicalize(a, dim); + dbm_print(a, dim); + } + + + return 0; +} + diff --git a/macro.h b/macro.h new file mode 100644 index 0000000..0653455 --- /dev/null +++ b/macro.h @@ -0,0 +1,31 @@ +#ifndef _INC_MACRO_H_ +#define _INC_MACRO_H_ + +static inline void *smalloc(size_t size) +{ + void *p; + + p = malloc(size); + if (!p) { + printf("malloc failed!\n"); + exit(1); + } + + return p; +} + +static inline void *smalloc_zero(size_t size) +{ + void *p; + + p = smalloc(size); + memset(p, 0, size); + + return p; +} + +/* Dodatkowe na czas debugowania, smieciowe... */ +#define DBP printf("DEBUG POINT (%s), line %d reached\n", __FILE__, __LINE__); +#define DBMPR(t, d) { printf("\n(line=%d) %s\n", __LINE__, (t)); dbm_print((d), dbm_size); printf("\n"); } + +#endif /* !_INC_MACRO_H_ */ diff --git a/netfiles/fischer-fail.aut b/netfiles/fischer-fail.aut new file mode 100644 index 0000000..2e01872 --- /dev/null +++ b/netfiles/fischer-fail.aut @@ -0,0 +1,92 @@ +####################################### +# Fischer's mutual exclusion protocol # +####################################### +# # +# przy setv1, setv2 - duza delta # +# przy enter1, enter2 - mala delta # +# # +# wzajemne wykluczanie przy: # +# # +# mala delta >= duza delta # +# # +####################################### + +net { + actions { + start1; + setv1; + enter1; + setv01; + + start2; + setv2; + enter2; + setv02; + }; + + automaton proc1 { + clocks { + x1; + }; + locations { + idle1 { init; }; + try1; + wait1; + crit1; + }; + trans { + idle1 -> try1, start1, , { x1; }; + try1 -> wait1, setv1, x1 < 2, { x1; }; + wait1 -> crit1, enter1, x1 > 1, { }; + crit1 -> idle1, setv01, , { }; + }; + }; + + automaton proc2 { + clocks { + x2; + }; + locations { + idle2 { init; }; + try2; + wait2; + crit2; + }; + trans { + idle2 -> try2, start2, , { x2; }; + try2 -> wait2, setv2, x2 < 2, { x2; }; + wait2 -> crit2, enter2, x2 > 1, { }; + crit2 -> idle2, setv02, , { }; + }; + }; + + automaton varV { + locations { + v0 { init; }; + v1; + v2; + }; + trans { + v0 -> v0, start1, , { }; + v0 -> v0, start2, , { }; + v0 -> v1, setv1, , { }; + v0 -> v2, setv2, , { }; + + v1 -> v0, setv01, , { }; + v1 -> v1, enter1, , { }; + v1 -> v1, setv1, , { }; + v1 -> v2, setv2, , { }; + + v2 -> v0, setv02, , { }; + v2 -> v2, enter2, , { }; + v2 -> v1, setv1, , { }; + v2 -> v2, setv2, , { }; + + }; + }; + +}; + +reach { + mutualexclusion_p1p2 { crit1@proc1 crit2@proc2 }; +}; \ No newline at end of file diff --git a/netfiles/fischer-orig.aut b/netfiles/fischer-orig.aut new file mode 100644 index 0000000..371b027 --- /dev/null +++ b/netfiles/fischer-orig.aut @@ -0,0 +1,87 @@ +####################################### +# Fischer's mutual exclusion protocol # +####################################### +# # +# przy setv1, setv2 - duza delta # +# przy enter1, enter2 - mala delta # +# # +# wzajemne wykluczanie przy: # +# # +# mala delta >= duza delta # +# # +####################################### + +net { + actions { + start1; + setv1; + enter1; + setv01; + + start2; + setv2; + enter2; + setv02; + }; + + automaton proc1 { + clocks { + x1; + }; + locations { + idle1 { init; }; + try1; + wait1; + crit1; + }; + trans { + idle1 -> try1, start1, , { x1; }; + try1 -> wait1, setv1, x1 < 1, { x1; }; + wait1 -> crit1, enter1, x1 > 2, { }; + crit1 -> idle1, setv01, , { }; + }; + }; + + automaton proc2 { + clocks { + x2; + }; + locations { + idle2 { init; }; + try2; + wait2; + crit2; + }; + trans { + idle2 -> try2, start2, , { x2; }; + try2 -> wait2, setv2, x2 < 1, { x2; }; + wait2 -> crit2, enter2, x2 > 2, { }; + crit2 -> idle2, setv02, , { }; + }; + }; + + automaton varV { + locations { + v0 { init; }; + v1; + v2; + }; + trans { + v0 -> v0, start1, , { }; + v0 -> v0, start2, , { }; + v0 -> v1, setv1, , { }; + v0 -> v2, setv2, , { }; + + v1 -> v0, setv01, , { }; + v1 -> v1, enter1, , { }; + v1 -> v1, setv1, , { }; + v1 -> v2, setv2, , { }; + + v2 -> v0, setv02, , { }; + v2 -> v2, enter2, , { }; + v2 -> v1, setv1, , { }; + v2 -> v2, setv2, , { }; + }; + }; + +}; \ No newline at end of file diff --git a/netfiles/fischer.aut b/netfiles/fischer.aut new file mode 100644 index 0000000..1a51b8b --- /dev/null +++ b/netfiles/fischer.aut @@ -0,0 +1,88 @@ +####################################### +# Fischer's mutual exclusion protocol # +####################################### +# # +# przy setv1, setv2 - duza delta # +# przy enter1, enter2 - mala delta # +# # +# wzajemne wykluczanie przy: # +# # +# mala delta >= duza delta # +# # +####################################### + +net { + actions { + start1; + setv1; + enter1; + setv01; + + start2; + setv2; + enter2; + setv02; + }; + + automaton proc1 { + clocks { + x1; + }; + locations { + idle1 { init; }; + try1; + wait1; + crit1; + }; + trans { + idle1 -> try1, start1, , { x1; }; + try1 -> wait1, setv1, x1 < 1, { x1; }; + wait1 -> crit1, enter1, x1 > 2, { }; + crit1 -> idle1, setv01, , { }; + }; + }; + + automaton proc2 { + clocks { + x2; + }; + locations { + idle2 { init; }; + try2; + wait2; + crit2; + }; + trans { + idle2 -> try2, start2, , { x2; }; + try2 -> wait2, setv2, x2 < 1, { x2; }; + wait2 -> crit2, enter2, x2 > 2, { }; + crit2 -> idle2, setv02, , { }; + }; + }; + + automaton varV { + locations { + v0 { init; }; + v1; + v2; + }; + trans { + v0 -> v0, start1, , { }; + v0 -> v0, start2, , { }; + v0 -> v1, setv1, , { }; + v0 -> v2, setv2, , { }; + + v1 -> v0, setv01, , { }; + v1 -> v1, enter1, , { }; + v1 -> v1, setv1, , { }; + v1 -> v2, setv2, , { }; + + v2 -> v0, setv02, , { }; + v2 -> v2, enter2, , { }; + v2 -> v1, setv1, , { }; + v2 -> v2, setv2, , { }; + + }; + }; + +}; \ No newline at end of file diff --git a/netfiles/fischer10p.aut b/netfiles/fischer10p.aut new file mode 100644 index 0000000..4fb41fe --- /dev/null +++ b/netfiles/fischer10p.aut @@ -0,0 +1,416 @@ +####################################### +# Fischer's mutual exclusion protocol # +####################################### +# # +# przy setv1, setv2 - duza delta # +# przy enter1, enter2 - mala delta # +# # +# wzajemne wykluczanie przy: # +# # +# mala delta >= duza delta # +# # +####################################### + +net { + actions { + start1; + setv1; + enter1; + setv01; + + start2; + setv2; + enter2; + setv02; + + start3; + setv3; + enter3; + setv03; + + start4; + setv4; + enter4; + setv04; + + start5; + setv5; + enter5; + setv05; + + start6; + setv6; + enter6; + setv06; + + start7; + setv7; + enter7; + setv07; + + start8; + setv8; + enter8; + setv08; + + start9; + setv9; + enter9; + setv09; + + start10; + setv10; + enter10; + setv010; + }; + + automaton proc1 { + clocks { + x1; + }; + locations { + idle1 { init; }; + try1; + wait1; + crit1; + }; + trans { + idle1 -> try1, start1, , { x1; }; + try1 -> wait1, setv1, x1 < 1, { x1; }; + wait1 -> crit1, enter1, x1 > 2, { }; + crit1 -> idle1, setv01, , { }; + }; + }; + + automaton proc2 { + clocks { + x2; + }; + locations { + idle2 { init; }; + try2; + wait2; + crit2; + }; + trans { + idle2 -> try2, start2, , { x2; }; + try2 -> wait2, setv2, x2 < 1, { x2; }; + wait2 -> crit2, enter2, x2 > 2, { }; + crit2 -> idle2, setv02, , { }; + }; + }; + + automaton proc3 { + clocks { + x3; + }; + locations { + idle3 { init; }; + try3; + wait3; + crit3; + }; + trans { + idle3 -> try3, start3, , { x3; }; + try3 -> wait3, setv3, x3 < 1, { x3; }; + wait3 -> crit3, enter3, x3 > 2, { }; + crit3 -> idle3, setv03, , { }; + }; + }; + + automaton proc4 { + clocks { + x4; + }; + locations { + idle4 { init; }; + try4; + wait4; + crit4; + }; + trans { + idle4 -> try4, start4, , { x4; }; + try4 -> wait4, setv4, x4 < 1, { x4; }; + wait4 -> crit4, enter4, x4 > 2, { }; + crit4 -> idle4, setv04, , { }; + }; + }; + + automaton proc5 { + clocks { + x5; + }; + locations { + idle5 { init; }; + try5; + wait5; + crit5; + }; + trans { + idle5 -> try5, start5, , { x5; }; + try5 -> wait5, setv5, x5 < 1, { x5; }; + wait5 -> crit5, enter5, x5 > 2, { }; + crit5 -> idle5, setv05, , { }; + }; + }; + + automaton proc6 { + clocks { + x6; + }; + locations { + idle6 { init; }; + try6; + wait6; + crit6; + }; + trans { + idle6 -> try6, start6, , { x6; }; + try6 -> wait6, setv6, x6 < 1, { x6; }; + wait6 -> crit6, enter6, x6 > 2, { }; + crit6 -> idle6, setv06, , { }; + }; + }; + + automaton proc7 { + clocks { + x7; + }; + locations { + idle7 { init; }; + try7; + wait7; + crit7; + }; + trans { + idle7 -> try7, start7, , { x7; }; + try7 -> wait7, setv7, x7 < 1, { x7; }; + wait7 -> crit7, enter7, x7 > 2, { }; + crit7 -> idle7, setv07, , { }; + }; + }; + + automaton proc8 { + clocks { + x8; + }; + locations { + idle8 { init; }; + try8; + wait8; + crit8; + }; + trans { + idle8 -> try8, start8, , { x8; }; + try8 -> wait8, setv8, x8 < 1, { x8; }; + wait8 -> crit8, enter8, x8 > 2, { }; + crit8 -> idle8, setv08, , { }; + }; + }; + + automaton proc9 { + clocks { + x9; + }; + locations { + idle9 { init; }; + try9; + wait9; + crit9; + }; + trans { + idle9 -> try9, start9, , { x9; }; + try9 -> wait9, setv9, x9 < 1, { x9; }; + wait9 -> crit9, enter9, x9 > 2, { }; + crit9 -> idle9, setv09, , { }; + }; + }; + + automaton proc10 { + clocks { + x10; + }; + locations { + idle10 { init; }; + try10; + wait10; + crit10; + }; + trans { + idle10 -> try10, start10, , { x10; }; + try10 -> wait10, setv10, x10 < 1, { x10; }; + wait10 -> crit10, enter10, x10 > 2, { }; + crit10 -> idle10, setv010, , { }; + }; + }; + + automaton varV { + locations { + v0 { init; }; + v1; + v2; + v3; + v4; + v5; + v6; + v7; + v8; + v9; + v10; + }; + trans { + v0 -> v0, start1, , { }; + v0 -> v0, start2, , { }; + v0 -> v0, start3, , { }; + v0 -> v0, start4, , { }; + v0 -> v0, start5, , { }; + v0 -> v0, start6, , { }; + v0 -> v0, start7, , { }; + v0 -> v0, start8, , { }; + v0 -> v0, start9, , { }; + v0 -> v0, start10, , { }; + v0 -> v1, setv1, , { }; + v0 -> v2, setv2, , { }; + v0 -> v3, setv3, , { }; + v0 -> v4, setv4, , { }; + v0 -> v5, setv5, , { }; + v0 -> v6, setv6, , { }; + v0 -> v7, setv7, , { }; + v0 -> v8, setv8, , { }; + v0 -> v9, setv9, , { }; + v0 -> v10, setv10, , { }; + + v1 -> v0, setv01, , { }; + v1 -> v1, enter1, , { }; + v1 -> v1, setv1, , { }; + v1 -> v2, setv2, , { }; + v1 -> v3, setv3, , { }; + v1 -> v4, setv4, , { }; + v1 -> v5, setv5, , { }; + v1 -> v6, setv6, , { }; + v1 -> v7, setv7, , { }; + v1 -> v8, setv8, , { }; + v1 -> v9, setv9, , { }; + v1 -> v10, setv10, , { }; + + v2 -> v0, setv02, , { }; + v2 -> v1, enter2, , { }; + v2 -> v1, setv1, , { }; + v2 -> v2, setv2, , { }; + v2 -> v3, setv3, , { }; + v2 -> v4, setv4, , { }; + v2 -> v5, setv5, , { }; + v2 -> v6, setv6, , { }; + v2 -> v7, setv7, , { }; + v2 -> v8, setv8, , { }; + v2 -> v9, setv9, , { }; + v2 -> v10, setv10, , { }; + + v3 -> v0, setv03, , { }; + v3 -> v1, enter3, , { }; + v3 -> v1, setv1, , { }; + v3 -> v2, setv2, , { }; + v3 -> v3, setv3, , { }; + v3 -> v4, setv4, , { }; + v3 -> v5, setv5, , { }; + v3 -> v6, setv6, , { }; + v3 -> v7, setv7, , { }; + v3 -> v8, setv8, , { }; + v3 -> v9, setv9, , { }; + v3 -> v10, setv10, , { }; + + v4 -> v0, setv04, , { }; + v4 -> v1, enter4, , { }; + v4 -> v1, setv1, , { }; + v4 -> v2, setv2, , { }; + v4 -> v3, setv3, , { }; + v4 -> v4, setv4, , { }; + v4 -> v5, setv5, , { }; + v4 -> v6, setv6, , { }; + v4 -> v7, setv7, , { }; + v4 -> v8, setv8, , { }; + v4 -> v9, setv9, , { }; + v4 -> v10, setv10, , { }; + + v5 -> v0, setv05, , { }; + v5 -> v1, enter5, , { }; + v5 -> v1, setv1, , { }; + v5 -> v2, setv2, , { }; + v5 -> v3, setv3, , { }; + v5 -> v4, setv4, , { }; + v5 -> v5, setv5, , { }; + v5 -> v6, setv6, , { }; + v5 -> v7, setv7, , { }; + v5 -> v8, setv8, , { }; + v5 -> v9, setv9, , { }; + v5 -> v10, setv10, , { }; + + v6 -> v0, setv06, , { }; + v6 -> v1, enter6, , { }; + v6 -> v1, setv1, , { }; + v6 -> v2, setv2, , { }; + v6 -> v3, setv3, , { }; + v6 -> v4, setv4, , { }; + v6 -> v5, setv5, , { }; + v6 -> v6, setv6, , { }; + v6 -> v7, setv7, , { }; + v6 -> v8, setv8, , { }; + v6 -> v9, setv9, , { }; + v6 -> v10, setv10, , { }; + + v7 -> v0, setv07, , { }; + v7 -> v1, enter7, , { }; + v7 -> v1, setv1, , { }; + v7 -> v2, setv2, , { }; + v7 -> v3, setv3, , { }; + v7 -> v4, setv4, , { }; + v7 -> v5, setv5, , { }; + v7 -> v6, setv6, , { }; + v7 -> v7, setv7, , { }; + v7 -> v8, setv8, , { }; + v7 -> v9, setv9, , { }; + v7 -> v10, setv10, , { }; + + v8 -> v0, setv08, , { }; + v8 -> v1, enter8, , { }; + v8 -> v1, setv1, , { }; + v8 -> v2, setv2, , { }; + v8 -> v3, setv3, , { }; + v8 -> v4, setv4, , { }; + v8 -> v5, setv5, , { }; + v8 -> v6, setv6, , { }; + v8 -> v7, setv7, , { }; + v8 -> v8, setv8, , { }; + v8 -> v9, setv9, , { }; + v8 -> v10, setv10, , { }; + + v9 -> v0, setv09, , { }; + v9 -> v1, enter9, , { }; + v9 -> v1, setv1, , { }; + v9 -> v2, setv2, , { }; + v9 -> v3, setv3, , { }; + v9 -> v4, setv4, , { }; + v9 -> v5, setv5, , { }; + v9 -> v6, setv6, , { }; + v9 -> v7, setv7, , { }; + v9 -> v8, setv8, , { }; + v9 -> v9, setv9, , { }; + v9 -> v10, setv10, , { }; + + v10 -> v0, setv010, , { }; + v10 -> v1, enter10, , { }; + v10 -> v1, setv1, , { }; + v10 -> v2, setv2, , { }; + v10 -> v3, setv3, , { }; + v10 -> v4, setv4, , { }; + v10 -> v5, setv5, , { }; + v10 -> v6, setv6, , { }; + v10 -> v7, setv7, , { }; + v10 -> v8, setv8, , { }; + v10 -> v9, setv9, , { }; + v10 -> v10, setv10, , { }; + + }; + }; + +}; \ No newline at end of file diff --git a/netfiles/fischer3p-fail.aut b/netfiles/fischer3p-fail.aut new file mode 100644 index 0000000..7615b72 --- /dev/null +++ b/netfiles/fischer3p-fail.aut @@ -0,0 +1,121 @@ +####################################### +# Fischer's mutual exclusion protocol # +####################################### +# # +# przy setv1, setv2 - duza delta # +# przy enter1, enter2 - mala delta # +# # +# wzajemne wykluczanie przy: # +# # +# mala delta >= duza delta # +# # +####################################### + +net { + actions { + start1; + setv1; + enter1; + setv01; + + start2; + setv2; + enter2; + setv02; + + start3; + setv3; + enter3; + setv03; + }; + + automaton proc1 { + clocks { + x1; + }; + locations { + idle1 { init; }; + try1; + wait1; + crit1; + }; + trans { + idle1 -> try1, start1, , { x1; }; + try1 -> wait1, setv1, x1 < 2, { x1; }; + wait1 -> crit1, enter1, x1 > 1, { }; + crit1 -> idle1, setv01, , { }; + }; + }; + + automaton proc2 { + clocks { + x2; + }; + locations { + idle2 { init; }; + try2; + wait2; + crit2; + }; + trans { + idle2 -> try2, start2, , { x2; }; + try2 -> wait2, setv2, x2 < 2, { x2; }; + wait2 -> crit2, enter2, x2 > 1, { }; + crit2 -> idle2, setv02, , { }; + }; + }; + + automaton proc3 { + clocks { + x3; + }; + locations { + idle3 { init; }; + try3; + wait3; + crit3; + }; + trans { + idle3 -> try3, start3, , { x3; }; + try3 -> wait3, setv3, x3 < 2, { x3; }; + wait3 -> crit3, enter3, x3 > 1, { }; + crit3 -> idle3, setv03, , { }; + }; + }; + + automaton varV { + locations { + v0 { init; }; + v1; + v2; + v3; + }; + trans { + v0 -> v0, start1, , { }; + v0 -> v0, start2, , { }; + v0 -> v0, start3, , { }; + v0 -> v1, setv1, , { }; + v0 -> v2, setv2, , { }; + v0 -> v3, setv3, , { }; + + v1 -> v0, setv01, , { }; + v1 -> v1, enter1, , { }; + v1 -> v1, setv1, , { }; + v1 -> v2, setv2, , { }; + v1 -> v3, setv3, , { }; + + v2 -> v0, setv02, , { }; + v2 -> v2, enter2, , { }; + v2 -> v1, setv1, , { }; + v2 -> v2, setv2, , { }; + v2 -> v3, setv3, , { }; + }; + }; + +}; + +reach { + mutualexclusion_p1p2 { crit1@proc1 crit2@proc2 }; + mutualexclusion_p1p3 { crit1@proc1 crit3@proc3 }; + mutualexclusion_p2p3 { crit2@proc2 crit3@proc3 }; +}; diff --git a/netfiles/fischer3p.aut b/netfiles/fischer3p.aut new file mode 100644 index 0000000..3a8a479 --- /dev/null +++ b/netfiles/fischer3p.aut @@ -0,0 +1,121 @@ +####################################### +# Fischer's mutual exclusion protocol # +####################################### +# # +# przy setv1, setv2 - duza delta # +# przy enter1, enter2 - mala delta # +# # +# wzajemne wykluczanie przy: # +# # +# mala delta >= duza delta # +# # +####################################### + +net { + actions { + start1; + setv1; + enter1; + setv01; + + start2; + setv2; + enter2; + setv02; + + start3; + setv3; + enter3; + setv03; + }; + + automaton proc1 { + clocks { + x1; + }; + locations { + idle1 { init; }; + try1; + wait1; + crit1; + }; + trans { + idle1 -> try1, start1, , { x1; }; + try1 -> wait1, setv1, x1 < 1, { x1; }; + wait1 -> crit1, enter1, x1 > 2, { }; + crit1 -> idle1, setv01, , { }; + }; + }; + + automaton proc2 { + clocks { + x2; + }; + locations { + idle2 { init; }; + try2; + wait2; + crit2; + }; + trans { + idle2 -> try2, start2, , { x2; }; + try2 -> wait2, setv2, x2 < 1, { x2; }; + wait2 -> crit2, enter2, x2 > 2, { }; + crit2 -> idle2, setv02, , { }; + }; + }; + + automaton proc3 { + clocks { + x3; + }; + locations { + idle3 { init; }; + try3; + wait3; + crit3; + }; + trans { + idle3 -> try3, start3, , { x3; }; + try3 -> wait3, setv3, x3 < 1, { x3; }; + wait3 -> crit3, enter3, x3 > 2, { }; + crit3 -> idle3, setv03, , { }; + }; + }; + + automaton varV { + locations { + v0 { init; }; + v1; + v2; + v3; + }; + trans { + v0 -> v0, start1, , { }; + v0 -> v0, start2, , { }; + v0 -> v0, start3, , { }; + v0 -> v1, setv1, , { }; + v0 -> v2, setv2, , { }; + v0 -> v3, setv3, , { }; + + v1 -> v0, setv01, , { }; + v1 -> v1, enter1, , { }; + v1 -> v1, setv1, , { }; + v1 -> v2, setv2, , { }; + v1 -> v3, setv3, , { }; + + v2 -> v0, setv02, , { }; + v2 -> v2, enter2, , { }; + v2 -> v1, setv1, , { }; + v2 -> v2, setv2, , { }; + v2 -> v3, setv3, , { }; + }; + }; + +}; + +reach { + mutualexclusion_p1p2 { crit1@proc1 crit2@proc2 }; + mutualexclusion_p1p3 { crit1@proc1 crit3@proc3 }; + mutualexclusion_p2p3 { crit2@proc2 crit3@proc3 }; +}; diff --git a/netfiles/fischer4p-fail.aut b/netfiles/fischer4p-fail.aut new file mode 100644 index 0000000..6c93c7a --- /dev/null +++ b/netfiles/fischer4p-fail.aut @@ -0,0 +1,167 @@ +####################################### +# Fischer's mutual exclusion protocol # +####################################### +# # +# przy setv1, setv2 - duza delta # +# przy enter1, enter2 - mala delta # +# # +# wzajemne wykluczanie przy: # +# # +# mala delta >= duza delta # +# # +####################################### + +net { + actions { + start1; + setv1; + enter1; + setv01; + + start2; + setv2; + enter2; + setv02; + + start3; + setv3; + enter3; + setv03; + + start4; + setv4; + enter4; + setv04; + }; + + automaton proc1 { + clocks { + x1; + }; + locations { + idle1 { init; }; + try1; + wait1; + crit1; + }; + trans { + idle1 -> try1, start1, , { x1; }; + try1 -> wait1, setv1, x1 < 2, { x1; }; + wait1 -> crit1, enter1, x1 > 1, { }; + crit1 -> idle1, setv01, , { }; + }; + }; + + automaton proc2 { + clocks { + x2; + }; + locations { + idle2 { init; }; + try2; + wait2; + crit2; + }; + trans { + idle2 -> try2, start2, , { x2; }; + try2 -> wait2, setv2, x2 < 2, { x2; }; + wait2 -> crit2, enter2, x2 > 1, { }; + crit2 -> idle2, setv02, , { }; + }; + }; + + automaton proc3 { + clocks { + x3; + }; + locations { + idle3 { init; }; + try3; + wait3; + crit3; + }; + trans { + idle3 -> try3, start3, , { x3; }; + try3 -> wait3, setv3, x3 < 2, { x3; }; + wait3 -> crit3, enter3, x3 > 1, { }; + crit3 -> idle3, setv03, , { }; + }; + }; + + automaton proc4 { + clocks { + x4; + }; + locations { + idle4 { init; }; + try4; + wait4; + crit4; + }; + trans { + idle4 -> try4, start4, , { x4; }; + try4 -> wait4, setv4, x4 < 2, { x4; }; + wait4 -> crit4, enter4, x4 > 1, { }; + crit4 -> idle4, setv04, , { }; + }; + }; + + automaton varV { + locations { + v0 { init; }; + v1; + v2; + v3; + v4; + }; + trans { + v0 -> v0, start1, , { }; + v0 -> v0, start2, , { }; + v0 -> v0, start3, , { }; + v0 -> v0, start4, , { }; + v0 -> v1, setv1, , { }; + v0 -> v2, setv2, , { }; + v0 -> v3, setv3, , { }; + v0 -> v4, setv4, , { }; + + v1 -> v0, setv01, , { }; + v1 -> v1, enter1, , { }; + v1 -> v1, setv1, , { }; + v1 -> v2, setv2, , { }; + v1 -> v3, setv3, , { }; + v1 -> v4, setv4, , { }; + + v2 -> v0, setv02, , { }; + v2 -> v2, enter2, , { }; + v2 -> v1, setv1, , { }; + v2 -> v2, setv2, , { }; + v2 -> v3, setv3, , { }; + v2 -> v4, setv4, , { }; + + v3 -> v0, setv03, , { }; + v3 -> v3, enter3, , { }; + v3 -> v1, setv1, , { }; + v3 -> v2, setv2, , { }; + v3 -> v3, setv3, , { }; + v3 -> v4, setv4, , { }; + + v4 -> v0, setv04, , { }; + v4 -> v4, enter4, , { }; + v4 -> v1, setv1, , { }; + v4 -> v2, setv2, , { }; + v4 -> v3, setv3, , { }; + v4 -> v4, setv4, , { }; + + }; + }; + +}; + +reach { + mutualexclusion_p1p2 { crit1@proc1 crit2@proc2 }; + mutualexclusion_p1p3 { crit1@proc1 crit3@proc3 }; + mutualexclusion_p1p4 { crit1@proc1 crit4@proc4 }; + mutualexclusion_p2p3 { crit2@proc2 crit3@proc3 }; + mutualexclusion_p2p4 { crit2@proc2 crit4@proc4 }; + mutualexclusion_p3p4 { crit3@proc3 crit4@proc4 }; +}; diff --git a/netfiles/fischer4p.aut b/netfiles/fischer4p.aut new file mode 100644 index 0000000..4b48f62 --- /dev/null +++ b/netfiles/fischer4p.aut @@ -0,0 +1,158 @@ +####################################### +# Fischer's mutual exclusion protocol # +####################################### +# # +# przy setv1, setv2 - duza delta # +# przy enter1, enter2 - mala delta # +# # +# wzajemne wykluczanie przy: # +# # +# mala delta >= duza delta # +# # +####################################### + +net { + actions { + start1; + setv1; + enter1; + setv01; + + start2; + setv2; + enter2; + setv02; + + start3; + setv3; + enter3; + setv03; + + start4; + setv4; + enter4; + setv04; + }; + + automaton proc1 { + clocks { + x1; + }; + locations { + idle1 { init; }; + try1; + wait1; + crit1; + }; + trans { + idle1 -> try1, start1, , { x1; }; + try1 -> wait1, setv1, x1 < 1, { x1; }; + wait1 -> crit1, enter1, x1 > 2, { }; + crit1 -> idle1, setv01, , { }; + }; + }; + + automaton proc2 { + clocks { + x2; + }; + locations { + idle2 { init; }; + try2; + wait2; + crit2; + }; + trans { + idle2 -> try2, start2, , { x2; }; + try2 -> wait2, setv2, x2 < 1, { x2; }; + wait2 -> crit2, enter2, x2 > 2, { }; + crit2 -> idle2, setv02, , { }; + }; + }; + + automaton proc3 { + clocks { + x3; + }; + locations { + idle3 { init; }; + try3; + wait3; + crit3; + }; + trans { + idle3 -> try3, start3, , { x3; }; + try3 -> wait3, setv3, x3 < 1, { x3; }; + wait3 -> crit3, enter3, x3 > 2, { }; + crit3 -> idle3, setv03, , { }; + }; + }; + + automaton proc4 { + clocks { + x4; + }; + locations { + idle4 { init; }; + try4; + wait4; + crit4; + }; + trans { + idle4 -> try4, start4, , { x4; }; + try4 -> wait4, setv4, x4 < 1, { x4; }; + wait4 -> crit4, enter4, x4 > 2, { }; + crit4 -> idle4, setv04, , { }; + }; + }; + + automaton varV { + locations { + v0 { init; }; + v1; + v2; + v3; + v4; + }; + trans { + v0 -> v0, start1, , { }; + v0 -> v0, start2, , { }; + v0 -> v0, start3, , { }; + v0 -> v0, start4, , { }; + v0 -> v1, setv1, , { }; + v0 -> v2, setv2, , { }; + v0 -> v3, setv3, , { }; + v0 -> v4, setv4, , { }; + + v1 -> v0, setv01, , { }; + v1 -> v1, enter1, , { }; + v1 -> v1, setv1, , { }; + v1 -> v2, setv2, , { }; + v1 -> v3, setv3, , { }; + v1 -> v4, setv4, , { }; + + v2 -> v0, setv02, , { }; + v2 -> v2, enter2, , { }; + v2 -> v1, setv1, , { }; + v2 -> v2, setv2, , { }; + v2 -> v3, setv3, , { }; + v2 -> v4, setv4, , { }; + + v3 -> v0, setv03, , { }; + v3 -> v3, enter3, , { }; + v3 -> v1, setv1, , { }; + v3 -> v2, setv2, , { }; + v3 -> v3, setv3, , { }; + v3 -> v4, setv4, , { }; + + v4 -> v0, setv04, , { }; + v4 -> v4, enter4, , { }; + v4 -> v1, setv1, , { }; + v4 -> v2, setv2, , { }; + v4 -> v3, setv3, , { }; + v4 -> v4, setv4, , { }; + + }; + }; + +}; \ No newline at end of file diff --git a/netfiles/fischer5p-fail.aut b/netfiles/fischer5p-fail.aut new file mode 100644 index 0000000..689062e --- /dev/null +++ b/netfiles/fischer5p-fail.aut @@ -0,0 +1,209 @@ +####################################### +# Fischer's mutual exclusion protocol # +####################################### +# # +# przy setv1, setv2 - duza delta # +# przy enter1, enter2 - mala delta # +# # +# wzajemne wykluczanie przy: # +# # +# mala delta >= duza delta # +# # +####################################### + +net { + actions { + start1; + setv1; + enter1; + setv01; + + start2; + setv2; + enter2; + setv02; + + start3; + setv3; + enter3; + setv03; + + start4; + setv4; + enter4; + setv04; + + start5; + setv5; + enter5; + setv05; + }; + + automaton proc1 { + clocks { + x1; + }; + locations { + idle1 { init; }; + try1; + wait1; + crit1; + }; + trans { + idle1 -> try1, start1, , { x1; }; + try1 -> wait1, setv1, x1 < 2, { x1; }; + wait1 -> crit1, enter1, x1 > 1, { }; + crit1 -> idle1, setv01, , { }; + }; + }; + + automaton proc2 { + clocks { + x2; + }; + locations { + idle2 { init; }; + try2; + wait2; + crit2; + }; + trans { + idle2 -> try2, start2, , { x2; }; + try2 -> wait2, setv2, x2 < 2, { x2; }; + wait2 -> crit2, enter2, x2 > 1, { }; + crit2 -> idle2, setv02, , { }; + }; + }; + + automaton proc3 { + clocks { + x3; + }; + locations { + idle3 { init; }; + try3; + wait3; + crit3; + }; + trans { + idle3 -> try3, start3, , { x3; }; + try3 -> wait3, setv3, x3 < 2, { x3; }; + wait3 -> crit3, enter3, x3 > 1, { }; + crit3 -> idle3, setv03, , { }; + }; + }; + + automaton proc4 { + clocks { + x4; + }; + locations { + idle4 { init; }; + try4; + wait4; + crit4; + }; + trans { + idle4 -> try4, start4, , { x4; }; + try4 -> wait4, setv4, x4 < 2, { x4; }; + wait4 -> crit4, enter4, x4 > 1, { }; + crit4 -> idle4, setv04, , { }; + }; + }; + + automaton proc5 { + clocks { + x5; + }; + locations { + idle5 { init; }; + try5; + wait5; + crit5; + }; + trans { + idle5 -> try5, start5, , { x5; }; + try5 -> wait5, setv5, x5 < 2, { x5; }; + wait5 -> crit5, enter5, x5 > 1, { }; + crit5 -> idle5, setv05, , { }; + }; + }; + + automaton varV { + locations { + v0 { init; }; + v1; + v2; + v3; + v4; + v5; + }; + trans { + v0 -> v0, start1, , { }; + v0 -> v0, start2, , { }; + v0 -> v0, start3, , { }; + v0 -> v0, start4, , { }; + v0 -> v0, start5, , { }; + v0 -> v1, setv1, , { }; + v0 -> v2, setv2, , { }; + v0 -> v3, setv3, , { }; + v0 -> v4, setv4, , { }; + v0 -> v5, setv5, , { }; + + v1 -> v0, setv01, , { }; + v1 -> v1, enter1, , { }; + v1 -> v1, setv1, , { }; + v1 -> v2, setv2, , { }; + v1 -> v3, setv3, , { }; + v1 -> v4, setv4, , { }; + v1 -> v5, setv5, , { }; + + v2 -> v0, setv02, , { }; + v2 -> v2, enter2, , { }; + v2 -> v1, setv1, , { }; + v2 -> v2, setv2, , { }; + v2 -> v3, setv3, , { }; + v2 -> v4, setv4, , { }; + v2 -> v5, setv5, , { }; + + v3 -> v0, setv03, , { }; + v3 -> v3, enter3, , { }; + v3 -> v1, setv1, , { }; + v3 -> v2, setv2, , { }; + v3 -> v3, setv3, , { }; + v3 -> v4, setv4, , { }; + v3 -> v5, setv5, , { }; + + v4 -> v0, setv04, , { }; + v4 -> v4, enter4, , { }; + v4 -> v1, setv1, , { }; + v4 -> v2, setv2, , { }; + v4 -> v3, setv3, , { }; + v4 -> v4, setv4, , { }; + v4 -> v5, setv5, , { }; + + v5 -> v0, setv05, , { }; + v5 -> v5, enter5, , { }; + v5 -> v1, setv1, , { }; + v5 -> v2, setv2, , { }; + v5 -> v3, setv3, , { }; + v5 -> v4, setv4, , { }; + v5 -> v5, setv5, , { }; + + }; + }; + +}; + +reach { + mutualexclusion_p1p2 { crit1@proc1 crit2@proc2 }; + mutualexclusion_p1p3 { crit1@proc1 crit3@proc3 }; + mutualexclusion_p1p4 { crit1@proc1 crit4@proc4 }; + mutualexclusion_p1p5 { crit1@proc1 crit5@proc5 }; + mutualexclusion_p2p3 { crit2@proc2 crit3@proc3 }; + mutualexclusion_p2p4 { crit2@proc2 crit4@proc4 }; + mutualexclusion_p2p5 { crit2@proc2 crit5@proc5 }; + mutualexclusion_p3p4 { crit3@proc3 crit4@proc4 }; + mutualexclusion_p3p5 { crit3@proc3 crit5@proc5 }; + mutualexclusion_p4p5 { crit4@proc4 crit5@proc5 }; +}; diff --git a/netfiles/fischer5p.aut b/netfiles/fischer5p.aut new file mode 100644 index 0000000..9d3d631 --- /dev/null +++ b/netfiles/fischer5p.aut @@ -0,0 +1,196 @@ +####################################### +# Fischer's mutual exclusion protocol # +####################################### +# # +# przy setv1, setv2 - duza delta # +# przy enter1, enter2 - mala delta # +# # +# wzajemne wykluczanie przy: # +# # +# mala delta >= duza delta # +# # +####################################### + +net { + actions { + start1; + setv1; + enter1; + setv01; + + start2; + setv2; + enter2; + setv02; + + start3; + setv3; + enter3; + setv03; + + start4; + setv4; + enter4; + setv04; + + start5; + setv5; + enter5; + setv05; + }; + + automaton proc1 { + clocks { + x1; + }; + locations { + idle1 { init; }; + try1; + wait1; + crit1; + }; + trans { + idle1 -> try1, start1, , { x1; }; + try1 -> wait1, setv1, x1 < 1, { x1; }; + wait1 -> crit1, enter1, x1 > 2, { }; + crit1 -> idle1, setv01, , { }; + }; + }; + + automaton proc2 { + clocks { + x2; + }; + locations { + idle2 { init; }; + try2; + wait2; + crit2; + }; + trans { + idle2 -> try2, start2, , { x2; }; + try2 -> wait2, setv2, x2 < 1, { x2; }; + wait2 -> crit2, enter2, x2 > 2, { }; + crit2 -> idle2, setv02, , { }; + }; + }; + + automaton proc3 { + clocks { + x3; + }; + locations { + idle3 { init; }; + try3; + wait3; + crit3; + }; + trans { + idle3 -> try3, start3, , { x3; }; + try3 -> wait3, setv3, x3 < 1, { x3; }; + wait3 -> crit3, enter3, x3 > 2, { }; + crit3 -> idle3, setv03, , { }; + }; + }; + + automaton proc4 { + clocks { + x4; + }; + locations { + idle4 { init; }; + try4; + wait4; + crit4; + }; + trans { + idle4 -> try4, start4, , { x4; }; + try4 -> wait4, setv4, x4 < 1, { x4; }; + wait4 -> crit4, enter4, x4 > 2, { }; + crit4 -> idle4, setv04, , { }; + }; + }; + + automaton proc5 { + clocks { + x5; + }; + locations { + idle5 { init; }; + try5; + wait5; + crit5; + }; + trans { + idle5 -> try5, start5, , { x5; }; + try5 -> wait5, setv5, x5 < 1, { x5; }; + wait5 -> crit5, enter5, x5 > 2, { }; + crit5 -> idle5, setv05, , { }; + }; + }; + + automaton varV { + locations { + v0 { init; }; + v1; + v2; + v3; + v4; + v5; + }; + trans { + v0 -> v0, start1, , { }; + v0 -> v0, start2, , { }; + v0 -> v0, start3, , { }; + v0 -> v0, start4, , { }; + v0 -> v0, start5, , { }; + v0 -> v1, setv1, , { }; + v0 -> v2, setv2, , { }; + v0 -> v3, setv3, , { }; + v0 -> v4, setv4, , { }; + v0 -> v5, setv5, , { }; + + v1 -> v0, setv01, , { }; + v1 -> v1, enter1, , { }; + v1 -> v1, setv1, , { }; + v1 -> v2, setv2, , { }; + v1 -> v3, setv3, , { }; + v1 -> v4, setv4, , { }; + v1 -> v5, setv5, , { }; + + v2 -> v0, setv02, , { }; + v2 -> v2, enter2, , { }; + v2 -> v1, setv1, , { }; + v2 -> v2, setv2, , { }; + v2 -> v3, setv3, , { }; + v2 -> v4, setv4, , { }; + v2 -> v5, setv5, , { }; + + v3 -> v0, setv03, , { }; + v3 -> v3, enter3, , { }; + v3 -> v1, setv1, , { }; + v3 -> v2, setv2, , { }; + v3 -> v3, setv3, , { }; + v3 -> v4, setv4, , { }; + v3 -> v5, setv5, , { }; + + v4 -> v0, setv04, , { }; + v4 -> v4, enter4, , { }; + v4 -> v1, setv1, , { }; + v4 -> v2, setv2, , { }; + v4 -> v3, setv3, , { }; + v4 -> v4, setv4, , { }; + v4 -> v5, setv5, , { }; + + v5 -> v0, setv05, , { }; + v5 -> v5, enter5, , { }; + v5 -> v1, setv1, , { }; + v5 -> v2, setv2, , { }; + v5 -> v3, setv3, , { }; + v5 -> v4, setv4, , { }; + v5 -> v5, setv5, , { }; + + }; + }; + +}; \ No newline at end of file diff --git a/netfiles/fischer6p-fail.aut b/netfiles/fischer6p-fail.aut new file mode 100644 index 0000000..d38e970 --- /dev/null +++ b/netfiles/fischer6p-fail.aut @@ -0,0 +1,253 @@ +####################################### +# Fischer's mutual exclusion protocol # +####################################### +# # +# przy setv1, setv2 - duza delta # +# przy enter1, enter2 - mala delta # +# # +# wzajemne wykluczanie przy: # +# # +# mala delta >= duza delta # +# # +####################################### + +net { + actions { + start1; + setv1; + enter1; + setv01; + + start2; + setv2; + enter2; + setv02; + + start3; + setv3; + enter3; + setv03; + + start4; + setv4; + enter4; + setv04; + + start5; + setv5; + enter5; + setv05; + + start6; + setv6; + enter6; + setv06; + }; + + automaton proc1 { + clocks { + x1; + }; + locations { + idle1 { init; }; + try1; + wait1; + crit1; + }; + trans { + idle1 -> try1, start1, , { x1; }; + try1 -> wait1, setv1, x1 < 2, { x1; }; + wait1 -> crit1, enter1, x1 > 1, { }; + crit1 -> idle1, setv01, , { }; + }; + }; + + automaton proc2 { + clocks { + x2; + }; + locations { + idle2 { init; }; + try2; + wait2; + crit2; + }; + trans { + idle2 -> try2, start2, , { x2; }; + try2 -> wait2, setv2, x2 < 2, { x2; }; + wait2 -> crit2, enter2, x2 > 1, { }; + crit2 -> idle2, setv02, , { }; + }; + }; + + automaton proc3 { + clocks { + x3; + }; + locations { + idle3 { init; }; + try3; + wait3; + crit3; + }; + trans { + idle3 -> try3, start3, , { x3; }; + try3 -> wait3, setv3, x3 < 2, { x3; }; + wait3 -> crit3, enter3, x3 > 1, { }; + crit3 -> idle3, setv03, , { }; + }; + }; + + automaton proc4 { + clocks { + x4; + }; + locations { + idle4 { init; }; + try4; + wait4; + crit4; + }; + trans { + idle4 -> try4, start4, , { x4; }; + try4 -> wait4, setv4, x4 < 2, { x4; }; + wait4 -> crit4, enter4, x4 > 1, { }; + crit4 -> idle4, setv04, , { }; + }; + }; + + automaton proc5 { + clocks { + x5; + }; + locations { + idle5 { init; }; + try5; + wait5; + crit5; + }; + trans { + idle5 -> try5, start5, , { x5; }; + try5 -> wait5, setv5, x5 < 2, { x5; }; + wait5 -> crit5, enter5, x5 > 1, { }; + crit5 -> idle5, setv05, , { }; + }; + }; + + automaton proc6 { + clocks { + x6; + }; + locations { + idle6 { init; }; + try6; + wait6; + crit6; + }; + trans { + idle6 -> try6, start6, , { x6; }; + try6 -> wait6, setv6, x6 < 2, { x6; }; + wait6 -> crit6, enter6, x6 > 1, { }; + crit6 -> idle6, setv06, , { }; + }; + }; + + automaton varV { + locations { + v0 { init; }; + v1; + v2; + v3; + v4; + v5; + v6; + }; + trans { + v0 -> v0, start1, , { }; + v0 -> v0, start2, , { }; + v0 -> v0, start3, , { }; + v0 -> v0, start4, , { }; + v0 -> v0, start5, , { }; + v0 -> v0, start6, , { }; + v0 -> v1, setv1, , { }; + v0 -> v2, setv2, , { }; + v0 -> v3, setv3, , { }; + v0 -> v4, setv4, , { }; + v0 -> v5, setv5, , { }; + v0 -> v6, setv6, , { }; + + v1 -> v0, setv01, , { }; + v1 -> v1, enter1, , { }; + v1 -> v1, setv1, , { }; + v1 -> v2, setv2, , { }; + v1 -> v3, setv3, , { }; + v1 -> v4, setv4, , { }; + v1 -> v5, setv5, , { }; + v1 -> v6, setv6, , { }; + + v2 -> v0, setv02, , { }; + v2 -> v2, enter2, , { }; + v2 -> v1, setv1, , { }; + v2 -> v2, setv2, , { }; + v2 -> v3, setv3, , { }; + v2 -> v4, setv4, , { }; + v2 -> v5, setv5, , { }; + v2 -> v6, setv6, , { }; + + v3 -> v0, setv03, , { }; + v3 -> v3, enter3, , { }; + v3 -> v1, setv1, , { }; + v3 -> v2, setv2, , { }; + v3 -> v3, setv3, , { }; + v3 -> v4, setv4, , { }; + v3 -> v5, setv5, , { }; + v3 -> v6, setv6, , { }; + + v4 -> v0, setv04, , { }; + v4 -> v4, enter4, , { }; + v4 -> v1, setv1, , { }; + v4 -> v2, setv2, , { }; + v4 -> v3, setv3, , { }; + v4 -> v4, setv4, , { }; + v4 -> v5, setv5, , { }; + v4 -> v6, setv6, , { }; + + v5 -> v0, setv05, , { }; + v5 -> v5, enter5, , { }; + v5 -> v1, setv1, , { }; + v5 -> v2, setv2, , { }; + v5 -> v3, setv3, , { }; + v5 -> v4, setv4, , { }; + v5 -> v5, setv5, , { }; + v5 -> v6, setv6, , { }; + + v6 -> v0, setv06, , { }; + v6 -> v6, enter6, , { }; + v6 -> v1, setv1, , { }; + v6 -> v2, setv2, , { }; + v6 -> v3, setv3, , { }; + v6 -> v4, setv4, , { }; + v6 -> v5, setv5, , { }; + v6 -> v6, setv6, , { }; + }; + }; + +}; + +reach { + mutualexclusion_p1p2 { crit1@proc1 crit2@proc2 }; + mutualexclusion_p1p3 { crit1@proc1 crit3@proc3 }; + mutualexclusion_p1p4 { crit1@proc1 crit4@proc4 }; + mutualexclusion_p1p5 { crit1@proc1 crit5@proc5 }; + mutualexclusion_p1p6 { crit1@proc1 crit6@proc6 }; + mutualexclusion_p2p3 { crit2@proc2 crit3@proc3 }; + mutualexclusion_p2p4 { crit2@proc2 crit4@proc4 }; + mutualexclusion_p2p5 { crit2@proc2 crit5@proc5 }; + mutualexclusion_p2p6 { crit2@proc2 crit6@proc6 }; + mutualexclusion_p3p4 { crit3@proc3 crit4@proc4 }; + mutualexclusion_p3p5 { crit3@proc3 crit5@proc5 }; + mutualexclusion_p3p6 { crit3@proc3 crit6@proc6 }; + mutualexclusion_p4p5 { crit4@proc4 crit5@proc5 }; + mutualexclusion_p4p6 { crit4@proc4 crit6@proc6 }; + mutualexclusion_p5p6 { crit5@proc5 crit6@proc6 }; +}; diff --git a/netfiles/fischer6p.aut b/netfiles/fischer6p.aut new file mode 100644 index 0000000..b782319 --- /dev/null +++ b/netfiles/fischer6p.aut @@ -0,0 +1,235 @@ +####################################### +# Fischer's mutual exclusion protocol # +####################################### +# # +# przy setv1, setv2 - duza delta # +# przy enter1, enter2 - mala delta # +# # +# wzajemne wykluczanie przy: # +# # +# mala delta >= duza delta # +# # +####################################### + +net { + actions { + start1; + setv1; + enter1; + setv01; + + start2; + setv2; + enter2; + setv02; + + start3; + setv3; + enter3; + setv03; + + start4; + setv4; + enter4; + setv04; + + start5; + setv5; + enter5; + setv05; + + start6; + setv6; + enter6; + setv06; + }; + + automaton proc1 { + clocks { + x1; + }; + locations { + idle1 { init; }; + try1; + wait1; + crit1; + }; + trans { + idle1 -> try1, start1, , { x1; }; + try1 -> wait1, setv1, x1 < 1, { x1; }; + wait1 -> crit1, enter1, x1 > 2, { }; + crit1 -> idle1, setv01, , { }; + }; + }; + + automaton proc2 { + clocks { + x2; + }; + locations { + idle2 { init; }; + try2; + wait2; + crit2; + }; + trans { + idle2 -> try2, start2, , { x2; }; + try2 -> wait2, setv2, x2 < 1, { x2; }; + wait2 -> crit2, enter2, x2 > 2, { }; + crit2 -> idle2, setv02, , { }; + }; + }; + + automaton proc3 { + clocks { + x3; + }; + locations { + idle3 { init; }; + try3; + wait3; + crit3; + }; + trans { + idle3 -> try3, start3, , { x3; }; + try3 -> wait3, setv3, x3 < 1, { x3; }; + wait3 -> crit3, enter3, x3 > 2, { }; + crit3 -> idle3, setv03, , { }; + }; + }; + + automaton proc4 { + clocks { + x4; + }; + locations { + idle4 { init; }; + try4; + wait4; + crit4; + }; + trans { + idle4 -> try4, start4, , { x4; }; + try4 -> wait4, setv4, x4 < 1, { x4; }; + wait4 -> crit4, enter4, x4 > 2, { }; + crit4 -> idle4, setv04, , { }; + }; + }; + + automaton proc5 { + clocks { + x5; + }; + locations { + idle5 { init; }; + try5; + wait5; + crit5; + }; + trans { + idle5 -> try5, start5, , { x5; }; + try5 -> wait5, setv5, x5 < 1, { x5; }; + wait5 -> crit5, enter5, x5 > 2, { }; + crit5 -> idle5, setv05, , { }; + }; + }; + + automaton proc6 { + clocks { + x6; + }; + locations { + idle6 { init; }; + try6; + wait6; + crit6; + }; + trans { + idle6 -> try6, start6, , { x6; }; + try6 -> wait6, setv6, x6 < 1, { x6; }; + wait6 -> crit6, enter6, x6 > 2, { }; + crit6 -> idle6, setv06, , { }; + }; + }; + + automaton varV { + locations { + v0 { init; }; + v1; + v2; + v3; + v4; + v5; + v6; + }; + trans { + v0 -> v0, start1, , { }; + v0 -> v0, start2, , { }; + v0 -> v0, start3, , { }; + v0 -> v0, start4, , { }; + v0 -> v0, start5, , { }; + v0 -> v0, start6, , { }; + v0 -> v1, setv1, , { }; + v0 -> v2, setv2, , { }; + v0 -> v3, setv3, , { }; + v0 -> v4, setv4, , { }; + v0 -> v5, setv5, , { }; + v0 -> v6, setv6, , { }; + + v1 -> v0, setv01, , { }; + v1 -> v1, enter1, , { }; + v1 -> v1, setv1, , { }; + v1 -> v2, setv2, , { }; + v1 -> v3, setv3, , { }; + v1 -> v4, setv4, , { }; + v1 -> v5, setv5, , { }; + v1 -> v6, setv6, , { }; + + v2 -> v0, setv02, , { }; + v2 -> v2, enter2, , { }; + v2 -> v1, setv1, , { }; + v2 -> v2, setv2, , { }; + v2 -> v3, setv3, , { }; + v2 -> v4, setv4, , { }; + v2 -> v5, setv5, , { }; + v2 -> v6, setv6, , { }; + + v3 -> v0, setv03, , { }; + v3 -> v3, enter3, , { }; + v3 -> v1, setv1, , { }; + v3 -> v2, setv2, , { }; + v3 -> v3, setv3, , { }; + v3 -> v4, setv4, , { }; + v3 -> v5, setv5, , { }; + v3 -> v6, setv6, , { }; + + v4 -> v0, setv04, , { }; + v4 -> v4, enter4, , { }; + v4 -> v1, setv1, , { }; + v4 -> v2, setv2, , { }; + v4 -> v3, setv3, , { }; + v4 -> v4, setv4, , { }; + v4 -> v5, setv5, , { }; + v4 -> v6, setv6, , { }; + + v5 -> v0, setv05, , { }; + v5 -> v5, enter5, , { }; + v5 -> v1, setv1, , { }; + v5 -> v2, setv2, , { }; + v5 -> v3, setv3, , { }; + v5 -> v4, setv4, , { }; + v5 -> v5, setv5, , { }; + v5 -> v6, setv6, , { }; + + v6 -> v0, setv06, , { }; + v6 -> v6, enter6, , { }; + v6 -> v1, setv1, , { }; + v6 -> v2, setv2, , { }; + v6 -> v3, setv3, , { }; + v6 -> v4, setv4, , { }; + v6 -> v5, setv5, , { }; + v6 -> v6, setv6, , { }; + }; + }; + +}; diff --git a/netfiles/fischer7p-fail.aut b/netfiles/fischer7p-fail.aut new file mode 100644 index 0000000..dea594c --- /dev/null +++ b/netfiles/fischer7p-fail.aut @@ -0,0 +1,301 @@ +####################################### +# Fischer's mutual exclusion protocol # +####################################### +# # +# przy setv1, setv2 - duza delta # +# przy enter1, enter2 - mala delta # +# # +# wzajemne wykluczanie przy: # +# # +# mala delta >= duza delta # +# # +####################################### + +net { + actions { + start1; + setv1; + enter1; + setv01; + + start2; + setv2; + enter2; + setv02; + + start3; + setv3; + enter3; + setv03; + + start4; + setv4; + enter4; + setv04; + + start5; + setv5; + enter5; + setv05; + + start6; + setv6; + enter6; + setv06; + + start7; + setv7; + enter7; + setv07; + }; + + automaton proc1 { + clocks { + x1; + }; + locations { + idle1 { init; }; + try1; + wait1; + crit1; + }; + trans { + idle1 -> try1, start1, , { x1; }; + try1 -> wait1, setv1, x1 < 2, { x1; }; + wait1 -> crit1, enter1, x1 > 1, { }; + crit1 -> idle1, setv01, , { }; + }; + }; + + automaton proc2 { + clocks { + x2; + }; + locations { + idle2 { init; }; + try2; + wait2; + crit2; + }; + trans { + idle2 -> try2, start2, , { x2; }; + try2 -> wait2, setv2, x2 < 2, { x2; }; + wait2 -> crit2, enter2, x2 > 1, { }; + crit2 -> idle2, setv02, , { }; + }; + }; + + automaton proc3 { + clocks { + x3; + }; + locations { + idle3 { init; }; + try3; + wait3; + crit3; + }; + trans { + idle3 -> try3, start3, , { x3; }; + try3 -> wait3, setv3, x3 < 2, { x3; }; + wait3 -> crit3, enter3, x3 > 1, { }; + crit3 -> idle3, setv03, , { }; + }; + }; + + automaton proc4 { + clocks { + x4; + }; + locations { + idle4 { init; }; + try4; + wait4; + crit4; + }; + trans { + idle4 -> try4, start4, , { x4; }; + try4 -> wait4, setv4, x4 < 2, { x4; }; + wait4 -> crit4, enter4, x4 > 1, { }; + crit4 -> idle4, setv04, , { }; + }; + }; + + automaton proc5 { + clocks { + x5; + }; + locations { + idle5 { init; }; + try5; + wait5; + crit5; + }; + trans { + idle5 -> try5, start5, , { x5; }; + try5 -> wait5, setv5, x5 < 2, { x5; }; + wait5 -> crit5, enter5, x5 > 1, { }; + crit5 -> idle5, setv05, , { }; + }; + }; + + automaton proc6 { + clocks { + x6; + }; + locations { + idle6 { init; }; + try6; + wait6; + crit6; + }; + trans { + idle6 -> try6, start6, , { x6; }; + try6 -> wait6, setv6, x6 < 2, { x6; }; + wait6 -> crit6, enter6, x6 > 1, { }; + crit6 -> idle6, setv06, , { }; + }; + }; + + automaton proc7 { + clocks { + x7; + }; + locations { + idle7 { init; }; + try7; + wait7; + crit7; + }; + trans { + idle7 -> try7, start7, , { x7; }; + try7 -> wait7, setv7, x7 < 2, { x7; }; + wait7 -> crit7, enter7, x7 > 1, { }; + crit7 -> idle7, setv07, , { }; + }; + }; + + automaton varV { + locations { + v0 { init; }; + v1; + v2; + v3; + v4; + v5; + v6; + v7; + }; + trans { + v0 -> v0, start1, , { }; + v0 -> v0, start2, , { }; + v0 -> v0, start3, , { }; + v0 -> v0, start4, , { }; + v0 -> v0, start5, , { }; + v0 -> v0, start6, , { }; + v0 -> v0, start7, , { }; + v0 -> v1, setv1, , { }; + v0 -> v2, setv2, , { }; + v0 -> v3, setv3, , { }; + v0 -> v4, setv4, , { }; + v0 -> v5, setv5, , { }; + v0 -> v6, setv6, , { }; + v0 -> v7, setv7, , { }; + + v1 -> v0, setv01, , { }; + v1 -> v1, enter1, , { }; + v1 -> v1, setv1, , { }; + v1 -> v2, setv2, , { }; + v1 -> v3, setv3, , { }; + v1 -> v4, setv4, , { }; + v1 -> v5, setv5, , { }; + v1 -> v6, setv6, , { }; + v1 -> v7, setv7, , { }; + + v2 -> v0, setv02, , { }; + v2 -> v2, enter2, , { }; + v2 -> v1, setv1, , { }; + v2 -> v2, setv2, , { }; + v2 -> v3, setv3, , { }; + v2 -> v4, setv4, , { }; + v2 -> v5, setv5, , { }; + v2 -> v6, setv6, , { }; + v2 -> v7, setv7, , { }; + + v3 -> v0, setv03, , { }; + v3 -> v3, enter3, , { }; + v3 -> v1, setv1, , { }; + v3 -> v2, setv2, , { }; + v3 -> v3, setv3, , { }; + v3 -> v4, setv4, , { }; + v3 -> v5, setv5, , { }; + v3 -> v6, setv6, , { }; + v3 -> v7, setv7, , { }; + + v4 -> v0, setv04, , { }; + v4 -> v4, enter4, , { }; + v4 -> v1, setv1, , { }; + v4 -> v2, setv2, , { }; + v4 -> v3, setv3, , { }; + v4 -> v4, setv4, , { }; + v4 -> v5, setv5, , { }; + v4 -> v6, setv6, , { }; + v4 -> v7, setv7, , { }; + + v5 -> v0, setv05, , { }; + v5 -> v5, enter5, , { }; + v5 -> v1, setv1, , { }; + v5 -> v2, setv2, , { }; + v5 -> v3, setv3, , { }; + v5 -> v4, setv4, , { }; + v5 -> v5, setv5, , { }; + v5 -> v6, setv6, , { }; + v5 -> v7, setv7, , { }; + + v6 -> v0, setv06, , { }; + v6 -> v6, enter6, , { }; + v6 -> v1, setv1, , { }; + v6 -> v2, setv2, , { }; + v6 -> v3, setv3, , { }; + v6 -> v4, setv4, , { }; + v6 -> v5, setv5, , { }; + v6 -> v6, setv6, , { }; + v6 -> v7, setv7, , { }; + + v7 -> v0, setv07, , { }; + v7 -> v7, enter7, , { }; + v7 -> v1, setv1, , { }; + v7 -> v2, setv2, , { }; + v7 -> v3, setv3, , { }; + v7 -> v4, setv4, , { }; + v7 -> v5, setv5, , { }; + v7 -> v6, setv6, , { }; + v7 -> v7, setv7, , { }; + }; + }; + +}; + +reach { + mutualexclusion_p1p2 { crit1@proc1 crit2@proc2 }; + mutualexclusion_p1p3 { crit1@proc1 crit3@proc3 }; + mutualexclusion_p1p4 { crit1@proc1 crit4@proc4 }; + mutualexclusion_p1p5 { crit1@proc1 crit5@proc5 }; + mutualexclusion_p1p6 { crit1@proc1 crit6@proc6 }; + mutualexclusion_p1p7 { crit1@proc1 crit7@proc7 }; + mutualexclusion_p2p3 { crit2@proc2 crit3@proc3 }; + mutualexclusion_p2p4 { crit2@proc2 crit4@proc4 }; + mutualexclusion_p2p5 { crit2@proc2 crit5@proc5 }; + mutualexclusion_p2p6 { crit2@proc2 crit6@proc6 }; + mutualexclusion_p2p7 { crit2@proc2 crit7@proc7 }; + mutualexclusion_p3p4 { crit3@proc3 crit4@proc4 }; + mutualexclusion_p3p5 { crit3@proc3 crit5@proc5 }; + mutualexclusion_p3p6 { crit3@proc3 crit6@proc6 }; + mutualexclusion_p3p7 { crit3@proc3 crit7@proc7 }; + mutualexclusion_p4p5 { crit4@proc4 crit5@proc5 }; + mutualexclusion_p4p6 { crit4@proc4 crit6@proc6 }; + mutualexclusion_p4p7 { crit4@proc4 crit7@proc7 }; + mutualexclusion_p5p6 { crit5@proc5 crit6@proc6 }; + mutualexclusion_p5p7 { crit5@proc5 crit7@proc7 }; + mutualexclusion_p6p7 { crit6@proc6 crit7@proc7 }; +}; diff --git a/netfiles/fischer7p.aut b/netfiles/fischer7p.aut new file mode 100644 index 0000000..00c533b --- /dev/null +++ b/netfiles/fischer7p.aut @@ -0,0 +1,301 @@ +####################################### +# Fischer's mutual exclusion protocol # +####################################### +# # +# przy setv1, setv2 - duza delta # +# przy enter1, enter2 - mala delta # +# # +# wzajemne wykluczanie przy: # +# # +# mala delta >= duza delta # +# # +####################################### + +net { + actions { + start1; + setv1; + enter1; + setv01; + + start2; + setv2; + enter2; + setv02; + + start3; + setv3; + enter3; + setv03; + + start4; + setv4; + enter4; + setv04; + + start5; + setv5; + enter5; + setv05; + + start6; + setv6; + enter6; + setv06; + + start7; + setv7; + enter7; + setv07; + }; + + automaton proc1 { + clocks { + x1; + }; + locations { + idle1 { init; }; + try1; + wait1; + crit1; + }; + trans { + idle1 -> try1, start1, , { x1; }; + try1 -> wait1, setv1, x1 < 1, { x1; }; + wait1 -> crit1, enter1, x1 > 2, { }; + crit1 -> idle1, setv01, , { }; + }; + }; + + automaton proc2 { + clocks { + x2; + }; + locations { + idle2 { init; }; + try2; + wait2; + crit2; + }; + trans { + idle2 -> try2, start2, , { x2; }; + try2 -> wait2, setv2, x2 < 1, { x2; }; + wait2 -> crit2, enter2, x2 > 2, { }; + crit2 -> idle2, setv02, , { }; + }; + }; + + automaton proc3 { + clocks { + x3; + }; + locations { + idle3 { init; }; + try3; + wait3; + crit3; + }; + trans { + idle3 -> try3, start3, , { x3; }; + try3 -> wait3, setv3, x3 < 1, { x3; }; + wait3 -> crit3, enter3, x3 > 2, { }; + crit3 -> idle3, setv03, , { }; + }; + }; + + automaton proc4 { + clocks { + x4; + }; + locations { + idle4 { init; }; + try4; + wait4; + crit4; + }; + trans { + idle4 -> try4, start4, , { x4; }; + try4 -> wait4, setv4, x4 < 1, { x4; }; + wait4 -> crit4, enter4, x4 > 2, { }; + crit4 -> idle4, setv04, , { }; + }; + }; + + automaton proc5 { + clocks { + x5; + }; + locations { + idle5 { init; }; + try5; + wait5; + crit5; + }; + trans { + idle5 -> try5, start5, , { x5; }; + try5 -> wait5, setv5, x5 < 1, { x5; }; + wait5 -> crit5, enter5, x5 > 2, { }; + crit5 -> idle5, setv05, , { }; + }; + }; + + automaton proc6 { + clocks { + x6; + }; + locations { + idle6 { init; }; + try6; + wait6; + crit6; + }; + trans { + idle6 -> try6, start6, , { x6; }; + try6 -> wait6, setv6, x6 < 1, { x6; }; + wait6 -> crit6, enter6, x6 > 2, { }; + crit6 -> idle6, setv06, , { }; + }; + }; + + automaton proc7 { + clocks { + x7; + }; + locations { + idle7 { init; }; + try7; + wait7; + crit7; + }; + trans { + idle7 -> try7, start7, , { x7; }; + try7 -> wait7, setv7, x7 < 1, { x7; }; + wait7 -> crit7, enter7, x7 > 2, { }; + crit7 -> idle7, setv07, , { }; + }; + }; + + automaton varV { + locations { + v0 { init; }; + v1; + v2; + v3; + v4; + v5; + v6; + v7; + }; + trans { + v0 -> v0, start1, , { }; + v0 -> v0, start2, , { }; + v0 -> v0, start3, , { }; + v0 -> v0, start4, , { }; + v0 -> v0, start5, , { }; + v0 -> v0, start6, , { }; + v0 -> v0, start7, , { }; + v0 -> v1, setv1, , { }; + v0 -> v2, setv2, , { }; + v0 -> v3, setv3, , { }; + v0 -> v4, setv4, , { }; + v0 -> v5, setv5, , { }; + v0 -> v6, setv6, , { }; + v0 -> v7, setv7, , { }; + + v1 -> v0, setv01, , { }; + v1 -> v1, enter1, , { }; + v1 -> v1, setv1, , { }; + v1 -> v2, setv2, , { }; + v1 -> v3, setv3, , { }; + v1 -> v4, setv4, , { }; + v1 -> v5, setv5, , { }; + v1 -> v6, setv6, , { }; + v1 -> v7, setv7, , { }; + + v2 -> v0, setv02, , { }; + v2 -> v2, enter2, , { }; + v2 -> v1, setv1, , { }; + v2 -> v2, setv2, , { }; + v2 -> v3, setv3, , { }; + v2 -> v4, setv4, , { }; + v2 -> v5, setv5, , { }; + v2 -> v6, setv6, , { }; + v2 -> v7, setv7, , { }; + + v3 -> v0, setv03, , { }; + v3 -> v3, enter3, , { }; + v3 -> v1, setv1, , { }; + v3 -> v2, setv2, , { }; + v3 -> v3, setv3, , { }; + v3 -> v4, setv4, , { }; + v3 -> v5, setv5, , { }; + v3 -> v6, setv6, , { }; + v3 -> v7, setv7, , { }; + + v4 -> v0, setv04, , { }; + v4 -> v4, enter4, , { }; + v4 -> v1, setv1, , { }; + v4 -> v2, setv2, , { }; + v4 -> v3, setv3, , { }; + v4 -> v4, setv4, , { }; + v4 -> v5, setv5, , { }; + v4 -> v6, setv6, , { }; + v4 -> v7, setv7, , { }; + + v5 -> v0, setv05, , { }; + v5 -> v5, enter5, , { }; + v5 -> v1, setv1, , { }; + v5 -> v2, setv2, , { }; + v5 -> v3, setv3, , { }; + v5 -> v4, setv4, , { }; + v5 -> v5, setv5, , { }; + v5 -> v6, setv6, , { }; + v5 -> v7, setv7, , { }; + + v6 -> v0, setv06, , { }; + v6 -> v6, enter6, , { }; + v6 -> v1, setv1, , { }; + v6 -> v2, setv2, , { }; + v6 -> v3, setv3, , { }; + v6 -> v4, setv4, , { }; + v6 -> v5, setv5, , { }; + v6 -> v6, setv6, , { }; + v6 -> v7, setv7, , { }; + + v7 -> v0, setv07, , { }; + v7 -> v7, enter7, , { }; + v7 -> v1, setv1, , { }; + v7 -> v2, setv2, , { }; + v7 -> v3, setv3, , { }; + v7 -> v4, setv4, , { }; + v7 -> v5, setv5, , { }; + v7 -> v6, setv6, , { }; + v7 -> v7, setv7, , { }; + }; + }; + +}; + +reach { + mutualexclusion_p1p2 { crit1@proc1 crit2@proc2 }; + mutualexclusion_p1p3 { crit1@proc1 crit3@proc3 }; + mutualexclusion_p1p4 { crit1@proc1 crit4@proc4 }; + mutualexclusion_p1p5 { crit1@proc1 crit5@proc5 }; + mutualexclusion_p1p6 { crit1@proc1 crit6@proc6 }; + mutualexclusion_p1p7 { crit1@proc1 crit7@proc7 }; + mutualexclusion_p2p3 { crit2@proc2 crit3@proc3 }; + mutualexclusion_p2p4 { crit2@proc2 crit4@proc4 }; + mutualexclusion_p2p5 { crit2@proc2 crit5@proc5 }; + mutualexclusion_p2p6 { crit2@proc2 crit6@proc6 }; + mutualexclusion_p2p7 { crit2@proc2 crit7@proc7 }; + mutualexclusion_p3p4 { crit3@proc3 crit4@proc4 }; + mutualexclusion_p3p5 { crit3@proc3 crit5@proc5 }; + mutualexclusion_p3p6 { crit3@proc3 crit6@proc6 }; + mutualexclusion_p3p7 { crit3@proc3 crit7@proc7 }; + mutualexclusion_p4p5 { crit4@proc4 crit5@proc5 }; + mutualexclusion_p4p6 { crit4@proc4 crit6@proc6 }; + mutualexclusion_p4p7 { crit4@proc4 crit7@proc7 }; + mutualexclusion_p5p6 { crit5@proc5 crit6@proc6 }; + mutualexclusion_p5p7 { crit5@proc5 crit7@proc7 }; + mutualexclusion_p6p7 { crit6@proc6 crit7@proc7 }; +}; diff --git a/netfiles/fischer8p.aut b/netfiles/fischer8p.aut new file mode 100644 index 0000000..606f4b1 --- /dev/null +++ b/netfiles/fischer8p.aut @@ -0,0 +1,354 @@ +####################################### +# Fischer's mutual exclusion protocol # +# dla 8 procesow # +####################################### +# # +# przy setv1, setv2 - duza delta # +# przy enter1, enter2 - mala delta # +# # +# wzajemne wykluczanie przy: # +# # +# mala delta >= duza delta # +# # +####################################### + +net { + actions { + start1; + setv1; + enter1; + setv01; + + start2; + setv2; + enter2; + setv02; + + start3; + setv3; + enter3; + setv03; + + start4; + setv4; + enter4; + setv04; + + start5; + setv5; + enter5; + setv05; + + start6; + setv6; + enter6; + setv06; + + start7; + setv7; + enter7; + setv07; + + start8; + setv8; + enter8; + setv08; + }; + + automaton proc1 { + clocks { + x1; + }; + locations { + idle1 { init; }; + try1; + wait1; + crit1; + }; + trans { + idle1 -> try1, start1, , { x1; }; + try1 -> wait1, setv1, x1 < 1, { x1; }; + wait1 -> crit1, enter1, x1 > 2, { }; + crit1 -> idle1, setv01, , { }; + }; + }; + + automaton proc2 { + clocks { + x2; + }; + locations { + idle2 { init; }; + try2; + wait2; + crit2; + }; + trans { + idle2 -> try2, start2, , { x2; }; + try2 -> wait2, setv2, x2 < 1, { x2; }; + wait2 -> crit2, enter2, x2 > 2, { }; + crit2 -> idle2, setv02, , { }; + }; + }; + + automaton proc3 { + clocks { + x3; + }; + locations { + idle3 { init; }; + try3; + wait3; + crit3; + }; + trans { + idle3 -> try3, start3, , { x3; }; + try3 -> wait3, setv3, x3 < 1, { x3; }; + wait3 -> crit3, enter3, x3 > 2, { }; + crit3 -> idle3, setv03, , { }; + }; + }; + + automaton proc4 { + clocks { + x4; + }; + locations { + idle4 { init; }; + try4; + wait4; + crit4; + }; + trans { + idle4 -> try4, start4, , { x4; }; + try4 -> wait4, setv4, x4 < 1, { x4; }; + wait4 -> crit4, enter4, x4 > 2, { }; + crit4 -> idle4, setv04, , { }; + }; + }; + + automaton proc5 { + clocks { + x5; + }; + locations { + idle5 { init; }; + try5; + wait5; + crit5; + }; + trans { + idle5 -> try5, start5, , { x5; }; + try5 -> wait5, setv5, x5 < 1, { x5; }; + wait5 -> crit5, enter5, x5 > 2, { }; + crit5 -> idle5, setv05, , { }; + }; + }; + + automaton proc6 { + clocks { + x6; + }; + locations { + idle6 { init; }; + try6; + wait6; + crit6; + }; + trans { + idle6 -> try6, start6, , { x6; }; + try6 -> wait6, setv6, x6 < 1, { x6; }; + wait6 -> crit6, enter6, x6 > 2, { }; + crit6 -> idle6, setv06, , { }; + }; + }; + + automaton proc7 { + clocks { + x7; + }; + locations { + idle7 { init; }; + try7; + wait7; + crit7; + }; + trans { + idle7 -> try7, start7, , { x7; }; + try7 -> wait7, setv7, x7 < 1, { x7; }; + wait7 -> crit7, enter7, x7 > 2, { }; + crit7 -> idle7, setv07, , { }; + }; + }; + + automaton proc8 { + clocks { + x8; + }; + locations { + idle8 { init; }; + try8; + wait8; + crit8; + }; + trans { + idle8 -> try8, start8, , { x8; }; + try8 -> wait8, setv8, x8 < 1, { x8; }; + wait8 -> crit8, enter8, x8 > 2, { }; + crit8 -> idle8, setv08, , { }; + }; + }; + + automaton varV { + locations { + v0 { init; }; + v1; + v2; + v3; + v4; + v5; + v6; + v7; + v8; + }; + trans { + v0 -> v0, start1, , { }; + v0 -> v0, start2, , { }; + v0 -> v0, start3, , { }; + v0 -> v0, start4, , { }; + v0 -> v0, start5, , { }; + v0 -> v0, start6, , { }; + v0 -> v0, start7, , { }; + v0 -> v0, start8, , { }; + v0 -> v1, setv1, , { }; + v0 -> v2, setv2, , { }; + v0 -> v3, setv3, , { }; + v0 -> v4, setv4, , { }; + v0 -> v5, setv5, , { }; + v0 -> v6, setv6, , { }; + v0 -> v7, setv7, , { }; + v0 -> v8, setv8, , { }; + + v1 -> v0, setv01, , { }; + v1 -> v1, enter1, , { }; + v1 -> v1, setv1, , { }; + v1 -> v2, setv2, , { }; + v1 -> v3, setv3, , { }; + v1 -> v4, setv4, , { }; + v1 -> v5, setv5, , { }; + v1 -> v6, setv6, , { }; + v1 -> v7, setv7, , { }; + v1 -> v8, setv8, , { }; + + v2 -> v0, setv02, , { }; + v2 -> v2, enter2, , { }; + v2 -> v1, setv1, , { }; + v2 -> v2, setv2, , { }; + v2 -> v3, setv3, , { }; + v2 -> v4, setv4, , { }; + v2 -> v5, setv5, , { }; + v2 -> v6, setv6, , { }; + v2 -> v7, setv7, , { }; + v2 -> v8, setv8, , { }; + + v3 -> v0, setv03, , { }; + v3 -> v3, enter3, , { }; + v3 -> v1, setv1, , { }; + v3 -> v2, setv2, , { }; + v3 -> v3, setv3, , { }; + v3 -> v4, setv4, , { }; + v3 -> v5, setv5, , { }; + v3 -> v6, setv6, , { }; + v3 -> v7, setv7, , { }; + v3 -> v8, setv8, , { }; + + v4 -> v0, setv04, , { }; + v4 -> v4, enter4, , { }; + v4 -> v1, setv1, , { }; + v4 -> v2, setv2, , { }; + v4 -> v3, setv3, , { }; + v4 -> v4, setv4, , { }; + v4 -> v5, setv5, , { }; + v4 -> v6, setv6, , { }; + v4 -> v7, setv7, , { }; + v4 -> v8, setv8, , { }; + + v5 -> v0, setv05, , { }; + v5 -> v5, enter5, , { }; + v5 -> v1, setv1, , { }; + v5 -> v2, setv2, , { }; + v5 -> v3, setv3, , { }; + v5 -> v4, setv4, , { }; + v5 -> v5, setv5, , { }; + v5 -> v6, setv6, , { }; + v5 -> v7, setv7, , { }; + v5 -> v8, setv8, , { }; + + v6 -> v0, setv06, , { }; + v6 -> v6, enter6, , { }; + v6 -> v1, setv1, , { }; + v6 -> v2, setv2, , { }; + v6 -> v3, setv3, , { }; + v6 -> v4, setv4, , { }; + v6 -> v5, setv5, , { }; + v6 -> v6, setv6, , { }; + v6 -> v7, setv7, , { }; + v6 -> v8, setv8, , { }; + + v7 -> v0, setv07, , { }; + v7 -> v7, enter7, , { }; + v7 -> v1, setv1, , { }; + v7 -> v2, setv2, , { }; + v7 -> v3, setv3, , { }; + v7 -> v4, setv4, , { }; + v7 -> v5, setv5, , { }; + v7 -> v6, setv6, , { }; + v7 -> v7, setv7, , { }; + v7 -> v8, setv8, , { }; + + v8 -> v0, setv08, , { }; + v8 -> v8, enter8, , { }; + v8 -> v1, setv1, , { }; + v8 -> v2, setv2, , { }; + v8 -> v3, setv3, , { }; + v8 -> v4, setv4, , { }; + v8 -> v5, setv5, , { }; + v8 -> v6, setv6, , { }; + v8 -> v7, setv7, , { }; + v8 -> v8, setv8, , { }; + + }; + }; + +}; + +reach { + mutualexclusion_p1p2 { crit1@proc1 crit2@proc2 }; + mutualexclusion_p1p3 { crit1@proc1 crit3@proc3 }; + mutualexclusion_p1p4 { crit1@proc1 crit4@proc4 }; + mutualexclusion_p1p5 { crit1@proc1 crit5@proc5 }; + mutualexclusion_p1p6 { crit1@proc1 crit6@proc6 }; + mutualexclusion_p1p7 { crit1@proc1 crit7@proc7 }; + mutualexclusion_p1p8 { crit1@proc1 crit8@proc8 }; + mutualexclusion_p2p3 { crit2@proc2 crit3@proc3 }; + mutualexclusion_p2p4 { crit2@proc2 crit4@proc4 }; + mutualexclusion_p2p5 { crit2@proc2 crit5@proc5 }; + mutualexclusion_p2p6 { crit2@proc2 crit6@proc6 }; + mutualexclusion_p2p7 { crit2@proc2 crit7@proc7 }; + mutualexclusion_p2p8 { crit2@proc2 crit8@proc8 }; + mutualexclusion_p3p4 { crit3@proc3 crit4@proc4 }; + mutualexclusion_p3p5 { crit3@proc3 crit5@proc5 }; + mutualexclusion_p3p6 { crit3@proc3 crit6@proc6 }; + mutualexclusion_p3p7 { crit3@proc3 crit7@proc7 }; + mutualexclusion_p3p8 { crit3@proc3 crit8@proc8 }; + mutualexclusion_p4p5 { crit4@proc4 crit5@proc5 }; + mutualexclusion_p4p6 { crit4@proc4 crit6@proc6 }; + mutualexclusion_p4p7 { crit4@proc4 crit7@proc7 }; + mutualexclusion_p4p8 { crit4@proc4 crit8@proc8 }; + mutualexclusion_p5p6 { crit5@proc5 crit6@proc6 }; + mutualexclusion_p5p7 { crit5@proc5 crit7@proc7 }; + mutualexclusion_p5p8 { crit5@proc5 crit8@proc8 }; + mutualexclusion_p6p7 { crit6@proc6 crit7@proc7 }; + mutualexclusion_p6p8 { crit6@proc6 crit8@proc8 }; + mutualexclusion_p7p8 { crit7@proc7 crit8@proc8 }; +}; diff --git a/netfiles/test-empty.ta b/netfiles/test-empty.ta new file mode 100644 index 0000000..4fd5b81 --- /dev/null +++ b/netfiles/test-empty.ta @@ -0,0 +1 @@ +net { }; diff --git a/netfiles/test-zn-clockconstrs.aut b/netfiles/test-zn-clockconstrs.aut new file mode 100644 index 0000000..4264bd7 --- /dev/null +++ b/netfiles/test-zn-clockconstrs.aut @@ -0,0 +1,39 @@ +# siec automatow z ZN, ale bez zmiennych calkowitych +# niezmienniki lokacji i ograniczenia na przejsciach uniemozliwiaja niektore z nich + +net { + + actions { m; n; p; q; w; }; + + automaton automacikB1 { + clocks { + x1; + }; + locations { + a { init; }; + b { inv x1 < 1; }; + }; + trans { + a -> b , m , , { x1; }; + b -> b , q , , { }; + b -> a , n , , { }; + }; + }; + + automaton automacikB2 { + clocks { + x2; + }; + locations { + d; + c { init; }; + e { inv x2 < 3; }; + }; + trans { + c -> d , p , , { }; + d -> e , m , x2 > 3 , { }; + e -> c , n , , { x2; }; + }; + }; + +}; diff --git a/netfiles/test-zn.aut b/netfiles/test-zn.aut new file mode 100644 index 0000000..973ef75 --- /dev/null +++ b/netfiles/test-zn.aut @@ -0,0 +1,38 @@ +# siec automatow z ZN, ale bez zmiennych calkowitych + +net { + + actions { m; n; p; q; w; }; + + automaton automacikB1 { + clocks { + x1; + }; + locations { + a { init; }; + b { inv x1 < 1; }; + }; + trans { + a -> b , m , , { }; + b -> b , q , , { }; + b -> a , n , , { }; + }; + }; + + automaton automacikB2 { + clocks { + x2; + }; + locations { + d; + c { init; }; + e { inv x2 < 6; }; + }; + trans { + c -> d , p , x2 > 5 , { }; + d -> e , m , , { x2; }; + e -> c , n , , { x2; }; + }; + }; + +}; diff --git a/netfiles/test-zn2.aut b/netfiles/test-zn2.aut new file mode 100644 index 0000000..c27aea4 --- /dev/null +++ b/netfiles/test-zn2.aut @@ -0,0 +1,50 @@ +# siec automatow z ZN, ale bez zmiennych calkowitych + +net { + + actions { m; n; p; q; w; }; + + automaton automacikB1 { + clocks { + x1; + }; + locations { + a { init; }; + b { inv x1 < 1; }; + }; + trans { + a -> b , m , , { x1; }; + b -> b , q , , { }; + b -> a , n , , { }; + }; + }; + + automaton automacikC32 { + clocks { x3; }; + locations { + A { init; }; + B; + }; + trans { + A -> B , w , , { }; + B -> A , w , , { }; + }; + }; + + automaton automacikB2 { + clocks { + x2; + }; + locations { + d; + c { init; }; + e { inv x2 < 3; }; + }; + trans { + c -> d , p , x2 > 5 , { }; + d -> e , m , , { x2; }; + e -> c , n , , { x2; }; + }; + }; + +}; diff --git a/netfiles/test-zn_noConstr.aut b/netfiles/test-zn_noConstr.aut new file mode 100644 index 0000000..7ce0252 --- /dev/null +++ b/netfiles/test-zn_noConstr.aut @@ -0,0 +1,36 @@ +# siec automatow z ZN, ale bez zmiennych calkowitych + +net { + + actions { m; n; p; q; w; }; + + automaton automacikB1 { + clocks { + }; + locations { + a { init; }; + b; + }; + trans { + a -> b , m , , { }; + b -> b , q , , { }; + b -> a , n , , { }; + }; + }; + + automaton automacikB2 { + clocks { + }; + locations { + d; + c { init; }; + e; + }; + trans { + c -> d , p , , { }; + d -> e , m , , { }; + e -> c , n , , { }; + }; + }; + +}; diff --git a/netfiles/test2.aut b/netfiles/test2.aut new file mode 100644 index 0000000..c3299cb --- /dev/null +++ b/netfiles/test2.aut @@ -0,0 +1,83 @@ +### +## Plik z testowa siecia z jednym automatem. +### + +net { + + automaton pierwszy1 { + + clocks { + x; y; z; + }; + + locations { + a1; + b2 { urgent; inv x > 5; }; + lokacyjka { init; }; + c3; + aa; + bb; + cc; + }; + actions { + reset { urgent; }; + open; + close; + bla; + ble; + blo; + ping; + }; + trans { + a1 -> aa, reset, y > 3, { x; }; + aa -> bb, open, z < 2 && y = 3, { x; }; + bb -> cc, close, x >= 4 && x-y > 5, { x; y; z; }; + aa -> aa, + bla, # akcja + y <= 6 && x >= 2 && x-y=5, # guard + { }; # co resetowac + aa -> aa, ble, y <= 5 && x >= 4 && x-y=5, { }; + aa -> aa, blo, y <= 3 && x >= 0 && x-y=5, { }; + aa -> aa, ping, y <= 2 && x >= 1 && x-y=5, { }; + }; + }; + + automaton drugi2 { + + clocks { + x; y; z; + }; + + locations { + a1; + b2 { urgent; inv x > 5; }; + lokacyjka; + c3; + aa { init; }; + bb; + cc; + }; + actions { + reset { urgent; }; + open; + close; + bla; + ble; + blo; + ping; + }; + trans { + a1 -> aa, reset, y > 3, { x; }; + aa -> bb, open, z < 2 && y = 3, { x; }; + bb -> cc, close, x >= 4 && x-y > 5, { x; y; z; }; + aa -> aa, + bla, # akcja + y <= 6 && x >= 2 && x-y=5, # guard + { }; # co resetowac + aa -> aa, ble, y <= 5 && x >= 4 && x-y=5, { }; + aa -> aa, blo, y <= 3 && x >= 0 && x-y=5, { }; + aa -> aa, ping, y <= 2 && x >= 1 && x-y=5, { }; + }; + }; + +}; diff --git a/netfiles/tgc-dummyClocks.aut b/netfiles/tgc-dummyClocks.aut new file mode 100644 index 0000000..f3eb00e --- /dev/null +++ b/netfiles/tgc-dummyClocks.aut @@ -0,0 +1,92 @@ +# Train-Gate-Controller + +net { + + actions { + approach; + in; + out; + exit; + lower; + down; + raise; + up; + }; + + automaton Train { + clocks { + x1; + }; + locations { + t0 { init; }; + t1 { inv x1 <= 500; }; + t2 { inv x1 <= 500; }; + t3 { inv x1 <= 500; }; + }; + trans { + t0 -> t1, approach, , { x1; }; + t1 -> t2, in, x1 >= 300, { }; + t2 -> t3, out, , { }; + t3 -> t0, exit, x1 <= 500, { }; + }; + }; + + automaton Gate { + clocks { + x2; + }; + locations { + g0 { init; }; + g1 { inv x2 <= 100; }; + g2; + g3 { inv x2 <= 200; }; + }; + trans { + g0 -> g1, lower, , { x2; }; + g1 -> g2, down, x2 <= 100, { }; + g2 -> g3, raise, , { x2; }; + g3 -> g0, up, x2 >= 100 && x2 <= 200, { }; + }; + }; + + automaton Controller { + clocks { + x3; + a;b;c;d;e;f;g;h;i;j;k;l;m;n;o;p;q;r;s;t;u;v;w;x;y;z; # atrapy do testowania wydajnosci + a1;b1;c1;d1;e1;f1;g1;h1;i1;j1;k1;l1;m1; + n1;o1;p1;q1;r1;s1;t1;u1;v1;w1;x1;y1;z1; + }; + locations { + c0 { init; }; + c1 { inv x3 <= 100; }; + c2; + c3 { inv x3 <= 100; }; + }; + trans { + c0 -> c1, approach, , { x3; }; + c1 -> c2, lower, x3 = 100, { }; + c2 -> c3, exit, , { x3; }; + c3 -> c0, raise, x3 <= 100, { }; + }; + }; + + automaton specification { + clocks { + x9; + }; + locations { + s0 { init; }; + s1; + sErr; + }; + trans { + s0 -> s0, up, , { }; + s0 -> s1, down, , { x9; }; + s1 -> sErr, up, x9 > 700, { }; + s1 -> s0, up, x9 <= 700, { }; + s1 -> s1, down, x9 <= 700, { }; + + }; + }; + +}; diff --git a/netfiles/tgc.aut b/netfiles/tgc.aut new file mode 100644 index 0000000..42372a1 --- /dev/null +++ b/netfiles/tgc.aut @@ -0,0 +1,92 @@ +# Train-Gate-Controller + +net { + + actions { + approach; + in; + out; + exit; + lower; + down; + raise; + up; + }; + + automaton Train { + clocks { + x1; + }; + locations { + t0 { init; }; + t1 { inv x1 <= 500; }; + t2 { inv x1 <= 500; }; + t3 { inv x1 <= 500; }; + }; + trans { + t0 -> t1, approach, , { x1; }; + t1 -> t2, in, x1 >= 300, { }; + t2 -> t3, out, , { }; + t3 -> t0, exit, x1 <= 500, { }; + }; + }; + + automaton Gate { + clocks { + x2; + }; + locations { + g0 { init; }; + g1 { inv x2 <= 100; }; + g2; + g3 { inv x2 <= 200; }; + }; + trans { + g0 -> g1, lower, , { x2; }; + g1 -> g2, down, x2 <= 100, { }; + g2 -> g3, raise, , { x2; }; + g3 -> g0, up, x2 >= 100 && x2 <= 200, { }; + }; + }; + + automaton Controller { + clocks { + x3; + #a;b;c;d;e;f;g;h;i;j;k;l;m;n;o;p;q;r;s;t;u;v;w;x;y;z; # atrapy do testowania DBM-ow + #a1;b1;c1;d1;e1;f1;g1;h1;i1;j1;k1;l1;m1; + #n1;o1;p1;q1;r1;s1;t1;u1;v1;w1;x1;y1;z1; + }; + locations { + c0 { init; }; + c1 { inv x3 <= 100; }; + c2; + c3 { inv x3 <= 100; }; + }; + trans { + c0 -> c1, approach, , { x3; }; + c1 -> c2, lower, x3 = 100, { }; + c2 -> c3, exit, , { x3; }; + c3 -> c0, raise, x3 <= 100, { }; + }; + }; + + automaton specification { + clocks { + x9; + }; + locations { + s0 { init; }; + s1; + sErr; + }; + trans { + s0 -> s0, up, , { }; + s0 -> s1, down, , { x9; }; + s1 -> sErr, up, x9 > 700, { }; + s1 -> s0, up, x9 <= 700, { }; + s1 -> s1, down, x9 <= 700, { }; + + }; + }; + +}; diff --git a/test.sh b/test.sh new file mode 100644 index 0000000..35d6a61 --- /dev/null +++ b/test.sh @@ -0,0 +1,8 @@ +#!/bin/sh + +if [ "$1" != "n" ];then + make clean all +fi + +time ./verifier < netfiles/tgc.aut + diff --git a/verifier.l b/verifier.l new file mode 100644 index 0000000..aee5532 --- /dev/null +++ b/verifier.l @@ -0,0 +1,37 @@ +%{ +#include +#include +#include "y.tab.h" +%} + +%% +\#.* ; +net return NETTOK; +automaton return AUTOMATONTOK; +locations return LOCATIONSTOK; +actions return ACTIONSTOK; +clocks return CLOCKSTOK; +trans return TRANSTOK; +init return INITIALTOK; +commited return COMMITEDTOK; +urgent return URGENTTOK; +inv return INVTOK; +reach return REACHTOK; +[0-9]+ yylval.number=atoi(yytext); return CONSTANT; +[a-zA-Z_][a-zA-Z0-9_]* yylval.string=strdup(yytext); return WORD; +\{ return OBRACETOK; +\} return EBRACETOK; +; return SEMICOLON; +, return COLON; +-> return RARRTOK; +\&\& return CONJUNCTION; +\<= return REL_LE; +\< return REL_LT; +\>= return REL_GE; +\> return REL_GT; +- return OP_DIFF; += return REL_EQ; +@ return ATTOK; +\n ; +[ \t]+ ; +%% diff --git a/verifier.y b/verifier.y new file mode 100644 index 0000000..e95d458 --- /dev/null +++ b/verifier.y @@ -0,0 +1,278 @@ +%{ +#include +#include +#include +#include "anread.h" +#include "antypes.h" +#include "anmacro.h" +#include "anproc.h" +#include "anpsmod.h" + +/*#define Y_VERBOSE*/ + +void yyerror(const char *str) +{ + fprintf(stderr, "error: %s\n", str); +} + +int yywrap() +{ + return 1; +} + +int main(void) +{ + AutNet an; + + printf("TA Verifier\n\n"); + yyparse(); + + an = get_autnet(); + + if (an.naut > 0) { + // prod_show(&an); + psmodel_builder(&an); + } else { + printf("Empty network!"); + } + + printf("\nDONE\n"); + return 0; +} + +%} + + +%start fileElements + +%token NETTOK AUTOMATONTOK LOCATIONSTOK ACTIONSTOK CLOCKSTOK TRANSTOK OBRACETOK REACHTOK +%token EBRACETOK SEMICOLON COLON ATTOK INITIALTOK INVTOK COMMITEDTOK URGENTTOK +%token RARRTOK CONJUNCTION CONSTANT +%token REL_LE REL_LT REL_GE REL_GT REL_EQ OP_DIFF + +%union { + int number; + char *string; +} + +%token WORD +%type clock +%type CONSTANT + +%left CONJUNCTION + +%% + +fileElements: + | fileElements fileElement + ; + +fileElement: + NETTOK OBRACETOK netElements EBRACETOK SEMICOLON { + complete_net(); + } + | REACHTOK OBRACETOK prodConfigurations EBRACETOK SEMICOLON + ; + +netElements: + | netElements netElement SEMICOLON + ; + +netElement: + | ACTIONSTOK OBRACETOK actions EBRACETOK { + actions_mkmap(); + } + | AUTOMATONTOK WORD OBRACETOK automatonElements EBRACETOK { + complete_automaton($2); + } + ; + +automatonElements: + | automatonElements automatonElement SEMICOLON + ; + +automatonElement: + CLOCKSTOK OBRACETOK clocks EBRACETOK { + clocks_mkmap(); + } + | LOCATIONSTOK OBRACETOK locations EBRACETOK { + locations_mkmap(); + } + | TRANSTOK OBRACETOK transitions EBRACETOK + ; + +clocks: + | clocks clock SEMICOLON { + clocks_append($2); + } + ; + +clock: + WORD { + $$=$1; + } + ; + +locations: + | locations location SEMICOLON + ; + +location: + WORD OBRACETOK locationParams EBRACETOK { /* lokacja z parametrami */ + locations_append($1); + } + | WORD { /* lokacja bez parametrow */ + locations_append($1); + } + ; + +locationParams: + | locationParams locationParam SEMICOLON + ; + +locationParam: + INITIALTOK { + set_loc_type(LOC_INITIAL); + } + | URGENTTOK { + set_loc_type(LOC_URGENT); + } + | COMMITEDTOK { + set_loc_type(LOC_COMMITED); + } + | INVTOK clockConstr + ; + +actions: + | actions action SEMICOLON + ; + +action: + WORD OBRACETOK actionParams EBRACETOK { + actions_append($1); + } + | WORD { + actions_append($1); + } + ; + +actionParams: + | actionParams actionParam SEMICOLON + ; + +actionParam: + URGENTTOK { + set_act_type(ACT_URGENT); + } + ; + +prodConfigurations: + | prodConfigurations prodConfiguration SEMICOLON + ; + +prodConfiguration: + WORD OBRACETOK prodConfigurationElements EBRACETOK { + property_got_one($1); + } + ; + +prodConfigurationElements: + | prodConfigurationElements prodConfigurationElement + ; + +prodConfigurationElement: + WORD ATTOK WORD { + property_append_loc($1, $3); /* pamietac o zwolnieniu pamieci $1 i $3 */ + } + ; + +/* TODO: sprawdzic czy ograniczenia sa wlasciwie wprowadzane */ +clockConstr: + | clock REL_LE CONSTANT { +#ifdef Y_VERBOSE + printf("%s <= %d --normalisation--> %s - 0 <= %d\n", $1, $3, $1, $3); +#endif + constr_append(get_cur_clock_idx($1), 0, CONSTR_LE, $3); + free($1); /* tylko $1 jest stringiem */ + } + | clock REL_LT CONSTANT { +#ifdef Y_VERBOSE + printf("%s < %d --normalisation--> %s - 0 < %d\n", $1, $3, $1, $3); +#endif + constr_append(get_cur_clock_idx($1), 0, CONSTR_LT, $3); + free($1); + } + | clock REL_GE CONSTANT { +#ifdef Y_VERBOSE + printf("%s >= %d --normalisation--> 0 - %s <= -%d\n", $1, $3, $1, $3); +#endif + constr_append(0, get_cur_clock_idx($1), CONSTR_LE, -$3); + free($1); + } + | clock REL_GT CONSTANT { +#ifdef Y_VERBOSE + printf("%s > %d --normalisation--> 0 - %s < -%d\n", $1, $3, $1, $3); +#endif + constr_append(0, get_cur_clock_idx($1), CONSTR_LT, -$3); + free($1); + } + | clock REL_EQ CONSTANT { +#ifdef Y_VERBOSE + printf("%s = %d --normalisation--> %s - 0 <= %d && 0 - %s <= -%d\n", $1, $3, $1, $3, $1, $3); +#endif + constr_append(get_cur_clock_idx($1), 0, CONSTR_LE, $3); + constr_append(0, get_cur_clock_idx($1), CONSTR_LE, -$3); + free($1); + } + | clock OP_DIFF clock REL_LE CONSTANT { +#ifdef Y_VERBOSE + printf("%s - %s <= %d --normalised--\n", $1, $3, $5); +#endif + constr_append(get_cur_clock_idx($1), get_cur_clock_idx($3), CONSTR_LE, $5); + free($1); free($3); + } + | clock OP_DIFF clock REL_LT CONSTANT { +#ifdef Y_VERBOSE + printf("%s - %s < %d --normalised--\n", $1, $3, $5); +#endif + constr_append(get_cur_clock_idx($1), get_cur_clock_idx($3), CONSTR_LT, $5); + free($1); free($3); + } + | clock OP_DIFF clock REL_GE CONSTANT { +#ifdef Y_VERBOSE + printf("%s - %s >= %d --normalisation--> %s - %s <= -%d\n", $1, $3, $5, $3, $1, $5); +#endif + constr_append(get_cur_clock_idx($1), get_cur_clock_idx($3), CONSTR_LE, -$5); + free($1); free($3); + } + | clock OP_DIFF clock REL_GT CONSTANT { +#ifdef Y_VERBOSE + printf("%s - %s > %d --normalisation--> %s - %s < -%d\n", $1, $3, $5, $3, $1, $5); +#endif + constr_append(get_cur_clock_idx($1), get_cur_clock_idx($3), CONSTR_LT, -$5); + free($1); free($3); + } + | clock OP_DIFF clock REL_EQ CONSTANT { +#ifdef Y_VERBOSE + printf("%s - %s = %d --normalisation--> %s - %s <= %d && %s - %s <= -%d\n", $1, $3, $5, $1, $3, $5, $3, $1, $5); +#endif + constr_append(get_cur_clock_idx($1), get_cur_clock_idx($3), CONSTR_LE, $5); + constr_append(get_cur_clock_idx($3), get_cur_clock_idx($1), CONSTR_LE, -$5); + free($1); free($3); + } + | clockConstr CONJUNCTION clockConstr + ; + +transitions: + | transitions transition SEMICOLON + ; + +transition: + WORD RARRTOK WORD COLON WORD COLON clockConstr COLON OBRACETOK clocks EBRACETOK { + trans_append(get_cur_loc_idx($1), get_cur_loc_idx($3), get_cur_act_idx($5)); + free($1); free($3); free($5); + } + ; + +%% +