File size: 2,818 Bytes
af91e01
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
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
#!/usr/bin/env python3
"""Differential test: the browser's cycle detection vs `gridlock`, on random graphs.

    python3 differential_test.py            # needs node and gridlock installed

The page reimplements gridlock's decision procedure in JavaScript so it can run with nothing
uploaded. A reimplementation is a second chance to be wrong, and a visualiser that disagrees with
the tool it advertises is worse than no visualiser — so the two are checked against each other
rather than assumed to agree.

Last run on this machine: 400 random graphs, gridlock found a cycle in 343, DISAGREEMENTS: 0.
"""
import json
import random
import re
import subprocess
import sys
import tempfile
import os

HERE = os.path.dirname(os.path.abspath(__file__))


def extract_js() -> str:
    html = open(os.path.join(HERE, "index.html"), encoding="utf-8").read()
    js = html.split("<script>")[1].split("</script>")[0]
    return js[js.index("function findCycle"):js.index("function draw")]


def main() -> int:
    try:
        from gridlock.core import WaitForGraph, certify
    except ImportError:
        print("gridlock is not installed: pip install gridlock", file=sys.stderr)
        return 2
    if subprocess.run(["node", "--version"], capture_output=True).returncode != 0:
        print("node is not available", file=sys.stderr)
        return 2

    rng = random.Random(11)
    cases = []
    for _ in range(400):
        keys = [f"n{i}" for i in range(rng.randint(0, 12))]
        g = {k: [] for k in keys}
        for k in keys:
            for _ in range(rng.randint(0, 3)):
                if keys:
                    g[k].append(rng.choice(keys))
        cases.append(g)

    d = tempfile.mkdtemp()
    cases_path = os.path.join(d, "cases.json")
    json.dump(cases, open(cases_path, "w"))
    script = extract_js() + """
const fs = require('fs');
const cases = JSON.parse(fs.readFileSync(process.argv[2], 'utf8'));
console.log(JSON.stringify(cases.map(g => findCycle(normalise(g)))));
"""
    js_path = os.path.join(d, "t.js")
    open(js_path, "w").write(script)
    out = subprocess.run(["node", js_path, cases_path], capture_output=True, text=True)
    if out.returncode != 0:
        print(out.stderr, file=sys.stderr)
        return 2
    js_results = json.loads(out.stdout)

    mismatches, with_cycle = 0, 0
    for g, jc in zip(cases, js_results):
        py = certify(WaitForGraph.from_mapping(g)).cycle
        with_cycle += py is not None
        if (py is not None) != (jc is not None):
            mismatches += 1
            print(f"DISAGREE on {g}\n  gridlock: {py}\n  browser:  {jc}")
    print(f"{len(cases)} random graphs | gridlock found a cycle in {with_cycle} | "
          f"DISAGREEMENTS: {mismatches}")
    return 1 if mismatches else 0


if __name__ == "__main__":
    sys.exit(main())