Specification-Narrowing/optimal.py at main · haslab/Specification-Narrowing · 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
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
96
97
import sys
from timeit import default_timer as timer
from itertools import combinations
from alloy import parse, build_instance, print_instances

import jpype
import jpype.imports

if not jpype.isJVMStarted():
    jpype.startJVM(classpath=["AlloyMax-1.0.2.jar"])

from edu.mit.csail.sdg.parser import CompUtil
from edu.mit.csail.sdg.translator import A4Options, TranslateAlloyToKodkod

def optimal_test_set(content, scope):
    collector = parse(content)

    model = "sig Atom {}\nabstract sig Formula {}\none sig " + ",".join(collector.predicates.keys()) + " extends Formula {}\nsig Instance {\n"

    for sig in sorted(collector.signatures):
        model += "\t" + sig + " : set Atom,\n"
    for field, typ in collector.fields.items():
        arity = typ.count("->") + 1
        model += "\t" + field + " : " + " -> ".join(["Atom"] * arity) + ",\n"
    model += "\tvalid : set Formula\n} {\n"

    for sig in sorted(collector.toplevel):
        model += "\t#" + sig + " <= " + str(scope) + "\n"
    for sig, parent in collector.subsets.items():
        model += "\t" + sig + " in " + parent + "\n"
    for a,b in combinations(sorted(collector.toplevel), 2):
        model += "\tno " + a + " & " + b + "\n"
    for sig in sorted(collector.abstract):
        model += "\t" + sig + " = " + " + ".join(collector.extensions.get(sig, [])) + "\n"
    for sig in collector.extensions:
        for a,b in combinations(collector.extensions[sig], 2):
            model += "\tno " + a + " & " + b + "\n"
    for sig, mult in collector.multiplicities.items():
        model += "\t"+ mult + " " + sig + "\n"
    for field, typ in collector.fields.items():
        model += "\t" + field + " in " + typ + "\n"

    for formula in collector.facts.values():
        model += "\t{" + formula + "}\n"

    for pred,formula in collector.predicates.items():
        model += "\t" + pred + " in valid iff {" + formula + "\n\t}\n"


    model += "}\nrun {\n\tall disj f,g : Formula | some i : Instance | f in i.valid iff g not in i.valid\n\tminsome Instance} for " + str(scope*len(collector.toplevel)) + " Atom, " + str(len(collector.predicates)-1) + " Instance\n"

    world = CompUtil.parseEverything_fromString(None,model)
    command = world.getAllCommands()[0]
    options = A4Options()
    options.solver = A4Options.SatSolver.SAT4JMax
    solution = TranslateAlloyToKodkod.execute_command(None, world.getAllReachableSigs(), command, options)
    if not solution.satisfiable():
        print("Some predicates are equivalent.")
        return []

    # build formulas for instances
    instances = []
    full_value = {}
    for sig in collector.signatures:
        full_value[sig] = solution.eval(CompUtil.parseOneExpression_fromString(world, sig))
    for field in collector.fields:
        full_value[field] = solution.eval(CompUtil.parseOneExpression_fromString(world, field))
    for tuple in solution.eval(CompUtil.parseOneExpression_fromString(world, "Instance")):
        id = tuple.atom(0)
        value = {}
        for sig in collector.signatures:
            value[sig] = [[t.atom(1)] for t in full_value[sig] if t.atom(0) == id]
        for field in collector.fields:
            value[field] = [[t.atom(i) for i in range(1, t.arity())] for t in full_value[field] if t.atom(0) == id]
        instances.append(build_instance(collector, value))
    return instances


def main():
        # check command line arguments
    if len(sys.argv) != 3:
        print("Usage: python parser.py <filename> <scope>")
        sys.exit(1)

    filename = sys.argv[1]
    scope = int(sys.argv[2])

    with open(filename,'r') as file:
        content = file.read()
        start = timer()
        test_set = optimal_test_set(content, scope)
        end = timer()
        print(f"// Generated {len(test_set)} test cases in {end - start} seconds")
        print_instances(test_set, scope)

if __name__ == "__main__":
    main()