blob: 504d428fbf24cfe5462fa8829e4c75c3d7621600 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
|
"""The unittest.TestCase for model-checking TLA+ specifications."""
import os
from . import interface
from ... import core
class TLAPlusTestCase(interface.ProcessTestCase):
"""A TLA+ specification to model-check."""
REGISTERED_NAME = "tla_plus_test"
def __init__(self, logger, model_config_file, java_binary=None):
"""Initialize the TLAPlusTestCase with a TLA+ model config file.
model_config_file is the full path to a file like
src/mongo/db/repl/tla_plus/MongoReplReconfig/MCMongoReplReconfig.cfg.
java_binary is the full path to the "java" program, or None.
"""
message = f"Path '{model_config_file}' doesn't" \
f" match **/<SpecName>/MC<SpecName>.cfg"
# spec_dir should be like src/mongo/db/repl/tla_plus/MongoReplReconfig.
spec_dir, filename = os.path.split(model_config_file)
if not (spec_dir and filename):
raise ValueError(message)
# working_dir is like src/mongo/db/repl/tla_plus.
self.working_dir, specname = os.path.split(spec_dir)
if not specname or filename != f'MC{specname}.cfg':
raise ValueError(message)
self.java_binary = java_binary
interface.ProcessTestCase.__init__(self, logger, "TLA+ test", specname)
def _make_process(self):
process_kwargs = {"cwd": self.working_dir}
if self.java_binary is not None:
process_kwargs["env_vars"] = {"JAVA_BINARY": self.java_binary}
return core.programs.generic_program(self.logger, ["sh", "model-check.sh", self.test_name],
process_kwargs=process_kwargs)
|
