diff --git a/CaseStudies/CSMA-CA-IWIGP2012/README.md b/CaseStudies/CSMA-CA-IWIGP2012/README.md
new file mode 100644
index 0000000..6840fa6
--- /dev/null
+++ b/CaseStudies/CSMA-CA-IWIGP2012/README.md
@@ -0,0 +1,21 @@
+# Computing Nash Equilibrium in Wireless Ad Hoc Networks: A Simulation-Based Approach
+
+_**Computing Nash Equilibrium in Wireless Ad Hoc Networks: A Simulation-Based Approach**_,
+Peter E. Bulychev, Alexandre David, Kim G. Larsen, Axel Legay, Marius Mikučionis. *2nd Internation Workshop on Interactions, Games and Protocols (IWIGP 2012)*, March 25, 2012, Electronic Proceedings in Theoretical Computer Science (EPTCS). [[DOI:10.4204/EPTCS.78.1](https://doi.org/10.4204/EPTCS.78.1)]
+
+## Abstract
+
+This paper studies the problem of computing Nash equilibrium in wireless networks modeled by
+Weighted Timed Automata. Such formalism comes together with a logic that can be used to describe
+complex features such as timed energy constraints. Our contribution is a method for solving this
+problem using Statistical Model Checking. The method has been implemented in UPPAAL model
+checker and has been applied to the analysis of Aloha CSMA/CD and IEEE 802.15.4 CSMA/CA
+protocols.
+
+## Model Files
+
+Uppaal SMC model of CSMA/CA protocol: [csma-ca.xml](csma-ca.xml)
+
+Image from the protocol model:
+
+
diff --git a/CaseStudies/CSMA-CA-IWIGP2012/csma-ca.svg b/CaseStudies/CSMA-CA-IWIGP2012/csma-ca.svg
new file mode 100644
index 0000000..19192ca
--- /dev/null
+++ b/CaseStudies/CSMA-CA-IWIGP2012/csma-ca.svg
@@ -0,0 +1,2559 @@
+
+
+
+
diff --git a/CaseStudies/CSMA-CA-IWIGP2012/csma-ca.svgz b/CaseStudies/CSMA-CA-IWIGP2012/csma-ca.svgz
new file mode 100644
index 0000000..42f9888
Binary files /dev/null and b/CaseStudies/CSMA-CA-IWIGP2012/csma-ca.svgz differ
diff --git a/CaseStudies/CSMA-CA-IWIGP2012/csma-ca.xml b/CaseStudies/CSMA-CA-IWIGP2012/csma-ca.xml
new file mode 100644
index 0000000..c724644
--- /dev/null
+++ b/CaseStudies/CSMA-CA-IWIGP2012/csma-ca.xml
@@ -0,0 +1,339 @@
+
+
+
+ /** This CSMA/CA model is described in the following publication:
+"Computing Nash Equilibrium in Wireless Ad Hoc Networks: A Simulation-Based Approach"
+by Peter E. Bulychev, Alexandre David, Kim G. Larsen, Axel Legay and Marius Mikučionis.
+2nd Internation Workshop on Interactions, Games and Protocols (IWIGP 2012),
+March 25, 2012, Electronic Proceedings in Theoretical Computer Science (EPTCS).
+DOI: https://doi.org/10.4204/EPTCS.78.1
+*/
+
+//const int N=10; // CORRECT
+const int N=6; // INCORRECT
+
+clock time;
+
+typedef int[0,N-1] id_t;
+
+broadcast chan ready;
+broadcast chan go;
+
+broadcast chan a;
+
+bool isTransmitting[N];
+
+const int macMaxCSMABackoffs = 4; // CORRECT
+//const int macMaxCSMABackoffs = 1; // INCORRECT
+
+// approved consts
+const int UnitBackoff = 20;
+const int CCA_duration = 8; // CORRECT
+const int aTurnaroundTime = 12; // CORRECT
+const int ACK_time = 88;
+const int aMaxFrameRetries = 3; // CORRECT
+
+const int macMinBE = 3; // CORRECT
+const int macMaxBE = 5; // CORRECT
+
+//const int macMinBE = 0; // INCORRECT
+//const int macMaxBE = 0; // INCORRECT
+
+//const int minDataLength = 15*8; // CORRECT
+//const int maxDataLength = 6*8; // CORRECT
+const int data_length = 35*8; // CORRECT 25*8 - is for header
+//const int data_length = maxDataLength;
+
+//const int data_length = 3; // INCORRECT
+//const int aTurnaroundTime = 2; // INCORRECT
+//const int CCA_duration = 10; // INCORRECT
+
+//const int max_waking_delay=6000; for sound speed is 300 m/s
+//const int max_waking_delay=10; //CORRECT for something else
+const int max_waking_delay=1000; //CORRECT for something else
+//const int max_waking_delay=aTurnaroundTime; //CORRECT to show that is_disrete_waiting qualitatively affects the model // exist
+//const int max_waking_delay=aTurnaroundTime + data_length + CCA_duration; //CORRECT to show that is_disrete_waiting qualitatively affects the model // forall
+
+const int aMinLIFSPeriod = 40; // CORRECT
+
+const bool is_discrete_waiting = false;
+const bool acknowledgment_supported = true;
+const bool recover_from_failures = false;
+
+const int wait_after_failure = 0;
+
+hybrid clock energy;
+int RX_Power, TX_Power;
+
+ Process
+ const id_t id
+
+int be;
+int nb;
+int nretries;
+
+int backoff;
+
+int waking_delay;
+
+clock x;
+
+bool cca_passed := false;
+bool collision_occured := false;
+
+bool is_busy() {
+ int i;
+ for(i=0; i<N; i++) {
+ if (isTransmitting[i])
+ return true;
+ }
+ return false;
+}
+
+void start_sending() {
+ isTransmitting[id] = true;
+}
+
+void finish_sending() {
+ isTransmitting[id] = false;
+}
+
+bool is_conflict() {
+ bool f = false;
+ int i;
+ for(i=0; i<N; i++) {
+ if (isTransmitting[i]) {
+ if (f)
+ return true;
+ else
+ f = true;
+ }
+ }
+ return false;
+}
+
+
+
+
+
+
+
+ FAILURE
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+ SUCCESS
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+ TRANSMIT_DATA
+
+
+
+ VULNERABLE
+
+
+
+ CCA
+
+
+
+ WAIT_BACKOFF
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+ // Place template instantiations here.
+
+system Process;
+
+
+
+
+
+
+
diff --git a/CaseStudies/README.md b/CaseStudies/README.md
index af89572..0ade7ee 100644
--- a/CaseStudies/README.md
+++ b/CaseStudies/README.md
@@ -1,6 +1,6 @@
# List of Case Studies
-_**[Randomized Reachability Analysis in Uppaal: Fast Error Detection in Timed Systems](RandomizedReachability2021)**_, Kiviriga A., Larsen K.G., Nyman U. (2021). In: Lluch Lafuente A., Mavridou A. (eds) Formal Methods for Industrial Critical Systems. FMICS 2021. Lecture Notes in Computer Science, vol 12863. Springer, Cham. [[DOI]](https://doi.org/10.1007/978-3-030-85248-1_9) [[Springer]](https://link.springer.com/chapter/10.1007/978-3-030-85248-1_9)
+_**[Randomized Reachability Analysis in Uppaal: Fast Error Detection in Timed Systems](RandomizedReachability2021)**_, Kiviriga A., Larsen K.G., Nyman U. (2021). In: Lluch Lafuente A., Mavridou A. (eds) Formal Methods for Industrial Critical Systems. FMICS 2021. Lecture Notes in Computer Science, vol 12863. Springer, Cham. [[DOI:10.1007/978-3-030-85248-1_9](https://doi.org/10.1007/978-3-030-85248-1_9)] [[Springer](https://link.springer.com/chapter/10.1007/978-3-030-85248-1_9)]
_**[Modeling and Analysis for Energy-Driven Computing using Statistical Model-Checking](EnergyNeutrality)**_,
Abdoulaye Gamatié, Gilles Sassatelli, Marius Mikučionis. *Design, Automation and Test in Europe (DATE 2021),* February 1, 2021.
@@ -9,11 +9,16 @@ _**[Fluid Model-Checking in UPPAAL for Covid-19](Covid-19)**_,
Peter G. Jensen, Kenneth Y. Jørgensen, Kim G. Larsen, Marius Mikučionis, Marco Muñiz, and Danny B. Poulsen. *Leveraging Applications of Formal Methods, Verification and Validation. Applications and Case Studies (ISoLA 2020),* October 2020. Springer-Verlag Berlin Heidelberg.
_**[Schedulability of Herschel-Planck Revisited Using Statistical Model Checking](HerschelPlanck2012)**_,
-Alexandre David, Kim G. Larsen, Axel Legay and Marius Mikučionis. *Leveraging Applications of Formal Methods, Verification and Validation. Applications and Case Studies (ISoLA 2012)*, October 2012, Springer-Verlag Berlin Heidelberg. ISBN 978-3-642-34032-1, 978-3-642-34031-4. [[DOI](https://doi.org/10.1007/978-3-642-34032-1_28)]
+Alexandre David, Kim G. Larsen, Axel Legay and Marius Mikučionis. *Leveraging Applications of Formal Methods, Verification and Validation. Applications and Case Studies (ISoLA 2012)*, October 2012, Springer-Verlag Berlin Heidelberg. ISBN 978-3-642-34032-1, 978-3-642-34031-4. [[DOI:10.1007/978-3-642-34032-1_28](https://doi.org/10.1007/978-3-642-34032-1_28)]
+_**[Rewrite-Based Statistical Model Checking of WMTL](CSMA-CA-RV2012)**_,
+Peter E. Bulychev, Alexandre David, Kim G. Larsen, Axel Legay, Guangyuan Li & Danny Bøgsted Poulsen. *Runtime Verification (RV 2012)*, 2012. Lecture Notes in Computer Science, Springer, Berlin, Heidelberg (LNCS). [[DOI:10.1007/978-3-642-35632-2_25](https://doi.org/10.1007/978-3-642-35632-2_25)]
+
+_**[Computing Nash Equilibrium in Wireless Ad Hoc Networks: A Simulation-Based Approach](CSMA-CA-IWIGP2012)**_,
+Peter E. Bulychev, Alexandre David, Kim G. Larsen, Axel Legay, Marius Mikučionis. *2nd Internation Workshop on Interactions, Games and Protocols (IWIGP 2012)*, March 25, 2012, Electronic Proceedings in Theoretical Computer Science (EPTCS). [[DOI:10.4204/EPTCS.78.1](https://doi.org/10.4204/EPTCS.78.1)]
_**[Schedulability Analysis of Herschel/Planck Software Using Uppaal](HerschelPlanck2011)**_
Marius Mikučionis, Kim G. Larsen and Brian Nielsen. Quasimodo Industrial Handbook, 2011.
_**[Schedulability Analysis Using Uppaal: Herschel-Planck Case Study](HerschelPlanck2010)**_
-Marius Mikučionis, Kim Guldstrand Larsen, Jacob Illum Rasmussen, Brian Nielsen, Arne Skou, Palm Steen Ulrik, Jan Storbank Pedersen, Poul Hougaard. _Proceedings of the 4th international conference on Leveraging applications of formal methods, verification, and validation (ISOLA 2010)_, October 2010, Springer-Verlag, ISBN 3-642-16560-5, 978-3-642-16560-3. [[DOI](https://doi.org/10.1007/978-3-642-16561-0_21)]
+Marius Mikučionis, Kim Guldstrand Larsen, Jacob Illum Rasmussen, Brian Nielsen, Arne Skou, Palm Steen Ulrik, Jan Storbank Pedersen, Poul Hougaard. _Proceedings of the 4th international conference on Leveraging applications of formal methods, verification, and validation (ISOLA 2010)_, October 2010, Springer-Verlag, ISBN 3-642-16560-5, 978-3-642-16560-3. [[DOI:10.1007/978-3-642-16561-0_21](https://doi.org/10.1007/978-3-642-16561-0_21)]