diff --git a/Resources/example - zeroconf abstract.xml b/Resources/example - zeroconf abstract.xml
new file mode 100644
index 0000000..5854985
--- /dev/null
+++ b/Resources/example - zeroconf abstract.xml
@@ -0,0 +1,202 @@
+//
+// CONSTANTS FROM RFC 3927 www.ietf.org/rfc/rfc3927.txt
+//
+// The following 10 constant declarations are copied almost verbatim from Section 9
+// "The following timing constants are used in this protocol; they are
+// not intended to be user configurable."
+
+const int PROBE_WAIT = 1; // second (initial random delay)
+const int PROBE_NUM = 3; // (number of probe packets)
+const int PROBE_MIN = 1; // second (minimum delay till repeated probe)
+const int PROBE_MAX = 2; // seconds (maximum delay till repeated probe)
+const int ANNOUNCE_WAIT = 2; // seconds (delay before announcing)
+const int ANNOUNCE_NUM = 2; // (number of announcement packets)
+const int ANNOUNCE_INTERVAL = 2; // seconds (time between announcement packets)
+const int MAX_CONFLICTS = 10; // (max conflicts before rate limiting)
+const int RATE_LIMIT_INTERVAL = 60; // second (delay between successive attempts)
+const int DEFEND_INTERVAL = 10; // seconds (minimum interval between defensive ARPs).
+
+//The following constants specify the dimensioning of the model
+const int l =3;//=9; // number of hardware addresses (including all zeroes address)
+const int m =4;//=15; // number of available link local IP addresses
+ //real value is 65024 but simulator can't handle that
+//const int n =2; // number of network automata
+
+typedef int[0,1] BOOL;
+typedef scalar[l] HAtype;
+HAtype nil;
+typedef scalar[m+1] IPtype; //an IP address in our model is either a link local address or the zero address
+IPtype zero;
+
+meta HAtype ha0;
+
+IPtype IP[HAtype]; // array recording (guessed) IP address for each host, zero means no address guessed
+bool UseIP[HAtype]; // array recording whether host is using an IP address
+
+// channels to send messages to network, reset a host, receive messages from network, and to send answers back to network
+chan send_req[HAtype],reset[HAtype],receive_msg[HAtype][HAtype],send_answer[HAtype];
+
+// trick to make certain transitions urgent
+urgent broadcast chan urg;
+
+typedef struct{
+ HAtype senderHA; // sender hardware address
+ IPtype senderIP; // sender IP address
+ IPtype targetIP; // target IP address
+ bool request; // is the packet a Request or a Reply
+}ARP_packet;
+
+void initialize(ARP_packet& p)
+{
+ p.senderHA := nil;
+ p.senderIP := zero;
+ p.targetIP := zero;
+ p.request := false;
+}
+
+//meta because it is used only for value passing in synchronizations
+meta ARP_packet packet;
+
+bool isConcreteHA[HAtype];Networkconst HAtype wclock z;
+bool send[HAtype];
+bool answer[HAtype];
+
+ARP_packet s_buffer;
+ARP_packet a_buffer;
+
+void set(bool& a[HAtype], bool b)
+{
+ for(i:HAtype) { if(isConcreteHA[i]) a[i]:=b; }
+}
+
+void handle_answer() {
+ if (isConcreteHA[packet.senderHA])
+ {a_buffer:=packet; set(answer,true); }
+}
+
+
+BUSYIDLEInitializer/*void assign_addresses()
+{
+ int c;
+ for(j:PIDtype) {
+ if(c<2) {
+ isConcretePID[j]:=true;
+ c++;
+ }
+ }
+
+ for (i:PIDtype) {
+ for (j:HAtype) {
+ if(j!=nil && isConcretePID[i] && not exists (k:PIDtype) HA[k]==j) {HA[i]:=j;}
+ }
+ }
+}*/Configconst HAtype hclock x;
+
+int [0,PROBE_NUM] counter; //number of probes or gratuitous ARP that have been sent
+//int [0,MAX_CONFLICTS] ConflictNum; //the number of times an address collision has occurred
+
+PRE_CLAIMWAITPROBEINITCLAIMEDChaosInputHandlerconst HAtype hclock y;
+ARP_packet answer;
+HAtype network;
+bool do_reset;
+
+void ihandler(bool defend)
+{
+ if (IP[h]==zero) // Scenario A: I have not selected an IP address
+ ;
+ else if (packet.senderHA==h) // Scenario B: I have sent the packet myself
+ ;
+ else if (packet.senderIP==IP[h]) //There is a conflict: somebody else is using my address!
+ {
+ if (not UseIP[h]) // Scenario C: select a new address
+ do_reset:=true;
+ else if (defend) // Scenario D: I am going to defend my address
+ {
+ answer.senderHA:=h;
+ answer.senderIP:=IP[h];
+ answer.targetIP:=IP[h];
+ answer.request:=true;
+ }
+ else // Scenario E: I will not defend my address
+ do_reset:=true;
+ }
+ else if (not UseIP[h])
+ {
+ if (packet.targetIP==IP[h] && packet.request && packet.senderIP==zero) // Scenario F: conflicting probe
+ do_reset:=true;
+ else //Scenario G: Packet is not conflicting with IP address that I want to use
+ ;
+ }
+ else // Packet is not conflicting with IP address that I am using
+ {
+ if (packet.targetIP==IP[h] && packet.request) // Scenario H: answer regular ARP request
+ {
+ answer.senderHA:=h;
+ answer.senderIP:=IP[h];
+ answer.targetIP:=packet.senderIP;
+ answer.request:=false;
+ }
+ else // Scenario I: no reply message required
+ ;
+ }
+}
+BUSYIDLEsystem Config, InputHandler,Network,Initializer,Chaos;
\ No newline at end of file
diff --git a/Resources/example - zeroconf full.xml b/Resources/example - zeroconf full.xml
new file mode 100644
index 0000000..4d52a55
--- /dev/null
+++ b/Resources/example - zeroconf full.xml
@@ -0,0 +1,207 @@
+//
+// CONSTANTS FROM RFC 3927 www.ietf.org/rfc/rfc3927.txt
+//
+// The following 10 constant declarations are copied almost verbatim from Section 9
+// "The following timing constants are used in this protocol; they are
+// not intended to be user configurable."
+const int PROBE_WAIT = 1; // second (initial random delay)
+const int PROBE_NUM = 3; // (number of probe packets)
+const int PROBE_MIN = 1; // second (minimum delay till repeated probe)
+const int PROBE_MAX = 2; // seconds (maximum delay till repeated probe)
+const int ANNOUNCE_WAIT = 2; // seconds (delay before announcing)
+const int ANNOUNCE_NUM = 2; // (number of announcement packets)
+const int ANNOUNCE_INTERVAL = 2; // seconds (time between announcement packets)
+const int MAX_CONFLICTS = 10; // (max conflicts before rate limiting)
+const int RATE_LIMIT_INTERVAL = 60; // second (delay between successive attempts)
+const int DEFEND_INTERVAL = 10; // seconds (minimum interval between defensive ARPs).
+
+//The following constants specify the dimensions of the model
+const int l = 2; // number of hardware addresses (including all zeroes address)
+
+const int m = 2; // number of available link local IP addresses
+ //real value is 65024 but simulator can't handle that
+const int n = 3; // number of network automata
+
+typedef scalar[l] HAtype;
+typedef scalar[m+1] IPtype; //an IP address in our model is either a link local address or the zero address
+IPtype zero;
+typedef scalar[n] Networktype;
+
+IPtype IP[HAtype]; // array recording (guessed) IP address for each host, zero means no address guessed
+bool UseIP[HAtype]; // array recording whether host is using an IP address
+
+// channels to send messages to network, reset a host, receive messages from network, and to send answers back to network
+chan send_req,reset[HAtype],receive_msg[Networktype][HAtype],send_answer[Networktype];
+
+// trick to make certain transitions urgent
+urgent broadcast chan urg;
+
+typedef struct{
+ HAtype senderHA; // sender hardware address
+ IPtype senderIP; // sender IP address
+ IPtype targetIP; // target IP address
+ bool request; // is the packet a Request or a Reply
+}ARP_packet;
+
+meta HAtype ha0;
+void initialize(ARP_packet& p)
+{
+ p.senderHA := ha0;
+ p.senderIP := zero;
+ p.targetIP := zero;
+ p.request := false;
+}
+
+//meta because it is used only for value passing in synchronizations
+meta ARP_packet packet;
+Configconst HAtype hclock x;
+
+int [0,PROBE_NUM] counter; //number of probes or gratuitous ARP that have been sent
+int [0,MAX_CONFLICTS] ConflictNum; //the number of times an address collision has occurredPRE_CLAIMWAITCOLLISIONPROBEINITCLAIMEDRegularconst HAtype hINITInputHandlerconst HAtype hclock y;
+ARP_packet answer;
+Networktype network;
+bool do_reset;
+
+void ihandler(bool defend)
+{
+ if (IP[h]==zero) // Scenario A: I have not selected an IP address
+ ;
+ else if (packet.senderHA==h) // Scenario B: I have sent the packet myself
+ ;
+ else if (packet.senderIP==IP[h]) //There is a conflict: somebody else is using my address!
+ {
+ if (not UseIP[h]) // Scenario C: select a new address
+ do_reset:=true;
+ else if (defend) // Scenario D: I am going to defend my address
+ {
+ answer.senderHA:=h;
+ answer.senderIP:=IP[h];
+ answer.targetIP:=IP[h];
+ answer.request:=true;
+ y:=0;
+ }
+ else // Scenario E: I will not defend my address
+ do_reset:=true;
+ }
+ else if (not UseIP[h])
+ {
+ if (packet.targetIP==IP[h] && packet.request && packet.senderIP==zero) // Scenario F: conflicting probe
+ do_reset:=true;
+ else //Scenario G: Packet is not conflicting with IP address that I want to use
+ ;
+ }
+ else // Packet is not conflicting with IP address that I am using
+ {
+ if (packet.targetIP==IP[h] && packet.request) // Scenario H: answer regular ARP request
+ {
+ answer.senderHA:=h;
+ answer.senderIP:=IP[h];
+ answer.targetIP:=packet.senderIP;
+ answer.request:=false;
+ }
+ else // Scenario I: no reply message required
+ ;
+ }
+}
+BUSYINITIDLENetworkconst Networktype wclock z;
+bool send[HAtype];
+bool answer[HAtype];
+
+ARP_packet s_buffer;
+ARP_packet a_buffer;
+
+void set(bool& a[HAtype]) {
+ for(i:HAtype){a[i]:=true;}
+}
+
+
+BUSYIDLEsystem Config, InputHandler,Regular,Network;
\ No newline at end of file
diff --git a/Resources/introduction to uppaal.pdf b/Resources/introduction to uppaal.pdf
new file mode 100644
index 0000000..6937383
Binary files /dev/null and b/Resources/introduction to uppaal.pdf differ
diff --git a/Resources/rfc793.pdf b/Resources/rfc793.pdf
new file mode 100644
index 0000000..917aa29
Binary files /dev/null and b/Resources/rfc793.pdf differ