Initial commit

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
+

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.
+

anmacro.h

@@ -0,0 +1,34 @@
+#ifndef _INC_ANMACRO_H_
+#define _INC_ANMACRO_H_
+
+#include <stdio.h>
+#include <stdlib.h>
+#include <string.h>
+
+#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_ */

anproc.c

@@ -0,0 +1,892 @@
+/** anproc.c **/
+
+/*
+ * Przetwarzanie struktur stworzonych podczas wczytywania sieci automatow,
+ * tworzenie produktu na podstawie sieci automatow.
+ */
+
+#include <stdio.h>
+#include <stdlib.h>
+#include <assert.h>
+#include <stdbool.h>
+#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);
+	
+}
+

anproc.h

@@ -0,0 +1,49 @@
+#ifndef _INC_ANPROC_H_
+#define _INC_ANPROC_H_
+
+#include <limits.h>
+#include <stdbool.h>
+#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_ */

anpsmod.c

@@ -0,0 +1,824 @@
+/** anpsmod.c **/
+
+/*
+ * Tutaj jest splitting. Zaczyna sie od psmodel_builder.
+ */
+
+#include <stdio.h>
+#include <stdlib.h>
+#include <stdbool.h>
+#include <assert.h>
+#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;
+}

anpsmod.h

@@ -0,0 +1,34 @@
+#ifndef _INC_ANPSMOD_H_
+#define _INC_ANPSMOD_H_
+
+#include <stdbool.h>
+#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_ */

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 <stdio.h>
+#include <string.h>
+#include <stdlib.h>
+#include <stdbool.h>
+#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;
+}
+

anread.h

@@ -0,0 +1,52 @@
+#ifndef _INC_ANREAD_H_
+#define _INC_ANREAD_H_
+
+#include "antypes.h"
+#include <stdbool.h>
+
+// #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_*/

antclass.c

@@ -0,0 +1,755 @@
+/** antclass.c **/
+
+/*
+ * Manipulacje klasami abstrakcyjnymi, tworzenie nowych,
+ * modyfikowanie ich parametrow, sprawdzanie, etc.
+ */
+
+#include <stdio.h>
+#include <stdlib.h>
+#include <stdbool.h>
+#include <assert.h>
+#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;
+}

antclass.h

@@ -0,0 +1,54 @@
+#ifndef _INC_ANTCLASS_H_
+#define _INC_ANTCLASS_H_
+
+#include <limits.h>
+#include <stdbool.h>
+#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_ */

antypes.h

@@ -0,0 +1,212 @@
+#ifndef _INC_ANTYPES_H_
+#define _INC_ANTYPES_H_
+
+#include <stdbool.h>
+#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_ */
+

dbm.h

@@ -0,0 +1,76 @@
+#ifndef _INC_DBM_H_
+#define _INC_DBM_H_
+
+#include <stdlib.h>
+#include <stdbool.h> /* troche elegancji ;-) */
+#include <assert.h>
+/* 
+ * 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_ */

dbm_macro.h

@@ -0,0 +1,82 @@
+#ifndef _INC_DBM_MACRO_H_
+#define _INC_DBM_MACRO_H_
+
+#include <limits.h>
+
+/* 
+ * 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_ */

dbm_testing.c

@@ -0,0 +1,475 @@
+#include <stdio.h>
+#include <stdlib.h>
+#include <limits.h>
+#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;
+}
+

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_ */

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 };
+};

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, , { };
+		};
+	};
+
+};

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, , { };
+		
+		};
+	};
+
+};

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, , { };
+			
+		};
+	};
+
+};

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 };
+};

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 };
+};

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 };
+};

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, , { };
+			
+		};
+	};
+
+};

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 };
+};

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, , { };
+			
+		};
+	};
+
+};

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 };
+};

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, , { };			
+		};
+	};
+
+};

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 };
+};

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 };
+};

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 };
+};

netfiles/test-empty.ta

@@ -0,0 +1 @@
+net { };

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; };
+		};
+	};
+		
+};

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; };
+		};
+	};
+		
+};

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; };
+		};
+	};
+	
+};

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 , , { };
+		};
+	};
+		
+};

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, { };
+		};
+	};
+	
+};

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, { };
+
+		};
+	};
+	
+};

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, { };
+
+		};
+	};
+	
+};

test.sh

@@ -0,0 +1,8 @@
+#!/bin/sh
+
+if [ "$1" != "n" ];then
+	make clean all
+fi
+
+time ./verifier < netfiles/tgc.aut
+	

verifier.l

@@ -0,0 +1,37 @@
+%{
+#include <stdio.h>
+#include <string.h>
+#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]+					;
+%%

verifier.y

@@ -0,0 +1,278 @@
+%{
+#include <stdio.h>
+#include <stdlib.h>
+#include <string.h>
+#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	<string>	WORD
+%type	<string>	clock
+%type	<number>	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);
+	}
+	;
+
+%%
+