LockServer/tla_trace_validation.py at main · tracevalidation/LockServer · GitHub

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
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
import os
import argparse
from subprocess import Popen

# Path to TLA installation
tla_dir = "/opt/TLAToolbox-1.8.0-nightly/toolbox"
tla_jar = os.path.join(tla_dir, "tla2tools.2.18.jar")
community_modules_jar = os.path.join(tla_dir, "CommunityModules-deps.2.18.jar")
tla_cp = f"{tla_jar}:{community_modules_jar}"

# Run TLC
def run_tla(trace_spec,trace="trace.ndjson",config="conf.ndjson",dfs=False):
    os.environ["TRACE_PATH"] = trace
    os.environ["CONFIG_PATH"] = config
    if dfs:
        tla_trace_validation_process = Popen([
            "java",
            "-XX:+UseParallelGC",
            "-Dtlc2.tool.impl.Tool.cdot=true",
            "-Dtlc2.tool.queue.IStateQueue=StateDeque",
            "-cp",
            tla_cp,
            "tlc2.TLC",
            "-note",
            "-dump",
            "dot,snapshot,colorize,actionlabel,constrained",
            "TD.dot",
            trace_spec])
    else:
        tla_trace_validation_process = Popen([
            "java",
            "-XX:+UseParallelGC",
            "-Dtlc2.tool.impl.Tool.cdot=true",
            "-cp",
            tla_cp,
            "tlc2.TLC",
            "-note",
            "-dump",
            "dot,snapshot,colorize,actionlabel,constrained",
            "TD.dot",
            # "java",
            # "-XX:+UseParallelGC",
            # "-cp",
            # tla_cp,
            # "tlc2.TLC",
            # "-note",
            trace_spec])
    tla_trace_validation_process.wait()
    tla_trace_validation_process.terminate()

if __name__ == "__main__":
    # Read program args
    parser = argparse.ArgumentParser(description="")
    parser.add_argument('spec', type=str, help="Specification file")
    parser.add_argument('--trace', type=str, required=False, default="trace.ndjson", help="Trace file")
    parser.add_argument('--config', type=str, required=False, default="conf.ndjson", help="Config file")
    # parser.add_argument('-dfs', '--dfs', type=bool, action=argparse.BooleanOptionalAction, help="breadth-first search")
    parser.add_argument('-dfs', '--dfs', default=False, action=argparse.BooleanOptionalAction, help="breadth-first search")
    args = parser.parse_args()
    # Run
    run_tla(args.spec,args.trace,args.config,args.dfs)