From 6a17587378bab70f5fb77201d7c6b7a095c12e30 Mon Sep 17 00:00:00 2001 From: Artur Meski Date: Fri, 22 Feb 2019 17:33:33 +0000 Subject: [PATCH] Initial commit --- Makefile | 45 + TODO | 25 + anmacro.h | 34 + anproc.c | 892 +++++++++++++++++++ anproc.h | 49 ++ anpsmod.c | 824 ++++++++++++++++++ anpsmod.h | 34 + anread.c | 862 ++++++++++++++++++ anread.h | 52 ++ antclass.c | 755 ++++++++++++++++ antclass.h | 54 ++ antypes.h | 212 +++++ dbm.c | 1348 +++++++++++++++++++++++++++++ dbm.h | 76 ++ dbm_macro.h | 82 ++ dbm_testing.c | 475 ++++++++++ macro.h | 31 + netfiles/fischer-fail.aut | 92 ++ netfiles/fischer-orig.aut | 87 ++ netfiles/fischer.aut | 88 ++ netfiles/fischer10p.aut | 416 +++++++++ netfiles/fischer3p-fail.aut | 121 +++ netfiles/fischer3p.aut | 121 +++ netfiles/fischer4p-fail.aut | 167 ++++ netfiles/fischer4p.aut | 158 ++++ netfiles/fischer5p-fail.aut | 209 +++++ netfiles/fischer5p.aut | 196 +++++ netfiles/fischer6p-fail.aut | 253 ++++++ netfiles/fischer6p.aut | 235 +++++ netfiles/fischer7p-fail.aut | 301 +++++++ netfiles/fischer7p.aut | 301 +++++++ netfiles/fischer8p.aut | 354 ++++++++ netfiles/test-empty.ta | 1 + netfiles/test-zn-clockconstrs.aut | 39 + netfiles/test-zn.aut | 38 + netfiles/test-zn2.aut | 50 ++ netfiles/test-zn_noConstr.aut | 36 + netfiles/test2.aut | 83 ++ netfiles/tgc-dummyClocks.aut | 92 ++ netfiles/tgc.aut | 92 ++ test.sh | 8 + verifier.l | 37 + verifier.y | 278 ++++++ 43 files changed, 9703 insertions(+) create mode 100644 Makefile create mode 100644 TODO create mode 100644 anmacro.h create mode 100644 anproc.c create mode 100644 anproc.h create mode 100644 anpsmod.c create mode 100644 anpsmod.h create mode 100644 anread.c create mode 100644 anread.h create mode 100644 antclass.c create mode 100644 antclass.h create mode 100644 antypes.h create mode 100644 dbm.c create mode 100644 dbm.h create mode 100644 dbm_macro.h create mode 100644 dbm_testing.c create mode 100644 macro.h create mode 100644 netfiles/fischer-fail.aut create mode 100644 netfiles/fischer-orig.aut create mode 100644 netfiles/fischer.aut create mode 100644 netfiles/fischer10p.aut create mode 100644 netfiles/fischer3p-fail.aut create mode 100644 netfiles/fischer3p.aut create mode 100644 netfiles/fischer4p-fail.aut create mode 100644 netfiles/fischer4p.aut create mode 100644 netfiles/fischer5p-fail.aut create mode 100644 netfiles/fischer5p.aut create mode 100644 netfiles/fischer6p-fail.aut create mode 100644 netfiles/fischer6p.aut create mode 100644 netfiles/fischer7p-fail.aut create mode 100644 netfiles/fischer7p.aut create mode 100644 netfiles/fischer8p.aut create mode 100644 netfiles/test-empty.ta create mode 100644 netfiles/test-zn-clockconstrs.aut create mode 100644 netfiles/test-zn.aut create mode 100644 netfiles/test-zn2.aut create mode 100644 netfiles/test-zn_noConstr.aut create mode 100644 netfiles/test2.aut create mode 100644 netfiles/tgc-dummyClocks.aut create mode 100644 netfiles/tgc.aut create mode 100644 test.sh create mode 100644 verifier.l create mode 100644 verifier.y 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); + } + ; + +%% +