Small bug fixes for QuaTEx and macOS

README.md

@@ -205,7 +205,11 @@ as described in the model checkers' [manual](https://maude.ucm.es/strategies/mod
 References
 ----------
 
-More details about the integration of the external classical model checkers can be found
-in [*Strategies, model checking and branching-time properties in Maude*](https://doi.org/10.1016/j.jlamp.2021.100700)
-and in [*Model checking of strategy-controlled systems in rewriting logic*](https://hdl.handle.net/20.500.14352/3553).
-Support for quantitative model checking is described in [*QMaude: quantitative specification and verification in rewriting logic*](https://doi.org/10.1007/978-3-031-27481-7_15).
+More details about the integration of the external classical model checkers can be found in
+[*Strategies, model checking and branching-time properties in Maude*](https://doi.org/10.1016/j.jlamp.2021.100700)
+(arXived [here](https://doi.org/10.48550/arXiv.2401.07680)) and in
+[*Model checking of strategy-controlled systems in rewriting logic*](https://hdl.handle.net/20.500.14352/3553)
+(arXived [here](https://doi.org/10.48550/arXiv.2401.07616)).
+Support for quantitative model checking is described in
+[*QMaude: quantitative specification and verification in rewriting logic*](https://doi.org/10.1007/978-3-031-27481-7_15)
+(archived [here](https://hdl.handle.net/20.500.14352/101033)).

pyproject.toml

@@ -1,6 +1,6 @@
 [project]
 name            = 'umaudemc'
-version         = '0.13.0'
+version         = '0.13.1'
 description     = 'Unified Maude model-checking utility'
 license.text    = 'GPLv3'
 classifiers     = [

umaudemc/__init__.py

@@ -1 +1 @@
-__version__ = '0.12.2'
+__version__ = '0.13.1'

umaudemc/simulators.py

@@ -79,8 +79,9 @@ def rval(self, observation):
 		if not t:
 			t, var = parse_hole_term(self.module, observation)
 			self.obs_cache[observation] = (t, var)
-		subs = maude.Substitution({var: self.state})
-		t = subs.instantiate(t)
+		if var is not None:
+			subs = maude.Substitution({var: self.state})
+			t = subs.instantiate(t)
 		t.reduce()
 
 		return float(t == self.true) if t.getSort() == self.bool_sort else float(t)

umaudemc/statistical.py

@@ -221,6 +221,7 @@ def thread_main(program, qdata, simulator, num_sims, block_size, seed, queue, ba
 def run_parallel(program, qdata, num_sims, max_sim, simulator, alpha, delta, block_size, jobs, verbose=False):
 	"""Run the simulation in multiple threads"""
 	import multiprocessing as mp
+	mp.set_start_method('fork', force=True)
 
 	# When the number of jobs is zero or negative, we take the CPU count
 	if jobs <= 0: