<commit_before># Description

[//]: # (Image References)

[image1]: doc/images/lt_ratio_speedup.png "Speedup analysis" 

Mercury is a high performance Model Checker developed for multicore, multiprocessors 
machine with shared memory. It is a state-of-the art Model Checking playground specially 
developed to experiment different approaches for  Parallel State Space construction  
(graph traversal)  and Parallel Model Checking of temporal formulas.

Mercury has been developed to be highly modular and extensible. The software is 
composed of separate, interchangeable modules that accept different memory layouts 
(shared/local data) and synchronization mechanisms.

Moreover, the software view of states is abstract and can be easily extended to 
take into account data structures and time classes. Altogether, we experimented 
several versions, two for probabilistic, four for exhaustive state space construction 
and three for parallel model checking (subset of CTL formulas).

For more information, check [Mercury's homepage](https://rodrigotaclasaad.wordpress.com/mercury/)

# Features:

1. Parallel State Space Exploration
   - Reachability analysis (see [ISPDC2011](https://rodrigotaclasaad.wordpress.com/2017/09/05/mixed-shared-distributed-hash-tables-approaches-for-parallel-state-space-construction/)
   - Local Sub-CTL Model Checking (see [ATVA2012](https://rodrigotaclasaad.wordpress.com/2017/09/05/an-experiment-on-parallel-model-checking-of-a-ctl-fragment/))
2. Probabilistic State Space Exploration
   - Reachability analysis
3. NEW: Disc based State Space Exploration (in ALFA, not stable)
   - Currently, supports only the state space exploration (prints the number of states and transitions);
   - The state space and the exploration stacks are partitioned on the hard disk;
   - Coming soon: Reachability analysis

# Benchmark (Speedup)

In Figure 1 we give the observed speedup of Mercury on a set of examples.  We give 
the absolute speedup, measured as the ratio between the execution time using **n** 
processors (**tn**) and the time of an optimized, sequential version (**ts**). 
Mercury delivers promising speedups. The results also show different behaviors 
according to the model.  For instance, Mercury efficiency may vary between 90% 
(Hanoi model) and 51% (Kanban model), whereas the system occupancy  is consistently 
over 95%.  Clearly, the algorithm depends on the ``degree of concurrency'' of the 
model -- it is not necessary to use lots of processors for a model with few concurrent 
actions -- but this is an inherent limitation with parallel state space construction [EL08](http://www.sciencedirect.com/science/article/pii/S1571066108000704), 
which is an irregular problem.

![alt text][image1]

Concerning the use of memory, we can measure the quality of the distribution of the 
state space using the *mean standard deviation* (*sigma*) of the number of states among 
the processors. In our experiments, we observe that the value of *sigma* is quite small 
and that it stays stable when we change the number of processors. For instance, we have 
*sigma* ~ 1.5% for the Hanoi model and *sigma* ~ 7% for Kanban. The difference between 
values of *sigma* can be explained by the difference in the ``degree of concurrency''. 
It may also be affected by the processor's performance, that is, a processor that handles 
``simpler states''--- states whose transition firing involves a small number of operations 
---may dynamically assign more states than others. Finally, our experiments are also 
affected by the Non-Uniform Memory Access (NUMA) architecture of our  machine, where 
the latency and bandwidth characteristics of memory actions depend on the processor 
or memory region being accessed. 

# History and Technical Details

I started developing Mercury in 2009 as part of my Ph.D. thesis at LAAS (Toulouse 
France) under the supervision of <NAME> and <NAME>. My main 
motivation was to implement a simple but powerful model checker engine to experiment 
different algorithms for Parallel Model Checking. It is implemented using the C language 
with Pthreads for concurrency and the Hoard Library for parallel memory allocation.  
It uses the work-stealing strategy for work-load and most of the data structures 
(hash tables, stacks, list, avl trees, etc) were specially developed for Mercury in 
order to obtain the best performance as possible.

# Contact

	<NAME>
	<EMAIL> 

# Instalation

To run this project, you first need to compile the code. After the code is compiled, <commit_msg>doc: change README<commit_after># Description

[//]: # (Image References)

[image1]: doc/images/lt_ratio_speedup.png "Speedup analysis" 

Mercury is a high performance Model Checker developed for multicore, multiprocessors 
machine with shared memory. It is a state-of-the art Model Checking playground specially 
developed to experiment different approaches for  Parallel State Space construction  
(graph traversal)  and Parallel Model Checking of temporal formulas.

Mercury has been developed to be highly modular and extensible. The software is 
composed of separate, interchangeable modules that accept different memory layouts 
(shared/local data) and synchronization mechanisms.

Moreover, the software view of states is abstract and can be easily extended to 
take into account data structures and time classes. Altogether, we experimented 
several versions, two for probabilistic, four for exhaustive state space construction 
and three for parallel model checking (subset of CTL formulas).

For more information, check [Mercury's homepage](https://rodrigotaclasaad.wordpress.com/mercury/)

# Features:

1. Parallel State Space Exploration
   - Reachability analysis (see [ISPDC2011](https://rodrigotaclasaad.wordpress.com/2017/09/05/mixed-shared-distributed-hash-tables-approaches-for-parallel-state-space-construction/)
   - Local Sub-CTL Model Checking (see [ATVA2012](https://rodrigotaclasaad.wordpress.com/2017/09/05/an-experiment-on-parallel-model-checking-of-a-ctl-fragment/))
2. Probabilistic State Space Exploration
   - Reachability analysis
3. NEW: Disc based State Space Exploration (in ALFA, not stable)
   - Currently, supports only the state space exploration (prints the number of states and transitions);
   - The state space and the exploration stacks are partitioned on the hard disk;
   - Coming soon: Reachability analysis

# Benchmark (Speedup)

In Figure 1 we give the observed speedup of Mercury on a set of examples.  We give 
the absolute speedup, measured as the ratio between the execution time using **n** 
processors (**tn**) and the time of an optimized, sequential version (**ts**). 
Mercury delivers promising speedups. The results also show different behaviors 
according to the model.  For instance, Mercury efficiency may vary between 90% 
(Hanoi model) and 51% (Kanban model), whereas the system occupancy  is consistently 
over 95%.  Clearly, the algorithm depends on the ``degree of concurrency'' of the 
model -- it is not necessary to use lots of processors for a model with few concurrent 
actions -- but this is an inherent limitation with parallel state space construction [EL08](http://www.sciencedirect.com/science/article/pii/S1571066108000704), 
which is an irregular problem.

![alt text][image1]

Concerning the use of memory, we can measure the quality of the distribution of the 
state space using the *mean standard deviation* (*sigma*) of the number of states among 
the processors. In our experiments, we observe that the value of *sigma* is quite small 
and that it stays stable when we change the number of processors. For instance, we have 
*sigma* ~ 1.5% for the Hanoi model and *sigma* ~ 7% for Kanban. The difference between 
values of *sigma* can be explained by the difference in the *degree of concurrency*. 
It may also be affected by the processor's performance, that is, a processor that handles 
*simpler states* --- states whose transition firing involves a small number of operations 
--- may dynamically assign more states than others. Finally, our experiments are also 
affected by the Non-Uniform Memory Access (NUMA) architecture of our  machine, where 
the latency and bandwidth characteristics of memory actions depend on the processor 
or memory region being accessed. 

# History and Technical Details

I started developing Mercury in 2009 as part of my Ph.D. thesis at LAAS (Toulouse 
France) under the supervision of <NAME> and <NAME>. My main 
motivation was to implement a simple but powerful model checker engine to experiment 
different algorithms for Parallel Model Checking. It is implemented using the C language 
with Pthreads for concurrency and the Hoard Library for parallel memory allocation.  
It uses the work-stealing strategy for work-load and most of the data structures 
(hash tables, stacks, list, avl trees, etc) were specially developed for Mercury in 
order to obtain the best performance as possible.

# Contact

	<NAME>
	<EMAIL> 

# Instalation

To run this project, you first need to compile the code. After the code is compiled, 
{'fraction_non_alphanumeric': 0.0590954110267415, 'fraction_numerical': 0.013425773082425443, 'mean_word_length': 4.59950708564387, 'pattern_counts': {'":': 0, '<': 11, '<?xml version=': 0, '>': 11, 'https://': 6, 'lorem ipsum': 0, 'www.': 2, 'xml': 0}, 'pii_count': 0, 'substrings_counts': 0, 'word_list_counts': {'cursed_substrings.json': 0, 'profanity_word_list.json': 0, 'sexual_word_list.json': 0, 'zh_pornsignals.json': 0}}
{'dir': 'git-commits-cleaned', 'id': '1706409', 'n_tokens_mistral': 2467, 'n_tokens_neox': 2260, 'n_words': 1200}