ccs 0.1.0

A simple implementation of the Calculus of Communicating Systems by Robin Milner
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
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95

import json
import os
import re
import subprocess
import sys

LTS_FILE_NAME = "/tmp/benchmark.ccs"
USE_PAIGE_TARJAN = True


def bench(binary: str, step_width: int, nsteps: int, use_pt: bool):
    pt_times = []
    for s in range(step_width, step_width * nsteps + 1, step_width):
        for t in range(step_width, step_width * nsteps + 1, step_width):
            pt = measure_time(binary, s, t, use_pt)
            pt_times.append((s, t, pt))
            print(f"finished {s}x{t}", file=sys.stderr)

    return pt_times

def measure_time(binary: str, states: int, transitions: int, pt: bool) -> float:
    subprocess.call(f"{binary} random-lts -s {states} -t {transitions} -a 1 >{LTS_FILE_NAME}", shell=True)

    if pt:
        algo = "paige-tarjan"
    else:
        algo = "naive"
    args = [binary, "bisimilarity", "-b", "-a", algo, LTS_FILE_NAME]
    result = subprocess.run(args, stdout=subprocess.PIPE)
    result = result.stdout.decode("utf-8")
    #todo maybe check if both bisimilarities are equal
    pattern = r"took (\d+\.?\d*\S*)"

    match = re.search(pattern, result)
    if match is None:
        raise ValueError("regex didnt match" + result)

    pt_time = parse_time(match.group(1))

    os.remove(LTS_FILE_NAME)

    return pt_time

def parse_time(time:str) -> float:
    nano = re.match(r"(\d+\.?\d+)ns", time)
    if not nano is None:
        return float(nano.group(1)) * 1e-9

    micro = re.match(r"(\d+\.?\d+)µs", time)
    if not micro is None:
        return float(micro.group(1)) * 1e-6

    milli = re.match(r"(\d+\.?\d+)ms", time)
    if not milli is None:
        return float(milli.group(1)) * 1e-3

    seconds = re.match(r"(\d+\.?\d+)s", time)
    if not seconds is None:
        return float(seconds.group(1))

    raise ValueError("unexpected time format " + time)


def usage():
    print("Usage:");
    print(f"  {sys.argv[0]} [binary] [step_width] [nsteps]");
    pass

def main():
    binary = "./target/release/ccs"
    step_width = 100000
    nsteps = 10
    outfile = "benchmark.json"

    if "-h" in sys.argv or "--help" in sys.argv or "help" in sys.argv:
        usage()
        return

    if len(sys.argv) > 1:
        binary = sys.argv[1]
    if len(sys.argv) > 2:
        step_width = int(sys.argv[2])
    if len(sys.argv) > 3:
        nsteps = int(sys.argv[3])

    print(f"Benchmarking {binary} with {nsteps} steps of width {step_width}")

    data = bench(binary, step_width, nsteps, USE_PAIGE_TARJAN)

    with open(outfile, "w") as write:
        json.dump(data, write)
        print(f"written data to {outfile}", file=sys.stderr)

if __name__ == '__main__':
    main()