\subsection options_concurrency_limit Concurrency limit
-The maximum number of variables in a system can be tuned through
-the \b maxmin/concurrency_limit item (default value: 100). Setting a higher value can lift some limitations, such as the number of concurrent processes running on a single host.
+The maximum number of variables per resource can be tuned through
+the \b maxmin/concurrency-limit item. The default value is -1, meaning that
+there is no such limitation. You can have as many simultaneous actions per
+resources as you want. If your simulation presents a very high level of
+concurrency, it may help to use e.g. 100 as a value here. It means that at
+most 100 actions can consume a resource at a given time. The extraneous actions
+are queued and wait until the amount of concurrency of the considered resource
+lowers under the given boundary.
+
+Such limitations help both to the simulation speed and simulation accuracy
+on highly constrained scenarios, but the simulation speed suffers of this
+setting on regular (less constrained) scenarios so it is off by default.
\subsection options_model_network Configuring the Network model
* none: Do not apply any kind of reduction (mandatory for now for
liveness properties)
* dpor: Apply Dynamic Partial Ordering Reduction. Only valid if you
- verify local safety properties.
+ verify local safety properties (default value for safety checks).
\subsection options_modelchecking_visited model-check/visited, Cycle detection
- \c host/model: \ref options_model_select
- \c maxmin/precision: \ref options_model_precision
+- \c maxmin/concurrency-limit: \ref options_concurrency_limit
- \c msg/debug-multiple-use: \ref options_msg_debug_multiple_use
